Minor updates to string utilities (#3675)

1 files changed, 15 insertions, 1 deletions

diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index e052889f6..819e4b98f 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -61,7 +61,8 @@ class TheoryStrings;
  * to doPendingLemmas.
  *
  * It also manages other kinds of interaction with the output channel of the
- * theory of strings, e.g. sendPhaseRequirement.
+ * theory of strings, e.g. sendPhaseRequirement, setIncomplete, and
+ * with the extended theory object e.g. markCongruent.
  */
 class InferenceManager
 {
@@ -249,6 +250,19 @@ class InferenceManager
    * the node corresponding to their conjunction.
    */
   void explain(TNode literal, std::vector<TNode>& assumptions) const;
+  /**
+   * Set that we are incomplete for the current set of assertions (in other
+   * words, we must answer "unknown" instead of "sat"); this calls the output
+   * channel's setIncomplete method.
+   */
+  void setIncomplete();
+  /**
+   * Mark that terms a and b are congruent in the current context.
+   * This makes a call to markCongruent in the extended theory object of
+   * the parent theory if the kind of a (and b) is owned by the extended
+   * theory.
+   */
+  void markCongruent(Node a, Node b);
 
  private:
   /**