diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-11 22:38:04 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-11 22:38:04 -0500 |
| commit | 3a8a27994584ca2168ef71d5eb0ce46ef558ba34 (patch) | |
| tree | efa67475c597a8fdb6664a67dd80e7b022919bd2 /src/smt/smt_engine.cpp | |
| parent | 383d061be2bc8162d3379c98ad106555d21e5f86 (diff) | |
(proof-new) Add SMT proof manager (#5054)
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.
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 27 |
1 files changed, 16 insertions, 11 deletions
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)); |