diff --git a/ivy/ivy_actions.py b/ivy/ivy_actions.py index fdb2f92..62c7f48 100644 --- a/ivy/ivy_actions.py +++ b/ivy/ivy_actions.py @@ -738,9 +738,13 @@ class EnvAction(ChoiceAction): ite = IfAction(cond,self.args[0],self.args[1]) return ite.update(domain,pvars) result = [], false_clauses(annot=EmptyAnnotation()), false_clauses(annot=EmptyAnnotation()) +# print 'env action:' for a in self.args: foo = a.update(domain, pvars) +# print 'sub vars = {}'.format([str(x) for x in used_symbols_clauses(foo[1])]) result = join_action(result, foo, domain.relations) +# print 'join vars = {}'.format([str(x) for x in used_symbols_clauses(result[1])]) +# print 'annot = {}'.format(result[1].annot) return result def __str__(self): if all(hasattr(a,'label') for a in self.args): @@ -807,7 +811,12 @@ class IfAction(Action): raise IvyError(self,'condition must be boolean') branches = [self.args[1],self.args[2] if len(self.args) >= 3 else Sequence()] upds = [a.int_update(domain,pvars) for a in branches] +# if hasattr(self,'lineno'): +# print 'ite at {}'.format(self.lineno) +# print 'if vars = {}'.format([str(x) for x in used_symbols_clauses(upds[0][1])]) +# print 'else vars = {}'.format([str(x) for x in used_symbols_clauses(upds[1][1])]) res = ite_action(self.args[0],upds[0],upds[1],domain.relations) +# print 'join vars = {}'.format([str(x) for x in used_symbols_clauses(res[1])]) return res if_part,else_part = (a.int_update(domain,pvars) for a in self.subactions()) @@ -1357,6 +1366,8 @@ def ite_annot(self,cond,other): Annotation.ite = ite_annot def unite_annot(annot): + if isinstance(annot,RenameAnnotation): + return [(annot.map.get(x,x),RenameAnnotation(y,annot.map)) for (x,y) in unite_annot(annot.arg)] if not isinstance(annot,IteAnnotation): return [] res = unite_annot(annot.elseb) diff --git a/ivy/ivy_logic_utils.py b/ivy/ivy_logic_utils.py index 84ab095..79cd5e5 100644 --- a/ivy/ivy_logic_utils.py +++ b/ivy/ivy_logic_utils.py @@ -1146,16 +1146,19 @@ def or_clauses(*args): else: used = set(chain(*[arg.symbols() for arg in args])) rn = UniqueRenamer('__ts0',used) - res,vs = or_clauses_int(rn,args) + res,vs,args = or_clauses_int(rn,args) fixed_vs = [] + fixed_args = [] idx = 0 for a in orig_args: if a.is_false(): fixed_vs.append(Or()) + fixed_args.append(a) else: fixed_vs.append(vs[idx]) + fixed_args.append(args[idx]) idx += 1 - return fix_or_annot(res,fixed_vs,orig_args) + return fix_or_annot(res,fixed_vs,fixed_args) def ite_clauses(cond,args): @@ -1213,7 +1216,7 @@ def or_clauses_int(rn,args): defs = [d for n,d in defidx.iteritems()] # TODO: hash traversal dependency res = Clauses(fmlas,defs) # print "or_clauses_int res = {}".format(res) - return res,vs + return res,vs,args def debug_clauses_list(cl): for clauses in cl: @@ -1262,7 +1265,7 @@ def tagged_or_clauses(prefix,*args): predicate symbols begin with "prefix". See find_true_disjunct. """ args = coerce_args_to_clauses(args) - res,vs = or_clauses_int(UniqueRenamer('__to0',dict()),args) + res,vs,args = or_clauses_int(UniqueRenamer('__to0',dict()),args) return fix_or_annot(res,vs,args) def find_true_disjunct(clauses,eval_fun): diff --git a/ivy/ivy_mc.py b/ivy/ivy_mc.py index d23a091..ade5a25 100644 --- a/ivy/ivy_mc.py +++ b/ivy/ivy_mc.py @@ -426,12 +426,12 @@ class Encoder(object): if cy is None: cy = self.sub.false() for i in range(len(x)-1,-1,-1): - cy = self.sub.orl(self.sub.andl(x[i],y[i]),self.sub.andl(self.sub.iff(x[i],y[i]),cy)) - return cy + cy = self.sub.orl(self.sub.andl(self.sub.notl(x[i]),y[i]),self.sub.andl(self.sub.iff(x[i],y[i]),cy)) + return [cy] def encode_le(self,sort,x,y): - return encode_lt(self,sort,x,y,cy=self.sub.true()) - + return self.encode_lt(sort,x,y,cy=self.sub.true()) + def encode_div(self,sort,x,y): thing = [self.sub.false() for _ in x] res = [] @@ -872,6 +872,8 @@ def uncompose_annot(annot): return res def unite_annot(annot): + if isinstance(annot,ia.RenameAnnotation): + return [(annot.map.get(x,x),ia.RenameAnnotation(y,annot.map)) for (x,y) in unite_annot(annot.arg)] if not isinstance(annot,ia.IteAnnotation): return [] res = unite_annot(annot.elseb) @@ -923,8 +925,9 @@ def match_annotation(action,annot,handler): cond = handler.eval(rncond) except KeyError: print '{}skipping conditional'.format(action.lineno) - iu.dbg('str_map(env)') - iu.dbg('env.get(annot.cond,annot.cond)') +# exit(1) +# iu.dbg('str_map(env)') +# iu.dbg('env.get(annot.cond,annot.cond)') return if cond: recur(action.args[1],annot.thenb,env) @@ -934,6 +937,7 @@ def match_annotation(action,annot,handler): return if isinstance(action,ia.ChoiceAction): assert isinstance(annot,ia.IteAnnotation) + annots = unite_annot(annot) assert len(annots) == len(action.args) for act,(cond,ann) in reversed(zip(action.args,annots)): @@ -943,11 +947,17 @@ def match_annotation(action,annot,handler): assert False,'problem in match_annotation' if isinstance(action,ia.CallAction): callee = im.module.actions[action.args[0].rep] - seq = ia.Sequence(*([ia.Sequence() for x in callee.formal_params] - + [callee] - + [ia.Sequence() for x in callee.formal_returns])) + seq = ia.Sequence(ia.IgnoreAction(),callee,ia.ReturnAction()) +# seq = ia.Sequence(*([ia.Sequence() for x in callee.formal_params] +# + [callee] +# + [ia.Sequence() for x in callee.formal_returns])) recur(seq,annot,env) return + if isinstance(action,ia.ReturnAction): + handler.do_return(action,env) + return + if isinstance(action,ia.IgnoreAction): + return if isinstance(action,ia.LocalAction): recur(action.args[-1],annot,env) return @@ -1096,6 +1106,7 @@ def to_aiger(mod,ext_act): # compute the transition relation stvars,trans,error = action.update(mod,None) +# iu.dbg('trans') # print 'action : {}'.format(action) @@ -1362,7 +1373,10 @@ class AigerMatchHandler(object): res = il.is_true(self.aiger.get_sym(cond)) # print 'eval: {} = {}'.format(cond,res) return res - + + def do_return(self,action,env): + pass + def handle(self,action,env): def my_is_skolem(x): @@ -1372,11 +1386,12 @@ class AigerMatchHandler(object): if all(x in inv_env or not my_is_skolem(x) and not tr.is_new(x) and x not in env for x in ilu.used_symbols_ast(decd)): expr = ilu.rename_ast(decd,inv_env) - if il.is_constant(expr) and expr in il.sig.constructors: - return - if not (expr in self.current and self.current[expr] == val): - print ' {} = {}'.format(expr,val) - self.current[expr] = val + if not tr.is_new(expr.rep): + if il.is_constant(expr) and expr in il.sig.constructors: + return + if not (expr in self.current and self.current[expr] == val): + print ' {} = {}'.format(expr,val) + self.current[expr] = val if hasattr(action,'lineno'): # print ' env: {}'.format('{'+','.join('{}:{}'.format(x,y) for x,y in env.iteritems())+'}')