Add TheoryState objects to each Theory (#4920)

This initializes all theories with a TheoryState object (apart from bool and builtin which do not require one).

Two additional theories are known to require special state objects: TheoryArith, which has a custom way of detecting when in conflict, and TheoryQuantifiers, which can leverage a special state object for the purposes of refactoring and splitting apart QuantifiersEngine further. All other theories use default TheoryState objects.

Notice this PR does not update the theories to use these states yet, it simply adds the objects.

2 files changed, 6 insertions, 1 deletions

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 7bca9da74..c8ae3d844 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -56,7 +56,8 @@ TheoryUF::TheoryUF(context::Context* c,
       d_ho(nullptr),
       d_conflict(c, false),
       d_functionsTerms(c),
-      d_symb(u, instanceName)
+      d_symb(u, instanceName),
+      d_state(c, u, valuation)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
 
@@ -65,6 +66,8 @@ TheoryUF::TheoryUF(context::Context* c,
   {
     d_ufProofChecker.registerTo(pc);
   }
+  // indicate we are using the default theory state object
+  d_theoryState = &d_state;
 }
 
 TheoryUF::~TheoryUF() {
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 414a2dd6a..4d0a3126f 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -219,6 +219,8 @@ private:
   TheoryUfRewriter d_rewriter;
   /** Proof rule checker */
   UfProofRuleChecker d_ufProofChecker;
+  /** A (default) theory state object */
+  TheoryState d_state;
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */