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
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
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 \
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
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])
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$,,'])
)
Muzzle : $enable_muzzle
Unit tests : $support_unit_tests
-Proof tests : $support_proof_tests
gcov support : $enable_coverage
gprof support: $enable_profiling
--- /dev/null
+# 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
-; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf\r
-\r
-; -------------------------------------------------------------------------------- \r
-; input :\r
-; ( a = b )\r
-; ( b = f(c) )\r
-; ( a != f(c) V a != b )\r
-\r
-; theory lemma (by transitivity) :\r
-; ( a != b V b != f(c) V a = f(c) )\r
-\r
-\r
-; With the theory lemma, the input is unsatisfiable.\r
-; -------------------------------------------------------------------------------- \r
-\r
-\r
-\r
-(check \r
-(% s sort\r
-(% a (term s)\r
-(% b (term s)\r
-(% c (term s)\r
-(% f (term (arrow s s))\r
-\r
-; -------------------- declaration of input formula -----------------------------------\r
-\r
-(% A1 (th_holds (= s a b))\r
-(% A2 (th_holds (= s b (apply _ _ f c)))\r
-(% A3 (th_holds (or (not (= s a (apply _ _ f c))) (not (= s a b))))\r
-\r
-\r
-; ------------------- specify that the following is a proof of the empty clause -----------------\r
-\r
-(: (holds cln)\r
-\r
-; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------\r
-\r
-(decl_atom (= s a b) (\ v1 (\ a1\r
-(decl_atom (= s b (apply _ _ f c)) (\ v2 (\ a2\r
-(decl_atom (= s a (apply _ _ f c)) (\ v3 (\ a3\r
-\r
-\r
-; --------------------------- proof of theory lemma ---------------------------------------------\r
-\r
-(satlem _ _\r
-(ast _ _ _ a1 (\ l1\r
-(ast _ _ _ a2 (\ l2\r
-(asf _ _ _ a3 (\ l3\r
-(clausify_false\r
-\r
-; this should be a proof of l1 ^ l2 ^ ~l3 => false\r
-; this is done by theory proof rules (currently just use "trust")\r
-\r
- trust\r
-\r
-))))))) (\ CT\r
-; CT is the clause ( ~v1 V ~v2 V v3 )\r
-\r
-; -------------------- clausification of input formulas -----------------------------------------\r
-\r
-(satlem _ _\r
-(asf _ _ _ a1 (\ l1\r
-(clausify_false\r
-\r
-; input formula A1 is ( ~l1 )\r
-; the following should be a proof of l1 ^ ( ~l1 ) => false\r
-; this is done by natural deduction rules\r
-\r
- (contra _ A1 l1)\r
-\r
-))) (\ C1\r
-; C1 is the clause ( v1 )\r
-\r
-\r
-(satlem _ _\r
-(asf _ _ _ a2 (\ l2\r
-(clausify_false\r
-\r
-; input formula A2 is ( ~l2 )\r
-; the following should be a proof of l2 ^ ( ~l2 ) => false\r
-; this is done by natural deduction rules\r
-\r
- (contra _ A2 l2)\r
- \r
-))) (\ C2 \r
-; C2 is the clause ( v2 )\r
-\r
-\r
-(satlem _ _\r
-(ast _ _ _ a3 (\ l3\r
-(ast _ _ _ a1 (\ l1\r
-(clausify_false\r
-\r
-; input formula A3 is ( ~a3 V ~a1 ) \r
-; the following should be a proof of a3 ^ a1 ^ ( ~a3 V ~a1 ) => false\r
-; this is done by natural deduction rules\r
-\r
- (contra _ l1 (or_elim_1 _ _ (not_not_intro _ l3) A3))\r
-\r
-))))) (\ C3 \r
-; C3 is the clause ( ~v3 V ~v1 )\r
-\r
-\r
-\r
-; -------------------- resolution proof ------------------------------------------------------------\r
-\r
-(satlem_simplify _ _ _ \r
-\r
-(R _ _ C1\r
-(R _ _ C2\r
-(R _ _ CT C3 v3) v2) v1)\r
-\r
-(\ x x))\r
-\r
-))))))))))))))))))))))))))\r
-)
\ 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))
+
+))))))))))))))))))))))))))
+)
-(declare bool type)\r
-(declare tt bool)\r
-(declare ff bool)\r
-\r
-(declare var type) \r
-\r
-(declare lit type)\r
-(declare pos (! x var lit))\r
-(declare neg (! x var lit))\r
-\r
-(declare clause type)\r
-(declare cln clause)\r
-(declare clc (! x lit (! c clause clause)))\r
-\r
-; constructs for general clauses for R, Q, satlem\r
-\r
-(declare concat (! c1 clause (! c2 clause clause)))\r
-(declare clr (! l lit (! c clause clause))) \r
-\r
-; code to check resolutions\r
-\r
-(program append ((c1 clause) (c2 clause)) clause\r
- (match c1 (cln c2) ((clc l c1') (clc l (append c1' c2)))))\r
-\r
-; we use marks as follows:\r
-; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable.\r
-; -- mark 2 to record if we are supposed to remove a negative occurrence of the variable.\r
-; -- mark 3 if we did indeed remove the variable positively\r
-; -- mark 4 if we did indeed remove the variable negatively\r
-(program simplify_clause ((c clause)) clause\r
- (match c\r
- (cln cln)\r
- ((clc l c1)\r
- (match l\r
- ; Set mark 1 on v if it is not set, to indicate we should remove it.\r
- ; After processing the rest of the clause, set mark 3 if we were already \r
- ; supposed to remove v (so if mark 1 was set when we began). Clear mark3\r
- ; if we were not supposed to be removing v when we began this call.\r
- ((pos v)\r
- (let m (ifmarked v tt (do (markvar v) ff))\r
- (let c' (simplify_clause c1)\r
- (match m\r
- (tt (do (ifmarked3 v v (markvar3 v)) c')) \r
- (ff (do (ifmarked3 v (markvar3 v) v) (markvar v) (clc l c')))))))\r
- ; the same as the code for tt, but using different marks.\r
- ((neg v)\r
- (let m (ifmarked2 v tt (do (markvar2 v) ff))\r
- (let c' (simplify_clause c1)\r
- (match m\r
- (tt (do (ifmarked4 v v (markvar4 v)) c')) \r
- (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c')))))))))\r
- ((concat c1 c2) (append (simplify_clause c1) (simplify_clause c2)))\r
- ((clr l c1)\r
- (match l\r
- ; set mark 1 to indicate we should remove v, and fail if\r
- ; mark 3 is not set after processing the rest of the clause\r
- ; (we will set mark 3 if we remove a positive occurrence of v).\r
- ((pos v)\r
- (let m (ifmarked v tt (do (markvar v) ff))\r
- (let m3 (ifmarked3 v (do (markvar3 v) tt) ff)\r
- (let c' (simplify_clause c1)\r
- (ifmarked3 v (do (match m3 (tt v) (ff (markvar3 v)))\r
- (match m (tt v) (ff (markvar v))) c')\r
- (fail clause))))))\r
- ; same as the tt case, but with different marks.\r
- ((neg v)\r
- (let m2 (ifmarked2 v tt (do (markvar2 v) ff))\r
- (let m4 (ifmarked4 v (do (markvar4 v) tt) ff)\r
- (let c' (simplify_clause c1)\r
- (ifmarked4 v (do (match m4 (tt v) (ff (markvar4 v)))\r
- (match m2 (tt v) (ff (markvar2 v))) c')\r
- (fail clause))))))\r
- ))))\r
-\r
-\r
-; resolution proofs\r
- \r
-(declare holds (! c clause type))\r
-\r
-(declare R (! c1 clause (! c2 clause \r
- (! u1 (holds c1)\r
- (! u2 (holds c2)\r
- (! n var\r
- (holds (concat (clr (pos n) c1)\r
- (clr (neg n) c2))))))))) \r
-\r
-(declare Q (! c1 clause (! c2 clause \r
- (! u1 (holds c1)\r
- (! u2 (holds c2)\r
- (! n var\r
- (holds (concat (clr (neg n) c1)\r
- (clr (pos n) c2)))))))))\r
- \r
-(declare satlem_simplify\r
- (! c1 clause\r
- (! c2 clause\r
- (! c3 clause\r
- (! u1 (holds c1)\r
- (! r (^ (simplify_clause c1) c2)\r
- (! u2 (! x (holds c2) (holds c3))\r
- (holds c3))))))))\r
- \r
-(declare satlem\r
- (! c clause\r
- (! c2 clause\r
- (! u (holds c)\r
- (! u2 (! v (holds c) (holds c2))\r
- (holds c2))))))\r
-\r
-; A little example to demonstrate simplify_clause.\r
-; It can handle nested clr's of both polarities,\r
-; and correctly cleans up marks when it leaves a\r
-; clr or clc scope. Uncomment and run with \r
-; --show-runs to see it in action.\r
-; \r
-; (check \r
-; (% v1 var\r
-; (% u1 (holds (concat (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln))))))\r
-; (clc (pos v1) (clc (pos v1) cln))))\r
-; (satlem _ _ _ u1 (\ x x))))))\r
-\r
-\r
-;(check \r
-; (% v1 var\r
-; (% u1 (holds (clr (neg v1) (concat (clc (neg v1) cln)\r
-; (clr (neg v1) (clc (neg v1) cln)))))\r
-; (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))))))
(! t1 (term (arrow s1 s2))
(! t2 (term s1)
(term s2))))))
-
+
(declare ite (! s sort
(! f formula
(! t1 (term s)
(! f formula
(! u (th_holds f)
(th_holds (not (not f))))))
-
+
(declare not_not_elim
(! f formula
(! u (th_holds (not (not f)))
(! 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
(! 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
(! 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))))))
(! 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
(! f2 formula
(! u1 (th_holds (iff f1 f2))
(th_holds (impl f1 f2))))))
-
+
(declare iff_elim_2
(! f1 formula
(! f2 formula
(! u1 (th_holds a)
(! u2 (th_holds (ifte a b c))
(th_holds b)))))))
-
+
(declare ite_elim_2
(! a formula
(! b formula
(! u1 (th_holds (not a))
(! u2 (th_holds (ifte a b c))
(th_holds c)))))))
-
+
(declare ite_elim_3
(! a formula
(! b formula
(! u1 (th_holds (not b))
(! u2 (th_holds (ifte a b c))
(th_holds c)))))))
-
+
(declare ite_elim_2n
(! a formula
(! b formula
(! 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
(! 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
(! 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
(! 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))))).
;; (contra _
;; (or_elim_1 _ _ l{n-1}
;; ...
-;; (or_elim_1 _ _ l2
+;; (or_elim_1 _ _ l2
;; (or_elim_1 _ _ l1 A))))) ln)
;;
;;))))))) (\ C
;;(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 )
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
-;\r
-; Atomization / Clausification\r
-;\r
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
- \r
-; binding between an LF var and an (atomic) formula\r
-(declare atom (! v var (! p formula type)))\r
-\r
-(declare decl_atom\r
- (! f formula\r
- (! u (! v var \r
- (! a (atom v f)\r
- (holds cln)))\r
- (holds cln))))\r
- \r
-; direct clausify\r
-(declare clausify_form\r
- (! f formula\r
- (! v var\r
- (! a (atom v f)\r
- (! u (th_holds f)\r
- (holds (clc (pos v) cln)))))))\r
- \r
-(declare clausify_form_not\r
- (! f formula\r
- (! v var\r
- (! a (atom v f)\r
- (! u (th_holds (not f))\r
- (holds (clc (neg v) cln)))))))\r
-\r
-(declare clausify_false\r
- (! u (th_holds false)\r
- (holds cln)))\r
-\r
- \r
-(declare th_let_pf\r
- (! f formula\r
- (! u (th_holds f)\r
- (! u2 (! v (th_holds f) (holds cln))\r
- (holds cln)))))\r
-\r
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
-;\r
-; Theory reasoning\r
-; - make a series of assumptions and then derive a contradiction (or false)\r
-; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"\r
-; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"\r
-;\r
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
-\r
-(declare ast\r
- (! v var\r
- (! f formula\r
- (! C clause\r
- (! r (atom v f) ;this is specified\r
- (! u (! o (th_holds f)\r
- (holds C))\r
- (holds (clc (neg v) C))))))))\r
-\r
-(declare asf\r
- (! v var\r
- (! f formula\r
- (! C clause\r
- (! r (atom v f)\r
- (! u (! o (th_holds (not f))\r
- (holds C))\r
- (holds (clc (pos v) C))))))))\r
-\r
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
-;\r
-; Theory of Equality and Congruence Closure\r
-;\r
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
-\r
-; temporary : \r
-(declare trust (th_holds false))\r
-\r
-(declare refl\r
- (! s sort\r
- (! t (term s)\r
- (th_holds (= s t t)))))\r
-\r
-(declare symm (! s sort\r
- (! x (term s)\r
- (! y (term s)\r
- (! u (th_holds (= _ x y))\r
- (th_holds (= _ y x)))))))\r
-\r
-(declare trans (! s sort\r
- (! x (term s)\r
- (! y (term s)\r
- (! z (term s)\r
- (! u (th_holds (= _ x y))\r
- (! u (th_holds (= _ y z))\r
- (th_holds (= _ x z)))))))))\r
-\r
-(declare cong (! s1 sort\r
- (! s2 sort\r
- (! a1 (term (arrow s1 s2))\r
- (! b1 (term (arrow s1 s2))\r
- (! a2 (term s1)\r
- (! b2 (term s1)\r
- (! u1 (th_holds (= _ a1 b1))\r
- (! u2 (th_holds (= _ a2 b2))\r
- (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))\r
- \r
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; 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))))))))))))
+
@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
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;
}
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
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 ?
! 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();
<< "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);
}
predicates=
links=
links_alternate=
+ smt_links=
options_already_documented=false
alternate_options_already_documented=false
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
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\"
#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
#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
#line $lineno \"$kf\"
if(key == \"$smtname\") {
#line $lineno \"$kf\"
- $run_handlers$run_links
+ $run_handlers$run_smt_links
return;
}"
else
#line $lineno \"$kf\"
if(key == \"$smtname\") {
#line $lineno \"$kf\"
- $run_handlers$run_links
+ $run_handlers$run_smt_links
return;
}"
fi
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) ||
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() << ")";
}
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) ||
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() << ")";
}
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) ||
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() << ")";
}
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);
}
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 */
-
**
** A manager for CnfProofs.
**
- **
+ **
**/
#ifndef __CVC4__CNF_PROOF_H
#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 */
#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)
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),
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() {
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() {
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));
}
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;
}
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 */
** 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"
#ifndef __CVC4__PROOF_MANAGER_H
#define __CVC4__PROOF_MANAGER_H
-#include <iostream>
+#include <iostream>
#include "proof/proof.h"
#include "util/proof.h"
// forward declarations
namespace Minisat {
class Solver;
-}
+}/* Minisat namespace */
namespace CVC4 {
namespace prop {
class CnfStream;
-}
+}/* CVC4::prop namespace */
-class SmtEngine;
+class SmtEngine;
typedef int ClauseId;
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 {
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;
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();
// 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(); }
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);
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 */
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 */
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;
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
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
*/
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
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);
}
}
{}
void ProofProxy::updateCRef(CRef oldref, CRef newref) {
- d_proof->updateCRef(oldref, newref);
+ d_proof->updateCRef(oldref, newref);
}
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) {
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;
}
}
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) {
<< (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";
}
/// 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) {
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);
}
}
}
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));
}
}
/// 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) {
// 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) {
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;
}
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();
}
}
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);
}
}
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
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Resolution proof
+ ** \brief Resolution proof
**
** Resolution proof
**/
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;
{}
};/* 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:
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; }
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:
};/* 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;
// 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
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);
{}
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);
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) {
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) {
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 << ")";
}
-}
+}
**
** A manager for UfProofs.
**
- **
+ **
**/
#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 */
// 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);
} 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;
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
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;
}
}
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);
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;
}
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)
} 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;
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)
#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"
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 */
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);
d_decisionEngine(NULL),
d_theoryEngine(NULL),
d_propEngine(NULL),
+ d_proofManager(NULL),
d_definedFunctions(NULL),
d_assertionList(NULL),
d_assignments(NULL),
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));
if(options::cumulativeMillisecondLimit() != 0) {
setTimeLimit(options::cumulativeMillisecondLimit(), true);
}
+
PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); );
}
}
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"));
finalOptionsAreSet();
doPendingPops();
-
- PROOF( ProofManager::currentPM()->addAssertion(ex); );
-
Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl;
if(d_queryMade && !options::incrementalSolving()) {
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
// 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();
}
}
// 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) {
// 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();
}
}
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
class DecisionEngine;
class TheoryEngine;
+class ProofManager;
+
class Model;
class StatisticsRegistry;
class BooleanTermConverter;
void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
+ ProofManager* currentProofManager();
struct CommandCleanup;
typedef context::CDList<Command*, CommandCleanup> CommandList;
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.
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;
**/
#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 */
#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;
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;
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());
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
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
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
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
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
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
ELSE FALSE
ENDIF;
QUERY a288;
-% PROOF
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
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
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
+% COMMAND-LINE: --no-check-proofs
+%
OPTION "incremental";
a1, a2 : []; % empty tuples (a unit type)
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
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
-; 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.
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
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
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
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
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
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
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
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
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
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
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
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
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
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
% EXPECT: valid
QUERY a OR (a AND b) <=> a;
-% PROOF
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
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
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
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
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,,'`
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,,'`
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=
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,,'`
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,,'`
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=
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
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
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"
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
projects / cvc5.git / commitdiff