Add interface to TheoryState for sort inference and facts (#5967)

This eliminates the need for direct references to TheoryEngine from quantifiers and UF+cardinality.

This PR also eliminates an unnecessary reference to TheoryEngine in TheoryModelBuilder and breaks a few more dependencies in quantifiers modules.

1 files changed, 5 insertions, 1 deletions

diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index dce515d0d..9d4a414e9 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -28,6 +28,7 @@ namespace CVC4 {
 namespace theory {
 
 class RepSetIterator;
+class DecisionManager;
 
 /**
  * Attribute set to 1 for literals that comprise the bounds of a quantified
@@ -164,7 +165,8 @@ private:
   BoundedIntegers(QuantifiersEngine* qe,
                   QuantifiersState& qs,
                   QuantifiersInferenceManager& qim,
-                  QuantifiersRegistry& qr);
+                  QuantifiersRegistry& qr,
+                  DecisionManager* dm);
   virtual ~BoundedIntegers();
 
   void presolve() override;
@@ -231,6 +233,8 @@ private:
   Node matchBoundVar( Node v, Node t, Node e );
   
   bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi );
+  /** Pointer to the decision manager */
+  DecisionManager* d_dm;
 };
 
 }