diff options
author | guykatzz <katz911@gmail.com> | 2017-03-17 14:11:41 -0700 |
---|---|---|
committer | guykatzz <katz911@gmail.com> | 2017-03-17 14:12:04 -0700 |
commit | 768534c0973788cab0097c6485e5113da1d406da (patch) | |
tree | 32e8eda1c7882f05b16c4bbec4e4095efbec34d3 /proofs | |
parent | afe84522b87b6fc0ad5d0e9a396b61f7b523f674 (diff) |
better support for proof production when encountering bool terms: handle the new proof constructs generated by the equality engine.
proof production for bool-array.smt2 passes
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/signatures/smt.plf | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index 38428dd1e..06dc16153 100644 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -71,6 +71,7 @@ (! x (term Bool) (! u (th_holds (p_app x)) (th_holds (= Bool x t_true))))) + (declare pred_eq_f (! x (term Bool) (! u (th_holds (not (p_app x))) @@ -104,6 +105,46 @@ (! u1 (th_holds (not (p_app x1))) (th_holds (= Bool x1 x1))))) +(declare pred_not_iff_f + (! x (term Bool) + (! u (th_holds (not (iff false (p_app x)))) + (th_holds (= Bool t_true x))))) + +(declare pred_not_iff_f_2 + (! x (term Bool) + (! u (th_holds (not (iff (p_app x) false))) + (th_holds (= Bool x t_true))))) + +(declare pred_not_iff_t + (! x (term Bool) + (! u (th_holds (not (iff true (p_app x)))) + (th_holds (= Bool t_false x))))) + +(declare pred_not_iff_t_2 + (! x (term Bool) + (! u (th_holds (not (iff (p_app x) true))) + (th_holds (= Bool x t_false))))) + +(declare pred_iff_f + (! x (term Bool) + (! u (th_holds (iff false (p_app x))) + (th_holds (= Bool t_false x))))) + +(declare pred_iff_f_2 + (! x (term Bool) + (! u (th_holds (iff (p_app x) false)) + (th_holds (= Bool x t_false))))) + +(declare pred_iff_t + (! x (term Bool) + (! u (th_holds (iff true (p_app x))) + (th_holds (= Bool t_true x))))) + +(declare pred_iff_t_2 + (! x (term Bool) + (! u (th_holds (iff (p_app x) true)) + (th_holds (= Bool x t_true))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; ; CNF Clausification |