From c0d4ac3d307b13c24471da5af2f916569a7f52b9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 21 Mar 2021 09:01:04 -0500 Subject: [PATCH] Simplify strings term registration (#6174) String terms may enter into the equality engine without appearing in assertions, due to eager context-dependent simplification internal to the equality engine (--strings-eager-eval). In rare cases, we did not catch when a new string constant appeared in the equality engine, meaning it would not be marked as relevant leading to bogus models in incremental mode. This makes it so that proxy variables are stored in a user-context dependent manner, which impacts when terms marked as having a proxy variable are registered. The PR also simplifies our policies for when string terms are registered slightly. Fixes #6072. --- src/theory/strings/term_registry.cpp | 20 +++++++++++-------- src/theory/strings/term_registry.h | 2 +- src/theory/strings/theory_strings.cpp | 12 ++++------- test/regress/CMakeLists.txt | 1 + .../strings/issue6072-inc-no-const-reg.smt2 | 11 ++++++++++ 5 files changed, 29 insertions(+), 17 deletions(-) create mode 100644 test/regress/regress1/strings/issue6072-inc-no-const-reg.smt2 diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 9497b9661..f24fe12e5 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -49,6 +49,7 @@ TermRegistry::TermRegistry(SolverState& s, d_preregisteredTerms(s.getSatContext()), d_registeredTerms(s.getUserContext()), d_registeredTypes(s.getUserContext()), + d_proxyVar(s.getUserContext()), d_lengthLemmaTermsCache(s.getUserContext()), d_epg(pnm ? new EagerProofGenerator( pnm, @@ -246,8 +247,15 @@ void TermRegistry::preRegisterTerm(TNode n) void TermRegistry::registerTerm(Node n, int effort) { - TypeNode tn = n.getType(); + Trace("strings-register") << "TheoryStrings::registerTerm() " << n + << ", effort = " << effort << std::endl; + if (d_registeredTerms.find(n) != d_registeredTerms.end()) + { + Trace("strings-register") << "...already registered" << std::endl; + return; + } bool do_register = true; + TypeNode tn = n.getType(); if (!tn.isStringLike()) { if (options::stringEagerLen()) @@ -261,17 +269,13 @@ void TermRegistry::registerTerm(Node n, int effort) } if (!do_register) { + Trace("strings-register") << "...do not register" << std::endl; return; } - if (d_registeredTerms.find(n) != d_registeredTerms.end()) - { - return; - } + Trace("strings-register") << "...register" << std::endl; d_registeredTerms.insert(n); // ensure the type is registered registerType(tn); - Debug("strings-register") << "TheoryStrings::registerTerm() " << n - << ", effort = " << effort << std::endl; TrustNode regTermLem; if (tn.isStringLike()) { @@ -555,7 +559,7 @@ Node TermRegistry::getSymbolicDefinition(Node n, std::vector& exp) const Node TermRegistry::getProxyVariableFor(Node n) const { - std::map::const_iterator it = d_proxyVar.find(n); + NodeNodeMap::const_iterator it = d_proxyVar.find(n); if (it != d_proxyVar.end()) { return (*it).second; diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index a3d1d1e0e..cb1b50816 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -237,7 +237,7 @@ class TermRegistry * which rewrites to 3 = 3. * In the above example, we store "ABC" -> v_{"ABC"} in this map. */ - std::map d_proxyVar; + NodeNodeMap d_proxyVar; /** * Map from proxy variables to their normalized length. In the above example, * we store "ABC" -> 3. diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index b92cdaf5b..204b938fa 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -583,16 +583,12 @@ bool TheoryStrings::preNotifyFact( // this is only required for internal facts, others are already registered if (isInternal && atom.getKind() == EQUAL) { - // we must ensure these terms are registered + // We must ensure these terms are registered. We register eagerly here for + // performance reasons. Alternatively, terms could be registered at full + // effort in e.g. BaseSolver::init. for (const Node& t : atom) { - // terms in the equality engine are already registered, hence skip - // currently done for only string-like terms, but this could potentially - // be avoided. - if (!d_equalityEngine->hasTerm(t) && t.getType().isStringLike()) - { - d_termReg.registerTerm(t, 0); - } + d_termReg.registerTerm(t, 0); } } return false; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 964e73fc0..a98ea84bb 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2036,6 +2036,7 @@ set(regress_1_tests regress1/strings/issue5692-infer-proxy.smt2 regress1/strings/issue5940-skc-len-conc.smt2 regress1/strings/issue5940-2-skc-len-conc.smt2 + regress1/strings/issue6072-inc-no-const-reg.smt2 regress1/strings/issue6075-repl-len-one-rr.smt2 regress1/strings/issue6142-repl-inv-rew.smt2 regress1/strings/kaluza-fl.smt2 diff --git a/test/regress/regress1/strings/issue6072-inc-no-const-reg.smt2 b/test/regress/regress1/strings/issue6072-inc-no-const-reg.smt2 new file mode 100644 index 000000000..178c8f6ac --- /dev/null +++ b/test/regress/regress1/strings/issue6072-inc-no-const-reg.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: -i --strings-exp +; EXPECT: sat +; EXPECT: sat +(set-logic ALL) +(declare-fun i4 () Int) +(declare-fun str5 () String) +(assert (= (str.++ str5 (str.from_int i4)) (str.++ "15" str5 "1"))) +(push) +(check-sat) +(pop) +(check-sat) -- 2.30.2