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.

2 files changed, 12 insertions, 27 deletions

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index aa73e3419..94402e2d9 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -740,7 +740,7 @@ void SortModel::check(Theory::Effort level)
   Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl;
   Trace("uf-ss-si") << "Must combine region" << std::endl;
   bool recheck = false;
-  SortInference* si = d_thss->getSortInference();
+  SortInference* si = d_state.getSortInference();
   if (si != nullptr)
   {
     // If sort inference is enabled, search for regions with same sort.
@@ -1021,14 +1021,18 @@ int SortModel::addSplit(Region* r)
         AlwaysAssert(false);
       }
     }
-    SortInference* si = d_thss->getSortInference();
-    if (si != nullptr)
+    if (Trace.isOn("uf-ss-split-si"))
     {
-      for( int i=0; i<2; i++ ){
-        int sid = si->getSortId(ss[i]);
-        Trace("uf-ss-split-si") << sid << " ";
+      SortInference* si = d_state.getSortInference();
+      if (si != nullptr)
+      {
+        for (size_t i = 0; i < 2; i++)
+        {
+          int sid = si->getSortId(ss[i]);
+          Trace("uf-ss-split-si") << sid << " ";
+        }
+        Trace("uf-ss-split-si") << std::endl;
       }
-      Trace("uf-ss-split-si")  << std::endl;
     }
     //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
     //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
@@ -1247,20 +1251,6 @@ CardinalityExtension::~CardinalityExtension()
   }
 }
 
-SortInference* CardinalityExtension::getSortInference()
-{
-  if (!options::sortInference())
-  {
-    return nullptr;
-  }
-  QuantifiersEngine* qe = d_th->getQuantifiersEngine();
-  if (qe != nullptr)
-  {
-    return qe->getTheoryEngine()->getSortInference();
-  }
-  return nullptr;
-}
-
 /** ensure eqc */
 void CardinalityExtension::ensureEqc(SortModel* c, Node a)
 {
@@ -1351,12 +1341,12 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
       Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl;
       if( lit[0]==ct ){
         if( options::ufssFairnessMonotone() ){
+          SortInference* si = d_state.getSortInference();
           Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl;
           if( tn!=d_tn_mono_master ){
             std::map< TypeNode, bool >::iterator it = d_tn_mono_slave.find( tn );
             if( it==d_tn_mono_slave.end() ){
               bool isMonotonic;
-              SortInference* si = getSortInference();
               if (si != nullptr)
               {
                 isMonotonic = si->isMonotonic(tn);
diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index 6b5349ce7..4f1566424 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -25,9 +25,6 @@
 #include "theory/decision_manager.h"
 
 namespace CVC4 {
-
-class SortInference;
-
 namespace theory {
 namespace uf {
 
@@ -366,8 +363,6 @@ class CardinalityExtension
   ~CardinalityExtension();
   /** get theory */
   TheoryUF* getTheory() { return d_th; }
-  /** get sort inference module */
-  SortInference* getSortInference();
   /** new node */
   void newEqClass( Node n );
   /** merge */