from dparser import Parser import os import sys import math import numpy import scipy import scipy.linalg ''' Description of the data structure: Var: Class{name: String; usedby: AFmla List; usedby_solvedform: (MyRep,MyRep)-List } AFmla: Class{ op: String; lhs,rhs,p: MyRep } MyRep: Class{ p: [Num,Dict:Var->Num] List } Removing variables attribute from class MyRep... ''' def d_source_text(s, nodes): "source_text: sexpr*" return s[0] def d_sexpr(s, nodes): "sexpr: str | '(' sexpr* ')'" if len(s) == 1: return s[0] else: return s[1] def d_str(t, s, nodes): 'str : "[a-zA-Z0-9_=+*-:]*"' return s[0].strip() def main(): global multilinear multilinear = True sys.setrecursionlimit(2500) ####DEBUG print sys.argv[0] ####DEBUG print sys.argv[1] args = sys.argv[1:] filename = args[0] if filename == 'test': return test() return sat_check(filename) def sat_check(filename, expected_answer = ''): if not(os.path.isfile(filename)): print "**ERROR**: File does not exist. Quitting." with open(filename, 'r') as f: x = f.read() y = Parser().parse(x) z = y.getStructure() answer = process_list_of_sexprs(z) if expected_answer != '': if answer == expected_answer: print "***Test {0} PASSED.".format(filename) else: print "**ERROR**: Test {0} FAILED.".format(filename) ####DEBUG print answer return answer def test(): "test the procedure on all benchmark examples" sat_check('test1.smt2', 'SATISFIABLE') sat_check('test2.smt2', 'SATISFIABLE') sat_check('test3.smt2', 'SATISFIABLE') sat_check('test4.smt2', 'SATISFIABLE') sat_check('test5.smt2', 'SATISFIABLE') sat_check('test6.smt2', 'SATISFIABLE') sat_check('test7.smt2', 'UNSATISFIABLE') sat_check('test8.smt2', 'SATISFIABLE') sat_check('test9.smt2', 'SATISFIABLE') sat_check('test10.smt2', 'SATISFIABLE') sat_check('cubeS.smt2', 'SATISFIABLE') sat_check('div_mod.smt2', 'SATISFIABLE') sat_check('div_modS.smt2', 'SATISFIABLE') sat_check('gcd_lcm.smt2', 'SATISFIABLE') sat_check('gcd_lcmS.smt2', 'SATISFIABLE') sat_check('product.smt2', 'SATISFIABLE') sat_check('product2.smt2', 'SATISFIABLE') sat_check('product2S.smt2', 'SATISFIABLE') sat_check('productS.smt2', 'SATISFIABLE') sat_check('productSY.smt2', 'SATISFIABLE') sat_check('root2.smt2', 'SATISFIABLE') sat_check('root2S.smt2', 'SATISFIABLE') sat_check('squareS.smt2', 'SATISFIABLE') class Var: def __init__(self, name): "variable" self.name = name self.usedby = [] self.usedby_solvedform = [] def add(self, e): if e not in self.usedby: self.usedby.append(e) def toStr(self): return self.name class AFmla: def __init__(self): "atomic formula self.p op 0...or lhs op rhs" self.op, self.lhs, self.rhs, self.p = None, None, None, None def __init__(self, op, lhs, rhs): "atomic formula" self.op, self.lhs, self.rhs = op, lhs, rhs rhs_copy = self.rhs.myrep_copy() rhs_copy.myrep_minus() lhs_copy = self.lhs.myrep_copy() lhs_copy.myrep_add1( rhs_copy ) self.p = lhs_copy def contains_variable(self, v): return self.lhs.contains_variable(v) or self.rhs.contains_variable(v) def setLevel(self, level): self.level = level self.history = [(level,self.p)] def solve_for(self, v): '''return a,b s.t. this.assertion == (a*v = b) (la, lb) = self.lhs.solve_for(v) # la*v + lb = self.lhs (ra, rb) = self.rhs.solve_for(v) # ra*v + rb = self.rhs ra.myrep_minus() la.myrep_add1(ra) lb.myrep_minus() rb.myrep_add1(lb) return (la,rb)''' (la, lb) = self.p.solve_for(v) # la*v + lb = self.p rhs = lb.myrep_copy() rhs.myrep_minus() return (la,rhs) def isVarVal(self): "is the formula of the form variable = value?" return self.p.myrep_is_ax_plus_b() def getVarVal(self): return self.p.myrep_getVarVal() def replaceVarByVal(self, var, val, level): if self.level == -1: return None elif not self.p.contains_variable(var): return None elif self.level == level: self.p.myrep_replaceVarByVal(var, val) elif self.level < level: self.history.append( (self.level, self.p) ) self.p = self.p.myrep_copy() self.level = level self.p.myrep_replaceVarByVal(var, val) else: assert False, 'Unreachable code reached...check code' return self.isSatisfiable() def backtrack(self, level): '''back to level version of the afmla; return True if successful return False if could not backtrack becoz that level didn't exist''' if self.level <= level: return True for i in range(len(self.history)-1,-1,-1): (tmp_level, tmp_p) = self.history[ i ] if tmp_level <= level and tmp_level >= 0: self.p = tmp_p self.level = tmp_level return True # print 'Delete the assertion' self.history = [] self.p = MyRep('0') self.level = -1 return False def isSatisfiable(self): "return False if self.p is a number and different from 0" val = self.p.myrep_isVal() return val == None or abs(val) < 1e-4 def isTrue(self): "return True if self.p is a number and equal to 0" val = self.p.myrep_isVal() return val != None and abs(val) < 1e-4 def setToTrueAt(self, newlevel): if self.level < newlevel: self.history.append( (self.level, self.p) ) self.p = MyRep('0') self.level = newlevel def toStr(self): #return self.lhs.toStr() + ' = ' + self.rhs.toStr() return self.p.toStr() + ' = 0' class BFmla: def __init__(self, op, afmls): "Boolean combination of atomic formulas" self.op, self.afmls = op, afmls class NFmla: def __init__(self, alist): "NEGATED conjunction of atomic formula" self.alist = alist self.level = 0 # -1 indicates already SATISFIED self.history = self.alist for a in alist: a.setLevel(0) def replaceVarByVal(self, var, val, level): "replace var by val in neg_asserts; return False if detect UNSAT" if self.alist == []: return None # No change else: issata_list = [] for a in self.alist: issata = a.replaceVarByVal(var, val, level) if issata == False: self.level = -1 self.alist = [] return True # is_satisfiable issata_list.append( issata ) if all( [ i == None for i in issata_list ] ): return None # No change self.level = level # There is change, so update level for a in self.alist: if a.isTrue() != True: return True # is_satisfiable and has changed return False # is_unsatisfiable def backtrack(self, level): '''back to level version of the afmla; return True always since backtrack always succeeds in this setting''' if self.level <= level: return True self.alist = self.history for a in self.alist: a.backtrack( level ) return True def toStr(self): #return self.lhs.toStr() + ' = ' + self.rhs.toStr() return 'not(and(', [a.toStr() for a in self.alist], '))' class MyRep: "My representation for polynomials" def __init__(self, f = None, variables = []): if f == None: self.p = None elif isinstance(f, (int, float, long)): v = float(f) self.p = [ [v, {}] ] elif type(f) == str and is_number(f): v = float(f) self.p = [ [v, {}] ] elif isinstance(f, Var): self.p = [ [1, {f:1}] ] elif type(f) == str and is_variable(f, variables): v = is_variable(f, variables) self.p = [ [1, {v:1}] ] else: assert False, 'Dont know how to convert {0}:{1}'.format(f,type(f)) def contains_variable(self, v): def contains_variable_mono(mu, v): return mu.has_key(v) def contains_variable_poly(p, v): ans = contains_variable_mono(p[0][1], v) if ans or len(p) == 1: return ans return contains_variable_poly(p[1:],v) if len(self.p) == 0: return False return contains_variable_poly(self.p, v) def solve_for(self, v): "a*v + b = self.p" global multilinear a = MyRep('0', []) b = MyRep('0', []) for mono in self.p: if mono[1].has_key(v): #assert mono[1][v] == 1, "Variable {0} not linear in mono {1}".format(v.toStr(),mono) if mono[1][v] != 1: # print "***NOT MULTILINEAR; e.g. {0}".format(v.toStr(),mono) #if multilinear: #print "***NOT MULTILINEAR; e.g. {1}".format(v.toStr(),mono) multilinear = False return (MyRep('0'),MyRep('0')) new_pp = mono[1].copy() new_pp.pop(v) a.myrep_add2( [mono[0], new_pp] ) else: b.myrep_add2(mono) return (a, b) def myrep_isVal(self): "return True if self.p is equivalent to a constant b" if len(self.p) > 1: return None if len(self.p) == 0: return 0 if len(self.p[0][1]) != 0: return None return self.p[0][0] def myrep_is_ax_plus_b(self): "return True if self.p is equivalent to a*var+b" def mono_degree_atmost_one(mono): if len(mono[1]) > 1: return False for (k,v) in mono[1].items(): if v > 1: return False return True if len(self.p) > 2: return False if len(self.p) == 1: return mono_degree_atmost_one(self.p[0]) if len(self.p) == 2: if not(mono_degree_atmost_one(self.p[0]) and mono_degree_atmost_one(self.p[1])): return False return len(self.p[0][1]) == 0 or len(self.p[1][1]) == 0 def myrep_getVarVal(self): "return (var,val) if self.p is equivalent to 1*var-val; assuming is_ax_plus_b is TRUE" ####DEBUG assert len(self.p) <= 2, 'Poly not of the form ax+b' a, b, var = 0, 0, None for mono in self.p: if len(mono[1]) == 0: b = b + mono[0] else: ####DEBUG assert var == None, 'Poly not of the form ax+b' a = mono[0] var = mono[1].keys()[0] ####DEBUG assert a != 0, 'Poly a*x+b has a = 0' return (var, b/a) def myrep_replaceVarByVal(self, var, val): "var is a Variable, val is a number, replace in p destructively; not in lhs, rhs" strtmp = 'replacing var {0} by val {1} in {2}'.format(var.toStr(), val, self.toStr()) ans = [] for i in range(len(self.p)-1,-1,-1): mono = self.p[i] if mono[1].has_key(var): del self.p[i] value = math.pow(val, mono[1][var]) coeff = mono[0] * value if abs(coeff) > 1e-4: pp = mono[1].copy() del pp[var] ans.append( [coeff, pp] ) for mono in ans: self.myrep_add2(mono) '''if len(ans) > 0: print strtmp print 'RESULT is {0}'.format(self.toStr())''' def myrep_copy(self): ans = MyRep(None, []) ans.p = [ [i[0], i[1]] for i in self.p ] return ans def myrep_minus(self): "modify self to be -self" for i in self.p: i[0] = -i[0] return self def myrep_add1(self, v2): "modify self to be self+v2, where v2 is a polynomial like me." for i in v2.p: self.myrep_add2(i) def myrep_add2(self, mono): "modify self to be self+mono, where mono is a MONOMIAL." for mono1 in self.p: if mono1[1] == mono[1]: mono1[0] += mono[0] if abs(mono1[0]) < 1e-4: self.p.remove(mono1) return self self.p.append(mono) return self def myrep_add(self, vlist): "modify self to be self+ \sum_v\in vlist v, where vlist=list_of_polynomials_like_me." for i in vlist: self.myrep_add1(i) return self def myrep_mul(self, vlist): "modify self to be self* \Pi_v\in vlist v, where vlist=list_of_polynomials_like_me." for i in vlist: ansObj = self.myrep_mul1(i) self.p = ansObj.p return self def myrep_mul1(self, v2): "modify self to be self*v2, where v2 is a POLYNOMIAL like me." v1list = [ self.myrep_mul2(mono) for mono in v2.p ] return v1list[0].myrep_add(v1list[1:]) def myrep_mul2(self, mono): "do NOT modify self, return a NEW self*mono, where mono is a MONOMIAL." c = mono[0] mu = mono[1] if c == 0: return MyRep('0', []) ansp = [ [ c*i[0], i[1].copy() ] for i in self.p ] for i in ansp: self.myrep_mul3(i[1], mu) ans = MyRep() ans.p = ansp return ans def myrep_mul3(self, mu, nu): "modify mu in place to mu*nu, where both are power-products dicts" for (var, deg) in nu.items(): if mu.has_key(var): mu[var] = mu[var] + deg else: mu[var] = deg def myrep_div(self, p2): "p2 is MODIFIED, but self is not modified!" assert len(p2.p)==1 and p2.p[0][1]=={}, 'Dividing by non-const {0}'.format(p2.p) p2.p[0][0] = 1/p2.p[0][0] return self.myrep_mul1(p2) def toStr(self): return self.toStrP(self.p) def toStrPP(self, mu): "return str representation of power-product mu, which is a dict" ans = '' for (k,v) in mu.items(): if v == 0: continue if ans != '': ans = ans + '*' if v == 1: ans = ans + k.toStr() else: ans = ans + k.toStr() + '**' + str(v) return ans def toStrP(self, p): "return str representation of MyRep polynomial p" if len(p) == 0: return '0' elif len(p) == 1: if p[0][0] == 0: return '0' elif len(p[0][1]) == 0: return str(p[0][0]) else: return str(p[0][0]) + '*' + self.toStrPP(p[0][1]) else: return self.toStrP([p[0]]) + ' + ' + self.toStrP(p[1:]) def process_list_of_sexprs(z): def is_var_decl(i): "check if i is ('declare-fun' var_name '()' 'Real')" return type(i) == list and len(i) == 4 and i[0] == 'declare-fun' and i[3] == 'Real' def is_assert(i): "check if i is ('assert' sexpr)" return type(i) == list and len(i) == 2 and i[0] == 'assert' var_decls = [i for i in z if is_var_decl(i)] # list_of ('declare-fun' var_name '()' 'Real') variables = [ Var(i[1]) for i in var_decls ] variables.reverse() print '--------------------------------------------' print '#Vars = {0}'.format(len(variables), [i.name for i in variables]), assert_decls = [i for i in z if is_assert(i)] print '#fmls = {0}'.format(len(assert_decls)) #for i in assert_decls: #print pp_sexpr(i[1]) # z is a list of sexprs ... asserts, negated_asserts = [], [] for i in assert_decls: my_assert = sexpr2myrep( i[1], variables ) if my_assert != None and type(my_assert) is not list: asserts.append( my_assert ) elif my_assert != None and type(my_assert) is list: negated_asserts.append( my_assert ) else: print 'None assert found' neg_asserts = [NFmla( i) for i in negated_asserts ] '''for i in asserts: print i.toStr() ''' # Now we should setup for iterative depth first search return dfs( [], 0, asserts, [], {}, variables, neg_asserts ) def assign_var_val(answer, level, v, val, variables): '''destructively update answer and variables''' if answer.has_key(level): answer[level][v] = val else: answer[level] = {v:val} variables.remove(v) def GFPeigenCheck( coeffsL, constsL ): '''if constsL_i is NOT LC of coeffs, put i in delete_index; else put the LC coeffs in Amatrix; ASSUME: coeffsL * var = constsL ''' Amatrix, delete_index = [], [] coeffsNP = numpy.matrix( coeffsL ) coeffsNPT = numpy.transpose( coeffsL ) for i in range( len(constsL)-1,-1,-1): const_iNP = numpy.matrix( constsL[i] ) const_iNPT = numpy.transpose( const_iNP) try: #ans = scipy.linalg.solve(coeffsNPT, const_iNPT) (ans,residual,rank,s) = scipy.linalg.lstsq(coeffsNPT, const_iNPT) '''print 'DEBUG: A = {0}, b = {1}'.format(coeffsNPT, const_iNPT) print 'DEBUG: ans = {0}, residual = {1}'.format(ans, residual) print 'DEBUG: rank = {0}, s = {1}'.format(rank, s)''' if not numpy.isscalar(residual): residual = scipy.linalg.norm(const_iNPT-coeffsNPT.dot(ans)) # print 'DEBUG: residual = {0}'.format(residual) if residual < 1e-5 or residual == []: # CHECK, bug in scipy Amatrix.append(numpy.reshape(ans,len(constsL))) else: raise scipy.linalg.LinAlgError except scipy.linalg.LinAlgError: # print 'Coeffs is SINGULAR??' delete_index.append( i ) return (Amatrix, delete_index) def GFPeigenCheckMain( coeffsL, constsL, coeffs, consts, source_asserts ): delete_index = [] while len(constsL) > len(delete_index): # delete from constsL and coeffsLNPT index i's in delete_index for i in delete_index: # scipy.delete( coeffsNPT, i, 1) del coeffsL[ i ], coeffs[ i ], source_asserts[ i ] del constsL[ i ], consts[ i ] Amatrix, delete_index = GFPeigenCheck(coeffsL, constsL) if delete_index == []: ''' print 'Var {1}: Amatrix size = {0}x{0}'.format(len(Amatrix),v.toStr()) print Amatrix print 'sources: ', [i.toStr() for i in source_asserts] print 'coeffs: ', [i.toStr() for i in coeffs] ''' break if delete_index != [] or len(constsL) == 0: return None return Amatrix def getRealEigenvalues( Amatrix ): try: (eigs,eigv) = scipy.linalg.eig(Amatrix) eigs_real = [] for eig in eigs: # numpy.nditer(eigs): if abs(eig.imag) < 1e-4: ####DEBUG assert type(numpy.asscalar(eig.real)) == float, 'Type = {0}'.format(type(eig.real)) this_eig = numpy.asscalar(eig.real) if all([abs(this_eig-i) > 1e-4 for i in eigs_real]): eigs_real.append(numpy.asscalar(eig.real)) except scipy.linalg.LinAlgError: print 'Eigenvalue computation did not converge' assert False, 'return None; handle it by continue with next variable' return eigs_real def replaceVarByValMain(asserts, neg_asserts, v, v_value, level): for i in asserts: iSat = i.replaceVarByVal(v, v_value, level) if iSat == False: return False for neg_assert in neg_asserts: retVal = neg_assert.replaceVarByVal(v, v_value, level) if retVal == False: return False return True def dfs( asserts, level, extra_asserts, todo_stack, answer, variables, neg_asserts ): '''asserts = List of AFmls; todo_stack = (level,variable,value/AFmla-list)-list extra_asserts = (level, AFmla-List) answer = level->(var->value)''' while len(variables) >= 0: # update the usedby list in each variable for v in variables: for a in extra_asserts: if a.contains_variable(v): v.usedby.append(a) # print 'Variable {0} used by {1} asserts'.format(v.name, len(v.usedby)) new_asserts = extra_asserts for i in new_asserts: i.setLevel( level ) asserts.extend( new_asserts ) extra_asserts = [] # if any assert is var = value, then replace var by value # in all other asserts; delete variable. unit_prop_res = unit_prop(asserts, level, answer, variables, neg_asserts) if unit_prop_res == None: if todo_stack == []: return 'UNSATISFIABLE' else: asserts, level, extra_asserts, todo_stack, answer, variables, neg_asserts = backtrack(asserts, level-1, todo_stack, answer, variables, neg_asserts) continue (asserts, answer, variables) = unit_prop_res if len(variables) == 0: print 'SATISFIABLE: model', for (k,v) in answer.items(): print '\nlevel {0}:'.format(k), for (k1,v1) in v.items(): print '{0} = {1}, '.format(k1.toStr(),v1), return 'SATISFIABLE' ''' print 'DFS search level {0}: {4} old asserts, {1} new asserts: {2} remaining cases: {3} variables left'.format(level,len(new_asserts),len(todo_stack),len(variables),len(asserts)) print 'asserts: ', [i.toStr()+'\n' for i in asserts] for i in range(len(asserts)): print i, ': ', asserts[i].toStr() print 'newasserts: ', [i.toStr()+'\n' for i in new_asserts] print 'answers: ', [(vv1.toStr(),vv2) for (lll,vvv) in answer.items() for (vv1,vv2) in vvv.items()] print 'variables: ', [i.toStr() for i in variables] print 'todo: ', todo_stack ''' '''for (k,v) in solution.items(): print '***Var {0} = {1}'.format(k.toStr(), v) # Now, substitute val v for variable k in all the asserts for i in asserts: i.replaceVarByVal(k, v, level)''' status = '' for v in variables: coeffs, consts, source_asserts = v.usedby_solvedform if len(coeffs) == 0: # variable v does not occur anywhere anymore!!! assign_var_val(answer, level, v, 666, variables) for neg_assert in neg_asserts: retVal = neg_assert.replaceVarByVal(v, 666, level) # check if retVal is None; not relevant for benchmarks status = 'dfs' extra_asserts = [] break #return dfs(asserts, level, [], todo_stack, answer, variables, neg_asserts) # Now we have to test our condition... # coeff.X=const => coeff.X=A.coeff => X=eigen(A) # check the condition A.coeff = const # Algorithm: # for every i: if const_i != LC(coeffs): remove i # if any i was removed, go back and repeat above step # if i-set is now empty, then FAIL; else # for all remaining i: we can get A!! mapping = [] mapping = myrep_pols2column_defs( coeffs, mapping ) mapping = myrep_pols2column_defs( consts, mapping ) '''print 'DEBUG: coeffs is ', [i.toStr() for i in coeffs] print 'DEBUG: consts is ', [i.toStr() for i in consts] print 'DEBUG: mapping is ', mapping for mm in mapping: for (mmk,mmv) in mm.items(): print mmk.toStr(), ':', mmv, ''' coeffsL = [myrep_pol2python_list(i,mapping) for i in coeffs] constsL = [myrep_pol2python_list(i,mapping) for i in consts] Amatrix = GFPeigenCheckMain(coeffsL, constsL, coeffs, consts, source_asserts) if Amatrix == None: '''print 'Variable {0} does not work, continue'.format(v.toStr())''' continue # with the next variable Amatrix.reverse() '''print 'Variable {0} works, recurse'.format(v.toStr())''' eigs_real = getRealEigenvalues( Amatrix ) if all([i.myrep_isVal()==None for i in coeffs]): coeffs_is_zero = [AFmla('=',i,MyRep(0)) for i in coeffs] else: coeffs_is_zero = [] if len(eigs_real) == 0 and coeffs_is_zero == []: if todo_stack == []: return 'UNSATISFIABLE' print 'No more cases here, backtrack' asserts,level,extra_asserts,todo_stack,answer,variables,neg_asserts = backtrack(asserts,level,todo_stack,answer,variables,neg_asserts) status = 'dfs' break # continue with next DFS call if len(eigs_real) == 0 and coeffs_is_zero != []: print 'Only 1 case: make coeffs = 0' # DELETE asserts that generated coeffs; else inf-loop here for a in source_asserts: a.setToTrueAt(level) extra_asserts = coeffs_is_zero status = 'dfs' break # continue with next DFS call #return dfs(asserts, level, coeffs_is_zero, todo_stack, answer, variables, neg_asserts) if coeffs_is_zero != []: todo_stack.append( (level+1, coeffs_is_zero, source_asserts ) ) eigs_real.sort() # give pref to nonzero values '''print 'New level searching; choices {0}'.format(eigs_real)''' variables.remove(v) v_value = eigs_real[-1] answer[level+1] = {v:v_value} for v_val in eigs_real[:-1]: fmla = AFmla('=', MyRep(v), MyRep(v_val,[])) todo_stack.append( (level+1, [ fmla ], [] ) ) iSat = replaceVarByValMain(asserts, neg_asserts, v, v_value, level+1) if iSat == False: if todo_stack == []: return 'UNSATISFIABLE' (asserts,level,extra_asserts,todo_stack,answer,variables,neg_asserts) = backtrack(asserts,level,todo_stack,answer,variables,neg_asserts) status = 'dfs' break # continue with next dfs call #return backtrack(asserts,level,todo_stack,answer,variables,neg_asserts) ####DEBUG print 'LEVEL {0}: Var {1} in {2}'.format(level+1, v.toStr(), eigs_real) level, extra_asserts = level+1, [] status = 'dfs' break #return dfs(asserts, level+1, [], todo_stack, answer, variables, neg_asserts) # loop on variable v ends if status == 'dfs': continue # if any good v was found, we would have exited the loop # Here: no good v found, exit with failure print 'Condition check failed. Guessing.' '''print 'Var {0}'.format(v.toStr()) print 'Coeffs {0}'.format([i.toStr() for i in coeffs]) print 'Consts {0}'.format([i.toStr() for i in consts])''' # just guess value 0 or 1 for one of the variables and continue v = variables.pop() #eigs_real = [-1,0,1] eigs_real = [-1,0] v_value = eigs_real[-1] answer[level+1] = {v:v_value} for v_val in eigs_real[:-1]: fmla = AFmla('=', MyRep(v), MyRep(v_val,[])) todo_stack.append( (level+1, [ fmla ], [] ) ) iSat = replaceVarByValMain(asserts, neg_asserts, v, v_value, level+1) if iSat == False: if todo_stack == []: return 'UNSATISFIABLE' (asserts,level,extra_asserts,todo_stack,answer,variables,neg_asserts) = backtrack(asserts,level,todo_stack,answer,variables,neg_asserts) status = 'dfs' continue #return backtrack(asserts,level,todo_stack,answer,variables,neg_asserts) ####DEBUG print 'LEVEL {0}: Var {1} guessed.'.format(level+1, v.toStr()) level, newasserts = level+1, [] #return dfs(asserts, level+1, [], todo_stack, answer, variables, neg_asserts) return 'UNSATISFIABLE' def backtrack(asserts, level, todo_stack, answer, variables, neg_asserts): '''go back to level''' assert todo_stack != [], 'Todo stack empty' '''if todo_stack == []: print 'UNSATISFIABLE' return 'UNSATISFIABLE' ''' (newlevel, newasserts, source_asserts) = todo_stack.pop() ####DEBUG assert newlevel >= 1, 'backtrack level is {0}?'.format(newlevel) ####DEBUG print 'backtracking to level {0}'.format(newlevel) for i in range(newlevel, level+2): if answer.has_key(i): var_vals = answer[i] for (var,val) in var_vals.items(): variables.append(var) del answer[i] # now update the asserts delete_asserts = [] for a in asserts: done = a.backtrack( newlevel-1 ) if not done: delete_asserts.append(a) ####DEBUG print 'deleting {0} asserts'.format(len(delete_asserts)) for a in delete_asserts: asserts.remove(a) for neg_assert in neg_asserts: neg_assert.backtrack( newlevel-1 ) # ------------------------------------------------ # in case when we make coeffs = 0, we should remove the # asserts that generated the coeffs to avoid infinite looping....... for a in source_asserts: a.setToTrueAt( newlevel ) ''' if len( source_asserts ) > 1: # find the variable..... var_which_generated_me = None for v in variables: print v.toStr(), len(v.usedby_solvedform) for (coeff,const,aa) in v.usedby_solvedform: for a in newasserts: print coeff, a.lhs if a.lhs == coeff: var_which_generated_me = v break if var_which_generated_me != None: break if var_which_generated_me != None: break if var_which_generated_me != None: for (coeff,const,a) in var_which_generated_me.usedby_solvedform: if a.level < newlevel: a.history.append( (a.level, a.p) ) a.p = MyRep('0') a.level = newlevel break else: print 'Did not find variable which generated case', print [i.toStr() for i in variables] ''' # ------------------------------------------------ return (asserts, newlevel, newasserts, todo_stack, answer, variables, neg_asserts) #return dfs(asserts, newlevel, newasserts, todo_stack, answer, variables, neg_asserts) def unit_prop(asserts, level, answer, variables, neg_asserts): '''Unit propagation; if var = value; substitute in same level return None if contradiction detected; return (asserts, answer, variables) updated after all unit-props; side-effect: v.usedby_solvedform caches results''' def isZero(val): return val != None and abs(val) < 1e-4 found_unit_var = True while found_unit_var: found_unit_var = False for v in variables: coeffs, consts, source_asserts = [], [], [] v.usedby_solvedform = None for a in v.usedby: (coeff,const) = a.solve_for(v) # no need of level here..... cc = coeff.myrep_isVal() dd = const.myrep_isVal() if isZero(cc): # and isZero(dd): continue if cc == None or dd == None: coeffs.append(coeff) consts.append(const) source_asserts.append(a) #elif isZero(cc) and not isZero(dd): #return None # backtrack(asserts, level-1, todo_stack, answer, variables) else: variables.remove(v) v_value = (1.0 * dd) / cc if answer.has_key(level): answer[level][v] = v_value else: answer[level] = {v:v_value} for i in asserts: iSat = i.replaceVarByVal(v, v_value, level) if iSat == False: return None # backtrack(asserts,level-1,todo_stack,answer,variables) del coeffs, consts, source_asserts coeffs, consts, source_asserts = [], [], [] ####DEBUG print '{0} -> {1}'.format(v.toStr(), v_value) for i in neg_asserts: iSat = i.replaceVarByVal(v, v_value, level) if iSat == False: return None # backtrack(asserts,level-1,todo_stack,answer,variables) found_unit_var = True break v.usedby_solvedform = (coeffs,consts,source_asserts) return (asserts, answer, variables) # --------------------------------------------------------------------- # Routines to convert myrep_pol to vectors... # --------------------------------------------------------------------- def myrep_pol2column_defs(pol, ans): "return all columns (monomials) that occur in pol; return dict ans" for cmu in pol.p: ####DEBUG assert len(cmu) == 2, 'Monomial error {0} in {1}'.format(cmu,pol) if cmu[1] in ans: pass else: ans.append( cmu[1] ) return ans def myrep_pols2column_defs(pols, ans): "return all columns (monomials) that occur in pols; return dict ans" for p in pols: ans = myrep_pol2column_defs(p, ans) return ans def myrep_pol2python_list(pol, mapping): '''mapping = dict from mono to index; pol = myrep_pol; return = python_list representation of the pol''' ans = [0] * len(mapping) for cmu in pol.p: ####DEBUG assert len(cmu) == 2, 'Mono error {0} in {1}'.format(cmu, pol) ####DEBUG assert cmu[1] in mapping, 'Mapping error {0}:{1}'.format(cmu[1],mapping) index = mapping.index( cmu[1] ) ans[ index ] = cmu[0] return ans # --------------------------------------------------------------------- def pp_sexpr(f): "pretty print sexpr" if type(f) == str: return f elif f[0] == '-': return '-' + pp_fml(f[1]) elif len(f) == 3: return pp_fml(f[1]) + f[0] + pp_fml(f[2]) elif len(f) == 2: return f[0] + pp_fml(f[1]) elif len(f) > 3: fs = [pp_fml(i) for i in f[1:]] ans = fs[0] for i in fs[1:]: ans = ans + f[0] + i return ans def is_number(s): try: float(s) return True except ValueError: return False def is_variable(s, variables): for i in variables: if i.name == s: return i return None def sexpr2myrep(f, variables): "convert sexpr f to MyRep or AFmla depending on its type" if type(f) == str: return MyRep( f, variables ) elif f[0] == '-': v = sexpr2myrep(f[1], variables) return v.myrep_minus() elif f[0] == '+': vlist = [ sexpr2myrep(i, variables) for i in f[1:] ] return vlist[0].myrep_add(vlist[1:]) elif f[0] == '*': vlist = [ sexpr2myrep(i, variables) for i in f[1:] ] return vlist[0].myrep_mul(vlist[1:]) elif f[0] == '/': num = sexpr2myrep(f[1], variables) den = sexpr2myrep(f[2], variables) return num.myrep_div(den) elif f[0] == '=': lhs = sexpr2myrep( f[1], variables ) rhs = sexpr2myrep( f[2], variables ) return AFmla('=', lhs, rhs) elif f[0] == 'not' and len(f[1]) > 0 and f[1][0] == 'and': facts = [ sexpr2myrep( i, variables ) for i in f[1][1:] ] return facts else: print 'Warning: Ignoring {0}'.format(f) return None if __name__ == '__main__': main()