diff options
| -rw-r--r-- | src/options/strings_options.toml | 8 | ||||
| -rw-r--r-- | src/theory/strings/term_registry.cpp | 12 | ||||
| -rw-r--r-- | src/theory/strings/term_registry.h | 9 | ||||
| -rw-r--r-- | 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<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)) { |