[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.

1 files changed, 22 insertions, 22 deletions

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))
         {