starting on proofs for conjectures

ivy/ivy_ast.py

@@ -536,6 +536,7 @@ class LabeledFormula(AST):
         self.args = args
         self.id = lf_counter
         self.temporal = None
+        self.explicit = False
         lf_counter += 1
     @property
     def label(self):
@@ -554,6 +555,7 @@ class LabeledFormula(AST):
         lf_counter -= 1
         res.id = self.id
         res.temporal = self.temporal
+        res.explicit = self.explicit
         return res
 
 class LabeledDecl(Decl):

ivy/ivy_check.py

@@ -326,10 +326,10 @@ def check_safety_in_state(mod,ag,post,report_pass=True):
 
 opt_summary = iu.BooleanParameter("summary",False)
 
-# This gets the pre-state for inductive checks
+# This gets the pre-state for inductive checks. Only implicit conjectures are used.
 
 def get_conjs(mod):
-    fmlas = [lf.formula for lf in mod.labeled_conjs]
+    fmlas = [lf.formula for lf in mod.labeled_conjs if not lf.explicit]
     return lut.Clauses(fmlas,annot=act.EmptyAnnotation())
 
 

ivy/ivy_isolate.py

@@ -1396,6 +1396,7 @@ def apply_present_conjectures(isol,mod):
         return []
     brackets = []
     conjs = get_isolate_conjs(mod,isol,verified=False)
+    conjs = [c for c in conjs if not c.explicit]
     cg = mod.call_graph()  # TODO: cg should be cached
     myexports = get_isolate_exports(mod,cg,isol)
     for actname in myexports:

ivy/ivy_lexer.py

@@ -138,6 +138,7 @@ reserved = all_reserved = {
    'showgoals' : 'SHOWGOALS',
    'defergoal' : 'DEFERGOAL',
    'spoil' : 'SPOIL',
+   'explicit' : 'EXPLICIT',
 }
 
 tokens += tuple(all_reserved.values())
@@ -245,7 +246,7 @@ class LexerVersion(object):
                 if s in reserved:
                     del reserved[s]
         if self.version <= [1,6]:
-            for s in ['decreases','specification','implementation','require','ensure','around','parameter','apply','theorem','showgoals','spoil']:
+            for s in ['decreases','specification','implementation','require','ensure','around','parameter','apply','theorem','showgoals','spoil','explicit']:
                 if s in reserved:
                     del reserved[s]
         else:

ivy/ivy_parser.py

@@ -374,14 +374,26 @@ def p_top_conjecture_labeledfmla(p):
 
 # from version 1.7, "invariant" replaces "conjecture"
 if not iu.get_numeric_version() <= [1,6]:
+
+    def p_optexplicit(p):
+        'optexplicit : '
+        p[0] = False
+
+    def p_optexplicit_explicit(p):
+        'optexplicit : EXPLICIT'
+        p[0] = True
+
     def p_top_invariant_labeledfmla(p):
-        'top : top INVARIANT labeledfmla optproof'
+        'top : top optexplicit INVARIANT labeledfmla optproof'
         p[0] = p[1]
-        d = ConjectureDecl(addlabel(p[3],'invar'))
-        d.lineno = get_lineno(p,2)
+        lf = addlabel(p[4],'invar')
+        if p[2]:
+            lf.explicit = True
+        d = ConjectureDecl(lf)
+        d.lineno = get_lineno(p,3)
         p[0].declare(d)
-        if p[4] is not None:
-            p[0].declare(ProofDecl(p[4]))
+        if p[5] is not None:
+            p[0].declare(ProofDecl(p[5]))
 
 def p_modulestart(p):
     'modulestart :'