diff options
Diffstat (limited to 'src/theory/builtin/theory_builtin.cpp')
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index bd0374675..c2d9520d5 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -22,8 +22,6 @@ #include "theory/theory_model.h" #include "theory/valuation.h" -using namespace std; - namespace cvc5 { namespace theory { namespace builtin { @@ -36,14 +34,12 @@ TheoryBuiltin::TheoryBuiltin(context::Context* c, 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); - } } +TheoryRewriter* TheoryBuiltin::getTheoryRewriter() { return &d_rewriter; } + +ProofRuleChecker* TheoryBuiltin::getProofChecker() { return &d_checker; } + std::string TheoryBuiltin::identify() const { return std::string("TheoryBuiltin"); |