code: def message_upperbound(self, tree, spins, subtheta):
          
          energy_sources = set()
          for v, subtree in tree.items():
  
              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 Times(limitReal(spins[u]), bias)
  
              energy = Plus(energy_contributions())
  
              # if there are no more variables in the order, we can stop
              # otherwise we need the next message variable
              if subtree:
                  spins[v] = 1.
                  plus = self.message_upperbound(subtree, spins, subtheta)
                  spins[v] = -1.
                  minus = self.message_upperbound(subtree, spins, subtheta)
                  del spins[v]
              else:
                  plus = minus = limitReal(0.0)
  
              # we now need a real-valued smt variable to be our message
              m = FreshSymbol(REAL)
  
              self.assertions.update({LE(m, Plus(energy, plus)),
                                      LE(m, Plus(Times(energy, limitReal(-1.)), minus))})
  
              energy_sources.add(m)
  
          return Plus(energy_sources)
docs: Determine an upper bound on 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.
  
          Returns:
              The formula for the energy of the tree.