[Strings] Add eager context-dependent evaluation (#4847)

This commit adds eager evaluation of string terms based on the current
context. To do so, it declares the string kinds to be "interpreted" in
the equality engine. This allows us to avoid making a series of
decisions such as:

** (= "describe" (str.substr actionName 0 8)) :DE-DECISION:
*** (= actionName "deletecertificate") :DE-DECISION:
**** (= resource_partition "aws") :DE-DECISION:
***** (= resource_region "af-south-1") :DE-DECISION:
****** (= resource_account "") :DE-DECISION:
******* (= (str.len (str.substr actionName 0 3)) 0) :DE-DECISION:
******** (= (str.len (str.substr actionName 0 4)) 0) :DE-DECISION:
********* (= (str.len (str.substr actionName 0 6)) 0) :DE-DECISION:
********** (= (str.len (str.substr actionName 0 5)) 0) :DE-DECISION:
*********** (= (str.len (str.substr actionName 0 9)) 0) :DE-DECISION:
************ (= (str.len (str.substr actionName 0 7)) 0) :DE-DECISION:
************* (= (str.len (str.substr actionName 0 10)) 0) :DE-DECISION:
************** (= (str.len (str.substr actionName 0 2)) 0) :DE-DECISION:
*************** (= (str.len (str.substr actionName 0 13)) 0) :DE-DECISION:
**************** (= (str.len (str.substr actionName 0 12)) 0) :DE-DECISION:
***************** (= (str.len resource_service) 0) :DE-DECISION:
****************** (= (str.len resource_account) 0) :DE-DECISION:
In such a case, we can detect that there is a conflict after the first
two decisions because (str.substr "deletecertificate" 0 8) is
deletece which is different from describe. The equality engine uses
the rewriter to evaluate interpreted kinds with constant arguments.

This technique leads to a significant speedup on some of the newer
Amazon benchmarks.

3 files changed, 43 insertions, 22 deletions

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 0b80db2ee..ed20406df 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -535,6 +535,18 @@ Node TermRegistry::getProxyVariableFor(Node n) const
   return Node::null();
 }
 
+Node TermRegistry::ensureProxyVariableFor(Node n)
+{
+  Node proxy = getProxyVariableFor(n);
+  if (proxy.isNull())
+  {
+    registerTerm(n, 0);
+    proxy = getProxyVariableFor(n);
+  }
+  Assert(!proxy.isNull());
+  return proxy;
+}
+
 void TermRegistry::inferSubstitutionProxyVars(Node n,
                                               std::vector<Node>& vars,
                                               std::vector<Node>& subs,
diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h
index d0589be90..9a66690b8 100644
--- a/src/theory/strings/term_registry.h
+++ b/src/theory/strings/term_registry.h
@@ -168,6 +168,15 @@ class TermRegistry
    */
   Node getProxyVariableFor(Node n) const;
 
+  /**
+   * Get the proxy variable for a term. If the proxy variable does not exist,
+   * this method registers the term and then returns its proxy variable.
+   *
+   * @param n The term
+   * @return Proxy variable for `n`
+   */
+  Node ensureProxyVariableFor(Node n);
+
   /** infer substitution proxy vars
    *
    * This method attempts to (partially) convert the formula n into a
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 84fd08e7c..102826591 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -64,29 +64,30 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_rsolver(d_state, d_im, d_csolver, d_esolver, d_statistics, c, u),
       d_stringsFmf(c, u, valuation, d_termReg)
 {
+  bool eagerEval = options::stringEagerEval();
   // The kinds we are treating as function application in congruence
-  d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
-  d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
-  d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
-  d_equalityEngine.addFunctionKind(kind::STRING_TO_CODE);
-  d_equalityEngine.addFunctionKind(kind::SEQ_UNIT);
+  d_equalityEngine.addFunctionKind(kind::STRING_LENGTH, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_CONCAT, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_TO_CODE, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::SEQ_UNIT, eagerEval);
 
   // extended functions
-  d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
-  d_equalityEngine.addFunctionKind(kind::STRING_LEQ);
-  d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR);
-  d_equalityEngine.addFunctionKind(kind::STRING_UPDATE);
-  d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
-  d_equalityEngine.addFunctionKind(kind::STRING_STOI);
-  d_equalityEngine.addFunctionKind(kind::STRING_STRIDOF);
-  d_equalityEngine.addFunctionKind(kind::STRING_STRREPL);
-  d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL);
-  d_equalityEngine.addFunctionKind(kind::STRING_REPLACE_RE);
-  d_equalityEngine.addFunctionKind(kind::STRING_REPLACE_RE_ALL);
-  d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL);
-  d_equalityEngine.addFunctionKind(kind::STRING_TOLOWER);
-  d_equalityEngine.addFunctionKind(kind::STRING_TOUPPER);
-  d_equalityEngine.addFunctionKind(kind::STRING_REV);
+  d_equalityEngine.addFunctionKind(kind::STRING_STRCTN, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_LEQ, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_UPDATE, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_ITOS, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_STOI, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_STRIDOF, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_STRREPL, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_REPLACE_RE, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_REPLACE_RE_ALL, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_TOLOWER, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_TOUPPER, eagerEval);
+  d_equalityEngine.addFunctionKind(kind::STRING_REV, eagerEval);
 
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
   d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
@@ -917,8 +918,7 @@ void TheoryStrings::checkCodes()
         Node cc = nm->mkNode(kind::STRING_TO_CODE, c);
         cc = Rewriter::rewrite(cc);
         Assert(cc.isConst());
-        Node cp = d_termReg.getProxyVariableFor(c);
-        AlwaysAssert(!cp.isNull());
+        Node cp = d_termReg.ensureProxyVariableFor(c);
         Node vc = nm->mkNode(STRING_TO_CODE, cp);
         if (!d_state.areEqual(cc, vc))
         {