Fix term registry for constant case, simplify. (#4538)

We were getting an assertion failure (causing nightlies to fail) due to the recent optimization to the strings skolem cache (978f455). This ensures we ignore constant strings in TermRegistry::getRegisterTermAtomicLemma.

It also removes a deprecated option that is deleted in the proof-new branch.

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 3cf8f585214ea40db7b14fd0f934fa716f6d2e6a..32c4c64c736e0ba5dd43c6dc0f36c0b414720378 100644 (file)
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -54,15 +54,6 @@ header = "options/strings_options.h"
   read_only  = true
   help       = "perform string preprocessing lazily"
 
-[[option]]
-  name       = "stringLenGeqZ"
-  category   = "regular"
-  long       = "strings-len-geqz"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "strings length greater than zero lemmas"
-
 [[option]]
   name       = "stringLenNorm"
   category   = "regular"

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index ec034b0c9964d4d7ae98849dced719f793a1481e..6330d7c10354536517b5a1dcc57b1774aa692087 100644 (file)
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -374,6 +374,13 @@ Node TermRegistry::getRegisterTermAtomicLemma(Node n,
                                               LengthStatus s,
                                               std::map<Node, bool>& reqPhase)
 {
+  if (n.isConst())
+  {
+    // No need to send length for constant terms. This case may be triggered
+    // for cases where the skolem cache automatically replaces a skolem by
+    // a constant.
+    return Node::null();
+  }
   Assert(n.getType().isStringLike());
   NodeManager* nm = NodeManager::currentNM();
   Node n_len = nm->mkNode(kind::STRING_LENGTH, n);
@@ -433,14 +440,6 @@ Node TermRegistry::getRegisterTermAtomicLemma(Node n,
     Assert(false);
   }
 
-  // additionally add len( x ) >= 0 ?
-  if (options::stringLenGeqZ())
-  {
-    Node n_len_geq = nm->mkNode(kind::GEQ, n_len, d_zero);
-    n_len_geq = Rewriter::rewrite(n_len_geq);
-    lems.push_back(n_len_geq);
-  }
-
   if (lems.empty())
   {
     return Node::null();