Regression tests for arithmetic proofs. (#3701)
authorAlex Ozdemir <aozdemir@hmc.edu>
Tue, 4 Feb 2020 06:42:27 +0000 (22:42 -0800)
committerGitHub <noreply@github.com>
Tue, 4 Feb 2020 06:42:27 +0000 (22:42 -0800)
* Add more arith proof regression tests

These tests are designed to test interesting cases of arithmetic proofs,
such as mixing integers and reals and tightening bounds.

Right now, they have the --no-check-proofs flag set, which prevents them
from testing the proof machinery. However, once we check that machinery
into master, we'll remove that flag, thus enabling the full effect of
the tests.

* A few comments explaining things.

* Add another tightening test

* Add new test to CMake

* No --no-check-models. There are no models anyway.

* Delete smt-lib-version, per Yoni

test/regress/CMakeLists.txt
test/regress/regress0/arith/arith-eq.smt2 [new file with mode: 0644]
test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2 [new file with mode: 0644]
test/regress/regress0/arith/arith-mixed-types-tighten.smt2 [new file with mode: 0644]
test/regress/regress0/arith/arith-mixed.smt2 [new file with mode: 0644]
test/regress/regress0/arith/arith-strict.smt2 [new file with mode: 0644]
test/regress/regress0/arith/arith-tighten-1.smt2 [new file with mode: 0644]

index 20272de2b8a5d155ee525422b70da2433f4f5934..35d60476838afb91fdc182d7cde9f2b48b97dbc0 100644 (file)
@@ -3,6 +3,12 @@
 
 set(regress_0_tests
   regress0/arith/ackermann.real.smt2
+  regress0/arith/arith-eq.smt2
+  regress0/arith/arith-mixed.smt2
+  regress0/arith/arith-tighten-1.smt2
+  regress0/arith/arith-strict.smt2
+  regress0/arith/arith-mixed-types-tighten.smt2
+  regress0/arith/arith-mixed-types-no-tighten.smt2
   regress0/arith/arith.01.cvc
   regress0/arith/arith.02.cvc
   regress0/arith/arith.03.cvc
diff --git a/test/regress/regress0/arith/arith-eq.smt2 b/test/regress/regress0/arith/arith-eq.smt2
new file mode 100644 (file)
index 0000000..661c3f2
--- /dev/null
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_LRA)
+
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun z () Real)
+
+(assert (= z 0))
+(assert (= (* 3 x) y))
+(assert (= (+ 1 (* 5 x)) y))
+(assert (= (+ 7 (* 4 x)) y))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2 b/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2
new file mode 100644 (file)
index 0000000..a066212
--- /dev/null
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_LIRA)
+
+(declare-fun x () Real)
+(declare-fun n () Int)
+
+; Even though `n` is an integer, this would be UNSAT for real `n`, so the integrality can be ignored.
+(assert
+    (and
+        (>= (+ x n) 1)
+        (<= n 0)
+        (<= x 0)
+    )
+)
+
+(check-sat)
+
diff --git a/test/regress/regress0/arith/arith-mixed-types-tighten.smt2 b/test/regress/regress0/arith/arith-mixed-types-tighten.smt2
new file mode 100644 (file)
index 0000000..2f737d5
--- /dev/null
@@ -0,0 +1,32 @@
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_LIRA)
+
+(declare-fun x_44 () Real)
+(declare-fun x_45 () Real)
+
+; This test is a subset of one of the `../lemmas` tests. I think `../lemmas/sc_init_frame_gap.induction.smtv1.smt2`.
+(declare-fun termITE_30 () Int)
+(declare-fun termITE_3 () Real)
+(declare-fun termITE_4 () Real)
+(declare-fun termITE_8 () Real)
+(declare-fun termITE_9 () Real)
+(declare-fun termITE_31 () Int)
+
+(assert
+    (let ((_let_0 (* (- 1.0) termITE_3)))
+        (and
+            (>= (+ termITE_8 (* (- 1.0) termITE_9)) 0.0)
+            ; This literal can be tightened to `termITE_31 <= 1`.
+            (not (>= termITE_31 2))
+            (>= (+ (* (- 1.0) x_44) (/ termITE_31 1)) 0.0)
+            (>= (+ x_44 (* (- 1.0) termITE_4)) 0.0)
+            (not (>= (+ _let_0 (* (/ 1 2) termITE_8)) 0.0))
+            (>= (+ (* (- 1.0) x_45) termITE_9) 0.0)
+            (>= (+ x_45 (/ (* (- 1) termITE_30) 1)) 0.0)
+            (>= termITE_30 2)
+            (>= (+ _let_0 termITE_4) 0.0)))
+)
+
+(check-sat)
+
diff --git a/test/regress/regress0/arith/arith-mixed.smt2 b/test/regress/regress0/arith/arith-mixed.smt2
new file mode 100644 (file)
index 0000000..5869a51
--- /dev/null
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_LRA)
+
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun z () Real)
+
+; Both strict and non-strict inequalities.
+(assert (< y 0))
+(assert (>= y x))
+(assert (>= y (- x)))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/arith-strict.smt2 b/test/regress/regress0/arith/arith-strict.smt2
new file mode 100644 (file)
index 0000000..969cfd0
--- /dev/null
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_LRA)
+
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun z () Real)
+
+(assert (< y 0))
+(assert (> y x))
+(assert (> y (- x)))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/arith-tighten-1.smt2 b/test/regress/regress0/arith/arith-tighten-1.smt2
new file mode 100644 (file)
index 0000000..237d5b1
--- /dev/null
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_LIRA)
+
+(declare-fun n () Int)
+
+; tests tightenings of the form [Int] >= r   to [Int] >= ceiling(r)
+; where r is a real.
+(assert
+    (and
+        (>= n 1.5)
+        (<= n 1.9)
+    )
+)
+
+(check-sat)
+