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, 22 insertions, 0 deletions

diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 1926c836e..0dd576a04 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -124,6 +124,15 @@ TheoryModel* Valuation::getModel() {
   }
   return d_engine->getModel();
 }
+SortInference* Valuation::getSortInference()
+{
+  if (d_engine == nullptr)
+  {
+    // no theory engine, thus we don't have a sort inference object
+    return nullptr;
+  }
+  return d_engine->getSortInference();
+}
 
 void Valuation::setUnevaluatedKind(Kind k)
 {
@@ -198,5 +207,18 @@ bool Valuation::needCheck() const{
 
 bool Valuation::isRelevant(Node lit) const { return d_engine->isRelevant(lit); }
 
+context::CDList<Assertion>::const_iterator Valuation::factsBegin(TheoryId tid)
+{
+  Theory* theory = d_engine->theoryOf(tid);
+  Assert(theory != nullptr);
+  return theory->facts_begin();
+}
+context::CDList<Assertion>::const_iterator Valuation::factsEnd(TheoryId tid)
+{
+  Theory* theory = d_engine->theoryOf(tid);
+  Assert(theory != nullptr);
+  return theory->facts_end();
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */