diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-10-29 05:21:49 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-10-29 05:21:49 +0000 |
commit | 02f4f0500849bc719cb45bbc771bea90eb6e96f8 (patch) | |
tree | 6df8a696dba89732dc17d30e80b1d326edf36a5c /src/smt | |
parent | b695ce10f294b2469434656fb2c5dc8e6d701c5d (diff) |
Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::getProof(), a few other things..
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 35 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 9 |
2 files changed, 40 insertions, 4 deletions
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<SExpr> 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<Expr> 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) @@ -319,6 +319,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. */ |