diff options
Diffstat (limited to 'src/theory/builtin')
| -rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 12 | ||||
| -rw-r--r-- | src/theory/builtin/theory_builtin.h | 6 |
2 files changed, 15 insertions, 3 deletions
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 695d5b91b..f6ce4414e 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -17,6 +17,7 @@ #include "theory/builtin/theory_builtin.h" #include "expr/kind.h" +#include "expr/proof_node_manager.h" #include "theory/builtin/theory_builtin_rewriter.h" #include "theory/theory_model.h" #include "theory/valuation.h" @@ -31,9 +32,16 @@ TheoryBuiltin::TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) - : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, pnm) { + ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; + if (pc != nullptr) + { + // add checkers + d_bProofChecker.registerTo(pc); + } } std::string TheoryBuiltin::identify() const diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index e4767645e..beca0b76a 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -19,6 +19,7 @@ #ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H #define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H +#include "theory/builtin/proof_checker.h" #include "theory/builtin/theory_builtin_rewriter.h" #include "theory/theory.h" @@ -33,7 +34,8 @@ class TheoryBuiltin : public Theory context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo); + const LogicInfo& logicInfo, + ProofNodeManager* pnm = nullptr); TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } @@ -45,6 +47,8 @@ class TheoryBuiltin : public Theory private: /** The theory rewriter for this theory. */ TheoryBuiltinRewriter d_rewriter; + /** Proof rule checker */ + BuiltinProofRuleChecker d_bProofChecker; }; /* class TheoryBuiltin */ } // namespace builtin |