diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-20 16:40:12 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-20 21:40:12 +0000 |
| commit | cc8ce1bcdf8d6a4b508723063879e891a6cbd8c3 (patch) | |
| tree | fef63c0628404e673eca56947d19411198ba3ce2 /test/regress | |
| parent | 18ce14653647a93319cc53eec9bc310d3a4c6f57 (diff) | |
Add instantiation pool feature to the API (#6358)
This adds the command declare-pool to the public API. It also adds parsing support for this feature, lifts the internal kinds to public kinds, adds an example regression, and a unit test for the new declare-pool solver method.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/pool-example.smt2 | 17 |
2 files changed, 18 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 12e0c568d..24d6602e9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1805,6 +1805,7 @@ set(regress_1_tests regress1/quantifiers/nra-interleave-inst.smt2 regress1/quantifiers/opisavailable-12.smt2 regress1/quantifiers/parametric-lists.smt2 + regress1/quantifiers/pool-example.smt2 regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2 regress1/quantifiers/psyco-001-bv.smt2 regress1/quantifiers/psyco-107-bv.smt2 diff --git a/test/regress/regress1/quantifiers/pool-example.smt2 b/test/regress/regress1/quantifiers/pool-example.smt2 new file mode 100644 index 000000000..8344f5412 --- /dev/null +++ b/test/regress/regress1/quantifiers/pool-example.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --pool-inst +; EXPECT: unsat +(set-logic ALL) +(declare-pool L Int ()) + +(declare-fun P (Int) Bool) + +(assert (not (= +(forall ((x Int)) (! (! + (P x) + :skolem-add-to-pool ((- x 100) L)) :pool (L) )) +(forall ((x Int)) (! (! + (P (+ x 100)) + :skolem-add-to-pool ((+ x 100) L)) :pool (L) ) +)))) + +(check-sat) |