diff options
| author | Ying Sheng <sqy1415@gmail.com> | 2019-10-08 08:18:21 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-08 08:18:21 -0700 |
| commit | 00ccc01140bcdeaadedf8ae1b9f224ccdc812bc0 (patch) | |
| tree | bc4981945d06c25d57854fbf2651431061e9ae42 /test/regress/regress0/arith/integers | |
| parent | 94feff6c3b03325115e2c1c91121b83945dba4b0 (diff) | |
Make ackermannization generally applicable rather than just BV (#3315)
The ackermannization process is currently already support general theories rather than specifically for BV. In this pull request, an option has been added to turn on ackermannization independently.
Diffstat (limited to 'test/regress/regress0/arith/integers')
6 files changed, 101 insertions, 0 deletions
diff --git a/test/regress/regress0/arith/integers/ackermann1.smt2 b/test/regress/regress0/arith/integers/ackermann1.smt2 new file mode 100644 index 000000000..b04210f36 --- /dev/null +++ b/test/regress/regress0/arith/integers/ackermann1.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_UFLIA) + +(declare-fun a () Int) +(declare-fun b () Int) + +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) + +(assert (= (f (g (f (f a)))) (f (g (f a))))) +(assert (= (f a) b)) +(assert (= (f b) a)) +(assert (not (= a b))) +(assert (= (g a) (f a))) +(assert (= (g b) (f b))) + +(check-sat) +(exit)
\ No newline at end of file diff --git a/test/regress/regress0/arith/integers/ackermann2.smt2 b/test/regress/regress0/arith/integers/ackermann2.smt2 new file mode 100644 index 000000000..f20fd99bf --- /dev/null +++ b/test/regress/regress0/arith/integers/ackermann2.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_UFLIA) + +(declare-fun a () Int) +(declare-fun b () Int) + +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) + +(assert (not (= (f (g (f (f a)))) (f (g (f (f b))))))) +(assert (= a b)) + +(check-sat) +(exit) diff --git a/test/regress/regress0/arith/integers/ackermann3.smt2 b/test/regress/regress0/arith/integers/ackermann3.smt2 new file mode 100644 index 000000000..4b4137cb9 --- /dev/null +++ b/test/regress/regress0/arith/integers/ackermann3.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_UFLIA) + +(declare-fun a () Int) +(declare-fun b () Int) + +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) + +(assert (= (f (g (f (f a)))) (f (g (f (f b)))))) +(assert (not (= a b))) + +(check-sat) +(exit) diff --git a/test/regress/regress0/arith/integers/ackermann4.smt2 b/test/regress/regress0/arith/integers/ackermann4.smt2 new file mode 100644 index 000000000..1b76e1075 --- /dev/null +++ b/test/regress/regress0/arith/integers/ackermann4.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_ALIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) + +(define-sort bv () Int) +(define-sort abv () (Array bv bv)) + +(declare-fun v0 () Int) +(declare-fun v1 () Int) +(declare-fun a () abv) +(declare-fun b () abv) +(declare-fun c () abv) + +(assert (not (= (select a (select b (select c v0))) (select a (select b (select c v1)))))) + +(assert (= v0 v1)) + +(check-sat) +(exit)
\ No newline at end of file diff --git a/test/regress/regress0/arith/integers/ackermann5.smt2 b/test/regress/regress0/arith/integers/ackermann5.smt2 new file mode 100644 index 000000000..8b93a3c35 --- /dev/null +++ b/test/regress/regress0/arith/integers/ackermann5.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_UFLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(declare-fun v0 () Int) +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) + +(assert (= (f v0) (g (f v0)))) +(assert (= (f (f v0)) (g (f v0)))) +(assert (= (f (f (f v0))) (g (f v0)))) + +(check-sat) +(exit) diff --git a/test/regress/regress0/arith/integers/ackermann6.smt2 b/test/regress/regress0/arith/integers/ackermann6.smt2 new file mode 100644 index 000000000..62f2f1276 --- /dev/null +++ b/test/regress/regress0/arith/integers/ackermann6.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_UFLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(declare-fun v0 () Int) +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) + +(assert (= (f v0) (g (f v0)))) +(assert (= (f (f v0)) (g (f v0)))) +(assert (not (= (f (f (f v0))) (g (f v0))))) + +(check-sat) +(exit) |