From d3e45c1fd1ef3f56f15ad08c783a3d5c54ea10c1 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 3 Feb 2020 22:42:27 -0800 Subject: [PATCH] Regression tests for arithmetic proofs. (#3701) * 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 | 6 ++++ test/regress/regress0/arith/arith-eq.smt2 | 14 ++++++++ .../arith/arith-mixed-types-no-tighten.smt2 | 18 +++++++++++ .../arith/arith-mixed-types-tighten.smt2 | 32 +++++++++++++++++++ test/regress/regress0/arith/arith-mixed.smt2 | 14 ++++++++ test/regress/regress0/arith/arith-strict.smt2 | 13 ++++++++ .../regress0/arith/arith-tighten-1.smt2 | 17 ++++++++++ 7 files changed, 114 insertions(+) create mode 100644 test/regress/regress0/arith/arith-eq.smt2 create mode 100644 test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2 create mode 100644 test/regress/regress0/arith/arith-mixed-types-tighten.smt2 create mode 100644 test/regress/regress0/arith/arith-mixed.smt2 create mode 100644 test/regress/regress0/arith/arith-strict.smt2 create mode 100644 test/regress/regress0/arith/arith-tighten-1.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 20272de2b..35d604768 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -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 index 000000000..661c3f242 --- /dev/null +++ b/test/regress/regress0/arith/arith-eq.smt2 @@ -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 index 000000000..a06621224 --- /dev/null +++ b/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2 @@ -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 index 000000000..2f737d5c5 --- /dev/null +++ b/test/regress/regress0/arith/arith-mixed-types-tighten.smt2 @@ -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 index 000000000..5869a51bd --- /dev/null +++ b/test/regress/regress0/arith/arith-mixed.smt2 @@ -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 index 000000000..969cfd0bb --- /dev/null +++ b/test/regress/regress0/arith/arith-strict.smt2 @@ -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 index 000000000..237d5b144 --- /dev/null +++ b/test/regress/regress0/arith/arith-tighten-1.smt2 @@ -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) + -- 2.30.2