From c8e8acd26b4bd5c47110b9448a74a45913b5518f Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 19 Jan 2021 19:28:08 -0600
Subject: [PATCH] Use arbitrary ground term assignment for sorts where
 isInterpretedFinite is true (#5790)

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.
---
 src/theory/theory_model_builder.cpp              | 13 ++++++++++---
 test/regress/CMakeLists.txt                      |  1 +
 .../regress1/fmf/issue5738-dt-interp-finite.smt2 | 16 ++++++++++++++++
 3 files changed, 27 insertions(+), 3 deletions(-)
 create mode 100644 test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 1fc609632..53b8f25a4 100644
--- 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 e2af099d7..d35758d5c 100644
--- 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
index 000000000..50373fde4
--- /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)
-- 
2.30.2