From 9c7f01d8dd7baf7ff8cbdd2e32fd2bf6d9495229 Mon Sep 17 00:00:00 2001 From: Hossein Hojjat Date: Wed, 31 May 2017 17:25:28 -0400 Subject: [PATCH] simple adt --- regression-tests/horn-adt/simple-adt-horn.smt2 | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 regression-tests/horn-adt/simple-adt-horn.smt2 diff --git a/regression-tests/horn-adt/simple-adt-horn.smt2 b/regression-tests/horn-adt/simple-adt-horn.smt2 new file mode 100644 index 00000000..2f01d0a7 --- /dev/null +++ b/regression-tests/horn-adt/simple-adt-horn.smt2 @@ -0,0 +1,17 @@ +(set-logic HORN) + +(declare-datatype Pair ( (P (left Int) (right Bool)) )) + +(declare-fun I1 (Pair) Bool) +(declare-fun I2 (Pair) Bool) + +(assert (I1 (P 0 true))) +(assert (forall ((p Pair)) + (=> (I1 p) (I2 (P (+ (left p) 1) (not (right p))))))) +(assert (forall ((p Pair)) + (=> (I2 p) (I1 (P (* (left p) 2) (not (right p))))))) + +(assert (forall ((p Pair)) + (=> (I1 p) (and (>= (left p) 0) (right p))))) + +(check-sat)