From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 3 Oct 2020 19:07:16 +0000 (-0500)
Subject: Fix theory white unit test (#5194)
X-Git-Tag: cvc5-1.0.0~2760
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7f08ae4ec52924110b648381280a07e6a812d09a;p=cvc5.git

Fix theory white unit test (#5194)
---

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 {