This module is responsible for constructing the proof checker, proof node manager, and implementing dumping and checking of the final proof.
This PR includes setting up some connections into the various modules for proof production.
smt/preprocess_proof_generator.h
smt/process_assertions.cpp
smt/process_assertions.h
+ smt/proof_manager.cpp
+ smt/proof_manager.h
smt/proof_post_processor.cpp
smt/proof_post_processor.h
smt/set_defaults.cpp
read_only = true
help = "check proofs eagerly with proof-new for local debugging"
+[[option]]
+ name = "proofGranularityMode"
+ category = "regular"
+ long = "proof-granularity=MODE"
+ type = "ProofGranularityMode"
+ default = "THEORY_REWRITE"
+ help = "modes for proof granularity"
+ help_mode = "Modes for proof granularity."
+[[option.mode.OFF]]
+ name = "off"
+ help = "Do not improve the granularity of proofs."
+[[option.mode.REWRITE]]
+ name = "rewrite"
+ help = "allow rewrite or substitution steps, expand macros."
+[[option.mode.THEORY_REWRITE]]
+ name = "theory-rewrite"
+ help = "allow theory rewrite steps, expand macros, rewrite and substitution steps."
+[[option.mode.DSL_REWRITE]]
+ name = "dsl-rewrite"
+ help = "Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory rewrite steps."
+
+[[option]]
+ name = "checkProofsNew"
+ category = "regular"
+ long = "check-proofs-new"
+ type = "bool"
+ help = "after UNSAT/VALID, check the generated proof (with proof-new)"
+
[[option]]
name = "dumpInstantiations"
category = "regular"
{
Assert(trn.getKind() == theory::TrustNodeKind::LEMMA);
// push back what was proven
- push_back(trn.getProven(), false, trn.getGenerator());
+ push_back(trn.getProven(), false, false, trn.getGenerator());
}
void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
}
// Add the normalized formula to the queue
- d_assertions.push_back(n, isAssumption);
+ d_assertions.push_back(n, isAssumption, true);
}
void Assertions::addDefineFunRecDefinition(Node n, bool global)
}
}
+void Assertions::setProofGenerator(smt::PreprocessProofGenerator* pppg)
+{
+ d_assertions.setProofGenerator(pppg);
+}
+
+bool Assertions::isProofEnabled() const
+{
+ return d_assertions.isProofEnabled();
+}
+
} // namespace smt
} // namespace CVC4
/** Flip the global negation flag. */
void flipGlobalNegated();
+ //------------------------------------ for proofs
+ /** Set proof generator */
+ void setProofGenerator(smt::PreprocessProofGenerator* pppg);
+ /** Is proof enabled? */
+ bool isProofEnabled() const;
+ //------------------------------------ end for proofs
private:
/**
* Fully type-check the argument, and also type-check that it's
--- /dev/null
+/********************* */
+/*! \file proof_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The proof manager of the SMT engine
+ **/
+
+#include "smt/proof_manager.h"
+
+#include "expr/proof_node_algorithm.h"
+#include "options/base_options.h"
+#include "options/smt_options.h"
+#include "smt/assertions.h"
+
+namespace CVC4 {
+namespace smt {
+
+PfManager::PfManager(SmtEngine* smte)
+ : d_pchecker(new ProofChecker(options::proofNewPedantic())),
+ d_pnm(new ProofNodeManager(d_pchecker.get())),
+ d_pppg(new PreprocessProofGenerator(d_pnm.get())),
+ d_pfpp(new ProofPostproccess(d_pnm.get(), smte, d_pppg.get())),
+ d_finalProof(nullptr)
+{
+ // add rules to eliminate here
+ if (options::proofGranularityMode() != options::ProofGranularityMode::OFF)
+ {
+ d_pfpp->setEliminateRule(PfRule::MACRO_SR_EQ_INTRO);
+ d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_INTRO);
+ d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_ELIM);
+ d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_TRANSFORM);
+ if (options::proofGranularityMode()
+ != options::ProofGranularityMode::REWRITE)
+ {
+ d_pfpp->setEliminateRule(PfRule::SUBS);
+ d_pfpp->setEliminateRule(PfRule::REWRITE);
+ if (options::proofGranularityMode()
+ != options::ProofGranularityMode::THEORY_REWRITE)
+ {
+ // this eliminates theory rewriting steps with finer-grained DSL rules
+ d_pfpp->setEliminateRule(PfRule::THEORY_REWRITE);
+ }
+ }
+ }
+ d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+PfManager::~PfManager() {}
+
+void PfManager::setFinalProof(ProofGenerator* pg, context::CDList<Node>* al)
+{
+ 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") << "=====" << std::endl;
+ }
+
+ if (Trace.isOn("smt-proof"))
+ {
+ std::vector<Node> fassumps;
+ expr::getFreeAssumptions(body.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") << "=====" << std::endl;
+
+ Trace("smt-proof") << "SmtEngine::setFinalProof(): postprocess...\n";
+ Assert(d_pfpp != nullptr);
+ d_pfpp->process(body);
+
+ 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);
+ Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n";
+}
+
+void PfManager::printProof(ProofGenerator* pg, Assertions& as)
+{
+ Trace("smt-proof") << "PfManager::printProof: start" << std::endl;
+ std::shared_ptr<ProofNode> fp = getFinalProof(pg, as);
+ // 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)
+{
+ 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;
+}
+
+ProofChecker* PfManager::getProofChecker() const { return d_pchecker.get(); }
+
+ProofNodeManager* PfManager::getProofNodeManager() const { return d_pnm.get(); }
+
+smt::PreprocessProofGenerator* PfManager::getPreprocessProofGenerator() const
+{
+ return d_pppg.get();
+}
+
+std::shared_ptr<ProofNode> PfManager::getFinalProof(ProofGenerator* pg,
+ Assertions& as)
+{
+ context::CDList<Node>* al = as.getAssertionList();
+ setFinalProof(pg, al);
+ Assert(d_finalProof);
+ return d_finalProof;
+}
+
+} // namespace smt
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file proof_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The proof manager of SmtEngine
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__PROOF_MANAGER_H
+#define CVC4__SMT__PROOF_MANAGER_H
+
+#include "context/cdlist.h"
+#include "expr/expr.h"
+#include "expr/node.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+#include "expr/proof_node_manager.h"
+#include "smt/preprocess_proof_generator.h"
+#include "smt/proof_post_processor.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+
+namespace smt {
+
+class Assertions;
+
+/**
+ * This class is responsible for managing the proof output of SmtEngine, as
+ * well as setting up the global proof checker and proof node manager.
+ */
+class PfManager
+{
+ public:
+ PfManager(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.
+ *
+ * Throws an assertion failure if pg cannot provide a closed proof with
+ * respect to assertions in as.
+ */
+ void printProof(ProofGenerator* pg, Assertions& as);
+ /**
+ * Check proof, same as above, without printing.
+ */
+ void checkProof(ProofGenerator* pg, Assertions& as);
+
+ /**
+ * Get final proof.
+ *
+ * The argument pg is the module that can provide a proof for false in the
+ * current context.
+ */
+ std::shared_ptr<ProofNode> getFinalProof(ProofGenerator* pg, Assertions& as);
+ //--------------------------- access to utilities
+ /** Get a pointer to the ProofChecker owned by this. */
+ ProofChecker* getProofChecker() const;
+ /** Get a pointer to the ProofNodeManager owned by this. */
+ ProofNodeManager* getProofNodeManager() const;
+ /** Get the proof generator for proofs of preprocessing. */
+ smt::PreprocessProofGenerator* getPreprocessProofGenerator() 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.
+ */
+ void setFinalProof(ProofGenerator* pg, context::CDList<Node>* al);
+ /** The false node */
+ Node d_false;
+ /** For the new proofs module */
+ std::unique_ptr<ProofChecker> d_pchecker;
+ /** A proof node manager based on the above checker */
+ std::unique_ptr<ProofNodeManager> d_pnm;
+ /** The preprocess proof generator. */
+ std::unique_ptr<smt::PreprocessProofGenerator> d_pppg;
+ /** The proof post-processor */
+ std::unique_ptr<smt::ProofPostproccess> d_pfpp;
+ /**
+ * The final proof produced by the SMT engine.
+ * Combines the proofs of preprocessing, prop engine and theory engine, to be
+ * connected by setFinalProof().
+ */
+ std::shared_ptr<ProofNode> d_finalProof;
+}; /* class SmtEngine */
+
+} // namespace smt
+} // namespace CVC4
+
+#endif /* CVC4__SMT__PROOF_MANAGER_H */
#include "expr/node_builder.h"
#include "expr/node_self_iterator.h"
#include "expr/node_visitor.h"
-#include "options/arith_options.h"
-#include "options/arrays_options.h"
#include "options/base_options.h"
-#include "options/booleans_options.h"
-#include "options/bv_options.h"
-#include "options/datatypes_options.h"
#include "options/decision_options.h"
#include "options/language.h"
#include "options/main_options.h"
#include "options/printer_options.h"
#include "options/prop_options.h"
#include "options/quantifiers_options.h"
-#include "options/sep_options.h"
#include "options/set_language.h"
#include "options/smt_options.h"
-#include "options/strings_options.h"
#include "options/theory_options.h"
-#include "options/uf_options.h"
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "preprocessing/preprocessing_pass_registry.h"
#include "smt/model_core_builder.h"
#include "smt/options_manager.h"
#include "smt/preprocessor.h"
+#include "smt/proof_manager.h"
#include "smt/quant_elim_solver.h"
#include "smt/smt_engine_scope.h"
#include "smt/smt_engine_state.h"
#include "smt/update_ostream.h"
#include "smt_util/boolean_simplification.h"
#include "smt_util/nary_builder.h"
-#include "theory/booleans/circuit_propagator.h"
-#include "theory/bv/theory_bv_rewriter.h"
#include "theory/logic_info.h"
#include "theory/rewriter.h"
#include "theory/sort_inference.h"
-#include "theory/strings/theory_strings.h"
#include "theory/substitutions.h"
#include "theory/theory_engine.h"
#include "theory/theory_model.h"
d_snmListener(new SmtNodeManagerListener(*d_dumpm.get())),
d_smtSolver(nullptr),
d_proofManager(nullptr),
+ d_pfManager(nullptr),
d_rewriter(new theory::Rewriter()),
d_definedFunctions(nullptr),
d_sygusSolver(nullptr),
// based on our heuristics.
d_optm->finishInit(d_logic, d_isInternalSubsolver);
+ ProofNodeManager* pnm = nullptr;
+ if (options::proofNew())
+ {
+ d_pfManager.reset(new PfManager(this));
+ // use this proof node manager
+ pnm = d_pfManager->getProofNodeManager();
+ // enable proof support in the rewriter
+ d_rewriter->setProofNodeManager(pnm);
+ // enable it in the assertions pipeline
+ d_asserts->setProofGenerator(d_pfManager->getPreprocessProofGenerator());
+ // enable it in the SmtSolver
+ d_smtSolver->setProofNodeManager(pnm);
+ }
+
Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
d_smtSolver->finishInit(const_cast<const LogicInfo&>(d_logic));
struct SmtEngineStatistics;
class SmtScope;
class ProcessAssertions;
+class PfManager;
ProofManager* currentProofManager();
}/* CVC4::smt namespace */
/** Get a pointer to the PropEngine owned by this SmtEngine. */
prop::PropEngine* getPropEngine();
- /** Get a pointer to the ProofManager owned by this SmtEngine. */
+ /**
+ * Get a pointer to the ProofManager owned by this SmtEngine.
+ * TODO (project #37): this is the old proof manager and will be deleted
+ */
ProofManager* getProofManager() { return d_proofManager.get(); };
/** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */
/** The SMT solver */
std::unique_ptr<smt::SmtSolver> d_smtSolver;
- /** The proof manager */
+ /** The (old) proof manager TODO (project #37): delete this */
std::unique_ptr<ProofManager> d_proofManager;
+ /**
+ * The proof manager, which manages all things related to checking,
+ * processing, and printing proofs.
+ */
+ std::unique_ptr<smt::PfManager> d_pfManager;
+
/**
* The rewriter associated with this SmtEngine. We have a different instance
* of the rewriter for each SmtEngine instance. This is because rewriters may
d_rm(rm),
d_pp(pp),
d_stats(stats),
+ d_pnm(nullptr),
d_theoryEngine(nullptr),
d_propEngine(nullptr)
{
as.clearCurrent();
}
+void SmtSolver::setProofNodeManager(ProofNodeManager* pnm) { d_pnm = pnm; }
+
TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); }
prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); }
class SmtEngine;
class TheoryEngine;
class ResourceManager;
+class ProofNodeManager;
namespace prop {
class PropEngine;
* into the SMT solver, and clears the buffer.
*/
void processAssertions(Assertions& as);
+ /**
+ * Set proof node manager. Enables proofs in this SmtSolver. Should be
+ * called before finishInit.
+ */
+ void setProofNodeManager(ProofNodeManager* pnm);
//------------------------------------------ access methods
/** Get a pointer to the TheoryEngine owned by this solver. */
TheoryEngine* getTheoryEngine();
Preprocessor& d_pp;
/** Reference to the statistics of SmtEngine */
SmtEngineStatistics& d_stats;
+ /**
+ * Pointer to the proof node manager used by this SmtSolver. A non-null
+ * proof node manager indicates that proofs are enabled.
+ */
+ ProofNodeManager* d_pnm;
/** The theory engine */
std::unique_ptr<TheoryEngine> d_theoryEngine;
/** The propositional engine */
projects / cvc5.git / commitdiff