Support sequences of fixed finite cardinality (#7371)

The only open case is dynamic cardinality types (e.g. uninterpreted sorts when FMF is enabled).

5 files changed, 55 insertions, 2 deletions

diff --git a/src/theory/incomplete_id.cpp b/src/theory/incomplete_id.cpp
index a2a3baa0f..c763fb9a0 100644
--- a/src/theory/incomplete_id.cpp
+++ b/src/theory/incomplete_id.cpp
@@ -40,6 +40,8 @@ const char* toString(IncompleteId i)
     case IncompleteId::STRINGS_LOOP_SKIP: return "STRINGS_LOOP_SKIP";
     case IncompleteId::STRINGS_REGEXP_NO_SIMPLIFY:
       return "STRINGS_REGEXP_NO_SIMPLIFY";
+    case IncompleteId::SEQ_FINITE_DYNAMIC_CARDINALITY:
+      return "SEQ_FINITE_DYNAMIC_CARDINALITY";
     case IncompleteId::UF_HO_EXT_DISABLED: return "UF_HO_EXT_DISABLED";
     case IncompleteId::UF_CARD_DISABLED: return "UF_CARD_DISABLED";
     case IncompleteId::UF_CARD_MODE: return "UF_CARD_MODE";
diff --git a/src/theory/incomplete_id.h b/src/theory/incomplete_id.h
index 951c2a94f..aaa458d8e 100644
--- a/src/theory/incomplete_id.h
+++ b/src/theory/incomplete_id.h
@@ -52,6 +52,11 @@ enum class IncompleteId
   STRINGS_LOOP_SKIP,
   // we could not simplify a regular expression membership
   STRINGS_REGEXP_NO_SIMPLIFY,
+  // incomplete due to sequence of a dynamic finite type (e.g. a type that
+  // we know is finite, but its exact cardinality is not fixed. For example,
+  // when finite model finding is enabled, uninterpreted sorts have a
+  // cardinality that depends on their interpretation in the current model).
+  SEQ_FINITE_DYNAMIC_CARDINALITY,
   // HO extensionality axiom was disabled
   UF_HO_EXT_DISABLED,
   // UF+cardinality solver was disabled
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index b675d2444..9396e3e87 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -17,6 +17,7 @@
 #include "theory/strings/base_solver.h"
 
 #include "expr/sequence.h"
+#include "options/quantifiers_options.h"
 #include "options/strings_options.h"
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
@@ -539,8 +540,41 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
       // infinite cardinality, we are fine
       return;
     }
-    // TODO (cvc4-projects #23): how to handle sequence for finite types?
-    return;
+    // we check the cardinality class of the type, assuming that FMF is
+    // disabled.
+    if (isCardinalityClassFinite(etn.getCardinalityClass(), false))
+    {
+      Cardinality c = etn.getCardinality();
+      bool smallCardinality = false;
+      if (!c.isLargeFinite())
+      {
+        Integer ci = c.getFiniteCardinality();
+        if (ci.fitsUnsignedInt())
+        {
+          smallCardinality = true;
+          typeCardSize = ci.toUnsignedInt();
+        }
+      }
+      if (!smallCardinality)
+      {
+        // if it is large finite, then there is no way we could have
+        // constructed that many terms in memory, hence there is nothing
+        // to do.
+        return;
+      }
+    }
+    else
+    {
+      Assert(options().quantifiers.finiteModelFind);
+      // we are in a case where the cardinality of the type is infinite
+      // if not FMF, and finite given the Env's option value for FMF. In this
+      // case, FMF must be true, and the cardinality is finite and dynamic
+      // (i.e. it depends on the model's finite interpretation for uninterpreted
+      // sorts). We do not know how to handle this case, we set incomplete.
+      // TODO (cvc4-projects #23): how to handle sequence for finite types?
+      d_im.setIncomplete(IncompleteId::SEQ_FINITE_DYNAMIC_CARDINALITY);
+      return;
+    }
   }
   // for each collection
   for (unsigned i = 0, csize = cols.size(); i < csize; ++i)
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 84f0ef408..a0f6f7999 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2268,6 +2268,7 @@ set(regress_1_tests
   regress1/strings/rev-ex5.smt2
   regress1/strings/rew-020618.smt2
   regress1/strings/rew-check1.smt2
+  regress1/strings/seq-cardinality.smt2
   regress1/strings/seq-quant-infinite-branch.smt2
   regress1/strings/simple-re-consume.smt2
   regress1/strings/stoi-400million.smt2
diff --git a/test/regress/regress1/strings/seq-cardinality.smt2 b/test/regress/regress1/strings/seq-cardinality.smt2
new file mode 100644
index 000000000..93a4985d4
--- /dev/null
+++ b/test/regress/regress1/strings/seq-cardinality.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun x () (Seq (_ BitVec 1)))
+(declare-fun y () (Seq (_ BitVec 1)))
+(declare-fun z () (Seq (_ BitVec 1)))
+
+(assert (= (seq.len x) 1))
+(assert (= (seq.len y) 1))
+(assert (= (seq.len z) 1))
+(assert (distinct x y z))
+(check-sat)