fixing mc issues

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)

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):

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())+'}')