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.

1 files changed, 81 insertions, 43 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 )
+
+