diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-03 14:07:16 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-03 12:07:16 -0700 |
commit | 7f08ae4ec52924110b648381280a07e6a812d09a (patch) | |
tree | ad07f3cd4df2834b323efb75db52131eb76fe054 /test/unit/theory/theory_white.h | |
parent | d972bd973320ed3b4c7a41ff6a16e76f754d7f58 (diff) |
Fix theory white unit test (#5194)
Diffstat (limited to 'test/unit/theory/theory_white.h')
-rw-r--r-- | test/unit/theory/theory_white.h | 30 |
1 files changed, 20 insertions, 10 deletions
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index 707255b05..552aeb3c6 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -100,9 +100,18 @@ class DummyTheory : public Theory { Valuation valuation, const LogicInfo& logicInfo, ProofNodeManager* pnm) - : Theory( - theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, pnm) - {} + : Theory(theory::THEORY_BUILTIN, + ctxt, + uctxt, + out, + valuation, + logicInfo, + pnm), + d_state(ctxt, uctxt, valuation) + { + // use a default theory state object + d_theoryState = &d_state; + } TheoryRewriter* getTheoryRewriter() { return nullptr; } @@ -128,19 +137,20 @@ class DummyTheory : public Theory { return done(); } - void check(Effort e) override - { - while(!done()) { - getWrapper(); - } - } - void presolve() override { Unimplemented(); } void preRegisterTerm(TNode n) override {} void propagate(Effort level) override {} + bool preNotifyFact( + TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) override + { + // do not assert to equality engine, since this theory does not use one + return true; + } TrustNode explain(TNode n) override { return TrustNode::null(); } Node getValue(TNode n) { return Node::null(); } string identify() const override { return "DummyTheory"; } + /** Default theory state object */ + TheoryState d_state; };/* class DummyTheory */ class TheoryBlack : public CxxTest::TestSuite { |