docs: def message(self, tree, spins, subtheta, auxvars):
          """Determine the energy of the elimination tree.
  
          Args:
              tree (dict): The current elimination tree
              spins (dict): The current fixed spins
              subtheta (dict): Theta with spins fixed.
              auxvars (dict): The auxiliary variables for the given spins.
  
          Returns:
              The formula for the energy of the tree.
  
          """
          energy_sources = set()
          for v, children in tree.items():
              aux = auxvars[v]
  
              assert all(u in spins for u in self._ancestors[v])
  
              # build an iterable over all of the energies contributions
              # that we can exactly determine given v and our known spins
              # in these contributions we assume that v is positive
              def energy_contributions():
                  yield subtheta.linear[v]
  
                  for u, bias in subtheta.adj[v].items():
                      if u in spins:
                          yield SpinTimes(spins[u], bias)
  
              plus_energy = Plus(energy_contributions())
              minus_energy = SpinTimes(-1, plus_energy)
  
              # if the variable has children, we need to recursively determine their energies
              if children:
                  # set v to be positive
                  spins[v] = 1
                  plus_energy = Plus(plus_energy, self.message(children, spins, subtheta, auxvars))
                  spins[v] = -1
                  minus_energy = Plus(minus_energy, self.message(children, spins, subtheta, auxvars))
                  del spins[v]
  
              # we now need a real-valued smt variable to be our message
              m = FreshSymbol(REAL)
  
              ancestor_aux = {auxvars[u] if spins[u] > 0 else Not(auxvars[u])
                              for u in self._ancestors[v]}
              plus_aux = And({aux}.union(ancestor_aux))
              minus_aux = And({Not(aux)}.union(ancestor_aux))
  
              self.assertions.update({LE(m, plus_energy),
                                      LE(m, minus_energy),
                                      Implies(plus_aux, GE(m, plus_energy)),
                                      Implies(minus_aux, GE(m, minus_energy))
                                      })
  
              energy_sources.add(m)
  
          return Plus(energy_sources)