From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 12 May 2021 13:30:42 +0000 (-0500)
Subject: Ensure sequences of Booleans generate Boolean term variable skolems when applicable... 
X-Git-Tag: cvc5-1.0.0~1772
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=111f98a41b488b8124fbecd28dba17465ea30786;p=cvc5.git

Ensure sequences of Booleans generate Boolean term variable skolems when applicable (#6529)

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 773159b09..b59d01fdd 100644
--- 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 13d0491a6..a6709373c 100644
--- 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 eb2df1285..9b23301f3 100644
--- 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 956f2148c..02c0c3130 100644
--- 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 538868c6c..8ed170da9 100644
--- 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
index 000000000..80bcea8a1
--- /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)