From ce2fa6ad8858c70aebf253b910bea3726065e85d Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 5 Aug 2020 07:18:10 -0700 Subject: [PATCH] [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. --- src/options/strings_options.toml | 8 +++++ src/theory/strings/term_registry.cpp | 12 ++++++++ src/theory/strings/term_registry.h | 9 ++++++ src/theory/strings/theory_strings.cpp | 44 +++++++++++++-------------- 4 files changed, 51 insertions(+), 22 deletions(-) diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index e69fa3317..f9893ef3a 100644 --- 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 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& vars, std::vector& 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)) { -- 2.30.2