Add rewrite for solving stoi (#2532)

1 files changed, 22 insertions, 0 deletions

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 2fd7b3525..6c653bf05 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -580,7 +580,12 @@ private:
   void doPendingFacts();
   void doPendingLemmas();
   bool hasProcessed();
+  /**
+   * Adds equality a = b to the vector exp if a and b are distinct terms. It
+   * must be the case that areEqual( a, b ) holds in this context.
+   */
   void addToExplanation(Node a, Node b, std::vector<Node>& exp);
+  /** Adds lit to the vector exp if it is non-null */
   void addToExplanation(Node lit, std::vector<Node>& exp);
 
   /** Register term
@@ -602,6 +607,22 @@ private:
    * effort, the call to this method does nothing.
    */
   void registerTerm(Node n, int effort);
+  //-------------------------------------send inferences
+  /** send internal inferences
+   *
+   * This is called when we have inferred exp => conc, where exp is a set
+   * of equalities and disequalities that hold in the current equality engine.
+   * This method adds equalities and disequalities ~( s = t ) via
+   * sendInference such that both s and t are either constants or terms
+   * that already occur in the equality engine, and ~( s = t ) is a consequence
+   * of conc. This function can be seen as a "conservative" version of
+   * sendInference below in that it does not introduce any new non-constant
+   * terms to the state.
+   *
+   * The argument c is a string identifying the reason for the interference.
+   * This string is used for debugging purposes.
+   */
+  void sendInternalInference(std::vector<Node>& exp, Node conc, const char* c);
   // send lemma
   void sendInference(std::vector<Node>& exp,
                      std::vector<Node>& exp_n,
@@ -615,6 +636,7 @@ private:
   void sendLemma(Node ant, Node conc, const char* c);
   void sendInfer(Node eq_exp, Node eq, const char* c);
   bool sendSplit(Node a, Node b, const char* c, bool preq = true);
+  //-------------------------------------end send inferences
 
   /** mkConcat **/
   inline Node mkConcat(Node n1, Node n2);