From: Morgan Deters Date: Sat, 29 Oct 2011 05:21:49 +0000 (+0000) Subject: Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::getProof... X-Git-Tag: cvc5-1.0.0~8403 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=02f4f0500849bc719cb45bbc771bea90eb6e96f8;p=cvc5.git Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::getProof(), a few other things.. --- diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 61702561a..345d7f956 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -423,6 +423,23 @@ void GetAssignmentCommand::printResult(std::ostream& out) const { out << d_result << endl; } +/* class GetProofCommand */ + +GetProofCommand::GetProofCommand() { +} + +void GetProofCommand::invoke(SmtEngine* smtEngine) { + d_result = smtEngine->getProof(); +} + +Proof* GetProofCommand::getResult() const { + return d_result; +} + +void GetProofCommand::printResult(std::ostream& out) const { + d_result->toStream(out); +} + /* class GetAssertionsCommand */ GetAssertionsCommand::GetAssertionsCommand() { diff --git a/src/expr/command.h b/src/expr/command.h index 5cf4f6fa0..b686025fe 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -35,6 +35,7 @@ #include "util/result.h" #include "util/sexpr.h" #include "util/datatype.h" +#include "util/proof.h" namespace CVC4 { @@ -232,6 +233,16 @@ public: void printResult(std::ostream& out) const; };/* class GetAssignmentCommand */ +class CVC4_PUBLIC GetProofCommand : public Command { +protected: + Proof* d_result; +public: + GetProofCommand(); + void invoke(SmtEngine* smtEngine); + Proof* getResult() const; + void printResult(std::ostream& out) const; +};/* class GetProofCommand */ + class CVC4_PUBLIC GetAssertionsCommand : public Command { protected: std::string d_result; diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 96c0933d8..22cf368eb 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -705,8 +705,10 @@ mainCommand[CVC4::Command*& cmd] | { PARSER_STATE->parseError("No filename given to INCLUDE command"); } ) - | ( DUMP_PROOF_TOK - | DUMP_ASSUMPTIONS_TOK + | DUMP_PROOF_TOK + { cmd = new GetProofCommand(); } + + | ( DUMP_ASSUMPTIONS_TOK | DUMP_SIG_TOK | DUMP_TCC_TOK | DUMP_TCC_ASSUMPTIONS_TOK diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 7fb671bb0..974de29b2 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -297,7 +297,7 @@ command returns [CVC4::Command* cmd = NULL] { cmd = new GetAssertionsCommand; } | /* get-proof */ GET_PROOF_TOK - { UNSUPPORTED("get-proof command not yet supported"); } + { cmd = new GetProofCommand; } | /* get-unsat-core */ GET_UNSAT_CORE_TOK { UNSUPPORTED("unsat cores not yet supported"); } diff --git a/src/proof/proof.h b/src/proof/proof.h index 3e5b54cc7..a3270c4c0 100644 --- a/src/proof/proof.h +++ b/src/proof/proof.h @@ -16,8 +16,8 @@ ** Proof manager **/ -#ifndef __CVC4__PROOF_H -#define __CVC4__PROOF_H +#ifndef __CVC4__PROOF__PROOF_H +#define __CVC4__PROOF__PROOF_H #include "util/options.h" @@ -33,4 +33,4 @@ -#endif /* __CVC4__PROOF_H */ +#endif /* __CVC4__PROOF__PROOF_H */ diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 2d7432cbc..4191d1046 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -18,6 +18,7 @@ **/ #include "proof/proof_manager.h" +#include "util/proof.h" #include "proof/sat_proof.h" #include "proof/cnf_proof.h" #include "util/Assert.h" @@ -40,7 +41,12 @@ ProofManager* ProofManager::currentPM() { proofManager = new ProofManager(); isInitialized = true; return proofManager; - } + } +} + +Proof* ProofManager::getProof() { + // for now, this is just the SAT proof + return getSatProof(); } SatProof* ProofManager::getSatProof() { diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index c79d26fed..e23fbd600 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -22,7 +22,7 @@ #define __CVC4__PROOF_MANAGER_H #include -#include "proof.h" +#include "proof/proof.h" // forward declarations namespace Minisat { @@ -33,6 +33,7 @@ namespace CVC4 { namespace prop { class CnfStream; } +class Proof; class SatProof; class CnfProof; @@ -56,6 +57,7 @@ public: static void initSatProof(Minisat::Solver* solver); static void initCnfProof(CVC4::prop::CnfStream* cnfStream); + static Proof* getProof(); static SatProof* getSatProof(); static CnfProof* getCnfProof(); diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index 57bb96513..37a3a9706 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -524,8 +524,9 @@ ClauseId SatProof::resolveUnit(Lit lit) { return unit_id; } -void SatProof::printProof() { +void SatProof::toStream(std::ostream& out) { Debug("proof:sat") << "SatProof::printProof\n"; + Unimplemented("native proof printing not supported yet"); } void SatProof::finalizeProof(CRef conflict_ref) { @@ -543,7 +544,6 @@ void SatProof::finalizeProof(CRef conflict_ref) { res->addStep(lit, res_id, !sign(lit)); } registerResolution(d_emptyClauseId, res); - printProof(); } /// CRef manager @@ -693,8 +693,7 @@ void LFSCSatProof::printVariables() { } -void LFSCSatProof::flush() { - ostringstream out; +void LFSCSatProof::flush(std::ostream& out) { out << "(check \n"; d_paren <<")"; out << d_varSS.str(); @@ -703,11 +702,10 @@ void LFSCSatProof::flush() { out << d_lemmaSS.str(); d_paren << "))"; out << d_paren.str(); - out << ";"; //to comment out the solver's answer - std::cout << out.str(); + out << "\n"; } -void LFSCSatProof::printProof() { +void LFSCSatProof::toStream(std::ostream& out) { Debug("proof:sat") << " LFSCSatProof::printProof \n"; // first collect lemmas to print in reverse order @@ -722,8 +720,7 @@ void LFSCSatProof::printProof() { printClauses(); printVariables(); - flush(); - + flush(out); } } /* CVC4 namespace */ diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 4641ea4cc..051266df8 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -32,6 +32,7 @@ typedef uint32_t CRef; } #include "prop/minisat/core/SolverTypes.h" +#include "util/proof.h" namespace std { using namespace __gnu_cxx; @@ -99,7 +100,7 @@ public: void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref); }; -class SatProof { +class SatProof : public Proof { protected: ::Minisat::Solver* d_solver; // clauses @@ -144,8 +145,8 @@ protected: ::Minisat::Lit getUnit(ClauseId id); ClauseId getUnitId(::Minisat::Lit lit); ::Minisat::Clause& getClause(ClauseId id); - virtual void printProof(); - + virtual void toStream(std::ostream& out); + bool checkResolution(ClauseId id); /** * Constructs a resolution tree that proves lit @@ -237,7 +238,7 @@ private: void printVariables(); void printClauses(); - void flush(); + void flush(std::ostream& out); public: LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false): @@ -249,7 +250,7 @@ public: d_seenLemmas(), d_seenInput() {} - void printProof(); + virtual void toStream(std::ostream& out); }; } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 96ee5b59b..7ea22ce8f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -34,6 +34,8 @@ #include "smt/no_such_function_exception.h" #include "smt/smt_engine.h" #include "theory/theory_engine.h" +#include "proof/proof_manager.h" +#include "util/proof.h" #include "util/boolean_simplification.h" #include "util/configuration.h" #include "util/exception.h" @@ -987,7 +989,7 @@ Expr SmtEngine::getValue(const Expr& e) d_status.asSatisfiabilityResult() != Result::SAT || d_problemExtended) { const char* msg = - "Cannot get value unless immediately proceded by SAT/INVALID response."; + "Cannot get value unless immediately preceded by SAT/INVALID response."; throw ModalException(msg); } if(type.isFunction() || type.isPredicate() || @@ -1040,6 +1042,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { Trace("smt") << "SMT getAssignment()" << endl; + NodeManagerScope nms(d_nodeManager); if(Dump.isOn("benchmark")) { Dump("benchmark") << GetAssignmentCommand() << endl; } @@ -1053,7 +1056,8 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { d_status.asSatisfiabilityResult() != Result::SAT || d_problemExtended) { const char* msg = - "Cannot get value unless immediately proceded by SAT/INVALID response."; + "Cannot get the current assignment unless immediately " + "preceded by SAT/INVALID response."; throw ModalException(msg); } @@ -1061,7 +1065,6 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { return SExpr(); } - NodeManagerScope nms(d_nodeManager); vector sexprs; TypeNode boolType = d_nodeManager->booleanType(); for(AssignmentSet::const_iterator i = d_assignments->begin(), @@ -1093,6 +1096,32 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { return SExpr(sexprs); } +Proof* SmtEngine::getProof() throw(ModalException, AssertionException) { + Trace("smt") << "SMT getProof()" << endl; + NodeManagerScope nms(d_nodeManager); + if(Dump.isOn("benchmark")) { + Dump("benchmark") << GetProofCommand() << endl; + } +#ifdef CVC4_PROOF + if(!Options::current()->proof) { + const char* msg = + "Cannot get a proof when produce-proofs option is off."; + throw ModalException(msg); + } + if(d_status.isNull() || + d_status.asSatisfiabilityResult() != Result::UNSAT || + d_problemExtended) { + const char* msg = + "Cannot get a proof unless immediately preceded by UNSAT/VALID response."; + throw ModalException(msg); + } + + return ProofManager::getProof(); +#else /* CVC4_PROOF */ + throw ModalException("This build of CVC4 doesn't have proof support."); +#endif /* CVC4_PROOF */ +} + vector SmtEngine::getAssertions() throw(ModalException, AssertionException) { if(Dump.isOn("benchmark")) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5d8f31d3c..90593569b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -28,6 +28,7 @@ #include "context/cdset_forward.h" #include "expr/expr.h" #include "expr/expr_manager.h" +#include "util/proof.h" #include "smt/bad_option_exception.h" #include "smt/modal_exception.h" #include "smt/no_such_function_exception.h" @@ -36,7 +37,6 @@ #include "util/result.h" #include "util/sexpr.h" #include "util/stats.h" -#include "proof/proof_manager.h" // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) @@ -318,6 +318,13 @@ public: */ SExpr getAssignment() throw(ModalException, AssertionException); + /** + * Get the last proof (only if immediately preceded by an UNSAT + * or VALID query). Only permitted if CVC4 was built with proof + * support and produce-proofs is on. + */ + Proof* getProof() throw(ModalException, AssertionException); + /** * Get the current set of assertions. Only permitted if the * SmtEngine is set to operate interactively. diff --git a/src/util/Makefile.am b/src/util/Makefile.am index e915fe483..c5a20cd5d 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -28,6 +28,7 @@ libutil_la_SOURCES = \ exception.h \ hash.h \ bool.h \ + proof.h \ options.h \ options.cpp \ output.cpp \ diff --git a/src/util/proof.h b/src/util/proof.h new file mode 100644 index 000000000..be833e33c --- /dev/null +++ b/src/util/proof.h @@ -0,0 +1,36 @@ +/********************* */ +/*! \file proof.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__PROOF_H +#define __CVC4__PROOF_H + +#include + +namespace CVC4 { + +class CVC4_PUBLIC Proof { +public: + virtual void toStream(std::ostream& out) = 0; +};/* class Proof */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__PROOF_H */ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 3a4583805..e564b567a 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -45,6 +45,7 @@ SMT2_TESTS = \ # Regression tests for PL inputs CVC_TESTS = \ + boolean.cvc \ boolean-prec.cvc \ hole6.cvc \ ite.cvc \ diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc index d6f428bdb..2d0eb59b2 100644 --- a/test/regress/regress0/boolean.cvc +++ b/test/regress/regress0/boolean.cvc @@ -804,5 +804,5 @@ a288 : BOOLEAN = ELSE FALSE ENDIF; QUERY a288; -% EXIT: 20 % PROOF +% EXIT: 20 diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc index 31204a6c1..ece29e17c 100644 --- a/test/regress/regress0/hole6.cvc +++ b/test/regress/regress0/hole6.cvc @@ -177,5 +177,5 @@ ASSERT x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37; QUERY FALSE; -% EXIT: 20 % PROOF +% EXIT: 20 diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc index 1aedcbe2b..04c7dafe0 100644 --- a/test/regress/regress0/wiki.05.cvc +++ b/test/regress/regress0/wiki.05.cvc @@ -2,5 +2,5 @@ a, b, c : BOOLEAN; % EXPECT: valid QUERY a OR (a AND b) <=> a; -% EXIT: 20 % PROOF +% EXIT: 20 diff --git a/test/regress/run_regression b/test/regress/run_regression index b836b39f6..6c06175d2 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -52,6 +52,8 @@ function gettemp { tmpbenchmark= if expr "$benchmark" : '.*\.smt$' &>/dev/null; then + proof_command=PROOFS-NOT-SUPPORTED-IN-SMTLIB-V1 + lang=smt if test -e "$benchmark.expect"; then expected_proof=`grep -q '^% PROOF' "$benchmark.expect" && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` @@ -68,9 +70,8 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle - # this frustrates our auto-language-detection, so add explicit --lang + # this frustrates our auto-language-detection gettemp tmpbenchmark cvc4_benchmark.smt.$$.XXXXXXXXXX - command_line="${command_line:+$command_line }--lang=smt" grep -v '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark" if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" @@ -90,6 +91,8 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then error "cannot determine status of \`$benchmark'" fi elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then + proof_command='(get-proof)' + lang=smt2 if test -e "$benchmark.expect"; then expected_proof=`grep -q '^% PROOF' "$benchmark.expect" && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` @@ -106,9 +109,8 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle - # this frustrates our auto-language-detection, so add explicit --lang + # this frustrates our auto-language-detection gettemp tmpbenchmark cvc4_benchmark.smt2.$$.XXXXXXXXXX - command_line="${command_line:+$command_line }--lang=smt2" grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark" if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" @@ -128,6 +130,8 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then error "cannot determine status of \`$benchmark'" fi elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then + proof_command='DUMP_PROOF;' + lang=cvc4 expected_proof=`grep -q '^% PROOF' "$benchmark" && echo yes` expected_output=$(grep '^% EXPECT: ' "$benchmark") expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` @@ -145,6 +149,8 @@ else error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2" fi +command_line="${command_line:+$command_line }--lang=$lang" + gettemp expoutfile cvc4_expect_stdout.$$.XXXXXXXXXX gettemp experrfile cvc4_expect_stderr.$$.XXXXXXXXXX gettemp outfile cvc4_stdout.$$.XXXXXXXXXX @@ -203,19 +209,27 @@ if [ "$exit_status" != "$expected_exit_status" ]; then fi if [ "$proof" = yes -a "$expected_proof" = yes ]; then - echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$benchmark"` [from working dir `dirname "$benchmark"`] - ( cd `dirname "$benchmark"`; - "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$benchmark"`; + gettemp pfbenchmark cvc4_pfbenchmark.$$.XXXXXXXXXX + cp "$benchmark" "$pfbenchmark"; + echo "$proof_command" >>"$pfbenchmark"; + echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`] + ( cd `dirname "$pfbenchmark"`; + "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"`; echo $? >"$exitstatusfile" ) > "$outfile" 2> "$errfile" - if [ ! -s "$outfile" ]; then + 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 "$outfile" [from working dir `dirname "$benchmark"`] - if ! $LFSC "$outfile" &> "$errfile"; then + 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