Use arbitrary ground term assignment for sorts where isInterpretedFinite is true...

This makes a small change to our model construction to assign arbitrary values to eqc for types that are "interpreted finite", that is, have finite cardinality under the assumption that uninterpreted sorts are finite/infinite (when finite model finding is on/off). Uninterpreted sorts themselves always use the type enumerator to assign distinct values.

This fixes #5738.

This change is necessary since there was previously a mismatch between types where isFinite != isInterpretedFinite, in particular a datatype with a single constructor with a unintepreted type field as in that issue.

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 1fc609632abf2f165f4b24380ea37a7a673ca092..53b8f25a4ff5af9aa535e994ae1a7028a76dfe3c 100644 (file)
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -782,10 +782,17 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
             n = itAssigner->second.getNextAssignment();
             Assert(!n.isNull());
           }
-          else if (!t.isFinite())
+          else if (t.isSort() || !t.isInterpretedFinite())
           {
-            // if its infinite, we get a fresh value that does not occur in
-            // the model.
+            // If its interpreted as infinite, we get a fresh value that does
+            // not occur in the model.
+            // Note we also consider uninterpreted sorts to be infinite here
+            // regardless of whether isInterpretedFinite is true (which is true
+            // for uninterpreted sorts iff finite model finding is enabled).
+            // This is required because the UF solver does not explicitly
+            // assign uninterpreted constants to equivalence classes in its
+            // collectModelValues method. Doing so would have the same effect
+            // as running the code in this case.
             bool success;
             do
             {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e2af099d7883e40970fdf36af3cb7380e9badcee..d35758d5c200a2bafa7b96c4a7e61877c956a00a 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1504,6 +1504,7 @@ set(regress_1_tests
   regress1/fmf/issue3689.smt2
   regress1/fmf/issue4068-si-qf.smt2
   regress1/fmf/issue4225-univ-fun.smt2
+  regress1/fmf/issue5738-dt-interp-finite.smt2
   regress1/fmf/issue916-fmf-or.smt2
   regress1/fmf/jasmin-cdt-crash.smt2
   regress1/fmf/ko-bound-set.cvc

diff --git a/test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2 b/test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2
new file mode 100644 (file)
index 0000000..50373fd
--- /dev/null
+++ b/test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2
@@ -0,0 +1,16 @@
+(set-logic UFLIA)
+(set-info :status sat)
+(set-option :finite-model-find true)
+(declare-sort a 0)
+(declare-sort b 0)
+(declare-datatypes ((c 0)) (((d (m b)))))
+(declare-sort d 0)
+(declare-sort e 0)
+(declare-datatypes ((f 0)) (((n))))
+(declare-fun o (f e d c) a)
+(declare-fun g (f) e)
+(declare-fun h (f d) c)
+(declare-fun i () f)
+(declare-fun j (e) d)
+(assert (forall ((k e)) (exists ((l c)) (= (o i k (j k) l) (o i (g i) (j k) (h i (j k)))))))
+(check-sat)