diff options
| author | Andres Notzli <andres.noetzli@gmail.com> | 2016-08-04 17:39:53 -0700 |
|---|---|---|
| committer | Andres Notzli <andres.noetzli@gmail.com> | 2017-05-08 11:50:15 -0700 |
| commit | 992dffa1eba7ee1a8dc2000ae7bef45fdaee8d0c (patch) | |
| tree | 856e7ca89c94df676d0eed98af68c8dcf829829b | |
| parent | 5ab14e1abdff2cd4e75b3b698dc3d65fb07be3c1 (diff) | |
Support rewrite proofs
31 files changed, 2309 insertions, 60 deletions
diff --git a/proofs/lfsc_checker/trie.cpp b/proofs/lfsc_checker/trie.cpp index fedb508b0..5e25e1e90 100644 --- a/proofs/lfsc_checker/trie.cpp +++ b/proofs/lfsc_checker/trie.cpp @@ -12,7 +12,7 @@ public: template <> Trie<int>::Cleaner *Trie<int>::cleaner = new Simple; -void unit_test_trie() { +int main() { Trie<int> t; t.insert("a", 1); t.insert("b", 2); diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index 06dc16153..a4de73c7d 100644 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -215,9 +215,7 @@ (! f formula (th_holds (iff f f)))) - ;; contradiction - (declare contra (! f formula (! r1 (th_holds f) @@ -385,6 +383,99 @@ (! u2 (th_holds (not (ifte a b c))) (th_holds (or (not b) (not c)))))))) +(declare t_eq_n_f (th_holds (iff true (not false)))) +(declare n_t_eq_f (th_holds (iff (not true) false))) + +;; XXX: check whether x and y are constant +;; (program constants_are_disequal ((s sort) (x (term s)) (y (term s))) formula +;; (match x +;; (bvn (fail formula)) +;; ((bvc bx x') +;; (match y +;; (bvn (fail formula)) +;; ((bvc by y') (match bx +;; (b0 (match by (b0 (constants_are_disequal x' y')) (b1 (true)))) +;; (b1 (match by (b0 (true)) (b1 (constants_are_disequal x' y')))) +;; )) +;; )) +;; )) +;; +;; (declare disequal_constants +;; (! s sort +;; (! x (term s) +;; (! y (term s) +;; (! c (^ (constants_are_disequal x y) true) +;; (th_holds (not (= _ x y)))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; +; Rewrite proofs +; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; Apply a unary operator to the original and the rewritten formula +(declare symm_formula_op1 + (! op formula_op1 + (! x formula + (! y formula + (! u (th_holds (iff x y)) + (th_holds (iff (op x) (op y)))))))) + +; Apply a binary operator to the original and the rewritten formulas +(declare symm_formula_op2 + (! op formula_op2 + (! x formula + (! y formula + (! z formula + (! w formula + (! u1 (th_holds (iff x z)) + (! u2 (th_holds (iff y w)) + (th_holds (iff (op x y) (op z w))))))))))) + +; Apply a ternary operator to the original and the rewritten formulas +(declare symm_formula_op3 + (! op formula_op3 + (! x formula + (! y formula + (! z formula + (! w formula + (! a formula + (! b formula + (! u1 (th_holds (iff x w)) + (! u2 (th_holds (iff y a)) + (! u2 (th_holds (iff z b)) + (th_holds (iff (op x y z) (op w a b)))))))))))))) + +(declare iff_intro + (! s sort + (! x (term s) + (! y (term s) + (! z (term s) + (! w (term s) + (! lhs (th_holds (= _ x y)) + (! rhs (th_holds (= _ z w)) + (th_holds (iff (= _ x z) (= _ y w))))))))))) + +; (not true) --> false +(declare not_t + (! o formula + (! u (th_holds (iff o (not true))) + (th_holds (iff o false))))))) + +; (=> true false) --> false +(declare t_impl_f + (! o formula + (! u (th_holds (iff o (impl true false))) + (th_holds (iff o false))))))) + +; (= y y) --> true +(declare iff_true + (! s sort + (! x formula + (! y (term s) + (! u (th_holds (iff x (= _ y y))) + (th_holds (iff x true))))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; ; For theory lemmas diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf index acfbd2f3b..6dc330967 100644 --- a/proofs/signatures/th_arrays.plf +++ b/proofs/signatures/th_arrays.plf @@ -63,3 +63,28 @@ (! 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))))))) + +; Rewrites +(declare wor (! s18 sort + (! s19 sort + (! i (term s18) + (! oa (term (Array s18 s19)) + (! a (term (Array s18 s19)) + (! u (th_holds (= _ oa (apply _ _ (apply _ _ (apply _ _ (write s18 s19) a) i) (apply _ _ (apply _ _ (read s18 s19) a) i)))) + (th_holds (= _ oa a)))))))))) + +(declare wow (! s1 sort + (! s2 sort + (! i (term s1) + (! i2 (term s1) + (! v (term s2) + (! w (term s2) + (! w2 (term s2) + (! oa (term (Array s1 s2)) + (! a (term (Array s1 s2)) + (! a2 (term (Array s1 s2)) + (! u (th_holds (= _ oa (apply _ _ (apply _ _ (apply _ _ (write s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) a) i) v)) i) w))) + (! u1 (th_holds (= _ a a2)) + (! u2 (th_holds (= _ i i2)) + (! u3 (th_holds (= _ w w2)) + (th_holds (= _ oa (apply _ _ (apply _ _ (apply _ _ (write s1 s2) a2) i2) w2)))))))))))))))))) diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf index 6012e052a..7b036c341 100644 --- a/proofs/signatures/th_bv.plf +++ b/proofs/signatures/th_bv.plf @@ -37,10 +37,10 @@ (declare bvc (! b bit (! v bv bv))) ; calculate the length of a bitvector -;; (program bv_len ((v bv)) mpz -;; (match v -;; (bvn 0) -;; ((bvc b v') (mp_add (bv_len v') 1)))) +(program bv_len ((v bv)) mpz + (match v + (bvn 0) + ((bvc b v') (mp_add (bv_len v') 1)))) ; a bv constant term @@ -190,3 +190,285 @@ (declare bvsle bvpred) (declare bvsgt bvpred) (declare bvsge bvpred) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Rewrite support ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; check whether a constant bitvector is zero +(program bv_is_constant_zero ((x bv)) formula + (match x + (bvn (true)) + ((bvc bx x') + (match bx + (b0 (bv_is_constant_zero x')) + (b1 (fail formula)) + ) + ) + ) +) + +; check whether a constant bitvector is all ones +(program bv_is_constant_all_ones ((x bv)) formula + (match x + (bvn (true)) + ((bvc bx x') + (match bx + (b0 (fail formula)) + (b1 (bv_is_constant_all_ones x')) + ) + ) + ) +) + +; check whether a constant bitvector is a power of two +(program bv_is_constant_pow2 ((x bv)) formula + (match x + (bvn (fail formula)) + ((bvc bx x') + (match bx + (b0 (bv_is_constant_pow2 x')) + (b1 (bv_is_constant_zero x')) + ) + ) + ) +) + +; compute 2**len +; TODO: add native mp_pow to lfsc more efficiency? +(program pow2len ((x bv)) mpz + (match x + (bvn (fail mpz)) + ((bvc bx x') + (match x' + (bvn 1) + ((bvc bx' x'') (mp_mul 2 (pow2len x'))) + ) + ) + ) +) + +; convert bitvector constant to size +(program bv_const_to_size ((x bv)) mpz + (match x + (bvn 0) + ((bvc bx x') + (match bx + (b0 (bv_const_to_size x')) + (b1 (mp_add (pow2len x) (bv_const_to_size x'))) + ) + ) + ) +) + +; computes log2 of a bitvector constant and returns the result as a size +; NOTE: requires the bitvector to be a power of two +(program bv_const_log2 ((x bv)) mpz + (match x + (bvn (fail mpz)) + ((bvc bx x') + (match bx + (b0 (bv_const_log2 x')) + (b1 (bv_len x')) + ) + ) + ) +) + +(program swap_op2_ ((op formula_op2) (x formula) (other formula) (n mpz)) formula + (mp_ifzero n + (match x + ((op l r) (op l (op other r))) + (default (op x other)) + ) + (match x + ((op l r) + (match (swap_op2_ op r other (mp_add n (~1))) + ((op e new_r) (op e (op l new_r))) + (x (fail formula)) + ) + ) + (default (fail formula)) + ) + ) +) + +(program swap_op2 ((op formula_op2) (x formula) (n mpz) (m mpz)) formula + (mp_ifzero n + (match x + ((op l r) (swap_op2_ op r l (mp_add m (~1)))) + (default (fail formula)) + ) + (match x + ((op l r) (op l (swap_op2 op r (mp_add n (~1)) (mp_add m (~1))))) + (default (fail formula)) + ) + ) +) + +(declare do_swap_op2 + (! op formula_op2 + (! n mpz + (! m mpz + (! p formula + (! q formula + (! r formula + (! x (th_holds (iff p q)) + (! c (^ (swap_op2 op q n m) r) + (th_holds (iff p r))))))))))) + +(program get_op2 ((op formula_op2) (x formula) (n mpz)) formula + (mp_ifzero n + (match x + ((op l r) l) + (default x) + ) + (match x + ((op l r) (get_op2 op r (mp_add n (~1)))) + (default (fail formula)) + ) + ) +) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Test helpers ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(declare test_bv_is_constant_zero + (! x bv + (! c (^ (bv_is_constant_zero x) true) + (th_holds true)))) + +(declare test_bv_is_constant_all_ones + (! x bv + (! c (^ (bv_is_constant_all_ones x) true) + (th_holds true)))) + +(declare test_bv_is_constant_pow2 + (! x bv + (! c (^ (bv_is_constant_pow2 x) true) + (th_holds true)))) + +(declare test_pow2len + (! n mpz + (! x bv + (! c (^ (pow2len x) n) + (th_holds true))))) + +(declare test_bv_const_to_size + (! n mpz + (! x bv + (! c (^ (bv_const_to_size x) n) + (th_holds true))))) + +(declare test_bv_const_log2 + (! n mpz + (! x bv + (! c (^ (bv_const_log2 x) n) + (th_holds true))))) + +(declare test_swap_op2 + (! x formula + (! y formula + (! op formula_op2 + (! n mpz + (! m mpz + (! c (^ (swap_op2 op x n m) y) + (th_holds y)))))))) + +(declare test_get_op2 + (! x formula + (! op formula_op2 + (! n mpz + (! c (^ (get_op2 op x n) (iff true false)) + (th_holds true)))))))))) + +(declare test_nested_get_op2 + (! x formula + (! op formula_op2 + (! n mpz + (! c (^ (get_op2 op x n) (iff true false)) + (th_holds true)))))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; EXAMPLES +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; XXX: remove +; (declare shl_by_const_zero +; (! n mpz +; (! x (term (BitVec n)) +; (! y bv +; (! o (term (BitVec n)) +; (! u1 (th_holds (= _ o (bvshl n x (a_bv n y)))) +; (! u2 (^ (bv_is_constant_zero y) true) +; (th_holds (= _ o x))))))))) + +(declare shl_by_const_zero + (! n10 mpz + (! x (term (BitVec n10)) + (! XXXv0 bv + (! o (term (BitVec n10)) + (! u (th_holds (= _ o (bvshl _ x (a_bv _ XXXv0)))) + (! u (^ (bv_is_constant_zero XXXv0) true) + (th_holds (= _ o x))))))))) + +; XXX: remove +; (declare shl_by_const_more_than_len +; (! n mpz +; (! x (term (BitVec n)) +; (! y bv +; (! o (term (BitVec n)) +; (! r bv +; (! u1 (th_holds (= _ o (bvshl n x (a_bv n y)))) +; (! u2 (^ (mpz_lte n (bv_const_to_size y)) true) +; (! u3 (^ (bv_is_constant_zero r) true) +; (th_holds (= _ o (a_bv n r)))))))))))) + +(declare shl_by_const_more_than_len + (! n26 mpz + (! x (term (BitVec n26)) + (! y bv + (! o (term (BitVec n26)) + (! XXXv1 bv + (! u (th_holds (= _ o (bvshl _ x (a_bv _ y)))) + (! u (^ (mpz_lte (n26) (bv_const_to_size y)) true) + (! u (^ (bv_is_constant_zero XXXv1) true) + (th_holds (= _ o (a_bv _ XXXv1)))))))))))) + +; Name: SHL_BY_CONST +; Precond: const_bv(#y) +; (bvshl #x #y) --> (concat (extract #x (size(#x) - 1 - to_unsigned_int(#y)) 0) (bvconst(to_unsigned_int(#y), 0))) +; +; (declare shl_by_const +; (! n mpz +; (! x (term (BitVec n)) +; (! y bv +; (! o (term (BitVec n)) +; (! n1 mpz +; (! n2 mpz +; (! r bv +; (! u (th_holds (= _ o (bvshl x (a_bv y)))) +; (! u (^ (mpz_sub (mpz_sub n 1) (bv_const_to_size y)) n1) +; (! u (^ (bv_is_constant_zero r) true) +; (th_holds (= _ o (concat (extract n2 n1 0 _ x) (a_bv r))))))))))))) + + +(declare lshr_by_const_zero (! n48 mpz (! x (term (BitVec n48)) (! XXXv3 bv (! o (term (BitVec n48)) (! u (^ (bv_is_constant_zero XXXv3) true) (! u (th_holds (= _ o (bvlshr _ x (a_bv _ XXXv3)))) (th_holds (= _ o x))))))))) +(declare lshr_by_const_more_than_len (! n63 mpz (! y bv (! x (term (BitVec n63)) (! XXXv4 bv (! o (term (BitVec n63)) (! u (^ (mpz_lte (n63) (bv_const_to_size y)) true) (! u (^ (bv_is_constant_zero XXXv4) true) (! u (th_holds (= _ o (bvlshr _ x (a_bv _ y)))) (th_holds (= _ o (a_bv _ XXXv4)))))))))))) +(declare bitwise_idemp_and (! n68 mpz (! x (term (BitVec n68)) (! o (term (BitVec n68)) (! u (th_holds (= _ o (bvand n68 x x))) (th_holds (= _ o x))))))) +(declare bitwise_idemp_or (! n73 mpz (! x (term (BitVec n73)) (! o (term (BitVec n73)) (! u (th_holds (= _ o (bvor _ x x))) (th_holds (= _ o x))))))) +(declare and_zero_r (! n88 mpz (! XXXv6 bv (! x (term (BitVec n88)) (! XXXv5 bv (! o (term (BitVec n88)) (! u (^ (bv_is_constant_zero XXXv6) true) (! u (^ (bv_is_constant_zero XXXv5) true) (! u (th_holds (= _ o (bvand n88 x (a_bv _ XXXv5)))) (th_holds (= _ o (a_bv _ XXXv6)))))))))))) +(declare and_zero_l (! n103 mpz (! XXXv8 bv (! x (term (BitVec n103)) (! XXXv7 bv (! o (term (BitVec n103)) (! u (^ (bv_is_constant_zero XXXv8) true) (! u (^ (bv_is_constant_zero XXXv7) true) (! u (th_holds (= _ o (bvand n103 (a_bv _ XXXv7) x))) (th_holds (= _ o (a_bv _ XXXv8)))))))))))) +(declare bitwise_not_and_r (! n114 mpz (! x (term (BitVec n114)) (! XXXv9 bv (! o (term (BitVec n114)) (! u (^ (bv_is_constant_zero XXXv9) true) (! u (th_holds (= _ o (bvand n114 x (bvnot _ x)))) (th_holds (= _ o (a_bv _ XXXv9)))))))))) +(declare bitwise_not_and_l (! n125 mpz (! x (term (BitVec n125)) (! XXXv10 bv (! o (term (BitVec n125)) (! u (^ (bv_is_constant_zero XXXv10) true) (! u (th_holds (= _ o (bvand n125 (bvnot _ x) x))) (th_holds (= _ o (a_bv _ XXXv10)))))))))) +(declare not_idemp (! n130 mpz (! x (term (BitVec n130)) (! o (term (BitVec n130)) (! u (th_holds (= _ o (bvnot _ (bvnot _ x)))) (th_holds (= _ o x))))))) +(declare lt_self_ult (! n135 mpz (! x (term (BitVec n135)) (! o formula (! u (th_holds (iff o (bvult _ x x))) (th_holds (iff o (false)))))))) +(declare lt_self_slt (! n139 mpz (! x (term (BitVec n139)) (! o formula (! u (th_holds (iff o (bvslt _ x x))) (th_holds (iff o (false)))))))) +(declare lte_self_ule (! n143 mpz (! x (term (BitVec n143)) (! o formula (! u (th_holds (iff o (bvule _ x x))) (th_holds (iff o (true)))))))) +(declare lte_self_sle (! n147 mpz (! x (term (BitVec n147)) (! o formula (! u (th_holds (iff o (bvsle _ x x))) (th_holds (iff o (true)))))))) +(declare ugt_eliminate (! n155 mpz (! y (term (BitVec n155)) (! x (term (BitVec n155)) (! o formula (! u (th_holds (iff o (bvugt _ x y))) (th_holds (iff o (bvult _ y x))))))))) +(declare uge_eliminate (! n163 mpz (! y (term (BitVec n163)) (! x (term (BitVec n163)) (! o formula (! u (th_holds (iff o (bvuge _ x y))) (th_holds (iff o (bvule _ y x))))))))) +(declare sgt_eliminate (! n171 mpz (! y (term (BitVec n171)) (! x (term (BitVec n171)) (! o formula (! u (th_holds (iff o (bvsgt _ x y))) (th_holds (iff o (bvslt _ y x))))))))) +(declare sge_eliminate (! n179 mpz (! y (term (BitVec n179)) (! x (term (BitVec n179)) (! o formula (! u (th_holds (iff o (bvsge _ x y))) (th_holds (iff o (bvsle _ y x))))))))) diff --git a/src/Makefile.am b/src/Makefile.am index e44bd920c..991ef5bf3 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -94,6 +94,10 @@ libcvc4_la_SOURCES = \ proof/proof_output_channel.h \ proof/proof_utils.cpp \ proof/proof_utils.h \ + proof/rewrite_proof.cpp \ + proof/rewrite_proof.h \ + proof/rewrite_proof_dispatcher.cpp \ + proof/rewrite_proof_dispatcher.h \ proof/sat_proof.h \ proof/sat_proof_implementation.h \ proof/simplify_boolean_node.cpp \ diff --git a/src/compat/Makefile.am b/src/compat/Makefile.am index df4603a9a..46a9155d3 100644 --- a/src/compat/Makefile.am +++ b/src/compat/Makefile.am @@ -26,7 +26,7 @@ libcvc4compat_la_LDFLAGS = \ libcvc4compat_la_LIBADD = \ @builddir@/../libcvc4.la \ - @builddir@/../parser/libcvc4parser.la \ + @builddir@/../parser/libcvc4parser.la @builddir@/../lib/libreplacements.la libcvc4compat_la_SOURCES = \ diff --git a/src/lib/Makefile.am b/src/lib/Makefile.am index 8db3d664c..1036e7169 100644 --- a/src/lib/Makefile.am +++ b/src/lib/Makefile.am @@ -7,7 +7,6 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libreplacements.la libreplacements_la_SOURCES = - libreplacements_la_LIBADD = \ $(LTLIBOBJS) diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 372e817f6..00c77ffc0 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -30,9 +30,8 @@ pcvc4_LDADD = \ libmain.a \ @builddir@/../parser/libcvc4parser.la \ @builddir@/../libcvc4.la \ - $(READLINE_LIBS) \ + $(READLINE_LIBS) @builddir@/../lib/libreplacements.la - pcvc4_CPPFLAGS = $(AM_CPPFLAGS) $(BOOST_CPPFLAGS) -DPORTFOLIO_BUILD pcvc4_LDADD += $(BOOST_THREAD_LIBS) pcvc4_LDADD += $(BOOST_THREAD_LDFLAGS) @@ -52,7 +51,7 @@ cvc4_LDADD = \ libmain.a \ @builddir@/../parser/libcvc4parser.la \ @builddir@/../libcvc4.la \ - $(READLINE_LIBS) \ + $(READLINE_LIBS) @builddir@/../lib/libreplacements.la BUILT_SOURCES = \ diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index ca10de684..b16028f87 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -29,7 +29,7 @@ libcvc4parser_la_LIBADD = \ @builddir@/smt2/libparsersmt2.la \ @builddir@/tptp/libparsertptp.la \ @builddir@/cvc/libparsercvc.la \ - @builddir@/../libcvc4.la \ + @builddir@/../libcvc4.la @builddir@/../lib/libreplacements.la libcvc4parser_la_SOURCES = \ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index b5bad6a2d..477cd940d 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -522,6 +522,8 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { #include "parser/parser.h" #include "util/integer.h" +#define _empty NULL + }/* @lexer::includes */ @parser::includes { diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g index 28c54fc80..eb7e918bd 100644 --- a/src/parser/smt1/Smt1.g +++ b/src/parser/smt1/Smt1.g @@ -62,6 +62,8 @@ options { #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ #include "parser/antlr_tracing.h" + +#define _empty NULL }/* @lexer::includes */ @parser::includes { diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a49190825..779715ca5 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -63,6 +63,8 @@ options { #include "parser/antlr_tracing.h" +#define _empty NULL + }/* @lexer::includes */ @lexer::postinclude { diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index cbc7f591a..9647668a8 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -25,6 +25,7 @@ #include "proof/clause_id.h" #include "proof/cnf_proof.h" #include "proof/proof_utils.h" +#include "proof/rewrite_proof_dispatcher.h" #include "proof/sat_proof_implementation.h" #include "proof/theory_proof.h" #include "smt/smt_engine.h" @@ -758,8 +759,6 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, for (; it != end; ++it) { // Rewrite preprocessing step if it cannot be eliminated if (!ProofManager::currentPM()->have_input_assertion((*it).toExpr())) { - os << "(th_let_pf _ (trust_f (iff "; - Expr inputAssertion; if (((*it).isConst() && *it == NodeManager::currentNM()->mkConst<bool>(true)) || @@ -802,12 +801,20 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, << ", AKA " << ProofManager::currentPM()->getInputFormulaName(inputAssertion) << std::endl; + os << "(th_let_pf _ "; + RewriteProof rp; + if ((*it).getKind() == kind::NOT && (*it)[0] == NodeManager::currentNM()->mkConst<bool>(false)) { + os << "t_eq_n_f "; + } else if (theory::Rewriter::rewriteWithProof(inputAssertion, &rp) == *it) { + printProof(ProofManager::currentPM()->getTheoryProofEngine(), rp, os, globalLetMap); + } else { + os << "(trust_f (iff "; + ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm(inputAssertion, os, globalLetMap); + os << " "; + ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap); + os << ")) "; + } - ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm(inputAssertion, os, globalLetMap); - os << " "; - ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap); - - os << "))"; os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; paren << "))"; diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 31638e8ee..e105a849c 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -31,7 +31,7 @@ #include "theory/logic_info.h" #include "theory/substitutions.h" #include "util/proof.h" - +#include "proof/rewrite_proof.h" namespace CVC4 { @@ -68,6 +68,7 @@ class UFProof; class ArithProof; class ArrayProof; class BitVectorProof; +class RewriteProof; template <class Solver> class LFSCSatProof; typedef LFSCSatProof< CVC4::Minisat::Solver> LFSCCoreSatProof; diff --git a/src/proof/rewrite_proof.cpp b/src/proof/rewrite_proof.cpp new file mode 100644 index 000000000..15e79d1e0 --- /dev/null +++ b/src/proof/rewrite_proof.cpp @@ -0,0 +1,157 @@ +#include "proof/rewrite_proof.h" + +#include "proof/rewrite_proof_dispatcher.h" +#include "proof_manager.h" +#include "theory/rewriter.h" + +namespace CVC4 { + +Rewrite::~Rewrite() { + for (size_t i = 0; i < d_subproofs.size(); i++) { + delete d_subproofs[i]; + } +} + +void Rewrite::deleteUncachedChildren() { + for (size_t i = 0; i < d_children.size(); i++) { + if (d_children[i] != NULL) { + d_children[i]->deleteUncachedChildren(); + if (!d_children[i]->d_cached_version_used) { + delete d_children[i]; + d_children[i] = NULL; + } + } + } +} + +void Rewrite::print(int tab) const { + for (int j = 0; j < tab; j++) + std::cout << " "; + std::cout << d_tag << " > " << d_original << " < " << std::endl; + + for (size_t i = 0; i < d_children.size(); i++) { + d_children[i]->print(tab + 1); + std::cout << std::endl; + } +} + +RewriteProof::~RewriteProof() { + for (ProofCacheIterator iter = preRewriteCache.begin(); + iter != preRewriteCache.end(); ++iter) { + if (!iter->second->d_cached_version_used) { + preRewriteCache[iter->first] = NULL; + } + } + /* + for (ProofCacheIterator iter = postRewriteCache.begin(); + iter != postRewriteCache.end(); ++iter) { + if (!iter->second->d_cached_version_used) { + postRewriteCache[iter->first] = NULL; + } + }*/ + + for (size_t i = 0; i < d_rewrites.size(); i++) { + d_rewrites[i]->deleteUncachedChildren(); + if (!d_rewrites[i]->d_cached_version_used) { + delete d_rewrites[i]; + } + } + + for (ProofCacheIterator iter = preRewriteCache.begin(); + iter != preRewriteCache.end(); ++iter) { + if (iter->second != NULL) { + delete iter->second; + } + } + /* + for (ProofCacheIterator iter = postRewriteCache.begin(); + iter != postRewriteCache.end(); ++iter) { + if (iter->second != NULL) { + delete iter->second; + } + }*/ +} + +void RewriteProof::attachSubproofToParent() { + Rewrite *topRewrite = d_rewrites.back(); + + // Simplify proof + if (topRewrite->d_tag == ORIGINAL_OP) { + bool allChildrenRefl = true; + for (size_t i = 0; i < topRewrite->d_children.size(); i++) { + if (topRewrite->d_children[i]->d_tag != ORIGINAL_OP) { + allChildrenRefl = false; + break; + } + } + if (allChildrenRefl) { + topRewrite->d_children.clear(); + } + } + d_rewrites[d_rewrites.size() - 2]->d_children.push_back(d_rewrites.back()); + d_rewrites.pop_back(); +} + +Rewrite *RewriteProof::getRewrite() const { + Assert(d_rewrites.size() == 1); + return d_rewrites[0]; +} + +void RewriteProof::registerRewrite(const int tag) { + Rewrite *topRewrite = d_rewrites.back(); + d_rewrites.pop_back(); + Rewrite *newRewrite = new Rewrite(tag, topRewrite->d_original); + newRewrite->d_children.push_back(topRewrite); + d_rewrites.push_back(newRewrite); +} + +void RewriteProof::registerSwap(const unsigned swap_id1, const unsigned swap_id2) { + // Register swap if it does not swap head with head + if (swap_id1 != swap_id2) { + Rewrite *topRewrite = d_rewrites.back(); + d_rewrites.pop_back(); + Rewrite *newRewrite = new Rewrite(SWAP, topRewrite->d_original); + newRewrite->swap_id1 = swap_id1; + newRewrite->swap_id2 = swap_id2; + newRewrite->d_children.push_back(topRewrite); + d_rewrites.push_back(newRewrite); + } +} + +void RewriteProof::replaceRewrite(Rewrite *rewrite) { + // XXX: make sure that this is always safe + delete d_rewrites.back(); + d_rewrites.back() = rewrite; +} + +Rewrite *RewriteProof::getPreRewriteCache(Node node) { + return NULL; //preRewriteCache[node]; +} + +Rewrite *RewriteProof::getPostRewriteCache(Node node) { + return NULL; //postRewriteCache[node]; +} + +void RewriteProof::setPreRewriteCache(Node node, Rewrite *rewrite) { + preRewriteCache[node] = rewrite; +} + +void RewriteProof::setPostRewriteCache(Node node, Rewrite *rewrite) { + postRewriteCache[node] = rewrite; +} + +void RewriteProof::printCachedProofs(TheoryProofEngine *tp, std::ostream &os, + std::ostream &paren, + ProofLetMap &globalLetMap) const { + for (ProofCacheIterator iter = preRewriteCache.begin(); + iter != preRewriteCache.end(); ++iter) { + if (iter->second->d_cached_version_used) { + os << std::endl; + os << "(@ let" << iter->second->d_id << " "; + callPrintRewriteProof(false, tp, iter->second, os, globalLetMap); + paren << ")"; + } + } +} + +} /* CVC4 namespace */ diff --git a/src/proof/rewrite_proof.h b/src/proof/rewrite_proof.h new file mode 100644 index 000000000..5701e019a --- /dev/null +++ b/src/proof/rewrite_proof.h @@ -0,0 +1,86 @@ +#include "cvc4_private.h" + +#pragma once + +#include "expr/node.h" +#include "proof/theory_proof.h" +#include "util/proof.h" + +namespace CVC4 { + +typedef int rewrite_tag_t; + +// Theory independent rewrites +enum SharedRewrites { + ORIGINAL_OP, // Mirror an original operator + TRUSTED, + SWAP, + LAST_SHARED, +}; + +struct Rewrite { + // The type of the rewrite + int d_tag; + // Node before the rewrite + Node d_original; + // Rewrite proofs for children + std::vector<Rewrite *> d_children; + // Subproofs + std::vector<Rewrite *> d_subproofs; + // Unique id to identify the rewrite + unsigned d_id; + // Stores whether the cached version of this rewrite is ever used + bool d_cached_version_used; + // XXX: refactor into seperate class + unsigned swap_id1, swap_id2; + + Rewrite(const Node original) + : d_tag(0), d_original(original), d_cached_version_used(false) { + d_id = ProofLetCount::newId(); + } + Rewrite(const rewrite_tag_t tag, const Node original) + : d_tag(tag), d_original(original), d_cached_version_used(false) { + d_id = ProofLetCount::newId(); + } + ~Rewrite(); + + void deleteUncachedChildren(); + void print(int tab) const; + bool isLeaf() const { return d_children.size() == 0; } +}; + +typedef __gnu_cxx::hash_map<Node, Rewrite *, NodeHashFunction> ProofCache; +typedef __gnu_cxx::hash_map<Node, Rewrite *, NodeHashFunction>::const_iterator + ProofCacheIterator; + +class RewriteProof { +private: + std::vector<Rewrite *> d_rewrites; + ProofCache preRewriteCache; + ProofCache postRewriteCache; + +public: + RewriteProof() {} + ~RewriteProof(); + + void addRewrite(Rewrite *rewrite) { d_rewrites.push_back(rewrite); } + + void attachSubproofToParent(); + + Rewrite *getRewrite() const; + Rewrite *getTopRewrite() const { return d_rewrites.back(); }; + + void registerRewrite(const int tag); + void registerSwap(const unsigned swap_id1, const unsigned swap_id2); + void replaceRewrite(Rewrite *rewrite); + + Rewrite *getPreRewriteCache(Node node); + Rewrite *getPostRewriteCache(Node node); + void setPreRewriteCache(Node node, Rewrite *rewrite); + void setPostRewriteCache(Node node, Rewrite *rewrite); + + void printCachedProofs(TheoryProofEngine *tp, std::ostream &os, + std::ostream &paren, ProofLetMap &globalLetMap) const; +}; + +} /* CVC4 namespace */ diff --git a/src/proof/rewrite_proof_dispatcher.cpp b/src/proof/rewrite_proof_dispatcher.cpp new file mode 100644 index 000000000..3b01719d2 --- /dev/null +++ b/src/proof/rewrite_proof_dispatcher.cpp @@ -0,0 +1,83 @@ +// TODO: decide whether this should be part of rewriter_tables +#include "proof/rewrite_proof_dispatcher.h" + +#include "theory/arrays/theory_arrays_rewriter.h" +#include "theory/booleans/theory_bool_rewriter.h" + +namespace CVC4 { + +void printProof(TheoryProofEngine *tp, const RewriteProof &rp, std::ostream &os, + ProofLetMap &globalLetMap) { + std::ostringstream paren; + rp.printCachedProofs(tp, os, paren, globalLetMap); + os << std::endl; + callPrintRewriteProof(true, tp, rp.getRewrite(), os, globalLetMap); + os << paren.str(); +} + +theory::RewriteResponse callPreRewriteWithProof(theory::TheoryId theory, + TNode node, + RewriteProof *proof) { + Assert(proof); + switch (theory) { + case theory::THEORY_ARRAY: + return theory::arrays::TheoryArraysRewriter::preRewriteEx<true>(node, + proof); + + case theory::THEORY_BOOL: + return theory::booleans::TheoryBoolRewriter::preRewriteEx<true>(node, + proof); + + default: + Unreachable(); + } +} + +theory::RewriteResponse callPostRewriteWithProof(theory::TheoryId theory, + TNode node, + RewriteProof *proof) { + Assert(proof); + switch (theory) { + case theory::THEORY_ARRAY: + return theory::arrays::TheoryArraysRewriter::postRewriteEx<true>(node, + proof); + + case theory::THEORY_BOOL: + return theory::booleans::TheoryBoolRewriter::postRewriteEx<true>(node, + proof); + + default: + Unreachable(); + } +} + +void callPrintRewriteProof(bool use_cache, TheoryProofEngine *tp, + const Rewrite *rewrite, std::ostream &os, + ProofLetMap &globalLetMap) { + if (use_cache && rewrite->d_cached_version_used) { + os << "let" << rewrite->d_id; + return; + } + + switch (theory::theoryOf(rewrite->d_original)) { + case theory::THEORY_ARRAY: + theory::arrays::TheoryArraysRewriter::printRewriteProof( + use_cache, tp, rewrite, os, globalLetMap); + break; + + case theory::THEORY_BOOL: + theory::booleans::TheoryBoolRewriter::printRewriteProof( + use_cache, tp, rewrite, os, globalLetMap); + break; + + default: + for (size_t i = 0; i < rewrite->d_children.size(); i++) { + callPrintRewriteProof(use_cache, tp, rewrite->d_children[i], os, + globalLetMap); + std::cout << std::endl; + } + break; + } +} + +} /* CVC4 namespace */ diff --git a/src/proof/rewrite_proof_dispatcher.h b/src/proof/rewrite_proof_dispatcher.h new file mode 100644 index 000000000..8c1202c16 --- /dev/null +++ b/src/proof/rewrite_proof_dispatcher.h @@ -0,0 +1,28 @@ +// TODO: decide whether this should be part of rewriter_tables +#include "cvc4_private.h" + +#pragma once + +#include "expr/node.h" +#include "proof/theory_proof.h" +#include "theory/rewriter.h" +#include "util/proof.h" + +namespace CVC4 { + +void printProof(TheoryProofEngine *tp, const RewriteProof &rp, std::ostream &os, + ProofLetMap &globalLetMap); + +theory::RewriteResponse callPreRewriteWithProof(theory::TheoryId theory, + TNode node, + RewriteProof *proof); + +theory::RewriteResponse callPostRewriteWithProof(theory::TheoryId theory, + TNode node, + RewriteProof *proof); + +void callPrintRewriteProof(bool use_cache, TheoryProofEngine *tp, + const Rewrite *rewrite, std::ostream &os, + ProofLetMap &globalLetMap); + +} /* CVC4 namespace */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 31b62f25a..bdffad056 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2861,6 +2861,8 @@ bool SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "asserting to propagator" << endl; for (unsigned i = 0; i < d_assertions.size(); ++ i) { + //std::cout << Rewriter::rewrite(d_assertions[i]) << std::endl; + //std::cout << d_assertions[i] << std::endl; Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]); // Don't reprocess substitutions if (d_substitutionsIndex > 0 && i == d_substitutionsIndex) { diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp index f1cf1d320..8a17a62eb 100644 --- a/src/theory/arrays/theory_arrays_rewriter.cpp +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -17,11 +17,80 @@ #include "expr/attribute.h" #include "theory/arrays/theory_arrays_rewriter.h" +#include "proof/rewrite_proof_dispatcher.h" namespace CVC4 { namespace theory { namespace arrays { +void TheoryArraysRewriter::printRewriteProof(bool use_cache, + TheoryProofEngine* tp, + const Rewrite* rewrite, + std::ostream& os, + ProofLetMap& globalLetMap) { + if (rewrite->d_tag == ORIGINAL_OP && rewrite->d_children.size() == 0) { + switch (rewrite->d_original.getKind()) { + case kind::EQUAL: + os << "(iff_symm "; + tp->printTheoryTerm(rewrite->d_original.toExpr(), os, globalLetMap); + os << ")"; + break; + default: + os << "(refl _ "; + tp->printTheoryTerm(rewrite->d_original.toExpr(), os, globalLetMap); + os << ")"; + break; + } + } else if (rewrite->d_tag == EQ) { + os << "(iff_true _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ORIGINAL_OP) { + switch (rewrite->d_original.getKind()) { + case kind::EQUAL: + os << "(iff_intro _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, globalLetMap); + os << " "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[1], os, globalLetMap); + os << ")"; + break; + case kind::SELECT: + os << "(cong _ _ _ _ _ _ (cong _ _ _ _ _ _ "; + os << "(refl _ (read "; + tp->printSort(ArrayType(rewrite->d_original.toExpr()[0].getType()).getIndexType(), os); + os << " "; + tp->printSort(ArrayType(rewrite->d_original.toExpr()[0].getType()).getConstituentType(), os); + os << ")) "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, globalLetMap); + os << ") "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[1], os, globalLetMap); + os << ")"; + break; + default: + std::cout << "ERROR!" << rewrite->d_original.getKind() << std::endl; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, globalLetMap); + Unreachable(); + } + } else if (rewrite->d_tag == WOR) { + os << "(wor _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, globalLetMap); + os << ")"; + } else if (rewrite->d_tag == WOW) { + os << "(wow _ _ _ _ _ _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, globalLetMap); + os << " "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[1], os, globalLetMap); + os << " "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[2], os, globalLetMap); + os << " "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[3], os, globalLetMap); + os << ")"; + } else { + std::cout << "ERROR" << rewrite->d_tag << std::endl; + Unreachable(); + } +} + namespace attr { struct ArrayConstantMostFrequentValueTag { }; struct ArrayConstantMostFrequentValueCountTag { }; diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index e63c224a0..ef4e49def 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -40,7 +40,14 @@ class TheoryArraysRewriter { static Node normalizeConstant(TNode node) { return normalizeConstant(node, node[1].getType().getCardinality()); } + public: + enum ArraysRewrites { + WOR = LAST_SHARED, + WOW, + EQ + }; + //this function is called by printers when using the option "--model-u-dt-enum" static Node normalizeConstant(TNode node, Cardinality indexCard) { TNode store = node[0]; @@ -228,7 +235,13 @@ public: public: - static RewriteResponse postRewrite(TNode node) { + static inline RewriteResponse postRewrite(TNode node) { + return postRewriteEx<false>(node, NULL); + } + + template<bool Proof> + static RewriteResponse postRewriteEx(TNode node, RewriteProof* proof) { + Assert(!Proof || proof != NULL); Trace("arrays-postrewrite") << "Arrays::postRewrite start " << node << std::endl; switch (node.getKind()) { case kind::SELECT: { @@ -281,6 +294,9 @@ public: value[0] == store && value[1] == node[1]) { Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << store << std::endl; + if (Proof) { + proof->registerRewrite(WOR); + } return RewriteResponse(REWRITE_DONE, store); } TNode index = node[1]; @@ -380,6 +396,9 @@ public: case kind::EQUAL:{ if(node[0] == node[1]) { Trace("arrays-postrewrite") << "Arrays::postRewrite returning true" << std::endl; + if (Proof) { + proof->registerRewrite(EQ); + } return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); } else if (node[0].isConst() && node[1].isConst()) { @@ -401,6 +420,12 @@ public: } static inline RewriteResponse preRewrite(TNode node) { + return preRewriteEx<false>(node, NULL); + } + + template<bool Proof> + static inline RewriteResponse preRewriteEx(TNode node, RewriteProof* proof) { + Assert(!Proof || proof != NULL); Trace("arrays-prerewrite") << "Arrays::preRewrite start " << node << std::endl; switch (node.getKind()) { case kind::SELECT: { @@ -453,6 +478,9 @@ public: value[0] == store && value[1] == node[1]) { Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << store << std::endl; + if (Proof) { + proof->registerRewrite(WOR); + } return RewriteResponse(REWRITE_AGAIN, store); } if (store.getKind() == kind::STORE) { @@ -477,6 +505,9 @@ public: // store(store(a,i,v),i,w) = store(a,i,w) Node newNode = nm->mkNode(kind::STORE, store[0], index, value); Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << newNode << std::endl; + if (Proof) { + proof->registerRewrite(WOW); + } return RewriteResponse(REWRITE_DONE, newNode); } } @@ -485,6 +516,9 @@ public: case kind::EQUAL:{ if(node[0] == node[1]) { Trace("arrays-prerewrite") << "Arrays::preRewrite returning true" << std::endl; + if (Proof) { + proof->registerRewrite(EQ); + } return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); } break; @@ -497,6 +531,12 @@ public: return RewriteResponse(REWRITE_DONE, node); } + static void printRewriteProof(bool use_cache, + TheoryProofEngine* tp, + const Rewrite* rewrite, + std::ostream& os, + ProofLetMap& globalLetMap); + static inline void init() {} static inline void shutdown() {} diff --git a/src/theory/booleans/bool.h b/src/theory/booleans/bool.h new file mode 100644 index 000000000..8654a63d8 --- /dev/null +++ b/src/theory/booleans/bool.h @@ -0,0 +1,1085 @@ + +#include "cvc4_private.h" + +#pragma once + +#include "proof/rewrite_proof_dispatcher.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { + +enum bool_Rewrites { + NOT_TRUE = LAST_SHARED, + NOT_FALSE, + NOT_NOT, + OR_TRUE, + OR_FALSE, + OR_DUP, + AND_FALSE, + AND_TRUE, + AND_DUP, + FALSE_IMPLIES, + IMPLIES_TRUE, + TRUE_IMPLIES_FALSE, + TRUE_IMPLIES, + IMPLIES_FALSE, + TRUE_EQ, + FALSE_EQ, + X_EQ_X, + N_X_EQ_X, + EQ_EQ_CONSTS, + EQ_NEQ_CONSTS_CARD2, + EQ_NEQ_CONSTS, + TRUE_XOR, + FALSE_XOR, + X_XOR_X, + N_X_XOR_X, + ITE_TRUE, + ITE_FALSE, + ITE_X_TRUE_FALSE, + ITE_C_FALSE_TRUE, + ITE_C_X_X, + ITE_C_X_N_X, + ITE_C_N_X_X, + ITE_X_X_Y, + ITE_N_X_X_Y, + ITE_X_N_X_Y, + ITE_X_Y_X, + ITE_N_X_Y_X, + ITE_X_Y_N_X, + ITE_C_ITE_C_X_Y_Z, + ITE_C_ITE_N_C_X_Y_Z, + ITE_N_C_ITE_C_X_Y_Z, + ITE_C_Z_ITE_C_X_Y, + ITE_C_Z_ITE_N_C_X_Y, + ITE_N_C_Z_ITE_C_X_Y +}; + +template <bool Proof> +inline RewriteResponse rewrite1(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_AGAIN, node); +} + +template <bool Proof> +inline RewriteResponse rewrite2(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + if ((node).getKind() == kind::ITE) { + if (((node[0]).getKind() == kind::CONST_BOOLEAN) && (true)) { + if (node[0] == nm->mkConst(true)) { + if (Proof) { + proof->registerRewrite(ITE_TRUE); + }; + Node rewritten_node = node[1]; + return rewrite1<Proof>(rewritten_node, proof); + }; + if (node[0] == nm->mkConst(false)) { + if (Proof) { + proof->registerRewrite(ITE_FALSE); + }; + Node rewritten_node = node[2]; + return rewrite1<Proof>(rewritten_node, proof); + } + }; + if (((node[1]).getKind() == kind::CONST_BOOLEAN) && + ((node[2]).getKind() == kind::CONST_BOOLEAN) && (true)) { + if ((node[1] == nm->mkConst(true)) && (node[2] == nm->mkConst(false))) { + if (Proof) { + proof->registerRewrite(ITE_X_TRUE_FALSE); + }; + Node rewritten_node = node[0]; + return rewrite1<Proof>(rewritten_node, proof); + }; + if ((node[1] == nm->mkConst(false)) && (node[2] == nm->mkConst(true))) { + if (Proof) { + proof->registerRewrite(ITE_C_FALSE_TRUE); + }; + Node rewritten_node = nm->mkNode(kind::NOT, node[0]); + return rewrite1<Proof>(rewritten_node, proof); + } + }; + if ((true) && (node[1] == node[2])) { + if (Proof) { + proof->registerRewrite(ITE_C_X_X); + }; + Node rewritten_node = node[1]; + return rewrite1<Proof>(rewritten_node, proof); + }; + if (((node[2]).getKind() == kind::NOT) && (true) && + (node[1] == node[2][0])) { + if (Proof) { + proof->registerRewrite(ITE_C_X_N_X); + }; + Node rewritten_node = nm->mkNode(kind::EQUAL, node[0], node[1]); + return rewrite1<Proof>(rewritten_node, proof); + }; + if (((node[1]).getKind() == kind::NOT) && (true) && + (node[1][0] == node[2])) { + if (Proof) { + proof->registerRewrite(ITE_C_N_X_X); + }; + Node rewritten_node = + nm->mkNode(kind::EQUAL, node[0], nm->mkNode(kind::NOT, node[1][0])); + return rewrite1<Proof>(rewritten_node, proof); + }; + if ((!((node[0]).isConst())) && (node[0] == node[1])) { + if (Proof) { + proof->registerRewrite(ITE_X_X_Y); + }; + Node rewritten_node = + nm->mkNode(kind::ITE, node[0], nm->mkConst(true), node[2]); + return rewrite1<Proof>(rewritten_node, proof); + }; + if (((node[0]).getKind() == kind::NOT) && (!((node[0][0]).isConst())) && + (node[0][0] == node[1])) { + if (Proof) { + proof->registerRewrite(ITE_N_X_X_Y); + }; + Node rewritten_node = + nm->mkNode(kind::ITE, nm->mkNode(kind::NOT, node[0][0]), + nm->mkConst(false), node[2]); + return rewrite1<Proof>(rewritten_node, proof); + }; + if (((node[1]).getKind() == kind::NOT) && (!((node[0]).isConst())) && + (node[0] == node[1][0])) { + if (Proof) { + proof->registerRewrite(ITE_X_N_X_Y); + }; + Node rewritten_node = + nm->mkNode(kind::ITE, node[0], nm->mkConst(false), node[2]); + return rewrite1<Proof>(rewritten_node, proof); + }; + if ((!((node[0]).isConst())) && (node[0] == node[2])) { + if (Proof) { + proof->registerRewrite(ITE_X_Y_X); + }; + Node rewritten_node = + nm->mkNode(kind::ITE, node[0], node[1], nm->mkConst(false)); + return rewrite1<Proof>(rewritten_node, proof); + }; + if (((node[0]).getKind() == kind::NOT) && (!((node[0][0]).isConst())) && + (node[0][0] == node[2])) { + if (Proof) { + proof->registerRewrite(ITE_N_X_Y_X); + }; + Node rewritten_node = + nm->mkNode(kind::ITE, nm->mkNode(kind::NOT, node[0][0]), node[1], + nm->mkConst(true)); + return rewrite1<Proof>(rewritten_node, proof); + }; + if (((node[2]).getKind() == kind::NOT) && (!((node[0]).isConst())) && + (node[0] == node[2][0])) { + if (Proof) { + proof->registerRewrite(ITE_X_Y_N_X); + }; + Node rewritten_node = + nm->mkNode(kind::ITE, node[0], node[1], nm->mkConst(true)); + return rewrite1<Proof>(rewritten_node, proof); + }; + if ((node[1]).getKind() == kind::ITE) { + if ((true) && (node[0] == node[1][0])) { + if (Proof) { + proof->registerRewrite(ITE_C_ITE_C_X_Y_Z); + }; + Node rewritten_node = + nm->mkNode(kind::ITE, node[0], node[1][1], node[2]); + return rewrite1<Proof>(rewritten_node, proof); + }; + if (((node[1][0]).getKind() == kind::NOT) && (true) && + (node[0] == node[1][0][0])) { + if (Proof) { + proof->registerRewrite(ITE_C_ITE_N_C_X_Y_Z); + }; + Node rewritten_node = + nm->mkNode(kind::ITE, node[0], node[1][2], node[2]); + return rewrite1<Proof>(rewritten_node, proof); + } + }; + if (((node[0]).getKind() == kind::NOT) && + ((node[1]).getKind() == kind::ITE) && (true) && + (node[0][0] == node[1][0])) { + if (Proof) { + proof->registerRewrite(ITE_N_C_ITE_C_X_Y_Z); + }; + Node rewritten_node = + nm->mkNode(kind::ITE, node[0][0], node[1][2], node[2]); + return rewrite1<Proof>(rewritten_node, proof); + }; + if ((node[2]).getKind() == kind::ITE) { + if ((true) && (node[0] == node[2][0])) { + if (Proof) { + proof->registerRewrite(ITE_C_Z_ITE_C_X_Y); + }; + Node rewritten_node = + nm->mkNode(kind::ITE, node[0], node[1], node[2][2]); + return rewrite1<Proof>(rewritten_node, proof); + }; + if (((node[2][0]).getKind() == kind::NOT) && (true) && + (node[0] == node[2][0][0])) { + if (Proof) { + proof->registerRewrite(ITE_C_Z_ITE_N_C_X_Y); + }; + Node rewritten_node = + nm->mkNode(kind::ITE, node[0], node[1], node[2][1]); + return rewrite1<Proof>(rewritten_node, proof); + } + }; + if (((node[0]).getKind() == kind::NOT) && + ((node[2]).getKind() == kind::ITE) && (true) && + (node[0][0] == node[2][0])) { + if (Proof) { + proof->registerRewrite(ITE_N_C_Z_ITE_C_X_Y); + }; + Node rewritten_node = + nm->mkNode(kind::ITE, node[0][0], node[1], node[2][1]); + return rewrite1<Proof>(rewritten_node, proof); + } + }; + return RewriteResponse(REWRITE_DONE, node); +} + +template <bool Proof> +inline RewriteResponse rewrite3(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_DONE, node); +} + +template <bool Proof> +inline RewriteResponse rewrite4(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + if (((node).getKind() == kind::XOR) && (true)) { + for (unsigned in_tmp352 = 0, in_tmp352_end = node.getNumChildren(); + in_tmp352 < in_tmp352_end; in_tmp352++) { + TNode n_tmp352 = node[in_tmp352]; + + for (unsigned in_tmp351 = 0, in_tmp351_end = node.getNumChildren(); + in_tmp351 < in_tmp351_end; in_tmp351++) { + TNode n_tmp351 = node[in_tmp351]; + if (!(in_tmp352 == in_tmp351)) { + if (n_tmp351 == n_tmp352) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(X_XOR_X); + }; + Node rewritten_node = nm->mkConst(false); + return rewrite3<Proof>(rewritten_node, proof); + }; + if (((n_tmp351).getKind() == kind::NOT) && + (n_tmp351[0] == n_tmp352)) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(N_X_XOR_X); + }; + Node rewritten_node = nm->mkConst(true); + return rewrite3<Proof>(rewritten_node, proof); + } + } + } + } + }; + return rewrite2<Proof>(node, proof); +} + +template <bool Proof> +inline RewriteResponse rewrite5(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_AGAIN, node); +} + +template <bool Proof> +inline RewriteResponse rewrite6(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + if (((node).getKind() == kind::XOR) && (true)) { + for (unsigned in_tmp348 = 0, in_tmp348_end = node.getNumChildren(); + in_tmp348 < in_tmp348_end; in_tmp348++) { + TNode n_tmp348 = node[in_tmp348]; + + for (unsigned in_tmp347 = 0, in_tmp347_end = node.getNumChildren(); + in_tmp347 < in_tmp347_end; in_tmp347++) { + TNode n_tmp347 = node[in_tmp347]; + if ((!(in_tmp348 == in_tmp347)) && + ((n_tmp347).getKind() == kind::CONST_BOOLEAN)) { + if (n_tmp347 == nm->mkConst(true)) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(TRUE_XOR); + }; + Node rewritten_node = nm->mkNode(kind::NOT, n_tmp348); + return rewrite5<Proof>(rewritten_node, proof); + }; + if (n_tmp347 == nm->mkConst(false)) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(FALSE_XOR); + }; + Node rewritten_node = n_tmp348; + return rewrite5<Proof>(rewritten_node, proof); + } + } + } + } + }; + return rewrite4<Proof>(node, proof); +} + +template <bool Proof> +inline RewriteResponse rewrite7(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_AGAIN_FULL, node); +} + +template <bool Proof> +inline RewriteResponse rewrite8(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + if ((node).getKind() == kind::EQUAL) { + for (unsigned in_tmp342 = 0, in_tmp342_end = node.getNumChildren(); + in_tmp342 < in_tmp342_end; in_tmp342++) { + TNode n_tmp342 = node[in_tmp342]; + if ((n_tmp342).getKind() == kind::EQUAL) { + for (unsigned in_tmp341 = 0, in_tmp341_end = node.getNumChildren(); + in_tmp341 < in_tmp341_end; in_tmp341++) { + TNode n_tmp341 = node[in_tmp341]; + if ((!(in_tmp342 == in_tmp341)) && + ((n_tmp341).getKind() == kind::EQUAL)) { + for (unsigned in_tmp346 = 0, + in_tmp346_end = n_tmp342.getNumChildren(); + in_tmp346 < in_tmp346_end; in_tmp346++) { + TNode n_tmp346 = n_tmp342[in_tmp346]; + + for (unsigned in_tmp345 = 0, + in_tmp345_end = n_tmp342.getNumChildren(); + in_tmp345 < in_tmp345_end; in_tmp345++) { + TNode n_tmp345 = n_tmp342[in_tmp345]; + if (!(in_tmp346 == in_tmp345)) { + for (unsigned in_tmp344 = 0, + in_tmp344_end = n_tmp341.getNumChildren(); + in_tmp344 < in_tmp344_end; in_tmp344++) { + TNode n_tmp344 = n_tmp341[in_tmp344]; + if (n_tmp344 == n_tmp346) { + for (unsigned in_tmp343 = 0, + in_tmp343_end = n_tmp341.getNumChildren(); + in_tmp343 < in_tmp343_end; in_tmp343++) { + TNode n_tmp343 = n_tmp341[in_tmp343]; + if ((!(in_tmp344 == in_tmp343)) && + ((((n_tmp343).isConst()) && + ((n_tmp345).isConst())) && + ((n_tmp343 != n_tmp345)))) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(EQ_NEQ_CONSTS); + }; + Node rewritten_node = nm->mkNode( + kind::AND, + nm->mkNode( + kind::NOT, + nm->mkNode(kind::EQUAL, n_tmp343, n_tmp344)), + nm->mkNode( + kind::NOT, + nm->mkNode(kind::EQUAL, n_tmp345, n_tmp344))); + return rewrite7<Proof>(rewritten_node, proof); + } + } + } + } + } + } + } + } + } + } + } + }; + return rewrite6<Proof>(node, proof); +} + +template <bool Proof> +inline RewriteResponse rewrite9(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_DONE, node); +} + +template <bool Proof> +inline RewriteResponse rewrite10(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + if ((node).getKind() == kind::EQUAL) { + for (unsigned in_tmp330 = 0, in_tmp330_end = node.getNumChildren(); + in_tmp330 < in_tmp330_end; in_tmp330++) { + TNode n_tmp330 = node[in_tmp330]; + if ((n_tmp330).getKind() == kind::EQUAL) { + for (unsigned in_tmp329 = 0, in_tmp329_end = node.getNumChildren(); + in_tmp329 < in_tmp329_end; in_tmp329++) { + TNode n_tmp329 = node[in_tmp329]; + if ((!(in_tmp330 == in_tmp329)) && + ((n_tmp329).getKind() == kind::EQUAL)) { + for (unsigned in_tmp334 = 0, + in_tmp334_end = n_tmp330.getNumChildren(); + in_tmp334 < in_tmp334_end; in_tmp334++) { + TNode n_tmp334 = n_tmp330[in_tmp334]; + + for (unsigned in_tmp333 = 0, + in_tmp333_end = n_tmp330.getNumChildren(); + in_tmp333 < in_tmp333_end; in_tmp333++) { + TNode n_tmp333 = n_tmp330[in_tmp333]; + if (!(in_tmp334 == in_tmp333)) { + for (unsigned in_tmp332 = 0, + in_tmp332_end = n_tmp329.getNumChildren(); + in_tmp332 < in_tmp332_end; in_tmp332++) { + TNode n_tmp332 = n_tmp329[in_tmp332]; + if (n_tmp332 == n_tmp334) { + for (unsigned in_tmp331 = 0, + in_tmp331_end = n_tmp329.getNumChildren(); + in_tmp331 < in_tmp331_end; in_tmp331++) { + TNode n_tmp331 = n_tmp329[in_tmp331]; + if ((!(in_tmp332 == in_tmp331)) && + ((n_tmp331).isConst()) && (n_tmp331 == n_tmp333)) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(EQ_EQ_CONSTS); + }; + Node rewritten_node = nm->mkConst(true); + return rewrite9<Proof>(rewritten_node, proof); + } + } + }; + if (n_tmp332 == n_tmp334) { + for (unsigned in_tmp337 = 0, + in_tmp337_end = n_tmp329.getNumChildren(); + in_tmp337 < in_tmp337_end; in_tmp337++) { + TNode n_tmp337 = n_tmp329[in_tmp337]; + if ((!(in_tmp332 == in_tmp337)) && + (((((n_tmp337).isConst()) && + ((n_tmp333).isConst())) && + ((n_tmp337 != n_tmp333))) && + ((n_tmp332) + .getType() + .getCardinality() + .knownLessThanOrEqual(Cardinality(2))))) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(EQ_NEQ_CONSTS_CARD2); + }; + Node rewritten_node = nm->mkConst(false); + return rewrite9<Proof>(rewritten_node, proof); + } + } + } + } + } + } + } + } + } + } + } + }; + return rewrite8<Proof>(node, proof); +} + +template <bool Proof> +inline RewriteResponse rewrite11(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_DONE, node); +} + +template <bool Proof> +inline RewriteResponse rewrite12(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + if (((node).getKind() == kind::EQUAL) && (true)) { + for (unsigned in_tmp326 = 0, in_tmp326_end = node.getNumChildren(); + in_tmp326 < in_tmp326_end; in_tmp326++) { + TNode n_tmp326 = node[in_tmp326]; + + for (unsigned in_tmp325 = 0, in_tmp325_end = node.getNumChildren(); + in_tmp325 < in_tmp325_end; in_tmp325++) { + TNode n_tmp325 = node[in_tmp325]; + if (!(in_tmp326 == in_tmp325)) { + if (n_tmp325 == n_tmp326) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(X_EQ_X); + }; + Node rewritten_node = nm->mkConst(true); + return rewrite11<Proof>(rewritten_node, proof); + }; + if (((n_tmp325).getKind() == kind::NOT) && + (n_tmp325[0] == n_tmp326)) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(N_X_EQ_X); + }; + Node rewritten_node = nm->mkConst(false); + return rewrite11<Proof>(rewritten_node, proof); + } + } + } + } + }; + return rewrite10<Proof>(node, proof); +} + +template <bool Proof> +inline RewriteResponse rewrite13(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_AGAIN, node); +} + +template <bool Proof> +inline RewriteResponse rewrite14(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + if (((node).getKind() == kind::EQUAL) && (true)) { + for (unsigned in_tmp322 = 0, in_tmp322_end = node.getNumChildren(); + in_tmp322 < in_tmp322_end; in_tmp322++) { + TNode n_tmp322 = node[in_tmp322]; + + for (unsigned in_tmp321 = 0, in_tmp321_end = node.getNumChildren(); + in_tmp321 < in_tmp321_end; in_tmp321++) { + TNode n_tmp321 = node[in_tmp321]; + if ((!(in_tmp322 == in_tmp321)) && + ((n_tmp321).getKind() == kind::CONST_BOOLEAN)) { + if (n_tmp321 == nm->mkConst(true)) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(TRUE_EQ); + }; + Node rewritten_node = n_tmp322; + return rewrite13<Proof>(rewritten_node, proof); + }; + if (n_tmp321 == nm->mkConst(false)) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(FALSE_EQ); + }; + Node rewritten_node = nm->mkNode(kind::NOT, n_tmp322); + return rewrite13<Proof>(rewritten_node, proof); + } + } + } + } + }; + return rewrite12<Proof>(node, proof); +} + +template <bool Proof> +inline RewriteResponse rewrite15(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_AGAIN, node); +} + +template <bool Proof> +inline RewriteResponse rewrite16(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + if ((node).getKind() == kind::IMPLIES) { + if (((node[0]).getKind() == kind::CONST_BOOLEAN) && (true) && + (node[0] == nm->mkConst(true))) { + if (Proof) { + proof->registerRewrite(TRUE_IMPLIES); + }; + Node rewritten_node = node[1]; + return rewrite15<Proof>(rewritten_node, proof); + }; + if (((node[1]).getKind() == kind::CONST_BOOLEAN) && (true) && + (node[1] == nm->mkConst(false))) { + if (Proof) { + proof->registerRewrite(IMPLIES_FALSE); + }; + Node rewritten_node = nm->mkNode(kind::NOT, node[0]); + return rewrite15<Proof>(rewritten_node, proof); + } + }; + return rewrite14<Proof>(node, proof); +} + +template <bool Proof> +inline RewriteResponse rewrite17(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_DONE, node); +} + +template <bool Proof> +inline RewriteResponse rewrite18(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + if ((node).getKind() == kind::IMPLIES) { + if (((node[0]).getKind() == kind::CONST_BOOLEAN) && (true) && + (node[0] == nm->mkConst(false))) { + if (Proof) { + proof->registerRewrite(FALSE_IMPLIES); + }; + Node rewritten_node = nm->mkConst(true); + return rewrite17<Proof>(rewritten_node, proof); + }; + if (((node[1]).getKind() == kind::CONST_BOOLEAN) && (true) && + (node[1] == nm->mkConst(true))) { + if (Proof) { + proof->registerRewrite(IMPLIES_TRUE); + }; + Node rewritten_node = nm->mkConst(true); + return rewrite17<Proof>(rewritten_node, proof); + }; + if (((node[0]).getKind() == kind::CONST_BOOLEAN) && + ((node[1]).getKind() == kind::CONST_BOOLEAN) && (true) && + (node[0] == nm->mkConst(true)) && (node[1] == nm->mkConst(false))) { + if (Proof) { + proof->registerRewrite(TRUE_IMPLIES_FALSE); + }; + Node rewritten_node = nm->mkConst(false); + return rewrite17<Proof>(rewritten_node, proof); + } + }; + return rewrite16<Proof>(node, proof); +} + +template <bool Proof> +inline RewriteResponse rewrite19(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_AGAIN, node); +} + +template <bool Proof> +inline RewriteResponse rewrite20(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + if (((node).getKind() == kind::AND) && (true)) { + for (unsigned in_tmp318 = 0, in_tmp318_end = node.getNumChildren(); + in_tmp318 < in_tmp318_end; in_tmp318++) { + TNode n_tmp318 = node[in_tmp318]; + if (((n_tmp318).getKind() == kind::CONST_BOOLEAN) && + (n_tmp318 == nm->mkConst(true))) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(AND_TRUE); + }; + std::vector<Node> new_children = + std::vector<Node>(node.begin(), node.end()); + ; + new_children.erase(new_children.begin() + in_tmp318); + Node x = mkCommutativeNode((node).getKind(), new_children); + ; + Node rewritten_node = x; + return rewrite19<Proof>(rewritten_node, proof); + }; + for (unsigned in_tmp319 = 0, in_tmp319_end = node.getNumChildren(); + in_tmp319 < in_tmp319_end; in_tmp319++) { + TNode n_tmp319 = node[in_tmp319]; + if ((!(in_tmp318 == in_tmp319)) && (n_tmp319 == n_tmp318)) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(AND_DUP); + }; + std::vector<Node> new_children = + std::vector<Node>(node.begin(), node.end()); + ; + new_children.erase(new_children.begin() + in_tmp319); + new_children.erase(new_children.begin() + in_tmp318); + Node x = mkCommutativeNode((node).getKind(), new_children); + ; + Node rewritten_node = nm->mkNode(kind::AND, n_tmp319, x); + return rewrite19<Proof>(rewritten_node, proof); + } + } + } + }; + return rewrite18<Proof>(node, proof); +} + +template <bool Proof> +inline RewriteResponse rewrite21(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_DONE, node); +} + +template <bool Proof> +inline RewriteResponse rewrite22(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + if (((node).getKind() == kind::AND) && (true)) { + for (unsigned in_tmp317 = 0, in_tmp317_end = node.getNumChildren(); + in_tmp317 < in_tmp317_end; in_tmp317++) { + TNode n_tmp317 = node[in_tmp317]; + if (((n_tmp317).getKind() == kind::CONST_BOOLEAN) && + (n_tmp317 == nm->mkConst(false))) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(AND_FALSE); + }; + std::vector<Node> new_children = + std::vector<Node>(node.begin(), node.end()); + ; + new_children.erase(new_children.begin() + in_tmp317); + Node x = mkCommutativeNode((node).getKind(), new_children); + ; + Node rewritten_node = nm->mkConst(false); + return rewrite21<Proof>(rewritten_node, proof); + } + } + }; + return rewrite20<Proof>(node, proof); +} + +template <bool Proof> +inline RewriteResponse rewrite23(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_AGAIN, node); +} + +template <bool Proof> +inline RewriteResponse rewrite24(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + if (((node).getKind() == kind::OR) && (true)) { + for (unsigned in_tmp314 = 0, in_tmp314_end = node.getNumChildren(); + in_tmp314 < in_tmp314_end; in_tmp314++) { + TNode n_tmp314 = node[in_tmp314]; + if (((n_tmp314).getKind() == kind::CONST_BOOLEAN) && + (n_tmp314 == nm->mkConst(false))) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(OR_FALSE); + }; + std::vector<Node> new_children = + std::vector<Node>(node.begin(), node.end()); + ; + new_children.erase(new_children.begin() + in_tmp314); + Node x = mkCommutativeNode((node).getKind(), new_children); + ; + Node rewritten_node = x; + return rewrite23<Proof>(rewritten_node, proof); + }; + for (unsigned in_tmp315 = 0, in_tmp315_end = node.getNumChildren(); + in_tmp315 < in_tmp315_end; in_tmp315++) { + TNode n_tmp315 = node[in_tmp315]; + if ((!(in_tmp314 == in_tmp315)) && (n_tmp315 == n_tmp314)) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(OR_DUP); + }; + std::vector<Node> new_children = + std::vector<Node>(node.begin(), node.end()); + ; + new_children.erase(new_children.begin() + in_tmp315); + new_children.erase(new_children.begin() + in_tmp314); + Node x = mkCommutativeNode((node).getKind(), new_children); + ; + Node rewritten_node = nm->mkNode(kind::OR, n_tmp315, x); + return rewrite23<Proof>(rewritten_node, proof); + } + } + } + }; + return rewrite22<Proof>(node, proof); +} + +template <bool Proof> +inline RewriteResponse rewrite25(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_DONE, node); +} + +template <bool Proof> +inline RewriteResponse rewrite26(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + if (((node).getKind() == kind::OR) && (true)) { + for (unsigned in_tmp313 = 0, in_tmp313_end = node.getNumChildren(); + in_tmp313 < in_tmp313_end; in_tmp313++) { + TNode n_tmp313 = node[in_tmp313]; + if (((n_tmp313).getKind() == kind::CONST_BOOLEAN) && + (n_tmp313 == nm->mkConst(true))) { + if (Proof) { + proof->registerSwap(0, 0); + proof->registerRewrite(OR_TRUE); + }; + std::vector<Node> new_children = + std::vector<Node>(node.begin(), node.end()); + ; + new_children.erase(new_children.begin() + in_tmp313); + Node x = mkCommutativeNode((node).getKind(), new_children); + ; + Node rewritten_node = nm->mkConst(true); + return rewrite25<Proof>(rewritten_node, proof); + } + } + }; + return rewrite24<Proof>(node, proof); +} + +template <bool Proof> +inline RewriteResponse rewrite27(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_AGAIN, node); +} + +template <bool Proof> +inline RewriteResponse rewrite28(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + if (((node).getKind() == kind::NOT) && ((node[0]).getKind() == kind::NOT) && + (true)) { + if (Proof) { + proof->registerRewrite(NOT_NOT); + }; + Node rewritten_node = node[0][0]; + return rewrite27<Proof>(rewritten_node, proof); + }; + return rewrite26<Proof>(node, proof); +} + +template <bool Proof> +inline RewriteResponse rewrite29(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse(REWRITE_DONE, node); +} + +template <bool Proof> +inline RewriteResponse rewrite30(TNode node, RewriteProof *proof) { + NodeManager *nm = NodeManager::currentNM(); + if (((node).getKind() == kind::NOT) && + ((node[0]).getKind() == kind::CONST_BOOLEAN) && (true)) { + if (node[0] == nm->mkConst(true)) { + if (Proof) { + proof->registerRewrite(NOT_TRUE); + }; + Node rewritten_node = nm->mkConst(false); + return rewrite29<Proof>(rewritten_node, proof); + }; + if (node[0] == nm->mkConst(false)) { + if (Proof) { + proof->registerRewrite(NOT_FALSE); + }; + Node rewritten_node = nm->mkConst(true); + return rewrite29<Proof>(rewritten_node, proof); + } + }; + return rewrite28<Proof>(node, proof); +} + +template <bool Proof> +inline RewriteResponse bool_applyRules(TNode node, RewriteProof *proof) { + + return rewrite30<Proof>(node, proof); +} + +inline void bool_printProof(bool use_cache, TheoryProofEngine *tp, + const Rewrite *rewrite, std::ostream &os, + ProofLetMap &globalLetMap) { + + if (rewrite->d_tag == NOT_TRUE) { + os << "(not_true _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == NOT_FALSE) { + os << "(not_false _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == NOT_NOT) { + os << "(not_not _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == OR_TRUE) { + os << "(or_true _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == OR_FALSE) { + os << "(or_false _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == OR_DUP) { + os << "(or_dup _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == AND_FALSE) { + os << "(and_false _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == AND_TRUE) { + os << "(and_true _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == AND_DUP) { + os << "(and_dup _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == FALSE_IMPLIES) { + os << "(false_implies _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == IMPLIES_TRUE) { + os << "(implies_true _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == TRUE_IMPLIES_FALSE) { + os << "(true_implies_false _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == TRUE_IMPLIES) { + os << "(true_implies _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == IMPLIES_FALSE) { + os << "(implies_false _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == TRUE_EQ) { + os << "(true_eq _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == FALSE_EQ) { + os << "(false_eq _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == X_EQ_X) { + os << "(x_eq_x _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == N_X_EQ_X) { + os << "(n_x_eq_x _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == EQ_EQ_CONSTS) { + os << "(eq_eq_consts _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == EQ_NEQ_CONSTS_CARD2) { + os << "(eq_neq_consts_card2 _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == EQ_NEQ_CONSTS) { + os << "(eq_neq_consts _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == TRUE_XOR) { + os << "(true_xor _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == FALSE_XOR) { + os << "(false_xor _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == X_XOR_X) { + os << "(x_xor_x _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == N_X_XOR_X) { + os << "(n_x_xor_x _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_TRUE) { + os << "(ite_true _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_FALSE) { + os << "(ite_false _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_X_TRUE_FALSE) { + os << "(ite_x_true_false _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_C_FALSE_TRUE) { + os << "(ite_c_false_true _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_C_X_X) { + os << "(ite_c_x_x _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_C_X_N_X) { + os << "(ite_c_x_n_x _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_C_N_X_X) { + os << "(ite_c_n_x_x _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_X_X_Y) { + os << "(ite_x_x_y _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_N_X_X_Y) { + os << "(ite_n_x_x_y _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_X_N_X_Y) { + os << "(ite_x_n_x_y _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_X_Y_X) { + os << "(ite_x_y_x _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_N_X_Y_X) { + os << "(ite_n_x_y_x _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_X_Y_N_X) { + os << "(ite_x_y_n_x _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_C_ITE_C_X_Y_Z) { + os << "(ite_c_ite_c_x_y_z _ _ _ _ _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_C_ITE_N_C_X_Y_Z) { + os << "(ite_c_ite_n_c_x_y_z _ _ _ _ _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_N_C_ITE_C_X_Y_Z) { + os << "(ite_n_c_ite_c_x_y_z _ _ _ _ _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_C_Z_ITE_C_X_Y) { + os << "(ite_c_z_ite_c_x_y _ _ _ _ _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_C_Z_ITE_N_C_X_Y) { + os << "(ite_c_z_ite_n_c_x_y _ _ _ _ _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } else if (rewrite->d_tag == ITE_N_C_Z_ITE_C_X_Y) { + os << "(ite_n_c_z_ite_c_x_y _ _ _ _ _ _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, + globalLetMap); + os << ")"; + } +} + +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 32f69e037..124b08cc9 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -15,15 +15,70 @@ ** \todo document this file **/ -#include <algorithm> #include "theory/booleans/theory_bool_rewriter.h" +#include <algorithm> + +#include "proof/rewrite_proof_dispatcher.h" + namespace CVC4 { namespace theory { namespace booleans { RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) { - return preRewrite(node); + return preRewriteEx<false>(node, NULL); +} + +Node flattenIfNeeded(TNode n) { + Kind k = n.getKind(); + if (k != kind::AND && k != kind::OR) { + return n; + } + + bool needed = false; + for (size_t i = 0; i < n.getNumChildren(); i++) { + if (n[i].getKind() == k) { + needed = true; + break; + } + } + if (!needed) { + return n; + } + + std::vector<TNode> toProcess; + toProcess.push_back(n); + + typedef std::vector<TNode> ChildList; + ChildList childList; + + for (unsigned i = 0; i < toProcess.size(); ++ i) { + TNode current = toProcess[i]; + for(unsigned j = 0, j_end = current.getNumChildren(); j < j_end; ++ j) { + TNode child = current[j]; + if(child.getKind() == k) { + toProcess.push_back(child); + } else { + childList.push_back(child); + } + } + } + + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(k, childList); +} + + +template<bool Proof> +RewriteResponse TheoryBoolRewriter::postRewriteEx(TNode node_, RewriteProof* proof) { + Node node = flattenIfNeeded(node_); + RewriteResponse r = bool_applyRules<Proof>(node, proof); + if (r.node != preRewrite(node).node) { + std::cout << node << " --> " << r.node << std::endl; + std::cout << preRewrite(node).node << std::endl; + } + return r; + } /** @@ -286,21 +341,21 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { if (n[0] == tt) { // ITE true x y - Debug("bool-ite") << "n[0] ==tt " << n << ": " << n[1] << std::endl; + Debug("bool-ite") << "n[0] == tt " << n << ": " << n[1] << std::endl; return RewriteResponse(REWRITE_AGAIN, n[1]); } else { Assert(n[0] == ff); // ITE false x y - Debug("bool-ite") << "n[0] ==ff " << n << ": " << n[1] << std::endl; + Debug("bool-ite") << "n[0] == ff " << n << ": " << n[1] << std::endl; return RewriteResponse(REWRITE_AGAIN, n[2]); } } else if (n[1].isConst()) { if (n[1] == tt && n[2] == ff) { - Debug("bool-ite") << "n[1] ==tt && n[2] == ff " << n << ": " << n[0] << std::endl; + Debug("bool-ite") << "n[1] == tt && n[2] == ff " << n << ": " << n[0] << std::endl; return RewriteResponse(REWRITE_AGAIN, n[0]); } else if (n[1] == ff && n[2] == tt) { - Debug("bool-ite") << "n[1] ==ff && n[2] == tt " << n << ": " << n[0].notNode() << std::endl; + Debug("bool-ite") << "n[1] == ff && n[2] == tt " << n << ": " << n[0].notNode() << std::endl; return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); } // else if(n[1] == ff){ @@ -367,6 +422,109 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { return RewriteResponse(REWRITE_DONE, n); } +template<bool Proof> +RewriteResponse TheoryBoolRewriter::preRewriteEx(TNode node_, RewriteProof* proof) { + Node node = flattenIfNeeded(node_); + RewriteResponse r = bool_applyRules<Proof>(node, NULL); + if (r.node != preRewrite(node).node) { + std::cout << node << " --> " << r.node << std::endl; + std::cout << preRewrite(node).node << std::endl; + } + return r; +} + +void TheoryBoolRewriter::printRewriteProof(bool use_cache, + TheoryProofEngine* tp, + const Rewrite* rewrite, + std::ostream& os, + ProofLetMap& globalLetMap) { + if (rewrite->d_tag == ORIGINAL_OP) { + if (rewrite->d_children.size() == 0) { + os << "(iff_symm "; + tp->printTheoryTerm(rewrite->d_original.toExpr(), os, globalLetMap); + os << ")"; + } else { + // XXX: we only need one of those options for each arity + switch (rewrite->d_original.getKind()) { + case kind::NOT: + os << "(symm_formula_op1 not _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, globalLetMap); + os << ")"; + break; + case kind::IMPLIES: + os << "(symm_formula_op2 impl _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, globalLetMap); + os << " "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[1], os, globalLetMap); + os << ")"; + break; + case kind::AND: + os << "(symm_formula_op2 and _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, globalLetMap); + os << " "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[1], os, globalLetMap); + os << ")"; + break; + // XXX: CHECK THIS + case kind::EQUAL: + os << "(symm_formula_op2 iff _ _ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, globalLetMap); + os << " "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[1], os, globalLetMap); + os << ")"; + break; + default: + std::cout << "IMPLEMENTATION MISSING " << rewrite->d_original.getKind() << std::endl; + Unreachable(); + } + } + } else if (rewrite->d_tag == SWAP) { + os << "(do_swap_op2 "; + switch (rewrite->d_original.getKind()) { + case kind::EQUAL: + os << "iff "; + break; + case kind::AND: + os << "and "; + break; + case kind::OR: + os << "or "; + break; + case kind::XOR: + os << "xor "; + break; + default: + std::cout << "IMPLEMENTATION MISSING " << rewrite->d_original.getKind() << std::endl; + Unreachable(); + } + os << rewrite->swap_id1 << " "; + os << rewrite->swap_id2 << " "; + os << "_ _ _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, globalLetMap); + os << ")"; + } else { + bool_printProof(use_cache, tp, rewrite, os, globalLetMap); + } + /* + if (rewrite->d_tag == NOT_TRUE) { + os << "(not_t _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, globalLetMap); + os << ")"; + } else if (rewrite->d_tag == TRUE_IMPLIES_FALSE) { + os << "(t_impl_f _ "; + callPrintRewriteProof(use_cache, tp, rewrite->d_children[0], os, globalLetMap); + os << ")"; + } else { + std::cout << "ERROR" << std::endl; + Unreachable(); + }*/ +} + +template RewriteResponse TheoryBoolRewriter::preRewriteEx<true>(TNode node, RewriteProof* proof); +template RewriteResponse TheoryBoolRewriter::preRewriteEx<false>(TNode node, RewriteProof* proof); +template RewriteResponse TheoryBoolRewriter::postRewriteEx<true>(TNode node, RewriteProof* proof); +template RewriteResponse TheoryBoolRewriter::postRewriteEx<false>(TNode node, RewriteProof* proof); + }/* CVC4::theory::booleans namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h index b7512ad09..cba66abe5 100644 --- a/src/theory/booleans/theory_bool_rewriter.h +++ b/src/theory/booleans/theory_bool_rewriter.h @@ -20,6 +20,7 @@ #ifndef __CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H #define __CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H +#include "theory/booleans/bool.h" #include "theory/rewriter.h" namespace CVC4 { @@ -27,15 +28,26 @@ namespace theory { namespace booleans { class TheoryBoolRewriter { - public: + enum BoolRewrites { + NOT_TRUE = LAST_SHARED, + TRUE_IMPLIES_FALSE, + }; static RewriteResponse preRewrite(TNode node); + template<bool Proof> + static RewriteResponse preRewriteEx(TNode node, RewriteProof* proof); static RewriteResponse postRewrite(TNode node); + template<bool Proof> + static RewriteResponse postRewriteEx(TNode node, RewriteProof* proof); + static void printRewriteProof(bool use_cache, + TheoryProofEngine* tp, + const Rewrite* rewrite, + std::ostream& os, + ProofLetMap& globalLetMap); static void init() {} static void shutdown() {} - };/* class TheoryBoolRewriter */ }/* CVC4::theory::booleans namespace */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 01352217e..6b4b890de 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -508,7 +508,7 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n Assert( !h.isNull() ); // if it is a function definition, rewrite the body independently Node fbody = TermDb::getFunDefBody( q ); - Assert( !body.isNull() ); + Assert( !fbody.isNull() ); Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl; Node r = computeProcessTerms2( fbody, true, true, curr_cond, 0, cache, icache, new_vars, new_conds, false ); Assert( new_vars.size()==h.getNumChildren() ); diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 0df122571..a5d011e9f 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -17,11 +17,8 @@ #include "theory/rewriter.h" -#include "theory/theory.h" -#include "smt/smt_engine_scope.h" -#include "smt/smt_statistics_registry.h" +#include "proof/rewrite_proof_dispatcher.h" #include "theory/rewriter_tables.h" -#include "util/resource_manager.h" using namespace std; @@ -30,10 +27,6 @@ namespace theory { unsigned long Rewriter::d_iterationCount = 0; -static TheoryId theoryOf(TNode node) { - return Theory::theoryOf(THEORY_OF_TYPE_BASED, node); -} - #ifdef CVC4_ASSERTIONS static CVC4_THREADLOCAL(std::hash_set<Node, NodeHashFunction>*) s_rewriteStack = NULL; #endif /* CVC4_ASSERTIONS */ @@ -85,11 +78,11 @@ struct RewriteStackElement { }; Node Rewriter::rewrite(TNode node) { - return rewriteTo(theoryOf(node), node); + return rewriteTo<false>(theoryOf(node), node, NULL); } -Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { - +template<bool Proof> +Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node, RewriteProof* rp) { #ifdef CVC4_ASSERTIONS bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean()); @@ -101,14 +94,19 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { Trace("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl; // Check if it's been cached already - Node cached = getPostRewriteCache(theoryId, node); - if (!cached.isNull()) { - return cached; + if (!Proof) { + Node cached = getPostRewriteCache(theoryId, node); + if (!cached.isNull()) { + return cached; + } } // Put the node on the stack in order to start the "recursive" rewrite vector<RewriteStackElement> rewriteStack; rewriteStack.push_back(RewriteStackElement(node, theoryId)); + if (Proof) { + rp->addRewrite(new Rewrite(ORIGINAL_OP, node)); + } ResourceManager* rm = NULL; bool hasSmtEngine = smt::smtEngineInScope(); @@ -119,26 +117,25 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { for (;;){ if (hasSmtEngine && - d_iterationCount % ResourceManager::getFrequencyCount() == 0) { + d_iterationCount % ResourceManager::getFrequencyCount() == 0) { rm->spendResource(options::rewriteStep()); d_iterationCount = 0; } // Get the top of the recursion stack RewriteStackElement& rewriteStackTop = rewriteStack.back(); - Trace("rewriter") << "Rewriter::rewriting: " << (TheoryId) rewriteStackTop.theoryId << "," << rewriteStackTop.node << std::endl; // Before rewriting children we need to do a pre-rewrite of the node if (rewriteStackTop.nextChild == 0) { - // Check if the pre-rewrite has already been done (it's in the cache) Node cached = Rewriter::getPreRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); - if (cached.isNull()) { + if ((Proof && rp->getPreRewriteCache(rewriteStackTop.node) == NULL) || cached.isNull()) { // Rewrite until fix-point is reached for(;;) { // Perform the pre-rewrite - RewriteResponse response = Rewriter::callPreRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); + RewriteResponse response = Proof ? callPreRewriteWithProof((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node, rp) : Rewriter::callPreRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); + // Put the rewritten node to the top of the stack rewriteStackTop.node = response.node; TheoryId newTheory = theoryOf(rewriteStackTop.node); @@ -148,14 +145,23 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { } rewriteStackTop.theoryId = newTheory; } + // Cache the rewrite Rewriter::setPreRewriteCache((TheoryId) rewriteStackTop.originalTheoryId, rewriteStackTop.original, rewriteStackTop.node); + if (Proof) { + rp->setPreRewriteCache(rewriteStackTop.original, rp->getTopRewrite()); + } } // Otherwise we're have already been pre-rewritten (in pre-rewrite cache) else { // Continue with the cached version rewriteStackTop.node = cached; rewriteStackTop.theoryId = theoryOf(cached); + if (Proof) { + Rewrite* cachedRewrite = rp->getPreRewriteCache(rewriteStackTop.original); + cachedRewrite->d_cached_version_used = true; + rp->replaceRewrite(cachedRewrite); + } } } @@ -163,7 +169,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Now it's time to rewrite the children, check if this has already been done Node cached = Rewriter::getPostRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); // If not, go through the children - if(cached.isNull()) { + if((Proof && rp->getPostRewriteCache(rewriteStackTop.node) == NULL) || cached.isNull()) { // The child we need to rewrite unsigned child = rewriteStackTop.nextChild++; @@ -186,6 +192,9 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { Node childNode = rewriteStackTop.node[child]; // Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now) rewriteStack.push_back(RewriteStackElement(childNode, theoryOf(childNode))); + if (Proof) { + rp->addRewrite(new Rewrite(ORIGINAL_OP, childNode)); + } // Go on with the rewriting continue; } @@ -200,7 +209,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Done with all pre-rewriting, so let's do the post rewrite for(;;) { // Do the post-rewrite - RewriteResponse response = Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); + RewriteResponse response = Proof ? callPostRewriteWithProof((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node, rp) : Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); // We continue with the response we got TheoryId newTheoryId = theoryOf(response.node); if (newTheoryId != (TheoryId) rewriteStackTop.theoryId || response.status == REWRITE_AGAIN_FULL) { @@ -211,24 +220,30 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { Assert(s_rewriteStack->find(response.node) == s_rewriteStack->end()); s_rewriteStack->insert(response.node); #endif - Node rewritten = rewriteTo(newTheoryId, response.node); - rewriteStackTop.node = rewritten; + if (Proof) { + RewriteProof subRp; + Node rewritten = rewriteWithProof(response.node, &subRp); + rewriteStackTop.node = rewritten; + } else { + rewriteStackTop.node = rewrite(response.node); + } #ifdef CVC4_ASSERTIONS + Assert(s_rewriteStack); s_rewriteStack->erase(response.node); #endif break; } else if (response.status == REWRITE_DONE) { #ifdef CVC4_ASSERTIONS - RewriteResponse r2 = Rewriter::callPostRewrite(newTheoryId, response.node); - Assert(r2.node == response.node); + RewriteResponse r2 = Rewriter::callPostRewrite(newTheoryId, response.node); + Assert(r2.node == response.node); #endif - rewriteStackTop.node = response.node; + rewriteStackTop.node = response.node; break; } // Check for trivial rewrite loops of size 1 or 2 Assert(response.node != rewriteStackTop.node); Assert(Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, response.node).node != rewriteStackTop.node); - rewriteStackTop.node = response.node; + rewriteStackTop.node = response.node; } // We're done with the post rewrite, so we add to the cache Rewriter::setPostRewriteCache((TheoryId) rewriteStackTop.originalTheoryId, rewriteStackTop.original, rewriteStackTop.node); @@ -237,6 +252,11 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // We were already in cache, so just remember it rewriteStackTop.node = cached; rewriteStackTop.theoryId = theoryOf(cached); + if (Proof) { + Rewrite* cachedRewrite = rp->getPostRewriteCache(rewriteStackTop.original); + cachedRewrite->d_cached_version_used = true; + rp->replaceRewrite(cachedRewrite); + } } // If this is the last node, just return @@ -248,12 +268,21 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // We're done with this node, append it to the parent rewriteStack[rewriteStack.size() - 2].builder << rewriteStackTop.node; rewriteStack.pop_back(); + + if (Proof) { + rp->attachSubproofToParent(); + } } Unreachable(); return Node::null(); }/* Rewriter::rewriteTo() */ +Node Rewriter::rewriteWithProof(TNode node, RewriteProof* rp) throw (UnsafeInterruptException){ + Node result = rewriteTo<true>(theoryOf(node), node, rp); + return result; +} + void Rewriter::clearCaches() { #ifdef CVC4_ASSERTIONS if(s_rewriteStack != NULL) { @@ -264,5 +293,8 @@ void Rewriter::clearCaches() { Rewriter::clearCachesInternal(); } +template Node Rewriter::rewriteTo<true>(theory::TheoryId theoryId, Node node, RewriteProof* rp); +template Node Rewriter::rewriteTo<false>(theory::TheoryId theoryId, Node node, RewriteProof* rp); + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index aed93a451..7f01be250 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -19,11 +19,43 @@ #pragma once #include "expr/node.h" +#include "smt/smt_engine_scope.h" +#include "smt/smt_statistics_registry.h" +#include "theory/theory.h" +#include "util/resource_manager.h" #include "util/unsafe_interrupt_exception.h" +using namespace std; + namespace CVC4 { namespace theory { +static inline Node mkCommutativeNode(Kind k, const std::vector<Node>& children) { + NodeManager *nm = NodeManager::currentNM(); + + if (children.size() == 0) { + switch (k) { + case kind::AND: + return nm->mkConst(true); + break; + case kind::OR: + return nm->mkConst(false); + break; + default: + abort(); + break; + } + } else if (children.size() == 1) { + return children[0]; + } else { + return nm->mkNode(k, children); + } +} + +static inline TheoryId theoryOf(TNode node) { + return Theory::theoryOf(THEORY_OF_TYPE_BASED, node); +} + /** * Theory rewriters signal whether more rewriting is needed (or not) * by using a member of this enumeration. See RewriteResponse, below. @@ -44,6 +76,7 @@ enum RewriteStatus { struct RewriteResponse { const RewriteStatus status; const Node node; + RewriteResponse(RewriteStatus status, Node node) : status(status), node(node) {} };/* struct RewriteResponse */ @@ -78,7 +111,8 @@ class Rewriter { /** * Rewrites the node using the given theory rewriter. */ - static Node rewriteTo(theory::TheoryId theoryId, Node node); + template<bool Proof> + static Node rewriteTo(theory::TheoryId theoryId, Node node, RewriteProof* rp); /** Calls the pre-rewriter for the given theory */ static RewriteResponse callPreRewrite(theory::TheoryId theoryId, TNode node); @@ -110,6 +144,12 @@ public: static Node rewrite(TNode node); /** + * Rewrites the node using theoryOf() to determine which rewriter to + * use on the node and generates a proof. + */ + static Node rewriteWithProof(TNode node, RewriteProof* rp) throw (UnsafeInterruptException); + + /** * Garbage collects the rewrite caches. */ static void clearCaches(); diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index 17cfa3fd4..5b46f9cd3 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -50,7 +50,10 @@ TESTS = \ constarr3.cvc \ parsing_ringer.cvc \ bug637.delta.smt2 \ - bool-array.smt2 + bool-array.smt2 \ + simple_rewrite_proof.smt2 \ + simple_rewrite_proof2.smt2 \ + rewrite_proof_cache.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/arrays/rewrite_proof_cache.smt2 b/test/regress/regress0/arrays/rewrite_proof_cache.smt2 new file mode 100644 index 000000000..c2d9ee09e --- /dev/null +++ b/test/regress/regress0/arrays/rewrite_proof_cache.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_AX) +(set-info :smt-lib-version 2.0) +(set-info :status unsat) +(declare-sort Index 0) +(declare-sort Element 0) +(declare-fun a1 () (Array Index Element)) +(declare-fun a2 () (Array Index Element)) +(declare-fun i1 () Index) +(declare-fun i2 () Index) +(declare-fun e1 () Element) +(declare-fun x () Bool) +(assert (=> (= (select (store a1 i2 (select a1 i2)) i1) (select a1 i1)) (not (= (select (store a1 i2 (select a1 i2)) i1) (select a1 i1))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/arrays/simple_rewrite_proof.smt2 b/test/regress/regress0/arrays/simple_rewrite_proof.smt2 new file mode 100644 index 000000000..0a3fe2229 --- /dev/null +++ b/test/regress/regress0/arrays/simple_rewrite_proof.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_AX) +(set-info :smt-lib-version 2.0) +(set-info :status unsat) +(declare-sort Index 0) +(declare-sort Element 0) +(declare-fun a1 () (Array Index Element)) +(declare-fun a2 () (Array Index Element)) +(declare-fun i1 () Index) +(declare-fun i2 () Index) +(declare-fun e1 () Element) +(assert (not (= (select (store a1 i2 (select a1 i2)) i1) (select a1 i1)))) +(check-sat) +(exit) diff --git a/test/regress/regress0/arrays/simple_rewrite_proof2.smt2 b/test/regress/regress0/arrays/simple_rewrite_proof2.smt2 new file mode 100644 index 000000000..639f21e38 --- /dev/null +++ b/test/regress/regress0/arrays/simple_rewrite_proof2.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_AX) +(set-info :smt-lib-version 2.0) +(set-info :status unsat) +(declare-sort Index 0) +(declare-sort Element 0) +(declare-fun a1 () (Array Index Element)) +(declare-fun a2 () (Array Index Element)) +(declare-fun i1 () Index) +(declare-fun i2 () Index) +(declare-fun e1 () Element) +(assert (not (= (select (store (store a1 i2 e1) i2 (select a1 i2)) i1) (select (store a1 i2 (select a1 i2)) i1)))) +(check-sat) +(exit) |