Fix models for sequences of infinite element type (#6870)

This fixes our model construction for sequences of infinite element type.

We were relying on getModelValue in our model construction which is incorrect since it assumes that the element type's theory can provide concrete values during model generation time. This makes the sequence model construction more robust by generalizing how model values are assigned: we use skeletons instead of concrete values when the element type is infinite.

This fixes some open model generation issues with Facebook benchmarks.

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 06464af609212940b35606d997c851d10c3a267c..b5a8472e6ddf16410ca80db820da29abebc6a0a4 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -271,17 +271,18 @@ void Smt2Printer::toStream(std::ostream& out,
         toStreamType(out, n.getType());
         out << ")";
       }
-      if (snvec.size() > 1)
+      else if (snvec.size() > 1)
       {
         out << "(seq.++";
+        for (const Node& snvc : snvec)
+        {
+          out << " (seq.unit " << snvc << ")";
+        }
+        out << ")";
       }
-      for (const Node& snvc : snvec)
-      {
-        out << " (seq.unit " << snvc << ")";
-      }
-      if (snvec.size() > 1)
+      else
       {
-        out << ")";
+        out << "(seq.unit " << snvec[0] << ")";
       }
       break;
     }

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 00491128a7526d54fb4b4c7c3136081206ad2912..b25f8f02176fcf99b74c0af7d100594ba267f2d0 100644 (file)
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -540,7 +540,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
   {
     Assert(tn.isSequence());
     TypeNode etn = tn.getSequenceElementType();
-    if (d_state.isFiniteType(etn))
+    if (!d_state.isFiniteType(etn))
     {
       // infinite cardinality, we are fine
       return;

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 8de43fd558a7c1d39424271e8f4cb4e3b6a1a398..8912bad3b046c18ab60ea3892b05d1c6d9155595 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -15,7 +15,10 @@
 
 #include "theory/strings/theory_strings.h"
 
+#include "expr/attribute.h"
+#include "expr/bound_var_manager.h"
 #include "expr/kind.h"
+#include "expr/sequence.h"
 #include "options/smt_options.h"
 #include "options/strings_options.h"
 #include "options/theory_options.h"
@@ -37,6 +40,16 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
+/**
+ * Attribute used for making unique (bound variables) which correspond to
+ * unique element values used in sequence models. See use in collectModelValues
+ * below.
+ */
+struct SeqModelVarAttributeId
+{
+};
+using SeqModelVarAttribute = expr::Attribute<SeqModelVarAttributeId, Node>;
+
 TheoryStrings::TheoryStrings(context::Context* c,
                              context::UserContext* u,
                              OutputChannel& out,
@@ -355,10 +368,13 @@ bool TheoryStrings::collectModelInfoType(
             }
             else
             {
-              // otherwise, it is a shared term
-              argVal = d_valuation.getModelValue(nfe.d_nf[0][0]);
+              // Otherwise, we use the term itself. We cannot get the model
+              // value of this term, since it might not be available yet, as
+              // it may belong to a theory that has not built its model yet.
+              // Hence, we assign a (non-constant) skeleton (seq.unit argVal).
+              argVal = nfe.d_nf[0][0];
             }
-            Assert(!argVal.isNull());
+            Assert(!argVal.isNull()) << "No value for " << nfe.d_nf[0][0];
             Node c = Rewriter::rewrite(nm->mkNode(SEQ_UNIT, argVal));
             pure_eq_assign[eqc] = c;
             Trace("strings-model") << "(unit: " << nfe.d_nf[0] << ") ";
@@ -483,6 +499,38 @@ bool TheoryStrings::collectModelInfoType(
               return false;
             }
             c = sel->getCurrent();
+            // if we are a sequence with infinite element type
+            if (tn.isSequence()
+                && !d_state.isFiniteType(tn.getSequenceElementType()))
+            {
+              // Make a skeleton instead. In particular, this means that
+              // a value:
+              //   (seq.++ (seq.unit 0) (seq.unit 1) (seq.unit 2))
+              // becomes:
+              //   (seq.++ (seq.unit k_0) (seq.unit k_1) (seq.unit k_2))
+              // where k_0, k_1, k_2 are fresh integer variables. These
+              // variables will be assigned values in the standard way by the
+              // model. This construction is necessary since the strings solver
+              // must constrain the length of the model of an equivalence class
+              // (e.g. in this case to length 3); moreover we cannot assign a
+              // concrete value since it may conflict with other skeletons we
+              // have assigned, e.g. for the case of (seq.unit argVal) above.
+              SkolemManager* sm = nm->getSkolemManager();
+              BoundVarManager* bvm = nm->getBoundVarManager();
+              Assert(c.getKind() == CONST_SEQUENCE);
+              const Sequence& sn = c.getConst<Sequence>();
+              const std::vector<Node>& snvec = sn.getVec();
+              std::vector<Node> skChildren;
+              for (const Node& snv : snvec)
+              {
+                TypeNode etn = snv.getType();
+                Node v = bvm->mkBoundVar<SeqModelVarAttribute>(snv, etn);
+                // use a skolem, not a bound variable
+                Node kv = sm->mkPurifySkolem(v, "smv");
+                skChildren.push_back(nm->mkNode(SEQ_UNIT, kv));
+              }
+              c = utils::mkConcat(skChildren, tn);
+            }
             // increment
             sel->increment();
           } while (m->hasTerm(c));