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.

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 9497b9661f77b43aa4ea3b15974e6c6bd7be6b6b..f24fe12e547bc85c4770f992ae26cee309b754b9 100644 (file)
--- 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<Node>& exp) const
 
 Node TermRegistry::getProxyVariableFor(Node n) const
 {
-  std::map<Node, Node>::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 a3d1d1e0e0e0944da5453c4cb85e4b6af8eb1d8d..cb1b50816eae82cbcf0eaaa663f730978ddf206f 100644 (file)
--- 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<Node, Node> 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 b92cdaf5b63220a3b4b82253b83ea0bd2980ab47..204b938fa7a2b310be875f2fe83dddaffc7b025e 100644 (file)
--- 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 964e73fc0aaddafc943c5a5d08bf4ce9302158a5..a98ea84bb35d6d0dcfbf362cb9198c4636ed9fa2 100644 (file)
--- 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 (file)
index 0000000..178c8f6
--- /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)