From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 14 Jul 2021 13:43:25 +0000 (-0500)
Subject: Fix models for sequences of infinite element type (#6870)
X-Git-Tag: cvc5-1.0.0~1492
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=51ea72ebbe4863be05055358ae02af09e8973585;p=cvc5.git

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 06464af60..b5a8472e6 100644
--- 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 00491128a..b25f8f021 100644
--- 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 8de43fd55..8912bad3b 100644
--- 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));