summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/cvc4cpp.cpp2
-rw-r--r--src/smt/command.cpp26
-rw-r--r--src/smt/command.h7
-rw-r--r--src/smt/proof_manager.cpp4
-rw-r--r--src/smt/proof_manager.h5
-rw-r--r--src/smt/smt_engine.cpp37
-rw-r--r--src/smt/smt_engine.h6
7 files changed, 67 insertions, 20 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 49974d30d..621e3c1c0 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2473,7 +2473,7 @@ Term DatatypeConstructor::getSpecializedConstructorTerm(Sort retSort) const
<< "Cannot get specialized constructor type for non-datatype type "
<< retSort;
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-
+
NodeManager* nm = d_solver->getNodeManager();
Node ret =
nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index f3b0ee915..0c8accf7a 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1886,7 +1886,31 @@ void BlockModelValuesCommand::toStream(std::ostream& out,
GetProofCommand::GetProofCommand() {}
void GetProofCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
- Unimplemented() << "Unimplemented get-proof\n";
+ try
+ {
+ d_result = solver->getSmtEngine()->getProof();
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (api::CVC4ApiRecoverableException& e)
+ {
+ d_commandStatus = new CommandRecoverableFailure(e.what());
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (ok())
+ {
+ out << d_result;
+ }
+ else
+ {
+ this->Command::printResult(out, verbosity);
+ }
}
Command* GetProofCommand::clone() const
diff --git a/src/smt/command.h b/src/smt/command.h
index 399050d94..9330f2015 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1015,6 +1015,9 @@ class CVC4_PUBLIC GetProofCommand : public Command
GetProofCommand();
void invoke(api::Solver* solver, SymbolManager* sm) override;
+
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1022,6 +1025,10 @@ class CVC4_PUBLIC GetProofCommand : public Command
int toDepth = -1,
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
+
+ private:
+ /** the result of the getProof call */
+ std::string d_result;
}; /* class GetProofCommand */
class CVC4_PUBLIC GetInstantiationsCommand : public Command
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index ce9b4923c..d82e22736 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -108,7 +108,8 @@ void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn,
Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n";
}
-void PfManager::printProof(std::shared_ptr<ProofNode> pfn,
+void PfManager::printProof(std::ostream& out,
+ std::shared_ptr<ProofNode> pfn,
Assertions& as,
DefinedFunctionMap& df)
{
@@ -116,7 +117,6 @@ void PfManager::printProof(std::shared_ptr<ProofNode> pfn,
std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as, df);
// TODO (proj #37) according to the proof format, post process the proof node
// TODO (proj #37) according to the proof format, print the proof node
- std::ostream& out = *options::out();
out << "(proof\n";
out << *fp;
out << "\n)\n";
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index be05fc2f7..a6f284cad 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -49,7 +49,7 @@ class PfManager
PfManager(context::UserContext* u, SmtEngine* smte);
~PfManager();
/**
- * Print the proof on the output channel of the current options in scope.
+ * Print the proof on the given output stream.
*
* The argument pfn is the proof for false in the current context.
*
@@ -58,7 +58,8 @@ class PfManager
* function map correspond to equalities of the form (= f (lambda (...) t)),
* which are considered assertions in the final proof.
*/
- void printProof(std::shared_ptr<ProofNode> pfn,
+ void printProof(std::ostream& out,
+ std::shared_ptr<ProofNode> pfn,
Assertions& as,
DefinedFunctionMap& df);
/**
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4c47587a6..d89b6e802 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -953,12 +953,6 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat")
<< "(" << assumptions << ") => " << r << endl;
- if (options::dumpProofs() && options::proofNew()
- && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
- {
- printProof();
- }
-
// Check that SAT results generate a model correctly.
if(options::checkModels()) {
if (r.asSatisfiabilityResult().isSat() == Result::SAT)
@@ -1496,23 +1490,38 @@ UnsatCore SmtEngine::getUnsatCore() {
return getUnsatCoreInternal();
}
-void SmtEngine::printProof()
+std::string SmtEngine::getProof()
{
- if (d_pfManager == nullptr)
+ Trace("smt") << "SMT getProof()\n";
+ SmtScope smts(this);
+ finishInit();
+ if (Dump.isOn("benchmark"))
{
- throw RecoverableModalException("Cannot print proof, no proof manager.");
+ getOutputManager().getPrinter().toStreamCmdGetProof(
+ getOutputManager().getDumpOut());
}
- if (getSmtMode() != SmtMode::UNSAT)
+#if IS_PROOFS_BUILD
+ if (!options::proofNew())
+ {
+ throw ModalException("Cannot get a proof when proof-new option is off.");
+ }
+ if (d_state->getMode() != SmtMode::UNSAT)
{
throw RecoverableModalException(
- "Cannot print proof unless immediately preceded by "
- "UNSAT/ENTAILED.");
+ "Cannot get a proof unless immediately preceded by "
+ "UNSAT/ENTAILED response.");
}
+ // the prop engine has the proof of false
PropEngine* pe = getPropEngine();
Assert(pe != nullptr);
Assert(pe->getProof() != nullptr);
- // the prop engine has the proof of false
- d_pfManager->printProof(pe->getProof(), *d_asserts, *d_definedFunctions);
+ Assert(d_pfManager);
+ std::ostringstream ss;
+ d_pfManager->printProof(ss, pe->getProof(), *d_asserts, *d_definedFunctions);
+ return ss.str();
+#else /* IS_PROOFS_BUILD */
+ throw ModalException("This build of CVC4 doesn't have proof support.");
+#endif /* IS_PROOFS_BUILD */
}
void SmtEngine::printInstantiations( std::ostream& out ) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 091f69642..558bd2b40 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -684,6 +684,12 @@ class CVC4_PUBLIC SmtEngine
UnsatCore getUnsatCore();
/**
+ * Get a refutation proof (only if immediately preceded by an UNSAT or
+ * ENTAILED query). Only permitted if CVC4 was built with proof support and
+ * the proof option is on. */
+ std::string getProof();
+
+ /**
* Get the current set of assertions. Only permitted if the
* SmtEngine is set to operate interactively.
*/
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback