diff options
Diffstat (limited to 'src/theory/booleans/theory_bool.cpp')
| -rw-r--r-- | src/theory/booleans/theory_bool.cpp | 28 |
1 files changed, 10 insertions, 18 deletions
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 04a1675a4..022249808 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -19,6 +19,7 @@ #include <stack> #include <vector> +#include "expr/proof_node_manager.h" #include "smt_util/boolean_simplification.h" #include "theory/booleans/circuit_propagator.h" #include "theory/booleans/theory_bool_rewriter.h" @@ -37,9 +38,16 @@ TheoryBool::TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) - : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo) + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, pnm) { + ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; + if (pc != nullptr) + { + // add checkers + d_bProofChecker.registerTo(pc); + } } Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { @@ -67,22 +75,6 @@ Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubsti return Theory::ppAssert(in, outSubstitutions); } -/* -void TheoryBool::check(Effort level) { - if (done() && !fullEffort(level)) { - return; - } - while (!done()) - { - // Get all the assertions - Assertion assertion = get(); - TNode fact = assertion.assertion; - } - if( Theory::fullEffort(level) ){ - } -} -*/ - }/* CVC4::theory::booleans namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |