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

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index e69fa33170e43282bd8a3d672cdd7ee162d5f2b5..f9893ef3a939c9b54975d11008f9ee558f07dfa2 100644 (file)
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -222,3 +222,11 @@ header = "options/strings_options.h"
   type       = "bool"
   default    = "false"
   help       = "add skolem length constraints in conclusions of inferences"
+
+[[option]]
+  name       = "stringEagerEval"
+  category   = "regular"
+  long       = "strings-eager-eval"
+  type       = "bool"
+  default    = "true"
+  help       = "perform eager context-dependent evaluation for applications of string kinds"

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 0b80db2ee1aa4fafbea9a8ea18e63446d3af0fec..ed20406df4e243fb8be5ca33d71a3009083c7fb9 100644 (file)
--- 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 d0589be9057d6563d066bdb5714a029398e6f275..9a66690b81738d6b6468190c514ba37fe7568c71 100644 (file)
--- 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 84fd08e7ca1bb81bd2b776d6f851ae8614f1add5..102826591914233026659b273143b3c6efd45db7 100644 (file)
--- 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))
         {