From 00ccc01140bcdeaadedf8ae1b9f224ccdc812bc0 Mon Sep 17 00:00:00 2001 From: Ying Sheng Date: Tue, 8 Oct 2019 08:18:21 -0700 Subject: 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. --- test/regress/regress0/arith/ackermann.real.smt2 | 19 +++++++++++++++++++ .../regress0/arith/integers/ackermann1.smt2 | 19 +++++++++++++++++++ .../regress0/arith/integers/ackermann2.smt2 | 15 +++++++++++++++ .../regress0/arith/integers/ackermann3.smt2 | 15 +++++++++++++++ .../regress0/arith/integers/ackermann4.smt2 | 22 ++++++++++++++++++++++ .../regress0/arith/integers/ackermann5.smt2 | 15 +++++++++++++++ .../regress0/arith/integers/ackermann6.smt2 | 15 +++++++++++++++ 7 files changed, 120 insertions(+) create mode 100644 test/regress/regress0/arith/ackermann.real.smt2 create mode 100644 test/regress/regress0/arith/integers/ackermann1.smt2 create mode 100644 test/regress/regress0/arith/integers/ackermann2.smt2 create mode 100644 test/regress/regress0/arith/integers/ackermann3.smt2 create mode 100644 test/regress/regress0/arith/integers/ackermann4.smt2 create mode 100644 test/regress/regress0/arith/integers/ackermann5.smt2 create mode 100644 test/regress/regress0/arith/integers/ackermann6.smt2 (limited to 'test/regress/regress0') diff --git a/test/regress/regress0/arith/ackermann.real.smt2 b/test/regress/regress0/arith/ackermann.real.smt2 new file mode 100644 index 000000000..00dd79ebe --- /dev/null +++ b/test/regress/regress0/arith/ackermann.real.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_UFNRA) + +(declare-fun a () Real) +(declare-fun b () Real) + +(declare-fun f (Real) Real) +(declare-fun g (Real) Real) + +(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/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) -- cgit v1.2.3