#NEWLINE# def assumptions( self ) : #NEWLINE# #INDENT# assumptions = self . _command . assumptions ( ) #NEWLINE# predicates = self . _make_predicate_dict ( assumptions ) #NEWLINE# new_assumptions = [ ] #NEWLINE# for p in predicates : #NEWLINE# #INDENT# predHolder = predicates [ p ] #NEWLINE# new_sig = self . _make_unique_signature ( predHolder ) #NEWLINE# new_sig_exs = [ VariableExpression ( v ) for v in new_sig ] #NEWLINE# disjuncts = [ ] #NEWLINE# for sig in predHolder . signatures : #NEWLINE# #INDENT# equality_exs = [ ] #NEWLINE# for ( v1 , v2 ) in zip ( new_sig_exs , sig ) : #NEWLINE# #INDENT# equality_exs . append ( EqualityExpression ( v1 , v2 ) ) #NEWLINE# #UNINDENT# disjuncts . append ( reduce ( ( lambda x , y : ( x & y ) ) , equality_exs ) ) #NEWLINE# #UNINDENT# for prop in predHolder . properties : #NEWLINE# #INDENT# bindings = { #NEWLINE# #INDENT# #NEWLINE# #UNINDENT# } #NEWLINE# for ( v1 , v2 ) in zip ( new_sig_exs , prop [ 0 ] ) : #NEWLINE# #INDENT# bindings [ v2 ] = v1 #NEWLINE# #UNINDENT# disjuncts . append ( prop [ 1 ] . substitute_bindings ( bindings ) ) #NEWLINE# #UNINDENT# if disjuncts : #NEWLINE# #INDENT# antecedent = self . _make_antecedent ( p , new_sig ) #NEWLINE# consequent = reduce ( ( lambda x , y : ( x | y ) ) , disjuncts ) #NEWLINE# accum = ImpExpression ( antecedent , consequent ) #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# accum = NegatedExpression ( self . _make_antecedent ( p , new_sig ) ) #NEWLINE# #UNINDENT# for new_sig_var in new_sig [ : : ( - 1 ) ] : #NEWLINE# #INDENT# accum = AllExpression ( new_sig_var , accum ) #NEWLINE# #UNINDENT# new_assumptions . append ( accum ) #NEWLINE# #UNINDENT# return ( assumptions + new_assumptions )