This PR adds infrastructure in SmtEngine and ProofManager for checking and printing proofs. It updates a previous interface that used ProofGenerator in favor of ProofNode.
This makes it so that it only remains to make PropEngine to be proof producing.
return true;
}
+std::shared_ptr<ProofNode> PropEngine::getProof()
+{
+ // TODO (proj #37) implement this
+ return nullptr;
+}
+
}/* CVC4::prop namespace */
}/* CVC4 namespace */
*/
bool properExplanation(TNode node, TNode expl) const;
+ /**
+ * Return the prop engine proof. This should be called only when proofs are
+ * enabled. Returns a proof of false whose free assumptions are the
+ * preprocessed assertions.
+ */
+ std::shared_ptr<ProofNode> getProof();
+
private:
/** Dump out the satisfying assignment (after SAT result) */
void printSatisfyingAssignment();
#include "options/base_options.h"
#include "options/smt_options.h"
#include "smt/assertions.h"
+#include "smt/defined_function.h"
namespace CVC4 {
namespace smt {
PfManager::~PfManager() {}
-void PfManager::setFinalProof(ProofGenerator* pg, context::CDList<Node>* al)
+void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn,
+ Assertions& as,
+ DefinedFunctionMap& df)
{
- Assert(al != nullptr);
// Note this assumes that setFinalProof is only called once per unsat
// response. This method would need to cache its result otherwise.
Trace("smt-proof") << "SmtEngine::setFinalProof(): get proof body...\n";
- // d_finalProof should just be a ProofNode
- std::shared_ptr<ProofNode> body = pg->getProofFor(d_false)->clone();
-
if (Trace.isOn("smt-proof-debug"))
{
Trace("smt-proof-debug")
<< "SmtEngine::setFinalProof(): Proof node for false:\n";
- Trace("smt-proof-debug") << *body.get() << std::endl;
+ Trace("smt-proof-debug") << *pfn.get() << std::endl;
Trace("smt-proof-debug") << "=====" << std::endl;
}
+ std::vector<Node> assertions;
+ getAssertions(as, df, assertions);
+
if (Trace.isOn("smt-proof"))
{
+ Trace("smt-proof") << "SmtEngine::setFinalProof(): get free assumptions..."
+ << std::endl;
std::vector<Node> fassumps;
- expr::getFreeAssumptions(body.get(), fassumps);
+ expr::getFreeAssumptions(pfn.get(), fassumps);
Trace("smt-proof")
<< "SmtEngine::setFinalProof(): initial free assumptions are:\n";
for (const Node& a : fassumps)
{
Trace("smt-proof") << "- " << a << std::endl;
}
- }
- std::vector<Node> assertions;
- Trace("smt-proof") << "SmtEngine::setFinalProof(): assertions are:\n";
- for (context::CDList<Node>::const_iterator i = al->begin(); i != al->end();
- ++i)
- {
- Node n = *i;
- Trace("smt-proof") << "- " << n << std::endl;
- assertions.push_back(n);
+ Trace("smt-proof") << "SmtEngine::setFinalProof(): assertions are:\n";
+ for (const Node& n : assertions)
+ {
+ Trace("smt-proof") << "- " << n << std::endl;
+ }
+ Trace("smt-proof") << "=====" << std::endl;
}
- Trace("smt-proof") << "=====" << std::endl;
Trace("smt-proof") << "SmtEngine::setFinalProof(): postprocess...\n";
Assert(d_pfpp != nullptr);
- d_pfpp->process(body);
+ d_pfpp->process(pfn);
Trace("smt-proof") << "SmtEngine::setFinalProof(): make scope...\n";
// Now make the final scope, which ensures that the only open leaves
// of the proof are the assertions.
- d_finalProof = d_pnm->mkScope(body, assertions);
+ d_finalProof = d_pnm->mkScope(pfn, assertions);
Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n";
}
-void PfManager::printProof(ProofGenerator* pg, Assertions& as)
+void PfManager::printProof(std::shared_ptr<ProofNode> pfn,
+ Assertions& as,
+ DefinedFunctionMap& df)
{
Trace("smt-proof") << "PfManager::printProof: start" << std::endl;
- std::shared_ptr<ProofNode> fp = getFinalProof(pg, as);
+ 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
- // leanPrinter(out, fp.get());
std::ostream& out = *options::out();
out << "(proof\n";
out << *fp;
out << "\n)\n";
}
-void PfManager::checkProof(ProofGenerator* pg, Assertions& as)
+void PfManager::checkProof(std::shared_ptr<ProofNode> pfn,
+ Assertions& as,
+ DefinedFunctionMap& df)
{
Trace("smt-proof") << "PfManager::checkProof: start" << std::endl;
- std::shared_ptr<ProofNode> fp = getFinalProof(pg, as);
- Trace("smt-proof") << "PfManager::checkProof: returned " << *fp.get()
- << std::endl;
+ std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as, df);
+ Trace("smt-proof-debug") << "PfManager::checkProof: returned " << *fp.get()
+ << std::endl;
}
ProofChecker* PfManager::getProofChecker() const { return d_pchecker.get(); }
return d_pppg.get();
}
-std::shared_ptr<ProofNode> PfManager::getFinalProof(ProofGenerator* pg,
- Assertions& as)
+std::shared_ptr<ProofNode> PfManager::getFinalProof(
+ std::shared_ptr<ProofNode> pfn, Assertions& as, DefinedFunctionMap& df)
{
- context::CDList<Node>* al = as.getAssertionList();
- setFinalProof(pg, al);
+ setFinalProof(pfn, as, df);
Assert(d_finalProof);
return d_finalProof;
}
+void PfManager::getAssertions(Assertions& as,
+ DefinedFunctionMap& df,
+ std::vector<Node>& assertions)
+{
+ context::CDList<Node>* al = as.getAssertionList();
+ Assert(al != nullptr);
+ for (context::CDList<Node>::const_iterator i = al->begin(); i != al->end();
+ ++i)
+ {
+ assertions.push_back(*i);
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ for (const std::pair<Node, smt::DefinedFunction>& dfn : df)
+ {
+ Node def = dfn.second.getFormula();
+ const std::vector<Node>& formals = dfn.second.getFormals();
+ if (!formals.empty())
+ {
+ Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, formals);
+ def = nm->mkNode(kind::LAMBDA, bvl, def);
+ }
+ // assume the (possibly higher order) equality
+ Node eq = dfn.first.eqNode(def);
+ assertions.push_back(eq);
+ }
+}
+
} // namespace smt
} // namespace CVC4
#ifndef CVC4__SMT__PROOF_MANAGER_H
#define CVC4__SMT__PROOF_MANAGER_H
+#include "context/cdhashmap.h"
#include "context/cdlist.h"
#include "expr/node.h"
#include "expr/proof_checker.h"
namespace smt {
class Assertions;
+class DefinedFunction;
/**
* This class is responsible for managing the proof output of SmtEngine, as
*/
class PfManager
{
+ /** The type of our internal map of defined functions */
+ using DefinedFunctionMap =
+ context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>;
+
public:
PfManager(context::UserContext* u, SmtEngine* smte);
~PfManager();
/**
* Print the proof on the output channel of the current options in scope.
*
- * The argument pg is the module that can provide a proof for false in the
- * current context.
+ * The argument pfn is the proof for false in the current context.
*
* Throws an assertion failure if pg cannot provide a closed proof with
- * respect to assertions in as.
+ * respect to assertions in as and df. For the latter, entries in the defined
+ * function map correspond to equalities of the form (= f (lambda (...) t)),
+ * which are considered assertions in the final proof.
*/
- void printProof(ProofGenerator* pg, Assertions& as);
+ void printProof(std::shared_ptr<ProofNode> pfn,
+ Assertions& as,
+ DefinedFunctionMap& df);
/**
* Check proof, same as above, without printing.
*/
- void checkProof(ProofGenerator* pg, Assertions& as);
+ void checkProof(std::shared_ptr<ProofNode> pfn,
+ Assertions& as,
+ DefinedFunctionMap& df);
/**
* Get final proof.
*
- * The argument pg is the module that can provide a proof for false in the
- * current context.
+ * The argument pfn is the proof for false in the current context.
*/
- std::shared_ptr<ProofNode> getFinalProof(ProofGenerator* pg, Assertions& as);
+ std::shared_ptr<ProofNode> getFinalProof(std::shared_ptr<ProofNode> pfn,
+ Assertions& as,
+ DefinedFunctionMap& df);
//--------------------------- access to utilities
/** Get a pointer to the ProofChecker owned by this. */
ProofChecker* getProofChecker() const;
//--------------------------- end access to utilities
private:
/**
- * Set final proof, which initializes d_finalProof to the proof of false
- * from pg, postprocesses it, and stores it in d_finalProof.
+ * Set final proof, which initializes d_finalProof to the given proof node of
+ * false, postprocesses it, and stores it in d_finalProof.
+ */
+ void setFinalProof(std::shared_ptr<ProofNode> pfn,
+ Assertions& as,
+ DefinedFunctionMap& df);
+ /**
+ * Get assertions from the assertions
*/
- void setFinalProof(ProofGenerator* pg, context::CDList<Node>* al);
+ void getAssertions(Assertions& as,
+ DefinedFunctionMap& df,
+ std::vector<Node>& assertions);
/** The false node */
Node d_false;
/** For the new proofs module */
#ifdef CVC4_PROOF
d_proofManager.reset(nullptr);
#endif
+ d_rewriter.reset(nullptr);
+ d_pfManager.reset(nullptr);
d_absValues.reset(nullptr);
d_asserts.reset(nullptr);
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)
checkModel();
}
}
+ // Check that UNSAT results generate a proof correctly.
+ if (options::checkProofsNew() || options::proofNewEagerChecking())
+ {
+ if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ {
+ if ((options::checkProofsNew() || options::proofNewEagerChecking())
+ && !options::proofNew())
+ {
+ throw ModalException(
+ "Cannot check-proofs-new because proof-new was disabled.");
+ }
+ checkProof();
+ }
+ }
// Check that UNSAT results generate an unsat core correctly.
if(options::checkUnsatCores()) {
if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
+void SmtEngine::checkProof()
+{
+ Assert(options::proofNew());
+ // internal check the proof
+ PropEngine* pe = getPropEngine();
+ Assert(pe != nullptr);
+ Assert(pe->getProof() != nullptr);
+ std::shared_ptr<ProofNode> pePfn = pe->getProof();
+ if (options ::checkProofsNew())
+ {
+ d_pfManager->checkProof(pePfn, *d_asserts, *d_definedFunctions);
+ }
+}
+
UnsatCore SmtEngine::getUnsatCoreInternal()
{
#if IS_PROOFS_BUILD
return getUnsatCoreInternal();
}
+void SmtEngine::printProof()
+{
+ if (d_pfManager == nullptr)
+ {
+ throw RecoverableModalException("Cannot print proof, no proof manager.");
+ }
+ if (getSmtMode() != SmtMode::UNSAT)
+ {
+ throw RecoverableModalException(
+ "Cannot print proof unless immediately preceded by "
+ "UNSAT/ENTAILED.");
+ }
+ 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);
+}
+
void SmtEngine::printInstantiations( std::ostream& out ) {
SmtScope smts(this);
finishInit();
// push the state to maintain global context around everything
d_state->setup();
+ // reset SmtSolver, which will construct a new prop engine
d_smtSolver->resetAssertions();
}
/** Print all instantiations made by the quantifiers module. */
void printInstantiations(std::ostream& out);
-
+ /**
+ * Print the current proof. This method should be called after an UNSAT
+ * response. It gets the proof of false from the PropEngine and passes
+ * it to the ProofManager, which post-processes the proof and prints it
+ * in the proper format.
+ */
+ void printProof();
/**
* Print solution for synthesis conjectures found by counter-example guided
* instantiation module.
/** Set solver instance that owns this SmtEngine. */
void setSolver(api::Solver* solver) { d_solver = solver; }
+ /** Get a pointer to the (new) PfManager owned by this SmtEngine. */
+ smt::PfManager* getPfManager() { return d_pfManager.get(); };
+
/** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */
StatisticsRegistry* getStatisticsRegistry()
{
*/
UnsatCore getUnsatCoreInternal();
+ /**
+ * Check that a generated proof checks. This method is the same as printProof,
+ * but does not print the proof. Like that method, it should be called
+ * after an UNSAT response. It ensures that a well-formed proof of false
+ * can be constructed by the combination of the PropEngine and ProofManager.
+ */
+ void checkProof();
+
/**
* Check that an unsatisfiable core is indeed unsatisfiable.
*/
projects / cvc5.git / commitdiff