From ad0f78965f23b0994cac6a210650697b9a20cceb Mon Sep 17 00:00:00 2001 From: lianah Date: Tue, 5 Nov 2013 20:03:49 -0500 Subject: [PATCH] fixed proof regression script and added a new uf test case --- src/proof/cnf_proof.cpp | 14 +++++++++++--- src/proof/proof_manager.cpp | 19 +++++++++++++++---- src/proof/proof_manager.h | 15 ++++++++++++--- src/proof/sat_proof.cpp | 6 +++--- src/proof/theory_proof.cpp | 2 +- src/smt/smt_engine.cpp | 3 ++- test/regress/regress0/uf/Makefile.am | 3 ++- test/regress/regress0/uf/proof00.smt2 | 21 +++++++++++++++++++++ test/regress/run_regression | 16 ++++++++++++---- 9 files changed, 79 insertions(+), 20 deletions(-) create mode 100644 test/regress/regress0/uf/proof00.smt2 diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index cb22ca819..8e9c4cd21 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -33,7 +33,8 @@ CnfProof::CnfProof(CnfStream* stream) Expr CnfProof::getAtom(prop::SatVariable var) { prop::SatLiteral lit (var); - Expr atom = d_cnfStream->getNode(lit).toExpr(); + Node node = d_cnfStream->getNode(lit); + Expr atom = node.toExpr(); return atom; } @@ -45,9 +46,16 @@ void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) { ProofManager::var_iterator end = ProofManager::currentPM()->end_vars(); for (;it != end; ++it) { - Expr atom = getAtom(*it); os << "(decl_atom "; - LFSCTheoryProof::printFormula(atom, os); + + if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) { + Expr atom = getAtom(*it); + LFSCTheoryProof::printFormula(atom, os); + } else { + // print fake atoms for all other logics + os << "true "; + } + os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n"; paren << ")))"; } diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 23ba0e4e7..110e6b79a 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -21,6 +21,8 @@ #include "proof/cnf_proof.h" #include "proof/theory_proof.h" #include "util/cvc4_assert.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" namespace CVC4 { @@ -68,12 +70,13 @@ ProofManager* ProofManager::currentPM() { } } -Proof* ProofManager::getProof() { +Proof* ProofManager::getProof(SmtEngine* smt) { if (currentPM()->d_fullProof != NULL) return currentPM()->d_fullProof; Assert (currentPM()->d_format == LFSC); - currentPM()->d_fullProof = new LFSCProof((LFSCSatProof*)getSatProof(), + currentPM()->d_fullProof = new LFSCProof(smt, + (LFSCSatProof*)getSatProof(), (LFSCCnfProof*)getCnfProof(), (LFSCTheoryProof*)getTheoryProof()); return currentPM()->d_fullProof; @@ -138,19 +141,27 @@ void ProofManager::addAssertion(Expr formula) { d_inputFormulas.insert(formula); } +void ProofManager::setLogic(const std::string& logic_string) { + d_logic = logic_string; +} + -LFSCProof::LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory) +LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory) : d_satProof(sat) , d_cnfProof(cnf) , d_theoryProof(theory) + , d_smtEngine(smtEngine) { d_satProof->constructProof(); } void LFSCProof::toStream(std::ostream& out) { + smt::SmtScope scope(d_smtEngine); std::ostringstream paren; out << "(check \n"; - d_theoryProof->printAssertions(out, paren); + if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) { + d_theoryProof->printAssertions(out, paren); + } out << "(: (holds cln) \n"; d_cnfProof->printAtomMapping(out, paren); d_cnfProof->printClauses(out, paren); diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 7642ba776..82a1bd6be 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -36,6 +36,9 @@ namespace CVC4 { namespace prop { class CnfStream; } + +class SmtEngine; + typedef int ClauseId; class Proof; @@ -91,6 +94,8 @@ class ProofManager { static bool isInitialized; ProofManager(ProofFormat format = LFSC); ~ProofManager(); +protected: + std::string d_logic; public: static ProofManager* currentPM(); // initialization @@ -98,7 +103,7 @@ public: static void initCnfProof(CVC4::prop::CnfStream* cnfStream); static void initTheoryProof(); - static Proof* getProof(); + static Proof* getProof(SmtEngine* smt); static SatProof* getSatProof(); static CnfProof* getCnfProof(); static TheoryProof* getTheoryProof(); @@ -131,14 +136,18 @@ public: static std::string getVarName(prop::SatVariable var); static std::string getAtomName(prop::SatVariable var); static std::string getLitName(prop::SatLiteral lit); + + void setLogic(const std::string& logic_string); + const std::string getLogic() const { return d_logic; } };/* class ProofManager */ class LFSCProof : public Proof { LFSCSatProof* d_satProof; LFSCCnfProof* d_cnfProof; - LFSCTheoryProof* d_theoryProof; + LFSCTheoryProof* d_theoryProof; + SmtEngine* d_smtEngine; public: - LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); + LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); virtual void toStream(std::ostream& out); virtual ~LFSCProof() {} }; diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index 2ac468b47..da9df0d42 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -579,9 +579,9 @@ void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { res->addStep(lit, res_id, !sign(lit)); } registerResolution(d_emptyClauseId, res); - // FIXME: massive hack - Proof* proof = ProofManager::getProof(); - proof->toStream(std::cout); + // // FIXME: massive hack + // Proof* proof = ProofManager::getProof(); + // proof->toStream(std::cout); } /// CRef manager diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 4ce804a74..696bd8309 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -167,7 +167,7 @@ void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) { // declaring the terms for (ExprSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) { Expr term = *it; - + os << "(% " << term << " (term "; paren <<")"; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 32d0d1703..0cfb674cf 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -680,6 +680,7 @@ void SmtEngine::finishInit() { if(options::cumulativeMillisecondLimit() != 0) { setTimeLimit(options::cumulativeMillisecondLimit(), true); } + PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); } void SmtEngine::finalOptionsAreSet() { @@ -3713,7 +3714,7 @@ Proof* SmtEngine::getProof() throw(ModalException) { throw ModalException(msg); } - return ProofManager::getProof(); + return ProofManager::getProof(this); #else /* CVC4_PROOF */ throw ModalException("This build of CVC4 doesn't have proof support."); #endif /* CVC4_PROOF */ diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index bf9a36df1..19e673fea 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -42,7 +42,8 @@ TESTS = \ simple.01.cvc \ simple.02.cvc \ simple.03.cvc \ - simple.04.cvc + simple.04.cvc \ + proof00.smt2 EXTRA_DIST = $(TESTS) \ mkpidgeon diff --git a/test/regress/regress0/uf/proof00.smt2 b/test/regress/regress0/uf/proof00.smt2 new file mode 100644 index 000000000..1b7e7b8dd --- /dev/null +++ b/test/regress/regress0/uf/proof00.smt2 @@ -0,0 +1,21 @@ +; PROOF +(set-logic QF_UF) +(set-info :source | +CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC + for more information. + +This benchmark was obtained by trying to find a finite model of a first-order +formula (Albert Oliveras). +|) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-sort U 0) +(declare-fun c3 () U) +(declare-fun f1 (U U) U) +(declare-fun f4 (U) U) +(declare-fun c2 () U) +(declare-fun c_0 () U) +(declare-fun c_1 () U) +(assert (let ((?v_1 (f1 c3 c_0))) (let ((?v_0 (f1 ?v_1 c_0)) (?v_2 (f1 c_0 c_0)) (?v_4 (f1 c_0 c_1)) (?v_3 (f1 ?v_1 c_1)) (?v_6 (f1 c3 c_1))) (let ((?v_5 (f1 ?v_6 c_0)) (?v_7 (f1 c_1 c_0)) (?v_9 (f1 c_1 c_1)) (?v_8 (f1 ?v_6 c_1)) (?v_10 (f4 c_0))) (let ((?v_11 (f1 c_0 ?v_10)) (?v_12 (f4 c_1))) (let ((?v_13 (f1 c_1 ?v_12)) (?v_15 (f1 c2 c_0))) (let ((?v_14 (f1 ?v_15 c_0)) (?v_16 (f1 ?v_15 c_1)) (?v_18 (f1 c2 c_1))) (let ((?v_17 (f1 ?v_18 c_0)) (?v_19 (f1 ?v_18 c_1))) (and (distinct c_0 c_1) (= (f1 ?v_0 c_0) (f1 c_0 ?v_2)) (= (f1 ?v_0 c_1) (f1 c_0 ?v_4)) (= (f1 ?v_3 c_0) (f1 c_1 ?v_2)) (= (f1 ?v_3 c_1) (f1 c_1 ?v_4)) (= (f1 ?v_5 c_0) (f1 c_0 ?v_7)) (= (f1 ?v_5 c_1) (f1 c_0 ?v_9)) (= (f1 ?v_8 c_0) (f1 c_1 ?v_7)) (= (f1 ?v_8 c_1) (f1 c_1 ?v_9)) (not (= ?v_11 (f1 ?v_10 ?v_11))) (not (= ?v_13 (f1 ?v_12 ?v_13))) (= (f1 ?v_14 c_0) (f1 (f1 ?v_2 c_0) c_0)) (= (f1 ?v_14 c_1) (f1 (f1 ?v_4 c_0) c_1)) (= (f1 ?v_16 c_0) (f1 (f1 ?v_2 c_1) c_0)) (= (f1 ?v_16 c_1) (f1 (f1 ?v_4 c_1) c_1)) (= (f1 ?v_17 c_0) (f1 (f1 ?v_7 c_0) c_0)) (= (f1 ?v_17 c_1) (f1 (f1 ?v_9 c_0) c_1)) (= (f1 ?v_19 c_0) (f1 (f1 ?v_7 c_1) c_0)) (= (f1 ?v_19 c_1) (f1 (f1 ?v_9 c_1) c_1)) (or (= ?v_2 c_0) (= ?v_2 c_1)) (or (= ?v_4 c_0) (= ?v_4 c_1)) (or (= ?v_7 c_0) (= ?v_7 c_1)) (or (= ?v_9 c_0) (= ?v_9 c_1)) (or (= ?v_10 c_0) (= ?v_10 c_1)) (or (= ?v_12 c_0) (= ?v_12 c_1)) (or (= c3 c_0) (= c3 c_1)) (or (= c2 c_0) (= c2 c_1))))))))))) +(check-sat) diff --git a/test/regress/run_regression b/test/regress/run_regression index e9c17a3af..44517cc0c 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -112,7 +112,7 @@ 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_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,,'` @@ -140,7 +140,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then expected_exit_status=10 command_line= elif grep '^ *( *set-info *:status *unsat' "$benchmark" &>/dev/null; then - expected_proof= + expected_proof=`grep '^; PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=unsat expected_exit_status=20 command_line= @@ -276,8 +276,15 @@ fi if [ "$proof" = yes -a "$expected_proof" = yes ]; then gettemp pfbenchmark cvc4_pfbenchmark.$$.XXXXXXXXXX - cp "$benchmark" "$pfbenchmark"; - echo "$proof_command" >>"$pfbenchmark"; + # 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"; + fi echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`] time ( :; \ ( cd `dirname "$pfbenchmark"`; @@ -286,6 +293,7 @@ if [ "$proof" = yes -a "$expected_proof" = yes ]; then ) > "$outfile" 2> "$errfile" ) gettemp pfoutfile cvc4_proof.$$.XXXXXXXXXX + diff --unchanged-group-format='' \ --old-group-format='' \ --new-group-format='%>' \ -- 2.30.2