diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-12-03 12:18:10 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-03 14:18:10 -0600 |
| commit | 8994bc9fd49a255286f8a6bac6c14407e8add41f (patch) | |
| tree | 145ea96fcb9381be1aa2f298ca66165d12864682 /test/regress | |
| parent | 8e1dc557383f754e33399b6b0f783e7048732df0 (diff) | |
Models as (#5581)
This PR relates to #4987 .
Our plan is to:
delete the model keyword (done in #5415 )
avoid printing extra declarations by default (done in #5432 )
wrap UF values with as expressions.
This PR does step 3, fixes a regression accordingly, and adds the formula from #4987 and a variant of it to the regressions.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress0/models-print-1.smt2 | 10 | ||||
| -rw-r--r-- | test/regress/regress0/models-print-2.smt2 | 11 | ||||
| -rw-r--r-- | test/regress/regress0/printer/empty_sort.smt2 | 1 |
4 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5ab1cd6c2..4145c0e27 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -613,6 +613,8 @@ set(regress_0_tests regress0/logops.04.cvc regress0/logops.05.cvc regress0/model-core.smt2 + regress0/models-print-1.smt2 + regress0/models-print-2.smt2 regress0/named-expr-use.smt2 regress0/nl/coeff-sat.smt2 regress0/nl/ext-rew-aggr-test.smt2 diff --git a/test/regress/regress0/models-print-1.smt2 b/test/regress/regress0/models-print-1.smt2 new file mode 100644 index 000000000..974c1f774 --- /dev/null +++ b/test/regress/regress0/models-print-1.smt2 @@ -0,0 +1,10 @@ +; the purpose of this test is to verify that there are no redundant `declare-fun`s + +; EXIT: 0 +; SCRUBBER: grep declare-fun +(set-logic QF_UF) +(set-option :produce-models true) +(declare-sort Sort0 0) +(declare-fun f1 (Sort0) Bool) +(check-sat) +(get-model) diff --git a/test/regress/regress0/models-print-2.smt2 b/test/regress/regress0/models-print-2.smt2 new file mode 100644 index 000000000..1e176d5c2 --- /dev/null +++ b/test/regress/regress0/models-print-2.smt2 @@ -0,0 +1,11 @@ +; the purpose of this test is to verify that there is a `as` term in the output. +; the scrubber excludes all lines without "(as @", and replaces this pattern by "AS". + +; SCRUBBER: sed -e 's/.*(as @.*/AS/; /sat/d; /cardinality/d; /^($/d; /^)$/d' +; EXPECT: AS +(set-logic QF_UF) +(set-option :produce-models true) +(declare-sort Sort0 0) +(declare-fun f1 () Sort0) +(check-sat) +(get-model) diff --git a/test/regress/regress0/printer/empty_sort.smt2 b/test/regress/regress0/printer/empty_sort.smt2 index efe68e920..eb963e443 100644 --- a/test/regress/regress0/printer/empty_sort.smt2 +++ b/test/regress/regress0/printer/empty_sort.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --model-u-print=decl-fun ; EXPECT: (declare-fun gt () us_image) ; EXPECT: (declare-fun gt () ||) ; SCRUBBER: sed -e '/declare-fun/!d; s/declare-fun [^[:space:]]*/declare-fun gt/g' |