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_solver.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_solver.cpp')
-rw-r--r-- | src/smt/smt_solver.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
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(); } |