diff options
68 files changed, 1339 insertions, 1048 deletions
diff --git a/.travis.yml b/.travis.yml index b8d958ed5..c47ad1928 100644 --- a/.travis.yml +++ b/.travis.yml @@ -27,7 +27,7 @@ script: make -j2 distcheck CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}DISTCHECK FAILED${normal}"; echo; exit 1); else (make -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}BUILD/TEST FAILED${normal}"; echo; exit 1)) && - (make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' || (echo; echo "${red}PORTFOLIO TEST FAILED${normal}"; echo; exit 1)) && + (make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' RUN_REGRESSION_ARGS= || (echo; echo "${red}PORTFOLIO TEST FAILED${normal}"; echo; exit 1)) && (make -j2 examples || (echo; echo "${red}COULD NOT BUILD EXAMPLES${normal}"; echo; exit 1)); fi; elif [ -n "$TRAVIS_LFSC" ]; then diff --git a/Makefile.am b/Makefile.am index 40f4c7006..55c357def 100644 --- a/Makefile.am +++ b/Makefile.am @@ -7,11 +7,11 @@ ACLOCAL_AMFLAGS = -I config SUBDIRS_BASE = src test contrib if CVC4_PROOF - SUBDIRS = proofs/lfsc_checker $(SUBDIRS_BASE) + SUBDIRS = proofs/signatures proofs/lfsc_checker $(SUBDIRS_BASE) else SUBDIRS = $(SUBDIRS_BASE) endif -DIST_SUBDIRS = proofs/lfsc_checker $(SUBDIRS_BASE) examples +DIST_SUBDIRS = proofs/signatures proofs/lfsc_checker $(SUBDIRS_BASE) examples .PHONY: examples examples: all @@ -130,11 +130,7 @@ EXTRA_DIST = \ doc/SmtEngine.3cvc_template.in \ doc/options.3cvc_template.in \ doc/libcvc4parser.3.in \ - doc/libcvc4compat.3.in \ - proofs/signatures/example.plf \ - proofs/signatures/sat.plf \ - proofs/signatures/smt.plf \ - proofs/signatures/th_base.plf + doc/libcvc4compat.3.in man_MANS = \ doc/cvc4.1 \ diff --git a/config/cvc4.m4 b/config/cvc4.m4 index 4b8b2e342..87d984ab4 100644 --- a/config/cvc4.m4 +++ b/config/cvc4.m4 @@ -17,6 +17,7 @@ handle_option() { ac_option="$[]1" case $ac_option in --bsd) ac_option='CVC4_BSD_LICENSED_CODE_ONLY=1' ;; + -enable-proofs | --enable-proofs) ac_option='--enable-proof' ;; -*|*=*) ;; production|production-*|debug|debug-*|competition|competition-*) # regexp `\?' not supported on Mac OS X diff --git a/configure.ac b/configure.ac index 38f5681fc..9179bc116 100644 --- a/configure.ac +++ b/configure.ac @@ -898,29 +898,13 @@ if test "$CVC4_CONFIGURE_IN_BUILDS" = yes -a -n "$CXXTEST"; then esac fi -AC_ARG_VAR(LFSC, [path to LFSC proof checker]) -AC_ARG_VAR(LFSCARGS, [arguments to pass to LFSC proof checker]) -if test -z "$LFSC"; then - AC_CHECK_PROGS(LFSC, lfsc, [], []) -else - AC_CHECK_PROG(LFSC, "$LFSC", [], []) -fi -AM_CONDITIONAL([PROOF_REGRESSIONS], [test -n "$LFSC" -a "$enable_proof" = yes]) -if test -n "$LFSC" -a "$enable_proof" = yes; then - TESTS_ENVIRONMENT="${TESTS_ENVIRONMENT:+$TESTS_ENVIRONMENT }LFSC=\"$LFSC $LFSCARGS\"" +TESTS_ENVIRONMENT= +RUN_REGRESSION_ARGS= +if test "$enable_proof" = yes; then RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--proof" fi AC_SUBST([TESTS_ENVIRONMENT]) AC_SUBST([RUN_REGRESSION_ARGS]) -if test -z "$LFSC"; then - support_proof_tests='no, lfsc proof checker unavailable' -elif test "$enable_proof" = yes; then - support_proof_tests='yes, proof regression tests enabled' -else - support_proof_tests='no, proof-generation disabled for this build' -fi -AC_SUBST([LFSC]) -AC_SUBST([LFSCARGS]) CXXTESTGEN= AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH]) @@ -1292,7 +1276,8 @@ AC_SUBST(MAN_DATE) AC_CONFIG_FILES([ Makefile.builds - Makefile] + Makefile + proofs/signatures/Makefile] m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^contrib/alttheoryskel/' | sort | sed 's,\.am$,,']) ) @@ -1422,7 +1407,6 @@ Dumping : $enable_dumping Muzzle : $enable_muzzle Unit tests : $support_unit_tests -Proof tests : $support_proof_tests gcov support : $enable_coverage gprof support: $enable_profiling diff --git a/proofs/signatures/Makefile.am b/proofs/signatures/Makefile.am new file mode 100644 index 000000000..610990ba2 --- /dev/null +++ b/proofs/signatures/Makefile.am @@ -0,0 +1,34 @@ +# These CORE_PLFs are combined to give a "master signature" against +# which proofs are checked internally when using --check-proofs. To +# add support for more theories, just list them here in the same order +# you would to the LFSC proof-checker binary. +# +CORE_PLFS = sat.plf smt.plf th_base.plf + +noinst_LTLIBRARIES = libsignatures.la + +dist_pkgdata_DATA = \ + $(CORE_PLFS) + +libsignatures_la_SOURCES = \ + signatures.cpp + +BUILT_SOURCES = \ + signatures.cpp + +signatures.cpp: $(CORE_PLFS) + $(AM_V_GEN)( \ + echo "namespace CVC4 {"; \ + echo "namespace proof {"; \ + echo; \ + echo "extern const char *const plf_signatures;"; \ + echo "const char *const plf_signatures = \"\\"; \ + cat $+ | sed 's,\\,\\\\,g;s,",\\",g;s,$$,\\n\\,g'; \ + echo "\";"; \ + echo; \ + echo "} /* CVC4::proof namespace */"; \ + echo "} /* CVC4 namespace */"; \ + ) > $@ + +EXTRA_DIST = \ + example.plf diff --git a/proofs/signatures/example.plf b/proofs/signatures/example.plf index 5df1f31c3..ab690eb51 100755 --- a/proofs/signatures/example.plf +++ b/proofs/signatures/example.plf @@ -1,116 +1,116 @@ -; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf
-
-; --------------------------------------------------------------------------------
-; input :
-; ( a = b )
-; ( b = f(c) )
-; ( a != f(c) V a != b )
-
-; theory lemma (by transitivity) :
-; ( a != b V b != f(c) V a = f(c) )
-
-
-; With the theory lemma, the input is unsatisfiable.
-; --------------------------------------------------------------------------------
-
-
-
-(check
-(% s sort
-(% a (term s)
-(% b (term s)
-(% c (term s)
-(% f (term (arrow s s))
-
-; -------------------- declaration of input formula -----------------------------------
-
-(% A1 (th_holds (= s a b))
-(% A2 (th_holds (= s b (apply _ _ f c)))
-(% A3 (th_holds (or (not (= s a (apply _ _ f c))) (not (= s a b))))
-
-
-; ------------------- specify that the following is a proof of the empty clause -----------------
-
-(: (holds cln)
-
-; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------
-
-(decl_atom (= s a b) (\ v1 (\ a1
-(decl_atom (= s b (apply _ _ f c)) (\ v2 (\ a2
-(decl_atom (= s a (apply _ _ f c)) (\ v3 (\ a3
-
-
-; --------------------------- proof of theory lemma ---------------------------------------------
-
-(satlem _ _
-(ast _ _ _ a1 (\ l1
-(ast _ _ _ a2 (\ l2
-(asf _ _ _ a3 (\ l3
-(clausify_false
-
-; this should be a proof of l1 ^ l2 ^ ~l3 => false
-; this is done by theory proof rules (currently just use "trust")
-
- trust
-
-))))))) (\ CT
-; CT is the clause ( ~v1 V ~v2 V v3 )
-
-; -------------------- clausification of input formulas -----------------------------------------
-
-(satlem _ _
-(asf _ _ _ a1 (\ l1
-(clausify_false
-
-; input formula A1 is ( ~l1 )
-; the following should be a proof of l1 ^ ( ~l1 ) => false
-; this is done by natural deduction rules
-
- (contra _ A1 l1)
-
-))) (\ C1
-; C1 is the clause ( v1 )
-
-
-(satlem _ _
-(asf _ _ _ a2 (\ l2
-(clausify_false
-
-; input formula A2 is ( ~l2 )
-; the following should be a proof of l2 ^ ( ~l2 ) => false
-; this is done by natural deduction rules
-
- (contra _ A2 l2)
-
-))) (\ C2
-; C2 is the clause ( v2 )
-
-
-(satlem _ _
-(ast _ _ _ a3 (\ l3
-(ast _ _ _ a1 (\ l1
-(clausify_false
-
-; input formula A3 is ( ~a3 V ~a1 )
-; the following should be a proof of a3 ^ a1 ^ ( ~a3 V ~a1 ) => false
-; this is done by natural deduction rules
-
- (contra _ l1 (or_elim_1 _ _ (not_not_intro _ l3) A3))
-
-))))) (\ C3
-; C3 is the clause ( ~v3 V ~v1 )
-
-
-
-; -------------------- resolution proof ------------------------------------------------------------
-
-(satlem_simplify _ _ _
-
-(R _ _ C1
-(R _ _ C2
-(R _ _ CT C3 v3) v2) v1)
-
-(\ x x))
-
-))))))))))))))))))))))))))
-)
\ No newline at end of file +; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf + +; -------------------------------------------------------------------------------- +; input : +; ( a = b ) +; ( b = f(c) ) +; ( a != f(c) V a != b ) + +; theory lemma (by transitivity) : +; ( a != b V b != f(c) V a = f(c) ) + + +; With the theory lemma, the input is unsatisfiable. +; -------------------------------------------------------------------------------- + + + +(check +(% s sort +(% a (term s) +(% b (term s) +(% c (term s) +(% f (term (arrow s s)) + +; -------------------- declaration of input formula ----------------------------------- + +(% A1 (th_holds (= s a b)) +(% A2 (th_holds (= s b (apply _ _ f c))) +(% A3 (th_holds (or (not (= s a (apply _ _ f c))) (not (= s a b)))) + + +; ------------------- specify that the following is a proof of the empty clause ----------------- + +(: (holds cln) + +; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------ + +(decl_atom (= s a b) (\ v1 (\ a1 +(decl_atom (= s b (apply _ _ f c)) (\ v2 (\ a2 +(decl_atom (= s a (apply _ _ f c)) (\ v3 (\ a3 + + +; --------------------------- proof of theory lemma --------------------------------------------- + +(satlem _ _ +(ast _ _ _ a1 (\ l1 +(ast _ _ _ a2 (\ l2 +(asf _ _ _ a3 (\ l3 +(clausify_false + +; this should be a proof of l1 ^ l2 ^ ~l3 => false +; this is done by theory proof rules (currently just use "trust") + + trust + +))))))) (\ CT +; CT is the clause ( ~v1 V ~v2 V v3 ) + +; -------------------- clausification of input formulas ----------------------------------------- + +(satlem _ _ +(asf _ _ _ a1 (\ l1 +(clausify_false + +; input formula A1 is ( ~l1 ) +; the following should be a proof of l1 ^ ( ~l1 ) => false +; this is done by natural deduction rules + + (contra _ A1 l1) + +))) (\ C1 +; C1 is the clause ( v1 ) + + +(satlem _ _ +(asf _ _ _ a2 (\ l2 +(clausify_false + +; input formula A2 is ( ~l2 ) +; the following should be a proof of l2 ^ ( ~l2 ) => false +; this is done by natural deduction rules + + (contra _ A2 l2) + +))) (\ C2 +; C2 is the clause ( v2 ) + + +(satlem _ _ +(ast _ _ _ a3 (\ l3 +(ast _ _ _ a1 (\ l1 +(clausify_false + +; input formula A3 is ( ~a3 V ~a1 ) +; the following should be a proof of a3 ^ a1 ^ ( ~a3 V ~a1 ) => false +; this is done by natural deduction rules + + (contra _ l1 (or_elim_1 _ _ (not_not_intro _ l3) A3)) + +))))) (\ C3 +; C3 is the clause ( ~v3 V ~v1 ) + + + +; -------------------- resolution proof ------------------------------------------------------------ + +(satlem_simplify _ _ _ + +(R _ _ C1 +(R _ _ C2 +(R _ _ CT C3 v3) v2) v1) + +(\ x x)) + +)))))))))))))))))))))))))) +) diff --git a/proofs/signatures/sat.plf b/proofs/signatures/sat.plf index 09255f612..5e2f1cc44 100755 --- a/proofs/signatures/sat.plf +++ b/proofs/signatures/sat.plf @@ -1,127 +1,127 @@ -(declare bool type)
-(declare tt bool)
-(declare ff bool)
-
-(declare var type)
-
-(declare lit type)
-(declare pos (! x var lit))
-(declare neg (! x var lit))
-
-(declare clause type)
-(declare cln clause)
-(declare clc (! x lit (! c clause clause)))
-
-; constructs for general clauses for R, Q, satlem
-
-(declare concat (! c1 clause (! c2 clause clause)))
-(declare clr (! l lit (! c clause clause)))
-
-; code to check resolutions
-
-(program append ((c1 clause) (c2 clause)) clause
- (match c1 (cln c2) ((clc l c1') (clc l (append c1' c2)))))
-
-; we use marks as follows:
-; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable.
-; -- mark 2 to record if we are supposed to remove a negative occurrence of the variable.
-; -- mark 3 if we did indeed remove the variable positively
-; -- mark 4 if we did indeed remove the variable negatively
-(program simplify_clause ((c clause)) clause
- (match c
- (cln cln)
- ((clc l c1)
- (match l
- ; Set mark 1 on v if it is not set, to indicate we should remove it.
- ; After processing the rest of the clause, set mark 3 if we were already
- ; supposed to remove v (so if mark 1 was set when we began). Clear mark3
- ; if we were not supposed to be removing v when we began this call.
- ((pos v)
- (let m (ifmarked v tt (do (markvar v) ff))
- (let c' (simplify_clause c1)
- (match m
- (tt (do (ifmarked3 v v (markvar3 v)) c'))
- (ff (do (ifmarked3 v (markvar3 v) v) (markvar v) (clc l c')))))))
- ; the same as the code for tt, but using different marks.
- ((neg v)
- (let m (ifmarked2 v tt (do (markvar2 v) ff))
- (let c' (simplify_clause c1)
- (match m
- (tt (do (ifmarked4 v v (markvar4 v)) c'))
- (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c')))))))))
- ((concat c1 c2) (append (simplify_clause c1) (simplify_clause c2)))
- ((clr l c1)
- (match l
- ; set mark 1 to indicate we should remove v, and fail if
- ; mark 3 is not set after processing the rest of the clause
- ; (we will set mark 3 if we remove a positive occurrence of v).
- ((pos v)
- (let m (ifmarked v tt (do (markvar v) ff))
- (let m3 (ifmarked3 v (do (markvar3 v) tt) ff)
- (let c' (simplify_clause c1)
- (ifmarked3 v (do (match m3 (tt v) (ff (markvar3 v)))
- (match m (tt v) (ff (markvar v))) c')
- (fail clause))))))
- ; same as the tt case, but with different marks.
- ((neg v)
- (let m2 (ifmarked2 v tt (do (markvar2 v) ff))
- (let m4 (ifmarked4 v (do (markvar4 v) tt) ff)
- (let c' (simplify_clause c1)
- (ifmarked4 v (do (match m4 (tt v) (ff (markvar4 v)))
- (match m2 (tt v) (ff (markvar2 v))) c')
- (fail clause))))))
- ))))
-
-
-; resolution proofs
-
-(declare holds (! c clause type))
-
-(declare R (! c1 clause (! c2 clause
- (! u1 (holds c1)
- (! u2 (holds c2)
- (! n var
- (holds (concat (clr (pos n) c1)
- (clr (neg n) c2)))))))))
-
-(declare Q (! c1 clause (! c2 clause
- (! u1 (holds c1)
- (! u2 (holds c2)
- (! n var
- (holds (concat (clr (neg n) c1)
- (clr (pos n) c2)))))))))
-
-(declare satlem_simplify
- (! c1 clause
- (! c2 clause
- (! c3 clause
- (! u1 (holds c1)
- (! r (^ (simplify_clause c1) c2)
- (! u2 (! x (holds c2) (holds c3))
- (holds c3))))))))
-
-(declare satlem
- (! c clause
- (! c2 clause
- (! u (holds c)
- (! u2 (! v (holds c) (holds c2))
- (holds c2))))))
-
-; A little example to demonstrate simplify_clause.
-; It can handle nested clr's of both polarities,
-; and correctly cleans up marks when it leaves a
-; clr or clc scope. Uncomment and run with
-; --show-runs to see it in action.
-;
-; (check
-; (% v1 var
-; (% u1 (holds (concat (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln))))))
-; (clc (pos v1) (clc (pos v1) cln))))
-; (satlem _ _ _ u1 (\ x x))))))
-
-
-;(check
-; (% v1 var
-; (% u1 (holds (clr (neg v1) (concat (clc (neg v1) cln)
-; (clr (neg v1) (clc (neg v1) cln)))))
-; (satlem _ _ _ u1 (\ x x))))))
\ No newline at end of file +(declare bool type) +(declare tt bool) +(declare ff bool) + +(declare var type) + +(declare lit type) +(declare pos (! x var lit)) +(declare neg (! x var lit)) + +(declare clause type) +(declare cln clause) +(declare clc (! x lit (! c clause clause))) + +; constructs for general clauses for R, Q, satlem + +(declare concat (! c1 clause (! c2 clause clause))) +(declare clr (! l lit (! c clause clause))) + +; code to check resolutions + +(program append ((c1 clause) (c2 clause)) clause + (match c1 (cln c2) ((clc l c1') (clc l (append c1' c2))))) + +; we use marks as follows: +; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable. +; -- mark 2 to record if we are supposed to remove a negative occurrence of the variable. +; -- mark 3 if we did indeed remove the variable positively +; -- mark 4 if we did indeed remove the variable negatively +(program simplify_clause ((c clause)) clause + (match c + (cln cln) + ((clc l c1) + (match l + ; Set mark 1 on v if it is not set, to indicate we should remove it. + ; After processing the rest of the clause, set mark 3 if we were already + ; supposed to remove v (so if mark 1 was set when we began). Clear mark3 + ; if we were not supposed to be removing v when we began this call. + ((pos v) + (let m (ifmarked v tt (do (markvar v) ff)) + (let c' (simplify_clause c1) + (match m + (tt (do (ifmarked3 v v (markvar3 v)) c')) + (ff (do (ifmarked3 v (markvar3 v) v) (markvar v) (clc l c'))))))) + ; the same as the code for tt, but using different marks. + ((neg v) + (let m (ifmarked2 v tt (do (markvar2 v) ff)) + (let c' (simplify_clause c1) + (match m + (tt (do (ifmarked4 v v (markvar4 v)) c')) + (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c'))))))))) + ((concat c1 c2) (append (simplify_clause c1) (simplify_clause c2))) + ((clr l c1) + (match l + ; set mark 1 to indicate we should remove v, and fail if + ; mark 3 is not set after processing the rest of the clause + ; (we will set mark 3 if we remove a positive occurrence of v). + ((pos v) + (let m (ifmarked v tt (do (markvar v) ff)) + (let m3 (ifmarked3 v (do (markvar3 v) tt) ff) + (let c' (simplify_clause c1) + (ifmarked3 v (do (match m3 (tt v) (ff (markvar3 v))) + (match m (tt v) (ff (markvar v))) c') + (fail clause)))))) + ; same as the tt case, but with different marks. + ((neg v) + (let m2 (ifmarked2 v tt (do (markvar2 v) ff)) + (let m4 (ifmarked4 v (do (markvar4 v) tt) ff) + (let c' (simplify_clause c1) + (ifmarked4 v (do (match m4 (tt v) (ff (markvar4 v))) + (match m2 (tt v) (ff (markvar2 v))) c') + (fail clause)))))) + )))) + + +; resolution proofs + +(declare holds (! c clause type)) + +(declare R (! c1 clause (! c2 clause + (! u1 (holds c1) + (! u2 (holds c2) + (! n var + (holds (concat (clr (pos n) c1) + (clr (neg n) c2))))))))) + +(declare Q (! c1 clause (! c2 clause + (! u1 (holds c1) + (! u2 (holds c2) + (! n var + (holds (concat (clr (neg n) c1) + (clr (pos n) c2))))))))) + +(declare satlem_simplify + (! c1 clause + (! c2 clause + (! c3 clause + (! u1 (holds c1) + (! r (^ (simplify_clause c1) c2) + (! u2 (! x (holds c2) (holds c3)) + (holds c3)))))))) + +(declare satlem + (! c clause + (! c2 clause + (! u (holds c) + (! u2 (! v (holds c) (holds c2)) + (holds c2)))))) + +; A little example to demonstrate simplify_clause. +; It can handle nested clr's of both polarities, +; and correctly cleans up marks when it leaves a +; clr or clc scope. Uncomment and run with +; --show-runs to see it in action. +; +; (check +; (% v1 var +; (% u1 (holds (concat (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln)))))) +; (clc (pos v1) (clc (pos v1) cln)))) +; (satlem _ _ _ u1 (\ x x)))))) + + +;(check +; (% v1 var +; (% u1 (holds (clr (neg v1) (concat (clc (neg v1) cln) +; (clr (neg v1) (clc (neg v1) cln))))) +; (satlem _ _ _ u1 (\ x x)))))) diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index 75bfc442f..67ce3988a 100755 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -31,7 +31,7 @@ (! t1 (term (arrow s1 s2)) (! t2 (term s1) (term s2)))))) - + (declare ite (! s sort (! f formula (! t1 (term s) @@ -102,7 +102,7 @@ (! f formula (! u (th_holds f) (th_holds (not (not f)))))) - + (declare not_not_elim (! f formula (! u (th_holds (not (not f))) @@ -116,14 +116,14 @@ (! u1 (th_holds (not f1)) (! u2 (th_holds (or f1 f2)) (th_holds f2)))))) - + (declare or_elim_2 (! f1 formula (! f2 formula (! u1 (th_holds (not f2)) (! u2 (th_holds (or f1 f2)) (th_holds f1)))))) - + ;; and elimination (declare and_elim_1 @@ -131,13 +131,13 @@ (! f2 formula (! u (th_holds (and f1 f2)) (th_holds f1))))) - + (declare and_elim_2 (! f1 formula (! f2 formula (! u (th_holds (and f1 f2)) (th_holds f2))))) - + ;; not impl elimination (declare not_impl_elim_1 @@ -145,18 +145,18 @@ (! f2 formula (! u (th_holds (not (impl f1 f2))) (th_holds f1))))) - + (declare not_impl_elim_2 (! f1 formula (! f2 formula (! u (th_holds (not (impl f1 f2))) (th_holds (not f2)))))) - + ;; impl elimination (declare impl_intro (! f1 formula (! f2 formula - (! i1 (! u (th_holds f1) + (! i1 (! u (th_holds f1) (th_holds f2)) (th_holds (impl f1 f2)))))) @@ -164,9 +164,9 @@ (! f1 formula (! f2 formula (! u1 (th_holds f1) - (! u2 (th_holds (impl f1 f2)) + (! u2 (th_holds (impl f1 f2)) (th_holds f2)))))) - + ;; iff elimination (declare iff_elim_1 @@ -174,7 +174,7 @@ (! f2 formula (! u1 (th_holds (iff f1 f2)) (th_holds (impl f1 f2)))))) - + (declare iff_elim_2 (! f1 formula (! f2 formula @@ -204,7 +204,7 @@ (! u1 (th_holds a) (! u2 (th_holds (ifte a b c)) (th_holds b))))))) - + (declare ite_elim_2 (! a formula (! b formula @@ -212,7 +212,7 @@ (! u1 (th_holds (not a)) (! u2 (th_holds (ifte a b c)) (th_holds c))))))) - + (declare ite_elim_3 (! a formula (! b formula @@ -220,7 +220,7 @@ (! u1 (th_holds (not b)) (! u2 (th_holds (ifte a b c)) (th_holds c))))))) - + (declare ite_elim_2n (! a formula (! b formula @@ -236,7 +236,7 @@ (! u1 (th_holds a) (! u2 (th_holds (not (ifte a b c))) (th_holds (not b)))))))) - + (declare not_ite_elim_2 (! a formula (! b formula @@ -244,7 +244,7 @@ (! u1 (th_holds (not a)) (! u2 (th_holds (not (ifte a b c))) (th_holds (not c)))))))) - + (declare not_ite_elim_3 (! a formula (! b formula @@ -252,7 +252,7 @@ (! u1 (th_holds b) (! u2 (th_holds (not (ifte a b c))) (th_holds (not c)))))))) - + (declare not_ite_elim_2n (! a formula (! b formula @@ -260,9 +260,9 @@ (! u1 (th_holds a) (! u2 (th_holds (not (ifte (not a) b c))) (th_holds (not c)))))))) - - - + + + ;; How to do CNF for disjunctions of theory literals. ;; ;; Given theory literals F1....Fn, and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))). @@ -287,7 +287,7 @@ ;; (contra _ ;; (or_elim_1 _ _ l{n-1} ;; ... -;; (or_elim_1 _ _ l2 +;; (or_elim_1 _ _ l2 ;; (or_elim_1 _ _ l1 A))))) ln) ;; ;;))))))) (\ C @@ -305,9 +305,9 @@ ;;(clausify_false ;; ;; (contra _ l3 -;; (or_elim_1 _ _ l2 +;; (or_elim_1 _ _ l2 ;; (or_elim_1 _ _ (not_not_intro l1) A)))) ;; ;;))))))) (\ C ;; -;; C should be the clause (~v1 V v2 V ~v3 )
\ No newline at end of file +;; C should be the clause (~v1 V v2 V ~v3 ) diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf index e66990de4..7b0b086dc 100755 --- a/proofs/signatures/th_base.plf +++ b/proofs/signatures/th_base.plf @@ -1,107 +1,107 @@ -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Atomization / Clausification
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-; binding between an LF var and an (atomic) formula
-(declare atom (! v var (! p formula type)))
-
-(declare decl_atom
- (! f formula
- (! u (! v var
- (! a (atom v f)
- (holds cln)))
- (holds cln))))
-
-; direct clausify
-(declare clausify_form
- (! f formula
- (! v var
- (! a (atom v f)
- (! u (th_holds f)
- (holds (clc (pos v) cln)))))))
-
-(declare clausify_form_not
- (! f formula
- (! v var
- (! a (atom v f)
- (! u (th_holds (not f))
- (holds (clc (neg v) cln)))))))
-
-(declare clausify_false
- (! u (th_holds false)
- (holds cln)))
-
-
-(declare th_let_pf
- (! f formula
- (! u (th_holds f)
- (! u2 (! v (th_holds f) (holds cln))
- (holds cln)))))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Theory reasoning
-; - make a series of assumptions and then derive a contradiction (or false)
-; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"
-; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(declare ast
- (! v var
- (! f formula
- (! C clause
- (! r (atom v f) ;this is specified
- (! u (! o (th_holds f)
- (holds C))
- (holds (clc (neg v) C))))))))
-
-(declare asf
- (! v var
- (! f formula
- (! C clause
- (! r (atom v f)
- (! u (! o (th_holds (not f))
- (holds C))
- (holds (clc (pos v) C))))))))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Theory of Equality and Congruence Closure
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-; temporary :
-(declare trust (th_holds false))
-
-(declare refl
- (! s sort
- (! t (term s)
- (th_holds (= s t t)))))
-
-(declare symm (! s sort
- (! x (term s)
- (! y (term s)
- (! u (th_holds (= _ x y))
- (th_holds (= _ y x)))))))
-
-(declare trans (! s sort
- (! x (term s)
- (! y (term s)
- (! z (term s)
- (! u (th_holds (= _ x y))
- (! u (th_holds (= _ y z))
- (th_holds (= _ x z)))))))))
-
-(declare cong (! s1 sort
- (! s2 sort
- (! a1 (term (arrow s1 s2))
- (! b1 (term (arrow s1 s2))
- (! a2 (term s1)
- (! b2 (term s1)
- (! u1 (th_holds (= _ a1 b1))
- (! u2 (th_holds (= _ a2 b2))
- (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))
-
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; +; Atomization / Clausification +; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; binding between an LF var and an (atomic) formula +(declare atom (! v var (! p formula type))) + +(declare decl_atom + (! f formula + (! u (! v var + (! a (atom v f) + (holds cln))) + (holds cln)))) + +; direct clausify +(declare clausify_form + (! f formula + (! v var + (! a (atom v f) + (! u (th_holds f) + (holds (clc (pos v) cln))))))) + +(declare clausify_form_not + (! f formula + (! v var + (! a (atom v f) + (! u (th_holds (not f)) + (holds (clc (neg v) cln))))))) + +(declare clausify_false + (! u (th_holds false) + (holds cln))) + + +(declare th_let_pf + (! f formula + (! u (th_holds f) + (! u2 (! v (th_holds f) (holds cln)) + (holds cln))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; +; Theory reasoning +; - make a series of assumptions and then derive a contradiction (or false) +; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false" +; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn" +; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(declare ast + (! v var + (! f formula + (! C clause + (! r (atom v f) ;this is specified + (! u (! o (th_holds f) + (holds C)) + (holds (clc (neg v) C)))))))) + +(declare asf + (! v var + (! f formula + (! C clause + (! r (atom v f) + (! u (! o (th_holds (not f)) + (holds C)) + (holds (clc (pos v) C)))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; +; Theory of Equality and Congruence Closure +; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; temporary : +(declare trust (th_holds false)) + +(declare refl + (! s sort + (! t (term s) + (th_holds (= s t t))))) + +(declare symm (! s sort + (! x (term s) + (! y (term s) + (! u (th_holds (= _ x y)) + (th_holds (= _ y x))))))) + +(declare trans (! s sort + (! x (term s) + (! y (term s) + (! z (term s) + (! u (th_holds (= _ x y)) + (! u (th_holds (= _ y z)) + (th_holds (= _ x z))))))))) + +(declare cong (! s1 sort + (! s2 sort + (! a1 (term (arrow s1 s2)) + (! b1 (term (arrow s1 s2)) + (! a2 (term s1) + (! b2 (term s1) + (! u1 (th_holds (= _ a1 b1)) + (! u2 (th_holds (= _ a2 b2)) + (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2)))))))))))) + diff --git a/src/Makefile.am b/src/Makefile.am index 18382a8ab..c765d325a 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -396,7 +396,8 @@ libcvc4_la_LIBADD = \ @builddir@/prop/bvminisat/libbvminisat.la if CVC4_PROOF libcvc4_la_LIBADD += \ - @top_builddir@/proofs/lfsc_checker/liblfsc_checker.la + @top_builddir@/proofs/lfsc_checker/liblfsc_checker.la \ + @top_builddir@/proofs/signatures/libsignatures.la endif if CVC4_NEEDS_REPLACEMENT_FUNCTIONS diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 467b150d3..485a478d8 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -76,14 +76,20 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) if(q != NULL) { d_result = res = q->getResult(); } - // dump the model if option is set - if( status && - d_options[options::produceModels] && - d_options[options::dumpModels] && - ( res.asSatisfiabilityResult() == Result::SAT || - (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) { - Command* gm = new GetModelCommand(); - status = doCommandSingleton(gm); + // dump the model/proof if option is set + if(status) { + if( d_options[options::produceModels] && + d_options[options::dumpModels] && + ( res.asSatisfiabilityResult() == Result::SAT || + (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) { + Command* gm = new GetModelCommand(); + status = doCommandSingleton(gm); + } else if( d_options[options::proof] && + d_options[options::dumpProofs] && + res.asSatisfiabilityResult() == Result::UNSAT ) { + Command* gp = new GetProofCommand(); + status = doCommandSingleton(gp); + } } return status; } diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 971aa2131..24469c668 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -213,7 +213,6 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) if(d_lastWinner != 0) delete cmdExported; return ret; } else if(mode == 1) { // portfolio - d_seq->addCommand(cmd->clone()); // We currently don't support changing number of threads for each @@ -327,7 +326,26 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) lemmaSharingCleanup(); delete[] fns; - return portfolioReturn.second; + + bool status = portfolioReturn.second; + + // dump the model/proof if option is set + if(status) { + if( d_options[options::produceModels] && + d_options[options::dumpModels] && + ( d_result.asSatisfiabilityResult() == Result::SAT || + (d_result.isUnknown() && d_result.whyUnknown() == Result::INCOMPLETE) ) ) { + Command* gm = new GetModelCommand(); + status = doCommandSingleton(gm); + } else if( d_options[options::proof] && + d_options[options::dumpProofs] && + d_result.asSatisfiabilityResult() == Result::UNSAT ) { + Command* gp = new GetProofCommand(); + status = doCommandSingleton(gp); + } + } + + return status; } else if(mode == 2) { Command* cmdExported = d_lastWinner == 0 ? diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index d1baaa2e9..bf66629dd 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -108,6 +108,10 @@ int runCvc4(int argc, char* argv[], Options& opts) { ! opts[options::threadArgv].empty() ) { throw OptionException("Thread options cannot be used with sequential CVC4. Please build and use the portfolio binary `pcvc4'."); } +# else + if( opts[options::checkProofs] ) { + throw OptionException("Cannot run portfolio in check-proofs mode."); + } # endif progName = opts[options::binary_name].c_str(); @@ -201,8 +205,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { << "Notice: ...the experimental --incremental-parallel option.\n"; exprMgr = new ExprManager(opts); pExecutor = new CommandExecutor(*exprMgr, opts); - } - else { + } else { exprMgr = new ExprManager(threadOpts[0]); pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts); } diff --git a/src/options/mkoptions b/src/options/mkoptions index 2ff857a2f..8a3cec494 100755 --- a/src/options/mkoptions +++ b/src/options/mkoptions @@ -241,6 +241,7 @@ function handle_option { predicates= links= links_alternate= + smt_links= options_already_documented=false alternate_options_already_documented=false @@ -412,10 +413,28 @@ function handle_option { links_alternate="${links_alternate} $(echo "${args[$i]}" | sed 's,[^/]*/,,')" else links="${links} ${args[$i]}" - links_alternate="${links_alternate} ${args[$i]}" fi done ;; + :link-smt) + j=0 + while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do + let ++i + let ++j + if [ $j -eq 3 ]; then + echo "$kf:$lineno: error: attribute :link-smt can only take two arguments" >&2 + exit 1 + fi + if expr "${args[$i]}" : '.*/' &>/dev/null; then + echo "$kf:$lineno: error: attribute :link-smt cannot take alternates" >&2 + exit 1 + fi + smt_links="${smt_links} ${args[$i]}" + done + if [ $j -eq 1 ]; then + smt_links="${smt_links} \"true\"" + fi + ;; :include) while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do let ++i @@ -544,14 +563,33 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r fi run_links= run_links_alternate= + run_smt_links= + if [ -n "$links" -a -z "$smt_links" -a -n "$smtname" ]; then + echo "$kf:$lineno: warning: $smtname has no :link-smt, but equivalent command-line has :link" >&2 + elif [ -n "$smt_links" -a -z "$links" ] && [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o "$long_option_alternate" ]; then + echo "$kf:$lineno: warning: $smtname has a :link-smt, but equivalent command-line has no :link" >&2 + fi if [ -n "$links" ]; then + # command-line links for link in $links; do run_links="$run_links #line $lineno \"$kf\" preemptGetopt(extra_argc, extra_argv, \"$link\");" done fi + if [ -n "$smt_links" ]; then + # smt links + smt_links=($smt_links) + i=0 + while [ $i -lt ${#smt_links[@]} ]; do + run_smt_links="$run_smt_links +#line $lineno \"$kf\" + smt->setOption(std::string(\"${smt_links[$i]}\"), SExpr(${smt_links[$(($i+1))]}));" + i=$((i+2)) + done + fi if [ -n "$links_alternate" ]; then + # command-line links for link in $links_alternate; do run_links_alternate="$run_links_alternate #line $lineno \"$kf\" @@ -732,7 +770,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - Options::current().assignBool(options::$internal, \"$smtname\", optionarg == \"true\", smt);$run_links + Options::current().assignBool(options::$internal, \"$smtname\", optionarg == \"true\", smt);$run_smt_links return; }" elif [ -n "$expect_arg" -a "$internal" != - ]; then @@ -749,7 +787,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - Options::current().assign(options::$internal, \"$smtname\", optionarg, smt);$run_links + Options::current().assign(options::$internal, \"$smtname\", optionarg, smt);$run_smt_links return; }" elif [ -n "$expect_arg" ]; then @@ -764,7 +802,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - $run_handlers$run_links + $run_handlers$run_smt_links return; }" else @@ -779,7 +817,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - $run_handlers$run_links + $run_handlers$run_smt_links return; }" fi diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 8ab5c121d..72bfa5603 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -153,6 +153,7 @@ void AstPrinter::toStream(std::ostream& out, const Command* c, tryToStream<GetModelCommand>(out, c) || tryToStream<GetAssignmentCommand>(out, c) || tryToStream<GetAssertionsCommand>(out, c) || + tryToStream<GetProofCommand>(out, c) || tryToStream<SetBenchmarkStatusCommand>(out, c) || tryToStream<SetBenchmarkLogicCommand>(out, c) || tryToStream<SetInfoCommand>(out, c) || @@ -307,6 +308,9 @@ static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() { static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() { out << "GetAssertions()"; } +static void toStream(std::ostream& out, const GetProofCommand* c) throw() { + out << "GetProof()"; +} static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { out << "SetBenchmarkStatus(" << c->getStatus() << ")"; } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index bd2626ddd..49ded4ecb 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -776,6 +776,7 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, tryToStream<GetModelCommand>(out, c) || tryToStream<GetAssignmentCommand>(out, c) || tryToStream<GetAssertionsCommand>(out, c) || + tryToStream<GetProofCommand>(out, c) || tryToStream<SetBenchmarkStatusCommand>(out, c) || tryToStream<SetBenchmarkLogicCommand>(out, c) || tryToStream<SetInfoCommand>(out, c) || @@ -1031,6 +1032,10 @@ static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() { out << "WHERE;"; } +static void toStream(std::ostream& out, const GetProofCommand* c) throw() { + out << "DUMP_PROOF;"; +} + static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { out << "% (set-info :status " << c->getStatus() << ")"; } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index b743ba70e..c56d87da6 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -577,6 +577,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream<GetModelCommand>(out, c) || tryToStream<GetAssignmentCommand>(out, c) || tryToStream<GetAssertionsCommand>(out, c) || + tryToStream<GetProofCommand>(out, c) || tryToStream<SetBenchmarkStatusCommand>(out, c) || tryToStream<SetBenchmarkLogicCommand>(out, c) || tryToStream<SetInfoCommand>(out, c) || @@ -858,6 +859,10 @@ static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() { out << "(get-assertions)"; } +static void toStream(std::ostream& out, const GetProofCommand* c) throw() { + out << "(get-proof)"; +} + static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { out << "(set-info :status " << c->getStatus() << ")"; } diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 8e9c4cd21..39e802b62 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -32,37 +32,45 @@ CnfProof::CnfProof(CnfStream* stream) Expr CnfProof::getAtom(prop::SatVariable var) { - prop::SatLiteral lit (var); - Node node = d_cnfStream->getNode(lit); + prop::SatLiteral lit (var); + Node node = d_cnfStream->getNode(lit); Expr atom = node.toExpr(); - return atom; + return atom; } CnfProof::~CnfProof() { } +LFSCCnfProof::iterator LFSCCnfProof::begin_atom_mapping() { + return iterator(*this, ProofManager::currentPM()->begin_vars()); +} + +LFSCCnfProof::iterator LFSCCnfProof::end_atom_mapping() { + return iterator(*this, ProofManager::currentPM()->end_vars()); +} + void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) { ProofManager::var_iterator it = ProofManager::currentPM()->begin_vars(); ProofManager::var_iterator end = ProofManager::currentPM()->end_vars(); - + for (;it != end; ++it) { os << "(decl_atom "; - + if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) { Expr atom = getAtom(*it); - LFSCTheoryProof::printFormula(atom, os); + LFSCTheoryProof::printTerm(atom, os); } else { // print fake atoms for all other logics - os << "true "; + os << "true "; } os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n"; - paren << ")))"; + paren << ")))"; } } void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) { - printInputClauses(os, paren); + printInputClauses(os, paren); printTheoryLemmas(os, paren); } @@ -70,51 +78,49 @@ void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { os << " ;; Input Clauses \n"; ProofManager::clause_iterator it = ProofManager::currentPM()->begin_input_clauses(); ProofManager::clause_iterator end = ProofManager::currentPM()->end_input_clauses(); - + for (; it != end; ++it) { ClauseId id = it->first; const prop::SatClause* clause = it->second; os << "(satlem _ _ "; - std::ostringstream clause_paren; + std::ostringstream clause_paren; printClause(*clause, os, clause_paren); os << " (clausify_false trust)" << clause_paren.str(); - os << "( \\ " << ProofManager::getInputClauseName(id) << "\n"; - paren << "))"; + os << "( \\ " << ProofManager::getInputClauseName(id) << "\n"; + paren << "))"; } } void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) { - os << " ;; Theory Lemmas \n"; + os << " ;; Theory Lemmas \n"; ProofManager::clause_iterator it = ProofManager::currentPM()->begin_lemmas(); ProofManager::clause_iterator end = ProofManager::currentPM()->end_lemmas(); - + for (; it != end; ++it) { ClauseId id = it->first; const prop::SatClause* clause = it->second; os << "(satlem _ _ "; - std::ostringstream clause_paren; + std::ostringstream clause_paren; printClause(*clause, os, clause_paren); os << " (clausify_false trust)" << clause_paren.str(); - os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n"; - paren << "))"; + os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n"; + paren << "))"; } } void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren) { for (unsigned i = 0; i < clause.size(); ++i) { prop::SatLiteral lit = clause[i]; - prop::SatVariable var = lit.getSatVariable(); + prop::SatVariable var = lit.getSatVariable(); if (lit.isNegated()) { os << "(ast _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " "; - paren << "))"; + paren << "))"; } else { os << "(asf _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " "; - paren << "))"; + paren << "))"; } } } - } /* CVC4 namespace */ - diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 9a2dbe655..0a932f906 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -13,7 +13,7 @@ ** ** A manager for CnfProofs. ** - ** + ** **/ #ifndef __CVC4__CNF_PROOF_H @@ -25,36 +25,68 @@ #include <ext/hash_set> #include <ext/hash_map> -#include <iostream> +#include <iostream> namespace CVC4 { namespace prop { -class CnfStream; + class CnfStream; } +class CnfProof; + +class AtomIterator { + CnfProof& d_cnf; + ProofManager::var_iterator d_it; + +public: + AtomIterator(CnfProof& cnf, const ProofManager::var_iterator& it) + : d_cnf(cnf), d_it(it) + {} + inline Expr operator*(); + AtomIterator& operator++() { ++d_it; return *this; } + AtomIterator operator++(int) { AtomIterator x = *this; ++d_it; return x; } + bool operator==(const AtomIterator& it) const { return &d_cnf == &it.d_cnf && d_it == it.d_it; } + bool operator!=(const AtomIterator& it) const { return !(*this == it); } +};/* class AtomIterator */ + class CnfProof { protected: CVC4::prop::CnfStream* d_cnfStream; Expr getAtom(prop::SatVariable var); + friend class AtomIterator; public: CnfProof(CVC4::prop::CnfStream* cnfStream); + typedef AtomIterator iterator; + virtual iterator begin_atom_mapping() = 0; + virtual iterator end_atom_mapping() = 0; + virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0; virtual void printClauses(std::ostream& os, std::ostream& paren) = 0; - virtual ~CnfProof(); + virtual ~CnfProof(); }; -class LFSCCnfProof: public CnfProof { +class LFSCCnfProof : public CnfProof { void printInputClauses(std::ostream& os, std::ostream& paren); void printTheoryLemmas(std::ostream& os, std::ostream& paren); void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren); + public: LFSCCnfProof(CVC4::prop::CnfStream* cnfStream) : CnfProof(cnfStream) {} + + virtual iterator begin_atom_mapping(); + virtual iterator end_atom_mapping(); + virtual void printAtomMapping(std::ostream& os, std::ostream& paren); virtual void printClauses(std::ostream& os, std::ostream& paren); }; +inline Expr AtomIterator::operator*() { + return d_cnf.getAtom(*d_it); +} + } /* CVC4 namespace */ + #endif /* __CVC4__CNF_PROOF_H */ diff --git a/src/proof/proof.h b/src/proof/proof.h index 02f8f7684..e3b776cce 100644 --- a/src/proof/proof.h +++ b/src/proof/proof.h @@ -23,7 +23,7 @@ #ifdef CVC4_PROOF # define PROOF(x) if(options::proof()) { x; } -# define NULLPROOF(x) (options::proof())? x : NULL +# define NULLPROOF(x) (options::proof()) ? x : NULL # define PROOF_ON() options::proof() #else /* CVC4_PROOF */ # define PROOF(x) diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 110e6b79a..14a82b17b 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -28,14 +28,10 @@ namespace CVC4 { std::string append(const std::string& str, uint64_t num) { std::ostringstream os; - os << str << num; - return os.str(); + os << str << num; + return os.str(); } - -bool ProofManager::isInitialized = false; -ProofManager* ProofManager::proofManager = NULL; - ProofManager::ProofManager(ProofFormat format): d_satProof(NULL), d_cnfProof(NULL), @@ -50,41 +46,43 @@ ProofManager::~ProofManager() { delete d_cnfProof; delete d_theoryProof; delete d_fullProof; - for (IdToClause::iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) { - delete it->second; + + for(IdToClause::iterator it = d_inputClauses.begin(); + it != d_inputClauses.end(); + ++it) { + delete it->second; } - for (IdToClause::iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) { - delete it->second; + + for(IdToClause::iterator it = d_theoryLemmas.begin(); + it != d_theoryLemmas.end(); + ++it) { + delete it->second; } - // FIXME: memory leak because there are deleted theory lemmas that were not used in the - // SatProof + + // FIXME: memory leak because there are deleted theory lemmas that + // were not used in the SatProof } ProofManager* ProofManager::currentPM() { - if (isInitialized) { - return proofManager; - } else { - proofManager = new ProofManager(); - isInitialized = true; - return proofManager; - } + return smt::currentProofManager(); } Proof* ProofManager::getProof(SmtEngine* smt) { - if (currentPM()->d_fullProof != NULL) + if (currentPM()->d_fullProof != NULL) { return currentPM()->d_fullProof; + } Assert (currentPM()->d_format == LFSC); currentPM()->d_fullProof = new LFSCProof(smt, (LFSCSatProof*)getSatProof(), (LFSCCnfProof*)getCnfProof(), - (LFSCTheoryProof*)getTheoryProof()); + (LFSCTheoryProof*)getTheoryProof()); return currentPM()->d_fullProof; } SatProof* ProofManager::getSatProof() { Assert (currentPM()->d_satProof); - return currentPM()->d_satProof; + return currentPM()->d_satProof; } CnfProof* ProofManager::getCnfProof() { @@ -107,7 +105,7 @@ void ProofManager::initSatProof(Minisat::Solver* solver) { void ProofManager::initCnfProof(prop::CnfStream* cnfStream) { Assert (currentPM()->d_cnfProof == NULL); Assert (currentPM()->d_format == LFSC); - currentPM()->d_cnfProof = new LFSCCnfProof(cnfStream); + currentPM()->d_cnfProof = new LFSCCnfProof(cnfStream); } void ProofManager::initTheoryProof() { @@ -126,8 +124,8 @@ std::string ProofManager::getLitName(prop::SatLiteral lit) {return append("l", l void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) { for (unsigned i = 0; i < clause->size(); ++i) { - prop::SatLiteral lit = clause->operator[](i); - d_propVars.insert(lit.getSatVariable()); + prop::SatLiteral lit = clause->operator[](i); + d_propVars.insert(lit.getSatVariable()); } if (kind == INPUT) { d_inputClauses.insert(std::make_pair(id, clause)); @@ -138,11 +136,11 @@ void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseK } void ProofManager::addAssertion(Expr formula) { - d_inputFormulas.insert(formula); + d_inputFormulas.insert(formula); } void ProofManager::setLogic(const std::string& logic_string) { - d_logic = logic_string; + d_logic = logic_string; } @@ -158,17 +156,24 @@ LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, void LFSCProof::toStream(std::ostream& out) { smt::SmtScope scope(d_smtEngine); std::ostringstream paren; - out << "(check \n"; - if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) { - d_theoryProof->printAssertions(out, paren); + out << "(check\n"; + if (d_theoryProof == NULL) { + d_theoryProof = new LFSCTheoryProof(); + } + for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping(); + i != d_cnfProof->end_atom_mapping(); + ++i) { + d_theoryProof->addDeclaration(*i); } - out << "(: (holds cln) \n"; + d_theoryProof->printAssertions(out, paren); + out << "(: (holds cln)\n"; d_cnfProof->printAtomMapping(out, paren); d_cnfProof->printClauses(out, paren); - d_satProof->printResolutions(out, paren); + d_satProof->printResolutions(out, paren); paren <<")))\n;;"; - out << paren.str(); + out << paren.str(); + out << "\n"; } -} /* CVC4 namespace */ +} /* CVC4 namespace */ diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index e33f1a63f..ab8a7b2bc 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -9,11 +9,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief A manager for Proofs. + ** \brief A manager for Proofs ** ** A manager for Proofs. - ** - ** **/ #include "cvc4_private.h" @@ -21,7 +19,7 @@ #ifndef __CVC4__PROOF_MANAGER_H #define __CVC4__PROOF_MANAGER_H -#include <iostream> +#include <iostream> #include "proof/proof.h" #include "util/proof.h" @@ -29,15 +27,15 @@ // forward declarations namespace Minisat { class Solver; -} +}/* Minisat namespace */ namespace CVC4 { namespace prop { class CnfStream; -} +}/* CVC4::prop namespace */ -class SmtEngine; +class SmtEngine; typedef int ClauseId; @@ -51,10 +49,10 @@ class LFSCCnfProof; class LFSCTheoryProof; namespace prop { -typedef uint64_t SatVariable; -class SatLiteral; -typedef std::vector<SatLiteral> SatClause; -} + typedef uint64_t SatVariable; + class SatLiteral; + typedef std::vector<SatLiteral> SatClause; +}/* CVC4::prop namespace */ // different proof modes enum ProofFormat { @@ -64,7 +62,7 @@ enum ProofFormat { std::string append(const std::string& str, uint64_t num); -typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; +typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet; typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; @@ -74,35 +72,36 @@ enum ClauseKind { INPUT, THEORY_LEMMA, LEARNT -}; +};/* enum ClauseKind */ class ProofManager { SatProof* d_satProof; CnfProof* d_cnfProof; - TheoryProof* d_theoryProof; + TheoryProof* d_theoryProof; // information that will need to be shared across proofs IdToClause d_inputClauses; IdToClause d_theoryLemmas; ExprSet d_inputFormulas; VarSet d_propVars; - - Proof* d_fullProof; + + Proof* d_fullProof; ProofFormat d_format; - - static ProofManager* proofManager; - static bool isInitialized; - ProofManager(ProofFormat format = LFSC); - ~ProofManager(); + protected: std::string d_logic; + public: + ProofManager(ProofFormat format = LFSC); + ~ProofManager(); + static ProofManager* currentPM(); - // initialization - static void initSatProof(Minisat::Solver* solver); + + // initialization + static void initSatProof(Minisat::Solver* solver); static void initCnfProof(CVC4::prop::CnfStream* cnfStream); static void initTheoryProof(); - + static Proof* getProof(SmtEngine* smt); static SatProof* getSatProof(); static CnfProof* getCnfProof(); @@ -110,9 +109,9 @@ public: // iterators over data shared by proofs typedef IdToClause::const_iterator clause_iterator; - typedef ExprSet::const_iterator assertions_iterator; + typedef ExprSet::const_iterator assertions_iterator; typedef VarSet::const_iterator var_iterator; - + clause_iterator begin_input_clauses() const { return d_inputClauses.begin(); } clause_iterator end_input_clauses() const { return d_inputClauses.end(); } @@ -124,10 +123,10 @@ public: var_iterator begin_vars() const { return d_propVars.begin(); } var_iterator end_vars() const { return d_propVars.end(); } - + void addAssertion(Expr formula); - void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); - + void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); + // variable prefixes static std::string getInputClauseName(ClauseId id); static std::string getLemmaClauseName(ClauseId id); @@ -136,7 +135,7 @@ public: static std::string getVarName(prop::SatVariable var); static std::string getAtomName(prop::SatVariable var); static std::string getLitName(prop::SatLiteral lit); - + void setLogic(const std::string& logic_string); const std::string getLogic() const { return d_logic; } };/* class ProofManager */ @@ -145,13 +144,13 @@ class LFSCProof : public Proof { LFSCSatProof* d_satProof; LFSCCnfProof* d_cnfProof; LFSCTheoryProof* d_theoryProof; - SmtEngine* d_smtEngine; + SmtEngine* d_smtEngine; public: - LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); + LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); virtual void toStream(std::ostream& out); virtual ~LFSCProof() {} -}; - +};/* class LFSCProof */ + }/* CVC4 namespace */ #endif /* __CVC4__PROOF_MANAGER_H */ diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index da9df0d42..3b5509ffb 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -25,7 +25,7 @@ using namespace Minisat; using namespace CVC4::prop; namespace CVC4 { -/// some helper functions +/// some helper functions void printLit (Minisat::Lit l) { Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1; @@ -33,16 +33,16 @@ void printLit (Minisat::Lit l) { void printClause (Minisat::Clause& c) { for (int i = 0; i < c.size(); i++) { - Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; + Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; } } void printLitSet(const LitSet& s) { for(LitSet::iterator it = s.begin(); it != s.end(); ++it) { printLit(*it); - Debug("proof:sat") << " "; + Debug("proof:sat") << " "; } - Debug("proof:sat") << endl; + Debug("proof:sat") << endl; } // purely debugging functions @@ -52,39 +52,38 @@ void printDebug (Minisat::Lit l) { void printDebug (Minisat::Clause& c) { for (int i = 0; i < c.size(); i++) { - Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; + Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; } Debug("proof:sat") << endl; } -int SatProof::d_idCounter = 0; +int SatProof::d_idCounter = 0; -/** +/** * Converts the clause associated to id to a set of literals - * + * * @param id the clause id - * @param set the clause converted to a set of literals + * @param set the clause converted to a set of literals */ void SatProof::createLitSet(ClauseId id, LitSet& set) { - Assert (set.empty()); + Assert(set.empty()); if(isUnit(id)) { set.insert(getUnit(id)); return; } if ( id == d_emptyClauseId) { - return; + return; } CRef ref = getClauseRef(id); - Assert (ref != CRef_Undef); - Clause& c = d_solver->ca[ref]; + Clause& c = getClause(ref); for (int i = 0; i < c.size(); i++) { - set.insert(c[i]); + set.insert(c[i]); } } -/** +/** * Resolves clause1 and clause2 on variable var and stores the * result in clause1 * @param v @@ -93,36 +92,40 @@ void SatProof::createLitSet(ClauseId id, LitSet& set) { */ bool resolve(const Lit v, LitSet& clause1, LitSet& clause2, bool s) { Assert(!clause1.empty()); - Assert(!clause2.empty()); - Lit var = sign(v) ? ~v : v; + Assert(!clause2.empty()); + Lit var = sign(v) ? ~v : v; if (s) { // literal appears positive in the first clause if( !clause2.count(~var)) { - Debug("proof:sat") << "proof:resolve: Missing literal "; - printLit(var); - Debug("proof:sat") << endl; - return false; + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:resolve: Missing literal "; + printLit(var); + Debug("proof:sat") << endl; + } + return false; } clause1.erase(var); clause2.erase(~var); for (LitSet::iterator it = clause2.begin(); it!= clause2.end(); ++it) { - clause1.insert(*it); + clause1.insert(*it); } } else { // literal appears negative in the first clause if( !clause1.count(~var) || !clause2.count(var)) { - Debug("proof:sat") << "proof:resolve: Missing literal "; - printLit(var); - Debug("proof:sat") << endl; - return false; + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:resolve: Missing literal "; + printLit(var); + Debug("proof:sat") << endl; + } + return false; } clause1.erase(~var); clause2.erase(var); for (LitSet::iterator it = clause2.begin(); it!= clause2.end(); ++it) { - clause1.insert(*it); + clause1.insert(*it); } } - return true; + return true; } /// ResChain @@ -135,16 +138,16 @@ ResChain::ResChain(ClauseId start) : void ResChain::addStep(Lit lit, ClauseId id, bool sign) { ResStep step(lit, id, sign); - d_steps.push_back(step); + d_steps.push_back(step); } void ResChain::addRedundantLit(Lit lit) { if (d_redundantLits) { - d_redundantLits->insert(lit); + d_redundantLits->insert(lit); } else { d_redundantLits = new LitSet(); - d_redundantLits->insert(lit); + d_redundantLits->insert(lit); } } @@ -156,7 +159,7 @@ ProofProxy::ProofProxy(SatProof* proof): {} void ProofProxy::updateCRef(CRef oldref, CRef newref) { - d_proof->updateCRef(oldref, newref); + d_proof->updateCRef(oldref, newref); } @@ -183,27 +186,27 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) : d_seenInput(), d_seenLemmas() { - d_proxy = new ProofProxy(this); + d_proxy = new ProofProxy(this); } -/** +/** * Returns true if the resolution chain corresponding to id * does resolve to the clause associated to id - * @param id - * - * @return + * @param id + * + * @return */ bool SatProof::checkResolution(ClauseId id) { if(d_checkRes) { - bool validRes = true; - Assert (d_resChains.find(id) != d_resChains.end()); + bool validRes = true; + Assert(d_resChains.find(id) != d_resChains.end()); ResChain* res = d_resChains[id]; LitSet clause1; createLitSet(res->getStart(), clause1); - ResSteps& steps = res->getSteps(); + ResSteps& steps = res->getSteps(); for (unsigned i = 0; i < steps.size(); i++) { Lit var = steps[i].lit; - LitSet clause2; + LitSet clause2; createLitSet (steps[i].id, clause2); bool res = resolve (var, clause1, clause2, steps[i].sign); if(res == false) { @@ -215,35 +218,38 @@ bool SatProof::checkResolution(ClauseId id) { if (isUnit(id)) { // special case if it was a unit clause Lit unit = getUnit(id); - validRes = clause1.size() == clause1.count(unit) && !clause1.empty(); - return validRes; + validRes = clause1.size() == clause1.count(unit) && !clause1.empty(); + return validRes; } if (id == d_emptyClauseId) { - return clause1.empty(); + return clause1.empty(); } CRef ref = getClauseRef(id); - Assert (ref != CRef_Undef); - Clause& c = d_solver->ca[ref]; + Clause& c = getClause(ref); for (int i = 0; i < c.size(); ++i) { int count = clause1.erase(c[i]); if (count == 0) { - Debug("proof:sat") << "proof:checkResolution::literal not in computed result "; - printLit(c[i]); - Debug("proof:sat") << "\n"; - validRes = false; + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:checkResolution::literal not in computed result "; + printLit(c[i]); + Debug("proof:sat") << "\n"; + } + validRes = false; } } validRes = clause1.empty(); if (! validRes) { - Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, unremoved literals: \n"; - printLitSet(clause1); - Debug("proof:sat") << "proof:checkResolution:: result should be: \n"; - printClause(c); + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, unremoved literals: \n"; + printLitSet(clause1); + Debug("proof:sat") << "proof:checkResolution:: result should be: \n"; + printClause(c); + } } - return validRes; - + return validRes; + } else { - return true; + return true; } } @@ -254,16 +260,16 @@ bool SatProof::checkResolution(ClauseId id) { ClauseId SatProof::getClauseId(::Minisat::CRef ref) { if(d_clauseId.find(ref) == d_clauseId.end()) { - Debug("proof:sat") << "Missing clause \n"; + Debug("proof:sat") << "Missing clause \n"; } Assert(d_clauseId.find(ref) != d_clauseId.end()); - return d_clauseId[ref]; + return d_clauseId[ref]; } ClauseId SatProof::getClauseId(::Minisat::Lit lit) { Assert(d_unitId.find(toInt(lit)) != d_unitId.end()); - return d_unitId[toInt(lit)]; + return d_unitId[toInt(lit)]; } Minisat::CRef SatProof::getClauseRef(ClauseId id) { @@ -273,79 +279,85 @@ Minisat::CRef SatProof::getClauseRef(ClauseId id) { << (isUnit(id)? "Unit" : "") << endl; } Assert(d_idClause.find(id) != d_idClause.end()); - return d_idClause[id]; + return d_idClause[id]; } Clause& SatProof::getClause(CRef ref) { - return d_solver->ca[ref]; + Assert(ref != CRef_Undef); + Assert(ref >= 0 && ref < d_solver->ca.size()); + return d_solver->ca[ref]; } + Minisat::Lit SatProof::getUnit(ClauseId id) { - Assert (d_idUnit.find(id) != d_idUnit.end()); - return d_idUnit[id]; + Assert(d_idUnit.find(id) != d_idUnit.end()); + return d_idUnit[id]; } bool SatProof::isUnit(ClauseId id) { - return d_idUnit.find(id) != d_idUnit.end(); + return d_idUnit.find(id) != d_idUnit.end(); } bool SatProof::isUnit(::Minisat::Lit lit) { - return d_unitId.find(toInt(lit)) != d_unitId.end(); + return d_unitId.find(toInt(lit)) != d_unitId.end(); } ClauseId SatProof::getUnitId(::Minisat::Lit lit) { - Assert(isUnit(lit)); - return d_unitId[toInt(lit)]; + Assert(isUnit(lit)); + return d_unitId[toInt(lit)]; } bool SatProof::hasResolution(ClauseId id) { - return d_resChains.find(id) != d_resChains.end(); + return d_resChains.find(id) != d_resChains.end(); } bool SatProof::isInputClause(ClauseId id) { - return (d_inputClauses.find(id) != d_inputClauses.end()); + return (d_inputClauses.find(id) != d_inputClauses.end()); } bool SatProof::isLemmaClause(ClauseId id) { - return (d_lemmaClauses.find(id) != d_lemmaClauses.end()); + return (d_lemmaClauses.find(id) != d_lemmaClauses.end()); } void SatProof::print(ClauseId id) { if (d_deleted.find(id) != d_deleted.end()) { - Debug("proof:sat") << "del"<<id; + Debug("proof:sat") << "del"<<id; } else if (isUnit(id)) { - printLit(getUnit(id)); + printLit(getUnit(id)); } else if (id == d_emptyClauseId) { - Debug("proof:sat") << "empty "<< endl; + Debug("proof:sat") << "empty "<< endl; } else { - CRef ref = getClauseRef(id); - Assert (ref != CRef_Undef); - printClause(d_solver->ca[ref]); + CRef ref = getClauseRef(id); + printClause(getClause(ref)); } } void SatProof::printRes(ClauseId id) { Assert(hasResolution(id)); Debug("proof:sat") << "id "<< id <<": "; - printRes(d_resChains[id]); + printRes(d_resChains[id]); } void SatProof::printRes(ResChain* res) { ClauseId start_id = res->getStart(); - Debug("proof:sat") << "("; - print(start_id); + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "("; + print(start_id); + } ResSteps& steps = res->getSteps(); for(unsigned i = 0; i < steps.size(); i++ ) { Lit v = steps[i].lit; ClauseId id = steps[i].id; - Debug("proof:sat") << "["; - printLit(v); - Debug("proof:sat") << "] "; - print(id); + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "["; + printLit(v); + Debug("proof:sat") << "] "; + print(id); + } } Debug("proof:sat") << ") \n"; } @@ -353,23 +365,23 @@ void SatProof::printRes(ResChain* res) { /// registration methods ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind) { - Assert(clause != CRef_Undef); + Assert(clause != CRef_Undef); ClauseIdMap::iterator it = d_clauseId.find(clause); - if (it == d_clauseId.end()) { - ClauseId newId = d_idCounter++; - d_clauseId[clause]= newId; - d_idClause[newId] =clause; - if (kind == INPUT) { - Assert (d_inputClauses.find(newId) == d_inputClauses.end()); - d_inputClauses.insert(newId); - } - if (kind == THEORY_LEMMA) { - Assert (d_lemmaClauses.find(newId) == d_lemmaClauses.end()); - d_lemmaClauses.insert(newId); - } - } - Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n"; - return d_clauseId[clause]; + if (it == d_clauseId.end()) { + ClauseId newId = d_idCounter++; + d_clauseId[clause] = newId; + d_idClause[newId] = clause; + if (kind == INPUT) { + Assert(d_inputClauses.find(newId) == d_inputClauses.end()); + d_inputClauses.insert(newId); + } + if (kind == THEORY_LEMMA) { + Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); + d_lemmaClauses.insert(newId); + } + } + Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n"; + return d_clauseId[clause]; } ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) { @@ -377,44 +389,42 @@ ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) { if (it == d_unitId.end()) { ClauseId newId = d_idCounter++; d_unitId[toInt(lit)] = newId; - d_idUnit[newId] = lit; + d_idUnit[newId] = lit; if (kind == INPUT) { - Assert (d_inputClauses.find(newId) == d_inputClauses.end()); - d_inputClauses.insert(newId); + Assert(d_inputClauses.find(newId) == d_inputClauses.end()); + d_inputClauses.insert(newId); } if (kind == THEORY_LEMMA) { - Assert (d_lemmaClauses.find(newId) == d_lemmaClauses.end()); - d_lemmaClauses.insert(newId); + Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); + d_lemmaClauses.insert(newId); } - } - Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n"; - return d_unitId[toInt(lit)]; + Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n"; + return d_unitId[toInt(lit)]; } void SatProof::removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen) { // if we already added the literal return if (seen.count(lit)) { - return; + return; } CRef reason_ref = d_solver->reason(var(lit)); if (reason_ref == CRef_Undef) { seen.insert(lit); - removeStack.push_back(lit); - return; + removeStack.push_back(lit); + return; } - Assert (reason_ref != CRef_Undef); - int size = d_solver->ca[reason_ref].size(); + int size = getClause(reason_ref).size(); for (int i = 1; i < size; i++ ) { - Lit v = d_solver->ca[reason_ref][i]; + Lit v = getClause(reason_ref)[i]; if(inClause.count(v) == 0 && seen.count(v) == 0) { removedDfs(v, removedSet, removeStack, inClause, seen); } } if(seen.count(lit) == 0) { - seen.insert(lit); + seen.insert(lit); removeStack.push_back(lit); } } @@ -427,39 +437,41 @@ void SatProof::removeRedundantFromRes(ResChain* res, ClauseId id) { } LitSet inClause; - createLitSet(id, inClause); - + createLitSet(id, inClause); + LitVector removeStack; - LitSet seen; + LitSet seen; for (LitSet::iterator it = removed->begin(); it != removed->end(); ++it) { - removedDfs(*it, removed, removeStack, inClause, seen); + removedDfs(*it, removed, removeStack, inClause, seen); } - + for (int i = removeStack.size()-1; i >= 0; --i) { Lit lit = removeStack[i]; CRef reason_ref = d_solver->reason(var(lit)); - ClauseId reason_id; + ClauseId reason_id; if (reason_ref == CRef_Undef) { Assert(isUnit(~lit)); - reason_id = getUnitId(~lit); + reason_id = getUnitId(~lit); } else { reason_id = registerClause(reason_ref); } res->addStep(lit, reason_id, !sign(lit)); } - removed->clear(); + removed->clear(); } void SatProof::registerResolution(ClauseId id, ResChain* res) { Assert(res != NULL); removeRedundantFromRes(res, id); - Assert(res->redundantRemoved()); + Assert(res->redundantRemoved()); d_resChains[id] = res; - printRes(id); - if (d_checkRes) { + if(Debug.isOn("proof:sat")) { + printRes(id); + } + if(d_checkRes) { Assert(checkResolution(id)); } } @@ -468,48 +480,46 @@ void SatProof::registerResolution(ClauseId id, ResChain* res) { /// recording resolutions void SatProof::startResChain(::Minisat::CRef start) { - ClauseId id = getClauseId(start); + ClauseId id = getClauseId(start); ResChain* res = new ResChain(id); - d_resStack.push_back(res); + d_resStack.push_back(res); } void SatProof::addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign) { ClauseId id = registerClause(clause); ResChain* res = d_resStack.back(); - res->addStep(lit, id, sign); + res->addStep(lit, id, sign); } void SatProof::endResChain(CRef clause) { Assert(d_resStack.size() > 0); - ClauseId id = registerClause(clause); + ClauseId id = registerClause(clause); ResChain* res = d_resStack.back(); registerResolution(id, res); - d_resStack.pop_back(); + d_resStack.pop_back(); } void SatProof::endResChain(::Minisat::Lit lit) { Assert(d_resStack.size() > 0); - ClauseId id = registerUnitClause(lit); + ClauseId id = registerUnitClause(lit); ResChain* res = d_resStack.back(); - - registerResolution(id, res); - d_resStack.pop_back(); + d_resStack.pop_back(); } void SatProof::storeLitRedundant(::Minisat::Lit lit) { Assert(d_resStack.size() > 0); ResChain* res = d_resStack.back(); - res->addRedundantLit(lit); + res->addRedundantLit(lit); } -/// constructing resolutions +/// constructing resolutions void SatProof::resolveOutUnit(::Minisat::Lit lit) { ClauseId id = resolveUnit(~lit); ResChain* res = d_resStack.back(); - res->addStep(lit, id, !sign(lit)); + res->addStep(lit, id, !sign(lit)); } void SatProof::storeUnitResolution(::Minisat::Lit lit) { @@ -520,28 +530,30 @@ ClauseId SatProof::resolveUnit(::Minisat::Lit lit) { // first check if we already have a resolution for lit if(isUnit(lit)) { ClauseId id = getClauseId(lit); - if(hasResolution(id) || isInputClause(id)) { - return id; - } - Assert (false); + Assert(hasResolution(id) || isInputClause(id) || isLemmaClause(id)); + return id; } CRef reason_ref = d_solver->reason(var(lit)); - Assert (reason_ref != CRef_Undef); - - ClauseId reason_id = registerClause(reason_ref); - - ResChain* res = new ResChain(reason_id); - Clause& reason = d_solver->ca[reason_ref]; - for (int i = 0; i < reason.size(); i++) { - Lit l = reason[i]; - if(lit != l) { + Assert(reason_ref != CRef_Undef); + + ClauseId reason_id = registerClause(reason_ref); + + ResChain* res = new ResChain(reason_id); + // Here, the call to resolveUnit() can reallocate memory in the + // clause allocator. So reload reason ptr each time. + Clause* reason = &getClause(reason_ref); + for (int i = 0; + i < reason->size(); + i++, reason = &getClause(reason_ref)) { + Lit l = (*reason)[i]; + if(lit != l) { ClauseId res_id = resolveUnit(~l); res->addStep(l, res_id, !sign(l)); } } - ClauseId unit_id = registerUnitClause(lit); + ClauseId unit_id = registerUnitClause(lit); registerResolution(unit_id, res); - return unit_id; + return unit_id; } void SatProof::toStream(std::ostream& out) { @@ -549,50 +561,62 @@ void SatProof::toStream(std::ostream& out) { Unimplemented("native proof printing not supported yet"); } -void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit) { - Assert (!d_storedUnitConflict); - d_unitConflictId = registerUnitClause(conflict_lit); +void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind) { + Assert(!d_storedUnitConflict); + d_unitConflictId = registerUnitClause(conflict_lit, kind); d_storedUnitConflict = true; - Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n"; + Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n"; } void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { Assert(d_resStack.size() == 0); - Assert (conflict_ref != ::Minisat::CRef_Undef); - ClauseId conflict_id; + Assert(conflict_ref != ::Minisat::CRef_Undef); + ClauseId conflict_id; if (conflict_ref == ::Minisat::CRef_Lazy) { - Assert (d_storedUnitConflict); - conflict_id = d_unitConflictId; + Assert(d_storedUnitConflict); + conflict_id = d_unitConflictId; + + ResChain* res = new ResChain(conflict_id); + Lit lit = d_idUnit[conflict_id]; + ClauseId res_id = resolveUnit(~lit); + res->addStep(lit, res_id, !sign(lit)); + + registerResolution(d_emptyClauseId, res); + + return; } else { - Assert (!d_storedUnitConflict); + Assert(!d_storedUnitConflict); conflict_id = registerClause(conflict_ref); //FIXME } - Debug("proof:sat") << "proof::finalizeProof Final Conflict "; - print(conflict_id); - + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof::finalizeProof Final Conflict "; + print(conflict_id); + } + ResChain* res = new ResChain(conflict_id); - Clause& conflict = d_solver->ca[conflict_ref] ; - for (int i = 0; i < conflict.size(); ++i) { - Lit lit = conflict[i]; + // Here, the call to resolveUnit() can reallocate memory in the + // clause allocator. So reload conflict ptr each time. + Clause* conflict = &getClause(conflict_ref); + for (int i = 0; + i < conflict->size(); + ++i, conflict = &getClause(conflict_ref)) { + Lit lit = (*conflict)[i]; ClauseId res_id = resolveUnit(~lit); - res->addStep(lit, res_id, !sign(lit)); + res->addStep(lit, res_id, !sign(lit)); } registerResolution(d_emptyClauseId, res); - // // FIXME: massive hack - // Proof* proof = ProofManager::getProof(); - // proof->toStream(std::cout); } /// CRef manager void SatProof::updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref) { if (d_clauseId.find(oldref) == d_clauseId.end()) { - return; + return; } ClauseId id = getClauseId(oldref); - Assert (d_temp_clauseId.find(newref) == d_temp_clauseId.end()); - Assert (d_temp_idClause.find(id) == d_temp_idClause.end()); + Assert(d_temp_clauseId.find(newref) == d_temp_clauseId.end()); + Assert(d_temp_idClause.find(id) == d_temp_idClause.end()); d_temp_clauseId[newref] = id; d_temp_idClause[id] = newref; } @@ -602,39 +626,39 @@ void SatProof::finishUpdateCRef() { d_temp_clauseId.clear(); d_idClause.swap(d_temp_idClause); - d_temp_idClause.clear(); + d_temp_idClause.clear(); } void SatProof::markDeleted(CRef clause) { if (d_clauseId.find(clause) != d_clauseId.end()) { ClauseId id = getClauseId(clause); - Assert (d_deleted.find(id) == d_deleted.end()); + Assert(d_deleted.find(id) == d_deleted.end()); d_deleted.insert(id); if (isLemmaClause(id)) { const Clause& minisat_cl = getClause(clause); - SatClause* sat_cl = new SatClause(); - MinisatSatSolver::toSatClause(minisat_cl, *sat_cl); - d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl)); + SatClause* sat_cl = new SatClause(); + MinisatSatSolver::toSatClause(minisat_cl, *sat_cl); + d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl)); } } } void SatProof::constructProof() { - collectClauses(d_emptyClauseId); + collectClauses(d_emptyClauseId); } std::string SatProof::clauseName(ClauseId id) { ostringstream os; if (isInputClause(id)) { - os << ProofManager::getInputClauseName(id); - return os.str(); - } else + os << ProofManager::getInputClauseName(id); + return os.str(); + } else if (isLemmaClause(id)) { - os << ProofManager::getLemmaClauseName(id); - return os.str(); + os << ProofManager::getLemmaClauseName(id); + return os.str(); }else { os << ProofManager::getLearntClauseName(id); - return os.str(); + return os.str(); } } @@ -643,58 +667,56 @@ void SatProof::addToProofManager(ClauseId id, ClauseKind kind) { Minisat::Lit lit = getUnit(id); prop::SatLiteral sat_lit = MinisatSatSolver::toSatLiteral(lit); prop::SatClause* clause = new SatClause(); - clause->push_back(sat_lit); - ProofManager::currentPM()->addClause(id, clause, kind); - return; + clause->push_back(sat_lit); + ProofManager::currentPM()->addClause(id, clause, kind); + return; } - + if (isDeleted(id)) { - Assert (kind == THEORY_LEMMA); + Assert(kind == THEORY_LEMMA); SatClause* clause = d_deletedTheoryLemmas.find(id)->second; - ProofManager::currentPM()->addClause(id, clause, kind); - return; + ProofManager::currentPM()->addClause(id, clause, kind); + return; } - + CRef ref = getClauseRef(id); const Clause& minisat_cl = getClause(ref); SatClause* clause = new SatClause(); - MinisatSatSolver::toSatClause(minisat_cl, *clause); - ProofManager::currentPM()->addClause(id, clause, kind); + MinisatSatSolver::toSatClause(minisat_cl, *clause); + ProofManager::currentPM()->addClause(id, clause, kind); } void SatProof::collectClauses(ClauseId id) { if (d_seenLearnt.find(id) != d_seenLearnt.end()) { - return; + return; } if (d_seenInput.find(id) != d_seenInput.end()) { - return; + return; } if (d_seenLemmas.find(id) != d_seenLemmas.end()) { - return; + return; } if (isInputClause(id)) { - addToProofManager(id, INPUT); + addToProofManager(id, INPUT); d_seenInput.insert(id); - return; - } - else if (isLemmaClause(id)) { - addToProofManager(id, THEORY_LEMMA); + return; + } else if (isLemmaClause(id)) { + addToProofManager(id, THEORY_LEMMA); d_seenLemmas.insert(id); - return; - } - else { - d_seenLearnt.insert(id); + return; + } else { + d_seenLearnt.insert(id); } - Assert (d_resChains.find(id) != d_resChains.end()); + Assert(d_resChains.find(id) != d_resChains.end()); ResChain* res = d_resChains[id]; ClauseId start = res->getStart(); collectClauses(start); - ResSteps steps = res->getSteps(); - for(unsigned i = 0; i < steps.size(); i++) { - collectClauses(steps[i].id); + ResSteps steps = res->getSteps(); + for(size_t i = 0; i < steps.size(); i++) { + collectClauses(steps[i].id); } } @@ -703,29 +725,29 @@ void SatProof::collectClauses(ClauseId id) { void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) { out << "(satlem_simplify _ _ _ "; - ResChain* res = d_resChains[id]; + ResChain* res = d_resChains[id]; ResSteps& steps = res->getSteps(); - + for (int i = steps.size()-1; i >= 0; i--) { out << "("; out << (steps[i].sign? "R" : "Q") << " _ _ "; - + } - + ClauseId start_id = res->getStart(); // WHY DID WE NEED THIS? // if(isInputClause(start_id)) { - // d_seenInput.insert(start_id); + // d_seenInput.insert(start_id); // } out << clauseName(start_id) << " "; - + for(unsigned i = 0; i < steps.size(); i++) { - out << clauseName(steps[i].id) << " "<<ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")"; + out << clauseName(steps[i].id) << " "<<ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")"; } - + if (id == d_emptyClauseId) { out <<"(\\empty empty)"; - return; + return; } out << "(\\" << clauseName(id) << "\n"; // bind to lemma name diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index a4178f518..477eeeb99 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -9,7 +9,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Resolution proof + ** \brief Resolution proof ** ** Resolution proof **/ @@ -43,11 +43,11 @@ namespace std { namespace CVC4 { -/** +/** * Helper debugging functions */ void printDebug(::Minisat::Lit l); -void printDebug(::Minisat::Clause& c); +void printDebug(::Minisat::Clause& c); struct ResStep { ::Minisat::Lit lit; @@ -60,8 +60,8 @@ struct ResStep { {} };/* struct ResStep */ -typedef std::vector< ResStep > ResSteps; -typedef std::set < ::Minisat::Lit> LitSet; +typedef std::vector< ResStep > ResSteps; +typedef std::set < ::Minisat::Lit> LitSet; class ResChain { private: @@ -72,7 +72,7 @@ public: ResChain(ClauseId start); void addStep(::Minisat::Lit, ClauseId, bool); bool redundantRemoved() { return (d_redundantLits == NULL || d_redundantLits->empty()); } - void addRedundantLit(::Minisat::Lit lit); + void addRedundantLit(::Minisat::Lit lit); ~ResChain(); // accessor methods ClauseId getStart() { return d_start; } @@ -83,16 +83,16 @@ public: typedef std::hash_map < ClauseId, ::Minisat::CRef > IdCRefMap; typedef std::hash_map < ::Minisat::CRef, ClauseId > ClauseIdMap; typedef std::hash_map < ClauseId, ::Minisat::Lit> IdUnitMap; -typedef std::hash_map < int, ClauseId> UnitIdMap; //FIXME -typedef std::hash_map < ClauseId, ResChain*> IdResMap; +typedef std::hash_map < int, ClauseId> UnitIdMap; //FIXME +typedef std::hash_map < ClauseId, ResChain*> IdResMap; typedef std::hash_set < ClauseId > IdHashSet; -typedef std::vector < ResChain* > ResStack; -typedef std::hash_map <ClauseId, prop::SatClause* > IdToSatClause; -typedef std::set < ClauseId > IdSet; -typedef std::vector < ::Minisat::Lit > LitVector; +typedef std::vector < ResChain* > ResStack; +typedef std::hash_map <ClauseId, prop::SatClause* > IdToSatClause; +typedef std::set < ClauseId > IdSet; +typedef std::vector < ::Minisat::Lit > LitVector; typedef __gnu_cxx::hash_map<ClauseId, ::Minisat::Clause& > IdToMinisatClause; -class SatProof; +class SatProof; class ProofProxy : public ProofProxyAbstract { private: @@ -103,31 +103,31 @@ public: };/* class ProofProxy */ -class CnfProof; +class CnfProof; class SatProof { protected: ::Minisat::Solver* d_solver; - // clauses + // clauses IdCRefMap d_idClause; ClauseIdMap d_clauseId; IdUnitMap d_idUnit; UnitIdMap d_unitId; IdHashSet d_deleted; - IdToSatClause d_deletedTheoryLemmas; - IdHashSet d_inputClauses; - IdHashSet d_lemmaClauses; - // resolutions + IdToSatClause d_deletedTheoryLemmas; + IdHashSet d_inputClauses; + IdHashSet d_lemmaClauses; + // resolutions IdResMap d_resChains; - ResStack d_resStack; + ResStack d_resStack; bool d_checkRes; - - static ClauseId d_idCounter; + + static ClauseId d_idCounter; const ClauseId d_emptyClauseId; const ClauseId d_nullId; - // proxy class to break circular dependencies + // proxy class to break circular dependencies ProofProxy* d_proxy; - + // temporary map for updating CRefs ClauseIdMap d_temp_clauseId; IdCRefMap d_temp_idClause; @@ -135,43 +135,43 @@ protected: // unit conflict ClauseId d_unitConflictId; bool d_storedUnitConflict; -public: +public: SatProof(::Minisat::Solver* solver, bool checkRes = false); virtual ~SatProof() {} protected: - void print(ClauseId id); + void print(ClauseId id); void printRes(ClauseId id); - void printRes(ResChain* res); - + void printRes(ResChain* res); + bool isInputClause(ClauseId id); bool isLemmaClause(ClauseId id); bool isUnit(ClauseId id); - bool isUnit(::Minisat::Lit lit); - bool hasResolution(ClauseId id); - void createLitSet(ClauseId id, LitSet& set); + bool isUnit(::Minisat::Lit lit); + bool hasResolution(ClauseId id); + void createLitSet(ClauseId id, LitSet& set); void registerResolution(ClauseId id, ResChain* res); - + ClauseId getClauseId(::Minisat::CRef clause); - ClauseId getClauseId(::Minisat::Lit lit); + ClauseId getClauseId(::Minisat::Lit lit); ::Minisat::CRef getClauseRef(ClauseId id); ::Minisat::Lit getUnit(ClauseId id); - ClauseId getUnitId(::Minisat::Lit lit); + ClauseId getUnitId(::Minisat::Lit lit); ::Minisat::Clause& getClause(::Minisat::CRef ref); virtual void toStream(std::ostream& out); bool checkResolution(ClauseId id); - /** + /** * Constructs a resolution tree that proves lit * and returns the ClauseId for the unit clause lit * @param lit the literal we are proving - * - * @return + * + * @return */ ClauseId resolveUnit(::Minisat::Lit lit); - /** + /** * Does a depth first search on removed literals and adds the literals - * to be removed in the proper order to the stack. - * + * to be removed in the proper order to the stack. + * * @param lit the literal we are recursing on * @param removedSet the previously computed set of redundant literals * @param removeStack the stack of literals in reverse order of resolution @@ -181,71 +181,71 @@ protected: public: void startResChain(::Minisat::CRef start); void addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign); - /** + /** * Pops the current resolution of the stack and stores it * in the resolution map. Also registers the 'clause' parameter - * @param clause the clause the resolution is proving + * @param clause the clause the resolution is proving */ void endResChain(::Minisat::CRef clause); void endResChain(::Minisat::Lit lit); - /** - * Stores in the current derivation the redundant literals that were - * eliminated from the conflict clause during conflict clause minimization. - * @param lit the eliminated literal + /** + * Stores in the current derivation the redundant literals that were + * eliminated from the conflict clause during conflict clause minimization. + * @param lit the eliminated literal */ void storeLitRedundant(::Minisat::Lit lit); /// update the CRef Id maps when Minisat does memory reallocation x void updateCRef(::Minisat::CRef old_ref, ::Minisat::CRef new_ref); void finishUpdateCRef(); - - /** + + /** * Constructs the empty clause resolution from the final conflict - * - * @param conflict + * + * @param conflict */ void finalizeProof(::Minisat::CRef conflict); - /// clause registration methods + /// clause registration methods ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind = LEARNT); ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind = LEARNT); - void storeUnitConflict(::Minisat::Lit lit); - - /** + void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind = LEARNT); + + /** * Marks the deleted clauses as deleted. Note we may still use them in the final - * resolution. - * @param clause + * resolution. + * @param clause */ void markDeleted(::Minisat::CRef clause); bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); } - /** + /** * Constructs the resolution of ~q and resolves it with the current * resolution thus eliminating q from the current clause * @param q the literal to be resolved out */ void resolveOutUnit(::Minisat::Lit q); - /** + /** * Constructs the resolution of the literal lit. Called when a clause - * containing lit becomes satisfied and is removed. - * @param lit + * containing lit becomes satisfied and is removed. + * @param lit */ - void storeUnitResolution(::Minisat::Lit lit); - + void storeUnitResolution(::Minisat::Lit lit); + ProofProxy* getProxy() {return d_proxy; } /** - Constructs the SAT proof identifying the needed lemmas + Constructs the SAT proof identifying the needed lemmas */ void constructProof(); - + protected: IdSet d_seenLearnt; IdHashSet d_seenInput; - IdHashSet d_seenLemmas; - + IdHashSet d_seenLemmas; + inline std::string varName(::Minisat::Lit lit); - inline std::string clauseName(ClauseId id); + inline std::string clauseName(ClauseId id); void collectClauses(ClauseId id); void addToProofManager(ClauseId id, ClauseKind kind); diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 696bd8309..4ed00aaaa 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -26,9 +26,10 @@ TheoryProof::TheoryProof() {} void TheoryProof::addDeclaration(Expr term) { - if (d_declarationCache.count(term)) + if (d_declarationCache.count(term)) { return; - + } + Type type = term.getType(); if (type.isSort()) d_sortDeclarations.insert(type); @@ -36,32 +37,14 @@ void TheoryProof::addDeclaration(Expr term) { Expr function = term.getOperator(); d_termDeclarations.insert(function); } else if (term.isVariable()) { - Assert (type.isSort()); + //Assert (type.isSort() || type.isBoolean()); d_termDeclarations.insert(term); } // recursively declare all other terms for (unsigned i = 0; i < term.getNumChildren(); ++i) { - addDeclaration(term[i]); - } - d_declarationCache.insert(term); -} - -void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) { - if (term.isVariable()) { - os << term; - return; - } - - Assert (term.getKind() == kind::APPLY_UF); - Expr func = term.getOperator(); - for (unsigned i = 0; i < term.getNumChildren(); ++i) { - os<< "(apply _ _ "; - } - os << func << " "; - for (unsigned i = 0; i < term.getNumChildren(); ++i) { - printTerm(term[i], os); - os << ")"; + addDeclaration(term[i]); } + d_declarationCache.insert(term); } std::string toLFSCKind(Kind kind) { @@ -70,71 +53,138 @@ std::string toLFSCKind(Kind kind) { case kind::AND: return "and"; case kind::XOR: return "xor"; case kind::EQUAL: return "="; + case kind::IFF: return "iff"; case kind::IMPLIES: return "impl"; case kind::NOT: return "not"; default: - Unreachable(); + Unreachable(); } } -void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) { - // should make this more general and overall sane - Assert (atom.getType().isBoolean() && "Only printing booleans." ); - Kind kind = atom.getKind(); - // this is the only predicate we have - if (kind == kind::EQUAL) { - os << "("; - os <<"= "; - os << atom[0].getType() <<" "; - printTerm(atom[0], os); - os <<" "; - printTerm(atom[1], os); - os <<")"; - } else if ( kind == kind::DISTINCT) { - os <<"(not (= "; - os << atom[0].getType() <<" "; - printTerm(atom[0], os); - os <<" "; - printTerm(atom[1], os); - os <<"))"; - } else if ( kind == kind::OR || - kind == kind::AND || - kind == kind::XOR || - kind == kind::IMPLIES || - kind == kind::NOT) { - // print the boolean operators +void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) { + if (term.isVariable()) { + if(term.getType().isBoolean()) { + os << "(p_app " << term << ")"; + } else { + os << term; + } + return; + } + + switch(Kind k = term.getKind()) { + case kind::APPLY_UF: { + if(term.getType().isBoolean()) { + os << "(p_app "; + } + Expr func = term.getOperator(); + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + os << "(apply _ _ "; + } + os << func << " "; + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + printTerm(term[i], os); + os << ")"; + } + if(term.getType().isBoolean()) { + os << ")"; + } + return; + } + + case kind::ITE: + os << (term.getType().isBoolean() ? "(ifte " : "(ite _ "); + printTerm(term[0], os); + os << " "; + printTerm(term[1], os); + os << " "; + printTerm(term[2], os); + os << ")"; + return; + + case kind::EQUAL: os << "("; - os << toLFSCKind(kind); - if (atom.getNumChildren() > 2) { + os << "= "; + os << term[0].getType() << " "; + printTerm(term[0], os); + os << " "; + printTerm(term[1], os); + os << ")"; + return; + + case kind::DISTINCT: + os << "(not (= "; + os << term[0].getType() << " "; + printTerm(term[0], os); + os << " "; + printTerm(term[1], os); + os << "))"; + return; + + case kind::OR: + case kind::AND: + case kind::XOR: + case kind::IFF: + case kind::IMPLIES: + case kind::NOT: + // print the Boolean operators + os << "(" << toLFSCKind(k); + if(term.getNumChildren() > 2) { + // LFSC doesn't allow declarations with variable numbers of + // arguments, so we have to flatten these N-ary versions. std::ostringstream paren; os << " "; - for (unsigned i =0; i < atom.getNumChildren(); ++i) { - printFormula(atom[i], os); + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + printTerm(term[i], os); os << " "; - if (i < atom.getNumChildren() - 2) { - os << "("<< toLFSCKind(kind) << " "; - paren << ")"; + if(i < term.getNumChildren() - 2) { + os << "(" << toLFSCKind(k) << " "; + paren << ")"; } } - os << paren.str() <<")"; + os << paren.str() << ")"; } else { - // this is for binary and unary operators - for (unsigned i = 0; i < atom.getNumChildren(); ++i) { - os <<" "; - printFormula(atom[i], os); + // this is for binary and unary operators + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + os << " "; + printTerm(term[i], os); + } + os << ")"; + } + return; + + case kind::CONST_BOOLEAN: + os << (term.getConst<bool>() ? "true" : "false"); + return; + + case kind::CHAIN: { + // LFSC doesn't allow declarations with variable numbers of + // arguments, so we have to flatten chained operators, like =. + Kind op = term.getOperator().getConst<Chain>().getOperator(); + size_t n = term.getNumChildren(); + std::ostringstream paren; + for(size_t i = 1; i < n; ++i) { + if(i + 1 < n) { + os << "(" << toLFSCKind(kind::AND) << " "; + paren << ")"; + } + os << "(" << toLFSCKind(op) << " "; + printTerm(term[i - 1], os); + os << " "; + printTerm(term[i], os); + os << ")"; + if(i + 1 < n) { + os << " "; } - os <<")"; } - } else if (kind == kind::CONST_BOOLEAN) { - if (atom.getConst<bool>()) - os << "true"; - else - os << "false"; + os << paren.str(); + return; } - else { - std::cout << kind << "\n"; - Assert (false && "Unsupported kind"); + + default: + Unhandled(k); } + + Unreachable(); } void LFSCTheoryProof::printAssertions(std::ostream& os, std::ostream& paren) { @@ -142,56 +192,57 @@ void LFSCTheoryProof::printAssertions(std::ostream& os, std::ostream& paren) { ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); - // collect declarations first + // collect declarations first for(; it != end; ++it) { - addDeclaration(*it); + addDeclaration(*it); } printDeclarations(os, paren); it = ProofManager::currentPM()->begin_assertions(); for (; it != end; ++it) { os << "(% A" << counter++ << " (th_holds "; - printFormula(*it, os); + printTerm(*it, os); os << ")\n"; - paren <<")"; + paren << ")"; } } void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) { // declaring the sorts for (SortSet::const_iterator it = d_sortDeclarations.begin(); it != d_sortDeclarations.end(); ++it) { - os << "(% " << *it << " sort \n"; - paren << ")"; + os << "(% " << *it << " sort\n"; + paren << ")"; } // declaring the terms for (ExprSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) { Expr term = *it; - os << "(% " << term << " (term "; - paren <<")"; + os << "(% " << term << " "; + os << "(term "; Type type = term.getType(); if (type.isFunction()) { - std::ostringstream fparen; + std::ostringstream fparen; FunctionType ftype = (FunctionType)type; std::vector<Type> args = ftype.getArgTypes(); - args.push_back(ftype.getRangeType()); - os << "(arrow "; + args.push_back(ftype.getRangeType()); + os << "(arrow"; for (unsigned i = 0; i < args.size(); i++) { Type arg_type = args[i]; - Assert (arg_type.isSort()); - os << arg_type << " "; + //Assert (arg_type.isSort() || arg_type.isBoolean()); + os << " " << arg_type; if (i < args.size() - 2) { - os << "(arrow "; - fparen <<")"; + os << " (arrow"; + fparen << ")"; } } - os << fparen.str() << "))\n"; + os << fparen.str() << "))\n"; } else { Assert (term.isVariable()); - Assert (type.isSort()); + //Assert (type.isSort() || type.isBoolean()); os << type << ")\n"; } + paren << ")"; } -} +} diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 457023a59..739299b7d 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -13,7 +13,7 @@ ** ** A manager for UfProofs. ** - ** + ** **/ @@ -24,33 +24,32 @@ #include "util/proof.h" #include "expr/expr.h" #include <ext/hash_set> -#include <iostream> +#include <iostream> namespace CVC4 { - typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet; - typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; + typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet; + typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; class TheoryProof { protected: ExprSet d_termDeclarations; - SortSet d_sortDeclarations; + SortSet d_sortDeclarations; ExprSet d_declarationCache; - - void addDeclaration(Expr atom); + public: TheoryProof(); virtual ~TheoryProof() {} virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0; + void addDeclaration(Expr atom); }; class LFSCTheoryProof: public TheoryProof { - static void printTerm(Expr term, std::ostream& os); void printDeclarations(std::ostream& os, std::ostream& paren); public: - static void printFormula(Expr atom, std::ostream& os); + static void printTerm(Expr term, std::ostream& os); virtual void printAssertions(std::ostream& os, std::ostream& paren); - }; + }; } /* CVC4 namespace */ #endif /* __CVC4__THEORY_PROOF_H */ diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 16fa3ba60..610023b70 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -263,7 +263,7 @@ CRef Solver::reason(Var x) { // Construct the reason CRef real_reason = ca.alloc(explLevel, explanation, true); - PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); ); + PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); ); vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x)); clauses_removable.push(real_reason); attachClause(real_reason); @@ -324,7 +324,18 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) } else { // If all false, we're in conflict if (ps.size() == falseLiteralsCount) { + if(PROOF_ON()) { + // Take care of false units here; otherwise, we need to + // construct the clause below to give to the proof manager + // as the final conflict. + if(falseLiteralsCount == 1) { + PROOF( ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT); ) + PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); ) + return ok = false; + } + } else { return ok = false; + } } CRef cr = CRef_Undef; @@ -339,7 +350,13 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) clauses_persistent.push(cr); attachClause(cr); - PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT); ) + if(PROOF_ON()) { + PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT); ) + if(ps.size() == falseLiteralsCount) { + PROOF( ProofManager::getSatProof()->finalizeProof(cr); ) + return ok = false; + } + } } // Check if it propagates @@ -347,8 +364,17 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) if(assigns[var(ps[0])] == l_Undef) { assert(assigns[var(ps[0])] != l_False); uncheckedEnqueue(ps[0], cr); - PROOF( if (ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); } ) - return ok = (propagate(CHECK_WITHOUT_THEORY) == CRef_Undef); + PROOF( if(ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); } ); + CRef confl = propagate(CHECK_WITHOUT_THEORY); + if(! (ok = (confl == CRef_Undef)) ) { + if(ca[confl].size() == 1) { + PROOF( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT); ); + PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); ) + } else { + PROOF( ProofManager::getSatProof()->finalizeProof(confl); ); + } + } + return ok; } else return ok; } } @@ -370,7 +396,7 @@ void Solver::attachClause(CRef cr) { void Solver::detachClause(CRef cr, bool strict) { const Clause& c = ca[cr]; - PROOF( ProofManager::getSatProof()->markDeleted(cr); ) + PROOF( ProofManager::getSatProof()->markDeleted(cr); ); Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl; assert(c.size() > 1); @@ -1580,7 +1606,7 @@ CRef Solver::updateLemmas() { vec<Lit>& lemma = lemmas[i]; // If it's an empty lemma, we have a conflict at zero level if (lemma.size() == 0) { - Assert (! PROOF_ON()); + Assert (! PROOF_ON()); conflict = CRef_Lazy; backtrackLevel = 0; Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl; @@ -1630,13 +1656,15 @@ CRef Solver::updateLemmas() { } lemma_ref = ca.alloc(clauseLevel, lemma, removable); - PROOF (ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); ); + PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); ); if (removable) { clauses_removable.push(lemma_ref); } else { clauses_persistent.push(lemma_ref); } attachClause(lemma_ref); + } else { + PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); ); } // If the lemma is propagating enqueue its literal (or set the conflict) @@ -1650,7 +1678,7 @@ CRef Solver::updateLemmas() { } else { Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl; conflict = CRef_Lazy; - PROOF(ProofManager::getSatProof()->storeUnitConflict(lemma[0]);); + PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0]); ); } } else { Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl; diff --git a/src/smt/options b/src/smt/options index 69b5102de..b76822caf 100644 --- a/src/smt/options +++ b/src/smt/options @@ -22,14 +22,16 @@ option expandDefinitions expand-definitions bool :default false always expand symbol definitions in output common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h" support the get-value and get-model commands -option checkProofs check-proofs --check-proofs bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" - after UNSAT/VALID, machine-check the generated proof -option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" +option checkModels check-models --check-models bool :link --produce-models --interactive :link-smt produce-models :link-smt interactive-mode :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions -option dumpModels --dump-models bool :default false +option dumpModels --dump-models bool :default false :link --produce-models output models after every SAT/INVALID/UNKNOWN response option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on proof generation +option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + after UNSAT/VALID, machine-check the generated proof +option dumpProofs --dump-proofs bool :default false :link --proof + output proofs after every UNSAT/VALID response # this is just a placeholder for later; it doesn't show up in command-line options listings undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on unsat core generation (NOT YET SUPPORTED) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1f83bb547..ec37eaf26 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -46,8 +46,10 @@ #include "theory/theory_engine.h" #include "theory/bv/theory_bv_rewriter.h" #include "proof/proof_manager.h" +#include "main/options.h" #include "util/proof.h" #include "proof/proof.h" +#include "proof/proof_manager.h" #include "util/boolean_simplification.h" #include "util/node_visitor.h" #include "util/configuration.h" @@ -157,6 +159,8 @@ struct SmtEngineStatistics { IntStat d_numAssertionsPost; /** time spent in checkModel() */ TimerStat d_checkModelTime; + /** time spent in checkProof() */ + TimerStat d_checkProofTime; /** time spent in PropEngine::checkSat() */ TimerStat d_solveTime; /** time spent in pushing/popping */ @@ -183,11 +187,11 @@ struct SmtEngineStatistics { d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0), d_checkModelTime("smt::SmtEngine::checkModelTime"), + d_checkProofTime("smt::SmtEngine::checkProofTime"), d_solveTime("smt::SmtEngine::solveTime"), d_pushPopTime("smt::SmtEngine::pushPopTime"), d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"), d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0) - { StatisticsRegistry::registerStat(&d_definitionExpansionTime); @@ -667,6 +671,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_decisionEngine(NULL), d_theoryEngine(NULL), d_propEngine(NULL), + d_proofManager(NULL), d_definedFunctions(NULL), d_assertionList(NULL), d_assignments(NULL), @@ -696,6 +701,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_statisticsRegistry = new StatisticsRegistry(); d_stats = new SmtEngineStatistics(); + PROOF( d_proofManager = new ProofManager(); ); + // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic)); @@ -763,6 +770,7 @@ void SmtEngine::finishInit() { if(options::cumulativeMillisecondLimit() != 0) { setTimeLimit(options::cumulativeMillisecondLimit(), true); } + PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); } @@ -777,16 +785,11 @@ void SmtEngine::finalOptionsAreSet() { } if(options::checkModels()) { - if(! options::produceModels()) { - Notice() << "SmtEngine: turning on produce-models to support check-model" << endl; - setOption("produce-models", SExpr("true")); - } if(! options::interactive()) { - Notice() << "SmtEngine: turning on interactive-mode to support check-model" << endl; + Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl; setOption("interactive-mode", SExpr("true")); } } - if(options::produceAssignments() && !options::produceModels()) { Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl; setOption("produce-models", SExpr("true")); @@ -3291,9 +3294,6 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc finalOptionsAreSet(); doPendingPops(); - - PROOF( ProofManager::currentPM()->addAssertion(ex); ); - Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl; if(d_queryMade && !options::incrementalSolving()) { @@ -3308,6 +3308,8 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); // Ensure expr is type-checked at this point. ensureBoolean(e); + // Give it to proof manager + PROOF( ProofManager::currentPM()->addAssertion(e); ); } // check to see if a postsolve() is pending @@ -3361,6 +3363,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc // Check that UNSAT results generate a proof correctly. if(options::checkProofs()) { if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime); checkProof(); } } @@ -3384,9 +3387,10 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept // Substitute out any abstract values in ex Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); - // Ensure that the expression is type-checked at this point, and Boolean ensureBoolean(e); + // Give it to proof manager + PROOF( ProofManager::currentPM()->addAssertion(e.notExpr()); ); // check to see if a postsolve() is pending if(d_needPostsolve) { @@ -3437,6 +3441,7 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept // Check that UNSAT results generate a proof correctly. if(options::checkProofs()) { if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime); checkProof(); } } @@ -3449,7 +3454,9 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); - PROOF( ProofManager::currentPM()->addAssertion(ex);); + + PROOF( ProofManager::currentPM()->addAssertion(ex); ); + Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl; // Substitute out any abstract values in ex diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 0781ac1c0..8e400468c 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -56,6 +56,8 @@ class SmtEngine; class DecisionEngine; class TheoryEngine; +class ProofManager; + class Model; class StatisticsRegistry; @@ -83,6 +85,7 @@ namespace smt { class BooleanTermConverter; void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); + ProofManager* currentProofManager(); struct CommandCleanup; typedef context::CDList<Command*, CommandCleanup> CommandList; @@ -135,8 +138,11 @@ class CVC4_PUBLIC SmtEngine { TheoryEngine* d_theoryEngine; /** The propositional engine */ prop::PropEngine* d_propEngine; + /** The proof manager */ + ProofManager* d_proofManager; /** An index of our defined functions */ DefinedFunctionMap* d_definedFunctions; + /** * The assertion list (before any conversion) for supporting * getAssertions(). Only maintained if in interactive mode. @@ -327,6 +333,7 @@ class CVC4_PUBLIC SmtEngine { friend class ::CVC4::smt::BooleanTermConverter; friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*); friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); + friend ProofManager* ::CVC4::smt::currentProofManager(); // to access d_modelCommands friend class ::CVC4::Model; friend class ::CVC4::theory::TheoryModel; diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index e4de1029b..a731ff024 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -16,16 +16,75 @@ **/ #include "smt/smt_engine.h" +#include "util/statistics_registry.h" #include "check.h" +#include <cstdlib> +#include <cstring> +#include <fstream> +#include <string> +#include <unistd.h> + using namespace CVC4; using namespace std; +namespace CVC4 { + +namespace proof { + extern const char *const plf_signatures; +}/* CVC4::proof namespace */ + +namespace smt { + +class UnlinkProofFile { + string d_filename; +public: + UnlinkProofFile(const char* filename) : d_filename(filename) {} + ~UnlinkProofFile() { unlink(d_filename.c_str()); } +};/* class UnlinkProofFile */ + +}/* CVC4::smt namespace */ + +}/* CVC4 namespace */ + void SmtEngine::checkProof() { #ifdef CVC4_PROOF - //TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime); + Chat() << "generating proof..." << endl; + + Proof* pf = getProof(); + + Chat() << "checking proof..." << endl; + + if(!d_logic.isPure(theory::THEORY_BOOL) && + !d_logic.isPure(theory::THEORY_UF)) { + // no checking for these yet + Notice() << "Notice: no proof-checking for non-UF proofs yet" << endl; + return; + } + + char* pfFile = strdup("/tmp/cvc4_proof.XXXXXX"); + int fd = mkstemp(pfFile); + + // ensure this temp file is removed after + smt::UnlinkProofFile unlinker(pfFile); + + ofstream pfStream(pfFile); + pfStream << proof::plf_signatures << endl; + pf->toStream(pfStream); + pfStream.close(); + args a; + a.show_runs = false; + a.no_tail_calls = false; + a.compile_scc = false; + a.compile_scc_debug = false; + a.run_scc = false; + a.use_nested_app = false; + a.compile_lib = false; + init(); + check_file(pfFile, args()); + close(fd); #else /* CVC4_PROOF */ diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index 21644d3f4..2389181b5 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -22,10 +22,14 @@ #include "util/cvc4_assert.h" #include "expr/node_manager.h" #include "util/output.h" +#include "proof/proof.h" #pragma once namespace CVC4 { + +class ProofManager; + namespace smt { extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current; @@ -35,6 +39,12 @@ inline SmtEngine* currentSmtEngine() { return s_smtEngine_current; } +inline ProofManager* currentProofManager() { + Assert(PROOF_ON()); + Assert(s_smtEngine_current != NULL); + return s_smtEngine_current->d_proofManager; +} + class SmtScope : public NodeManagerScope { /** The old NodeManager, to be restored on destruction. */ SmtEngine* d_oldSmtEngine; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7cf4d7ad9..c598fd01b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -146,6 +146,7 @@ TheoryEngine::TheoryEngine(context::Context* context, StatisticsRegistry::registerStat(&d_combineTheoriesTime); d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); + PROOF (ProofManager::currentPM()->initTheoryProof(); ); d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor()); diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 5c591d39c..d7663e298 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -7,12 +7,12 @@ DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatype end@mk_if@ LOG_COMPILER = @srcdir@/../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index 6897ee3c4..e7810c7c4 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . integers end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am index 3511c6b30..3b6a86bc0 100644 --- a/test/regress/regress0/arith/integers/Makefile.am +++ b/test/regress/regress0/arith/integers/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index 33f05ab40..62877ddf3 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index e151a4846..e45358a8a 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am index ca1fc25d3..31d9c0797 100644 --- a/test/regress/regress0/auflia/Makefile.am +++ b/test/regress/regress0/auflia/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc index cba092e9e..eb0e7ab52 100644 --- a/test/regress/regress0/boolean.cvc +++ b/test/regress/regress0/boolean.cvc @@ -804,4 +804,3 @@ a288 : BOOLEAN = ELSE FALSE ENDIF; QUERY a288; -% PROOF diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index f0bfb2842..5d2a54b11 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . core end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index 888e9d8dc..7c411121a 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 67b97add3..84adb4f84 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/datatypes/empty_tuprec.cvc b/test/regress/regress0/datatypes/empty_tuprec.cvc index 415da3c18..5fe17b412 100644 --- a/test/regress/regress0/datatypes/empty_tuprec.cvc +++ b/test/regress/regress0/datatypes/empty_tuprec.cvc @@ -1,3 +1,5 @@ +% COMMAND-LINE: --no-check-proofs +% OPTION "incremental"; a1, a2 : []; % empty tuples (a unit type) diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am index 0f8ef8e8e..366204191 100644 --- a/test/regress/regress0/decision/Makefile.am +++ b/test/regress/regress0/decision/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index bfbc851ef..2633949c8 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/fmf/PUZ001+1.smt2 b/test/regress/regress0/fmf/PUZ001+1.smt2 index bf156367e..f0e53fc98 100644 --- a/test/regress/regress0/fmf/PUZ001+1.smt2 +++ b/test/regress/regress0/fmf/PUZ001+1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find +; COMMAND-LINE: --finite-model-find --no-check-proofs ; EXPECT: unsat ;%------------------------------------------------------------------------------ ;% File : PUZ001+1 : TPTP v5.4.0. Released v2.0.0. diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc index 5cc4de9be..dfa9b72d5 100644 --- a/test/regress/regress0/hole6.cvc +++ b/test/regress/regress0/hole6.cvc @@ -177,4 +177,3 @@ ASSERT x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37; QUERY FALSE; -% PROOF diff --git a/test/regress/regress0/lemmas/Makefile.am b/test/regress/regress0/lemmas/Makefile.am index 260b3600d..9ede6d4c0 100644 --- a/test/regress/regress0/lemmas/Makefile.am +++ b/test/regress/regress0/lemmas/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am index 141510ea2..1d980997d 100644 --- a/test/regress/regress0/precedence/Makefile.am +++ b/test/regress/regress0/precedence/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am index 73d13e78d..d83df4192 100644 --- a/test/regress/regress0/preprocess/Makefile.am +++ b/test/regress/regress0/preprocess/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index 0a1094238..29ad34255 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = boolean arith . end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/push-pop/arith/Makefile.am b/test/regress/regress0/push-pop/arith/Makefile.am index 6fd183ec3..7838e202d 100644 --- a/test/regress/regress0/push-pop/arith/Makefile.am +++ b/test/regress/regress0/push-pop/arith/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/push-pop/boolean/Makefile.am b/test/regress/regress0/push-pop/boolean/Makefile.am index 0757ebfc2..995312cee 100644 --- a/test/regress/regress0/push-pop/boolean/Makefile.am +++ b/test/regress/regress0/push-pop/boolean/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 0b74d83b7..d0a93a142 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am index d2e748fbf..32f8a72ba 100644 --- a/test/regress/regress0/rewriterules/Makefile.am +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -7,12 +7,12 @@ export CVC4_REGRESSION_ARGS end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index e24cbc565..a5c6ae2f4 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/tptp/Makefile.am b/test/regress/regress0/tptp/Makefile.am index e227e0bba..f8f106362 100644 --- a/test/regress/regress0/tptp/Makefile.am +++ b/test/regress/regress0/tptp/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 19e673fea..98194413d 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am index 2ef7be862..2946d886a 100644 --- a/test/regress/regress0/uflia/Makefile.am +++ b/test/regress/regress0/uflia/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index 63d362bf9..cd39284b8 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am index c9a38d7b1..ecf427fb5 100644 --- a/test/regress/regress0/unconstrained/Makefile.am +++ b/test/regress/regress0/unconstrained/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc index fa9f56f81..0fe647f7b 100644 --- a/test/regress/regress0/wiki.05.cvc +++ b/test/regress/regress0/wiki.05.cvc @@ -2,4 +2,3 @@ a, b, c : BOOLEAN; % EXPECT: valid QUERY a OR (a AND b) <=> a; -% PROOF diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index 674f5c75e..5f292b893 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . arith end@mk_if@ LOG_COMPILER = @srcdir@/../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress1/arith/Makefile.am b/test/regress/regress1/arith/Makefile.am index ca362f479..fff5372c6 100644 --- a/test/regress/regress1/arith/Makefile.am +++ b/test/regress/regress1/arith/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am index e4e5d8d29..9deb1f37b 100644 --- a/test/regress/regress2/Makefile.am +++ b/test/regress/regress2/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am index 213157491..3fb798bcc 100644 --- a/test/regress/regress3/Makefile.am +++ b/test/regress/regress3/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/run_regression b/test/regress/run_regression index 4d23e796b..ef2bb9a35 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -71,10 +71,8 @@ function gettemp { tmpbenchmark= if expr "$benchmark" : '.*\.smt$' &>/dev/null; then - proof_command=PROOFS-NOT-SUPPORTED-IN-SMTLIB-V1 lang=smt1 if test -e "$benchmark.expect"; then - expected_proof=`grep '^% PROOF' "$benchmark.expect" &>/dev/null && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -83,7 +81,6 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then expected_exit_status=0 fi elif grep '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then - expected_proof=`grep '^% PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -97,12 +94,10 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then fi benchmark=$tmpbenchmark elif grep '^ *:status *sat' "$benchmark" &>/dev/null; then - expected_proof= expected_output=sat expected_exit_status=0 command_line= elif grep '^ *:status *unsat' "$benchmark" &>/dev/null; then - expected_proof= expected_output=unsat expected_exit_status=0 command_line= @@ -110,10 +105,8 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then error "cannot determine status of \`$benchmark'" fi elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then - proof_command='(get-proof)' lang=smt2 if test -e "$benchmark.expect"; then - expected_proof=`grep '^[%;] PROOF' "$benchmark.expect" &>/dev/null && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -122,7 +115,6 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then expected_exit_status=0 fi elif grep '^\(%\|;\) \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then - expected_proof=`grep '^[%;] PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=`grep '^[%;] EXPECT: ' "$benchmark" | sed 's,^[%;] EXPECT: ,,'` expected_error=`grep '^[%;] EXPECT-ERROR: ' "$benchmark" | sed 's,^[%;] EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^[%;] EXIT: ' "$benchmark" | perl -pe 's,^[%;] EXIT: ,,;s,\r,,'` @@ -136,12 +128,10 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then fi benchmark=$tmpbenchmark elif grep '^ *( *set-info *:status *sat' "$benchmark" &>/dev/null; then - expected_proof= expected_output=sat expected_exit_status=0 command_line= elif grep '^ *( *set-info *:status *unsat' "$benchmark" &>/dev/null; then - expected_proof=`grep '^; PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=unsat expected_exit_status=0 command_line= @@ -149,9 +139,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then error "cannot determine status of \`$benchmark'" fi elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then - proof_command='DUMP_PROOF;' lang=cvc4 - expected_proof=`grep '^% PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=$(grep '^% EXPECT: ' "$benchmark") expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` if [ -z "$expected_output" -a -z "$expected_error" ]; then @@ -165,10 +153,8 @@ elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then fi command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` elif expr "$benchmark" : '.*\.p$' &>/dev/null; then - proof_command=PROOFS-NOT-SUPPORTED-IN-TPTP; lang=tptp command_line=--finite-model-find - expected_proof=`grep '^% PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=$(grep '^% EXPECT: ' "$benchmark") expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` if [ -z "$expected_output" -a -z "$expected_error" ]; then @@ -213,14 +199,28 @@ if [ -z "$expected_output" ]; then else echo "$expected_output" >"$expoutfile" fi + check_models=false if grep '^sat$' "$expoutfile" &>/dev/null || grep '^invalid$' "$expoutfile" &>/dev/null || grep '^unknown$' "$expoptfile" &>/dev/null; then - if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-models' &>/dev/null && - ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-models' &>/dev/null; then + if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-models\>' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-models\>' &>/dev/null; then # later on, we'll run another test with --check-models on check_models=true fi fi +check_proofs=false +if [ "$proof" = yes ]; then + # proofs not currently supported in incremental mode, turn it off + if grep '^unsat$' "$expoutfile" &>/dev/null || grep '^valid$' "$expoutfile" &>/dev/null &>/dev/null; then + if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-proofs\>' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-proofs\>' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental\>' &>/dev/null && + ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null; then + # later on, we'll run another test with --check-proofs on + check_proofs=true + fi + fi +fi if [ -z "$expected_error" ]; then # in case expected stderr output is empty, make sure we don't differ # by a newline, which we would if we echo "" >"$experrfile" @@ -275,47 +275,16 @@ if [ "$exit_status" != "$expected_exit_status" ]; then exitcode=1 fi -if [ "$proof" = yes -a "$expected_proof" = yes ]; then - gettemp pfbenchmark cvc4_pfbenchmark.$$.XXXXXXXXXX - # remove exit command to add proof command for smt2 benchmarks - if expr "$benchmark" : '.*\.smt2$' &>/dev/null; then - head -n -0 "$benchmark" > "$pfbenchmark"; - echo "$proof_command" >>"$pfbenchmark"; - echo "(exit)" >> "$pfbenchmark"; - else - cp $benchmark $pfbenchmark - echo "$proof_command" >>"$pfbenchmark"; +if $check_models || $check_proofs; then + check_cmdline= + if $check_models; then + check_cmdline="$check_cmdline --check-models" fi - echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`] - time ( :; \ - ( cd `dirname "$pfbenchmark"`; - $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof `basename "$pfbenchmark"`; - echo $? >"$exitstatusfile" - ) > "$outfile" 2> "$errfile" ) - - gettemp pfoutfile cvc4_proof.$$.XXXXXXXXXX - - diff --unchanged-group-format='' \ - --old-group-format='' \ - --new-group-format='%>' \ - "$expoutfile" "$outfile" > "$pfoutfile" - if [ ! -s "$pfoutfile" ]; then - echo "$prog: error: proof generation failed with empty output (stderr follows)" - cat "$errfile" - exitcode=1 - else - echo running $LFSC "$pfoutfile" [from working dir `dirname "$pfbenchmark"`] - if ! $LFSC "$pfoutfile" &> "$errfile"; then - echo "$prog: error: proof checker failed (output follows)" - cat "$errfile" - exitcode=1 - fi + if $check_proofs; then + check_cmdline="$check_cmdline --check-proofs" fi -fi - -if $check_models; then - # at least one sat/invalid response: run an extra model-checking pass - if ! CVC4_REGRESSION_ARGS="$CVC4_REGRESSION_ARGS --check-models" "$0" $wrapper "$cvc4" "$benchmark_orig"; then + # at least one sat/invalid response: run an extra model/proof-checking pass + if ! CVC4_REGRESSION_ARGS="$CVC4_REGRESSION_ARGS$check_cmdline" "$0" $wrapper "$cvc4" "$benchmark_orig"; then exitcode=1 fi fi |