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

diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 9759309fa..305795881 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -21,8 +21,10 @@
 #ifndef CVC4__THEORY__VALUATION_H
 #define CVC4__THEORY__VALUATION_H
 
+#include "context/cdlist.h"
 #include "expr/node.h"
 #include "options/theory_options.h"
+#include "theory/assertion.h"
 
 namespace CVC4 {
 
@@ -31,6 +33,7 @@ class TheoryEngine;
 namespace theory {
 
 class TheoryModel;
+class SortInference;
 
 /**
  * The status of an equality in the current context.
@@ -111,6 +114,11 @@ public:
    * check.
    */
   TheoryModel* getModel();
+  /**
+   * Returns a pointer to the sort inference module, which lives in TheoryEngine
+   * and is non-null when options::sortInference is true.
+   */
+  SortInference* getSortInference();
 
   //-------------------------------------- static configuration of the model
   /**
@@ -195,6 +203,17 @@ public:
    * or during LAST_CALL effort.
    */
   bool isRelevant(Node lit) const;
+
+  //------------------------------------------- access methods for assertions
+  /**
+   * The following methods are intended only to be used in limited use cases,
+   * for cases where a theory (e.g. quantifiers) requires knowing about the
+   * assertions from other theories.
+   */
+  /** The beginning iterator of facts for theory tid.*/
+  context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
+  /** The beginning iterator of facts for theory tid.*/
+  context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
 };/* class Valuation */
 
 }/* CVC4::theory namespace */