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)
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.