1 files changed, 16 insertions, 12 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index f4aa0675c..0f59e73dc 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -97,27 +97,33 @@ class TheoryStrings : public Theory {
   void shutdown() override {}
   /** add shared term */
   void notifySharedTerm(TNode n) override;
-  /** get equality status */
-  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   /** preregister term */
   void preRegisterTerm(TNode n) override;
   /** Expand definition */
   TrustNode expandDefinition(Node n) override;
-  /** Check at effort e */
-  void check(Effort e) override;
-  /** needs check last effort */
+  //--------------------------------- standard check
+  /** Do we need a check call at last call effort? */
   bool needsCheckLastEffort() override;
+  bool preNotifyFact(TNode atom,
+                     bool pol,
+                     TNode fact,
+                     bool isPrereg,
+                     bool isInternal) override;
+  void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
+  /** Post-check, called after the fact queue of the theory is processed. */
+  void postCheck(Effort level) override;
+  //--------------------------------- end standard check
+  /** propagate method */
+  bool propagateLit(TNode literal);
   /** Conflict when merging two constants */
   void conflict(TNode a, TNode b);
   /** called when a new equivalence class is created */
   void eqNotifyNewClass(TNode t);
   /** preprocess rewrite */
   TrustNode ppRewrite(TNode atom) override;
-  /**
-   * Get all relevant information in this theory regarding the current
-   * model. Return false if a contradiction is discovered.
-   */
-  bool collectModelInfo(TheoryModel* m) override;
+  /** Collect model values in m based on the relevant terms given by termSet */
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
 
  private:
   /** NotifyClass for equality engine */
@@ -171,8 +177,6 @@ class TheoryStrings : public Theory {
     /** The solver state of the theory of strings */
     SolverState& d_state;
   };/* class TheoryStrings::NotifyClass */
-  /** propagate method */
-  bool propagateLit(TNode literal);
   /** compute care graph */
   void computeCareGraph() override;
   /**