From 89ba584531115b7f6d47088d7614368ea05ab9d8 Mon Sep 17 00:00:00 2001 From: Guy Date: Wed, 1 Jun 2016 17:33:41 -0700 Subject: [PATCH] Merging proof branch --- proofs/signatures/th_arrays.plf | 2 +- proofs/signatures/th_bv.plf | 27 +- proofs/signatures/th_bv_bitblast.plf | 419 +++++++++--- src/Makefile.am | 4 + src/options/Makefile.am | 3 +- src/proof/arith_proof.cpp | 4 + src/proof/arith_proof.h | 1 + src/proof/array_proof.cpp | 173 +++-- src/proof/array_proof.h | 33 + src/proof/bitvector_proof.cpp | 495 ++++++++++++-- src/proof/bitvector_proof.h | 14 +- src/proof/cnf_proof.cpp | 115 +++- src/proof/cnf_proof.h | 34 +- src/proof/lemma_proof.cpp | 193 ++++++ src/proof/lemma_proof.h | 79 +++ src/proof/proof_manager.cpp | 91 ++- src/proof/proof_manager.h | 7 + src/proof/proof_output_channel.cpp | 82 +++ src/proof/proof_output_channel.h | 50 ++ src/proof/proof_utils.cpp | 52 +- src/proof/proof_utils.h | 53 +- src/proof/sat_proof_implementation.h | 27 +- src/proof/skolemization_manager.h | 1 - src/proof/theory_proof.cpp | 620 +++++++++++++----- src/proof/theory_proof.h | 55 +- src/proof/uf_proof.cpp | 103 ++- src/proof/uf_proof.h | 1 + src/prop/cnf_stream.cpp | 23 +- src/prop/cnf_stream.h | 21 +- src/prop/minisat/core/Solver.cc | 24 + src/prop/minisat/minisat.cpp | 16 +- src/prop/prop_engine.cpp | 4 +- src/prop/prop_engine.h | 3 +- src/prop/theory_proxy.cpp | 33 +- src/smt/smt_engine.cpp | 34 +- src/smt/smt_engine_check_proof.cpp | 23 +- .../arrays/array_proof_reconstruction.cpp | 51 ++ src/theory/arrays/theory_arrays.cpp | 5 +- src/theory/bv/abstraction.cpp | 352 +++++----- src/theory/bv/abstraction.h | 90 +-- src/theory/bv/bv_subtheory_bitblast.cpp | 37 +- src/theory/bv/bv_subtheory_bitblast.h | 6 +- src/theory/bv/theory_bv.cpp | 38 +- src/theory/bv/theory_bv.h | 31 +- src/theory/theory_engine.cpp | 322 ++++++++- src/theory/theory_engine.h | 46 +- src/theory/uf/equality_engine.cpp | 26 +- src/theory/uf/equality_engine.h | 8 +- src/theory/uf/theory_uf.cpp | 3 +- test/regress/regress0/aufbv/Makefile.am | 1 - 50 files changed, 2992 insertions(+), 943 deletions(-) create mode 100644 src/proof/lemma_proof.cpp create mode 100644 src/proof/lemma_proof.h create mode 100644 src/proof/proof_output_channel.cpp create mode 100644 src/proof/proof_output_channel.h diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf index 5ed3d2f6f..b54a4ed5b 100755 --- a/proofs/signatures/th_arrays.plf +++ b/proofs/signatures/th_arrays.plf @@ -60,4 +60,4 @@ (! u1 (! k (term s1) (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k))))) (holds cln))) - (holds cln))))))) + (holds cln))))))) \ No newline at end of file diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf index c93541085..7f478d823 100644 --- a/proofs/signatures/th_bv.plf +++ b/proofs/signatures/th_bv.plf @@ -8,7 +8,7 @@ (program mp_ispos ((x mpz)) formula (mp_ifneg x false true)) - + (program mpz_eq ((x mpz) (y mpz)) formula (mp_ifzero (mpz_sub x y) true false)) @@ -21,7 +21,7 @@ (program mpz_ ((x mpz) (y mpz)) formula (mp_ifzero (mpz_sub x y) true false)) - + ; "bitvec" is a term of type "sort" ; (declare BitVec sort) (declare BitVec (!n mpz sort)) @@ -37,7 +37,7 @@ (declare bvc (! b bit (! v bv bv))) ; calculate the length of a bitvector -;; (program bv_len ((v bv)) mpz +;; (program bv_len ((v bv)) mpz ;; (match v ;; (bvn 0) ;; ((bvc b v') (mp_add (bv_len v') 1)))) @@ -48,7 +48,7 @@ (! n mpz (! v bv (term (BitVec n))))) - + ; a bv variable (declare var_bv type) @@ -61,7 +61,7 @@ ; bit vector binary operators (define bvop2 (! n mpz - (! x (term (BitVec n)) + (! x (term (BitVec n)) (! y (term (BitVec n)) (term (BitVec n)))))) @@ -88,7 +88,7 @@ ; bit vector unary operators (define bvop1 (! n mpz - (! x (term (BitVec n)) + (! x (term (BitVec n)) (term (BitVec n))))) @@ -111,8 +111,8 @@ (! t1 (term (BitVec m)) (! t2 (term (BitVec m')) (term (BitVec n)))))))) - -;; side-condition fails in signature only?? + +;; side-condition fails in signature only?? ;; (! s (^ (mp_add m m') n) ;; (declare repeat bvopp) @@ -147,22 +147,22 @@ (term (BitVec n))))))) - -;; TODO: add checks for valid typing for these operators + +;; TODO: add checks for valid typing for these operators ;; (! c1 (^ (mpz_lte i j) ;; (! c2 (^ (mpz_lt i n) true) ;; (! c3 (^ (mp_ifneg i false true) true) -;; (! c4 (^ (mp_ifneg j false true) true) +;; (! c4 (^ (mp_ifneg j false true) true) ;; (! s (^ (mp_add (mpz_sub i j) 1) m) - + ; bit vector predicates (define bvpred (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) formula)))) - + (declare bvult bvpred) (declare bvule bvpred) (declare bvugt bvpred) @@ -171,4 +171,3 @@ (declare bvsle bvpred) (declare bvsgt bvpred) (declare bvsge bvpred) - diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf index 580b54418..d8ce7be22 100644 --- a/proofs/signatures/th_bv_bitblast.plf +++ b/proofs/signatures/th_bv_bitblast.plf @@ -4,7 +4,7 @@ (declare bbltc (! f formula (! v bblt bblt))) ; calculate the length of a bit-blasted term -(program bblt_len ((v bblt)) mpz +(program bblt_len ((v bblt)) mpz (match v (bbltn 0) ((bbltc b v') (mp_add (bblt_len v') 1)))) @@ -25,6 +25,7 @@ (bblast_term n x y))))) +; Binds a symbol to the bblast_term to be used later on. (declare decl_bblast (! n mpz (! b bblt @@ -46,31 +47,31 @@ ;; BITBLASTING RULES ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST CONSTANT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_const ((v bv) (n mpz)) bblt - (mp_ifneg n (match v (bvn bbltn) + (mp_ifneg n (match v (bvn bbltn) (default (fail bblt))) (match v ((bvc b v') (bbltc (match b (b0 false) (b1 true)) (bblast_const v' (mp_add n (~ 1))))) (default (fail bblt))))) - + (declare bv_bbl_const (! n mpz (! f bblt (! v bv (! c (^ (bblast_const v (mp_add n (~ 1))) f) (bblast_term n (a_bv n v) f)))))) - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST VARIABLE ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_var ((x var_bv) (n mpz)) bblt - (mp_ifneg n bbltn + (mp_ifneg n bbltn (bbltc (bitof x n) (bblast_var x (mp_add n (~ 1)))))) (declare bv_bbl_var (! n mpz @@ -79,18 +80,16 @@ (! c (^ (bblast_var x (mp_add n (~ 1))) f) (bblast_term n (a_var_bv n x) f)))))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST CONCAT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_concat ((x bblt) (y bblt)) bblt - (match x + (match x (bbltn (match y ((bbltc by y') (bbltc by (bblast_concat x y'))) (bbltn bbltn))) ((bbltc bx x') (bbltc bx (bblast_concat x' y))))) - - + (declare bv_bbl_concat (! n mpz (! m mpz (! m1 mpz @@ -104,35 +103,93 @@ (! c (^ (bblast_concat xb yb ) rb) (bblast_term n (concat n m m1 x y) rb))))))))))))) - +(declare bv_bbl_concat_alias_1 (! n mpz + (! m mpz + (! m1 mpz + (! x (term (BitVec m)) + (! y (term (BitVec m1)) + (! xb bblt + (! yb bblt + (! rb bblt + (! a (term (BitVec m)) + (! e (th_holds (= _ x a)) + (! xbb (bblast_term m x xb) + (! ybb (bblast_term m1 y yb) + (! c (^ (bblast_concat xb yb) rb) + (bblast_term n (concat n m m1 a y) rb))))))))))))))) + +(declare bv_bbl_concat_alias_2 (! n mpz + (! m mpz + (! m1 mpz + (! x (term (BitVec m)) + (! y (term (BitVec m1)) + (! xb bblt + (! yb bblt + (! rb bblt + (! xbb (bblast_term m x xb) + (! a (term (BitVec m1)) + (! e (th_holds (= _ y a)) + (! ybb (bblast_term m1 y yb) + (! c (^ (bblast_concat xb yb) rb) + (bblast_term n (concat n m m1 x a) rb))))))))))))))) + +(declare bv_bbl_concat_alias_1_2 (! n mpz + (! m mpz + (! m1 mpz + (! x (term (BitVec m)) + (! y (term (BitVec m1)) + (! xb bblt + (! yb bblt + (! rb bblt + (! a1 (term (BitVec m)) + (! e (th_holds (= _ x a1)) + (! xbb (bblast_term m x xb) + (! a2 (term (BitVec m1)) + (! e (th_holds (= _ y a2)) + (! ybb (bblast_term m1 y yb) + (! c (^ (bblast_concat xb yb) rb) + (bblast_term n (concat n m m1 a1 a2) rb))))))))))))))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST EXTRACT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_extract_rec ((x bblt) (i mpz) (j mpz) (n mpz)) bblt - (match x + (match x ((bbltc bx x') (mp_ifneg (mpz_sub (mpz_sub j n) 1) (mp_ifneg (mpz_sub (mpz_sub n i) 1) (bbltc bx (bblast_extract_rec x' i j (mpz_sub n 1))) (bblast_extract_rec x' i j (mpz_sub n 1))) - + bbltn)) (bbltn bbltn))) (program bblast_extract ((x bblt) (i mpz) (j mpz) (n mpz)) bblt - (bblast_extract_rec x i j (mpz_sub n 1))) + (bblast_extract_rec x i j (mpz_sub n 1))) (declare bv_bbl_extract (! n mpz (! i mpz (! j mpz (! m mpz - (! x (term (BitVec m)) + (! x (term (BitVec m)) (! xb bblt (! rb bblt (! xbb (bblast_term m x xb) (! c ( ^ (bblast_extract xb i j m) rb) (bblast_term n (extract n i j m x) rb))))))))))) +(declare bv_bbl_extract_alias (! n mpz + (! i mpz + (! j mpz + (! m mpz + (! x (term (BitVec m)) + (! xb bblt + (! rb bblt + (! a (term (BitVec m)) + (! e (th_holds (= _ x a)) + (! xbb (bblast_term m x xb) + (! c ( ^ (bblast_extract xb i j m) rb) + (bblast_term n (extract n i j m a) rb))))))))))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST ZERO/SIGN EXTEND @@ -148,42 +205,50 @@ (declare bv_bbl_zero_extend (! n mpz (! k mpz (! m mpz - (! x (term (BitVec m)) + (! x (term (BitVec m)) (! xb bblt (! rb bblt (! xbb (bblast_term m x xb) (! c ( ^ (bblast_zextend xb k m) rb) (bblast_term n (zero_extend n k m x) rb)))))))))) - (program bblast_sextend ((x bblt) (i mpz)) bblt (match x (bbltn (fail bblt)) - ((bbltc xb x') (extend_rec x (mpz_sub i 1) xb)))) + ((bbltc xb x') (extend_rec x (mpz_sub i 1) xb)))) (declare bv_bbl_sign_extend (! n mpz (! k mpz (! m mpz - (! x (term (BitVec m)) + (! x (term (BitVec m)) (! xb bblt (! rb bblt (! xbb (bblast_term m x xb) (! c ( ^ (bblast_sextend xb k m) rb) (bblast_term n (sign_extend n k m x) rb)))))))))) - - - + +(declare bv_bbl_sign_extend_alias (! n mpz + (! k mpz + (! m mpz + (! x (term (BitVec m)) + (! xb bblt + (! rb bblt + (! a (term (BitVec m)) + (! e (th_holds (= _ x a)) + (! xbb (bblast_term m x xb) + (! c ( ^ (bblast_sextend xb k m) rb) + (bblast_term n (sign_extend n k m a) rb)))))))))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVAND ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvand ((x bblt) (y bblt)) bblt - (match x + (match x (bbltn (match y (bbltn bbltn) (default (fail bblt)))) - ((bbltc bx x') (match y + ((bbltc bx x') (match y (bbltn (fail bblt)) ((bbltc by y') (bbltc (and bx by) (bblast_bvand x' y'))))))) - - + (declare bv_bbl_bvand (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -199,11 +264,10 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_bvnot ((x bblt)) bblt - (match x - (bbltn bbltn) + (match x + (bbltn bbltn) ((bbltc bx x') (bbltc (not bx) (bblast_bvnot x'))))) - - + (declare bv_bbl_bvnot (! n mpz (! x (term (BitVec n)) (! xb bblt @@ -215,15 +279,14 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVOR ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvor ((x bblt) (y bblt)) bblt - (match x + (match x (bbltn (match y (bbltn bbltn) (default (fail bblt)))) - ((bbltc bx x') (match y + ((bbltc bx x') (match y (bbltn (fail bblt)) ((bbltc by y') (bbltc (or bx by) (bblast_bvor x' y'))))))) - - + (declare bv_bbl_bvor (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -238,15 +301,14 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVXOR ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvxor ((x bblt) (y bblt)) bblt - (match x + (match x (bbltn (match y (bbltn bbltn) (default (fail bblt)))) - ((bbltc bx x') (match y + ((bbltc bx x') (match y (bbltn (fail bblt)) ((bbltc by y') (bbltc (xor bx by) (bblast_bvxor x' y'))))))) - - + (declare bv_bbl_bvxor (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -262,8 +324,8 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVADD ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; return the carry bit after adding x y + +;; return the carry bit after adding x y ;; FIXME: not the most efficient thing in the world (program bblast_bvadd_carry ((a bblt) (b bblt) (carry formula)) formula (match a @@ -272,7 +334,7 @@ (bbltn (fail formula)) ((bbltc bi b') (or (and ai bi) (and (xor ai bi) (bblast_bvadd_carry a' b' carry)))))))) -;; ripple carry adder where carry is the initial carry bit +;; ripple carry adder where carry is the initial carry bit (program bblast_bvadd ((a bblt) (b bblt) (carry formula)) bblt (match a ( bbltn (match b (bbltn bbltn) (default (fail bblt)))) @@ -296,19 +358,19 @@ ;(program bblast_bvadd_2h ((a bblt) (b bblt) (carry formula)) bblt ;(match a ; ( bbltn (match b (bbltn bbltn) (default (fail bblt)))) -; ((bbltc ai a') (match b +; ((bbltc ai a') (match b ; (bbltn (fail bblt)) -; ((bbltc bi b') +; ((bbltc bi b') ; (let carry' (or (and ai bi) (and (xor ai bi) carry)) ; (bbltc (xor (xor ai bi) carry) ; (bblast_bvadd_2h a' b' carry')))))))) ;(program bblast_bvadd_2 ((a bblt) (b bblt) (carry formula)) bblt -;(let ar (reverseb a) ;; reverse a and b so that we can build the circuit +;(let ar (reverseb a) ;; reverse a and b so that we can build the circuit ;(let br (reverseb b) ;; from the least significant bit up ;(let ret (bblast_bvadd_2h ar br carry) ; (reverseb ret))))) - + (declare bv_bbl_bvadd (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -320,6 +382,18 @@ (! c (^ (bblast_bvadd xb yb false) rb) (bblast_term n (bvadd n x y) rb))))))))))) +(declare bv_bbl_bvadd_alias_1 (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! xb bblt + (! yb bblt + (! rb bblt + (! a (term (BitVec n)) + (! e (th_holds (= _ x a)) + (! xbb (bblast_term n x xb) + (! ybb (bblast_term n y yb) + (! c (^ (bblast_bvadd xb yb false) rb) + (bblast_term n (bvadd n a y) rb))))))))))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVNEG @@ -331,8 +405,8 @@ (program bblast_bvneg ((x bblt) (n mpz)) bblt (bblast_bvadd (bblast_bvnot x) (bblast_zero n) true)) - - + + (declare bv_bbl_bvneg (! n mpz (! x (term (BitVec n)) (! xb bblt @@ -346,14 +420,14 @@ ;; BITBLAST BVMUL ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + ;; shift add multiplier ;; (program concat ((a bblt) (b bblt)) bblt ;; (match a (bbltn b) ;; ((bbltc ai a') (bbltc ai (concat a' b))))) - + (program top_k_bits ((a bblt) (k mpz)) bblt (mp_ifzero k bbltn (match a (bbltn (fail bblt)) @@ -362,7 +436,7 @@ (program bottom_k_bits ((a bblt) (k mpz)) bblt (reverseb (top_k_bits (reverseb a) k))) -;; assumes the least signigicant bit is at the beginning of the list +;; assumes the least signigicant bit is at the beginning of the list (program k_bit ((a bblt) (k mpz)) formula (mp_ifneg k (fail formula) (match a (bbltn (fail formula)) @@ -371,7 +445,7 @@ (program and_with_bit ((a bblt) (bt formula)) bblt (match a (bbltn bbltn) ((bbltc ai a') (bbltc (and bt ai) (and_with_bit a' bt))))) - + ;; a is going to be the current result ;; carry is going to be false initially ;; b is the and of a and b[k] @@ -395,19 +469,19 @@ (let ak (top_k_bits a k') (let b' (and_with_bit ak (k_bit b k)) (mp_ifzero (mpz_sub k' 1) - (mult_step_k_h res b' bbltn false k) + (mult_step_k_h res b' bbltn false k) (let res' (mult_step_k_h res b' bbltn false k) (mult_step a b (reverseb res') n (mp_add k 1)))))))) (program bblast_bvmul ((a bblt) (b bblt) (n mpz)) bblt -(let ar (reverseb a) ;; reverse a and b so that we can build the circuit +(let ar (reverseb a) ;; reverse a and b so that we can build the circuit (let br (reverseb b) ;; from the least significant bit up (let res (and_with_bit ar (k_bit br 0)) - (mp_ifzero (mpz_sub n 1) ;; if multiplying 1 bit numbers no need to call mult_step + (mp_ifzero (mpz_sub n 1) ;; if multiplying 1 bit numbers no need to call mult_step res (mult_step ar br res n 1)))))) - + (declare bv_bbl_bvmul (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -420,18 +494,18 @@ (bblast_term n (bvmul n x y) rb))))))))))) - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST EQUALS ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + ; bit blast x = y ; for x,y of size n, it will return a conjuction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1}))) ; f is the accumulator formula that builds the equality in the right order (program bblast_eq_rec ((x bblt) (y bblt) (f formula)) formula - (match x + (match x (bbltn (match y (bbltn f) (default (fail formula)))) - ((bbltc fx x') (match y + ((bbltc fx x') (match y (bbltn (fail formula)) ((bbltc fy y') (bblast_eq_rec x' y' (and (iff fx fy) f))))) (default (fail formula)))) @@ -441,7 +515,23 @@ ((bbltc bx x') (match y ((bbltc by y') (bblast_eq_rec x' y' (iff bx by))) (default (fail formula)))) (default (fail formula)))) - + + +;; TODO: a temporary bypass for rewrites that we don't support yet. As soon +;; as we do, remove this rule. + +(declare bv_bbl_=_false + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq bx by) f) + (th_holds (iff (= (BitVec n) x y) false)))))))))))) + (declare bv_bbl_= (! n mpz (! x (term (BitVec n)) @@ -454,11 +544,110 @@ (! c (^ (bblast_eq bx by) f) (th_holds (iff (= (BitVec n) x y) f)))))))))))) - +(declare bv_bbl_=_swap + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq by bx) f) + (th_holds (iff (= (BitVec n) x y) f)))))))))))) + +(declare bv_bbl_=_alias_1 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! a (term (BitVec n)) + (! e (th_holds (= _ x a)) + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq bx by) f) + (th_holds (iff (= (BitVec n) a y) f)))))))))))))) + +(declare bv_bbl_=_alias_1_swap + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! a (term (BitVec n)) + (! e (th_holds (= _ x a)) + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq by bx) f) + (th_holds (iff (= (BitVec n) a y) f)))))))))))))) + +(declare bv_bbl_=_alias_2 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! a (term (BitVec n)) + (! e (th_holds (= _ y a)) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq bx by) f) + (th_holds (iff (= (BitVec n) x a) f)))))))))))))) + +(declare bv_bbl_=_alias_2_swap + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! a (term (BitVec n)) + (! e (th_holds (= _ y a)) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq by bx) f) + (th_holds (iff (= (BitVec n) x a) f)))))))))))))) + +(declare bv_bbl_=_alias_1_2 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! a1 (term (BitVec n)) + (! e1 (th_holds (= _ x a1)) + (! bbx (bblast_term n x bx) + (! a2 (term (BitVec n)) + (! e2 (th_holds (= _ y a2)) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq bx by) f) + (th_holds (iff (= (BitVec n) a1 a2) f)))))))))))))))) + +(declare bv_bbl_=_alias_1_2_swap + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! a1 (term (BitVec n)) + (! e1 (th_holds (= _ x a1)) + (! bbx (bblast_term n x bx) + (! a2 (term (BitVec n)) + (! e2 (th_holds (= _ y a2)) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq by bx) f) + (th_holds (iff (= (BitVec n) a1 a2) f)))))))))))))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVULT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvult ((x bblt) (y bblt) (n mpz)) formula (match x ( bbltn (fail formula)) @@ -480,10 +669,54 @@ (! c (^ (bblast_bvult bx by (mp_add n (~1))) f) (th_holds (iff (bvult n x y) f)))))))))))) +(declare bv_bbl_bvult_alias_1 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! a1 (term (BitVec n)) + (! e1 (th_holds (= _ x a1)) + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_bvult bx by (mp_add n (~1))) f) + (th_holds (iff (bvult n a1 y) f)))))))))))))) + +(declare bv_bbl_bvult_alias_2 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! a2 (term (BitVec n)) + (! e2 (th_holds (= _ y a2)) + (! bby (bblast_term n y by) + (! c (^ (bblast_bvult bx by (mp_add n (~1))) f) + (th_holds (iff (bvult n x a2) f)))))))))))))) + +(declare bv_bbl_bvult_alias_1_2 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! a1 (term (BitVec n)) + (! e1 (th_holds (= _ x a1)) + (! bbx (bblast_term n x bx) + (! a2 (term (BitVec n)) + (! e2 (th_holds (= _ y a2)) + (! bby (bblast_term n y by) + (! c (^ (bblast_bvult bx by (mp_add n (~1))) f) + (th_holds (iff (bvult n a1 a2) f)))))))))))))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVSLT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvslt ((x bblt) (y bblt) (n mpz)) formula (match x ( bbltn (fail formula)) @@ -506,7 +739,34 @@ (! bby (bblast_term n y by) (! c (^ (bblast_bvslt bx by n) f) (th_holds (iff (bvslt n x y) f)))))))))))) - + +(declare bv_bbl_bvslt_alias_1 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! a (term (BitVec n)) + (! e (th_holds (= _ x a)) + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_bvslt bx by n) f) + (th_holds (iff (bvslt n a y) f)))))))))))))) + +(declare bv_bbl_bvslt_alias_2 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! a (term (BitVec n)) + (! e (th_holds (= _ y a)) + (! bby (bblast_term n y by) + (! c (^ (bblast_bvslt bx by n) f) + (th_holds (iff (bvslt n x a) f)))))))))))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -543,8 +803,8 @@ ;; REWRITE RULES ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - + + ; rewrite rule : ; x + y = y + x (declare bvadd_symm @@ -552,7 +812,7 @@ (! x (term (BitVec n)) (! y (term (BitVec n)) (th_holds (= (BitVec n) (bvadd _ x y) (bvadd _ y x))))))) - + ;; (declare bvcrazy_rewrite ;; (! n mpz ;; (! x (term (BitVec n)) @@ -564,12 +824,12 @@ ;; (! s (^ (rewrite_scc xn yn) true) ;; (! u (! x (term (BitVec n)) (holds cln)) ;; (holds cln))))))))))) - + ;; (th_holds (= (BitVec n) (bvadd x y) (bvadd y x))))))) - - -; necessary? + + +; necessary? ;; (program calc_bvand ((a bv) (b bv)) bv ;; (match a ;; (bvn (match b (bvn bvn) (default (fail bv)))) @@ -578,7 +838,7 @@ ;; (default (fail bv)))))) ;; ; rewrite rule (w constants) : -;; ; a & b = c +;; ; a & b = c ;; (declare bvand_const (! c bv ;; (! a bv ;; (! b bv @@ -586,7 +846,7 @@ ;; (th_holds (= BitVec (bvand (a_bv a) (a_bv b)) (a_bv c)))))))) -;; making constant bit-vectors +;; making constant bit-vectors (program mk_ones ((n mpz)) bv (mp_ifzero n bvn (bvc b1 (mk_ones (mpz_sub n 1))))) @@ -594,7 +854,7 @@ (mp_ifzero n bvn (bvc b0 (mk_ones (mpz_sub n 1))))) - + ;; (bvxnor a b) => (bvnot (bvxor a b)) ;; (declare bvxnor_elim ;; (! n mpz @@ -621,7 +881,7 @@ ;; (! rwb (rw_term _ b (a_bv _ zero_bits)) ;; (rw_term _ (bvxor _ a b) ;; a')))))))))) - + ;; ;; (bvxor a 11) => (bvnot a) ;; (declare bvxor_one ;; (! n mpz @@ -635,7 +895,7 @@ ;; (rw_term _ (bvxor _ a b) ;; (bvnot _ a'))))))))))) - + ;; ;; (bvnot (bvnot a)) => a ;; (declare bvnot_idemp ;; (! n mpz @@ -644,4 +904,3 @@ ;; (! rwa (rw_term _ a a') ;; (rw_term _ (bvnot _ (bvnot _ a)) ;; a')))))) - diff --git a/src/Makefile.am b/src/Makefile.am index a3580989c..cfa4982ca 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -96,10 +96,14 @@ libcvc4_la_SOURCES = \ proof/skolemization_manager.h \ proof/theory_proof.cpp \ proof/theory_proof.h \ + proof/lemma_proof.cpp \ + proof/lemma_proof.h \ proof/uf_proof.cpp \ proof/uf_proof.h \ proof/unsat_core.cpp \ proof/unsat_core.h \ + proof/proof_output_channel.cpp \ + proof/proof_output_channel.h \ prop/cnf_stream.cpp \ prop/cnf_stream.h \ prop/prop_engine.cpp \ diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 643932781..e8a18481b 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -10,7 +10,7 @@ # Step 4: Generate X_options.h from X_options.sed # Step 5: Generate X_options.cpp from X_options.sed. # This stage also waits for X_options.h as otherwise it cannot compile. -# +# OPTIONS_SRC_FILES = \ arith_options \ @@ -424,4 +424,3 @@ $(DOCUMENTATION_FILES) : % : %_template %_template.sed mkoptions summary.sed # directories that are cleaned first. Without this rule, "distclean" # fails. %.Plo:; $(MKDIR_P) "$(dir $@)" && : > "$@" - diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index a1287b667..b9907aac9 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -830,4 +830,8 @@ void LFSCArithProof::printDeferredDeclarations(std::ostream& os, std::ostream& p // Nothing to do here at this point. } +void LFSCArithProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} + } /* CVC4 namespace */ diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index 788e4bd86..810d41155 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -74,6 +74,7 @@ public: virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren); }; diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index 8aba8dce9..aee236677 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -81,14 +81,29 @@ inline static bool match(TNode n1, TNode n2) { void ProofArray::setRowMergeTag(unsigned tag) { d_reasonRow = tag; + d_proofPrinter.d_row = tag; } void ProofArray::setRow1MergeTag(unsigned tag) { d_reasonRow1 = tag; + d_proofPrinter.d_row1 = tag; } void ProofArray::setExtMergeTag(unsigned tag) { d_reasonExt = tag; + d_proofPrinter.d_ext = tag; +} + +unsigned ProofArray::getRowMergeTag() const { + return d_reasonRow; +} + +unsigned ProofArray::getRow1MergeTag() const { + return d_reasonRow1; +} + +unsigned ProofArray::getExtMergeTag() const { + return d_reasonExt; } void ProofArray::toStream(std::ostream& out) { @@ -101,7 +116,7 @@ void ProofArray::toStream(std::ostream& out) { void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map) { Debug("pf::array") << "Printing array proof in LFSC : " << std::endl; - pf->debug_print("pf::array"); + pf->debug_print("pf::array", 0, &d_proofPrinter); Debug("pf::array") << std::endl; toStreamRecLFSC( out, tp, pf, 0, map ); Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl; @@ -114,7 +129,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, const LetMap& map) { Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; - pf->debug_print("pf::array"); + pf->debug_print("pf::array", 0, &d_proofPrinter); Debug("pf::array") << std::endl; if(tb == 0) { @@ -150,7 +165,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, pf->d_children[i + count]->d_node.isNull(); ++count) { Debug("pf::array") << "Found a congruence: " << std::endl; - pf->d_children[i+count]->debug_print("pf::array"); + pf->d_children[i+count]->debug_print("pf::array", 0, &d_proofPrinter); congruenceClosures.push_back(pf->d_children[i+count]); } @@ -220,48 +235,48 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, ++i; } } - Assert(neg >= 0); + + bool disequalityFound = (neg >= 0); + if (!disequalityFound) { + Debug("pf::array") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl; + Debug("pf::array") << "Proof for: " << pf->d_node << std::endl; + Assert(pf->d_node.getKind() == kind::EQUAL); + Assert(pf->d_node.getNumChildren() == 2); + Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst()); + } Node n1; std::stringstream ss, ss2; //Assert(subTrans.d_children.size() == pf->d_children.size() - 1); Debug("mgdx") << "\nsubtrans has " << subTrans.d_children.size() << " children\n"; - if(pf->d_children.size() > 2) { + if(!disequalityFound || pf->d_children.size() > 2) { n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map); } else { n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map); Debug("mgdx") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl; } - Node n2 = pf->d_children[neg]->d_node; - Assert(n2.getKind() == kind::NOT); - Debug("mgdx") << "\nhave proven: " << n1 << std::endl; - Debug("mgdx") << "n2 is " << n2 << std::endl; - Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl; - Debug("mgdx") << "n2[0] is " << n2[0] << std::endl; - - if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; } - if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; } - - if (pf->d_children[neg]->d_id == d_reasonExt) { - // The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b. - - // (clausify_false (contra _ .gl2 (or_elim_1 _ _ .gl1 FIXME))))))) (\ .glemc6 - - out << "(clausify_false (contra _ "; - out << ss.str(); - - toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map); + out << "(clausify_false (contra _ "; - out << " "; - out << ss2.str(); - out << "))"; + if (disequalityFound) { + Node n2 = pf->d_children[neg]->d_node; + Assert(n2.getKind() == kind::NOT); + Debug("mgdx") << "\nhave proven: " << n1 << std::endl; + Debug("mgdx") << "n2 is " << n2 << std::endl; + Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl; + Debug("mgdx") << "n2[0] is " << n2[0] << std::endl; - } else { - // The negative node is, e.g., a pure equality - out << "(clausify_false (contra _ "; + if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; } + if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; } - if(n2[0].getKind() == kind::APPLY_UF) { + if ((pf->d_children[neg]->d_id == d_reasonExt) || + (pf->d_children[neg]->d_id == theory::eq::MERGED_THROUGH_TRANS)) { + // Ext case: The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b. + out << ss.str(); + out << " "; + toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map); + out << ss2.str(); + } else if (n2[0].getKind() == kind::APPLY_UF) { out << "(trans _ _ _ _ "; out << "(symm _ _ _ "; out << ss.str(); @@ -276,16 +291,27 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("pf::array") << "ArrayProof::toStream: getLitName( " << n2[0] << " ) = " << ProofManager::getLitName(n2[0]) << std::endl; - out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; + out << " " << ProofManager::getLitName(n2[0]); } + } else { + Node n2 = pf->d_node; + Assert(n2.getKind() == kind::EQUAL); + Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1])); + + out << ss.str(); + out << " "; + ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, + n1[0].toExpr(), + n1[1].toExpr()); } + out << "))" << std::endl; return Node(); } if (pf->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) { Debug("mgd") << "\nok, looking at congruence:\n"; - pf->debug_print("mgd"); + pf->debug_print("mgd", 0, &d_proofPrinter); std::stack stk; for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) { Assert(!pf2->d_node.isNull()); @@ -315,7 +341,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n"; - pf2->debug_print("mgd"); + pf2->debug_print("mgd", 0, &d_proofPrinter); // Temp Debug("mgd") << "n1 is a proof for: " << pf2->d_children[0]->d_node << ". It is: " << n1 << std::endl; Debug("mgd") << "n2 is a proof for: " << pf2->d_children[1]->d_node << ". It is: " << n2 << std::endl; @@ -332,7 +358,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "SIDE IS 1\n"; if(!match(pf2->d_node, n1[1])) { Debug("mgd") << "IN BAD CASE, our first subproof is\n"; - pf2->d_children[0]->debug_print("mgd"); + pf2->d_children[0]->debug_print("mgd", 0, &d_proofPrinter); } Assert(match(pf2->d_node, n1[1])); side = 1; @@ -546,6 +572,20 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return pf->d_node; } + else if (pf->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) { + Debug("pf::array") << "Proof for: " << pf->d_node << std::endl; + Assert(pf->d_node.getKind() == kind::NOT); + Node n = pf->d_node[0]; + Assert(n.getKind() == kind::EQUAL); + Assert(n.getNumChildren() == 2); + Assert(n[0].isConst() && n[1].isConst()); + + ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, + n[0].toExpr(), + n[1].toExpr()); + return pf->d_node; + } + else if (pf->d_id == theory::eq::MERGED_THROUGH_TRANS) { bool firstNeg = false; bool secondNeg = false; @@ -554,7 +594,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Assert(pf->d_children.size() >= 2); std::stringstream ss; Debug("mgd") << "\ndoing trans proof[[\n"; - pf->debug_print("mgd"); + pf->debug_print("mgd", 0, &d_proofPrinter); Debug("mgd") << "\n"; Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n"; @@ -772,7 +812,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Warning() << "\n\ntrans proof failure at step " << i << "\n\n"; Warning() << "0 proves " << n1 << "\n"; Warning() << "1 proves " << n2 << "\n\n"; - pf->debug_print("mgdx",0); + pf->debug_print("mgdx", 0, &d_proofPrinter); //toStreamRec(Warning.getStream(), pf, 0); Warning() << "\n\n"; Unreachable(); @@ -931,6 +971,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, t4 = pf->d_children[0]->d_node[0][side][0][2]; ret = pf->d_node; + // The order of indices needs to match; we might have to swap t1 and t2 and then apply symmetry. + bool swap = (t2 == pf->d_children[0]->d_node[0][side][0][1]); + Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; Assert(pf->d_children.size() == 1); @@ -939,28 +982,31 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("pf::array") << "Subproof is: " << ss.str() << std::endl; + if (swap) { + out << "(symm _ _ _ "; + } + out << "(negativerow _ _ "; - tp->printTerm(t1.toExpr(), out, map); + tp->printTerm(swap ? t2.toExpr() : t1.toExpr(), out, map); out << " "; - tp->printTerm(t2.toExpr(), out, map); + tp->printTerm(swap ? t1.toExpr() : t2.toExpr(), out, map); out << " "; tp->printTerm(t3.toExpr(), out, map); out << " "; tp->printTerm(t4.toExpr(), out, map); out << " "; - - // if (subproof[0][1] == t3) { - Debug("pf::array") << "Dont need symmetry!" << std::endl; - out << ss.str(); - // } else { - // Debug("pf::array") << "Need symmetry!" << std::endl; - // out << "(negsymm _ _ _ " << ss.str() << ")"; - // } + if (side != 0) { + out << "(negsymm _ _ _ " << ss.str() << ")"; + } else { + out << ss.str(); + } out << ")"; - // Unreachable(); + if (swap) { + out << ") "; + } return ret; } @@ -1071,13 +1117,12 @@ void ArrayProof::registerTerm(Expr term) { } std::string ArrayProof::skolemToLiteral(Expr skolem) { + Debug("pf::array") << "ArrayProof::skolemToLiteral( " << skolem << ")" << std::endl; Assert(d_skolemToLiteral.find(skolem) != d_skolemToLiteral.end()); return d_skolemToLiteral[skolem]; } void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { - Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedTerm: term = " << term << std::endl; - Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAY); if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAY) { @@ -1154,7 +1199,21 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& m void LFSCArrayProof::printOwnedSort(Type type, std::ostream& os) { Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl; Assert (type.isArray() || type.isSort()); - os << type <<" "; + if (type.isArray()){ + ArrayType array_type(type); + + Debug("pf::array") << "LFSCArrayProof::printOwnedSort: type is an array. Index type: " + << array_type.getIndexType() + << ", element type: " << array_type.getConstituentType() << std::endl; + + os << "(Array "; + printSort(array_type.getIndexType(), os); + os << " "; + printSort(array_type.getConstituentType(), os); + os << ")"; + } else { + os << type <<" "; + } } void LFSCArrayProof::printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren) { @@ -1169,8 +1228,6 @@ void LFSCArrayProof::printTheoryLemmaProof(std::vector& lemma, std::ostrea void LFSCArrayProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { // declaring the sorts - Debug("pf::array") << "Arrays declaring sorts..." << std::endl; - for (TypeSet::const_iterator it = d_sorts.begin(); it != d_sorts.end(); ++it) { if (!ProofManager::currentPM()->wasPrinted(*it)) { os << "(% " << *it << " sort\n"; @@ -1229,6 +1286,7 @@ void LFSCArrayProof::printTermDeclarations(std::ostream& os, std::ostream& paren void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) { Debug("pf::array") << "Array: print deferred declarations called" << std::endl; + unsigned count = 1; for (ExprSet::const_iterator it = d_skolemDeclarations.begin(); it != d_skolemDeclarations.end(); ++it) { Expr term = *it; Node equality = ProofManager::getSkolemizationManager()->getDisequality(*it); @@ -1237,7 +1295,7 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p << "It is a witness for: " << equality << std::endl; std::ostringstream newSkolemLiteral; - newSkolemLiteral << ".sl" << d_skolemToLiteral.size(); + newSkolemLiteral << ".sl" << count++; std::string skolemLiteral = newSkolemLiteral.str(); d_skolemToLiteral[*it] = skolemLiteral; @@ -1251,13 +1309,12 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p Node array_two = equality[0][1]; LetMap map; - os << "(ext _ _ "; printTerm(array_one.toExpr(), os, map); os << " "; printTerm(array_two.toExpr(), os, map); os << " (\\ "; - printTerm(*it, os, map); + os << ProofManager::sanitize(*it); os << " (\\ "; os << skolemLiteral.c_str(); os << "\n"; @@ -1266,4 +1323,8 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p } } +void LFSCArrayProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} + } /* CVC4 namespace */ diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index fb25c9433..076ba7381 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -30,6 +30,32 @@ namespace CVC4 { //proof object outputted by TheoryARRAY class ProofArray : public Proof { private: + class ArrayProofPrinter : public theory::eq::EqProof::PrettyPrinter { + public: + ArrayProofPrinter() : d_row(0), d_row1(0), d_ext(0) { + } + + std::string printTag(unsigned tag) { + if (tag == theory::eq::MERGED_THROUGH_CONGRUENCE) return "Congruence"; + if (tag == theory::eq::MERGED_THROUGH_EQUALITY) return "Pure Equality"; + if (tag == theory::eq::MERGED_THROUGH_REFLEXIVITY) return "Reflexivity"; + if (tag == theory::eq::MERGED_THROUGH_CONSTANTS) return "Constants"; + if (tag == theory::eq::MERGED_THROUGH_TRANS) return "Transitivity"; + + if (tag == d_row) return "Read Over Write"; + if (tag == d_row1) return "Read Over Write (1)"; + if (tag == d_ext) return "Extensionality"; + + std::ostringstream result; + result << tag; + return result.str(); + } + + unsigned d_row; + unsigned d_row1; + unsigned d_ext; + }; + Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, unsigned tb, @@ -41,6 +67,8 @@ private: unsigned d_reasonRow1; /** Merge tag for EXT applications */ unsigned d_reasonExt; + + ArrayProofPrinter d_proofPrinter; public: ProofArray(theory::eq::EqProof* pf) : d_proof(pf) {} //it is simply an equality engine proof @@ -53,6 +81,10 @@ public: void setRowMergeTag(unsigned tag); void setRow1MergeTag(unsigned tag); void setExtMergeTag(unsigned tag); + + unsigned getRowMergeTag() const; + unsigned getRow1MergeTag() const; + unsigned getExtMergeTag() const; }; namespace theory { @@ -91,6 +123,7 @@ public: virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren); }; diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index b63782226..479266db4 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -15,9 +15,11 @@ **/ -#include "proof/bitvector_proof.h" #include "options/bv_options.h" +#include "proof/array_proof.h" +#include "proof/bitvector_proof.h" #include "proof/clause_id.h" +#include "proof/proof_output_channel.h" #include "proof/proof_utils.h" #include "proof/sat_proof_implementation.h" #include "prop/bvminisat/bvminisat.h" @@ -80,20 +82,40 @@ BVSatProof* BitVectorProof::getSatProof() { } void BitVectorProof::registerTermBB(Expr term) { + Debug("pf::bv") << "BitVectorProof::registerTermBB( " << term << " )" << std::endl; + if (d_seenBBTerms.find(term) != d_seenBBTerms.end()) return; d_seenBBTerms.insert(term); d_bbTerms.push_back(term); + + // If this term gets used in the final proof, we will want to register it. However, + // we don't know this at this point; and when the theory proof engine sees it, if it belongs + // to another theory, it won't register it with this proof. So, we need to tell the + // engine to inform us. + + if (theory::Theory::theoryOf(term) != theory::THEORY_BV) { + Debug("pf::bv") << "\tMarking term " << term << " for future BV registration" << std::endl; + d_proofEngine->markTermForFutureRegistration(term, theory::THEORY_BV); + } } void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) { + Debug("pf::bv") << "BitVectorProof::registerAtomBB( " << atom << ", " << atom_bb << " )" << std::endl; + Expr def = atom.iffExpr(atom_bb); - d_bbAtoms.insert(std::make_pair(atom, def)); + d_bbAtoms.insert(std::make_pair(atom, def)); registerTerm(atom); + + // Register the atom's terms for bitblasting + registerTermBB(atom[0]); + registerTermBB(atom[1]); } void BitVectorProof::registerTerm(Expr term) { + Debug("pf::bv") << "BitVectorProof::registerTerm( " << term << " )" << std::endl; + d_usedBB.insert(term); if (Theory::isLeafOf(term, theory::THEORY_BV) && @@ -101,6 +123,11 @@ void BitVectorProof::registerTerm(Expr term) { d_declarations.insert(term); } + Debug("pf::bv") << "Going to register children: " << std::endl; + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + Debug("pf::bv") << "\t" << term[i] << std::endl; + } + // don't care about parametric operators for bv? for (unsigned i = 0; i < term.getNumChildren(); ++i) { d_proofEngine->registerTerm(term[i]); @@ -108,6 +135,7 @@ void BitVectorProof::registerTerm(Expr term) { } std::string BitVectorProof::getBBTermName(Expr expr) { + Debug("pf::bv") << "BitVectorProof::getBBTermName( " << expr << " ) = bt" << expr.getId() << std::endl; std::ostringstream os; os << "bt"<< expr.getId(); return os.str(); @@ -122,6 +150,8 @@ void BitVectorProof::startBVConflict(CVC4::BVMinisat::Solver::TLit lit) { } void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl) { + Debug("pf::bv") << "BitVectorProof::endBVConflict called" << std::endl; + std::vector expr_confl; for (int i = 0; i < confl.size(); ++i) { prop::SatLiteral lit = prop::BVMinisatSatSolver::toSatLiteral(confl[i]); @@ -129,6 +159,7 @@ void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom; expr_confl.push_back(expr_lit); } + Expr conflict = utils::mkSortedExpr(kind::OR, expr_confl); Debug("pf::bv") << "Make conflict for " << conflict << std::endl; @@ -144,25 +175,99 @@ void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl ClauseId clause_id = d_resolutionProof->registerAssumptionConflict(confl); d_bbConflictMap[conflict] = clause_id; d_resolutionProof->endResChain(clause_id); - Debug("pf::bv") << "BitVectorProof::endBVConflict id"< " << conflict << "\n"; + Debug("pf::bv") << "BitVectorProof::endBVConflict id" < " << conflict << "\n"; d_isAssumptionConflict = false; } void BitVectorProof::finalizeConflicts(std::vector& conflicts) { + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { Debug("pf::bv") << "Construct full proof." << std::endl; d_resolutionProof->constructProof(); return; } - for(unsigned i = 0; i < conflicts.size(); ++i) { + + for (unsigned i = 0; i < conflicts.size(); ++i) { Expr confl = conflicts[i]; - Debug("pf::bv") << "Finalize conflict " << confl << std::endl; - //Assert (d_bbConflictMap.find(confl) != d_bbConflictMap.end()); - if(d_bbConflictMap.find(confl) != d_bbConflictMap.end()){ + Debug("pf::bv") << "Finalize conflict #" << i << ": " << confl << std::endl; + + // Special case: if the conflict has a (true) or a (not false) in it, it is trivial... + bool ignoreConflict = false; + if ((confl.isConst() && confl.getConst()) || + (confl.getKind() == kind::NOT && confl[0].isConst() && !confl[0].getConst())) { + ignoreConflict = true; + } else if (confl.getKind() == kind::OR) { + for (unsigned k = 0; k < confl.getNumChildren(); ++k) { + if ((confl[k].isConst() && confl[k].getConst()) || + (confl[k].getKind() == kind::NOT && confl[k][0].isConst() && !confl[k][0].getConst())) { + ignoreConflict = true; + } + } + } + if (ignoreConflict) { + Debug("pf::bv") << "Ignoring conflict due to (true) or (not false)" << std::endl; + continue; + } + + if (d_bbConflictMap.find(confl) != d_bbConflictMap.end()) { ClauseId id = d_bbConflictMap[confl]; d_resolutionProof->collectClauses(id); - }else{ - Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl; + } else { + // There is no exact match for our conflict, but maybe it is a subset of another conflict + ExprToClauseId::const_iterator it; + bool matchFound = false; + for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) { + Expr possibleMatch = it->first; + if (possibleMatch.getKind() != kind::OR) { + // This is a single-node conflict. If this node is in the conflict we're trying to prove, + // we have a match. + for (unsigned k = 0; k < confl.getNumChildren(); ++k) { + if (confl[k] == possibleMatch) { + matchFound = true; + d_resolutionProof->collectClauses(it->second); + break; + } + } + } else { + if (possibleMatch.getNumChildren() > confl.getNumChildren()) + continue; + + unsigned k = 0; + bool matching = true; + for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) { + // j is the index in possibleMatch + // k is the index in confl + while (k < confl.getNumChildren() && confl[k] != possibleMatch[j]) { + ++k; + } + if (k == confl.getNumChildren()) { + // We couldn't find a match for possibleMatch[j], so not a match + matching = false; + break; + } + } + + if (matching) { + Debug("pf::bv") << "Collecting info from a sub-conflict" << std::endl; + d_resolutionProof->collectClauses(it->second); + matchFound = true; + break; + } + } + } + + if (!matchFound) { + Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl + << "Dumping existing conflicts:" << std::endl; + + i = 0; + for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) { + ++i; + Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl; + } + + Unreachable(); + } } } } @@ -238,11 +343,25 @@ void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const LetMa printBitOf(term, os, map); return; } - case kind::VARIABLE: + + case kind::VARIABLE: { + os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")"; + return; + } + case kind::SKOLEM: { - os << "(a_var_bv " << utils::getSize(term)<<" " << ProofManager::sanitize(term) <<")"; + + // TODO: we need to distinguish between "real" skolems (e.g. from array) and "fake" skolems, + // like ITE terms. Is there a more elegant way? + + if (ProofManager::getSkolemizationManager()->isSkolem(term)) { + os << ProofManager::sanitize(term); + } else { + os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")"; + } return; } + default: Unreachable(); } @@ -258,14 +377,7 @@ void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const LetMap& m << ", var = " << var << std::endl; os << "(bitof "; - if (var.getKind() == kind::VARIABLE || var.getKind() == kind::SKOLEM) { - // If var is "simple", we can just sanitize and print - os << ProofManager::sanitize(var); - } else { - // If var is "complex", it can belong to another theory. Therefore, dispatch again. - d_proofEngine->printBoundTerm(var, os, map); - } - + os << d_exprToVariableName[var]; os << " " << bit << ")"; } @@ -349,14 +461,16 @@ void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, co void LFSCBitVectorProof::printOwnedSort(Type type, std::ostream& os) { Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedSort( " << type << " )" << std::endl; - Assert (type.isBitVector()); unsigned width = utils::getSize(type); os << "(BitVec "<& lemma, std::ostream& os, std::ostream& paren) { + Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called" << std::endl; Expr conflict = utils::mkSortedExpr(kind::OR, lemma); + Debug("pf::bv") << "\tconflict = " << conflict << std::endl; + if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) { std::ostringstream lemma_paren; for (unsigned i = 0; i < lemma.size(); ++i) { @@ -377,7 +491,7 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector& lemma, std::os // print corresponding literal in bv sat solver prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable(); os << pm->getAtomName(bb_var, "bb"); - os <<"(\\unit"<& lemma, std::os d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren); os <first; + + if (possibleMatch.getKind() != kind::OR) { + // This is a single-node conflict. If this node is in the conflict we're trying to prove, + // we have a match. + matching = false; + + for (unsigned k = 0; k < conflict.getNumChildren(); ++k) { + if (conflict[k] == possibleMatch) { + matching = true; + break; + } + } + } else { + if (possibleMatch.getNumChildren() > conflict.getNumChildren()) + continue; + + unsigned k = 0; + + matching = true; + for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) { + // j is the index in possibleMatch + // k is the index in conflict + while (k < conflict.getNumChildren() && conflict[k] != possibleMatch[j]) { + ++k; + } + if (k == conflict.getNumChildren()) { + // We couldn't find a match for possibleMatch[j], so not a match + matching = false; + break; + } + } + } + + if (matching) { + Debug("pf::bv") << "Found a match with conflict #" << i << ": " << std::endl << possibleMatch << std::endl; + // The rest is just a copy of the usual handling, if a precise match is found. + // We only use the literals that appear in the matching conflict, though, and not in the + // original lemma - as these may not have even been bit blasted! + std::ostringstream lemma_paren; + + if (possibleMatch.getKind() == kind::OR) { + for (unsigned i = 0; i < possibleMatch.getNumChildren(); ++i) { + Expr lit = possibleMatch[i]; + + if (lit.getKind() == kind::NOT) { + os << "(intro_assump_t _ _ _ "; + } else { + os << "(intro_assump_f _ _ _ "; + } + lemma_paren <<")"; + // print corresponding literal in main sat solver + ProofManager* pm = ProofManager::currentPM(); + CnfProof* cnf = pm->getCnfProof(); + prop::SatLiteral main_lit = cnf->getLiteral(lit); + os << pm->getLitName(main_lit); + os <<" "; + // print corresponding literal in bv sat solver + prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable(); + os << pm->getAtomName(bb_var, "bb"); + os <<"(\\ unit"<getCnfProof(); + prop::SatLiteral main_lit = cnf->getLiteral(lit); + os << pm->getLitName(main_lit); + os <<" "; + // print corresponding literal in bv sat solver + prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable(); + os << pm->getAtomName(bb_var, "bb"); + os <<"(\\ unit"<second; + d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren); + os <first << std::endl; + } + + Unreachable(); } } @@ -402,7 +625,13 @@ void LFSCBitVectorProof::printTermDeclarations(std::ostream& os, std::ostream& p ExprSet::const_iterator it = d_declarations.begin(); ExprSet::const_iterator end = d_declarations.end(); for (; it != end; ++it) { - os << "(% " << ProofManager::sanitize(*it) <<" var_bv\n"; + if ((it->isVariable() || it->isConst()) && !ProofManager::getSkolemizationManager()->isSkolem(*it)) { + d_exprToVariableName[*it] = ProofManager::sanitize(*it); + } else { + d_exprToVariableName[*it] = assignAlias(*it); + } + + os << "(% " << d_exprToVariableName[*it] <<" var_bv" << "\n"; paren <<")"; } } @@ -411,15 +640,43 @@ void LFSCBitVectorProof::printDeferredDeclarations(std::ostream& os, std::ostrea // Nothing to do here at this point. } +void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + // Print "trust" statements to bind complex bv variables to their associated terms + + ExprToString::const_iterator it = d_assignedAliases.begin(); + ExprToString::const_iterator end = d_assignedAliases.end(); + + for (; it != end; ++it) { + Debug("pf::bv") << "Printing aliasing declaration for: " << *it << std::endl; + std::stringstream declaration; + declaration << ".fbvd" << d_aliasToBindDeclaration.size(); + d_aliasToBindDeclaration[it->second] = declaration.str(); + + os << "(th_let_pf _ "; + + os << "(trust_f "; + os << "(= (BitVec " << utils::getSize(it->first) << ") "; + os << "(a_var_bv " << utils::getSize(it->first) << " " << it->second << ") "; + LetMap emptyMap; + d_proofEngine->printBoundTerm(it->first, os, emptyMap); + os << ")) "; + os << "(\\ "<< d_aliasToBindDeclaration[it->second] << "\n"; + paren << "))"; + } + + os << "\n"; +} + void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { // TODO: once we have the operator elimination rules remove those that we // eliminated Assert (term.getType().isBitVector()); Kind kind = term.getKind(); - if (Theory::isLeafOf(term, theory::THEORY_BV) && - !term.isConst()) { - os << "(bv_bbl_var "< 1) { + // This is not the inner-most operation; only child i+1 can be aliased + if (hasAlias(term[i])) {os << "_alias_2";} + } else { + // This is the inner-most operation; both children can be aliased + if (hasAlias(term[i-1]) || hasAlias(term[i])) {os << "_alias";} + if (hasAlias(term[i-1])) {os << "_1";} + if (hasAlias(term[i])) {os << "_2";} + } + if (kind == kind::BITVECTOR_CONCAT) { - os << " " << utils::getSize(term) <<" _ "; + os << " " << utils::getSize(term) << " _"; } - os <<" _ _ _ _ _ _ "; + os << " _ _ _ _ _ _ "; } - os << getBBTermName(term[0]) <<" "; + + if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";} + os << getBBTermName(term[0]) << " "; for (unsigned i = 1; i < term.getNumChildren(); ++i) { + if (hasAlias(term[i])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[i]]] << " ";} os << getBBTermName(term[i]); os << ") "; } return; } + case kind::BITVECTOR_NEG : case kind::BITVECTOR_NOT : case kind::BITVECTOR_ROTATE_LEFT : case kind::BITVECTOR_ROTATE_RIGHT : { - os <<"(bv_bbl_"<().repeatAmount; @@ -501,7 +781,9 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { unsigned amount = term.getOperator().getConst().zeroExtendAmount; os << amount; } + os <<" _ _ _ _ "; + if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";} os << getBBTermName(term[0]); os <<")"; return; @@ -539,7 +821,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { } } -void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) { +void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool swap) { Kind kind = atom.getKind(); switch(kind) { case kind::BITVECTOR_ULT : @@ -550,11 +832,28 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) { case kind::BITVECTOR_SLE : case kind::BITVECTOR_SGT : case kind::BITVECTOR_SGE : - case kind::EQUAL: - { - os <<"(bv_bbl_" << utils::toLFSCKind(atom.getKind()); + case kind::EQUAL: { + Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl; + + os << "(bv_bbl_" << utils::toLFSCKind(atom.getKind()); + + if (hasAlias(atom[0]) || hasAlias(atom[1])) {os << "_alias";} + if (hasAlias(atom[0])) {os << "_1";} + if (hasAlias(atom[1])) {os << "_2";} + + if (swap) {os << "_swap";} + os << " _ _ _ _ _ _ "; - os << getBBTermName(atom[0])<<" " << getBBTermName(atom[1]) <<")"; + + if (hasAlias(atom[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[0]]] << " ";} + os << getBBTermName(atom[0]); + + os << " "; + + if (hasAlias(atom[1])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[1]]] << " ";} + os << getBBTermName(atom[1]); + + os << ")"; return; } default: @@ -562,19 +861,53 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) { } } +void LFSCBitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os) { + Assert(atom.getKind() == kind::EQUAL); + + os << "(bv_bbl_=_false"; + os << " _ _ _ _ _ _ "; + if (hasAlias(atom[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[0]]] << " ";} + os << getBBTermName(atom[0]); + + os << " "; + + if (hasAlias(atom[1])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[1]]] << " ";} + os << getBBTermName(atom[1]); + + os << ")"; +} void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) { // bit-blast terms + { + Debug("pf::bv") << "LFSCBitVectorProof::printBitblasting: the bitblasted terms are: " << std::endl; + std::vector::const_iterator it = d_bbTerms.begin(); + std::vector::const_iterator end = d_bbTerms.end(); + + Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER); + + for (; it != end; ++it) { + if (d_usedBB.find(*it) == d_usedBB.end()) { + Debug("pf::bv") << "\t" << *it << "\t(UNUSED)" << std::endl; + } else { + Debug("pf::bv") << "\t" << *it << std::endl; + } + } + + Debug("pf::bv") << std::endl; + } + std::vector::const_iterator it = d_bbTerms.begin(); std::vector::const_iterator end = d_bbTerms.end(); for (; it != end; ++it) { if (d_usedBB.find(*it) == d_usedBB.end() && options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) continue; - os <<"(decl_bblast _ _ _ "; + + os << "(decl_bblast _ _ _ "; printTermBitblasting(*it, os); - os << "(\\ "<< getBBTermName(*it); - paren <<"\n))"; + os << "(\\ "<< getBBTermName(*it) << "\n"; + paren << "))"; } // bit-blast atoms ExprToExpr::const_iterator ait = d_bbAtoms.begin(); @@ -589,7 +922,35 @@ void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) bool val = ait->first.getConst(); os << "(iff_symm " << (val ? "true" : "false" ) << ")"; } else { - printAtomBitblasting(ait->first, os); + Assert(ait->first == ait->second[0]); + + bool swap = false; + if (ait->first.getKind() == kind::EQUAL) { + Expr bitwiseEquivalence = ait->second[1]; + if ((bitwiseEquivalence.getKind() == kind::CONST_BOOLEAN) && !bitwiseEquivalence.getConst()) { + printAtomBitblastingToFalse(ait->first, os); + } else { + if (bitwiseEquivalence.getKind() != kind::AND) { + // Just one bit + if (bitwiseEquivalence.getNumChildren() > 0 && bitwiseEquivalence[0].getKind() == kind::BITVECTOR_BITOF) { + swap = (ait->first[1] == bitwiseEquivalence[0][0]); + } + } else { + // Multiple bits + if (bitwiseEquivalence[0].getNumChildren() > 0 && + bitwiseEquivalence[0][0].getKind() == kind::BITVECTOR_BITOF) { + swap = (ait->first[1] == bitwiseEquivalence[0][0][0]); + } else if (bitwiseEquivalence[0].getNumChildren() > 0 && + bitwiseEquivalence[0][1].getKind() == kind::BITVECTOR_BITOF) { + swap = (ait->first[0] == bitwiseEquivalence[0][1][0]); + } + } + + printAtomBitblasting(ait->first, os, swap); + } + } else { + printAtomBitblasting(ait->first, os, swap); + } } os <<"(\\ " << ProofManager::getPreprocessedAssertionName(ait->second) <<"\n"; @@ -606,25 +967,53 @@ void LFSCBitVectorProof::printResolutionProof(std::ostream& os, used_lemmas); Assert (used_lemmas.empty()); + IdToSatClause::iterator it2; + Debug("pf::bv") << std::endl << "BV Used inputs: " << std::endl; + for (it2 = used_inputs.begin(); it2 != used_inputs.end(); ++it2) { + Debug("pf::bv") << "\t input = " << *(it2->second) << std::endl; + } + Debug("pf::bv") << std::endl; + // print mapping between theory atoms and internal SAT variables - os << ";; BB atom mapping\n"; + os << std::endl << ";; BB atom mapping\n" << std::endl; + + std::set atoms; + d_cnfProof->collectAtomsForClauses(used_inputs, atoms); - NodeSet atoms; - d_cnfProof->collectAtomsForClauses(used_inputs,atoms); + std::set::iterator atomIt; + Debug("pf::bv") << std::endl << "BV Dumping atoms from inputs: " << std::endl << std::endl; + for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) { + Debug("pf::bv") << "\tAtom: " << *atomIt << std::endl; + } + Debug("pf::bv") << std::endl; // first print bit-blasting printBitblasting(os, paren); // print CNF conversion proof for bit-blasted facts d_cnfProof->printAtomMapping(atoms, os, paren); - os << ";; Bit-blasting definitional clauses \n"; + os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl; for (IdToSatClause::iterator it = used_inputs.begin(); it != used_inputs.end(); ++it) { d_cnfProof->printCnfProofForClause(it->first, it->second, os, paren); } - os << ";; Bit-blasting learned clauses \n"; + os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl; d_resolutionProof->printResolutions(os, paren); } +std::string LFSCBitVectorProof::assignAlias(Expr expr) { + static unsigned counter = 0; + Assert(d_exprToVariableName.find(expr) == d_exprToVariableName.end()); + std::stringstream ss; + ss << "fbv" << counter++; + Debug("pf::bv") << "assignAlias( " << expr << ") = " << ss.str() << std::endl; + d_assignedAliases[expr] = ss.str(); + return ss.str(); +} + +bool LFSCBitVectorProof::hasAlias(Expr expr) { + return d_assignedAliases.find(expr) != d_assignedAliases.end(); +} + } /* namespace CVC4 */ diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 4a1f4015d..4e5e98541 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -60,6 +60,7 @@ typedef __gnu_cxx::hash_set ExprSet; typedef __gnu_cxx::hash_map ExprToClauseId; typedef __gnu_cxx::hash_map ExprToId; typedef __gnu_cxx::hash_map ExprToExpr; +typedef __gnu_cxx::hash_map ExprToString; class BitVectorProof : public TheoryProof { protected: @@ -108,7 +109,8 @@ public: virtual void registerTerm(Expr term); virtual void printTermBitblasting(Expr term, std::ostream& os) = 0; - virtual void printAtomBitblasting(Expr term, std::ostream& os) = 0; + virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap) = 0; + virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os) = 0; virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0; virtual void printResolutionProof(std::ostream& os, std::ostream& paren) = 0; @@ -123,6 +125,12 @@ class LFSCBitVectorProof: public BitVectorProof { void printPredicate(Expr term, std::ostream& os, const LetMap& map); void printOperatorParametric(Expr term, std::ostream& os, const LetMap& map); void printBitOf(Expr term, std::ostream& os, const LetMap& map); + + ExprToString d_exprToVariableName; + ExprToString d_assignedAliases; + std::map d_aliasToBindDeclaration; + std::string assignAlias(Expr expr); + bool hasAlias(Expr expr); public: LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) :BitVectorProof(bv, proofEngine) @@ -130,11 +138,13 @@ public: virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); virtual void printOwnedSort(Type type, std::ostream& os); virtual void printTermBitblasting(Expr term, std::ostream& os); - virtual void printAtomBitblasting(Expr term, std::ostream& os); + virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap); + virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os); virtual void printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren); virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren); virtual void printBitblasting(std::ostream& os, std::ostream& paren); virtual void printResolutionProof(std::ostream& os, std::ostream& paren); }; diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 19e9cbac9..abe48e3cd 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -19,6 +19,7 @@ #include "proof/clause_id.h" #include "proof/proof_manager.h" +#include "proof/proof_utils.h" #include "proof/theory_proof.h" #include "prop/cnf_stream.h" #include "prop/minisat/minisat.h" @@ -32,7 +33,6 @@ CnfProof::CnfProof(prop::CnfStream* stream, : d_cnfStream(stream) , d_clauseToAssertion(ctx) , d_assertionToProofRule(ctx) - , d_clauseIdToOwnerTheory(ctx) , d_currentAssertionStack() , d_currentDefinitionStack() , d_clauseToDefinition(ctx) @@ -103,7 +103,6 @@ void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) { setClauseAssertion(clause, current_assertion); setClauseDefinition(clause, current_expr); - registerExplanationLemma(clause); } void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { @@ -143,16 +142,15 @@ void CnfProof::registerAssertion(Node assertion, ProofRule reason) { d_assertionToProofRule.insert(assertion, reason); } -void CnfProof::registerExplanationLemma(ClauseId clauseId) { - d_clauseIdToOwnerTheory.insert(clauseId, getExplainerTheory()); +LemmaProofRecipe CnfProof::getProofRecipe(const std::set &lemma) { + Assert(d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end()); + return d_lemmaToProofRecipe[lemma]; } -theory::TheoryId CnfProof::getOwnerTheory(ClauseId clause) { - Assert(d_clauseIdToOwnerTheory.find(clause) != d_clauseIdToOwnerTheory.end()); - return d_clauseIdToOwnerTheory[clause]; +bool CnfProof::haveProofRecipe(const std::set &lemma) { + return d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end(); } - void CnfProof::setCnfDependence(Node from, Node to) { Debug("proof:cnf") << "CnfProof::setCnfDependence " << "from " << from << std::endl @@ -183,12 +181,10 @@ Node CnfProof::getCurrentAssertion() { return d_currentAssertionStack.back(); } -void CnfProof::setExplainerTheory(theory::TheoryId theory) { - d_explainerTheory = theory; -} - -theory::TheoryId CnfProof::getExplainerTheory() { - return d_explainerTheory; +void CnfProof::setProofRecipe(LemmaProofRecipe* proofRecipe) { + Assert(proofRecipe); + Assert(proofRecipe->getNumSteps() > 0); + d_lemmaToProofRecipe[proofRecipe->getBaseAssertions()] = *proofRecipe; } void CnfProof::pushCurrentDefinition(Node definition) { @@ -212,22 +208,19 @@ Node CnfProof::getCurrentDefinition() { return d_currentDefinitionStack.back(); } - Node CnfProof::getAtom(prop::SatVariable var) { prop::SatLiteral lit (var); Node node = d_cnfStream->getNode(lit); return node; } - void CnfProof::collectAtoms(const prop::SatClause* clause, - NodeSet& atoms) { + std::set& atoms) { for (unsigned i = 0; i < clause->size(); ++i) { prop::SatLiteral lit = clause->operator[](i); prop::SatVariable var = lit.getSatVariable(); TNode atom = getAtom(var); if (atoms.find(atom) == atoms.end()) { - Assert (atoms.find(atom) == atoms.end()); atoms.insert(atom); } } @@ -237,14 +230,75 @@ prop::SatLiteral CnfProof::getLiteral(TNode atom) { return d_cnfStream->getLiteral(atom); } +bool CnfProof::hasLiteral(TNode atom) { + return d_cnfStream->hasLiteral(atom); +} + +void CnfProof::ensureLiteral(TNode atom, bool noPreregistration) { + d_cnfStream->ensureLiteral(atom, noPreregistration); +} + void CnfProof::collectAtomsForClauses(const IdToSatClause& clauses, - NodeSet& atom_map) { + std::set& atoms) { IdToSatClause::const_iterator it = clauses.begin(); for (; it != clauses.end(); ++it) { const prop::SatClause* clause = it->second; - collectAtoms(clause, atom_map); + collectAtoms(clause, atoms); } +} + +void CnfProof::collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses, + std::set& atoms, + NodePairSet& rewrites) { + IdToSatClause::const_iterator it = lemmaClauses.begin(); + for (; it != lemmaClauses.end(); ++it) { + const prop::SatClause* clause = it->second; + + // TODO: just calculate the map from ID to recipe once, + // instead of redoing this over and over again + std::vector clause_expr; + std::set clause_expr_nodes; + for(unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = (*clause)[i]; + Node node = getAtom(lit.getSatVariable()); + Expr atom = node.toExpr(); + if (atom.isConst()) { + Assert (atom == utils::mkTrue()); + continue; + } + clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node); + } + + LemmaProofRecipe recipe = getProofRecipe(clause_expr_nodes); + for (unsigned i = 0; i < recipe.getNumSteps(); ++i) { + const LemmaProofRecipe::ProofStep* proofStep = recipe.getStep(i); + Node atom = proofStep->getLiteral(); + + if (atom == Node()) { + // The last proof step always has the empty node as its target... + continue; + } + + if (atom.getKind() == kind::NOT) { + atom = atom[0]; + } + + atoms.insert(atom); + } + + LemmaProofRecipe::RewriteIterator rewriteIt; + for (rewriteIt = recipe.rewriteBegin(); rewriteIt != recipe.rewriteEnd(); ++rewriteIt) { + rewrites.insert(NodePair(rewriteIt->first, rewriteIt->second)); + + // The unrewritten terms also need to have literals, so insert them into atoms + Node rewritten = rewriteIt->first; + if (rewritten.getKind() == kind::NOT) { + rewritten = rewritten[0]; + } + atoms.insert(rewritten); + } + } } void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses, @@ -263,13 +317,13 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses, } } -void LFSCCnfProof::printAtomMapping(const NodeSet& atoms, +void LFSCCnfProof::printAtomMapping(const std::set& atoms, std::ostream& os, std::ostream& paren) { - NodeSet::const_iterator it = atoms.begin(); - NodeSet::const_iterator end = atoms.end(); + std::set::const_iterator it = atoms.begin(); + std::set::const_iterator end = atoms.end(); - for (;it != end; ++it) { + for (;it != end; ++it) { os << "(decl_atom "; Node atom = *it; prop::SatVariable var = getLiteral(atom).getSatVariable(); @@ -277,8 +331,8 @@ void LFSCCnfProof::printAtomMapping(const NodeSet& atoms, LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); pe->printLetTerm(atom.toExpr(), os); - os << " (\\ " << ProofManager::getVarName(var, d_name) - << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; + os << " (\\ " << ProofManager::getVarName(var, d_name); + os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; paren << ")))"; } } @@ -304,6 +358,9 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, const prop::SatClause* clause, std::ostream& os, std::ostream& paren) { + Debug("cnf-pf") << std::endl << std::endl << "LFSCCnfProof::printCnfProofForClause( " << id << " ) starting " + << std::endl; + os << "(satlem _ _ "; std::ostringstream clause_paren; printClause(*clause, os, clause_paren); @@ -336,6 +393,10 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, // and prints the proof of the top-level formula bool is_input = printProofTopLevel(base_assertion, os_base); + if (is_input) { + Debug("cnf-pf") << std::endl << "; base assertion is input. proof: " << os_base.str() << std::endl; + } + //get base assertion with polarity bool base_pol = base_assertion.getKind()!=kind::NOT; base_assertion = base_assertion.getKind()==kind::NOT ? base_assertion[0] : base_assertion; @@ -564,6 +625,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, if( !pols[0] || num_nots_1==1 ){ os_base_n << "(not_not_intro _ " << ProofManager::getLitName(lit1, d_name) << ") "; }else{ + Trace("cnf-pf-debug") << "CALLING getlitname" << std::endl; os_base_n << ProofManager::getLitName(lit1, d_name) << " "; } Assert( elimNum!=0 ); @@ -662,6 +724,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, os << ")" << clause_paren.str() << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n"; + paren << "))"; } diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index a21cb1c0e..62036ced0 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -27,6 +27,7 @@ #include "context/cdhashmap.h" #include "proof/clause_id.h" +#include "proof/lemma_proof.h" #include "proof/sat_proof.h" #include "util/proof.h" @@ -43,7 +44,9 @@ typedef __gnu_cxx::hash_set ClauseIdSet; typedef context::CDHashMap ClauseIdToNode; typedef context::CDHashMap NodeToProofRule; -typedef context::CDHashMap ClauseIdToTheory; +typedef std::map, LemmaProofRecipe> LemmaToRecipe; +typedef std::pair NodePair; +typedef std::set NodePairSet; class CnfProof { protected: @@ -55,11 +58,8 @@ protected: /** Map from assertion to reason for adding assertion **/ NodeToProofRule d_assertionToProofRule; - /** Map from assertion to the theory that added this assertion **/ - ClauseIdToTheory d_clauseIdToOwnerTheory; - - /** The last theory to explain a lemma **/ - theory::TheoryId d_explainerTheory; + /** Map from lemma to the recipe for proving it **/ + LemmaToRecipe d_lemmaToProofRecipe; /** Top of stack is assertion currently being converted to CNF **/ std::vector d_currentAssertionStack; @@ -91,10 +91,16 @@ public: Node getAtom(prop::SatVariable var); prop::SatLiteral getLiteral(TNode node); + bool hasLiteral(TNode node); + void ensureLiteral(TNode node, bool noPreregistration = false); + void collectAtoms(const prop::SatClause* clause, - NodeSet& atoms); + std::set& atoms); void collectAtomsForClauses(const IdToSatClause& clauses, - NodeSet& atoms); + std::set& atoms); + void collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses, + std::set& atoms, + NodePairSet& rewrites); void collectAssertionsForClauses(const IdToSatClause& clauses, NodeSet& assertions); @@ -121,11 +127,9 @@ public: void popCurrentDefinition(); Node getCurrentDefinition(); - void setExplainerTheory(theory::TheoryId theory); - theory::TheoryId getExplainerTheory(); - theory::TheoryId getOwnerTheory(ClauseId clause); - - void registerExplanationLemma(ClauseId clauseId); + void setProofRecipe(LemmaProofRecipe* proofRecipe); + LemmaProofRecipe getProofRecipe(const std::set &lemma); + bool haveProofRecipe(const std::set &lemma); // accessors for the leaf assertions that are being converted to CNF bool isAssertion(Node node); @@ -134,7 +138,7 @@ public: Node getAssertionForClause(ClauseId clause); /** Virtual methods for printing things **/ - virtual void printAtomMapping(const NodeSet& atoms, + virtual void printAtomMapping(const std::set& atoms, std::ostream& os, std::ostream& paren) = 0; @@ -161,7 +165,7 @@ public: {} ~LFSCCnfProof() {} - void printAtomMapping(const NodeSet& atoms, + void printAtomMapping(const std::set& atoms, std::ostream& os, std::ostream& paren); diff --git a/src/proof/lemma_proof.cpp b/src/proof/lemma_proof.cpp new file mode 100644 index 000000000..a12a516cf --- /dev/null +++ b/src/proof/lemma_proof.cpp @@ -0,0 +1,193 @@ +/********************* */ +/*! \file lemma_proof.h +** \verbatim +** +** \brief A class for recoding the steps required in order to prove a theory lemma. +** +** A class for recoding the steps required in order to prove a theory lemma. +** +**/ + +#include "proof/lemma_proof.h" +#include "theory/rewriter.h" + +namespace CVC4 { + +LemmaProofRecipe::ProofStep::ProofStep(theory::TheoryId theory, Node literalToProve) : + d_theory(theory), d_literalToProve(literalToProve) { +} + +theory::TheoryId LemmaProofRecipe::ProofStep::getTheory() const { + return d_theory; +} + +Node LemmaProofRecipe::ProofStep::getLiteral() const { + return d_literalToProve; +} + +void LemmaProofRecipe::ProofStep::addAssertion(const Node& assertion) { + d_assertions.insert(assertion); +} + +std::set LemmaProofRecipe::ProofStep::getAssertions() const { + return d_assertions; +} + +void LemmaProofRecipe::addStep(ProofStep& proofStep) { + std::list::iterator existingFirstStep = d_proofSteps.begin(); + d_proofSteps.push_front(proofStep); +} + +std::set LemmaProofRecipe::getMissingAssertionsForStep(unsigned index) const { + Assert(index < d_proofSteps.size()); + + std::set existingAssertions = getBaseAssertions(); + + std::list::const_iterator step = d_proofSteps.begin(); + while (index != 0) { + existingAssertions.insert(step->getLiteral().negate()); + ++step; + --index; + } + + std::set neededAssertions = step->getAssertions(); + + std::set result; + std::set_difference(neededAssertions.begin(), neededAssertions.end(), + existingAssertions.begin(), existingAssertions.end(), + std::inserter(result, result.begin())); + return result; +} + +void LemmaProofRecipe::dump(const char *tag) const { + + if (d_proofSteps.size() == 1) { + Debug(tag) << std::endl << "[Simple lemma]" << std::endl << std::endl; + } + + unsigned count = 1; + Debug(tag) << "Base assertions:" << std::endl; + for (std::set::iterator baseIt = d_baseAssertions.begin(); + baseIt != d_baseAssertions.end(); + ++baseIt) { + Debug(tag) << "\t#" << count << ": " << "\t" << *baseIt << std::endl; + ++count; + } + + Debug(tag) << std::endl << std::endl << "Proof steps:" << std::endl; + + count = 1; + for (std::list::const_iterator step = d_proofSteps.begin(); step != d_proofSteps.end(); ++step) { + Debug(tag) << "\tStep #" << count << ": " << "\t[" << step->getTheory() << "] "; + if (step->getLiteral() == Node()) { + Debug(tag) << "Contradiction"; + } else { + Debug(tag) << step->getLiteral(); + } + + Debug(tag) << std::endl; + + std::set missingAssertions = getMissingAssertionsForStep(count - 1); + for (std::set::const_iterator it = missingAssertions.begin(); it != missingAssertions.end(); ++it) { + Debug(tag) << "\t\t\tMissing assertion for step: " << *it << std::endl; + } + + Debug(tag) << std::endl; + ++count; + } + + if (!d_assertionToExplanation.empty()) { + Debug(tag) << std::endl << "Rewrites used:" << std::endl; + count = 1; + for (std::map::const_iterator rewrite = d_assertionToExplanation.begin(); + rewrite != d_assertionToExplanation.end(); + ++rewrite) { + Debug(tag) << "\tRewrite #" << count << ":" << std::endl + << "\t\t" << rewrite->first + << std::endl << "\t\trewritten into" << std::endl + << "\t\t" << rewrite->second + << std::endl << std::endl; + ++count; + } + } +} + +void LemmaProofRecipe::addBaseAssertion(Node baseAssertion) { + d_baseAssertions.insert(baseAssertion); +} + +std::set LemmaProofRecipe::getBaseAssertions() const { + return d_baseAssertions; +} + +theory::TheoryId LemmaProofRecipe::getTheory() const { + Assert(d_proofSteps.size() > 0); + return d_proofSteps.back().getTheory(); +} + +void LemmaProofRecipe::addRewriteRule(Node assertion, Node explanation) { + if (d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end()) { + Assert(d_assertionToExplanation[assertion] == explanation); + } + + d_assertionToExplanation[assertion] = explanation; +} + +bool LemmaProofRecipe::wasRewritten(Node assertion) const { + return d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end(); +} + +Node LemmaProofRecipe::getExplanation(Node assertion) const { + Assert(d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end()); + return d_assertionToExplanation.find(assertion)->second; +} + +LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteBegin() const { + return d_assertionToExplanation.begin(); +} + +LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteEnd() const { + return d_assertionToExplanation.end(); +} + +bool LemmaProofRecipe::operator<(const LemmaProofRecipe& other) const { + return d_baseAssertions < other.d_baseAssertions; + } + +bool LemmaProofRecipe::simpleLemma() const { + return d_proofSteps.size() == 1; +} + +bool LemmaProofRecipe::compositeLemma() const { + return !simpleLemma(); +} + +const LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) const { + Assert(index < d_proofSteps.size()); + + std::list::const_iterator it = d_proofSteps.begin(); + while (index != 0) { + ++it; + --index; + } + + return &(*it); +} + +LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) { + Assert(index < d_proofSteps.size()); + + std::list::iterator it = d_proofSteps.begin(); + while (index != 0) { + ++it; + --index; + } + + return &(*it); +} + +unsigned LemmaProofRecipe::getNumSteps() const { + return d_proofSteps.size(); +} + +} /* namespace CVC4 */ diff --git a/src/proof/lemma_proof.h b/src/proof/lemma_proof.h new file mode 100644 index 000000000..e96ff5337 --- /dev/null +++ b/src/proof/lemma_proof.h @@ -0,0 +1,79 @@ +/********************* */ +/*! \file lemma_proof.h +** \verbatim +** +** \brief A class for recoding the steps required in order to prove a theory lemma. +** +** A class for recoding the steps required in order to prove a theory lemma. +** +**/ + +#include "cvc4_private.h" + +#ifndef __CVC4__LEMMA_PROOF_H +#define __CVC4__LEMMA_PROOF_H + +#include "expr/expr.h" +#include "proof/clause_id.h" +#include "prop/sat_solver_types.h" +#include "util/proof.h" +#include "expr/node.h" + +namespace CVC4 { + +class LemmaProofRecipe { +public: + class ProofStep { + public: + ProofStep(theory::TheoryId theory, Node literalToProve); + theory::TheoryId getTheory() const; + Node getLiteral() const; + void addAssertion(const Node& assertion); + std::set getAssertions() const; + + private: + theory::TheoryId d_theory; + Node d_literalToProve; + std::set d_assertions; + }; + + //* The lemma assertions and owner */ + void addBaseAssertion(Node baseAssertion); + std::set getBaseAssertions() const; + theory::TheoryId getTheory() const; + + //* Rewrite rules */ + typedef std::map::const_iterator RewriteIterator; + RewriteIterator rewriteBegin() const; + RewriteIterator rewriteEnd() const; + + void addRewriteRule(Node assertion, Node explanation); + bool wasRewritten(Node assertion) const; + Node getExplanation(Node assertion) const; + + //* Proof Steps */ + void addStep(ProofStep& proofStep); + const ProofStep* getStep(unsigned index) const; + ProofStep* getStep(unsigned index); + unsigned getNumSteps() const; + std::set getMissingAssertionsForStep(unsigned index) const; + bool simpleLemma() const; + bool compositeLemma() const; + + void dump(const char *tag) const; + bool operator<(const LemmaProofRecipe& other) const; + +private: + //* The list of assertions for this lemma */ + std::set d_baseAssertions; + + //* The various steps needed to derive the empty clause */ + std::list d_proofSteps; + + //* A map from assertions to their rewritten explanations (toAssert --> toExplain) */ + std::map d_assertionToExplanation; +}; + +} /* CVC4 namespace */ + +#endif /* __CVC4__LEMMA_PROOF_H */ diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index a3689d746..5ce8b523f 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -200,7 +200,6 @@ std::string ProofManager::getLitName(prop::SatLiteral lit, return append(prefix+".l", lit.toInt()); } - std::string ProofManager::getPreprocessedAssertionName(Node node, const std::string& prefix) { node = node.getKind() == kind::BITVECTOR_EAGER_ATOM ? node[0] : node; @@ -217,9 +216,15 @@ std::string ProofManager::getAtomName(TNode atom, Assert(!lit.isNegated()); return getAtomName(lit.getSatVariable(), prefix); } + std::string ProofManager::getLitName(TNode lit, const std::string& prefix) { - return getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix); + std::string litName = getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix); + if (currentPM()->d_rewriteFilters.find(litName) != currentPM()->d_rewriteFilters.end()) { + return currentPM()->d_rewriteFilters[litName]; + } + + return litName; } std::string ProofManager::sanitize(TNode node) { @@ -331,6 +336,9 @@ LFSCProof::LFSCProof(SmtEngine* smtEngine, {} void LFSCProof::toStream(std::ostream& out) { + + Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER); + d_satProof->constructProof(); // collecting leaf clauses in resolution proof @@ -384,8 +392,37 @@ void LFSCProof::toStream(std::ostream& out) { for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3) Debug("pf::pm") << "\t assertion = " << *it3 << std::endl; - NodeSet atoms; + std::set atoms; + NodePairSet rewrites; // collects the atoms in the clauses + d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites); + + if (!rewrites.empty()) { + Debug("pf::pm") << std::endl << "Rewrites used in lemmas: " << std::endl; + NodePairSet::const_iterator rewriteIt; + for (rewriteIt = rewrites.begin(); rewriteIt != rewrites.end(); ++rewriteIt) { + Debug("pf::pm") << "\t" << rewriteIt->first << " --> " << rewriteIt->second << std::endl; + } + Debug("pf::pm") << std::endl << "Rewrite printing done" << std::endl; + } else { + Debug("pf::pm") << "No rewrites in lemmas found" << std::endl; + } + + // The derived/unrewritten atoms may not have CNF literals required later on. + // If they don't, add them. + std::set::const_iterator it; + for (it = atoms.begin(); it != atoms.end(); ++it) { + Debug("pf::pm") << "Ensure literal for atom: " << *it << std::endl; + if (!d_cnfProof->hasLiteral(*it)) { + // For arithmetic: these literals are not normalized, causing an error in Arith. + if (theory::Theory::theoryOf(*it) == theory::THEORY_ARITH) { + d_cnfProof->ensureLiteral(*it, true); // This disables preregistration with the theory solver. + } else { + d_cnfProof->ensureLiteral(*it); // Normal method, with theory solver preregisteration. + } + } + } + d_cnfProof->collectAtomsForClauses(used_inputs, atoms); d_cnfProof->collectAtomsForClauses(used_lemmas, atoms); @@ -393,38 +430,23 @@ void LFSCProof::toStream(std::ostream& out) { for (NodeSet::const_iterator it = used_assertions.begin(); it != used_assertions.end(); ++it) { utils::collectAtoms(*it, atoms); + // utils::collectAtoms(*it, newAtoms); } - NodeSet::iterator atomIt; - Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: " << std::endl << std::endl; + std::set::iterator atomIt; + Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: " + << std::endl << std::endl; for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) { Debug("pf::pm") << "\tAtom: " << *atomIt << std::endl; - - if (Debug.isOn("proof:pm")) { - // std::cout << NodeManager::currentNM(); - Debug("proof:pm") << "LFSCProof::Used assertions: "<< std::endl; - for(NodeSet::const_iterator it = used_assertions.begin(); it != used_assertions.end(); ++it) { - Debug("proof:pm") << " " << *it << std::endl; - } - - Debug("proof:pm") << "LFSCProof::Used atoms: "<< std::endl; - for(NodeSet::const_iterator it = atoms.begin(); it != atoms.end(); ++it) { - Debug("proof:pm") << " " << *it << std::endl; - } - } } - smt::SmtScope scope(d_smtEngine); std::ostringstream paren; out << "(check\n"; out << " ;; Declarations\n"; // declare the theory atoms - NodeSet::const_iterator it = atoms.begin(); - NodeSet::const_iterator end = atoms.end(); - Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl; - for(; it != end; ++it) { + for(it = atoms.begin(); it != atoms.end(); ++it) { Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl; d_theoryProof->registerTerm((*it).toExpr()); } @@ -444,9 +466,15 @@ void LFSCProof::toStream(std::ostream& out) { out << "(: (holds cln)\n\n"; // Have the theory proofs print deferred declarations, e.g. for skolem variables. - out << " ;; Printing deferred declarations \n"; + out << " ;; Printing deferred declarations \n\n"; d_theoryProof->printDeferredDeclarations(out, paren); + out << " ;; Printing aliasing declarations \n\n"; + d_theoryProof->printAliasingDeclarations(out, paren); + + out << " ;; Rewrites for Lemmas \n"; + d_theoryProof->printLemmaRewrites(rewrites, out, paren); + // print trust that input assertions are their preprocessed form printPreprocessedAssertions(used_assertions, out, paren); @@ -464,10 +492,6 @@ void LFSCProof::toStream(std::ostream& out) { Debug("pf::pm") << std::endl << "Printing cnf proof for clauses DONE" << std::endl; - // FIXME: for now assume all theory lemmas are in CNF form so - // distinguish between them and inputs - // print theory lemmas for resolution proof - Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl; d_theoryProof->printTheoryLemmas(used_lemmas, out, paren); Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl; @@ -496,6 +520,8 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, NodeSet::const_iterator it = assertions.begin(); NodeSet::const_iterator end = assertions.end(); + Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions starting" << std::endl; + for (; it != end; ++it) { os << "(th_let_pf _ "; @@ -506,7 +532,6 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; paren << "))"; - } os << "\n"; @@ -568,6 +593,14 @@ void ProofManager::markPrinted(const Type& type) { d_printedTypes.insert(type); } +void ProofManager::addRewriteFilter(const std::string &original, const std::string &substitute) { + d_rewriteFilters[original] = substitute; +} + +void ProofManager::clearRewriteFilters() { + d_rewriteFilters.clear(); +} + std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) { switch(k) { case RULE_GIVEN: diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index c74aac237..c6454b652 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -34,6 +34,8 @@ namespace CVC4 { +class SmtGlobals; + // forward declarations namespace Minisat { class Solver; @@ -136,6 +138,8 @@ class ProofManager { std::set d_printedTypes; + std::map d_rewriteFilters; + protected: LogicInfo d_logic; @@ -224,6 +228,9 @@ public: void markPrinted(const Type& type); bool wasPrinted(const Type& type) const; + void addRewriteFilter(const std::string &original, const std::string &substitute); + void clearRewriteFilters(); + };/* class ProofManager */ class LFSCProof : public Proof { diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp new file mode 100644 index 000000000..6d729db1f --- /dev/null +++ b/src/proof/proof_output_channel.cpp @@ -0,0 +1,82 @@ +/********************* */ +/*! \file proof_output_channel.cpp +** \verbatim +** \brief [[ Add one-line brief description here ]] +** +** [[ Add lengthier description here ]] +** \todo document this file +**/ + +#include "base/cvc4_assert.h" +#include "proof_output_channel.h" +#include "theory/term_registration_visitor.h" +#include "theory/valuation.h" + +namespace CVC4 { + +ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(NULL) {} + +void ProofOutputChannel::conflict(TNode n, Proof* pf) throw() { + Trace("pf::tp") << "ProofOutputChannel: CONFLICT: " << n << std::endl; + Assert(d_conflict.isNull()); + Assert(!n.isNull()); + d_conflict = n; + Assert(pf != NULL); + d_proof = pf; +} + +bool ProofOutputChannel::propagate(TNode x) throw() { + Trace("pf::tp") << "ProofOutputChannel: got a propagation: " << x << std::endl; + d_propagations.insert(x); + return true; +} + +theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool, bool, bool) throw() { + Trace("pf::tp") << "ProofOutputChannel: new lemma: " << n << std::endl; + d_lemma = n; + return theory::LemmaStatus(TNode::null(), 0); +} + +theory::LemmaStatus ProofOutputChannel::splitLemma(TNode, bool) throw() { + AlwaysAssert(false); + return theory::LemmaStatus(TNode::null(), 0); +} + +void ProofOutputChannel::requirePhase(TNode n, bool b) throw() { + Debug("pf::tp") << "ProofOutputChannel::requirePhase called" << std::endl; + Trace("pf::tp") << "requirePhase " << n << " " << b << std::endl; +} + +bool ProofOutputChannel::flipDecision() throw() { + Debug("pf::tp") << "ProofOutputChannel::flipDecision called" << std::endl; + AlwaysAssert(false); + return false; +} + +void ProofOutputChannel::setIncomplete() throw() { + Debug("pf::tp") << "ProofOutputChannel::setIncomplete called" << std::endl; + AlwaysAssert(false); +} + + +MyPreRegisterVisitor::MyPreRegisterVisitor(theory::Theory* theory) + : d_theory(theory) + , d_visited() { +} + +bool MyPreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { + return d_visited.find(current) != d_visited.end(); +} + +void MyPreRegisterVisitor::visit(TNode current, TNode parent) { + d_theory->preRegisterTerm(current); + d_visited.insert(current); +} + +void MyPreRegisterVisitor::start(TNode node) { +} + +void MyPreRegisterVisitor::done(TNode node) { +} + +} /* namespace CVC4 */ diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h new file mode 100644 index 000000000..b85af5fb5 --- /dev/null +++ b/src/proof/proof_output_channel.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \file proof_output_channel.h + ** \verbatim + ** + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H +#define __CVC4__PROOF_OUTPUT_CHANNEL_H + +#include "theory/output_channel.h" + +namespace CVC4 { + +class ProofOutputChannel : public theory::OutputChannel { +public: + Node d_conflict; + Proof* d_proof; + Node d_lemma; + std::set d_propagations; + + ProofOutputChannel(); + + virtual ~ProofOutputChannel() throw() {} + + void conflict(TNode n, Proof* pf) throw(); + bool propagate(TNode x) throw(); + theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) throw(); + theory::LemmaStatus splitLemma(TNode, bool) throw(); + void requirePhase(TNode n, bool b) throw(); + bool flipDecision() throw(); + void setIncomplete() throw(); +};/* class ProofOutputChannel */ + +class MyPreRegisterVisitor { + theory::Theory* d_theory; + __gnu_cxx::hash_set d_visited; +public: + typedef void return_type; + MyPreRegisterVisitor(theory::Theory* theory); + bool alreadyVisited(TNode current, TNode parent); + void visit(TNode current, TNode parent); + void start(TNode node); + void done(TNode node); +}; /* class MyPreRegisterVisitor */ + +} /* CVC4 namespace */ + +#endif /* __CVC4__PROOF_OUTPUT_CHANNEL_H */ diff --git a/src/proof/proof_utils.cpp b/src/proof/proof_utils.cpp index 5b04c281d..fe0d42242 100644 --- a/src/proof/proof_utils.cpp +++ b/src/proof/proof_utils.cpp @@ -21,14 +21,14 @@ namespace CVC4 { namespace utils { -void collectAtoms(TNode node, CVC4::NodeSet& seen) { +void collectAtoms(TNode node, std::set& seen) { if (seen.find(node) != seen.end()) return; if (theory::Theory::theoryOf(node) != theory::THEORY_BOOL || node.isVar()) { seen.insert(node); return; } - + for (unsigned i = 0; i < node.getNumChildren(); ++i) { collectAtoms(node[i], seen); } @@ -47,23 +47,23 @@ std::string toLFSCKind(Kind kind) { // bit-vector kinds case kind::BITVECTOR_AND : - return "bvand"; + return "bvand"; case kind::BITVECTOR_OR : - return "bvor"; + return "bvor"; case kind::BITVECTOR_XOR : - return "bvxor"; + return "bvxor"; case kind::BITVECTOR_NAND : - return "bvnand"; + return "bvnand"; case kind::BITVECTOR_NOR : - return "bvnor"; + return "bvnor"; case kind::BITVECTOR_XNOR : - return "bvxnor"; + return "bvxnor"; case kind::BITVECTOR_COMP : - return "bvcomp"; + return "bvcomp"; case kind::BITVECTOR_MULT : return "bvmul"; case kind::BITVECTOR_PLUS : - return "bvadd"; + return "bvadd"; case kind::BITVECTOR_SUB : return "bvsub"; case kind::BITVECTOR_UDIV : @@ -71,49 +71,49 @@ std::string toLFSCKind(Kind kind) { return "bvudiv"; case kind::BITVECTOR_UREM : case kind::BITVECTOR_UREM_TOTAL : - return "bvurem"; + return "bvurem"; case kind::BITVECTOR_SDIV : - return "bvsdiv"; + return "bvsdiv"; case kind::BITVECTOR_SREM : return "bvsrem"; case kind::BITVECTOR_SMOD : - return "bvsmod"; + return "bvsmod"; case kind::BITVECTOR_SHL : - return "bvshl"; + return "bvshl"; case kind::BITVECTOR_LSHR : return "bvlshr"; case kind::BITVECTOR_ASHR : return "bvashr"; case kind::BITVECTOR_CONCAT : - return "concat"; + return "concat"; case kind::BITVECTOR_NEG : - return "bvneg"; + return "bvneg"; case kind::BITVECTOR_NOT : - return "bvnot"; + return "bvnot"; case kind::BITVECTOR_ROTATE_LEFT : - return "rotate_left"; + return "rotate_left"; case kind::BITVECTOR_ROTATE_RIGHT : return "rotate_right"; case kind::BITVECTOR_ULT : - return "bvult"; + return "bvult"; case kind::BITVECTOR_ULE : - return "bvule"; + return "bvule"; case kind::BITVECTOR_UGT : return "bvugt"; case kind::BITVECTOR_UGE : return "bvuge"; case kind::BITVECTOR_SLT : - return "bvslt"; + return "bvslt"; case kind::BITVECTOR_SLE : - return "bvsle"; + return "bvsle"; case kind::BITVECTOR_SGT : - return "bvsgt"; + return "bvsgt"; case kind::BITVECTOR_SGE : - return "bvsge"; + return "bvsge"; case kind::BITVECTOR_EXTRACT : - return "extract"; + return "extract"; case kind::BITVECTOR_REPEAT : - return "repeat"; + return "repeat"; case kind::BITVECTOR_ZERO_EXTEND : return "zero_extend"; case kind::BITVECTOR_SIGN_EXTEND : diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h index da10c33a0..8c734c892 100644 --- a/src/proof/proof_utils.h +++ b/src/proof/proof_utils.h @@ -17,7 +17,7 @@ #include "cvc4_private.h" -#pragma once +#pragma once #include #include @@ -29,6 +29,9 @@ namespace CVC4 { typedef __gnu_cxx::hash_set ExprSet; typedef __gnu_cxx::hash_set NodeSet; +typedef std::pair NodePair; +typedef std::set NodePairSet; + namespace utils { std::string toLFSCKind(Kind kind); @@ -42,7 +45,7 @@ inline unsigned getExtractLow(Expr node) { } inline unsigned getSize(Type type) { - BitVectorType bv(type); + BitVectorType bv(type); return bv.getSize(); } @@ -60,8 +63,8 @@ inline Expr mkFalse() { return NodeManager::currentNM()->toExprManager()->mkConst(false); } inline BitVector mkBitVectorOnes(unsigned size) { - Assert(size > 0); - return BitVector(1, Integer(1)).signExtend(size - 1); + Assert(size > 0); + return BitVector(1, Integer(1)).signExtend(size - 1); } inline Expr mkExpr(Kind k , Expr expr) { @@ -73,16 +76,16 @@ inline Expr mkExpr(Kind k , Expr e1, Expr e2) { inline Expr mkExpr(Kind k , std::vector& children) { return NodeManager::currentNM()->toExprManager()->mkExpr(k, children); } - - + + inline Expr mkOnes(unsigned size) { - BitVector val = mkBitVectorOnes(size); - return NodeManager::currentNM()->toExprManager()->mkConst(val); + BitVector val = mkBitVectorOnes(size); + return NodeManager::currentNM()->toExprManager()->mkConst(val); } inline Expr mkConst(unsigned size, unsigned int value) { BitVector val(size, value); - return NodeManager::currentNM()->toExprManager()->mkConst(val); + return NodeManager::currentNM()->toExprManager()->mkConst(val); } inline Expr mkConst(const BitVector& value) { @@ -92,14 +95,14 @@ inline Expr mkConst(const BitVector& value) { inline Expr mkOr(const std::vector& nodes) { std::set all; all.insert(nodes.begin(), nodes.end()); - Assert(all.size() != 0 ); + Assert(all.size() != 0 ); if (all.size() == 1) { // All the same, or just one return nodes[0]; } - - + + NodeBuilder<> disjunction(kind::OR); std::set::const_iterator it = all.begin(); std::set::const_iterator it_end = all.end(); @@ -109,23 +112,23 @@ inline Expr mkOr(const std::vector& nodes) { } Node res = disjunction; - return res.toExpr(); + return res.toExpr(); }/* mkOr() */ - + inline Expr mkAnd(const std::vector& conjunctions) { std::set all; all.insert(conjunctions.begin(), conjunctions.end()); if (all.size() == 0) { - return mkTrue(); + return mkTrue(); } - + if (all.size() == 1) { // All the same, or just one return conjunctions[0]; } - + NodeBuilder<> conjunction(kind::AND); std::set::const_iterator it = all.begin(); @@ -135,7 +138,7 @@ inline Expr mkAnd(const std::vector& conjunctions) { ++ it; } - Node res = conjunction; + Node res = conjunction; return res.toExpr(); }/* mkAnd() */ @@ -144,14 +147,14 @@ inline Expr mkSortedExpr(Kind kind, const std::vector& children) { all.insert(children.begin(), children.end()); if (all.size() == 0) { - return mkTrue(); + return mkTrue(); } - + if (all.size() == 1) { // All the same, or just one return children[0]; } - + NodeBuilder<> res(kind); std::set::const_iterator it = all.begin(); @@ -165,13 +168,13 @@ inline Expr mkSortedExpr(Kind kind, const std::vector& children) { }/* mkSortedNode() */ inline const bool getBit(Expr expr, unsigned i) { - Assert (i < utils::getSize(expr) && - expr.isConst()); + Assert (i < utils::getSize(expr) && + expr.isConst()); Integer bit = expr.getConst().extract(i, i).getValue(); - return (bit == 1u); + return (bit == 1u); } -void collectAtoms(TNode node, NodeSet& seen); +void collectAtoms(TNode node, std::set& seen); } diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index 4f3330ef7..1e01e4dce 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -543,12 +543,9 @@ ClauseId TSatProof::registerClause(typename Solver::TCRef clause, if (kind == THEORY_LEMMA) { Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); d_lemmaClauses.insert(newId); - Debug("pf::sat") - << "TSatProof::registerClause registering a new lemma clause: " - << newId << " = " << *buildClause(newId) - << ". Explainer theory: " << d_cnfProof->getExplainerTheory() - << std::endl; - d_cnfProof->registerExplanationLemma(newId); + Debug("pf::sat") << "TSatProof::registerClause registering a new lemma clause: " + << newId << " = " << *buildClause(newId) + << std::endl; } } @@ -579,12 +576,10 @@ ClauseId TSatProof::registerUnitClause(typename Solver::TLit lit, } if (kind == THEORY_LEMMA) { Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); - Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new " - "lemma (UNIT CLAUSE): " - << lit << ". Explainer theory: " - << d_cnfProof->getExplainerTheory() << std::endl; + Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new lemma (UNIT CLAUSE): " + << lit + << std::endl; d_lemmaClauses.insert(newId); - d_cnfProof->registerExplanationLemma(newId); } } ClauseId id = d_unitId[toInt(lit)]; @@ -842,7 +837,7 @@ ClauseId TSatProof::resolveUnit(typename Solver::TLit lit) { // clause allocator. So reload reason ptr each time. const typename Solver::TClause& initial_reason = getClause(reason_ref); size_t current_reason_size = initial_reason.size(); - for (int i = 0; i < current_reason_size; i++) { + for (size_t i = 0; i < current_reason_size; i++) { const typename Solver::TClause& current_reason = getClause(reason_ref); current_reason_size = current_reason.size(); typename Solver::TLit l = current_reason[i]; @@ -904,7 +899,7 @@ void TSatProof::finalizeProof(typename Solver::TCRef conflict_ref) { // Here, the call to resolveUnit() can reallocate memory in the // clause allocator. So reload conflict ptr each time. size_t conflict_size = getClause(conflict_ref).size(); - for (int i = 0; i < conflict_size; ++i) { + for (size_t i = 0; i < conflict_size; ++i) { const typename Solver::TClause& conflict = getClause(conflict_ref); typename Solver::TLit lit = conflict[i]; ClauseId res_id = resolveUnit(~lit); @@ -1106,12 +1101,12 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, } if (id == this->d_emptyClauseId) { - out << "(\\empty empty)"; + out <<"(\\ empty empty)"; return; } - out << "(\\" << this->clauseName(id) << "\n"; // bind to lemma name - paren << "))"; // closing parethesis for lemma binding and satlem + out << "(\\ " << this->clauseName(id) << "\n"; // bind to lemma name + paren << "))"; // closing parethesis for lemma binding and satlem } /// LFSCSatProof class diff --git a/src/proof/skolemization_manager.h b/src/proof/skolemization_manager.h index de510e514..b026e21c2 100644 --- a/src/proof/skolemization_manager.h +++ b/src/proof/skolemization_manager.h @@ -37,7 +37,6 @@ public: Node getSkolem(Node disequality); Node getDisequality(Node skolem); bool isSkolem(Node skolem); - void clear(); std::hash_map::const_iterator begin(); diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 088275b3f..eaf21846b 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -25,6 +25,7 @@ #include "proof/clause_id.h" #include "proof/cnf_proof.h" #include "proof/proof_manager.h" +#include "proof/proof_output_channel.h" #include "proof/proof_utils.h" #include "proof/sat_proof.h" #include "proof/uf_proof.h" @@ -48,74 +49,6 @@ namespace CVC4 { unsigned CVC4::LetCount::counter = 0; static unsigned LET_COUNT = 1; -//for proof replay -class ProofOutputChannel : public theory::OutputChannel { -public: - Node d_conflict; - Proof* d_proof; - Node d_lemma; - - ProofOutputChannel() : d_conflict(), d_proof(NULL) {} - virtual ~ProofOutputChannel() throw() {} - - void conflict(TNode n, Proof* pf) throw() { - Trace("theory-proof-debug") << "; CONFLICT: " << n << std::endl; - Assert(d_conflict.isNull()); - Assert(!n.isNull()); - d_conflict = n; - Assert(pf != NULL); - d_proof = pf; - } - bool propagate(TNode x) throw() { - Trace("theory-proof-debug") << "got a propagation: " << x << std::endl; - return true; - } - theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) throw() { - Trace("theory-proof-debug") << "new lemma: " << n << std::endl; - d_lemma = n; - return theory::LemmaStatus(TNode::null(), 0); - } - theory::LemmaStatus splitLemma(TNode, bool) throw() { - AlwaysAssert(false); - return theory::LemmaStatus(TNode::null(), 0); - } - void requirePhase(TNode n, bool b) throw() { - Debug("theory-proof-debug") << "ProofOutputChannel::requirePhase called" << std::endl; - Trace("theory-proof-debug") << "requirePhase " << n << " " << b << std::endl; - } - bool flipDecision() throw() { - Debug("theory-proof-debug") << "ProofOutputChannel::flipDecision called" << std::endl; - AlwaysAssert(false); - return false; - } - void setIncomplete() throw() { - Debug("theory-proof-debug") << "ProofOutputChannel::setIncomplete called" << std::endl; - AlwaysAssert(false); - } -};/* class ProofOutputChannel */ - -//for proof replay -class MyPreRegisterVisitor { - theory::Theory* d_theory; - __gnu_cxx::hash_set d_visited; -public: - typedef void return_type; - MyPreRegisterVisitor(theory::Theory* theory) - : d_theory(theory) - , d_visited() - {} - bool alreadyVisited(TNode current, TNode parent) { return d_visited.find(current) != d_visited.end(); } - void visit(TNode current, TNode parent) { - if(theory::Theory::theoryOf(current) == d_theory->getId()) { - //Trace("theory-proof-debug") << "preregister " << current << std::endl; - d_theory->preRegisterTerm(current); - d_visited.insert(current); - } - } - void start(TNode node) { } - void done(TNode node) { } -}; /* class MyPreRegisterVisitor */ - TheoryProofEngine::TheoryProofEngine() : d_registrationCache() , d_theoryProofTable() @@ -131,13 +64,12 @@ TheoryProofEngine::~TheoryProofEngine() { } } - void TheoryProofEngine::registerTheory(theory::Theory* th) { - if( th ){ + if (th) { theory::TheoryId id = th->getId(); if(d_theoryProofTable.find(id) == d_theoryProofTable.end()) { - Trace("theory-proof-debug") << "; register theory " << id << std::endl; + Trace("pf::tp") << "TheoryProofEngine::registerTheory: " << id << std::endl; if (id == theory::THEORY_UF) { d_theoryProofTable[id] = new LFSCUFProof((theory::uf::TheoryUF*)th, this); @@ -167,19 +99,42 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { } TheoryProof* TheoryProofEngine::getTheoryProof(theory::TheoryId id) { + // The UF theory handles queries for the Builtin theory. + if (id == theory::THEORY_BUILTIN) { + Debug("pf::tp") << "TheoryProofEngine::getTheoryProof: BUILTIN --> UF" << std::endl; + id = theory::THEORY_UF; + } + Assert (d_theoryProofTable.find(id) != d_theoryProofTable.end()); return d_theoryProofTable[id]; } +void TheoryProofEngine::markTermForFutureRegistration(Expr term, theory::TheoryId id) { + d_exprToTheoryIds[term].insert(id); +} + +void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) { + LetMap emptyMap; + + os << "(trust_f (not (= _ "; + printBoundTerm(c1, os, emptyMap); + os << " "; + printBoundTerm(c2, os, emptyMap); + os << ")))"; +} + void TheoryProofEngine::registerTerm(Expr term) { + Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering term: " << term << std::endl; + if (d_registrationCache.count(term)) { return; } - Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering new term: " << term << std::endl; + + Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering NEW term: " << term << std::endl; theory::TheoryId theory_id = theory::Theory::theoryOf(term); - Debug("pf::tp") << "Term's theory: " << theory_id << std::endl; + Debug("pf::tp") << "Term's theory( " << term << " ) = " << theory_id << std::endl; // don't need to register boolean terms if (theory_id == theory::THEORY_BUILTIN || @@ -193,32 +148,38 @@ void TheoryProofEngine::registerTerm(Expr term) { if (!supportedTheory(theory_id)) return; + // Register the term with its owner theory getTheoryProof(theory_id)->registerTerm(term); + + // A special case: the array theory needs to know of every skolem, even if + // it belongs to another theory (e.g., a BV skolem) + if (ProofManager::getSkolemizationManager()->isSkolem(term) && theory_id != theory::THEORY_ARRAY) { + Debug("pf::tp") << "TheoryProofEngine::registerTerm: Special case: registering a non-array skolem: " << term << std::endl; + getTheoryProof(theory::THEORY_ARRAY)->registerTerm(term); + } + d_registrationCache.insert(term); } -theory::TheoryId TheoryProofEngine::getTheoryForLemma(ClauseId id) { +theory::TheoryId TheoryProofEngine::getTheoryForLemma(const prop::SatClause* clause) { ProofManager* pm = ProofManager::currentPM(); - Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma( " << id << " )" - << " = " << pm->getCnfProof()->getOwnerTheory(id) << std::endl; + std::set nodes; + for(unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = (*clause)[i]; + Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); + Expr atom = node.toExpr(); + if (atom.isConst()) { + Assert (atom == utils::mkTrue()); + continue; + } - if ((pm->getLogic() == "QF_UFLIA") || (pm->getLogic() == "QF_UFLRA")) { - Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma: special hack for Arithmetic-with-holes support. " - << "Returning THEORY_ARITH" << std::endl; - return theory::THEORY_ARITH; + nodes.insert(lit.isNegated() ? node.notNode() : node); } - return pm->getCnfProof()->getOwnerTheory(id); - - // if (pm->getLogic() == "QF_UF") return theory::THEORY_UF; - // if (pm->getLogic() == "QF_BV") return theory::THEORY_BV; - // if (pm->getLogic() == "QF_AX") return theory::THEORY_ARRAY; - // if (pm->getLogic() == "ALL_SUPPORTED") return theory::THEORY_BV; - - // Debug("pf::tp") << "Unsupported logic (" << pm->getLogic() << ")" << std::endl; - - // Unreachable(); + // Ensure that the lemma is in the database. + Assert (pm->getCnfProof()->haveProofRecipe(nodes)); + return pm->getCnfProof()->getProofRecipe(nodes).getTheory(); } void LFSCTheoryProofEngine::bind(Expr term, LetMap& map, Bindings& let_order) { @@ -272,8 +233,6 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) { void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const LetMap& map) { theory::TheoryId theory_id = theory::Theory::theoryOf(term); - Debug("pf::tp") << std::endl << "LFSCTheoryProofEngine::printTheoryTerm: term = " << term - << ", theory_id = " << theory_id << std::endl; // boolean terms and ITEs are special because they // are common to all theories @@ -315,6 +274,29 @@ void LFSCTheoryProofEngine::printSort(Type type, std::ostream& os) { Unreachable(); } +void LFSCTheoryProofEngine::performExtraRegistrations() { + ExprToTheoryIds::const_iterator it; + for (it = d_exprToTheoryIds.begin(); it != d_exprToTheoryIds.end(); ++it) { + if (d_registrationCache.count(it->first)) { // Only register if the term appeared + TheoryIdSet::const_iterator theoryIt; + for (theoryIt = it->second.begin(); theoryIt != it->second.end(); ++theoryIt) { + Debug("pf::tp") << "\tExtra registration of term " << it->first + << " with theory: " << *theoryIt << std::endl; + Assert(supportedTheory(*theoryIt)); + getTheoryProof(*theoryIt)->registerTerm(it->first); + } + } + } +} + +void LFSCTheoryProofEngine::treatBoolsAsFormulas(bool value) { + TheoryProofTable::const_iterator it = d_theoryProofTable.begin(); + TheoryProofTable::const_iterator end = d_theoryProofTable.end(); + for (; it != end; ++it) { + it->second->treatBoolsAsFormulas(value); + } +} + void LFSCTheoryProofEngine::registerTermsFromAssertions() { ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); @@ -322,6 +304,8 @@ void LFSCTheoryProofEngine::registerTermsFromAssertions() { for(; it != end; ++it) { registerTerm(*it); } + + performExtraRegistrations(); } void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) { @@ -333,17 +317,43 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare for (; it != end; ++it) { Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl; - // FIXME: merge this with counter - os << "(% A" << counter++ << " (th_holds "; + std::ostringstream name; + name << "A" << counter++; + os << "(% " << name.str() << " (th_holds "; printLetTerm(*it, os); os << ")\n"; paren << ")"; } - //store map between assertion and counter - // ProofManager::currentPM()->setAssertion( *it ); + Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions done" << std::endl << std::endl; } +void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites called" << std::endl << std::endl; + + NodePairSet::const_iterator it; + + for (it = rewrites.begin(); it != rewrites.end(); ++it) { + Debug("pf::tp") << "printLemmaRewrites: " << it->first << " --> " << it->second << std::endl; + + std::ostringstream rewriteRule; + rewriteRule << ".lrr" << d_assertionToRewrite.size(); + + LetMap emptyMap; + os << "(th_let_pf _ (trust_f (iff "; + printBoundTerm(it->second.toExpr(), os, emptyMap); + os << " "; + printBoundTerm(it->first.toExpr(), os, emptyMap); + os << ")) (\\ " << rewriteRule.str() << "\n"; + + d_assertionToRewrite[it->first] = rewriteRule.str(); + Debug("pf::tp") << "d_assertionToRewrite[" << it->first << "] = " << rewriteRule.str() << std::endl; + paren << "))"; + } + + Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites done" << std::endl << std::endl; +} + void LFSCTheoryProofEngine::printSortDeclarations(std::ostream& os, std::ostream& paren) { Debug("pf::tp") << "LFSCTheoryProofEngine::printSortDeclarations called" << std::endl << std::endl; @@ -378,55 +388,148 @@ void LFSCTheoryProofEngine::printDeferredDeclarations(std::ostream& os, std::ost } } -void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, - std::ostream& os, - std::ostream& paren) { - os << " ;; Theory Lemmas \n"; - ProofManager* pm = ProofManager::currentPM(); - IdToSatClause::const_iterator it = lemmas.begin(); - IdToSatClause::const_iterator end = lemmas.end(); - - Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: checking lemma owners..." << std::endl; +void LFSCTheoryProofEngine::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printAliasingDeclarations called" << std::endl; + TheoryProofTable::const_iterator it = d_theoryProofTable.begin(); + TheoryProofTable::const_iterator end = d_theoryProofTable.end(); for (; it != end; ++it) { - Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: new lemma" << std::endl; - ClauseId id = it->first; - Debug("pf::tp") << "\tLemma = " << id - << ". Owner theory: " << pm->getCnfProof()->getOwnerTheory(id) << std::endl; + it->second->printAliasingDeclarations(os, paren); } - it = lemmas.begin(); +} - // BitVector theory is special case: must know all - // conflicts needed ahead of time for resolution - // proof lemmas - std::vector bv_lemmas; - for (; it != end; ++it) { +void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause& lemmas) { + Debug("pf::dumpLemmas") << "Dumping ALL theory lemmas" << std::endl << std::endl; + + ProofManager* pm = ProofManager::currentPM(); + for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) { ClauseId id = it->first; + Debug("pf::dumpLemmas") << "**** \tLemma ID = " << id << std::endl; const prop::SatClause* clause = it->second; + std::set nodes; + for(unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = (*clause)[i]; + Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); + if (node.isConst()) { + Assert (node.toExpr() == utils::mkTrue()); + continue; + } + nodes.insert(lit.isNegated() ? node.notNode() : node); + } + + LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(nodes); + recipe.dump("pf::dumpLemmas"); + } - theory::TheoryId theory_id = getTheoryForLemma(id); - if (theory_id != theory::THEORY_BV) continue; + Debug("pf::dumpLemmas") << "Theory lemma printing DONE" << std::endl << std::endl; +} + +// TODO: this function should be moved into the BV prover. +void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren) { + // BitVector theory is special case: must know all conflicts needed + // ahead of time for resolution proof lemmas + std::vector bv_lemmas; + + for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) { + const prop::SatClause* clause = it->second; std::vector conflict; + std::set conflictNodes; for(unsigned i = 0; i < clause->size(); ++i) { prop::SatLiteral lit = (*clause)[i]; - Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr(); + Node node = ProofManager::currentPM()->getCnfProof()->getAtom(lit.getSatVariable()); + Expr atom = node.toExpr(); + + // The literals (true) and (not false) are omitted from conflicts if (atom.isConst()) { Assert (atom == utils::mkTrue() || (atom == utils::mkFalse() && lit.isNegated())); continue; } + Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom; conflict.push_back(expr_lit); + conflictNodes.insert(lit.isNegated() ? node.notNode() : node); + } + + LemmaProofRecipe recipe = ProofManager::currentPM()->getCnfProof()->getProofRecipe(conflictNodes); + + unsigned numberOfSteps = recipe.getNumSteps(); + + prop::SatClause currentClause = *clause; + std::vector currentClauseExpr = conflict; + + for (unsigned i = 0; i < numberOfSteps; ++i) { + const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i); + + if (currentStep->getTheory() != theory::THEORY_BV) { + continue; + } + + // If any rewrites took place, we need to update the conflict clause accordingly + std::set missingAssertions = recipe.getMissingAssertionsForStep(i); + std::map explanationToMissingAssertion; + std::set::iterator assertionIt; + for (assertionIt = missingAssertions.begin(); + assertionIt != missingAssertions.end(); + ++assertionIt) { + Node negated = (*assertionIt).negate(); + explanationToMissingAssertion[recipe.getExplanation(negated)] = negated; + } + + currentClause = *clause; + currentClauseExpr = conflict; + + for (unsigned j = 0; j < i; ++j) { + // Literals already used in previous steps need to be negated + Node previousLiteralNode = recipe.getStep(j)->getLiteral(); + + // If this literal is the result of a rewrite, we need to translate it + if (explanationToMissingAssertion.find(previousLiteralNode) != + explanationToMissingAssertion.end()) { + previousLiteralNode = explanationToMissingAssertion[previousLiteralNode]; + } + + Node previousLiteralNodeNegated = previousLiteralNode.negate(); + prop::SatLiteral previousLiteralNegated = + ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated); + + currentClause.push_back(previousLiteralNegated); + currentClauseExpr.push_back(previousLiteralNodeNegated.toExpr()); + } + + // If we're in the final step, the last literal is Null and should not be added. + // Otherwise, the current literal does NOT need to be negated + Node currentLiteralNode = currentStep->getLiteral(); + + if (currentLiteralNode != Node()) { + prop::SatLiteral currentLiteral = + ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode); + + currentClause.push_back(currentLiteral); + currentClauseExpr.push_back(currentLiteralNode.toExpr()); + } + + bv_lemmas.push_back(utils::mkSortedExpr(kind::OR, currentClauseExpr)); } - bv_lemmas.push_back(utils::mkSortedExpr(kind::OR, conflict)); } - // FIXME: ugly, move into bit-vector proof by adding lemma - // queue inside each theory_proof + BitVectorProof* bv = ProofManager::getBitVectorProof(); bv->finalizeConflicts(bv_lemmas); - bv->printResolutionProof(os, paren); +} + +void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, + std::ostream& os, + std::ostream& paren) { + os << " ;; Theory Lemmas \n"; + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: starting" << std::endl; + + if (Debug.isOn("pf::dumpLemmas")) { + dumpTheoryLemmas(lemmas); + } + + finalizeBvConflicts(lemmas, os, paren); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { Assert (lemmas.size() == 1); @@ -434,54 +537,247 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, return; } - it = lemmas.begin(); - + ProofManager* pm = ProofManager::currentPM(); Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemmas..." << std::endl; - for (; it != end; ++it) { - Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing a new lemma!" << std::endl; - - // Debug("pf::tp") << "\tLemma = " << it->first << ", " << *(it->second) << std::endl; + for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) { ClauseId id = it->first; - Debug("pf::tp") << "Owner theory:" << pm->getCnfProof()->getOwnerTheory(id) << std::endl; const prop::SatClause* clause = it->second; - // printing clause as it appears in resolution proof - os << "(satlem _ _ "; - std::ostringstream clause_paren; - Debug("pf::tp") << "CnfProof printing clause..." << std::endl; - pm->getCnfProof()->printClause(*clause, os, clause_paren); - Debug("pf::tp") << "CnfProof printing clause - Done!" << std::endl; + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemma. ID = " + << id << std::endl; std::vector clause_expr; + std::set clause_expr_nodes; for(unsigned i = 0; i < clause->size(); ++i) { prop::SatLiteral lit = (*clause)[i]; - Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr(); + Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); + Expr atom = node.toExpr(); if (atom.isConst()) { Assert (atom == utils::mkTrue()); continue; } Expr expr_lit = lit.isNegated() ? atom.notExpr(): atom; clause_expr.push_back(expr_lit); + clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node); } - Debug("pf::tp") << "Expression printing done!" << std::endl; - - // query appropriate theory for proof of clause - theory::TheoryId theory_id = getTheoryForLemma(id); - Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl; - Debug("theory-proof-debug") << ";; Get theory lemma from " << theory_id << "..." << std::endl; - getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren); - Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl; - // os << " (clausify_false trust)"; - os << clause_paren.str(); - os << "( \\ " << pm->getLemmaClauseName(id) <<"\n"; - paren << "))"; + LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(clause_expr_nodes); + + if (recipe.simpleLemma()) { + // In a simple lemma, there will be no propositional resolution in the end + + Debug("pf::tp") << "Simple lemma" << std::endl; + // Printing the clause as it appears in resolution proof + os << "(satlem _ _ "; + std::ostringstream clause_paren; + pm->getCnfProof()->printClause(*clause, os, clause_paren); + + // Find and handle missing assertions, due to rewrites + std::set missingAssertions = recipe.getMissingAssertionsForStep(0); + if (!missingAssertions.empty()) { + Debug("pf::tp") << "Have missing assertions for this simple lemma!" << std::endl; + } + + std::set::const_iterator missingAssertion; + for (missingAssertion = missingAssertions.begin(); + missingAssertion != missingAssertions.end(); + ++missingAssertion) { + + Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion << std::endl; + Assert(recipe.wasRewritten(missingAssertion->negate())); + Node explanation = recipe.getExplanation(missingAssertion->negate()).negate(); + Debug("pf::tp") << "Found explanation: " << explanation << std::endl; + + // We have a missing assertion. + // rewriteIt->first is the assertion after the rewrite (the explanation), + // rewriteIt->second is the original assertion that needs to be fed into the theory. + + bool found = false; + unsigned k; + for (k = 0; k < clause_expr.size(); ++k) { + if (clause_expr[k] == explanation.toExpr()) { + found = true; + break; + } + } + + Assert(found); + Debug("pf::tp") << "Replacing theory assertion " + << clause_expr[k] + << " with " + << *missingAssertion + << std::endl; + + clause_expr[k] = missingAssertion->toExpr(); + + std::ostringstream rewritten; + rewritten << "(or_elim_1 _ _ "; + rewritten << "(not_not_intro _ "; + rewritten << pm->getLitName(explanation); + rewritten << ") (iff_elim_1 _ _ "; + rewritten << d_assertionToRewrite[missingAssertion->negate()]; + rewritten << "))"; + + Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl + << pm->getLitName(*missingAssertion) << " --> " << rewritten.str() + << std::endl << std::endl; + + pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str()); + } + + // Query the appropriate theory for a proof of this clause + theory::TheoryId theory_id = getTheoryForLemma(clause); + Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl; + getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren); + + // Turn rewrite filter OFF + pm->clearRewriteFilters(); + + Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl; + os << clause_paren.str(); + os << "( \\ " << pm->getLemmaClauseName(id) <<"\n"; + paren << "))"; + } else { // This is a composite lemma + + unsigned numberOfSteps = recipe.getNumSteps(); + prop::SatClause currentClause = *clause; + std::vector currentClauseExpr = clause_expr; + + for (unsigned i = 0; i < numberOfSteps; ++i) { + const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i); + + currentClause = *clause; + currentClauseExpr = clause_expr; + + for (unsigned j = 0; j < i; ++j) { + // Literals already used in previous steps need to be negated + Node previousLiteralNode = recipe.getStep(j)->getLiteral(); + Node previousLiteralNodeNegated = previousLiteralNode.negate(); + prop::SatLiteral previousLiteralNegated = + ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated); + currentClause.push_back(previousLiteralNegated); + currentClauseExpr.push_back(previousLiteralNodeNegated.toExpr()); + } + + // If the current literal is NULL, can ignore (final step) + // Otherwise, the current literal does NOT need to be negated + Node currentLiteralNode = currentStep->getLiteral(); + if (currentLiteralNode != Node()) { + prop::SatLiteral currentLiteral = + ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode); + + currentClause.push_back(currentLiteral); + currentClauseExpr.push_back(currentLiteralNode.toExpr()); + } + + os << "(satlem _ _ "; + std::ostringstream clause_paren; + + pm->getCnfProof()->printClause(currentClause, os, clause_paren); + + // query appropriate theory for proof of clause + theory::TheoryId theory_id = currentStep->getTheory(); + Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl; + + std::set missingAssertions = recipe.getMissingAssertionsForStep(i); + if (!missingAssertions.empty()) { + Debug("pf::tp") << "Have missing assertions for this step!" << std::endl; + } + + // Turn rewrite filter ON + std::set::const_iterator missingAssertion; + for (missingAssertion = missingAssertions.begin(); + missingAssertion != missingAssertions.end(); + ++missingAssertion) { + + Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion << std::endl; + + Assert(recipe.wasRewritten(missingAssertion->negate())); + Node explanation = recipe.getExplanation(missingAssertion->negate()).negate(); + + Debug("pf::tp") << "Found explanation: " << explanation << std::endl; + + // We have a missing assertion. + // rewriteIt->first is the assertion after the rewrite (the explanation), + // rewriteIt->second is the original assertion that needs to be fed into the theory. + + bool found = false; + unsigned k; + for (k = 0; k < currentClauseExpr.size(); ++k) { + if (currentClauseExpr[k] == explanation.toExpr()) { + found = true; + break; + } + } + + Assert(found); + + Debug("pf::tp") << "Replacing theory assertion " + << currentClauseExpr[k] + << " with " + << *missingAssertion + << std::endl; + + currentClauseExpr[k] = missingAssertion->toExpr(); + + std::ostringstream rewritten; + rewritten << "(or_elim_1 _ _ "; + rewritten << "(not_not_intro _ "; + rewritten << pm->getLitName(explanation); + rewritten << ") (iff_elim_1 _ _ "; + rewritten << d_assertionToRewrite[missingAssertion->negate()]; + rewritten << "))"; + + Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl + << pm->getLitName(*missingAssertion) << " --> " << rewritten.str() + << std::endl << std::endl; + + pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str()); + } + + getTheoryProof(theory_id)->printTheoryLemmaProof(currentClauseExpr, os, paren); + + // Turn rewrite filter OFF + pm->clearRewriteFilters(); + + Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl; + os << clause_paren.str(); + os << "( \\ " << pm->getLemmaClauseName(id) << "s" << i <<"\n"; + paren << "))"; + } + + Assert(numberOfSteps >= 2); + + os << "(satlem_simplify _ _ _ "; + for (unsigned i = 0; i < numberOfSteps - 1; ++i) { + // Resolve step i with step i + 1 + if (recipe.getStep(i)->getLiteral().getKind() == kind::NOT) { + os << "(Q _ _ "; + } else { + os << "(R _ _ "; + } + + os << pm->getLemmaClauseName(id) << "s" << i; + os << " "; + } + + os << pm->getLemmaClauseName(id) << "s" << numberOfSteps - 1 << " "; + + prop::SatLiteral v; + for (int i = numberOfSteps - 2; i >= 0; --i) { + v = ProofManager::currentPM()->getCnfProof()->getLiteral(recipe.getStep(i)->getLiteral()); + os << ProofManager::getVarName(v.getSatVariable(), "") << ") "; + } + + os << "( \\ " << pm->getLemmaClauseName(id) << "\n"; + paren << "))"; + } } } void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const LetMap& map) { - // Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl; + Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl; LetMap::const_iterator it = map.find(term); if (it != map.end()) { @@ -597,19 +893,21 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Let } void TheoryProof::printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren) { - //default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory - Assert( d_theory!=NULL ); + // Default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory + Assert(d_theory!=NULL); + context::UserContext fakeContext; ProofOutputChannel oc; theory::Valuation v(NULL); //make new copy of theory theory::Theory* th; - Trace("theory-proof-debug") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl; - if(d_theory->getId()==theory::THEORY_UF) { + Trace("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl; + + if (d_theory->getId()==theory::THEORY_UF) { th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v, ProofManager::currentPM()->getLogicInfo(), "replay::"); - } else if(d_theory->getId()==theory::THEORY_ARRAY) { + } else if (d_theory->getId()==theory::THEORY_ARRAY) { th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v, ProofManager::currentPM()->getLogicInfo(), "replay::"); @@ -714,7 +1012,10 @@ void BooleanProof::registerTerm(Expr term) { void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { Assert (term.getType().isBoolean()); if (term.isVariable()) { - os << "(p_app " << ProofManager::sanitize(term) <<")"; + if (d_treatBoolsAsFormulas) + os << "(p_app " << ProofManager::sanitize(term) <<")"; + else + os << ProofManager::sanitize(term); return; } @@ -753,7 +1054,10 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& return; case kind::CONST_BOOLEAN: - os << (term.getConst() ? "true" : "false"); + if (d_treatBoolsAsFormulas) + os << (term.getConst() ? "true" : "false"); + else + os << (term.getConst() ? "t_true" : "t_false"); return; default: @@ -786,6 +1090,10 @@ void LFSCBooleanProof::printDeferredDeclarations(std::ostream& os, std::ostream& // Nothing to do here at this point. } +void LFSCBooleanProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} + void LFSCBooleanProof::printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren) { diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 54c86f3f3..c8c776ec9 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -27,6 +27,7 @@ #include "proof/clause_id.h" #include "prop/sat_solver_types.h" #include "util/proof.h" +#include "proof/proof_utils.h" namespace CVC4 { @@ -90,10 +91,14 @@ class TheoryProof; typedef __gnu_cxx::hash_set ExprSet; typedef std::map TheoryProofTable; +typedef std::set TheoryIdSet; +typedef std::map ExprToTheoryIds; + class TheoryProofEngine { protected: ExprSet d_registrationCache; TheoryProofTable d_theoryProofTable; + ExprToTheoryIds d_exprToTheoryIds; /** * Returns whether the theory is currently supported in proof @@ -147,6 +152,14 @@ public: */ virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0; + /** + * Print aliasing declarations. + * + * @param os + * @param paren closing parenthesis + */ + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0; + /** * Print proofs of all the theory lemmas (must prove * actual clause used in resolution proof). @@ -171,8 +184,14 @@ public: */ void registerTheory(theory::Theory* theory); - theory::TheoryId getTheoryForLemma(ClauseId id); + theory::TheoryId getTheoryForLemma(const prop::SatClause* clause); TheoryProof* getTheoryProof(theory::TheoryId id); + + void markTermForFutureRegistration(Expr term, theory::TheoryId id); + + void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2); + + virtual void treatBoolsAsFormulas(bool value) {}; }; class LFSCTheoryProofEngine : public TheoryProofEngine { @@ -190,11 +209,25 @@ public: virtual void printLetTerm(Expr term, std::ostream& os); virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map); virtual void printAssertions(std::ostream& os, std::ostream& paren); + virtual void printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren); virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren); virtual void printSort(Type type, std::ostream& os); + + void performExtraRegistrations(); + + void treatBoolsAsFormulas(bool value); + +private: + static void dumpTheoryLemmas(const IdToSatClause& lemmas); + + // TODO: this function should be moved into the BV prover. + void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren); + + std::map d_assertionToRewrite; }; class TheoryProof { @@ -269,12 +302,21 @@ public: * @param paren */ virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0; + /** + * Print any aliasing declarations. + * + * @param os + * @param paren + */ + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0; /** * Register a term of this theory that appears in the proof. * * @param term */ virtual void registerTerm(Expr term) = 0; + + virtual void treatBoolsAsFormulas(bool value) {} }; class BooleanProof : public TheoryProof { @@ -292,12 +334,13 @@ public: virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0; virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0; virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0; + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0; }; class LFSCBooleanProof : public BooleanProof { public: LFSCBooleanProof(TheoryProofEngine* proofEngine) - : BooleanProof(proofEngine) + : BooleanProof(proofEngine), d_treatBoolsAsFormulas(true) {} virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); virtual void printOwnedSort(Type type, std::ostream& os); @@ -305,6 +348,14 @@ public: virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren); + + void treatBoolsAsFormulas(bool value) { + d_treatBoolsAsFormulas = value; + } + +private: + bool d_treatBoolsAsFormulas; }; } /* CVC4 namespace */ diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index 32ca122b0..bc409901c 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -86,7 +86,16 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E pf->debug_print("pf::uf"); Debug("pf::uf") << std::endl; - if(tb == 0) { + if (tb == 0) { + // Special case: false was an input, so the proof is just "false". + if (pf->d_id == theory::eq::MERGED_THROUGH_EQUALITY && + pf->d_node == NodeManager::currentNM()->mkConst(false)) { + out << "(clausify_false "; + out << ProofManager::getLitName(NodeManager::currentNM()->mkConst(false).notNode()); + out << ")" << std::endl; + return Node(); + } + Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS); Assert(!pf->d_node.isNull()); Assert(pf->d_children.size() >= 2); @@ -190,42 +199,71 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E ++i; } } - Assert(neg >= 0); + + bool disequalityFound = (neg >= 0); + if (!disequalityFound) { + Debug("pf::uf") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl; + Debug("pf::uf") << "Proof for: " << pf->d_node << std::endl; + Assert(pf->d_node.getKind() == kind::EQUAL); + Assert(pf->d_node.getNumChildren() == 2); + Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst()); + } Node n1; std::stringstream ss; - //Assert(subTrans.d_children.size() == pf->d_children.size() - 1); Debug("pf::uf") << "\nsubtrans has " << subTrans.d_children.size() << " children\n"; - if(pf->d_children.size() > 2) { + + if(!disequalityFound || subTrans.d_children.size() >= 2) { n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map); } else { n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map); Debug("pf::uf") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl; } - Node n2 = pf->d_children[neg]->d_node; - Assert(n2.getKind() == kind::NOT); - out << "(clausify_false (contra _ "; Debug("pf::uf") << "\nhave proven: " << n1 << std::endl; - Debug("pf::uf") << "n2 is " << n2[0] << std::endl; - if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; } - if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; } + out << "(clausify_false (contra _ "; + + if (disequalityFound) { + Node n2 = pf->d_children[neg]->d_node; + Assert(n2.getKind() == kind::NOT); + Debug("pf::uf") << "n2 is " << n2[0] << std::endl; - if(n2[0].getKind() == kind::APPLY_UF) { - out << "(trans _ _ _ _ "; - out << "(symm _ _ _ "; - out << ss.str(); - out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl; - } else { - Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1])); - if(n1[1] == n2[0][0]) { - out << "(symm _ _ _ " << ss.str() << ")"; + if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; } + if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; } + + if(n2[0].getKind() == kind::APPLY_UF) { + out << "(trans _ _ _ _ "; + + if (n1[0] == n2[0]) { + out << "(symm _ _ _ "; + out << ss.str(); + out << ") "; + } else { + Assert(n1[1] == n2[0]); + out << ss.str(); + } + out << "(pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl; } else { - out << ss.str(); + Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1])); + if(n1[1] == n2[0][0]) { + out << "(symm _ _ _ " << ss.str() << ")"; + } else { + out << ss.str(); + } + out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; } - out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; + } else { + Node n2 = pf->d_node; + Assert(n2.getKind() == kind::EQUAL); + Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1])); + + out << ss.str(); + out << " "; + ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, n1[0].toExpr(), n1[1].toExpr()); + out << "))" << std::endl; } + return Node(); } @@ -584,10 +622,10 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) { // n1 is an equality/iff, but n2 is a predicate if(n1[0] == n2) { - n1 = n1[1]; + n1 = n1[1].iffNode(NodeManager::currentNM()->mkConst(true)); ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")"; } else if(n1[1] == n2) { - n1 = n1[0]; + n1 = n1[0].iffNode(NodeManager::currentNM()->mkConst(true)); ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")"; } else { Unreachable(); @@ -595,16 +633,16 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { // n2 is an equality/iff, but n1 is a predicate if(n2[0] == n1) { - n1 = n2[1]; + n1 = n2[1].iffNode(NodeManager::currentNM()->mkConst(true)); ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")"; } else if(n2[1] == n1) { - n1 = n2[0]; + n1 = n2[0].iffNode(NodeManager::currentNM()->mkConst(true)); ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")"; } else { Unreachable(); } } else { - // Both n1 and n2 are prediacates. Don't know what to do... + // Both n1 and n2 are predicates. Don't know what to do... Unreachable(); } @@ -667,6 +705,7 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) } Assert (term.getKind() == kind::APPLY_UF); + d_proofEngine->treatBoolsAsFormulas(false); if(term.getType().isBoolean()) { os << "(p_app "; @@ -683,6 +722,7 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) if(term.getType().isBoolean()) { os << ")"; } + d_proofEngine->treatBoolsAsFormulas(true); } void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) { @@ -714,6 +754,8 @@ void LFSCUFProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { // declaring the terms + Debug("pf::uf") << "LFSCUFProof::printTermDeclarations called" << std::endl; + for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) { Expr term = *it; @@ -729,7 +771,8 @@ void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { os << "(arrow"; for (unsigned i = 0; i < args.size(); i++) { Type arg_type = args[i]; - os << " " << arg_type; + os << " "; + d_proofEngine->printSort(arg_type, os); if (i < args.size() - 2) { os << " (arrow"; fparen << ")"; @@ -742,10 +785,16 @@ void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { } paren << ")"; } + + Debug("pf::uf") << "LFSCUFProof::printTermDeclarations done" << std::endl; } void LFSCUFProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) { // Nothing to do here at this point. } +void LFSCUFProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} + } /* namespace CVC4 */ diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h index e359eaebd..0a23267d8 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -69,6 +69,7 @@ public: virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); + virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren); }; diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index aa1fc9587..eda736b8a 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -120,7 +120,7 @@ bool CnfStream::hasLiteral(TNode n) const { return find != d_nodeToLiteralMap.end(); } -void TseitinCnfStream::ensureLiteral(TNode n) { +void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) { // These are not removable and have no proof ID d_removable = false; @@ -163,7 +163,7 @@ void TseitinCnfStream::ensureLiteral(TNode n) { d_literalToNodeMap.insert_safe(~lit, n.notNode()); } else { // We have a theory atom or variable. - lit = convertAtom(n); + lit = convertAtom(n, noPreregistration); } Assert(hasLiteral(n) && getNode(lit) == n); @@ -232,7 +232,7 @@ void CnfStream::setProof(CnfProof* proof) { d_cnfProof = proof; } -SatLiteral CnfStream::convertAtom(TNode node) { +SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) { Debug("cnf") << "convertAtom(" << node << ")" << endl; Assert(!hasLiteral(node), "atom already mapped!"); @@ -247,7 +247,7 @@ SatLiteral CnfStream::convertAtom(TNode node) { } else { theoryLiteral = true; canEliminate = false; - preRegister = true; + preRegister = !noPreregistration; } // Make a new literal (variables are not considered theory literals) @@ -258,7 +258,11 @@ SatLiteral CnfStream::convertAtom(TNode node) { SatLiteral CnfStream::getLiteral(TNode node) { Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node"); - Assert(d_nodeToLiteralMap.contains(node), "Literal not in the CNF Cache: %s\n", node.toString().c_str()); + + Assert(d_nodeToLiteralMap.contains(node), + "Literal not in the CNF Cache: %s\n", + node.toString().c_str()); + SatLiteral literal = d_nodeToLiteralMap[node]; Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; return literal; @@ -675,7 +679,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proof_id, TNode from, - theory::TheoryId ownerTheory) { + LemmaProofRecipe* proofRecipe) { Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl; @@ -685,7 +689,12 @@ void TseitinCnfStream::convertAndAssert(TNode node, Node assertion = negated ? node.notNode() : (Node)node; Node from_assertion = negated? from.notNode() : (Node) from; - d_cnfProof->setExplainerTheory(ownerTheory); + if (proofRecipe) { + Debug("pf::sat") << "TseitinCnfStream::convertAndAssert: setting proof recipe" << std::endl; + proofRecipe->dump("pf::sat"); + d_cnfProof->setProofRecipe(proofRecipe); + } + if (proof_id != RULE_INVALID) { d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion); d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id); diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index cf9d519a7..6cc10d878 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -36,6 +36,9 @@ #include "smt_util/lemma_channels.h" namespace CVC4 { + +class LemmaProofRecipe; + namespace prop { class PropEngine; @@ -174,7 +177,7 @@ protected: * structure in this expression. Assumed to not be in the * translation cache. */ - SatLiteral convertAtom(TNode node); + SatLiteral convertAtom(TNode node, bool noPreprocessing = false); public: @@ -207,14 +210,10 @@ public: * @param node node to convert and assert * @param removable whether the sat solver can choose to remove the clauses * @param negated whether we are asserting the node negated - * @param ownerTheory indicates the theory that should invoked to prove the formula. + * @param proofRecipe contains the proof recipe for proving this node */ - virtual void convertAndAssert(TNode node, - bool removable, - bool negated, - ProofRule proof_id, - TNode from = TNode::null(), - theory::TheoryId ownerTheory = theory::THEORY_LAST) = 0; + virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null(), LemmaProofRecipe* proofRecipe = NULL) = 0; + /** * Get the node that is represented by the given SatLiteral. * @param literal the literal from the sat solver @@ -235,7 +234,7 @@ public: * this is like a "convert-but-don't-assert" version of * convertAndAssert(). */ - virtual void ensureLiteral(TNode n) = 0; + virtual void ensureLiteral(TNode n, bool noPreregistration = false) = 0; /** * Returns the literal that represents the given node in the SAT CNF @@ -284,7 +283,7 @@ public: */ void convertAndAssert(TNode node, bool removable, bool negated, ProofRule rule, TNode from = TNode::null(), - theory::TheoryId ownerTheory = theory::THEORY_LAST); + LemmaProofRecipe* proofRecipe = NULL); /** * Constructs the stream to use the given sat solver. @@ -337,7 +336,7 @@ private: */ SatLiteral toCNF(TNode node, bool negated = false); - void ensureLiteral(TNode n); + void ensureLiteral(TNode n, bool noPreregistration = false); };/* class TseitinCnfStream */ diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 411b89514..d898b66a2 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -232,6 +232,8 @@ CRef Solver::reason(Var x) { vec explanation; MinisatSatSolver::toMinisatClause(explanation_cl, explanation); + Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl << std::endl; + // Sort the literals by trail index level lemma_lt lt(*this); sort(explanation, lt); @@ -266,6 +268,12 @@ CRef Solver::reason(Var x) { } explanation.shrink(i - j); + Debug("pf::sat") << "Solver::reason: explanation = " ; + for (int i = 0; i < explanation.size(); ++i) { + Debug("pf::sat") << explanation[i] << " "; + } + Debug("pf::sat") << std::endl; + // We need an explanation clause so we add a fake literal if (j == 1) { // Add not TRUE to the clause @@ -276,6 +284,7 @@ CRef Solver::reason(Var x) { CRef real_reason = ca.alloc(explLevel, explanation, true); // FIXME: at some point will need more information about where this explanation // came from (ie. the theory/sharing) + Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl; PROOF (ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); ProofManager::getCnfProof()->registerConvertedClause(id, true); // no need to pop current assertion as this is not converted to cnf @@ -336,6 +345,12 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) // If we are in solve or decision level > 0 if (minisat_busy || decisionLevel() > 0) { + Debug("pf::sat") << "Add clause adding a new lemma: "; + for (int k = 0; k < ps.size(); ++k) { + Debug("pf::sat") << ps[k] << " "; + } + Debug("pf::sat") << std::endl; + lemmas.push(); ps.copyTo(lemmas.last()); lemmas_removable.push(removable); @@ -1666,6 +1681,13 @@ CRef Solver::updateLemmas() { { // The current lemma vec& lemma = lemmas[i]; + + Debug("pf::sat") << "Solver::updateLemmas: working on lemma: "; + for (int k = 0; k < lemma.size(); ++k) { + Debug("pf::sat") << lemma[k] << " "; + } + Debug("pf::sat") << std::endl; + // If it's an empty lemma, we have a conflict at zero level if (lemma.size() == 0) { Assert (! PROOF_ON()); @@ -1725,6 +1747,7 @@ CRef Solver::updateLemmas() { TNode cnf_assertion = lemmas_cnf_assertion[i].first; TNode cnf_def = lemmas_cnf_assertion[i].second; + Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl; ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); @@ -1741,6 +1764,7 @@ CRef Solver::updateLemmas() { Node cnf_assertion = lemmas_cnf_assertion[i].first; Node cnf_def = lemmas_cnf_assertion[i].second; + Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3)" << std::endl; ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index bfbf9da6f..ff726e299 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -150,7 +150,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) { // FIXME: This relies on the invariant that when ok() is false // the SAT solver does not add the clause (which is what Minisat currently does) if (!ok()) { - return ClauseIdUndef; + return ClauseIdUndef; } d_minisat->addClause(minisat_clause, removable, clause_id); PROOF( Assert (clause_id != ClauseIdError);); @@ -185,7 +185,7 @@ SatValue MinisatSatSolver::solve() { } bool MinisatSatSolver::ok() const { - return d_minisat->okay(); + return d_minisat->okay(); } void MinisatSatSolver::interrupt() { @@ -204,20 +204,20 @@ bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const return true; } -void MinisatSatSolver::requirePhase(SatLiteral lit) { +void MinisatSatSolver::requirePhase(SatLiteral lit) { Assert(!d_minisat->rnd_pol); Debug("minisat") << "requirePhase(" << lit << ")" << " " << lit.getSatVariable() << " " << lit.isNegated() << std::endl; SatVariable v = lit.getSatVariable(); d_minisat->freezePolarity(v, lit.isNegated()); } -bool MinisatSatSolver::flipDecision() { +bool MinisatSatSolver::flipDecision() { Debug("minisat") << "flipDecision()" << std::endl; return d_minisat->flipDecision(); } -bool MinisatSatSolver::isDecision(SatVariable decn) const { - return d_minisat->isDecision( decn ); +bool MinisatSatSolver::isDecision(SatVariable decn) const { + return d_minisat->isDecision( decn ); } /** Incremental interface */ @@ -291,7 +291,7 @@ namespace CVC4 { template<> prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) { return prop::MinisatSatSolver::toSatLiteral(lit); -} +} template<> void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl, @@ -300,5 +300,3 @@ void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& } } /* namespace CVC4 */ - - diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 54cf4c457..eb607e901 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -132,13 +132,13 @@ void PropEngine::assertFormula(TNode node) { void PropEngine::assertLemma(TNode node, bool negated, bool removable, ProofRule rule, - theory::TheoryId ownerTheory, + LemmaProofRecipe* proofRecipe, TNode from) { //Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; // Assert as (possibly) removable - d_cnfStream->convertAndAssert(node, removable, negated, rule, from, ownerTheory); + d_cnfStream->convertAndAssert(node, removable, negated, rule, from, proofRecipe); } void PropEngine::requirePhase(TNode n, bool phase) { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index b9ce7ca7e..c02015931 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -37,6 +37,7 @@ namespace CVC4 { class ResourceManager; class DecisionEngine; class TheoryEngine; +class LemmaProofRecipe; namespace theory { class TheoryRegistrar; @@ -134,7 +135,7 @@ public: * @param removable whether this lemma can be quietly removed based * on an activity heuristic (or not) */ - void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, theory::TheoryId ownerTheory, TNode from = TNode::null()); + void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, LemmaProofRecipe* proofRecipe, TNode from = TNode::null()); /** * If ever n is decided upon, it must be in the given phase. This diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 4a4515eb9..6e8f1fbbf 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -99,29 +99,34 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { TNode lNode = d_cnfStream->getNode(l); Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl; - NodeTheoryPair theoryExplanation = d_theoryEngine->getExplanationAndExplainer(lNode); - Node explanationNode = theoryExplanation.node; - theory::TheoryId explainerTheory = theoryExplanation.theory; + LemmaProofRecipe* proofRecipe = NULL; + PROOF(proofRecipe = new LemmaProofRecipe;); + + Node theoryExplanation = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe); PROOF({ - ProofManager::getCnfProof()->pushCurrentAssertion(explanationNode); - ProofManager::getCnfProof()->setExplainerTheory(explainerTheory); + ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); + ProofManager::getCnfProof()->setProofRecipe(proofRecipe); + + Debug("pf::sat") << "TheoryProxy::explainPropagation: setting lemma recipe to: " + << std::endl; + proofRecipe->dump("pf::sat"); - Debug("pf::sat") << "TheoryProxy::explainPropagation: setting explainer theory to: " - << explainerTheory << std::endl; + delete proofRecipe; + proofRecipe = NULL; }); - Debug("prop-explain") << "explainPropagation() => " << explanationNode << std::endl; - if (explanationNode.getKind() == kind::AND) { - Node::const_iterator it = explanationNode.begin(); - Node::const_iterator it_end = explanationNode.end(); + Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl; + if (theoryExplanation.getKind() == kind::AND) { + Node::const_iterator it = theoryExplanation.begin(); + Node::const_iterator it_end = theoryExplanation.end(); explanation.push_back(l); for (; it != it_end; ++ it) { explanation.push_back(~d_cnfStream->getLiteral(*it)); } } else { explanation.push_back(l); - explanation.push_back(~d_cnfStream->getLiteral(explanationNode)); + explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation)); } } @@ -175,7 +180,9 @@ void TheoryProxy::notifyRestart() { if(lemmaCount % 1 == 0) { Debug("shared") << "=) " << asNode << std::endl; } - d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, theory::THEORY_LAST); + + LemmaProofRecipe* noProofRecipe = NULL; + d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, noProofRecipe); } else { Debug("shared") << "=(" << asNode << std::endl; } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8f282b413..63afb0b72 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -990,7 +990,7 @@ public: Trace("smt-qe-debug") << " return : " << ret << std::endl; //recursive (for nested quantification) ret = replaceQuantifiersWithInstantiations( reti, insts, visited ); - } + } }else if( n.getNumChildren()>0 ){ bool childChanged = false; std::vector< Node > children; @@ -1723,14 +1723,14 @@ void SmtEngine::setDefaults() { //must have finite model finding on options::finiteModelFind.set( true ); } - + //if it contains a theory with non-termination, do not strictly enforce that quantifiers and theory combination must be interleaved if( d_logic.isTheoryEnabled(THEORY_STRINGS) || (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) ){ if( !options::instWhenStrictInterleave.wasSetByUser() ){ options::instWhenStrictInterleave.set( false ); } } - + //local theory extensions if( options::localTheoryExt() ){ if( !options::instMaxLevel.wasSetByUser() ){ @@ -1803,8 +1803,8 @@ void SmtEngine::setDefaults() { //apply counterexample guided instantiation options if( options::cegqiSingleInvMode()!=quantifiers::CEGQI_SI_MODE_NONE ){ if( !options::ceGuidedInst.wasSetByUser() ){ - options::ceGuidedInst.set( true ); - } + options::ceGuidedInst.set( true ); + } } if( options::ceGuidedInst() ){ //counterexample-guided instantiation for sygus @@ -1845,7 +1845,7 @@ void SmtEngine::setDefaults() { } //counterexample-guided instantiation for non-sygus // enable if any quantifiers with arithmetic or datatypes - if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) || + if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) || options::cbqiAll() ){ if( !options::cbqi.wasSetByUser() ){ options::cbqi.set( true ); @@ -3858,7 +3858,7 @@ void SmtEnginePrivate::processAssertions() { ProofManager::currentPM()->addAssertion(d_assertions[i].toExpr()); } ); - + Debug("smt") << " d_assertions : " << d_assertions.size() << endl; if( options::ceGuidedInst() ){ @@ -4240,7 +4240,7 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl; dumpAssertions("post-everything", d_assertions); - + //set instantiation level of everything to zero if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){ @@ -4434,18 +4434,18 @@ Result SmtEngine::checkSynth(const Expr& e) throw(TypeCheckingException, ModalEx //possibly run quantifier elimination to make formula into single invocation if( conj[1].getKind()==kind::EXISTS ){ Node conj_se = conj[1][1]; - + Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl; quantifiers::SingleInvocationPartition sip( kind::APPLY ); sip.init( conj_se ); Trace("smt-synth") << "...finished, got:" << std::endl; sip.debugPrint("smt-synth"); - + if( !sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation() ){ //We are in the case where our synthesis conjecture is exists f. forall xy. P( f( x ), x, y ), P does not contain f. - //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ), + //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ), // and then constructs exists f. forall x. Q( f( x ), x ), where Q does not contain f. We invoke synthesis solver on this result. - + //create new smt engine to do quantifier elimination SmtEngine smt_qe( d_exprManager ); smt_qe.setLogic(getLogicInfo()); @@ -4480,11 +4480,11 @@ Result SmtEngine::checkSynth(const Expr& e) throw(TypeCheckingException, ModalEx Node conj_se_ngsi_subs = conj_se_ngsi.substitute( orig.begin(), orig.end(), subs.begin(), subs.end() ); Assert( !qe_vars.empty() ); conj_se_ngsi_subs = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, qe_vars ), conj_se_ngsi_subs ); - + Trace("smt-synth") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl; Expr qe_res = smt_qe.doQuantifierElimination( conj_se_ngsi_subs.toExpr(), true, false ); Trace("smt-synth") << "Result : " << qe_res << std::endl; - + //create single invocation conjecture Node qe_res_n = Node::fromExpr( qe_res ); qe_res_n = qe_res_n.substitute( subs.begin(), subs.end(), orig.begin(), orig.end() ); @@ -4498,7 +4498,7 @@ Result SmtEngine::checkSynth(const Expr& e) throw(TypeCheckingException, ModalEx } } } - + return checkSatisfiability( e_check, true, false ); } @@ -5125,7 +5125,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl; } Trace("smt-qe") << "Do quantifier elimination " << e << std::endl; - Node n_e = Node::fromExpr( e ); + Node n_e = Node::fromExpr( e ); if( n_e.getKind()!=kind::EXISTS ){ throw ModalException("Expecting an existentially quantified formula as argument to get-qe."); } @@ -5152,7 +5152,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) InternalError(ss.str().c_str()); } //get the instantiations for all quantified formulas - std::map< Node, std::vector< Node > > insts; + std::map< Node, std::vector< Node > > insts; d_theoryEngine->getInstantiations( insts ); //find the quantified formula that corresponds to the input Node top_q; diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index 5634a4651..808f5162c 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -63,14 +63,21 @@ void SmtEngine::checkProof() { Chat() << "checking proof..." << endl; - if ( !(d_logic.isPure(theory::THEORY_BOOL) || - d_logic.isPure(theory::THEORY_BV) || - d_logic.isPure(theory::THEORY_ARRAY) || - (d_logic.isPure(theory::THEORY_UF) && - ! d_logic.hasCardinalityConstraints())) || - d_logic.isQuantified()) { - // no checking for these yet - Notice() << "Notice: no proof-checking for non-UF/Bool/BV proofs yet" << endl; + std::string logicString = d_logic.getLogicString(); + + if (!( + // Pure logics + logicString == "QF_UF" || + logicString == "QF_AX" || + logicString == "QF_BV" || + // Non-pure logics + logicString == "QF_AUF" || + logicString == "QF_UFBV" || + logicString == "QF_ABV" || + logicString == "QF_AUFBV" + )) { + // This logic is not yet supported + Notice() << "Notice: no proof-checking for " << logicString << " proofs yet" << endl; return; } diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp index 11c3dc081..6dfd14157 100644 --- a/src/theory/arrays/array_proof_reconstruction.cpp +++ b/src/theory/arrays/array_proof_reconstruction.cpp @@ -101,8 +101,59 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, Debug("pf::ee") << "Getting explanation for ROW guard: " << indexOne << " != " << indexTwo << std::endl; + eq::EqProof* childProof = new eq::EqProof; d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities, childProof); + + // It could be that the guard condition is a constant disequality. In this case, + // we need to change it to a different format. + if (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) { + // The proof has two children, explaining why each index is a (different) constant. + Assert(childProof->d_children.size() == 2); + + Node constantOne, constantTwo; + // Each subproof explains why one of the indices is constant. + + if (childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) { + constantOne = childProof->d_children[0]->d_node; + } else { + Assert(childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_EQUALITY); + if ((childProof->d_children[0]->d_node[0] == indexOne) || + (childProof->d_children[0]->d_node[0] == indexTwo)) { + constantOne = childProof->d_children[0]->d_node[1]; + } else { + constantOne = childProof->d_children[0]->d_node[0]; + } + } + + if (childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) { + constantTwo = childProof->d_children[1]->d_node; + } else { + Assert(childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_EQUALITY); + if ((childProof->d_children[1]->d_node[0] == indexOne) || + (childProof->d_children[1]->d_node[0] == indexTwo)) { + constantTwo = childProof->d_children[1]->d_node[1]; + } else { + constantTwo = childProof->d_children[1]->d_node[0]; + } + } + + eq::EqProof* constantDisequalityProof = new eq::EqProof; + constantDisequalityProof->d_id = theory::eq::MERGED_THROUGH_CONSTANTS; + constantDisequalityProof->d_node = + NodeManager::currentNM()->mkNode(kind::EQUAL, constantOne, constantTwo).negate(); + + // Middle is where we need to insert the new disequality + std::vector::iterator middle = childProof->d_children.begin(); + ++middle; + + childProof->d_children.insert(middle, constantDisequalityProof); + + childProof->d_id = theory::eq::MERGED_THROUGH_TRANS; + childProof->d_node = + NodeManager::currentNM()->mkNode(kind::EQUAL, indexOne, indexTwo).negate(); + } + proof->d_children.push_back(childProof); } else { // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]), diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 6add1b55f..28a08630e 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -829,7 +829,8 @@ void TheoryArrays::propagate(Effort e) Node TheoryArrays::explain(TNode literal) { - return explain(literal, NULL); + Node explanation = explain(literal, NULL); + return explanation; } Node TheoryArrays::explain(TNode literal, eq::EqProof *proof) @@ -1394,6 +1395,7 @@ void TheoryArrays::check(Effort e) { break; default: Unreachable(); + break; } } @@ -2231,6 +2233,7 @@ bool TheoryArrays::dischargeLemmas() void TheoryArrays::conflict(TNode a, TNode b) { Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl; eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL; + if (a.getKind() == kind::CONST_BOOLEAN) { d_conflictNode = explain(a.iffNode(b), proof); } else { diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index fdc36ce72..dc5520411 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -41,7 +41,7 @@ bool AbstractionModule::applyAbstraction(const std::vector& assertions, st continue; } Node signature = computeSignature(assertions[i][j]); - storeSignature(signature, assertions[i][j]); + storeSignature(signature, assertions[i][j]); Debug("bv-abstraction") << " assertion: " << assertions[i][j] <<"\n"; Debug("bv-abstraction") << " signature: " << signature <<"\n"; } @@ -52,7 +52,7 @@ bool AbstractionModule::applyAbstraction(const std::vector& assertions, st for (unsigned i = 0; i < assertions.size(); ++i) { if (assertions[i].getKind() == kind::OR && assertions[i][0].getKind() == kind::AND) { - std::vector new_children; + std::vector new_children; for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) { if (hasSignature(assertions[i][j])) { new_children.push_back(abstractSignatures(assertions[i][j])); @@ -60,10 +60,10 @@ bool AbstractionModule::applyAbstraction(const std::vector& assertions, st new_children.push_back(assertions[i][j]); } } - new_assertions.push_back(utils::mkNode(kind::OR, new_children)); + new_assertions.push_back(utils::mkNode(kind::OR, new_children)); } else { // assertions that are not changed - new_assertions.push_back(assertions[i]); + new_assertions.push_back(assertions[i]); } } @@ -71,21 +71,21 @@ bool AbstractionModule::applyAbstraction(const std::vector& assertions, st skolemizeArguments(new_assertions); } - + // if we are using the eager solver reverse the abstraction if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { if (d_funcToSignature.size() == 0) { // we did not change anything return false; } - NodeNodeMap seen; + NodeNodeMap seen; for (unsigned i = 0; i < new_assertions.size(); ++i) { - new_assertions[i] = reverseAbstraction(new_assertions[i], seen); + new_assertions[i] = reverseAbstraction(new_assertions[i], seen); } // we undo the abstraction functions so the logic is QF_BV still - return true; + return true; } - + // return true if we have created new function symbols for the problem return d_funcToSignature.size() != 0; } @@ -99,7 +99,7 @@ bool AbstractionModule::isConjunctionOfAtoms(TNode node) { bool AbstractionModule::isConjunctionOfAtomsRec(TNode node, TNodeSet& seen) { if (seen.find(node)!= seen.end()) return true; - + if (!node.getType().isBitVector()) { return (node.getKind() == kind::AND || utils::isBVPredicate(node)); } @@ -120,30 +120,30 @@ Node AbstractionModule::reverseAbstraction(Node assertion, NodeNodeMap& seen) { if (seen.find(assertion) != seen.end()) return seen[assertion]; - + if (isAbstraction(assertion)) { Node interp = getInterpretation(assertion); seen[assertion] = interp; - Assert (interp.getType() == assertion.getType()); + Assert (interp.getType() == assertion.getType()); return interp; } if (assertion.getNumChildren() == 0) { seen[assertion] = assertion; - return assertion; + return assertion; } - + NodeBuilder<> result(assertion.getKind()); if (assertion.getMetaKind() == kind::metakind::PARAMETERIZED) { - result << assertion.getOperator(); + result << assertion.getOperator(); } for (unsigned i = 0; i < assertion.getNumChildren(); ++i) { - result << reverseAbstraction(assertion[i], seen); + result << reverseAbstraction(assertion[i], seen); } Node res = result; seen[assertion] = res; - return res; + return res; } void AbstractionModule::skolemizeArguments(std::vector& assertions) { @@ -151,7 +151,7 @@ void AbstractionModule::skolemizeArguments(std::vector& assertions) { TNode assertion = assertions[i]; if (assertion.getKind() != kind::OR) continue; - + bool is_skolemizable = true; for (unsigned k = 0; k < assertion.getNumChildren(); ++k) { if (assertion[k].getKind() != kind::EQUAL || @@ -191,54 +191,54 @@ void AbstractionModule::skolemizeArguments(std::vector& assertions) { NodeBuilder<> skolem_func (kind::APPLY_UF); skolem_func << func; std::vector skolem_args; - + for (unsigned j = 0; j < args.getArity(); ++j) { bool all_same = true; for (unsigned k = 1; k < args.getNumEntries(); ++k) { if ( args.getEntry(k)[j] != args.getEntry(0)[j]) - all_same = false; + all_same = false; } - Node new_arg = all_same ? (Node)args.getEntry(0)[j] : utils::mkVar(utils::getSize(args.getEntry(0)[j])); + Node new_arg = all_same ? (Node)args.getEntry(0)[j] : utils::mkVar(utils::getSize(args.getEntry(0)[j])); skolem_args.push_back(new_arg); - skolem_func << new_arg; + skolem_func << new_arg; } - - Node skolem_func_eq1 = utils::mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u)); - + + Node skolem_func_eq1 = utils::mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u)); + // enumerate arguments assignments - std::vector or_assignments; + std::vector or_assignments; for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); ++it) { NodeBuilder<> arg_assignment(kind::AND); ArgsVec& args = *it; for (unsigned k = 0; k < args.size(); ++k) { Node eq = utils::mkNode(kind::EQUAL, args[k], skolem_args[k]); - arg_assignment << eq; + arg_assignment << eq; } or_assignments.push_back(arg_assignment); } - + Node new_func_def = utils::mkNode(kind::AND, skolem_func_eq1, utils::mkNode(kind::OR, or_assignments)); - assertion_builder << new_func_def; + assertion_builder << new_func_def; } Node new_assertion = assertion_builder; Debug("bv-abstraction-dbg") << "AbstractionModule::skolemizeArguments " << assertions[i] << " => \n"; - Debug("bv-abstraction-dbg") << " " << new_assertion; + Debug("bv-abstraction-dbg") << " " << new_assertion; assertions[i] = new_assertion; } } void AbstractionModule::storeSignature(Node signature, TNode assertion) { if(d_signatures.find(signature) == d_signatures.end()) { - d_signatures[signature] = 0; + d_signatures[signature] = 0; } - d_signatures[signature] = d_signatures[signature] + 1; - d_assertionToSignature[assertion] = signature; + d_signatures[signature] = d_signatures[signature] + 1; + d_assertionToSignature[assertion] = signature; } Node AbstractionModule::computeSignature(TNode node) { - resetSignatureIndex(); - NodeNodeMap cache; + resetSignatureIndex(); + NodeNodeMap cache; Node sig = computeSignatureRec(node, cache); return sig; } @@ -247,17 +247,17 @@ Node AbstractionModule::getSignatureSkolem(TNode node) { Assert (node.getKind() == kind::VARIABLE); unsigned bitwidth = utils::getSize(node); if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end()) { - d_signatureSkolems[bitwidth] = vector(); + d_signatureSkolems[bitwidth] = vector(); } - + vector& skolems = d_signatureSkolems[bitwidth]; // get the index of bv variables of this size - unsigned index = getBitwidthIndex(bitwidth); + unsigned index = getBitwidthIndex(bitwidth); Assert (skolems.size() + 1 >= index ); if (skolems.size() == index) { ostringstream os; os << "sig_" <mkSkolem(os.str(), nm->mkBitVectorType(bitwidth), "skolem for computing signatures")); } ++(d_signatureIndices[bitwidth]); @@ -268,12 +268,12 @@ unsigned AbstractionModule::getBitwidthIndex(unsigned bitwidth) { if (d_signatureIndices.find(bitwidth) == d_signatureIndices.end()) { d_signatureIndices[bitwidth] = 0; } - return d_signatureIndices[bitwidth]; + return d_signatureIndices[bitwidth]; } void AbstractionModule::resetSignatureIndex() { for (IndexMap::iterator it = d_signatureIndices.begin(); it != d_signatureIndices.end(); ++it) { - it->second = 0; + it->second = 0; } } @@ -282,24 +282,24 @@ bool AbstractionModule::hasSignature(Node node) { } Node AbstractionModule::getGeneralizedSignature(Node node) { - NodeNodeMap::const_iterator it = d_assertionToSignature.find(node); + NodeNodeMap::const_iterator it = d_assertionToSignature.find(node); Assert (it != d_assertionToSignature.end()); - Node generalized_signature = getGeneralization(it->second); - return generalized_signature; + Node generalized_signature = getGeneralization(it->second); + return generalized_signature; } Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) { if (cache.find(node) != cache.end()) { - return cache.find(node)->second; + return cache.find(node)->second; } - + if (node.getNumChildren() == 0) { if (node.getKind() == kind::CONST_BITVECTOR) return node; Node sig = getSignatureSkolem(node); - cache[node] = sig; - return sig; + cache[node] = sig; + return sig; } NodeBuilder<> builder(node.getKind()); @@ -308,30 +308,30 @@ Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) { } for (unsigned i = 0; i < node.getNumChildren(); ++i) { Node converted = computeSignatureRec(node[i], cache); - builder << converted; + builder << converted; } Node result = builder; cache[node] = result; - return result; + return result; } -/** +/** * Returns 0, if the two are equal, * 1 if s is a generalization of t * 2 if t is a generalization of s * -1 if the two cannot be unified * - * @param s - * @param t - * - * @return + * @param s + * @param t + * + * @return */ int AbstractionModule::comparePatterns(TNode s, TNode t) { if (s.getKind() == kind::SKOLEM && t.getKind() == kind::SKOLEM) { return 0; } - + if (s.getKind() == kind::CONST_BITVECTOR && t.getKind() == kind::CONST_BITVECTOR) { if (s == t) { @@ -350,7 +350,7 @@ int AbstractionModule::comparePatterns(TNode s, TNode t) { t.getKind() == kind::SKOLEM) { return 2; } - + if (s.getNumChildren() != t.getNumChildren() || s.getKind() != t.getKind()) return -1; @@ -370,26 +370,26 @@ int AbstractionModule::comparePatterns(TNode s, TNode t) { } TNode AbstractionModule::getGeneralization(TNode term) { - NodeNodeMap::iterator it = d_sigToGeneralization.find(term); + NodeNodeMap::iterator it = d_sigToGeneralization.find(term); // if not in the map we add it if (it == d_sigToGeneralization.end()) { d_sigToGeneralization[term] = term; - return term; + return term; } - // doesn't have a generalization + // doesn't have a generalization if (it->second == term) return term; - + TNode generalization = getGeneralization(it->second); Assert (generalization != term); d_sigToGeneralization[term] = generalization; - return generalization; + return generalization; } void AbstractionModule::storeGeneralization(TNode s, TNode t) { Assert (s == getGeneralization(s)); Assert (t == getGeneralization(t)); - d_sigToGeneralization[s] = t; + d_sigToGeneralization[s] = t; } void AbstractionModule::finalizeSignatures() { @@ -402,29 +402,29 @@ void AbstractionModule::finalizeSignatures() { for (SignatureMap::const_iterator tt = ss; tt != d_signatures.end(); ++tt) { TNode t = getGeneralization(tt->first); TNode s = getGeneralization(ss->first); - + if (t != s) { int status = comparePatterns(s, t); - Assert (status); + Assert (status); if (status < 0) continue; if (status == 1) { - storeGeneralization(t, s); + storeGeneralization(t, s); } else { - storeGeneralization(s, t); + storeGeneralization(s, t); } } } } // keep only most general signatures for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) { - TNode sig = it->first; + TNode sig = it->first; TNode gen = getGeneralization(sig); if (sig != gen) { - Assert (d_signatures.find(gen) != d_signatures.end()); + Assert (d_signatures.find(gen) != d_signatures.end()); // update the count d_signatures[gen]+= d_signatures[sig]; - d_signatures.erase(it++); + d_signatures.erase(it++); } else { ++it; } @@ -434,12 +434,12 @@ void AbstractionModule::finalizeSignatures() { // remove signatures that are not frequent enough for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) { if (it->second <= 7) { - d_signatures.erase(it++); + d_signatures.erase(it++); } else { ++it; } } - + for (SignatureMap::const_iterator it = d_signatures.begin(); it != d_signatures.end(); ++it) { TNode signature = it->first; // we already processed this signature @@ -451,31 +451,31 @@ void AbstractionModule::finalizeSignatures() { collectArgumentTypes(signature, arg_types, seen); Assert (signature.getType().isBoolean()); // make function return a bitvector of size 1 - //Node bv_function = utils::mkNode(kind::ITE, signature, utils::mkConst(1, 1u), utils::mkConst(1, 0u)); + //Node bv_function = utils::mkNode(kind::ITE, signature, utils::mkConst(1, 1u), utils::mkConst(1, 0u)); TypeNode range = NodeManager::currentNM()->mkBitVectorType(1); - + TypeNode abs_type = nm->mkFunctionType(arg_types, range); Node abs_func = nm->mkSkolem("abs_$$", abs_type, "abstraction function for bv theory"); Debug("bv-abstraction") << " abstracted by function " << abs_func << "\n"; // NOTE: signature expression type is BOOLEAN d_signatureToFunc[signature] = abs_func; - d_funcToSignature[abs_func] = signature; + d_funcToSignature[abs_func] = signature; } d_statistics.d_numFunctionsAbstracted.setData(d_signatureToFunc.size()); - + Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted " << d_signatureToFunc.size() << " signatures. \n"; } void AbstractionModule::collectArgumentTypes(TNode sig, std::vector& types, TNodeSet& seen) { if (seen.find(sig) != seen.end()) return; - + if (sig.getKind() == kind::SKOLEM) { types.push_back(sig.getType()); - seen.insert(sig); - return; + seen.insert(sig); + return; } for (unsigned i = 0; i < sig.getNumChildren(); ++i) { @@ -487,36 +487,36 @@ void AbstractionModule::collectArgumentTypes(TNode sig, std::vector& t void AbstractionModule::collectArguments(TNode node, TNode signature, std::vector& args, TNodeSet& seen) { if (seen.find(node)!= seen.end()) return; - + if (node.getKind() == kind::VARIABLE || node.getKind() == kind::CONST_BITVECTOR) { // a constant in the node can either map to an argument of the abstraction - // or can be hard-coded and part of the abstraction + // or can be hard-coded and part of the abstraction if (signature.getKind() == kind::SKOLEM) { args.push_back(node); seen.insert(node); } else { - Assert (signature.getKind() == kind::CONST_BITVECTOR); + Assert (signature.getKind() == kind::CONST_BITVECTOR); } - // - return; + // + return; } Assert (node.getKind() == signature.getKind() && - node.getNumChildren() == signature.getNumChildren()); + node.getNumChildren() == signature.getNumChildren()); for (unsigned i = 0; i < node.getNumChildren(); ++i) { - collectArguments(node[i], signature[i], args, seen); - seen.insert(node); + collectArguments(node[i], signature[i], args, seen); + seen.insert(node); } } Node AbstractionModule::abstractSignatures(TNode assertion) { - Debug("bv-abstraction") << "AbstractionModule::abstractSignatures "<< assertion <<"\n"; + Debug("bv-abstraction") << "AbstractionModule::abstractSignatures "<< assertion <<"\n"; // assume the assertion has been fully abstracted Node signature = getGeneralizedSignature(assertion); - - Debug("bv-abstraction") << " with sig "<< signature <<"\n"; + + Debug("bv-abstraction") << " with sig "<< signature <<"\n"; NodeNodeMap::iterator it = d_signatureToFunc.find(signature); if (it!= d_signatureToFunc.end()) { std::vector args; @@ -527,16 +527,16 @@ Node AbstractionModule::abstractSignatures(TNode assertion) { collectArguments(assertion, signature, args, seen); std::vector real_args; for (unsigned i = 1; i < args.size(); ++i) { - real_args.push_back(args[i]); + real_args.push_back(args[i]); } - d_argsTable.addEntry(func, real_args); - Node result = utils::mkNode(kind::EQUAL, utils::mkNode(kind::APPLY_UF, args), + d_argsTable.addEntry(func, real_args); + Node result = utils::mkNode(kind::EQUAL, utils::mkNode(kind::APPLY_UF, args), utils::mkConst(1, 1u)); - Debug("bv-abstraction") << "=> "<< result << "\n"; - Assert (result.getType() == assertion.getType()); - return result; + Debug("bv-abstraction") << "=> "<< result << "\n"; + Assert (result.getType() == assertion.getType()); + return result; } - return assertion; + return assertion; } bool AbstractionModule::isAbstraction(TNode node) { @@ -557,11 +557,11 @@ bool AbstractionModule::isAbstraction(TNode node) { if (constant != utils::mkConst(1, 1u)) return false; - TNode func_symbol = func.getOperator(); + TNode func_symbol = func.getOperator(); if (d_funcToSignature.find(func_symbol) == d_funcToSignature.end()) return false; - return true; + return true; } Node AbstractionModule::getInterpretation(TNode node) { @@ -571,51 +571,51 @@ Node AbstractionModule::getInterpretation(TNode node) { Assert (constant.getKind() == kind::CONST_BITVECTOR && apply.getKind() == kind::APPLY_UF); - Node func = apply.getOperator(); + Node func = apply.getOperator(); Assert (d_funcToSignature.find(func) != d_funcToSignature.end()); - + Node sig = d_funcToSignature[func]; - + // substitute arguments in signature TNodeTNodeMap seen; unsigned index = 0; Node result = substituteArguments(sig, apply, index, seen); - Assert (result.getType().isBoolean()); + Assert (result.getType().isBoolean()); Assert (index == apply.getNumChildren()); // Debug("bv-abstraction") << "AbstractionModule::getInterpretation " << node << "\n"; // Debug("bv-abstraction") << " => " << result << "\n"; - return result; + return result; } Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsigned& index, TNodeTNodeMap& seen) { if (seen.find(signature) != seen.end()) { - return seen[signature]; + return seen[signature]; } - + if (signature.getKind() == kind::SKOLEM) { // return corresponding argument and increment counter seen[signature] = apply[index]; - return apply[index++]; + return apply[index++]; } if (signature.getNumChildren() == 0) { Assert (signature.getKind() != kind::VARIABLE && - signature.getKind() != kind::SKOLEM); + signature.getKind() != kind::SKOLEM); seen[signature] = signature; - return signature; + return signature; } - + NodeBuilder<> builder(signature.getKind()); if (signature.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << signature.getOperator(); } - + for (unsigned i = 0; i < signature.getNumChildren(); ++i) { Node child = substituteArguments(signature[i], apply, index, seen); - builder << child; + builder << child; } - Node result = builder; + Node result = builder; seen[signature]= result; return result; @@ -625,20 +625,20 @@ Node AbstractionModule::simplifyConflict(TNode conflict) { if (Dump.isOn("bv-abstraction")) { NodeNodeMap seen; Node c = reverseAbstraction(conflict, seen); - Dump("bv-abstraction") << PushCommand(); + Dump("bv-abstraction") << PushCommand(); Dump("bv-abstraction") << AssertCommand(c.toExpr()); Dump("bv-abstraction") << CheckSatCommand(); - Dump("bv-abstraction") << PopCommand(); + Dump("bv-abstraction") << PopCommand(); } - Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n"; + Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n"; if (conflict.getKind() != kind::AND) - return conflict; + return conflict; std::vector conjuncts; for (unsigned i = 0; i < conflict.getNumChildren(); ++i) conjuncts.push_back(conflict[i]); - + theory::SubstitutionMap subst(new context::Context()); for (unsigned i = 0; i < conjuncts.size(); ++i) { TNode conjunct = conjuncts[i]; @@ -658,12 +658,12 @@ Node AbstractionModule::simplifyConflict(TNode conflict) { } else { continue; } - + Assert (!subst.hasSubstitution(s)); Assert (!t.isNull() && !s.isNull() && s!= t); - subst.addSubstitution(s, t); + subst.addSubstitution(s, t); for (unsigned k = 0; k < conjuncts.size(); k++) { conjuncts[k] = subst.apply(conjuncts[k]); @@ -671,28 +671,28 @@ Node AbstractionModule::simplifyConflict(TNode conflict) { } } Node new_conflict = Rewriter::rewrite(utils::mkAnd(conjuncts)); - + Debug("bv-abstraction") << "AbstractionModule::simplifyConflict conflict " << conflict <<"\n"; Debug("bv-abstraction") << " => " << new_conflict <<"\n"; if (Dump.isOn("bv-abstraction")) { - + NodeNodeMap seen; Node nc = reverseAbstraction(new_conflict, seen); - Dump("bv-abstraction") << PushCommand(); + Dump("bv-abstraction") << PushCommand(); Dump("bv-abstraction") << AssertCommand(nc.toExpr()); Dump("bv-abstraction") << CheckSatCommand(); - Dump("bv-abstraction") << PopCommand(); + Dump("bv-abstraction") << PopCommand(); } - - return new_conflict; + + return new_conflict; } void DebugPrintInstantiations(const std::vector< std::vector >& instantiations, const std::vector functions) { // print header - Debug("bv-abstraction-dbg") <<"[ "; + Debug("bv-abstraction-dbg") <<"[ "; for (unsigned i = 0; i < functions.size(); ++i) { for (unsigned j = 1; j < functions[i].getNumChildren(); ++j) { Debug("bv-abstraction-dgb") << functions[i][j] <<" "; @@ -706,16 +706,16 @@ void DebugPrintInstantiations(const std::vector< std::vector >& instant const std::vector& inst = instantiations[i]; for (unsigned j = 0; j < inst.size(); ++j) { for (unsigned k = 0; k < inst[j].size(); ++k) { - Debug("bv-abstraction-dbg") << inst[j][k] << " "; + Debug("bv-abstraction-dbg") << inst[j][k] << " "; } - Debug("bv-abstraction-dbg") << " || "; + Debug("bv-abstraction-dbg") << " || "; } Debug("bv-abstraction-dbg") <<"]\n"; } } void AbstractionModule::generalizeConflict(TNode conflict, std::vector& lemmas) { - Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n"; + Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n"; std::vector functions; // collect abstract functions @@ -737,11 +737,11 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector& le // if (functions.size() >= 3) { // // dump conflict // NodeNodeMap seen; - // Node reversed = reverseAbstraction(conflict, seen); - // std::cout << "CONFLICT " << reversed << "\n"; + // Node reversed = reverseAbstraction(conflict, seen); + // std::cout << "CONFLICT " << reversed << "\n"; // } - + if (functions.size() == 0 || functions.size() > options::bvNumFunc()) { return; } @@ -751,31 +751,31 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector& le SubstitutionMap skolem_subst(new context::Context()); SubstitutionMap reverse_skolem(new context::Context()); makeFreshSkolems(conflict, skolem_subst, reverse_skolem); - + Node skolemized_conflict = skolem_subst.apply(conflict); for (unsigned i = 0; i < functions.size(); ++i) { functions[i] = skolem_subst.apply(functions[i]); } - conflict = skolem_subst.apply(conflict); + conflict = skolem_subst.apply(conflict); LemmaInstantiatior inst(functions, d_argsTable, conflict); std::vector new_lemmas; - inst.generateInstantiations(new_lemmas); + inst.generateInstantiations(new_lemmas); for (unsigned i = 0; i < new_lemmas.size(); ++i) { TNode lemma = reverse_skolem.apply(new_lemmas[i]); if (d_addedLemmas.find(lemma) == d_addedLemmas.end()) { lemmas.push_back(lemma); - Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n"; + Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n"; storeLemma(lemma); if (Dump.isOn("bv-abstraction")) { NodeNodeMap seen; Node l = reverseAbstraction(lemma, seen); - Dump("bv-abstraction") << PushCommand(); + Dump("bv-abstraction") << PushCommand(); Dump("bv-abstraction") << AssertCommand(l.toExpr()); Dump("bv-abstraction") << CheckSatCommand(); - Dump("bv-abstraction") << PopCommand(); + Dump("bv-abstraction") << PopCommand(); } } } @@ -787,18 +787,18 @@ int AbstractionModule::LemmaInstantiatior::next(int val, int index) { return -1; } -/** +/** * Assumes the stack without top is consistent, and checks that the * full stack is consistent - * - * @param stack - * - * @return + * + * @param stack + * + * @return */ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector& stack) { if (stack.empty()) return true; - + unsigned current = stack.size() - 1; TNode func = d_functions[current]; ArgsTableEntry& matches = d_argsTable.getEntry(func.getOperator()); @@ -807,12 +807,12 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector& stac for (unsigned k = 0; k < args.size(); ++k) { TNode s = func[k]; TNode t = args[k]; - + TNode s0 = s; while (d_subst.hasSubstitution(s0)) { s0 = d_subst.getSubstitution(s0); } - + TNode t0 = t; while (d_subst.hasSubstitution(t0)) { t0 = d_subst.getSubstitution(t0); @@ -824,7 +824,7 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector& stac else continue; } - + if(s0.getMetaKind() == kind::metakind::VARIABLE && t0.isConst()) { d_subst.addSubstitution(s0, t0); @@ -839,12 +839,12 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector& stac Assert (s0.getMetaKind() == kind::metakind::VARIABLE && t0.getMetaKind() == kind::metakind::VARIABLE); - + if (s0 != t0) { d_subst.addSubstitution(s0, t0); } } - return true; + return true; } bool AbstractionModule::LemmaInstantiatior::accept(const vector& stack) { @@ -854,13 +854,13 @@ bool AbstractionModule::LemmaInstantiatior::accept(const vector& stack) { void AbstractionModule::LemmaInstantiatior::mkLemma() { Node lemma = d_subst.apply(d_conflict); // Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::mkLemma " << lemma <<"\n"; - d_lemmas.push_back(lemma); + d_lemmas.push_back(lemma); } void AbstractionModule::LemmaInstantiatior::backtrack(vector& stack) { if (!isConsistent(stack)) return; - + if (accept(stack)) { mkLemma(); return; @@ -871,7 +871,7 @@ void AbstractionModule::LemmaInstantiatior::backtrack(vector& stack) { d_ctx->push(); stack.push_back(x); backtrack(stack); - + d_ctx->pop(); stack.pop_back(); x = next(x, stack.size()); @@ -880,13 +880,13 @@ void AbstractionModule::LemmaInstantiatior::backtrack(vector& stack) { void AbstractionModule::LemmaInstantiatior::generateInstantiations(std::vector& lemmas) { - Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations "; + Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations "; std::vector stack; backtrack(stack); - Assert (d_ctx->getLevel() == 0); - Debug("bv-abstraction-gen") << "numLemmas=" << d_lemmas.size() <<"\n"; - lemmas.swap(d_lemmas); + Assert (d_ctx->getLevel() == 0); + Debug("bv-abstraction-gen") << "numLemmas=" << d_lemmas.size() <<"\n"; + lemmas.swap(d_lemmas); } void AbstractionModule::makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map) { @@ -910,7 +910,7 @@ void AbstractionModule::makeFreshSkolems(TNode node, SubstitutionMap& map, Subst void AbstractionModule::makeFreshArgs(TNode func, std::vector& fresh_args) { Assert (fresh_args.size() == 0); Assert (func.getKind() == kind::APPLY_UF); - TNodeNodeMap d_map; + TNodeNodeMap d_map; for (unsigned i = 0; i < func.getNumChildren(); ++i) { TNode arg = func[i]; if (arg.isConst()) { @@ -918,9 +918,9 @@ void AbstractionModule::makeFreshArgs(TNode func, std::vector& fresh_args) continue; } Assert (arg.getMetaKind() == kind::metakind::VARIABLE); - TNodeNodeMap::iterator it = d_map.find(arg); + TNodeNodeMap::iterator it = d_map.find(arg); if (it != d_map.end()) { - fresh_args.push_back(it->second); + fresh_args.push_back(it->second); } else { Node skolem = utils::mkVar(utils::getSize(arg)); d_map[arg] = skolem; @@ -947,7 +947,7 @@ Node AbstractionModule::tryMatching(const std::vector& ss, const std::vect Debug("bv-abstraction-dbg") <<"\n"; } - + SubstitutionMap subst(new context::Context()); for (unsigned i = 0; i < ss.size(); ++i) { @@ -982,10 +982,10 @@ Node AbstractionModule::tryMatching(const std::vector& ss, const std::vect Assert (s0 != t0); subst.addSubstitution(s0, t0); } - + Node res = subst.apply(conflict); - Debug("bv-abstraction-dbg") << " Lemma: " << res <<"\n"; - return res; + Debug("bv-abstraction-dbg") << " Lemma: " << res <<"\n"; + return res; } void AbstractionModule::storeLemma(TNode lemma) { @@ -996,7 +996,7 @@ void AbstractionModule::storeLemma(TNode lemma) { atom = atom.getKind() == kind::NOT ? atom[0] : atom; Assert (atom.getKind() != kind::NOT); Assert (utils::isBVPredicate(atom)); - d_lemmaAtoms.insert(atom); + d_lemmaAtoms.insert(atom); } } else { lemma = lemma.getKind() == kind::NOT? lemma[0] : lemma; @@ -1009,9 +1009,9 @@ void AbstractionModule::storeLemma(TNode lemma) { bool AbstractionModule::isLemmaAtom(TNode node) const { Assert (node.getType().isBoolean()); node = node.getKind() == kind::NOT? node[0] : node; - + return d_inputAtoms.find(node) == d_inputAtoms.end() && - d_lemmaAtoms.find(node) != d_lemmaAtoms.end(); + d_lemmaAtoms.find(node) != d_lemmaAtoms.end(); } void AbstractionModule::addInputAtom(TNode atom) { @@ -1022,31 +1022,31 @@ void AbstractionModule::addInputAtom(TNode atom) { void AbstractionModule::ArgsTableEntry::addArguments(const ArgsVec& args) { Assert (args.size() == d_arity); - d_data.push_back(args); + d_data.push_back(args); } void AbstractionModule::ArgsTable::addEntry(TNode signature, const ArgsVec& args) { if (d_data.find(signature) == d_data.end()) { - d_data[signature] = ArgsTableEntry(args.size()); + d_data[signature] = ArgsTableEntry(args.size()); } ArgsTableEntry& entry = d_data[signature]; - entry.addArguments(args); + entry.addArguments(args); } bool AbstractionModule::ArgsTable::hasEntry(TNode signature) const { - return d_data.find(signature) != d_data.end(); + return d_data.find(signature) != d_data.end(); } AbstractionModule::ArgsTableEntry& AbstractionModule::ArgsTable::getEntry(TNode signature) { Assert (hasEntry(signature)); - return d_data.find(signature)->second; + return d_data.find(signature)->second; } -AbstractionModule::Statistics::Statistics() - : d_numFunctionsAbstracted("theory::bv::AbstractioModule::NumFunctionsAbstracted", 0) - , d_numArgsSkolemized("theory::bv::AbstractioModule::NumArgsSkolemized", 0) - , d_abstractionTime("theory::bv::AbstractioModule::AbstractionTime") +AbstractionModule::Statistics::Statistics(const std::string& name) + : d_numFunctionsAbstracted(name + "theory::bv::AbstractioModule::NumFunctionsAbstracted", 0) + , d_numArgsSkolemized(name + "theory::bv::AbstractioModule::NumArgsSkolemized", 0) + , d_abstractionTime(name + "theory::bv::AbstractioModule::AbstractionTime") { smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted); smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized); diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index 5d580f6ce..5d48b926e 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -38,11 +38,11 @@ class AbstractionModule { IntStat d_numFunctionsAbstracted; IntStat d_numArgsSkolemized; TimerStat d_abstractionTime; - Statistics(); + Statistics(const std::string& name); ~Statistics(); }; - + class ArgsTableEntry { std::vector d_data; unsigned d_arity; @@ -61,11 +61,11 @@ class AbstractionModule { unsigned getArity() { return d_arity; } unsigned getNumEntries() { return d_data.size(); } ArgsVec& getEntry(unsigned i ) { Assert (i < d_data.size()); return d_data[i]; } - }; + }; class ArgsTable { __gnu_cxx::hash_map d_data; - bool hasEntry(TNode signature) const; + bool hasEntry(TNode signature) const; public: typedef __gnu_cxx::hash_map::iterator iterator; ArgsTable() {} @@ -75,12 +75,12 @@ class AbstractionModule { iterator end() { return d_data.end(); } }; - /** + /** * Checks if one pattern is a generalization of the other - * - * @param s - * @param t - * + * + * @param s + * @param t + * * @return 1 if s :> t, 2 if s <: t, 0 if they equivalent and -1 if they are incomparable */ static int comparePatterns(TNode s, TNode t); @@ -93,7 +93,7 @@ class AbstractionModule { theory::SubstitutionMap d_subst; TNode d_conflict; std::vector d_lemmas; - + void backtrack(std::vector& stack); int next(int val, int index); bool isConsistent(const std::vector& stack); @@ -108,7 +108,7 @@ class AbstractionModule { , d_conflict(conflict) , d_lemmas() { - Debug("bv-abstraction-gen") << "LemmaInstantiator conflict:" << conflict << "\n"; + Debug("bv-abstraction-gen") << "LemmaInstantiator conflict:" << conflict << "\n"; // initializing the search space for (unsigned i = 0; i < functions.size(); ++i) { TNode func_op = functions[i].getOperator(); @@ -118,31 +118,31 @@ class AbstractionModule { } } - void generateInstantiations(std::vector& lemmas); - + void generateInstantiations(std::vector& lemmas); + }; - + typedef __gnu_cxx::hash_map, NodeHashFunction> NodeVecMap; typedef __gnu_cxx::hash_map NodeTNodeMap; typedef __gnu_cxx::hash_map TNodeTNodeMap; typedef __gnu_cxx::hash_map NodeNodeMap; typedef __gnu_cxx::hash_map TNodeNodeMap; typedef __gnu_cxx::hash_set TNodeSet; - typedef __gnu_cxx::hash_map IntNodeMap; + typedef __gnu_cxx::hash_map IntNodeMap; typedef __gnu_cxx::hash_map IndexMap; typedef __gnu_cxx::hash_map > SkolemMap; typedef __gnu_cxx::hash_map SignatureMap; - - ArgsTable d_argsTable; + + ArgsTable d_argsTable; // mapping between signature and uninterpreted function symbol used to // abstract the signature NodeNodeMap d_signatureToFunc; - NodeNodeMap d_funcToSignature; + NodeNodeMap d_funcToSignature; - NodeNodeMap d_assertionToSignature; + NodeNodeMap d_assertionToSignature; SignatureMap d_signatures; - NodeNodeMap d_sigToGeneralization; + NodeNodeMap d_sigToGeneralization; TNodeSet d_skolems; // skolems maps @@ -165,7 +165,7 @@ class AbstractionModule { Node getGeneralizedSignature(Node node); Node getSignatureSkolem(TNode node); - unsigned getBitwidthIndex(unsigned bitwidth); + unsigned getBitwidthIndex(unsigned bitwidth); void resetSignatureIndex(); Node computeSignatureRec(TNode, NodeNodeMap&); void storeSignature(Node signature, TNode assertion); @@ -175,14 +175,14 @@ class AbstractionModule { // crazy instantiation methods void generateInstantiations(unsigned current, - std::vector& matches, + std::vector& matches, std::vector >& instantiations, std::vector >& new_instantiations); Node tryMatching(const std::vector& ss, const std::vector& tt, TNode conflict); void makeFreshArgs(TNode func, std::vector& fresh_args); void makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map); - + void skolemizeArguments(std::vector& assertions); Node reverseAbstraction(Node assertion, NodeNodeMap& seen); @@ -192,9 +192,9 @@ class AbstractionModule { void storeLemma(TNode lemma); Statistics d_statistics; - + public: - AbstractionModule() + AbstractionModule(const std::string& name) : d_argsTable() , d_signatureToFunc() , d_funcToSignature() @@ -207,34 +207,34 @@ public: , d_addedLemmas() , d_lemmaAtoms() , d_inputAtoms() - , d_statistics() + , d_statistics(name) {} - /** + /** * returns true if there are new uninterepreted functions symbols in the output - * - * @param assertions - * @param new_assertions - * - * @return + * + * @param assertions + * @param new_assertions + * + * @return */ bool applyAbstraction(const std::vector& assertions, std::vector& new_assertions); - /** - * Returns true if the node represents an abstraction predicate. - * - * @param node - * - * @return + /** + * Returns true if the node represents an abstraction predicate. + * + * @param node + * + * @return */ bool isAbstraction(TNode node); - /** - * Returns the interpretation of the abstraction predicate. - * - * @param node - * - * @return + /** + * Returns the interpretation of the abstraction predicate. + * + * @param node + * + * @return */ Node getInterpretation(TNode node); - Node simplifyConflict(TNode conflict); + Node simplifyConflict(TNode conflict); void generalizeConflict(TNode conflict, std::vector& lemmas); void addInputAtom(TNode atom); bool isLemmaAtom(TNode node) const; diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index b7619c4bb..6c6c13ee8 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -37,9 +37,9 @@ namespace bv { BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv) : SubtheorySolver(c, bv), - d_bitblaster(new TLazyBitblaster(c, bv, "lazy")), + d_bitblaster(new TLazyBitblaster(c, bv, bv->getFullInstanceName() + "lazy")), d_bitblastQueue(c), - d_statistics(), + d_statistics(bv->getFullInstanceName()), d_validModelCache(c, true), d_lemmaAtomsQueue(c), d_useSatPropagation(options::bitvectorPropagate()), @@ -55,9 +55,9 @@ BitblastSolver::~BitblastSolver() { delete d_bitblaster; } -BitblastSolver::Statistics::Statistics() - : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0) - , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0) +BitblastSolver::Statistics::Statistics(const std::string &instanceName) + : d_numCallstoCheck(instanceName + "theory::bv::BitblastSolver::NumCallsToCheck", 0) + , d_numBBLemmas(instanceName + "theory::bv::BitblastSolver::NumTimesLemmasBB", 0) { smtStatisticsRegistry()->registerStat(&d_numCallstoCheck); smtStatisticsRegistry()->registerStat(&d_numBBLemmas); @@ -68,8 +68,8 @@ BitblastSolver::Statistics::~Statistics() { } void BitblastSolver::setAbstraction(AbstractionModule* abs) { - d_abstractionModule = abs; - d_bitblaster->setAbstraction(abs); + d_abstractionModule = abs; + d_bitblaster->setAbstraction(abs); } void BitblastSolver::preRegister(TNode node) { @@ -117,7 +117,7 @@ void BitblastSolver::bitblastQueue() { bool BitblastSolver::check(Theory::Effort e) { Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; - Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); + Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); ++(d_statistics.d_numCallstoCheck); @@ -135,10 +135,10 @@ bool BitblastSolver::check(Theory::Effort e) { // skip atoms that are the result of abstraction lemmas if (d_abstractionModule->isLemmaAtom(fact)) { d_lemmaAtomsQueue.push_back(fact); - continue; + continue; } } - + if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) { // Some atoms have not been bit-blasted yet @@ -183,7 +183,7 @@ bool BitblastSolver::check(Theory::Effort e) { if (options::bvAbstraction() && e == Theory::EFFORT_FULL && d_lemmaAtomsQueue.size()) { - + // bit-blast lemma atoms while(!d_lemmaAtomsQueue.empty()) { TNode lemma_atom = d_lemmaAtomsQueue.front(); @@ -199,7 +199,7 @@ bool BitblastSolver::check(Theory::Effort e) { return false; } } - + Assert(!d_bv->inConflict()); bool ok = d_bitblaster->solve(); if (!ok) { @@ -210,9 +210,9 @@ bool BitblastSolver::check(Theory::Effort e) { ++(d_statistics.d_numBBLemmas); return false; } - + } - + return true; } @@ -228,9 +228,9 @@ void BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) { Node BitblastSolver::getModelValue(TNode node) { if (d_bv->d_invalidateModelCache.get()) { - d_bitblaster->invalidateModelCache(); + d_bitblaster->invalidateModelCache(); } - d_bv->d_invalidateModelCache.set(false); + d_bv->d_invalidateModelCache.set(false); Node val = d_bitblaster->getTermModel(node, true); return val; } @@ -241,9 +241,9 @@ void BitblastSolver::setConflict(TNode conflict) { Node final_conflict = conflict; if (options::bitvectorQuickXplain() && conflict.getKind() == kind::AND) { - // std::cout << "Original conflict " << conflict.getNumChildren() << "\n"; + // std::cout << "Original conflict " << conflict.getNumChildren() << "\n"; final_conflict = d_quickXplain->minimizeConflict(conflict); - //std::cout << "Minimized conflict " << final_conflict.getNumChildren() << "\n"; + //std::cout << "Minimized conflict " << final_conflict.getNumChildren() << "\n"; } d_bv->setConflict(final_conflict); } @@ -256,4 +256,3 @@ void BitblastSolver::setProofLog( BitVectorProof * bvp ) { }/* namespace CVC4::theory::bv */ }/* namespace CVC4::theory */ }/* namespace CVC4 */ - diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index e9300138b..fe16d2702 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -37,7 +37,7 @@ class BitblastSolver : public SubtheorySolver { struct Statistics { IntStat d_numCallstoCheck; IntStat d_numBBLemmas; - Statistics(); + Statistics(const std::string &instanceName); ~Statistics(); }; /** Bitblaster */ @@ -71,8 +71,8 @@ public: Node getModelValue(TNode node); bool isComplete() { return true; } void bitblastQueue(); - void setAbstraction(AbstractionModule* module); - uint64_t computeAtomWeight(TNode atom); + void setAbstraction(AbstractionModule* module); + uint64_t computeAtomWeight(TNode atom); void setProofLog( BitVectorProof * bvp ); }; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index f5b2175f3..fec93e033 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -42,14 +42,16 @@ namespace CVC4 { namespace theory { namespace bv { -TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) - : Theory(THEORY_BV, c, u, out, valuation, logicInfo), +TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, std::string name) + : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name), d_context(c), d_alreadyPropagatedSet(c), d_sharedTermsSet(c), d_subtheories(), d_subtheoryMap(), - d_statistics(), + d_statistics(getFullInstanceName()), d_staticLearnCache(), d_BVDivByZero(), d_BVRemByZero(), @@ -62,7 +64,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_literalsToPropagateIndex(c, 0), d_propagatedBy(c), d_eagerSolver(NULL), - d_abstractionModule(new AbstractionModule()), + d_abstractionModule(new AbstractionModule(getFullInstanceName())), d_isCoreTheory(false), d_calledPreregister(false) { @@ -119,14 +121,14 @@ void TheoryBV::spendResource(unsigned ammount) throw(UnsafeInterruptException) { getOutputChannel().spendResource(ammount); } -TheoryBV::Statistics::Statistics(): - d_avgConflictSize("theory::bv::AvgBVConflictSize"), - d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0), - d_solveTimer("theory::bv::solveTimer"), - d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0), - d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0), - d_weightComputationTimer("theory::bv::weightComputationTimer"), - d_numMultSlice("theory::bv::NumMultSliceApplied", 0) +TheoryBV::Statistics::Statistics(const std::string &name): + d_avgConflictSize(name + "theory::bv::AvgBVConflictSize"), + d_solveSubstitutions(name + "theory::bv::NumberOfSolveSubstitutions", 0), + d_solveTimer(name + "theory::bv::solveTimer"), + d_numCallsToCheckFullEffort(name + "theory::bv::NumberOfFullCheckCalls", 0), + d_numCallsToCheckStandardEffort(name + "theory::bv::NumberOfStandardCheckCalls", 0), + d_weightComputationTimer(name + "theory::bv::weightComputationTimer"), + d_numMultSlice(name + "theory::bv::NumMultSliceApplied", 0) { smtStatisticsRegistry()->registerStat(&d_avgConflictSize); smtStatisticsRegistry()->registerStat(&d_solveSubstitutions); @@ -234,7 +236,7 @@ void TheoryBV::mkAckermanizationAsssertions(std::vector& assertions) { for (unsigned i = 0; i < args1.getNumChildren(); ++i) { eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]); } - + Node args_eq = eqs.size() == 1 ? eqs[0] : nm->mkNode(kind::AND, eqs); Node func_eq = nm->mkNode(kind::EQUAL, args1, args2); Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq); @@ -276,9 +278,9 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { // if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { // // Ackermanize UF if using eager bit-blasting - // Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num); + // Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num); // node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen); - // return node; + // return node; // } else { Node divByZero = getBVDivByZero(node.getKind(), width); Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num); @@ -327,7 +329,7 @@ void TheoryBV::sendConflict() { if (d_conflictNode.isNull()) { return; } else { - Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode; + Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode << std::endl; d_out->conflict(d_conflictNode); d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren()); d_conflictNode = Node::null(); @@ -703,7 +705,7 @@ Node TheoryBV::explain(TNode node) { // return the explanation Node explanation = utils::mkAnd(assumptions); Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl; - Debug("bitvector::explain") << "TheoryBV::explain done. \n"; + Debug("bitvector::explain") << "TheoryBV::explain done. \n"; return explanation; } @@ -723,7 +725,7 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) return EQUALITY_UNKNOWN; - Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); + Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); for (unsigned i = 0; i < d_subtheories.size(); ++i) { EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b); if (status != EQUALITY_UNKNOWN) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 7f0494dc1..ba2a4fc2a 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -56,7 +56,8 @@ class TheoryBV : public Theory { public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo); + Valuation valuation, const LogicInfo& logicInfo, + std::string name = ""); ~TheoryBV(); @@ -88,8 +89,8 @@ public: void presolve(); - bool applyAbstraction(const std::vector& assertions, std::vector& new_assertions); - + bool applyAbstraction(const std::vector& assertions, std::vector& new_assertions); + void setProofLog( BitVectorProof * bvp ); private: @@ -100,10 +101,10 @@ private: IntStat d_solveSubstitutions; TimerStat d_solveTimer; IntStat d_numCallsToCheckFullEffort; - IntStat d_numCallsToCheckStandardEffort; + IntStat d_numCallsToCheckStandardEffort; TimerStat d_weightComputationTimer; IntStat d_numMultSlice; - Statistics(); + Statistics(const std::string &name); ~Statistics(); }; @@ -121,12 +122,12 @@ private: */ Node getBVDivByZero(Kind k, unsigned width); - typedef __gnu_cxx::hash_set TNodeSet; + typedef __gnu_cxx::hash_set TNodeSet; void collectFunctionSymbols(TNode term, TNodeSet& seen); void storeFunction(TNode func, TNode term); typedef __gnu_cxx::hash_set NodeSet; NodeSet d_staticLearnCache; - + /** * Maps from bit-vector width to division-by-zero uninterpreted * function symbols. @@ -142,7 +143,7 @@ private: CVC4::theory::SubstitutionMap d_funcToSkolem; context::CDO d_lemmasAdded; - + // Are we in conflict? context::CDO d_conflict; @@ -165,17 +166,17 @@ private: typedef context::CDHashMap PropagatedMap; PropagatedMap d_propagatedBy; - EagerBitblastSolver* d_eagerSolver; + EagerBitblastSolver* d_eagerSolver; AbstractionModule* d_abstractionModule; bool d_isCoreTheory; bool d_calledPreregister; - + bool wasPropagatedBySubtheory(TNode literal) const { - return d_propagatedBy.find(literal) != d_propagatedBy.end(); + return d_propagatedBy.find(literal) != d_propagatedBy.end(); } - + SubTheory getPropagatingSubtheory(TNode literal) const { - Assert(wasPropagatedBySubtheory(literal)); + Assert(wasPropagatedBySubtheory(literal)); PropagatedMap::const_iterator find = d_propagatedBy.find(literal); return (*find).second; } @@ -191,7 +192,7 @@ private: void addSharedTerm(TNode t); bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); } - + EqualityStatus getEqualityStatus(TNode a, TNode b); Node getModelValue(TNode var); @@ -212,7 +213,7 @@ private: void lemma(TNode node) { d_out->lemma(node, RULE_CONFLICT); d_lemmasAdded = true; } - void checkForLemma(TNode node); + void checkForLemma(TNode node); friend class LazyBitblaster; friend class TLazyBitblaster; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 1ab4c228b..618fda4c0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -26,6 +26,8 @@ #include "options/bv_options.h" #include "options/options.h" #include "options/quantifiers_options.h" +#include "proof/cnf_proof.h" +#include "proof/lemma_proof.h" #include "proof/proof_manager.h" #include "proof/theory_proof.h" #include "smt/ite_removal.h" @@ -53,6 +55,104 @@ using namespace CVC4::theory; namespace CVC4 { +inline void flattenAnd(Node n, std::vector& out){ + Assert(n.getKind() == kind::AND); + for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){ + Node curr = *i; + if(curr.getKind() == kind::AND){ + flattenAnd(curr, out); + }else{ + out.push_back(curr); + } + } +} + +inline Node flattenAnd(Node n){ + std::vector out; + flattenAnd(n, out); + return NodeManager::currentNM()->mkNode(kind::AND, out); +} + +theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma, + ProofRule rule, + bool removable, + bool preprocess, + bool sendAtoms) + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { + Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << ", preprocess = " << preprocess << std::endl; + ++ d_statistics.lemmas; + d_engine->d_outputChannelUsed = true; + + LemmaProofRecipe* proofRecipe = NULL; + PROOF({ + // Theory lemmas have one step that proves the empty clause + proofRecipe = new LemmaProofRecipe; + + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(d_theory, emptyNode); + + Node rewritten; + if (lemma.getKind() == kind::OR) { + for (unsigned i = 0; i < lemma.getNumChildren(); ++i) { + rewritten = theory::Rewriter::rewrite(lemma[i]); + if (rewritten != lemma[i]) { + proofRecipe->addRewriteRule(lemma[i].negate(), rewritten.negate()); + } + proofStep.addAssertion(lemma[i]); + proofRecipe->addBaseAssertion(rewritten); + } + } else { + rewritten = theory::Rewriter::rewrite(lemma); + if (rewritten != lemma) { + proofRecipe->addRewriteRule(lemma.negate(), rewritten.negate()); + } + proofStep.addAssertion(lemma); + proofRecipe->addBaseAssertion(rewritten); + } + proofRecipe->addStep(proofStep); + }); + + theory::LemmaStatus result = d_engine->lemma(lemma, + rule, + false, + removable, + preprocess, + sendAtoms ? d_theory : theory::THEORY_LAST, + proofRecipe); + PROOF(delete proofRecipe;); + return result; +} + +theory::LemmaStatus TheoryEngine::EngineOutputChannel::splitLemma(TNode lemma, bool removable) + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { + Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; + ++ d_statistics.lemmas; + d_engine->d_outputChannelUsed = true; + + + LemmaProofRecipe* proofRecipe = NULL; + Debug("pf::explain") << "TheoryEngine::EngineOutputChannel::splitLemma( " << lemma << " )" << std::endl; + theory::LemmaStatus result = d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, proofRecipe); + return result; +} + +bool TheoryEngine::EngineOutputChannel::propagate(TNode literal) + throw(AssertionException, UnsafeInterruptException) { + Debug("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; + ++ d_statistics.propagations; + d_engine->d_outputChannelUsed = true; + return d_engine->propagate(literal, d_theory); +} + +void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf) + throw(AssertionException, UnsafeInterruptException) { + Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; + Assert (pf == NULL); // Theory shouldn't be producing proofs yet + ++ d_statistics.conflicts; + d_engine->d_outputChannelUsed = true; + d_engine->conflict(conflictNode, d_theory); +} + void TheoryEngine::finishInit() { // initialize the quantifiers engine d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); @@ -497,7 +597,10 @@ void TheoryEngine::combineTheories() { // We need to split on it Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; - lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, carePair.theory); + + LemmaProofRecipe* proofRecipe = NULL; + lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, proofRecipe); + // This code is supposed to force preference to follow what the theory models already have // but it doesn't seem to make a big difference - need to explore more -Clark // if (true) { @@ -963,7 +1066,7 @@ bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, the void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) { - Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << endl; + Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")" << endl; Assert(toTheoryId != fromTheoryId); if(toTheoryId != THEORY_SAT_SOLVER && @@ -1176,6 +1279,23 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory); } } else { + // We could be propagating a unit-clause lemma. In this case, we need to provide a + // recipe. + // TODO: Consider putting this someplace else? This is the only refence to the proof + // manager in this class. + + PROOF({ + LemmaProofRecipe proofRecipe; + proofRecipe.addBaseAssertion(literal); + + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(theory, emptyNode); + proofStep.addAssertion(literal); + proofRecipe.addStep(proofStep); + + ProofManager::getCnfProof()->setProofRecipe(&proofRecipe); + }); + // Just send off to the SAT solver Assert(d_propEngine->isSatLiteral(literal)); assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory); @@ -1270,7 +1390,7 @@ static Node mkExplanation(const std::vector& explanation) { return conjunction; } -NodeTheoryPair TheoryEngine::getExplanationAndExplainer(TNode node) { +Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe) { Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl; bool polarity = node.getKind() != kind::NOT; @@ -1278,32 +1398,90 @@ NodeTheoryPair TheoryEngine::getExplanationAndExplainer(TNode node) { // If we're not in shared mode, explanations are simple if (!d_logicInfo.isSharingEnabled()) { + Debug("theory::explain") << "TheoryEngine::getExplanation: sharing is NOT enabled. " + << " Responsible theory is: " + << theoryOf(atom)->getId() << std::endl; + Node explanation = theoryOf(atom)->explain(node); Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl; - return NodeTheoryPair(explanation, theoryOf(atom)->getId()); + PROOF({ + if(proofRecipe) { + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(theoryOf(atom)->getId(), emptyNode); + proofStep.addAssertion(node); + proofRecipe->addBaseAssertion(node); + + if (explanation.getKind() == kind::AND) { + // If the explanation is a conjunction, the recipe for the corresponding lemma is + // the negation of its conjuncts. + Node flat = flattenAnd(explanation); + for (unsigned i = 0; i < flat.getNumChildren(); ++i) { + if (flat[i].isConst() && flat[i].getConst()) { + ++ i; + continue; + } + if (flat[i].getKind() == kind::NOT && + flat[i][0].isConst() && !flat[i][0].getConst()) { + ++ i; + continue; + } + Debug("theory::explain") << "TheoryEngine::getExplanationAndRecipe: adding recipe assertion: " + << flat[i].negate() << std::endl; + proofStep.addAssertion(flat[i].negate()); + proofRecipe->addBaseAssertion(flat[i].negate()); + } + } else { + // The recipe for proving it is by negating it. "True" is not an acceptable reason. + if (!((explanation.isConst() && explanation.getConst()) || + (explanation.getKind() == kind::NOT && + explanation[0].isConst() && !explanation[0].getConst()))) { + proofStep.addAssertion(explanation.negate()); + proofRecipe->addBaseAssertion(explanation.negate()); + } + } + + proofRecipe->addStep(proofStep); + } + }); + + return explanation; } + Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl; + // Initial thing to explain NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp); Assert(d_propagationMap.find(toExplain) != d_propagationMap.end()); NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain]; + Debug("theory::explain") << "TheoryEngine::getExplanation: explainer for node " + << nodeExplainerPair.node + << " is theory: " << nodeExplainerPair.theory << std::endl; TheoryId explainer = nodeExplainerPair.theory; // Create the workplace for explanations std::vector explanationVector; explanationVector.push_back(d_propagationMap[toExplain]); // Process the explanation - getExplanation(explanationVector); + if (proofRecipe) { + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(explainer, emptyNode); + proofStep.addAssertion(node); + proofRecipe->addStep(proofStep); + proofRecipe->addBaseAssertion(node); + } + + getExplanation(explanationVector, proofRecipe); Node explanation = mkExplanation(explanationVector); Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl; - return NodeTheoryPair(explanation, explainer); + return explanation; } Node TheoryEngine::getExplanation(TNode node) { - return getExplanationAndExplainer(node).node; + LemmaProofRecipe *dontCareRecipe = NULL; + return getExplanationAndRecipe(node, dontCareRecipe); } struct AtomsCollect { @@ -1406,7 +1584,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool removable, bool preprocess, theory::TheoryId atomsTo, - theory::TheoryId ownerTheory) { + LemmaProofRecipe* proofRecipe) { // For resource-limiting (also does a time check). // spendResource(); @@ -1456,10 +1634,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, } // assert to prop engine - d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, ownerTheory, node); + d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, proofRecipe, node); for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); - d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, ownerTheory, node); + d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, proofRecipe, node); } // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. @@ -1493,22 +1671,69 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { << CheckSatCommand(conflict.toExpr()); } + LemmaProofRecipe* proofRecipe = NULL; + PROOF({ + proofRecipe = new LemmaProofRecipe; + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode); + + if (conflict.getKind() == kind::AND) { + for (unsigned i = 0; i < conflict.getNumChildren(); ++i) { + proofStep.addAssertion(conflict[i].negate()); + } + } else { + proofStep.addAssertion(conflict.negate()); + } + + proofRecipe->addStep(proofStep); + }); + // In the multiple-theories case, we need to reconstruct the conflict if (d_logicInfo.isSharingEnabled()) { // Create the workplace for explanations std::vector explanationVector; explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp)); + // Process the explanation - getExplanation(explanationVector); + getExplanation(explanationVector, proofRecipe); Node fullConflict = mkExplanation(explanationVector); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; Assert(properConflict(fullConflict)); - lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId); + lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe); + } else { // When only one theory, the conflict should need no processing Assert(properConflict(conflict)); - lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId); + PROOF({ + if (conflict.getKind() == kind::AND) { + // If the conflict is a conjunction, the corresponding lemma is derived by negating + // its conjuncts. + for (unsigned i = 0; i < conflict.getNumChildren(); ++i) { + if (conflict[i].isConst() && conflict[i].getConst()) { + ++ i; + continue; + } + if (conflict[i].getKind() == kind::NOT && + conflict[i][0].isConst() && !conflict[i][0].getConst()) { + ++ i; + continue; + } + proofRecipe->getStep(0)->addAssertion(conflict[i].negate()); + proofRecipe->addBaseAssertion(conflict[i].negate()); + } + } else { + proofRecipe->getStep(0)->addAssertion(conflict.negate()); + proofRecipe->addBaseAssertion(conflict.negate()); + } + }); + + lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe); } + + PROOF({ + delete proofRecipe; + proofRecipe = NULL; + }); } void TheoryEngine::staticInitializeBVOptions(const std::vector& assertions) { @@ -1660,19 +1885,21 @@ bool TheoryEngine::donePPSimpITE(std::vector& assertions){ return result; } -void TheoryEngine::getExplanation(std::vector& explanationVector) -{ +void TheoryEngine::getExplanation(std::vector& explanationVector, LemmaProofRecipe* proofRecipe) { Assert(explanationVector.size() > 0); unsigned i = 0; // Index of the current literal we are processing unsigned j = 0; // Index of the last literal we are keeping - while (i < explanationVector.size()) { + std::set inputAssertions; + PROOF(inputAssertions = proofRecipe->getStep(0)->getAssertions();); + while (i < explanationVector.size()) { // Get the current literal to explain NodeTheoryPair toExplain = explanationVector[i]; - Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl; + Debug("theory::explain") << "[i=" << i << "] TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl; + // If a true constant or a negation of a false constant we can ignore it if (toExplain.node.isConst() && toExplain.node.getConst()) { @@ -1686,6 +1913,7 @@ void TheoryEngine::getExplanation(std::vector& explanationVector // If from the SAT solver, keep it if (toExplain.theory == THEORY_SAT_SOLVER) { + Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl; explanationVector[j++] = explanationVector[i++]; continue; } @@ -1704,10 +1932,26 @@ void TheoryEngine::getExplanation(std::vector& explanationVector // See if it was sent to the theory by another theory PropagationMap::const_iterator find = d_propagationMap.find(toExplain); if (find != d_propagationMap.end()) { + Debug("theory::explain") << "\tTerm was propagated by another theory (theory = " + << theoryOf((*find).second.theory)->getId() << ")" << std::endl; // There is some propagation, check if its a timely one if ((*find).second.timestamp < toExplain.timestamp) { + Debug("theory::explain") << "\tRelevant timetsamp, pushing " + << (*find).second.node << "to index = " << explanationVector.size() << std::endl; explanationVector.push_back((*find).second); - ++ i; + ++i; + + PROOF({ + if (toExplain.node != (*find).second.node) { + Debug("pf::explain") << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " << toExplain.node + << ", toExplain = " << (*find).second.node << std::endl; + + if (proofRecipe) { + proofRecipe->addRewriteRule(toExplain.node, (*find).second.node); + } + } + }) + continue; } } @@ -1716,21 +1960,61 @@ void TheoryEngine::getExplanation(std::vector& explanationVector Node explanation; if (toExplain.theory == THEORY_BUILTIN) { explanation = d_sharedTerms.explain(toExplain.node); + Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl; } else { explanation = theoryOf(toExplain.theory)->explain(toExplain.node); + Debug("theory::explain") << "\tTerm was propagated by owner theory: " + << theoryOf(toExplain.theory)->getId() + << ". Explanation: " << explanation << std::endl; } + Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl; Assert(explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially"); // Mark the explanation NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp); explanationVector.push_back(newExplain); + ++ i; + + PROOF({ + if (proofRecipe) { + // If we're expanding the target node of the explanation (this is the first expansion...), + // we don't want to add it as a separate proof step. It is already part of the assertions. + if (inputAssertions.find(toExplain.node) == inputAssertions.end()) { + LemmaProofRecipe::ProofStep proofStep(toExplain.theory, toExplain.node); + if (explanation.getKind() == kind::AND) { + Node flat = flattenAnd(explanation); + for (unsigned k = 0; k < flat.getNumChildren(); ++ k) { + // If a true constant or a negation of a false constant we can ignore it + if (! ((flat[k].isConst() && flat[k].getConst()) || + (flat[k].getKind() == kind::NOT && flat[k][0].isConst() && !flat[k][0].getConst()))) { + proofStep.addAssertion(flat[k].negate()); + } + } + } else { + if (! ((explanation.isConst() && explanation.getConst()) || + (explanation.getKind() == kind::NOT && explanation[0].isConst() && !explanation[0].getConst()))) { + proofStep.addAssertion(explanation.negate()); + } + } + proofRecipe->addStep(proofStep); + } + } + }); } // Keep only the relevant literals explanationVector.resize(j); -} + PROOF({ + if (proofRecipe) { + // The remaining literals are the base of the proof + for (unsigned k = 0; k < explanationVector.size(); ++k) { + proofRecipe->addBaseAssertion(explanationVector[k].node.negate()); + } + } + }); +} void TheoryEngine::ppUnconstrainedSimp(vector& assertions) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index db94edd7c..53c4aac77 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -50,6 +50,7 @@ namespace CVC4 { class ResourceManager; +class LemmaProofRecipe; /** * A pair of a theory and a node. This is used to mark the flow of @@ -270,46 +271,18 @@ class TheoryEngine { } } - void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) { - Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; - Assert(pf == NULL); // theory shouldn't be producing proofs yet - ++ d_statistics.conflicts; - d_engine->d_outputChannelUsed = true; - d_engine->conflict(conflictNode, d_theory); - } + void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException); - bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException) { - Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; - ++ d_statistics.propagations; - d_engine->d_outputChannelUsed = true; - return d_engine->propagate(literal, d_theory); - } + bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException); theory::LemmaStatus lemma(TNode lemma, ProofRule rule, bool removable = false, bool preprocess = false, bool sendAtoms = false) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { - Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; - ++ d_statistics.lemmas; - d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, rule, false, removable, preprocess, sendAtoms ? d_theory : theory::THEORY_LAST, d_theory); - } + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException); - /*theory::LemmaStatus preservedLemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) { - Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::preservedLemma(" << lemma << ")" << std::endl; - ++ d_statistics.lemmas; - d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, false, removable, preprocess, d_theory); - }*/ - - theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { - Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::splitLemma(" << lemma << ")" << std::endl; - ++ d_statistics.lemmas; - d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, d_theory); - } + theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException); void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { NodeManager* curr = NodeManager::currentNM(); @@ -456,7 +429,7 @@ class TheoryEngine { bool removable, bool preprocess, theory::TheoryId atomsTo, - theory::TheoryId ownerTheory); + LemmaProofRecipe* proofRecipe); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector& atoms, theory::TheoryId theory); @@ -606,9 +579,10 @@ private: * asking relevant theories to explain the propagations. Initially * the explanation vector should contain only the element (node, theory) * where the node is the one to be explained, and the theory is the - * theory that sent the literal. + * theory that sent the literal. The lemmaProofRecipe will contain a list + * of the explanation steps required to produce the original node. */ - void getExplanation(std::vector& explanationVector); + void getExplanation(std::vector& explanationVector, LemmaProofRecipe* lemmaProofRecipe); public: @@ -730,7 +704,7 @@ public: * Returns an explanation of the node propagated to the SAT solver and the theory * that propagated it. */ - NodeTheoryPair getExplanationAndExplainer(TNode node); + Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe); /** * collect model info diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 9b429765e..25b12f75f 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -964,12 +964,9 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec std::vector orderedChildren; bool nullCongruenceFound = false; for (unsigned i = 0; i < eqpc->d_children.size(); ++i) { - if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && eqpc->d_children[i]->d_node.isNull()) { - - // For now, assume there can only be one null congruence child - Assert(!nullCongruenceFound); + if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && + eqpc->d_children[i]->d_node.isNull()) { nullCongruenceFound = true; - Debug("pf::ee") << "Have congruence with empty d_node. Splitting..." << std::endl; orderedChildren.insert(orderedChildren.begin(), eqpc->d_children[i]->d_children[0]); orderedChildren.push_back(eqpc->d_children[i]->d_children[1]); @@ -1192,6 +1189,9 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st getExplanation(childId, getEqualityNode(childId).getFind(), equalities, eqpcc); if( eqpc ) { eqpc->d_children.push_back( eqpcc ); + + Debug("pf::ee") << "MERGED_THROUGH_CONSTANTS. Dumping the child proof" << std::endl; + eqpc->debug_print("pf::ee", 1); } } @@ -1605,6 +1605,7 @@ void EqualityEngine::propagate() { } void EqualityEngine::debugPrintGraph() const { + Debug("equality::graph") << std::endl << "Dumping graph" << std::endl; for (EqualityNodeId nodeId = 0; nodeId < d_nodes.size(); ++ nodeId) { Debug("equality::graph") << d_nodes[nodeId] << " " << nodeId << "(" << getEqualityNode(nodeId).getFind() << "):"; @@ -1618,6 +1619,7 @@ void EqualityEngine::debugPrintGraph() const { Debug("equality::graph") << std::endl; } + Debug("equality::graph") << std::endl; } bool EqualityEngine::areEqual(TNode t1, TNode t2) const { @@ -2209,9 +2211,15 @@ bool EqClassIterator::isFinished() const { return d_current == null_id; } -void EqProof::debug_print( const char * c, unsigned tb ) const{ - for( unsigned i=0; iprintTag(d_id); + else + Debug( c ) << d_id; + + Debug( c ) << "("; if( !d_children.empty() || !d_node.isNull() ){ if( !d_node.isNull() ){ Debug( c ) << std::endl; @@ -2221,7 +2229,7 @@ void EqProof::debug_print( const char * c, unsigned tb ) const{ for( unsigned i=0; i0 || !d_node.isNull() ) Debug( c ) << ","; Debug( c ) << std::endl; - d_children[i]->debug_print( c, tb+1 ); + d_children[i]->debug_print( c, tb+1, prettyPrinter ); } } Debug( c ) << ")" << std::endl; diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index f30f1e8a0..843e7ce7f 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -902,11 +902,17 @@ public: class EqProof { public: + class PrettyPrinter { + public: + virtual ~PrettyPrinter() {} + virtual std::string printTag(unsigned tag) = 0; + }; + EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){} unsigned d_id; Node d_node; std::vector< EqProof * > d_children; - void debug_print( const char * c, unsigned tb = 0 ) const; + void debug_print(const char * c, unsigned tb = 0, PrettyPrinter* prettyPrinter = NULL) const; };/* class EqProof */ } // Namespace eq diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index d1685bdd1..9c461f57b 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -502,7 +502,7 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg void TheoryUF::computeCareGraph() { if (d_sharedTerms.size() > 0) { - //use term indexing + //use term indexing Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl; std::map< Node, quantifiers::TermArgTrie > index; std::map< Node, unsigned > arity; @@ -533,6 +533,7 @@ void TheoryUF::computeCareGraph() { void TheoryUF::conflict(TNode a, TNode b) { eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL; + if (a.getKind() == kind::CONST_BOOLEAN) { d_conflictNode = explain(a.iffNode(b),pf); } else { diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index 38b58cedd..38705c22a 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -22,7 +22,6 @@ TESTS = \ bug00.smt \ bug338.smt2 \ bug347.smt \ - bug348.smt \ bug451.smt \ bug509.smt \ bug580.smt2 \ -- 2.30.2