Added support for proof production in Equality Engine. Cleaned up existing proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup.

3 files changed, 167 insertions, 110 deletions

diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf
index 67ce3988a..bbee2d49b 100755
--- a/proofs/signatures/smt.plf
+++ b/proofs/signatures/smt.plf
@@ -3,15 +3,14 @@
 ; SMT syntax and semantics (not theory-specific)
 ;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; depends on sat.plf
 
 (declare formula type)
 (declare th_holds (! f formula type))
 
-; constants
+; standard logic definitions
 (declare true formula)
 (declare false formula)
-
-; logical connectives
 (declare not (! f formula formula))
 (declare and (! f1 formula (! f2 formula formula)))
 (declare or (! f1 formula (! f2 formula formula)))
@@ -21,24 +20,19 @@
 (declare ifte (! b formula (! f1 formula (! f2 formula formula))))
 
 ; terms
-(declare sort type)				; sort in the theory
-(declare arrow (! s1 sort (! s2 sort sort)))	; function constructor
-
+(declare sort type)
 (declare term (! t sort type))	; declared terms in formula
 
-(declare apply (! s1 sort
-               (! s2 sort
-               (! t1 (term (arrow s1 s2))
-               (! t2 (term s1)
-                (term s2))))))
-
+; standard definitions for =, ite, let and flet
+(declare = (! s sort
+           (! x (term s)
+           (! y (term s)
+             formula))))
 (declare ite (! s sort
              (! f formula
              (! t1 (term s)
              (! t2 (term s)
                (term s))))))
-
-; let/flet
 (declare let (! s sort
              (! t (term s)
              (! f (! v (term s) formula)
@@ -47,38 +41,52 @@
               (! f2 (! v formula formula)
                 formula)))
 
-; predicates
-(declare = (! s sort
-           (! x (term s)
-           (! y (term s)
-             formula))))
-
-; To avoid duplicating some of the rules (e.g., cong), we will view
-; applications of predicates as terms of sort "Bool".
+; We view applications of predicates as terms of sort "Bool".
 ; Such terms can be injected as atomic formulas using "p_app".
-
 (declare Bool sort)				; the special sort for predicates
 (declare p_app (! x (term Bool) formula))	; propositional application of term
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-; Examples
+;
+; CNF Clausification
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-; an example of "(p1 or p2(0)) and t1=t2(1)"
-;(! p1 (term Bool)
-;(! p2 (term (arrow Int Bool))
-;(! t1 (term Int)
-;(! t2 (term (arrow Int Int))
-;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0)))
-;                    (= _ t1 (apply _ _ t2 1))))
-;  ...
+; binding between an LF var and an (atomic) formula
+(declare atom (! v var (! p formula type)))
 
-; another example of "p3(a,b)"
-;(! a (term Int)
-;(! b (term Int)
-;(! p3 (term (arrow Int (arrow Int Bool)))	; arrow is right assoc.
-;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc.
-;  ...
+(declare decl_atom
+  (! f formula
+  (! u (! v var
+       (! a (atom v f)
+         (holds cln)))
+    (holds cln))))
+
+; clausify a formula directly
+(declare clausify_form
+  (! f formula
+  (! v var
+  (! a (atom v f)
+  (! u (th_holds f)
+    (holds (clc (pos v) cln)))))))
+    
+(declare clausify_form_not
+  (! f formula
+  (! v var
+  (! a (atom v f)
+  (! u (th_holds (not f))
+    (holds (clc (neg v) cln)))))))
+    
+(declare clausify_false
+  (! u (th_holds false)
+    (holds cln)))
+
+(declare th_let_pf
+  (! f formula
+  (! u (th_holds f)
+  (! u2 (! v (th_holds f) (holds cln))
+    (holds cln)))))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -261,13 +269,41 @@
   (! u2 (th_holds (not (ifte (not a) b c)))
     (th_holds (not c))))))))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; For theory lemmas
+; - make a series of assumptions and then derive a contradiction (or false)
+; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"
+; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(declare ast
+  (! v var
+  (! f formula
+  (! C clause
+  (! r (atom v f)       ;this is specified
+  (! u (! o (th_holds f)
+         (holds C))
+    (holds (clc (neg v) C))))))))
+
+(declare asf
+  (! v var
+  (! f formula
+  (! C clause
+  (! r (atom v f)
+  (! u (! o (th_holds (not f))
+         (holds C))
+    (holds (clc (pos v) C))))))))
+    
+
 
 
-;; How to do CNF for disjunctions of theory literals.
+;; Example:
 ;;
-;; Given theory literals F1....Fn, and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))).
+;; Given theory literals (F1....Fn), and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))).
 ;;
-;; We introduce atoms a1...an for literals F1...Fn, mapping them to boolean literals v1...vn.
+;; We introduce atoms (a1,...,an) to map boolean literals (v1,...,vn) top literals (F1,...,Fn).
 ;; Do this at the beginning of the proof:
 ;;
 ;; (decl_atom F1 (\ v1 (\ a1
@@ -275,7 +311,7 @@
 ;; ....
 ;; (decl_atom Fn (\ vn (\ an
 ;;
-;; Our input A is clausified by the following proof:
+;;  A is then clausified by the following proof:
 ;;
 ;;(satlem _ _
 ;;(asf _ _ _ a1 (\ l1
@@ -294,7 +330,7 @@
 ;;
 ;; We now have the free variable C, which should be the clause (v1 V ... V vn).
 ;;
-;; We also need to consider the polarity of literals, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))).
+;; Polarity of literals should be considered, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))).
 ;; Where necessary, we use "ast" instead of "asf", introduce negations by "not_not_intro" for pattern matching, and flip
 ;; the arguments of contra:
 ;;
@@ -311,3 +347,5 @@
 ;;))))))) (\ C
 ;;
 ;; C should be the clause (~v1 V v2 V ~v3 )
+
+
diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf
new file mode 100755
index 000000000..6e0e6438d
--- /dev/null
+++ b/proofs/signatures/th_arrays.plf
@@ -0,0 +1,53 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

+;

+; Theory of Arrays

+;

+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

+; depdends on : th_base.plf

+

+; sorts

+

+(declare array (! s1 sort (! s2 sort sort)))	; s1 is index, s2 is element

+

+; functions

+(declare write (! s1 sort

+               (! s2 sort

+               (! t1 (term (array s1 s2))

+               (! t2 (term s1)

+               (! t3 (term s2)

+                (term (array s1 s2))))))))

+(declare read (! s1 sort

+              (! s2 sort

+              (! t1 (term (array s1 s2))

+              (! t2 (term s1)

+                (term s2))))))

+                

+; inference rules

+(declare row1 (! s1 sort

+              (! s2 sort

+              (! t1 (term (array s1 s2))

+              (! t2 (term s1)

+              (! t3 (term s2)

+              	(th_holds (= _ (read (write t1 t2 t3) t2) t3))))))))

+              	

+

+(declare row (! s1 sort

+             (! s2 sort

+             (! t1 (term (array s1 s2))

+             (! t2 (term s1)

+             (! t3 (term s1)

+             (! t4 (term s2)

+             (! u (th_holds (not (= _ t2 t3)))

+               (th_holds (= _ (read (write t1 t2 t4) t3) (read t1 t3))))))))))

+

+(declare ext (! s1 sort

+             (! s2 sort

+             (! f formula

+             (! t1 (term (array s1 s2))

+             (! t2 (term (array s1 s2))

+             (! u (th_holds (not (= _ t1 t2)))

+             (! u1 (! k (term s1)

+                   (! u2 (th_holds (not (= _ (read t1 k) (read t2 k))))

+                     (th_holds f)))

+               (th_holds f)))))))))

+               
\ No newline at end of file
diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf
index 7b0b086dc..977409b6a 100755
--- a/proofs/signatures/th_base.plf
+++ b/proofs/signatures/th_base.plf
@@ -1,80 +1,28 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Atomization / Clausification
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-; binding between an LF var and an (atomic) formula
-(declare atom (! v var (! p formula type)))
-
-(declare decl_atom
-  (! f formula
-  (! u (! v var
-       (! a (atom v f)
-         (holds cln)))
-    (holds cln))))
-
-; direct clausify
-(declare clausify_form
-  (! f formula
-  (! v var
-  (! a (atom v f)
-  (! u (th_holds f)
-    (holds (clc (pos v) cln)))))))
-
-(declare clausify_form_not
-  (! f formula
-  (! v var
-  (! a (atom v f)
-  (! u (th_holds (not f))
-    (holds (clc (neg v) cln)))))))
-
-(declare clausify_false
-  (! u (th_holds false)
-    (holds cln)))
 
 
-(declare th_let_pf
-  (! f formula
-  (! u (th_holds f)
-  (! u2 (! v (th_holds f) (holds cln))
-    (holds cln)))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;
-; Theory reasoning
-; - make a series of assumptions and then derive a contradiction (or false)
-; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"
-; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"
+; Theory of Equality and Congruence Closure
 ;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; depends on : smt.plf
 
-(declare ast
-  (! v var
-  (! f formula
-  (! C clause
-  (! r (atom v f)       ;this is specified
-  (! u (! o (th_holds f)
-         (holds C))
-    (holds (clc (neg v) C))))))))
+; sorts :
 
-(declare asf
-  (! v var
-  (! f formula
-  (! C clause
-  (! r (atom v f)
-  (! u (! o (th_holds (not f))
-         (holds C))
-    (holds (clc (pos v) C))))))))
+(declare arrow (! s1 sort (! s2 sort sort)))	; function constructor
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Theory of Equality and Congruence Closure
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; functions :
 
-; temporary :
-(declare trust (th_holds false))
+(declare apply (! s1 sort
+               (! s2 sort
+               (! t1 (term (arrow s1 s2))
+               (! t2 (term s1)
+                (term s2))))))
+                
+                
+; inference rules :
+
+(declare trust (th_holds false))	; temporary
 
 (declare refl
   (! s sort
@@ -105,3 +53,21 @@
               (! u2 (th_holds (= _ a2 b2))
                 (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Examples
+
+; an example of "(p1 or p2(0)) and t1=t2(1)"
+;(! p1 (term Bool)
+;(! p2 (term (arrow Int Bool))
+;(! t1 (term Int)
+;(! t2 (term (arrow Int Int))
+;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0)))
+;                    (= _ t1 (apply _ _ t2 1))))
+;  ...
+
+; another example of "p3(a,b)"
+;(! a (term Int)
+;(! b (term Int)
+;(! p3 (term (arrow Int (arrow Int Bool)))	; arrow is right assoc.
+;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc.
+;  ...