From fa61fb4a7ba5dd5a6f1704f78a97e60d967f4f35 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Fri, 2 Nov 2018 15:48:36 -0700
Subject: [PATCH] starting on proofs for conjectures

---
 ivy/ivy_ast.py     |  2 ++
 ivy/ivy_check.py   |  4 ++--
 ivy/ivy_isolate.py |  1 +
 ivy/ivy_lexer.py   |  3 ++-
 ivy/ivy_parser.py  | 22 +++++++++++++++++-----
 5 files changed, 24 insertions(+), 8 deletions(-)

diff --git a/ivy/ivy_ast.py b/ivy/ivy_ast.py
index 3f370fb..b75c4f1 100644
--- a/ivy/ivy_ast.py
+++ b/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):
diff --git a/ivy/ivy_check.py b/ivy/ivy_check.py
index c591bcd..f9e574a 100644
--- a/ivy/ivy_check.py
+++ b/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())
 
 
diff --git a/ivy/ivy_isolate.py b/ivy/ivy_isolate.py
index b91e999..06ce71f 100644
--- a/ivy/ivy_isolate.py
+++ b/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:
diff --git a/ivy/ivy_lexer.py b/ivy/ivy_lexer.py
index 1d5880e..dcfd703 100644
--- a/ivy/ivy_lexer.py
+++ b/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:
diff --git a/ivy/ivy_parser.py b/ivy/ivy_parser.py
index 062b50c..13586cb 100644
--- a/ivy/ivy_parser.py
+++ b/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 :'