diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-05 18:37:36 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-05 23:37:36 +0000 |
| commit | 7762098d624be5c46fee33a98dc8b85a9335dd43 (patch) | |
| tree | 76bce1d14a5fe9bec99120cf1393b3c47215c397 /test | |
| parent | 0181355bdf6b76fc550a2dca16fc0ac5e48c25ca (diff) | |
Fix exclusion criteria for codatatype model values (#7546)
This fixes codatatype model value construction.
Model construction for codatatypes is non-standard since it requires analyzing whether (possibly recursively defined) terms are alpha equivalent to others during model construction. This is currently handled as a special case within the theory model builder. (This should eventually be moved somewhere more appropriate via a new callback to theory).
This fixes the criteria which was too permissive about which values can be used in models. We now exclude values that match the skeleton of representative codatatype terms. Previously we additionally required that the terms were bisimilar.
Fixes #4851.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/datatypes/issue4851-cdt-model.smt2 | 8 |
2 files changed, 9 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 13434f829..a61b9df19 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1639,6 +1639,7 @@ set(regress_1_tests regress1/datatypes/dt-color-2.6.smt2 regress1/datatypes/dt-param-card4-unsat.smt2 regress1/datatypes/issue3266-small.smt2 + regress1/datatypes/issue4851-cdt-model.smt2 regress1/datatypes/issue-variant-dt-zero.smt2 regress1/datatypes/manos-model.smt2 regress1/datatypes/non-simple-rec.smt2 diff --git a/test/regress/regress1/datatypes/issue4851-cdt-model.smt2 b/test/regress/regress1/datatypes/issue4851-cdt-model.smt2 new file mode 100644 index 000000000..e0ed3ea9f --- /dev/null +++ b/test/regress/regress1/datatypes/issue4851-cdt-model.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status sat) +(declare-codatatypes ((a 0)) (((b (c Int) (d a))))) +(declare-fun e () a) +(declare-fun f () a) +(assert (distinct f (b 0 f))) +(assert (= e f)) +(check-sat) |