From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 21 Mar 2021 14:01:04 +0000 (-0500)
Subject: Simplify strings term registration (#6174)
X-Git-Tag: cvc5-1.0.0~2048
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c0d4ac3d307b13c24471da5af2f916569a7f52b9;p=cvc5.git

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 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<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 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<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 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)