diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/options/smt_options.toml | 28 | ||||
| -rw-r--r-- | src/preprocessing/assertion_pipeline.cpp | 2 | ||||
| -rw-r--r-- | src/smt/assertions.cpp | 12 | ||||
| -rw-r--r-- | src/smt/assertions.h | 6 | ||||
| -rw-r--r-- | src/smt/proof_manager.cpp | 150 | ||||
| -rw-r--r-- | src/smt/proof_manager.h | 103 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 27 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 14 | ||||
| -rw-r--r-- | src/smt/smt_solver.cpp | 3 | ||||
| -rw-r--r-- | src/smt/smt_solver.h | 11 |
11 files changed, 343 insertions, 15 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index a7c50d1e4..65ccabd89 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -222,6 +222,8 @@ libcvc4_add_sources( 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 diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 2c87158de..4e1a89259 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -174,6 +174,34 @@ header = "options/smt_options.h" 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" long = "dump-instantiations" diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index a9e2d4d36..735a93f56 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -72,7 +72,7 @@ void AssertionPipeline::pushBackTrusted(theory::TrustNode trn) { 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) diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 8019c383d..714622bae 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -197,7 +197,7 @@ void Assertions::addFormula( } // 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) @@ -234,5 +234,15 @@ void Assertions::ensureBoolean(const Node& n) } } +void Assertions::setProofGenerator(smt::PreprocessProofGenerator* pppg) +{ + d_assertions.setProofGenerator(pppg); +} + +bool Assertions::isProofEnabled() const +{ + return d_assertions.isProofEnabled(); +} + } // namespace smt } // namespace CVC4 diff --git a/src/smt/assertions.h b/src/smt/assertions.h index a74c58bd8..a73cd32d6 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -109,6 +109,12 @@ class Assertions /** 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 diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp new file mode 100644 index 000000000..b78bb771a --- /dev/null +++ b/src/smt/proof_manager.cpp @@ -0,0 +1,150 @@ +/********************* */ +/*! \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 diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h new file mode 100644 index 000000000..925d9fa02 --- /dev/null +++ b/src/smt/proof_manager.h @@ -0,0 +1,103 @@ +/********************* */ +/*! \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 */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 81d4f594d..7f824bff3 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -50,12 +50,7 @@ #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" @@ -64,12 +59,9 @@ #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" @@ -89,6 +81,7 @@ #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" @@ -99,12 +92,9 @@ #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" @@ -139,6 +129,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) 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), @@ -262,6 +253,20 @@ void SmtEngine::finishInit() // 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)); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5ef8b63c6..e95e36c3d 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -117,6 +117,7 @@ class DefinedFunction; struct SmtEngineStatistics; class SmtScope; class ProcessAssertions; +class PfManager; ProofManager* currentProofManager(); }/* CVC4::smt namespace */ @@ -900,7 +901,10 @@ class CVC4_PUBLIC SmtEngine /** 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. */ @@ -1072,10 +1076,16 @@ class CVC4_PUBLIC 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 * hold references to objects that belong to theory solvers, which are diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 706c18416..c64689be6 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -35,6 +35,7 @@ SmtSolver::SmtSolver(SmtEngine& smt, d_rm(rm), d_pp(pp), d_stats(stats), + d_pnm(nullptr), d_theoryEngine(nullptr), d_propEngine(nullptr) { @@ -245,6 +246,8 @@ void SmtSolver::processAssertions(Assertions& as) 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(); } diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index 8d0644800..07d81f92b 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -28,6 +28,7 @@ namespace CVC4 { class SmtEngine; class TheoryEngine; class ResourceManager; +class ProofNodeManager; namespace prop { class PropEngine; @@ -108,6 +109,11 @@ class SmtSolver * 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(); @@ -125,6 +131,11 @@ class SmtSolver 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 */ |