Ensure sequences of Booleans generate Boolean term variable skolems when applicable...

Fixes #6510.

This PR also eliminates a deprecated variant mkBooleanTermVariable from SkolemManager.

diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index 773159b09739c87169921888c289fba6c1c108c2..b59d01fdd483684b11125f053c77b3aeec73f67d 100644 (file)
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -215,11 +215,6 @@ Node SkolemManager::mkDummySkolem(const std::string& prefix,
   return NodeManager::currentNM()->mkSkolem(prefix, type, comment, flags);
 }
 
-Node SkolemManager::mkBooleanTermVariable(Node t)
-{
-  return mkPurifySkolem(t, "", "", NodeManager::SKOLEM_BOOL_TERM_VAR);
-}
-
 ProofGenerator* SkolemManager::getProofGenerator(Node t) const
 {
   std::map<Node, ProofGenerator*>::const_iterator it = d_gens.find(t);

diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 13d0491a619b5220c13da7bfb9a02bb11d0f08fa..a6709373cc1f543427cc35bcda01372d67dcbb15 100644 (file)
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -254,12 +254,6 @@ class SkolemManager
                      const TypeNode& type,
                      const std::string& comment = "",
                      int flags = NodeManager::SKOLEM_DEFAULT);
-  /**
-   * Make Boolean term variable for term t. This is a special case of
-   * mkPurifySkolem above, where the returned term has kind
-   * BOOLEAN_TERM_VARIABLE.
-   */
-  Node mkBooleanTermVariable(Node t);
   /**
    * Get proof generator for existentially quantified formula q. This returns
    * the proof generator that was provided in a call to mkSkolem above.

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index eb2df12856a2f96710dfdee33a791040fc9ca552..9b23301f3b173c920cba7d3ac9c8f95066e328b5 100644 (file)
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -96,8 +96,14 @@ Node SkolemCache::mkTypedSkolemCached(
   {
     // exists k. k = a
     case SK_PURIFY:
-      sk = sm->mkPurifySkolem(a, c, "string purify skolem");
-      break;
+    {
+      // for sequences of Booleans, we may purify Boolean terms, in which case
+      // they must be Boolean term variables.
+      int flags = a.getType().isBoolean() ? NodeManager::SKOLEM_BOOL_TERM_VAR
+                                          : NodeManager::SKOLEM_DEFAULT;
+      sk = sm->mkPurifySkolem(a, c, "string purify skolem", flags);
+    }
+    break;
     // these are eliminated by normalizeStringSkolem
     case SK_ID_V_SPT:
     case SK_ID_V_SPT_REV:

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 956f2148c43be5eb78d746d278f6fabd34806305..02c0c3130f449783f836a0f9291612a15a1bb398 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -331,6 +331,7 @@ bool TheoryStrings::collectModelInfoType(
               // otherwise, it is a shared term
               argVal = d_valuation.getModelValue(nfe.d_nf[0][0]);
             }
+            Assert(!argVal.isNull());
             Node c = Rewriter::rewrite(nm->mkNode(SEQ_UNIT, argVal));
             pure_eq_assign[eqc] = c;
             Trace("strings-model") << "(unit: " << nfe.d_nf[0] << ") ";

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 538868c6cd66427772075fb3a4bdfeddac4c74c9..8ed170da904ccc20532afc29a1c3b3af6570a6cf 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1127,6 +1127,7 @@ set(regress_0_tests
   regress0/strings/issue5816-re-kind.smt2
   regress0/strings/issue5915-repl-ctn-rewrite.smt2
   regress0/strings/issue6203-3-unfold-trivial-true.smt2
+  regress0/strings/issue6510-seq-bool.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2

diff --git a/test/regress/regress0/strings/issue6510-seq-bool.smt2 b/test/regress/regress0/strings/issue6510-seq-bool.smt2
new file mode 100644 (file)
index 0000000..80bcea8
--- /dev/null
+++ b/test/regress/regress0/strings/issue6510-seq-bool.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --strings-exp -q
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun e () (Seq Bool))
+(assert (seq.nth (ite (= 0 (seq.len e)) (as seq.empty (Seq Bool)) (seq.unit false)) 0))
+(check-sat)