diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-19 19:28:08 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-19 19:28:08 -0600 |
| commit | c8e8acd26b4bd5c47110b9448a74a45913b5518f (patch) | |
| tree | 91a27c3e9269e2ff4f852fb7b4d7475e00826ef0 | |
| parent | 3c754308f66d92cd4b03d5f159464585c315b528 (diff) | |
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.
| -rw-r--r-- | src/theory/theory_model_builder.cpp | 13 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2 | 16 |
3 files changed, 27 insertions, 3 deletions
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) |