working on tc1

ivy/ivy_check.py

@@ -19,6 +19,7 @@ import ivy_theory as ith
 import ivy_transrel as itr
 import ivy_solver as islv
 import ivy_fragment as ifc
+import ivy_proof
 
 import sys
 from collections import defaultdict
@@ -312,13 +313,14 @@ def check_fcs_in_state(mod,ag,post,fcs):
     return not any(fc.failed for fc in fcs)
 
 def check_conjs_in_state(mod,ag,post,indent=8):
+    conjs = mod.conj_subgoals if mod.conj_subgoals is not None else mod.labeled_conjs
     check_lineno = act.checked_assert.get()
     if check_lineno == "":
         check_lineno = None
     if check_lineno is not None:
-        lcs = [sub for sub in mod.labeled_conjs if sub.lineno == check_lineno]
+        lcs = [sub for sub in conjs if sub.lineno == check_lineno]
     else:
-        lcs = mod.labeled_conjs
+        lcs = conjs
     return check_fcs_in_state(mod,ag,post,[ConjChecker(c,indent) for c in lcs])
 
 def check_safety_in_state(mod,ag,post,report_pass=True):
@@ -332,6 +334,21 @@ def get_conjs(mod):
     fmlas = [lf.formula for lf in mod.labeled_conjs]
     return lut.Clauses(fmlas,annot=act.EmptyAnnotation())
 
+def apply_conj_proofs(mod):
+    # Apply any proof tactics to the conjs to get the conj_subgoals.
+
+    pc = ivy_proof.ProofChecker(mod.axioms,mod.definitions,mod.schemata)
+    pmap = dict((lf.id,p) for lf,p in mod.proofs)
+    conjs = []
+    for lf in mod.labeled_conjs:
+        if lf.id in pmap:
+            proof = pmap[lf.id]
+            subgoals = pc.admit_proposition(lf,proof)
+            conjs.extend(subgoals)
+        else:
+            conjs.append(lf)
+    mod.conj_subgoals = conjs
+
 
 def summarize_isolate(mod):
 
@@ -383,6 +400,8 @@ def summarize_isolate(mod):
         for lf in mod.labeled_conjs:
             print pretty_lf(lf)
 
+    apply_conj_proofs(mod)
+    
     if mod.isolate_info.implementations:
         print "\n    The following action implementations are present:"
         for mixer,mixee,action in sorted(mod.isolate_info.implementations,key=lambda x: x[0]):

ivy/ivy_module.py

@@ -77,6 +77,7 @@ class Module(object):
         self.subgoals = [] # (labeled formula * labeled formula list) list
         self.isolate_info = None # IsolateInfo or None
         self.conj_actions = dict() # map from conj names to action name list
+        self.con_subgoals = None # None or labeled formula list
 
         
         self.sig = il.sig.copy() # capture the current signature

test/tc1.ivy

@@ -0,0 +1,100 @@
+#lang ivy1.7
+
+include deduction
+
+module tree_tc(t) = {
+
+    action add(x:t,y:t)
+    action succ(x:t,y:t) returns (r:bool)
+    action reaches(x:t,y:t) returns (r:bool)
+
+    specification {
+	relation tc(X:t,Y:t)
+
+	after init {
+	    tc(X,Y) := false
+	}
+
+	# we require that adding an edge preserve the shape as an oriented tree
+	# the transitive closure is updated so that x and everything that previously
+	# reached x now reaches x
+
+	around add {
+	    require x ~= y;                # no trivial cycles added
+	    require ~tc(y,x);              # no non-trivial cycles added
+	    require ~(tc(Z,x) & tc(Z,y))   # no reconvergence added
+	    ...
+	    tc(X,y) := X = x | tc(X,x)
+	}
+
+	# y is a successor of x is x reaches y and there is nothing between x and y
+
+	after succ {
+	    ensure r <-> (tc(x,y) & ~exists Z. tc(x,Z) & tc(Z,y))
+	}
+
+	after reaches {
+	    ensure r = tc(x,y)
+	}
+
+	# These invariants state that tc is the transitive closure of a tree
+	# Treeness means there are no cycles, and the ancestors of every node are totally ordered.
+
+	invariant ~tc(X,X)
+	invariant tc(X,Y) & tc(Z,Y) -> (X = Z | tc(X,Z) | tc(Z,X))
+
+    }
+
+    implementation {
+
+	relation tree(X:t,Y:t)
+
+	# lfp ttc(X,Y) = tree(X,Y) | exists Z. (ttc(X,Z) & ttc(Z,Y))
+
+	relation ttc(X:t,Y:t)
+	# ttc is a fixed point
+	schema fp = {
+	    property (tree(X,Y) | exists Z. (ttc(X,Z) & ttc(Z,Y))) -> ttc(X,Y) 
+	}
+	# ttc is the least fixed point
+	schema lep = {
+	    relation r(X:t,Y:t)
+	    forall X,Y. ((tree(X,Y) | exists Z. (r(X,Z) & r(Z,Y))) -> r(X,Y))
+	    property ttc(X,Y) -> r(X,Y)
+	}
+	    
+
+	after init {
+	    tree(X,Y) := false;
+	}
+
+	implement add {
+	    tree(x,y) := true;
+	}
+
+	implement succ {
+	    r := tree(x,y);
+	}
+
+	implement reaches {
+	    r := ttc(x,y);
+	}
+
+    }
+
+    # The representation invariant is that the transitive closure of 'tree' is equal to tc.
+
+    private {
+	invariant tc(X,Y) <-> ttc(X,Y)
+	proof {
+	    apply elimImp with p = ttc(X,Y) -> tr.tree(X,Y); showgoals;
+	    apply lep with r(X,Y) = tree(X,Y) ; showgoals }
+    }
+    
+    isolate iso = this
+
+}
+
+type t
+instance tr : tree_tc(t)
+export tr.add