From de0dd1dc966b05467f1a5443ff33094262f5076a Mon Sep 17 00:00:00 2001 From: Guy Date: Wed, 1 Jun 2016 17:41:17 -0700 Subject: [PATCH] Revert "Merging proof branch" This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8. --- 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, 943 insertions(+), 2992 deletions(-) delete mode 100644 src/proof/lemma_proof.cpp delete mode 100644 src/proof/lemma_proof.h delete mode 100644 src/proof/proof_output_channel.cpp delete mode 100644 src/proof/proof_output_channel.h diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf index b54a4ed5b..5ed3d2f6f 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))))))) \ No newline at end of file + (holds cln))))))) diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf index 7f478d823..c93541085 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,3 +171,4 @@ (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 d8ce7be22..580b54418 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,7 +25,6 @@ (bblast_term n x y))))) -; Binds a symbol to the bblast_term to be used later on. (declare decl_bblast (! n mpz (! b bblt @@ -47,31 +46,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 @@ -80,16 +79,18 @@ (! 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 @@ -103,93 +104,35 @@ (! 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 @@ -205,50 +148,42 @@ (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)) @@ -264,10 +199,11 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (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 @@ -279,14 +215,15 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; 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)) @@ -301,14 +238,15 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; 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)) @@ -324,8 +262,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 @@ -334,7 +272,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)))) @@ -358,19 +296,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)) @@ -382,18 +320,6 @@ (! 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 @@ -405,8 +331,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 @@ -420,14 +346,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)) @@ -436,7 +362,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)) @@ -445,7 +371,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] @@ -469,19 +395,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)) @@ -494,18 +420,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)))) @@ -515,23 +441,7 @@ ((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)) @@ -544,110 +454,11 @@ (! 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)) @@ -669,54 +480,10 @@ (! 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)) @@ -739,34 +506,7 @@ (! 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)))))))))))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -803,8 +543,8 @@ ;; REWRITE RULES ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - + + ; rewrite rule : ; x + y = y + x (declare bvadd_symm @@ -812,7 +552,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)) @@ -824,12 +564,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)))) @@ -838,7 +578,7 @@ ;; (default (fail bv)))))) ;; ; rewrite rule (w constants) : -;; ; a & b = c +;; ; a & b = c ;; (declare bvand_const (! c bv ;; (! a bv ;; (! b bv @@ -846,7 +586,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))))) @@ -854,7 +594,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 @@ -881,7 +621,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 @@ -895,7 +635,7 @@ ;; (rw_term _ (bvxor _ a b) ;; (bvnot _ a'))))))))))) - + ;; ;; (bvnot (bvnot a)) => a ;; (declare bvnot_idemp ;; (! n mpz @@ -904,3 +644,4 @@ ;; (! rwa (rw_term _ a a') ;; (rw_term _ (bvnot _ (bvnot _ a)) ;; a')))))) + diff --git a/src/Makefile.am b/src/Makefile.am index cfa4982ca..a3580989c 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -96,14 +96,10 @@ 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 e8a18481b..643932781 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,3 +424,4 @@ $(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 b9907aac9..a1287b667 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -830,8 +830,4 @@ 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 810d41155..788e4bd86 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -74,7 +74,6 @@ 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 aee236677..8aba8dce9 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -81,29 +81,14 @@ 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) { @@ -116,7 +101,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", 0, &d_proofPrinter); + pf->debug_print("pf::array"); Debug("pf::array") << std::endl; toStreamRecLFSC( out, tp, pf, 0, map ); Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl; @@ -129,7 +114,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", 0, &d_proofPrinter); + pf->debug_print("pf::array"); Debug("pf::array") << std::endl; if(tb == 0) { @@ -165,7 +150,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", 0, &d_proofPrinter); + pf->d_children[i+count]->debug_print("pf::array"); congruenceClosures.push_back(pf->d_children[i+count]); } @@ -235,48 +220,48 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, ++i; } } - - 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()); - } + Assert(neg >= 0); 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(!disequalityFound || pf->d_children.size() > 2) { + if(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; } - out << "(clausify_false (contra _ "; + 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 (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; + 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].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. - 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) { + // (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 << " "; + out << ss2.str(); + out << "))"; + + } else { + // The negative node is, e.g., a pure equality + out << "(clausify_false (contra _ "; + + if(n2[0].getKind() == kind::APPLY_UF) { out << "(trans _ _ _ _ "; out << "(symm _ _ _ "; out << ss.str(); @@ -291,27 +276,16 @@ 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]); + 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(); } if (pf->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) { Debug("mgd") << "\nok, looking at congruence:\n"; - pf->debug_print("mgd", 0, &d_proofPrinter); + pf->debug_print("mgd"); 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()); @@ -341,7 +315,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n"; - pf2->debug_print("mgd", 0, &d_proofPrinter); + pf2->debug_print("mgd"); // 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; @@ -358,7 +332,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", 0, &d_proofPrinter); + pf2->d_children[0]->debug_print("mgd"); } Assert(match(pf2->d_node, n1[1])); side = 1; @@ -572,20 +546,6 @@ 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; @@ -594,7 +554,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", 0, &d_proofPrinter); + pf->debug_print("mgd"); Debug("mgd") << "\n"; Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n"; @@ -812,7 +772,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, &d_proofPrinter); + pf->debug_print("mgdx",0); //toStreamRec(Warning.getStream(), pf, 0); Warning() << "\n\n"; Unreachable(); @@ -971,9 +931,6 @@ 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); @@ -982,31 +939,28 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("pf::array") << "Subproof is: " << ss.str() << std::endl; - if (swap) { - out << "(symm _ _ _ "; - } - out << "(negativerow _ _ "; - tp->printTerm(swap ? t2.toExpr() : t1.toExpr(), out, map); + tp->printTerm(t1.toExpr(), out, map); out << " "; - tp->printTerm(swap ? t1.toExpr() : t2.toExpr(), out, map); + tp->printTerm(t2.toExpr(), out, map); out << " "; tp->printTerm(t3.toExpr(), out, map); out << " "; tp->printTerm(t4.toExpr(), out, map); out << " "; - if (side != 0) { - out << "(negsymm _ _ _ " << ss.str() << ")"; - } else { - out << ss.str(); - } + + // 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() << ")"; + // } out << ")"; - if (swap) { - out << ") "; - } + // Unreachable(); return ret; } @@ -1117,12 +1071,13 @@ 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) { @@ -1199,21 +1154,7 @@ 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()); - 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 <<" "; - } + os << type <<" "; } void LFSCArrayProof::printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren) { @@ -1228,6 +1169,8 @@ 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"; @@ -1286,7 +1229,6 @@ 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); @@ -1295,7 +1237,7 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p << "It is a witness for: " << equality << std::endl; std::ostringstream newSkolemLiteral; - newSkolemLiteral << ".sl" << count++; + newSkolemLiteral << ".sl" << d_skolemToLiteral.size(); std::string skolemLiteral = newSkolemLiteral.str(); d_skolemToLiteral[*it] = skolemLiteral; @@ -1309,12 +1251,13 @@ 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 << " (\\ "; - os << ProofManager::sanitize(*it); + printTerm(*it, os, map); os << " (\\ "; os << skolemLiteral.c_str(); os << "\n"; @@ -1323,8 +1266,4 @@ 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 076ba7381..fb25c9433 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -30,32 +30,6 @@ 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, @@ -67,8 +41,6 @@ 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 @@ -81,10 +53,6 @@ public: void setRowMergeTag(unsigned tag); void setRow1MergeTag(unsigned tag); void setExtMergeTag(unsigned tag); - - unsigned getRowMergeTag() const; - unsigned getRow1MergeTag() const; - unsigned getExtMergeTag() const; }; namespace theory { @@ -123,7 +91,6 @@ 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 479266db4..b63782226 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -15,11 +15,9 @@ **/ -#include "options/bv_options.h" -#include "proof/array_proof.h" #include "proof/bitvector_proof.h" +#include "options/bv_options.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" @@ -82,40 +80,20 @@ 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) && @@ -123,11 +101,6 @@ 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]); @@ -135,7 +108,6 @@ 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(); @@ -150,8 +122,6 @@ 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]); @@ -159,7 +129,6 @@ 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; @@ -175,99 +144,25 @@ 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 #" << 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()) { + Debug("pf::bv") << "Finalize conflict " << confl << std::endl; + //Assert (d_bbConflictMap.find(confl) != d_bbConflictMap.end()); + if(d_bbConflictMap.find(confl) != d_bbConflictMap.end()){ ClauseId id = d_bbConflictMap[confl]; d_resolutionProof->collectClauses(id); - } 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(); - } + }else{ + Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl; } } } @@ -343,25 +238,11 @@ void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const LetMa printBitOf(term, os, map); return; } - - case kind::VARIABLE: { - os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")"; - return; - } - + case kind::VARIABLE: case kind::SKOLEM: { - - // 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) << ")"; - } + os << "(a_var_bv " << utils::getSize(term)<<" " << ProofManager::sanitize(term) <<")"; return; } - default: Unreachable(); } @@ -377,7 +258,14 @@ void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const LetMap& m << ", var = " << var << std::endl; os << "(bitof "; - os << d_exprToVariableName[var]; + 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 << " " << bit << ")"; } @@ -461,16 +349,14 @@ 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) { @@ -491,7 +377,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(); + Debug("pf::bv") << std::endl << "; Print non-bitblast theory conflict " << conflict << std::endl; + BitVectorProof::printTheoryLemmaProof( lemma, os, paren ); } } @@ -625,13 +402,7 @@ 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) { - 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"; + os << "(% " << ProofManager::sanitize(*it) <<" var_bv\n"; paren <<")"; } } @@ -640,43 +411,15 @@ 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()) { - // A term is a leaf if it has no children, or if it belongs to another theory - os << "(bv_bbl_var " << utils::getSize(term) << " " << d_exprToVariableName[term]; - os << " _ )"; + 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 <<" _ _ _ _ _ _ "; } - - if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";} - os << getBBTermName(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; @@ -781,9 +501,7 @@ 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; @@ -821,7 +539,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { } } -void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool swap) { +void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) { Kind kind = atom.getKind(); switch(kind) { case kind::BITVECTOR_ULT : @@ -832,28 +550,11 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool case kind::BITVECTOR_SLE : case kind::BITVECTOR_SGT : case kind::BITVECTOR_SGE : - 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";} - + case kind::EQUAL: + { + os <<"(bv_bbl_" << utils::toLFSCKind(atom.getKind()); 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 << ")"; + os << getBBTermName(atom[0])<<" " << getBBTermName(atom[1]) <<")"; return; } default: @@ -861,53 +562,19 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool } } -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) << "\n"; - paren << "))"; + os << "(\\ "<< getBBTermName(*it); + paren <<"\n))"; } // bit-blast atoms ExprToExpr::const_iterator ait = d_bbAtoms.begin(); @@ -922,35 +589,7 @@ void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) bool val = ait->first.getConst(); os << "(iff_symm " << (val ? "true" : "false" ) << ")"; } else { - 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); - } + printAtomBitblasting(ait->first, os); } os <<"(\\ " << ProofManager::getPreprocessedAssertionName(ait->second) <<"\n"; @@ -967,53 +606,25 @@ 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 << std::endl << ";; BB atom mapping\n" << std::endl; - - std::set atoms; - d_cnfProof->collectAtomsForClauses(used_inputs, atoms); + os << ";; BB atom mapping\n"; - 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; + NodeSet atoms; + d_cnfProof->collectAtomsForClauses(used_inputs,atoms); // first print bit-blasting printBitblasting(os, paren); // print CNF conversion proof for bit-blasted facts d_cnfProof->printAtomMapping(atoms, os, paren); - os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl; + os << ";; Bit-blasting definitional clauses \n"; for (IdToSatClause::iterator it = used_inputs.begin(); it != used_inputs.end(); ++it) { d_cnfProof->printCnfProofForClause(it->first, it->second, os, paren); } - os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl; + os << ";; Bit-blasting learned clauses \n"; 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 4e5e98541..4a1f4015d 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -60,7 +60,6 @@ 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: @@ -109,8 +108,7 @@ public: virtual void registerTerm(Expr term); virtual void printTermBitblasting(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 printAtomBitblasting(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; @@ -125,12 +123,6 @@ 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) @@ -138,13 +130,11 @@ 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, bool swap); - virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os); + virtual void printAtomBitblasting(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 abe48e3cd..19e9cbac9 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -19,7 +19,6 @@ #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" @@ -33,6 +32,7 @@ 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,6 +103,7 @@ void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) { setClauseAssertion(clause, current_assertion); setClauseDefinition(clause, current_expr); + registerExplanationLemma(clause); } void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { @@ -142,15 +143,16 @@ void CnfProof::registerAssertion(Node assertion, ProofRule reason) { d_assertionToProofRule.insert(assertion, reason); } -LemmaProofRecipe CnfProof::getProofRecipe(const std::set &lemma) { - Assert(d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end()); - return d_lemmaToProofRecipe[lemma]; +void CnfProof::registerExplanationLemma(ClauseId clauseId) { + d_clauseIdToOwnerTheory.insert(clauseId, getExplainerTheory()); } -bool CnfProof::haveProofRecipe(const std::set &lemma) { - return d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end(); +theory::TheoryId CnfProof::getOwnerTheory(ClauseId clause) { + Assert(d_clauseIdToOwnerTheory.find(clause) != d_clauseIdToOwnerTheory.end()); + return d_clauseIdToOwnerTheory[clause]; } + void CnfProof::setCnfDependence(Node from, Node to) { Debug("proof:cnf") << "CnfProof::setCnfDependence " << "from " << from << std::endl @@ -181,10 +183,12 @@ Node CnfProof::getCurrentAssertion() { return d_currentAssertionStack.back(); } -void CnfProof::setProofRecipe(LemmaProofRecipe* proofRecipe) { - Assert(proofRecipe); - Assert(proofRecipe->getNumSteps() > 0); - d_lemmaToProofRecipe[proofRecipe->getBaseAssertions()] = *proofRecipe; +void CnfProof::setExplainerTheory(theory::TheoryId theory) { + d_explainerTheory = theory; +} + +theory::TheoryId CnfProof::getExplainerTheory() { + return d_explainerTheory; } void CnfProof::pushCurrentDefinition(Node definition) { @@ -208,19 +212,22 @@ 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, - std::set& atoms) { + NodeSet& 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); } } @@ -230,75 +237,14 @@ 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, - std::set& atoms) { + NodeSet& atom_map) { IdToSatClause::const_iterator it = clauses.begin(); for (; it != clauses.end(); ++it) { const prop::SatClause* clause = it->second; - collectAtoms(clause, atoms); + collectAtoms(clause, atom_map); } -} - -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, @@ -317,13 +263,13 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses, } } -void LFSCCnfProof::printAtomMapping(const std::set& atoms, +void LFSCCnfProof::printAtomMapping(const NodeSet& atoms, std::ostream& os, std::ostream& paren) { - std::set::const_iterator it = atoms.begin(); - std::set::const_iterator end = atoms.end(); + NodeSet::const_iterator it = atoms.begin(); + NodeSet::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(); @@ -331,8 +277,8 @@ void LFSCCnfProof::printAtomMapping(const std::set& atoms, LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); pe->printLetTerm(atom.toExpr(), os); - os << " (\\ " << ProofManager::getVarName(var, d_name); - os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; + os << " (\\ " << ProofManager::getVarName(var, d_name) + << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; paren << ")))"; } } @@ -358,9 +304,6 @@ 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); @@ -393,10 +336,6 @@ 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; @@ -625,7 +564,6 @@ 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 ); @@ -724,7 +662,6 @@ 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 62036ced0..a21cb1c0e 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -27,7 +27,6 @@ #include "context/cdhashmap.h" #include "proof/clause_id.h" -#include "proof/lemma_proof.h" #include "proof/sat_proof.h" #include "util/proof.h" @@ -44,9 +43,7 @@ typedef __gnu_cxx::hash_set ClauseIdSet; typedef context::CDHashMap ClauseIdToNode; typedef context::CDHashMap NodeToProofRule; -typedef std::map, LemmaProofRecipe> LemmaToRecipe; -typedef std::pair NodePair; -typedef std::set NodePairSet; +typedef context::CDHashMap ClauseIdToTheory; class CnfProof { protected: @@ -58,8 +55,11 @@ protected: /** Map from assertion to reason for adding assertion **/ NodeToProofRule d_assertionToProofRule; - /** Map from lemma to the recipe for proving it **/ - LemmaToRecipe d_lemmaToProofRecipe; + /** Map from assertion to the theory that added this assertion **/ + ClauseIdToTheory d_clauseIdToOwnerTheory; + + /** The last theory to explain a lemma **/ + theory::TheoryId d_explainerTheory; /** Top of stack is assertion currently being converted to CNF **/ std::vector d_currentAssertionStack; @@ -91,16 +91,10 @@ 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, - std::set& atoms); + NodeSet& atoms); void collectAtomsForClauses(const IdToSatClause& clauses, - std::set& atoms); - void collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses, - std::set& atoms, - NodePairSet& rewrites); + NodeSet& atoms); void collectAssertionsForClauses(const IdToSatClause& clauses, NodeSet& assertions); @@ -127,9 +121,11 @@ public: void popCurrentDefinition(); Node getCurrentDefinition(); - void setProofRecipe(LemmaProofRecipe* proofRecipe); - LemmaProofRecipe getProofRecipe(const std::set &lemma); - bool haveProofRecipe(const std::set &lemma); + void setExplainerTheory(theory::TheoryId theory); + theory::TheoryId getExplainerTheory(); + theory::TheoryId getOwnerTheory(ClauseId clause); + + void registerExplanationLemma(ClauseId clauseId); // accessors for the leaf assertions that are being converted to CNF bool isAssertion(Node node); @@ -138,7 +134,7 @@ public: Node getAssertionForClause(ClauseId clause); /** Virtual methods for printing things **/ - virtual void printAtomMapping(const std::set& atoms, + virtual void printAtomMapping(const NodeSet& atoms, std::ostream& os, std::ostream& paren) = 0; @@ -165,7 +161,7 @@ public: {} ~LFSCCnfProof() {} - void printAtomMapping(const std::set& atoms, + void printAtomMapping(const NodeSet& atoms, std::ostream& os, std::ostream& paren); diff --git a/src/proof/lemma_proof.cpp b/src/proof/lemma_proof.cpp deleted file mode 100644 index a12a516cf..000000000 --- a/src/proof/lemma_proof.cpp +++ /dev/null @@ -1,193 +0,0 @@ -/********************* */ -/*! \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 deleted file mode 100644 index e96ff5337..000000000 --- a/src/proof/lemma_proof.h +++ /dev/null @@ -1,79 +0,0 @@ -/********************* */ -/*! \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 5ce8b523f..a3689d746 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -200,6 +200,7 @@ 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; @@ -216,15 +217,9 @@ std::string ProofManager::getAtomName(TNode atom, Assert(!lit.isNegated()); return getAtomName(lit.getSatVariable(), prefix); } - std::string ProofManager::getLitName(TNode lit, const std::string& 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; + return getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix); } std::string ProofManager::sanitize(TNode node) { @@ -336,9 +331,6 @@ 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 @@ -392,37 +384,8 @@ void LFSCProof::toStream(std::ostream& out) { for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3) Debug("pf::pm") << "\t assertion = " << *it3 << std::endl; - std::set atoms; - NodePairSet rewrites; + NodeSet atoms; // 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); @@ -430,23 +393,38 @@ 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); } - std::set::iterator atomIt; - Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: " - << std::endl << std::endl; + NodeSet::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 = atoms.begin(); it != atoms.end(); ++it) { + for(; it != end; ++it) { Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl; d_theoryProof->registerTerm((*it).toExpr()); } @@ -466,15 +444,9 @@ 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\n"; + out << " ;; Printing deferred declarations \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); @@ -492,6 +464,10 @@ 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; @@ -520,8 +496,6 @@ 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 _ "; @@ -532,6 +506,7 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; paren << "))"; + } os << "\n"; @@ -593,14 +568,6 @@ 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 c6454b652..c74aac237 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -34,8 +34,6 @@ namespace CVC4 { -class SmtGlobals; - // forward declarations namespace Minisat { class Solver; @@ -138,8 +136,6 @@ class ProofManager { std::set d_printedTypes; - std::map d_rewriteFilters; - protected: LogicInfo d_logic; @@ -228,9 +224,6 @@ 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 deleted file mode 100644 index 6d729db1f..000000000 --- a/src/proof/proof_output_channel.cpp +++ /dev/null @@ -1,82 +0,0 @@ -/********************* */ -/*! \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 deleted file mode 100644 index b85af5fb5..000000000 --- a/src/proof/proof_output_channel.h +++ /dev/null @@ -1,50 +0,0 @@ -/********************* */ -/*! \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 fe0d42242..5b04c281d 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, std::set& seen) { +void collectAtoms(TNode node, CVC4::NodeSet& 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 8c734c892..da10c33a0 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,9 +29,6 @@ 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); @@ -45,7 +42,7 @@ inline unsigned getExtractLow(Expr node) { } inline unsigned getSize(Type type) { - BitVectorType bv(type); + BitVectorType bv(type); return bv.getSize(); } @@ -63,8 +60,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) { @@ -76,16 +73,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) { @@ -95,14 +92,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(); @@ -112,23 +109,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(); @@ -138,7 +135,7 @@ inline Expr mkAnd(const std::vector& conjunctions) { ++ it; } - Node res = conjunction; + Node res = conjunction; return res.toExpr(); }/* mkAnd() */ @@ -147,14 +144,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(); @@ -168,13 +165,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, std::set& seen); +void collectAtoms(TNode node, NodeSet& seen); } diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index 1e01e4dce..4f3330ef7 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -543,9 +543,12 @@ 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) - << std::endl; + Debug("pf::sat") + << "TSatProof::registerClause registering a new lemma clause: " + << newId << " = " << *buildClause(newId) + << ". Explainer theory: " << d_cnfProof->getExplainerTheory() + << std::endl; + d_cnfProof->registerExplanationLemma(newId); } } @@ -576,10 +579,12 @@ 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 - << std::endl; + Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new " + "lemma (UNIT CLAUSE): " + << lit << ". Explainer theory: " + << d_cnfProof->getExplainerTheory() << std::endl; d_lemmaClauses.insert(newId); + d_cnfProof->registerExplanationLemma(newId); } } ClauseId id = d_unitId[toInt(lit)]; @@ -837,7 +842,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 (size_t i = 0; i < current_reason_size; i++) { + for (int 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]; @@ -899,7 +904,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 (size_t i = 0; i < conflict_size; ++i) { + for (int 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); @@ -1101,12 +1106,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 b026e21c2..de510e514 100644 --- a/src/proof/skolemization_manager.h +++ b/src/proof/skolemization_manager.h @@ -37,6 +37,7 @@ 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 eaf21846b..088275b3f 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -25,7 +25,6 @@ #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" @@ -49,6 +48,74 @@ 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() @@ -64,12 +131,13 @@ 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("pf::tp") << "TheoryProofEngine::registerTheory: " << id << std::endl; + Trace("theory-proof-debug") << "; register theory " << id << std::endl; if (id == theory::THEORY_UF) { d_theoryProofTable[id] = new LFSCUFProof((theory::uf::TheoryUF*)th, this); @@ -99,42 +167,19 @@ 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( " << term << " ) = " << theory_id << std::endl; + Debug("pf::tp") << "Term's theory: " << theory_id << std::endl; // don't need to register boolean terms if (theory_id == theory::THEORY_BUILTIN || @@ -148,38 +193,32 @@ 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(const prop::SatClause* clause) { +theory::TheoryId TheoryProofEngine::getTheoryForLemma(ClauseId id) { ProofManager* pm = ProofManager::currentPM(); - 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; - } + Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma( " << id << " )" + << " = " << pm->getCnfProof()->getOwnerTheory(id) << std::endl; - nodes.insert(lit.isNegated() ? node.notNode() : node); + 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; } - // Ensure that the lemma is in the database. - Assert (pm->getCnfProof()->haveProofRecipe(nodes)); - return pm->getCnfProof()->getProofRecipe(nodes).getTheory(); + 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(); } void LFSCTheoryProofEngine::bind(Expr term, LetMap& map, Bindings& let_order) { @@ -233,6 +272,8 @@ 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 @@ -274,29 +315,6 @@ 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(); @@ -304,8 +322,6 @@ void LFSCTheoryProofEngine::registerTermsFromAssertions() { for(; it != end; ++it) { registerTerm(*it); } - - performExtraRegistrations(); } void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) { @@ -317,43 +333,17 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare for (; it != end; ++it) { Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl; - std::ostringstream name; - name << "A" << counter++; - os << "(% " << name.str() << " (th_holds "; + // FIXME: merge this with counter + os << "(% A" << counter++ << " (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; @@ -388,148 +378,55 @@ void LFSCTheoryProofEngine::printDeferredDeclarations(std::ostream& os, std::ost } } -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) { - it->second->printAliasingDeclarations(os, paren); - } -} +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(); -void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause& lemmas) { - Debug("pf::dumpLemmas") << "Dumping ALL theory lemmas" << std::endl << std::endl; + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: checking lemma owners..." << std::endl; - ProofManager* pm = ProofManager::currentPM(); - for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) { + for (; it != end; ++it) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: new lemma" << std::endl; 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"); + Debug("pf::tp") << "\tLemma = " << id + << ". Owner theory: " << pm->getCnfProof()->getOwnerTheory(id) << std::endl; } + it = lemmas.begin(); - 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 + // 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) { + for (; it != end; ++it) { + ClauseId id = it->first; const prop::SatClause* clause = it->second; + theory::TheoryId theory_id = getTheoryForLemma(id); + if (theory_id != theory::THEORY_BV) continue; + std::vector conflict; - std::set conflictNodes; for(unsigned i = 0; i < clause->size(); ++i) { prop::SatLiteral lit = (*clause)[i]; - Node node = ProofManager::currentPM()->getCnfProof()->getAtom(lit.getSatVariable()); - Expr atom = node.toExpr(); - - // The literals (true) and (not false) are omitted from conflicts + Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr(); 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); + bv->printResolutionProof(os, paren); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { Assert (lemmas.size() == 1); @@ -537,247 +434,54 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, return; } - ProofManager* pm = ProofManager::currentPM(); + it = lemmas.begin(); + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemmas..." << std::endl; - for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) { + 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; 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") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemma. ID = " - << id << std::endl; + Debug("pf::tp") << "CnfProof printing clause..." << std::endl; + pm->getCnfProof()->printClause(*clause, os, clause_paren); + Debug("pf::tp") << "CnfProof printing clause - Done!" << std::endl; std::vector clause_expr; - std::set clause_expr_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(); + Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).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); } - 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 << "))"; - } + 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 << "))"; } } 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()) { @@ -893,21 +597,19 @@ 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("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl; - - if (d_theory->getId()==theory::THEORY_UF) { + Trace("theory-proof-debug") << ";; 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::"); @@ -1012,10 +714,7 @@ void BooleanProof::registerTerm(Expr term) { void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { Assert (term.getType().isBoolean()); if (term.isVariable()) { - if (d_treatBoolsAsFormulas) - os << "(p_app " << ProofManager::sanitize(term) <<")"; - else - os << ProofManager::sanitize(term); + os << "(p_app " << ProofManager::sanitize(term) <<")"; return; } @@ -1054,10 +753,7 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& return; case kind::CONST_BOOLEAN: - if (d_treatBoolsAsFormulas) - os << (term.getConst() ? "true" : "false"); - else - os << (term.getConst() ? "t_true" : "t_false"); + os << (term.getConst() ? "true" : "false"); return; default: @@ -1090,10 +786,6 @@ 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 c8c776ec9..54c86f3f3 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -27,7 +27,6 @@ #include "proof/clause_id.h" #include "prop/sat_solver_types.h" #include "util/proof.h" -#include "proof/proof_utils.h" namespace CVC4 { @@ -91,14 +90,10 @@ 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 @@ -152,14 +147,6 @@ 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). @@ -184,14 +171,8 @@ public: */ void registerTheory(theory::Theory* theory); - theory::TheoryId getTheoryForLemma(const prop::SatClause* clause); + theory::TheoryId getTheoryForLemma(ClauseId id); 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 { @@ -209,25 +190,11 @@ 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 { @@ -302,21 +269,12 @@ 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 { @@ -334,13 +292,12 @@ 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), d_treatBoolsAsFormulas(true) + : BooleanProof(proofEngine) {} virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); virtual void printOwnedSort(Type type, std::ostream& os); @@ -348,14 +305,6 @@ 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 bc409901c..32ca122b0 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -86,16 +86,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E pf->debug_print("pf::uf"); Debug("pf::uf") << std::endl; - 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(); - } - + if(tb == 0) { Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS); Assert(!pf->d_node.isNull()); Assert(pf->d_children.size() >= 2); @@ -199,71 +190,42 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E ++i; } } - - 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()); - } + Assert(neg >= 0); 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(!disequalityFound || subTrans.d_children.size() >= 2) { + if(pf->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; } - Debug("pf::uf") << "\nhave proven: " << 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 (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].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 (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 (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; + 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() << ")"; } 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() << ")"; - } else { - out << ss.str(); - } - out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; + out << ss.str(); } - } 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; + out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; } - return Node(); } @@ -622,10 +584,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].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n1[1]; ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")"; } else if(n1[1] == n2) { - n1 = n1[0].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n1[0]; ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")"; } else { Unreachable(); @@ -633,16 +595,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].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n2[1]; ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")"; } else if(n2[1] == n1) { - n1 = n2[0].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n2[0]; ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")"; } else { Unreachable(); } } else { - // Both n1 and n2 are predicates. Don't know what to do... + // Both n1 and n2 are prediacates. Don't know what to do... Unreachable(); } @@ -705,7 +667,6 @@ 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 "; @@ -722,7 +683,6 @@ 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) { @@ -754,8 +714,6 @@ 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; @@ -771,8 +729,7 @@ 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 << " "; - d_proofEngine->printSort(arg_type, os); + os << " " << arg_type; if (i < args.size() - 2) { os << " (arrow"; fparen << ")"; @@ -785,16 +742,10 @@ 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 0a23267d8..e359eaebd 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -69,7 +69,6 @@ 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 eda736b8a..aa1fc9587 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, bool noPreregistration) { +void TseitinCnfStream::ensureLiteral(TNode n) { // These are not removable and have no proof ID d_removable = false; @@ -163,7 +163,7 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) { d_literalToNodeMap.insert_safe(~lit, n.notNode()); } else { // We have a theory atom or variable. - lit = convertAtom(n, noPreregistration); + lit = convertAtom(n); } Assert(hasLiteral(n) && getNode(lit) == n); @@ -232,7 +232,7 @@ void CnfStream::setProof(CnfProof* proof) { d_cnfProof = proof; } -SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) { +SatLiteral CnfStream::convertAtom(TNode node) { Debug("cnf") << "convertAtom(" << node << ")" << endl; Assert(!hasLiteral(node), "atom already mapped!"); @@ -247,7 +247,7 @@ SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) { } else { theoryLiteral = true; canEliminate = false; - preRegister = !noPreregistration; + preRegister = true; } // Make a new literal (variables are not considered theory literals) @@ -258,11 +258,7 @@ SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) { 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; @@ -679,7 +675,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proof_id, TNode from, - LemmaProofRecipe* proofRecipe) { + theory::TheoryId ownerTheory) { Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl; @@ -689,12 +685,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, Node assertion = negated ? node.notNode() : (Node)node; Node from_assertion = negated? from.notNode() : (Node) from; - if (proofRecipe) { - Debug("pf::sat") << "TseitinCnfStream::convertAndAssert: setting proof recipe" << std::endl; - proofRecipe->dump("pf::sat"); - d_cnfProof->setProofRecipe(proofRecipe); - } - + d_cnfProof->setExplainerTheory(ownerTheory); 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 6cc10d878..cf9d519a7 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -36,9 +36,6 @@ #include "smt_util/lemma_channels.h" namespace CVC4 { - -class LemmaProofRecipe; - namespace prop { class PropEngine; @@ -177,7 +174,7 @@ protected: * structure in this expression. Assumed to not be in the * translation cache. */ - SatLiteral convertAtom(TNode node, bool noPreprocessing = false); + SatLiteral convertAtom(TNode node); public: @@ -210,10 +207,14 @@ 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 proofRecipe contains the proof recipe for proving this node + * @param ownerTheory indicates the theory that should invoked to prove the formula. */ - virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null(), LemmaProofRecipe* proofRecipe = NULL) = 0; - + virtual void convertAndAssert(TNode node, + bool removable, + bool negated, + ProofRule proof_id, + TNode from = TNode::null(), + theory::TheoryId ownerTheory = theory::THEORY_LAST) = 0; /** * Get the node that is represented by the given SatLiteral. * @param literal the literal from the sat solver @@ -234,7 +235,7 @@ public: * this is like a "convert-but-don't-assert" version of * convertAndAssert(). */ - virtual void ensureLiteral(TNode n, bool noPreregistration = false) = 0; + virtual void ensureLiteral(TNode n) = 0; /** * Returns the literal that represents the given node in the SAT CNF @@ -283,7 +284,7 @@ public: */ void convertAndAssert(TNode node, bool removable, bool negated, ProofRule rule, TNode from = TNode::null(), - LemmaProofRecipe* proofRecipe = NULL); + theory::TheoryId ownerTheory = theory::THEORY_LAST); /** * Constructs the stream to use the given sat solver. @@ -336,7 +337,7 @@ private: */ SatLiteral toCNF(TNode node, bool negated = false); - void ensureLiteral(TNode n, bool noPreregistration = false); + void ensureLiteral(TNode n); };/* class TseitinCnfStream */ diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index d898b66a2..411b89514 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -232,8 +232,6 @@ 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); @@ -268,12 +266,6 @@ 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 @@ -284,7 +276,6 @@ 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 @@ -345,12 +336,6 @@ 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); @@ -1681,13 +1666,6 @@ 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()); @@ -1747,7 +1725,6 @@ 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); @@ -1764,7 +1741,6 @@ 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 ff726e299..bfbf9da6f 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,3 +300,5 @@ 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 eb607e901..54cf4c457 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, - LemmaProofRecipe* proofRecipe, + theory::TheoryId ownerTheory, 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, proofRecipe); + d_cnfStream->convertAndAssert(node, removable, negated, rule, from, ownerTheory); } void PropEngine::requirePhase(TNode n, bool phase) { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index c02015931..b9ce7ca7e 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -37,7 +37,6 @@ namespace CVC4 { class ResourceManager; class DecisionEngine; class TheoryEngine; -class LemmaProofRecipe; namespace theory { class TheoryRegistrar; @@ -135,7 +134,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, LemmaProofRecipe* proofRecipe, TNode from = TNode::null()); + void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, theory::TheoryId ownerTheory, 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 6e8f1fbbf..4a4515eb9 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -99,34 +99,29 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { TNode lNode = d_cnfStream->getNode(l); Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl; - LemmaProofRecipe* proofRecipe = NULL; - PROOF(proofRecipe = new LemmaProofRecipe;); - - Node theoryExplanation = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe); + NodeTheoryPair theoryExplanation = d_theoryEngine->getExplanationAndExplainer(lNode); + Node explanationNode = theoryExplanation.node; + theory::TheoryId explainerTheory = theoryExplanation.theory; PROOF({ - ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); - ProofManager::getCnfProof()->setProofRecipe(proofRecipe); - - Debug("pf::sat") << "TheoryProxy::explainPropagation: setting lemma recipe to: " - << std::endl; - proofRecipe->dump("pf::sat"); + ProofManager::getCnfProof()->pushCurrentAssertion(explanationNode); + ProofManager::getCnfProof()->setExplainerTheory(explainerTheory); - delete proofRecipe; - proofRecipe = NULL; + Debug("pf::sat") << "TheoryProxy::explainPropagation: setting explainer theory to: " + << explainerTheory << std::endl; }); - 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(); + 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(); 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(theoryExplanation)); + explanation.push_back(~d_cnfStream->getLiteral(explanationNode)); } } @@ -180,9 +175,7 @@ void TheoryProxy::notifyRestart() { if(lemmaCount % 1 == 0) { Debug("shared") << "=) " << asNode << std::endl; } - - LemmaProofRecipe* noProofRecipe = NULL; - d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, noProofRecipe); + d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, theory::THEORY_LAST); } else { Debug("shared") << "=(" << asNode << std::endl; } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 63afb0b72..8f282b413 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 808f5162c..5634a4651 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -63,21 +63,14 @@ void SmtEngine::checkProof() { Chat() << "checking proof..." << 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; + 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; return; } diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp index 6dfd14157..11c3dc081 100644 --- a/src/theory/arrays/array_proof_reconstruction.cpp +++ b/src/theory/arrays/array_proof_reconstruction.cpp @@ -101,59 +101,8 @@ 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 28a08630e..6add1b55f 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -829,8 +829,7 @@ void TheoryArrays::propagate(Effort e) Node TheoryArrays::explain(TNode literal) { - Node explanation = explain(literal, NULL); - return explanation; + return explain(literal, NULL); } Node TheoryArrays::explain(TNode literal, eq::EqProof *proof) @@ -1395,7 +1394,6 @@ void TheoryArrays::check(Effort e) { break; default: Unreachable(); - break; } } @@ -2233,7 +2231,6 @@ 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 dc5520411..fdc36ce72 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(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") +AbstractionModule::Statistics::Statistics() + : d_numFunctionsAbstracted("theory::bv::AbstractioModule::NumFunctionsAbstracted", 0) + , d_numArgsSkolemized("theory::bv::AbstractioModule::NumArgsSkolemized", 0) + , d_abstractionTime("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 5d48b926e..5d580f6ce 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(const std::string& name); + Statistics(); ~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(const std::string& name) + AbstractionModule() : d_argsTable() , d_signatureToFunc() , d_funcToSignature() @@ -207,34 +207,34 @@ public: , d_addedLemmas() , d_lemmaAtoms() , d_inputAtoms() - , d_statistics(name) + , d_statistics() {} - /** + /** * 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 6c6c13ee8..b7619c4bb 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, bv->getFullInstanceName() + "lazy")), + d_bitblaster(new TLazyBitblaster(c, bv, "lazy")), d_bitblastQueue(c), - d_statistics(bv->getFullInstanceName()), + d_statistics(), d_validModelCache(c, true), d_lemmaAtomsQueue(c), d_useSatPropagation(options::bitvectorPropagate()), @@ -55,9 +55,9 @@ BitblastSolver::~BitblastSolver() { delete d_bitblaster; } -BitblastSolver::Statistics::Statistics(const std::string &instanceName) - : d_numCallstoCheck(instanceName + "theory::bv::BitblastSolver::NumCallsToCheck", 0) - , d_numBBLemmas(instanceName + "theory::bv::BitblastSolver::NumTimesLemmasBB", 0) +BitblastSolver::Statistics::Statistics() + : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0) + , d_numBBLemmas("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,3 +256,4 @@ 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 fe16d2702..e9300138b 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(const std::string &instanceName); + Statistics(); ~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 fec93e033..f5b2175f3 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -42,16 +42,14 @@ namespace CVC4 { namespace theory { namespace bv { -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), +TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) + : Theory(THEORY_BV, c, u, out, valuation, logicInfo), d_context(c), d_alreadyPropagatedSet(c), d_sharedTermsSet(c), d_subtheories(), d_subtheoryMap(), - d_statistics(getFullInstanceName()), + d_statistics(), d_staticLearnCache(), d_BVDivByZero(), d_BVRemByZero(), @@ -64,7 +62,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, d_literalsToPropagateIndex(c, 0), d_propagatedBy(c), d_eagerSolver(NULL), - d_abstractionModule(new AbstractionModule(getFullInstanceName())), + d_abstractionModule(new AbstractionModule()), d_isCoreTheory(false), d_calledPreregister(false) { @@ -121,14 +119,14 @@ void TheoryBV::spendResource(unsigned ammount) throw(UnsafeInterruptException) { getOutputChannel().spendResource(ammount); } -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) +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) { smtStatisticsRegistry()->registerStat(&d_avgConflictSize); smtStatisticsRegistry()->registerStat(&d_solveSubstitutions); @@ -236,7 +234,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); @@ -278,9 +276,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); @@ -329,7 +327,7 @@ void TheoryBV::sendConflict() { if (d_conflictNode.isNull()) { return; } else { - Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode << std::endl; + Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode; d_out->conflict(d_conflictNode); d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren()); d_conflictNode = Node::null(); @@ -705,7 +703,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; } @@ -725,7 +723,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 ba2a4fc2a..7f0494dc1 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -56,8 +56,7 @@ class TheoryBV : public Theory { public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, - std::string name = ""); + Valuation valuation, const LogicInfo& logicInfo); ~TheoryBV(); @@ -89,8 +88,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: @@ -101,10 +100,10 @@ private: IntStat d_solveSubstitutions; TimerStat d_solveTimer; IntStat d_numCallsToCheckFullEffort; - IntStat d_numCallsToCheckStandardEffort; + IntStat d_numCallsToCheckStandardEffort; TimerStat d_weightComputationTimer; IntStat d_numMultSlice; - Statistics(const std::string &name); + Statistics(); ~Statistics(); }; @@ -122,12 +121,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. @@ -143,7 +142,7 @@ private: CVC4::theory::SubstitutionMap d_funcToSkolem; context::CDO d_lemmasAdded; - + // Are we in conflict? context::CDO d_conflict; @@ -166,17 +165,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; } @@ -192,7 +191,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); @@ -213,7 +212,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 618fda4c0..1ab4c228b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -26,8 +26,6 @@ #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" @@ -55,104 +53,6 @@ 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); @@ -597,10 +497,7 @@ void TheoryEngine::combineTheories() { // We need to split on it Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; - - LemmaProofRecipe* proofRecipe = NULL; - lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, proofRecipe); - + lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, carePair.theory); // 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) { @@ -1066,7 +963,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 << ", " << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")" << endl; + Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << endl; Assert(toTheoryId != fromTheoryId); if(toTheoryId != THEORY_SAT_SOLVER && @@ -1279,23 +1176,6 @@ 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); @@ -1390,7 +1270,7 @@ static Node mkExplanation(const std::vector& explanation) { return conjunction; } -Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe) { +NodeTheoryPair TheoryEngine::getExplanationAndExplainer(TNode node) { Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl; bool polarity = node.getKind() != kind::NOT; @@ -1398,90 +1278,32 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe // 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; - 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; + return NodeTheoryPair(explanation, theoryOf(atom)->getId()); } - 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 - if (proofRecipe) { - Node emptyNode; - LemmaProofRecipe::ProofStep proofStep(explainer, emptyNode); - proofStep.addAssertion(node); - proofRecipe->addStep(proofStep); - proofRecipe->addBaseAssertion(node); - } - - getExplanation(explanationVector, proofRecipe); + getExplanation(explanationVector); Node explanation = mkExplanation(explanationVector); Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl; - return explanation; + return NodeTheoryPair(explanation, explainer); } Node TheoryEngine::getExplanation(TNode node) { - LemmaProofRecipe *dontCareRecipe = NULL; - return getExplanationAndRecipe(node, dontCareRecipe); + return getExplanationAndExplainer(node).node; } struct AtomsCollect { @@ -1584,7 +1406,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool removable, bool preprocess, theory::TheoryId atomsTo, - LemmaProofRecipe* proofRecipe) { + theory::TheoryId ownerTheory) { // For resource-limiting (also does a time check). // spendResource(); @@ -1634,10 +1456,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, } // assert to prop engine - d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, proofRecipe, node); + d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, ownerTheory, node); for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); - d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, proofRecipe, node); + d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, ownerTheory, node); } // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. @@ -1671,69 +1493,22 @@ 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, proofRecipe); + getExplanation(explanationVector); 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, proofRecipe); - + lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId); } else { // When only one theory, the conflict should need no processing Assert(properConflict(conflict)); - 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); + lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId); } - - PROOF({ - delete proofRecipe; - proofRecipe = NULL; - }); } void TheoryEngine::staticInitializeBVOptions(const std::vector& assertions) { @@ -1885,21 +1660,19 @@ bool TheoryEngine::donePPSimpITE(std::vector& assertions){ return result; } -void TheoryEngine::getExplanation(std::vector& explanationVector, LemmaProofRecipe* proofRecipe) { +void TheoryEngine::getExplanation(std::vector& explanationVector) +{ 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 - 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") << "[i=" << i << "] TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl; - + Debug("theory::explain") << "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()) { @@ -1913,7 +1686,6 @@ 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; } @@ -1932,26 +1704,10 @@ 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; - - 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); - } - } - }) - + ++ i; continue; } } @@ -1960,62 +1716,22 @@ 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) { d_unconstrainedSimp->processAssertions(assertions); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 53c4aac77..db94edd7c 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -50,7 +50,6 @@ namespace CVC4 { class ResourceManager; -class LemmaProofRecipe; /** * A pair of a theory and a node. This is used to mark the flow of @@ -271,18 +270,46 @@ class TheoryEngine { } } - void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException); + 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); + } - bool propagate(TNode literal) 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); + } theory::LemmaStatus lemma(TNode lemma, ProofRule rule, bool removable = false, bool preprocess = false, bool sendAtoms = false) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException); + 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); + } - theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) 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); + } void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { NodeManager* curr = NodeManager::currentNM(); @@ -429,7 +456,7 @@ class TheoryEngine { bool removable, bool preprocess, theory::TheoryId atomsTo, - LemmaProofRecipe* proofRecipe); + theory::TheoryId ownerTheory); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector& atoms, theory::TheoryId theory); @@ -579,10 +606,9 @@ 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. The lemmaProofRecipe will contain a list - * of the explanation steps required to produce the original node. + * theory that sent the literal. */ - void getExplanation(std::vector& explanationVector, LemmaProofRecipe* lemmaProofRecipe); + void getExplanation(std::vector& explanationVector); public: @@ -704,7 +730,7 @@ public: * Returns an explanation of the node propagated to the SAT solver and the theory * that propagated it. */ - Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe); + NodeTheoryPair getExplanationAndExplainer(TNode node); /** * collect model info diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 25b12f75f..9b429765e 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -964,9 +964,12 @@ 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()) { + 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); 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]); @@ -1189,9 +1192,6 @@ 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,7 +1605,6 @@ 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() << "):"; @@ -1619,7 +1618,6 @@ void EqualityEngine::debugPrintGraph() const { Debug("equality::graph") << std::endl; } - Debug("equality::graph") << std::endl; } bool EqualityEngine::areEqual(TNode t1, TNode t2) const { @@ -2211,15 +2209,9 @@ bool EqClassIterator::isFinished() const { return d_current == null_id; } -void EqProof::debug_print(const char* c, unsigned tb, PrettyPrinter* prettyPrinter) const { - for(unsigned i=0; iprintTag(d_id); - else - Debug( c ) << d_id; - - Debug( c ) << "("; +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, prettyPrinter ); + d_children[i]->debug_print( c, tb+1 ); } } Debug( c ) << ")" << std::endl; diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 843e7ce7f..f30f1e8a0 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -902,17 +902,11 @@ 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, PrettyPrinter* prettyPrinter = NULL) const; + void debug_print( const char * c, unsigned tb = 0 ) const; };/* class EqProof */ } // Namespace eq diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 9c461f57b..d1685bdd1 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,7 +533,6 @@ 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 38705c22a..38b58cedd 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -22,6 +22,7 @@ TESTS = \ bug00.smt \ bug338.smt2 \ bug347.smt \ + bug348.smt \ bug451.smt \ bug509.smt \ bug580.smt2 \ -- 2.30.2