[Seq/Model] Do not enumerate elements of constants (#8179)

Fixes #8133. In the input from the issue, the string solver was
assigning a skeleton `(seq.unit smvX)` to a constant of sort `(Seq (Seq
Int))`. This constant was asserted to be different from `(seq.unit (as
seq.empty (Seq Int)))`. However, the `TheoryModelBuilder` was assigning
`smvX` the value `(as seq.empty (Seq Int))`, because `(as seq.empty (Seq
Int))` was not being registered with the equality engine. This is
because elements of constant sequences are not considered children, but
are a data member of the `Sequence` class. The commit updates
`TheoryStrings::collectModelInfoType()` to also register elements of
sequence constants with the equality engine.

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 3dc97ddc4c4e664c4a435856df5ea2ef56d11a51..eb02dc17844b8e248457ec85305d123d61f3c4b3 100644 (file)
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -2530,7 +2530,8 @@ void CoreSolver::checkNormalFormsDeq()
   NodeManager* nm = NodeManager::currentNM();
   Trace("str-deq") << "Process disequalites..." << std::endl;
   std::vector<Node> relevantDeqs;
-  //for each pair of disequal strings, must determine whether their lengths are equal or disequal
+  // for each pair of disequal strings, must determine whether their lengths
+  // are equal or disequal
   for (const Node& eq : deqs)
   {
     Trace("str-deq") << "- disequality " << eq << std::endl;

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 1f9d8caa5649ad8dde680cb2611ac4e7fad1f825..81733d5714a660602c41cc2fedb8d7805eeadd94 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -318,7 +318,7 @@ bool TheoryStrings::collectModelInfoType(
   std::vector<Node> len_splits;
   for (size_t i = 0, csize = col.size(); i < csize; i++)
   {
-    Trace("strings-model") << "Checking length for {" << col[i];
+    Trace("strings-model") << "Checking length for { " << col[i];
     Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl;
     Node len_value;
     if( lts[i].isConst() ) {
@@ -393,6 +393,26 @@ bool TheoryStrings::collectModelInfoType(
         // in the term set and, as a result, are skipped when the equality
         // engine is asserted to the theory model.
         m->getEqualityEngine()->addTerm(eqc);
+
+        // For sequences constants, also add the elements (expanding elements
+        // as necessary)
+        if (eqc.getType().isSequence())
+        {
+          const std::vector<Node> elems = eqc.getConst<Sequence>().getVec();
+          std::vector<TNode> visit(elems.begin(), elems.end());
+          for (size_t j = 0; j < visit.size(); j++)
+          {
+            Node se = visit[j];
+            Assert(se.isConst());
+            if (se.getType().isSequence())
+            {
+              const std::vector<Node> selems = se.getConst<Sequence>().getVec();
+              visit.insert(visit.end(), selems.begin(), selems.end());
+            }
+            m->getEqualityEngine()->addTerm(se);
+          }
+        }
+
         Trace("strings-model") << "-> constant" << std::endl;
         continue;
       }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9119708712ddb78fe7c2ccf23fa01fedb7995d51..984e0e8a78ab13bf7c2f47fc8e0597d7f4856892 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1145,6 +1145,7 @@ set(regress_0_tests
   regress0/seq/issue5547-small-seq-len-unit.smt2
   regress0/seq/issue5665-invalid-model.smt2
   regress0/seq/issue6337-seq.smt2
+  regress0/seq/issue8133-block-const-elems.smt2
   regress0/seq/len_simplify.smt2
   regress0/seq/mixed-types-seq-nth.smt2
   regress0/seq/nth-oob.smt2

diff --git a/test/regress/regress0/seq/issue8133-block-const-elems.smt2 b/test/regress/regress0/seq/issue8133-block-const-elems.smt2
new file mode 100644 (file)
index 0000000..2bffbb6
--- /dev/null
+++ b/test/regress/regress0/seq/issue8133-block-const-elems.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL)
+(declare-fun v () (Seq (Seq Int)))
+(declare-fun a () (Seq Int))
+(declare-fun r () (Seq Int))
+(declare-fun r3 () (Seq (Seq Int)))
+
+(assert (and
+  (not (= v r3))
+  (not (= v (seq.unit (as seq.empty (Seq Int)))))
+  (not (= r3 (seq.unit (as seq.empty (Seq Int)))))))
+
+(set-info :status sat)
+(check-sat)