1 files changed, 16 insertions, 0 deletions
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
index 891016f0a..60b45878f 100644
--- a/src/theory/theory_state.h
+++ b/src/theory/theory_state.h
@@ -81,10 +81,26 @@ class TheoryState
    * 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();
 
   /** Returns true if n has a current SAT assignment and stores it in value. */
   virtual bool hasSatValue(TNode n, bool& value) 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);
+
   /** Get the underlying valuation class */
   Valuation& getValuation();