working on loop unrolling

ivy/ivy_actions.py

@@ -1,7 +1,7 @@
 #
 # Copyright (c) Microsoft Corporation. All Rights Reserved.
 #
-from ivy_logic import Variable,Constant,Atom,Literal,App,sig,And,Or,Not,Implies,EnumeratedSort,Ite,Definition, is_atom, equals, Equals, Symbol,ast_match_lists, is_in_logic, Exists, RelationSort, is_boolean
+from ivy_logic import Variable,Constant,Atom,Literal,App,sig,And,Or,Not,Implies,EnumeratedSort,Ite,Definition, is_atom, equals, Equals, Symbol,ast_match_lists, is_in_logic, Exists, RelationSort, is_boolean, is_app, is_eq
 
 from ivy_logic_utils import to_clauses, formula_to_clauses, substitute_constants_clause,\
     substitute_clause, substitute_ast, used_symbols_clauses, used_symbols_ast, rename_clauses, subst_both_clauses,\
@@ -209,6 +209,14 @@ class Action(AST):
         if hasattr(self,'formal_returns'):
             res.formal_returns = self.formal_returns
         return res
+    def unroll_loops(self,card):
+        args = [a.unroll_loops(card) if isinstance(a,Action) else a for a in self.args]
+        res = self.clone(args)
+        if hasattr(self,'formal_params'):
+            res.formal_params = self.formal_params
+        if hasattr(self,'formal_returns'):
+            res.formal_returns = self.formal_returns
+        return res
     def iter_calls(self):
         for a in self.args:
             if isinstance(a,Action):
@@ -725,7 +733,7 @@ class WhileAction(Action):
     def decompose(self,pre,post,fail=False):
         return self.expand(ivy_module.module,[]).decompose(pre,post,fail)
     def assert_to_assume(self):
-        return self.clone(self.args[:2])
+        return self.clone([self.args[0],self.args[1].assert_to_assume()])
     def drop_invariants(self):
         res = self.clone(self.args[:2])
         if hasattr(self,'formal_params'):
@@ -733,7 +741,26 @@ class WhileAction(Action):
         if hasattr(self,'formal_returns'):
             res.formal_returns = self.formal_returns
         return res
-
+    def unroll_loops(self,card):
+        cond = self.args[0]
+        if is_app(cond) and cond.rep.name in ['<','>','<=','>=']:
+            idx_sort = cond.args[0].sort
+        elif isinstance(cond,Not) and is_eq(cond.args[0]):
+            idx_sort = cond.args[0].args[0].sort
+        else:
+            raise IvyError(self,'cannot determine an index sort for loop')
+        cardsort = card(idx_sort)
+        if cardsort is None:
+            raise IvyError(self,'cannot determine an iteration bound for loop over {}'.format(idx_sort))
+        res = AssumeAction(Not(cond))
+        for idx in range(cardsort):
+            res = IfAction(cond,Sequence(self.args[1],res))
+        if hasattr(self,'formal_params'):
+            res.formal_params = self.formal_params
+        if hasattr(self,'formal_returns'):
+            res.formal_returns = self.formal_returns
+        return res
+            
 
 
 local_action_ctr = 0

ivy/ivy_to_cpp.py

@@ -640,6 +640,9 @@ def emit_action_gen(header,impl,name,action,classname):
     caname = varname(name)
     if name in im.module.before_export:
         action = im.module.before_export[name]
+    def card(sort):
+        return sort_card(sort)
+    action = action.unroll_loops(card)
     upd = action.update(im.module,None)
     pre = tr.reverse_image(ilu.true_clauses(),ilu.true_clauses(),upd)
     pre_clauses = ilu.trim_clauses(pre)

test/unroll1.ivy

@@ -0,0 +1,26 @@
+#lang ivy1.6
+
+type t
+
+relation p(X:t)
+
+individual idx : t
+
+action a(max:t)
+
+object spec = {
+    before a {
+	idx := 0;
+	while idx < max {
+	    assert p(idx);
+	    idx := idx + 1
+	}
+    }
+}
+
+interpret t -> bv[2]
+
+export a
+
+isolate iso = this
+