working on "for some" and collections.ivy

ivy/include/collections.ivy

@@ -0,0 +1,157 @@
+#lang ivy1.6
+
+################################################################################
+#
+# Maps. 
+#
+# This module provides a relational model of a function from a type
+# dom to a type rng. Initially, everything is mapped to the element zero.
+# 
+# The key invariant of a map is that it is a function, i.e., for every
+# X there exists a Y such that map(X,Y). The module does not state
+# this invariant, however, since the quantifier alternation could
+# destroy stratification.  Instead it provides a "lemma" that allows
+# the user to instantiate Y for particular values of X.
+#
+# Parameters:
+#
+#  dom        The domain type
+#  rng        The range type
+#  zero       The initial value for every domain element
+
+module map(dom,rng,zero) = {
+
+    relation map(X:dom,Y:rng)
+    init map(X,Y) <-> Y = zero
+
+    # set the value of x to y
+    action set_(x:dom,y:rng) = {
+	local oldval:rng {
+	    assume map(x,oldval)
+	};
+	map(x,Y) := Y = y
+    }
+
+    # get the value of x
+    action get(x:dom) returns (y:rng) = {
+	assume map(x,y)
+    }
+
+    # prove there exists a value for x
+    action lemma(x:dom) = {
+	assume exists Y. map(x,Y)
+    }
+
+    conjecture map(K,L) & map(K,M) -> L = M
+
+}
+
+module set_wrapper(key) = {
+
+    object s = {}
+
+    <<< header
+	#include <set>
+    >>>
+
+    <<< member
+	std::set<int> `s`;
+    >>>
+
+    <<< init
+        `s`.insert(0);
+    >>>
+
+    implement insert(x:key) {
+	<<<
+	    `s`.insert(`x`);
+	>>>
+    }
+
+    implement erase(lo:key,hi:key) {
+	<<<
+            `s`.erase(`s`.lower_bound(`lo`),`s`.upper_bound(`hi`));
+	>>>
+    }
+
+    implement get_glb(k:key) returns (res:key) {
+	<<<
+            `res` = *(--`s`.upper_bound(`k`));
+	>>>
+	
+    }
+
+
+}
+
+################################################################################
+#
+# Ordered set representation
+#
+# This is intended to be implemented using the STL set template.
+#
+# Ordered sets assume the element type has a total non-strict order,
+# with a least element 0.  They provide insertion of elements (in log
+# time), deletion of ranges (in n log(n) time) and finding greatest
+# lower bounds (log n).
+# 
+# For help with proofs, this module also provides an auxiliary map
+# "succ" that gives the successor of every element in the set. The
+# "successor" of the maximal element in the set is 0.
+
+module ordered_set(key) = {
+
+    action insert(nkey:key)
+    action erase(lo:key,hi:key)
+    action get_glb(k:key) returns (res:key)
+
+    relation s(K:key)
+    init s(K) <-> K = 0
+
+    instantiate succ : map(key,key,0) # ghost
+
+    # insert one element
+    before insert {
+	s(nkey) := true;
+
+	# following is ghost code to update the successor relation
+	local v:key {
+	    if some lub:key. ~(lub <= nkey) & s(lub) minimizing lub {
+		v := lub
+	    }
+	    else {
+		v := 0
+	    };
+	    call succ.set_(nkey,v)
+	};
+	if some glb:key. ~(nkey <= glb) & s(glb) maximizing glb {
+	    call succ.lemma(glb); # instantiate succ(glb)
+	    call succ.set_(glb,nkey)
+	}
+    }
+    
+    # erase elements in a closed interval
+    before erase {
+	s(K) := s(K) & ~(lo <= K & K <= hi)
+    }
+
+    # the the greatest element <= k
+    after get_glb {
+	if some glb:key. glb <= k & s(glb) maximizing glb {
+	    call succ.lemma(glb); # instantiate succ(glb)
+	    assert res = glb
+	}
+    }
+
+    # Useful invariants of the "succ" relation. The successor of K is
+    # also in the set, and nothing between K and its successor is in
+    # the set. Here, if L = 0 it means K is the maximim element, so we
+    # have to treat this as a special case.
+
+    conjecture s(K) & succ.map(K,L) & L ~= 0 -> ~(L <= K) & s(L)
+    conjecture s(K) & succ.map(K,L) & ~(M <= K) & (L = 0 | ~(L <= M)) -> ~s(M)
+
+    instance impl : set_wrapper(key)
+    private impl
+
+}

ivy/ivy_to_cpp.py

@@ -520,11 +520,11 @@ def init_method():
     res.formal_returns = []
     return res
 
-def open_loop(impl,vs):
+def open_loop(impl,vs,declare=True):
     global indent_level
     for idx in vs:
         indent(impl)
-        impl.append('for (int ' + idx.name + ' = 0; ' + idx.name + ' < ' + str(sort_card(idx.sort)) + '; ' + idx.name + '++) {\n')
+        impl.append('for ('+ ('int ' if declare else '') + idx.name + ' = 0; ' + idx.name + ' < ' + str(sort_card(idx.sort)) + '; ' + idx.name + '++) {\n')
         indent_level += 1
 
 def close_loop(impl,vs):
@@ -534,6 +534,25 @@ def close_loop(impl,vs):
         indent(impl)
         impl.append('}\n')
         
+def open_scope(impl,newline=False,line=None):
+    global indent_level
+    if line != None:
+        indent(impl)
+        impl.append(line)
+    if newline:
+        impl.append('\n')
+        indent(impl)
+    impl.append('{\n')
+    indent_level += 1
+
+def open_if(impl,cond):
+    open_scope(impl,line='if('+(''.join(cond) if isinstance(cond,list) else cond)+')')
+    
+def close_scope(impl):
+    global indent_level
+    indent_level -= 1
+    indent(impl)
+    impl.append('}\n')
 
 # This generates the "tick" method, called by the test environment to
 # represent passage of time. For each progress property, if it is not
@@ -1020,9 +1039,57 @@ def emit_quant(variables,body,header,code,exists=False):
     header.append('}\n')
     code.append(res)    
 
+
 lg.ForAll.emit = lambda self,header,code: emit_quant(list(self.variables),self.body,header,code,False)
 lg.Exists.emit = lambda self,header,code: emit_quant(list(self.variables),self.body,header,code,True)
 
+def code_line(impl,line):
+    indent(impl)
+    impl.append(line+';\n')
+
+def code_asgn(impl,lhs,rhs):
+    code_line(impl,lhs + ' = ' + rhs)
+
+def code_eval(impl,expr):
+    code = []
+    expr.emit(impl,code)
+    return ''.join(code)
+
+def emit_some(self,header,code):
+    vs = [il.Variable('X__'+str(idx),p.sort) for idx,p in enumerate(self.params())]
+    subst = dict(zip(self.params(),vs))
+    fmla = ilu.substitute_constants_ast(self.fmla(),subst)
+    some = new_temp(header)
+    code_asgn(header,some,'0')
+    if isinstance(self,ivy_ast.SomeMinMax):
+        minmax = new_temp(header)
+    open_loop(header,vs)
+    open_if(header,code_eval(header,fmla))
+    if isinstance(self,ivy_ast.SomeMinMax):
+        index = new_temp(header)
+        idxfmla =  ilu.substitute_constants_ast(self.index(),subst)
+        code_asgn(header,index,code_eval(header,idxfmla))
+        open_if(header,some)
+        sort = self.index().sort
+        op = il.Symbol('<',il.RelationSort([sort,sort]))
+        idx = il.Symbol(index,sort)
+        mm = il.Symbol(minmax,sort)
+        pred = op(idx,mm) if isinstance(self,ivy_ast.SomeMin) else op(mm,idx)
+        open_if(header,code_eval(header,il.Not(pred)))
+        code_line(header,'continue')
+        close_scope(header)
+        close_scope(header)
+        code_asgn(header,minmax,index)
+    for p,v in zip(self.params(),vs):
+        code_asgn(header,varname(p),varname(v))
+    code_line(header,some+'= 1')
+    close_scope(header)
+    close_loop(header,vs)
+    code.append(some)
+
+ivy_ast.Some.emit = emit_some
+
+
 def emit_unop(self,header,code,op):
     code.append(op)
     self.args[0].emit(header,code)
@@ -1172,25 +1239,36 @@ def emit_call(self,header):
 
 ia.CallAction.emit = emit_call
 
-def emit_local(self,header):
+def local_start(header,params,nondet_id=None):
     global indent_level
     indent(header)
     header.append('{\n')
     indent_level += 1
-    for p in self.args[0:-1]:
+    for p in params:
         indent(header)
         header.append('int ' + varname(p.name) + ';\n')
-        mk_nondet(header,p.name,sort_card(p.sort),p.name,self.unique_id)
-    self.args[-1].emit(header)
+        if nondet_id != None:
+            mk_nondet(header,p.name,sort_card(p.sort),p.name,nondet_id)
+
+def local_end(header):
+    global indent_level
     indent_level -= 1
     indent(header)
     header.append('}\n')
 
+
+def emit_local(self,header):
+    local_start(header,self.args[0:-1],self.unique_id)
+    self.args[-1].emit(header)
+    local_end(header)
+
 ia.LocalAction.emit = emit_local
 
 def emit_if(self,header):
     global indent_level
     code = []
+    if isinstance(self.args[0],ivy_ast.Some):
+        local_start(header,self.args[0].params())
     indent(code)
     code.append('if(');
     self.args[0].emit(header,code)
@@ -1209,6 +1287,9 @@ def emit_if(self,header):
         indent_level -= 1
         indent(header)
         header.append('}\n')
+    if isinstance(self.args[0],ivy_ast.Some):
+        local_end(header)
+
 
 ia.IfAction.emit = emit_if
 

test/ordered_set.ivy

@@ -0,0 +1,13 @@
+#lang ivy1.6
+
+include collections
+
+type t
+
+instance s : ordered_set(t)
+
+interpret t -> bv[2]
+
+export s.insert
+export s.erase
+export s.get_glb

test/some.ivy

@@ -0,0 +1,19 @@
+#lang ivy1.6
+
+type t
+
+relation p(X:t)
+init p(X) <-> X = 1
+
+action foo = {
+    if some x:t. p(x) {
+	call bar(x)
+    }
+}
+
+action bar(x:t)
+
+interpret t -> bv[1]
+
+export foo
+import bar

test/somemax.ivy

@@ -0,0 +1,20 @@
+#lang ivy1.6
+
+type t
+type q
+
+relation p(X:t)
+init p(X) 
+
+action foo = {
+    if some x:t. p(x) maximizing x {
+	call bar(x)
+    }
+}
+
+action bar(x:t)
+
+interpret t -> bv[1]
+
+export foo
+import bar

test/somemin.ivy

@@ -0,0 +1,20 @@
+#lang ivy1.6
+
+type t
+type q
+
+relation p(X:t)
+init p(X) 
+
+action foo = {
+    if some x:t. p(x) minimizing x {
+	call bar(x)
+    }
+}
+
+action bar(x:t)
+
+interpret t -> bv[1]
+
+export foo
+import bar