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.

8 files changed, 127 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3045ea35e..d3f463afd 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2,6 +2,7 @@
 # Regression level 0 tests
 
 set(regress_0_tests
+  regress0/arith/ackermann.real.smt2
   regress0/arith/arith.01.cvc
   regress0/arith/arith.02.cvc
   regress0/arith/arith.03.cvc
@@ -16,6 +17,12 @@ set(regress_0_tests
   regress0/arith/div.05.smt2
   regress0/arith/div.07.smt2
   regress0/arith/fuzz_3-eq.smtv1.smt2
+  regress0/arith/integers/ackermann1.smt2
+  regress0/arith/integers/ackermann2.smt2
+  regress0/arith/integers/ackermann3.smt2
+  regress0/arith/integers/ackermann4.smt2
+  regress0/arith/integers/ackermann5.smt2
+  regress0/arith/integers/ackermann6.smt2
   regress0/arith/integers/arith-int-042.cvc
   regress0/arith/integers/arith-int-042.min.cvc
   regress0/arith/leq.01.smtv1.smt2
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)