class_docstr: This is a prover decorator that adds unique names assumptions before
  proving.
class_docstr_tok: ["This","is","a","prover","decorator","that","adds","unique","names","assumptions","before","proving","."]
docstr: - Domain = union([e.free()|e.constants() for e in all_expressions])
  - if "d1 = d2" cannot be proven from the premises, then add "d1 != d2"
docstr_tok: ["-","Domain","=","union","(","[","e.free","(",")","|e.constants","(",")","for","e","in","all_expressions","]",")","-","if","``","d1","=","d2","''","can","not","be","proven","from","the","premises",",","then","add","``","d1","!","=","d2","''"]
code: def assumptions(self):
      """
      - Domain = union([e.free()|e.constants() for e in all_expressions])
      - if "d1 = d2" cannot be proven from the premises, then add "d1 != d2"
      """
      assumptions = self._command.assumptions()
  
      domain = list(get_domain(self._command.goal(), assumptions))
  
      # build a dictionary of obvious equalities
      eq_sets = SetHolder()
      for a in assumptions:
          if isinstance(a, EqualityExpression):
              av = a.first.variable
              bv = a.second.variable
              # put 'a' and 'b' in the same set
              eq_sets[av].add(bv)
  
      new_assumptions = []
      for i, a in enumerate(domain):
          for b in domain[i + 1 :]:
              # if a and b are not already in the same equality set
              if b not in eq_sets[a]:
                  newEqEx = EqualityExpression(
                      VariableExpression(a), VariableExpression(b)
                  )
                  if Prover9().prove(newEqEx, assumptions):
                      # we can prove that the names are the same entity.
                      # remember that they are equal so we don't re-check.
                      eq_sets[a].add(b)
                  else:
                      # we can't prove it, so assume unique names
                      new_assumptions.append(-newEqEx)
  
      return assumptions + new_assumptions
  
imports: from collections import defaultdict
  from functools import reduce
  from nltk.inference.api import Prover, ProverCommandDecorator
  from nltk.inference.prover9 import Prover9, Prover9Command
  from nltk.sem.logic import AbstractVariableExpression, AllExpression, AndExpression, ApplicationExpression, BooleanExpression, EqualityExpression, ExistsExpression, Expression, ImpExpression, NegatedExpression, Variable, VariableExpression, operator, unique_variable
label_desc: Use image node_id 1 for calling the UniqueNamesProver obj's underlying member method code with example usage: obj.assumptions() and returns: unknown