Make ExtTheory a utility and not a member of Theory (#4753)

Previously, we assumed that ExtTheory, the module for doing context-dependent simplification, was one-to-one with Theory. This design is not necessary. This makes this class a utility, which can be used as needed. This makes e.g. the initialization of TheoryStrings much easier, since the ExtTheory object can be created first.

1 files changed, 6 insertions, 2 deletions

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index c98de0f18..b0991c8b0 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -38,10 +38,11 @@ namespace CVC4 {
 namespace proof {
 class BitVectorProof;
 }
-}  // namespace CVC4
 
-namespace CVC4 {
 namespace theory {
+
+class ExtTheory;
+
 namespace bv {
 
 class CoreSolver;
@@ -180,6 +181,9 @@ class TheoryBV : public Theory {
   /** Index of the next literal to propagate */
   context::CDO<unsigned> d_literalsToPropagateIndex;
 
+  /** Extended theory module, for context-dependent simplification. */
+  std::unique_ptr<ExtTheory> d_extTheory;
+
   /**
    * Keeps a map from nodes to the subtheory that propagated it so that we can explain it
    * properly.