From 83d07f5d7662557f2087136563606872b217511a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 22 Aug 2018 20:47:27 -0500 Subject: [PATCH] More regressions that increase coverage (#2354) --- test/regress/Makefile.tests | 4 + .../regress1/quantifiers/dump-inst-proof.smt2 | 26 ++++ .../regress1/quantifiers/lra-vts-inf.smt2 | 144 ++++++++++++++++++ .../regress1/quantifiers/qe-partial.smt2 | 9 ++ test/regress/regress1/quantifiers/qe.smt2 | 7 + 5 files changed, 190 insertions(+) create mode 100644 test/regress/regress1/quantifiers/dump-inst-proof.smt2 create mode 100644 test/regress/regress1/quantifiers/lra-vts-inf.smt2 create mode 100644 test/regress/regress1/quantifiers/qe-partial.smt2 create mode 100644 test/regress/regress1/quantifiers/qe.smt2 diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 9f547eb86..ea3a70362 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1282,6 +1282,7 @@ REG1_TESTS = \ regress1/quantifiers/constfunc.cvc \ regress1/quantifiers/dump-inst.smt2 \ regress1/quantifiers/dump-inst-i.smt2 \ + regress1/quantifiers/dump-inst-proof.smt2 \ regress1/quantifiers/ext-ex-deq-trigger.smt2 \ regress1/quantifiers/extract-nproc.smt2 \ regress1/quantifiers/florian-case-ax.smt2 \ @@ -1295,6 +1296,7 @@ REG1_TESTS = \ regress1/quantifiers/isaplanner-goal20.smt2 \ regress1/quantifiers/is-even.smt2 \ regress1/quantifiers/javafe.ast.StmtVec.009.smt2 \ + regress1/quantifiers/lra-vts-inf.smt2 \ regress1/quantifiers/mix-coeff.smt2 \ regress1/quantifiers/model_6_1_bv.smt2 \ regress1/quantifiers/mutualrec2.cvc \ @@ -1323,6 +1325,8 @@ REG1_TESTS = \ regress1/quantifiers/qbv-test-urem-rewrite.smt2 \ regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 \ regress1/quantifiers/qcft-smtlib3dbc51.smt2 \ + regress1/quantifiers/qe.smt2 \ + regress1/quantifiers/qe-partial.smt2 \ regress1/quantifiers/quant-wf-int-ind.smt2 \ regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 \ regress1/quantifiers/repair-const-nterm.smt2 \ diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2 new file mode 100644 index 000000000..c4eedc16f --- /dev/null +++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2 @@ -0,0 +1,26 @@ +; COMMAND-LINE: --dump-instantiations --proof +; EXPECT: unsat +; EXPECT: (instantiation (forall ((x Int)) (or (P x) (Q x)) ) +; EXPECT: ( 2 ) +; EXPECT: ) +; EXPECT: (instantiation (forall ((x Int)) (or (not (S x)) (not (Q x))) ) +; EXPECT: ( 2 ) +; EXPECT: ) +(set-logic UFLIA) +(set-info :status unsat) +(declare-fun P (Int) Bool) +(declare-fun Q (Int) Bool) +(declare-fun R (Int) Bool) +(declare-fun S (Int) Bool) +(declare-fun W (Int) Bool) +(declare-fun U (Int) Bool) +(assert (forall ((x Int)) (or (P x) (Q x)))) +(assert (forall ((x Int)) (or (R x) (W x)))) +(assert (forall ((x Int)) (or (S x) (U x)))) +(assert (forall ((x Int)) (or (not (S x)) (not (Q x))))) +(assert (and (not (R 0)) (not (R 10)) (not (S 1)) (not (P 2)))) +(assert (S 2)) +; This tests that --proof minimizes the instantiations printed out. +; This regression should require only the 2 instantiations above, but +; may try more. +(check-sat) diff --git a/test/regress/regress1/quantifiers/lra-vts-inf.smt2 b/test/regress/regress1/quantifiers/lra-vts-inf.smt2 new file mode 100644 index 000000000..22d6455fb --- /dev/null +++ b/test/regress/regress1/quantifiers/lra-vts-inf.smt2 @@ -0,0 +1,144 @@ +; COMMAND-LINE: --cbqi-use-inf-int --cbqi-use-inf-real +; EXPECT: unsat +(set-info :smt-lib-version 2.6) +(set-logic LRA) +(set-info :source | + Monniaux, David; Quantifier Elimination by Lazy Model Enumeration, CAV 2010 +|) +(set-info :category "random") +; ./Mjollnir_examples/B5/formula_171.m +(set-info :status unsat) +(assert + (forall ((|v17:0| Real) )(forall ((|v16:1| Real) )(forall ((|v15:2| Real) )(forall ((|v14:3| Real) )(forall ((|v13:4| Real) )(forall ((|v12:5| Real) )(exists ((|v11:6| Real) )(exists ((|v10:7| Real) )(exists ((|v9:8| Real) )(exists ((|v8:9| Real) )(exists ((|v7:10| Real) )(exists ((|v6:11| Real) )(forall ((|v5:12| Real) )(forall ((|v4:13| Real) )(forall ((|v3:14| Real) )(forall ((|v2:15| Real) )(forall ((|v1:16| Real) )(forall ((|v0:17| Real) )(let ((?x104 10)) +(let ((?x10 8)) +(let ((?x457 (* ?x10 |v0:17|))) +(let ((?x538 (+ (+ (* (- 7) |v5:12|) (* 14 |v10:7|)) (* (- 19) |v15:2|)))) +(let ((?x49 19)) +(let ((?x27 (- 15))) +(let ((?x310 (* ?x27 |v10:7|))) +(let ((?x532 (+ (+ (+ (* 7 |v12:5|) (* (- 20) |v4:13|)) ?x310) (* 20 |v16:1|)))) +(let ((?x59 (- 16))) +(let ((?x85 (- 13))) +(let ((?x187 (* ?x85 |v3:14|))) +(let ((?x524 (+ (+ (* (- 20) |v5:12|) (* 4 |v13:4|)) (* (- 10) |v2:15|)))) +(let ((?x266 18)) +(let ((?x170 (- 14))) +(let ((?x308 (* ?x170 |v16:1|))) +(let ((?x520 (+ (+ (+ (* (- 19) |v2:15|) (* 13 |v7:10|)) ?x308) (* (- 12) |v1:16|)))) +(let (($x542 (and (and (<= ?x520 ?x266) (<= (+ ?x524 ?x187) ?x59)) (and (<= ?x532 ?x49) (<= (+ ?x538 ?x457) ?x104))))) +(let ((?x158 (- 11))) +(let ((?x79 6)) +(let ((?x290 (* ?x79 |v3:14|))) +(let ((?x512 (+ (+ (+ (* (- 8) |v9:8|) (* (- 9) |v0:17|)) ?x290) (* (- 18) |v8:9|)))) +(let ((?x504 (+ (+ (* (- 18) |v12:5|) (* (- 18) |v10:7|)) (* 15 |v5:12|)))) +(let ((?x14 (- 18))) +(let ((?x100 7)) +(let ((?x471 (* ?x100 |v6:11|))) +(let (($x499 (<= (+ (+ (+ (* (- 8) |v6:11|) (* ?x100 |v2:15|)) |v17:0|) ?x471) ?x14))) +(let ((?x177 (- 3))) +(let ((?x490 (+ (+ (* (- 19) |v14:3|) (* (- 8) |v13:4|)) (* ?x158 |v16:1|)))) +(let (($x515 (and (or (<= (+ ?x490 (* (- 7) |v10:7|)) ?x177) $x499) (or (<= (+ ?x504 (* ?x79 |v0:17|)) ?x266) (<= ?x512 ?x158))))) +(let ((?x479 (+ (+ (* 13 |v4:13|) (* (- 17) |v4:13|)) (* 11 |v3:14|)))) +(let ((?x110 3)) +(let ((?x33 (* ?x14 |v9:8|))) +(let (($x474 (<= (+ (+ (+ (* ?x110 |v0:17|) (* 16 |v7:10|)) ?x471) ?x33) ?x110))) +(let ((?x233 1)) +(let ((?x464 (+ (+ (* ?x158 |v17:0|) (* 4 |v4:13|)) (* (- 5) |v8:9|)))) +(let ((?x24 12)) +(let ((?x458 (+ (+ (+ (* (- 12) |v5:12|) (* 14 |v16:1|)) |v3:14|) ?x457))) +(let (($x484 (or (and (<= ?x458 ?x24) (<= (+ ?x464 (* (- 12) |v4:13|)) ?x233)) (and $x474 (<= (+ ?x479 (* (- 4) |v12:5|)) ?x59))))) +(let ((?x447 (+ (+ (* (- 20) |v14:3|) (* (- 19) |v16:1|)) (* 2 |v2:15|)))) +(let ((?x439 (+ (+ (* ?x10 |v13:4|) (* 4 |v13:4|)) (* (- 7) |v11:6|)))) +(let (($x451 (or (<= (+ ?x439 (* (- 5) |v7:10|)) ?x24) (<= (+ ?x447 (* ?x170 |v14:3|)) ?x110)))) +(let ((?x62 (- 17))) +(let ((?x430 (+ (+ (* (- 1) |v11:6|) (* 5 |v14:3|)) (* ?x104 |v17:0|)))) +(let ((?x190 11)) +(let ((?x424 (+ (+ (+ (* ?x190 |v5:12|) (* (- 10) |v5:12|)) (* ?x27 |v14:3|)) (* 2 |v12:5|)))) +(let (($x485 (or (and (and (<= ?x424 ?x190) (<= (+ ?x430 (* ?x24 |v16:1|)) ?x62)) $x451) $x484))) +(let ((?x164 4)) +(let ((?x415 (+ (+ (* ?x104 |v15:2|) (* (- 6) |v7:10|)) (* 17 |v1:16|)))) +(let ((?x407 (+ (+ (+ (* ?x59 |v11:6|) (* ?x10 |v14:3|)) (* ?x10 |v7:10|)) (* (- 6) |v8:9|)))) +(let ((?x52 16)) +(let ((?x395 (+ (+ (* (- 5) |v12:5|) (* ?x104 |v15:2|)) (* (- 7) |v1:16|)))) +(let ((?x121 (- 8))) +(let ((?x389 (+ (+ (+ (* (- 9) |v13:4|) (* ?x110 |v0:17|)) (* ?x59 |v17:0|)) (* ?x190 |v4:13|)))) +(let ((?x346 (* ?x27 |v16:1|))) +(let ((?x381 (+ (+ (+ (* ?x158 |v12:5|) (* ?x121 |v16:1|)) (* 5 |v0:17|)) ?x346))) +(let (($x410 (and (or (<= ?x381 ?x104) (<= ?x389 ?x121)) (or (<= (+ ?x395 (* 9 |v9:8|)) ?x52) (<= ?x407 ?x110))))) +(let ((?x370 (+ (+ (* (- 2) |v14:3|) (* (- 1) |v15:2|)) (* ?x85 |v6:11|)))) +(let ((?x97 (- 2))) +(let ((?x361 (+ (+ (* ?x27 |v15:2|) (* (- 20) |v4:13|)) (* 20 |v9:8|)))) +(let (($x374 (or (<= (+ ?x361 (* (- 9) |v7:10|)) ?x97) (<= (+ ?x370 (* (- 19) |v17:0|)) ?x52)))) +(let ((?x195 20)) +(let ((?x354 (+ (+ (+ (* ?x49 |v11:6|) (* ?x59 |v2:15|)) (* 17 |v8:9|)) |v17:0|))) +(let ((?x347 (+ (+ (+ (* (- 7) |v7:10|) (* ?x104 |v10:7|)) (* ?x104 |v6:11|)) ?x346))) +(let (($x419 (or (and (or (or (<= ?x347 ?x100) (<= ?x354 ?x195)) $x374) $x410) (<= (+ ?x415 (* ?x27 |v1:16|)) ?x164)))) +(let ((?x151 (- 20))) +(let ((?x333 (* ?x151 |v5:12|))) +(let (($x335 (<= (+ (+ (+ (* ?x104 |v9:8|) (* ?x151 |v3:14|)) (* ?x110 |v13:4|)) ?x333) ?x151))) +(let ((?x327 (+ (+ (+ (* ?x158 |v5:12|) (* ?x266 |v14:3|)) (* (- 12) |v14:3|)) (* 5 |v1:16|)))) +(let ((?x314 (* ?x14 |v13:4|))) +(let (($x319 (<= (+ (+ (+ (* (- 19) |v4:13|) ?x314) (* ?x62 |v15:2|)) ?x314) ?x164))) +(let ((?x311 (+ (+ (+ (* (- 19) |v6:11|) (* 17 |v0:17|)) ?x308) ?x310))) +(let ((?x302 (+ (+ (+ (* ?x121 |v9:8|) (* ?x97 |v3:14|)) (* ?x59 |v11:6|)) (* ?x158 |v9:8|)))) +(let ((?x135 (- 10))) +(let ((?x293 (+ (+ (+ (* ?x27 |v14:3|) (* ?x190 |v7:10|)) ?x290) (* (- 5) |v3:14|)))) +(let ((?x88 (- 5))) +(let (($x288 (<= (+ (+ (+ (* ?x177 |v1:16|) (* ?x135 |v4:13|)) (* ?x135 |v7:10|)) |v14:3|) ?x88))) +(let (($x338 (and (and (and $x288 (<= ?x293 ?x135)) (<= ?x302 ?x59)) (and (or (<= ?x311 ?x158) $x319) (or (<= ?x327 ?x233) $x335))))) +(let ((?x278 (+ (+ (+ (* ?x27 |v12:5|) (* ?x85 |v9:8|)) (* ?x49 |v5:12|)) (* ?x49 |v15:2|)))) +(let ((?x270 (+ (+ (+ (* ?x10 |v14:3|) (* 17 |v6:11|)) (* ?x266 |v7:10|)) (* ?x24 |v9:8|)))) +(let ((?x41 (- 4))) +(let ((?x259 (+ (+ (+ (* ?x100 |v8:9|) (* ?x177 |v6:11|)) (* 2 |v4:13|)) (* 13 |v12:5|)))) +(let ((?x249 (+ (+ (* 13 |v1:16|) (* ?x151 |v3:14|)) (* 17 |v15:2|)))) +(let (($x281 (and (and (<= (+ ?x249 (* ?x62 |v1:16|)) ?x110) (<= ?x259 ?x41)) (and (<= ?x270 ?x104) (<= ?x278 ?x24))))) +(let ((?x228 15)) +(let ((?x241 (+ (+ (+ (* ?x88 |v5:12|) (* ?x49 |v10:7|)) (* ?x27 |v14:3|)) (* 17 |v7:10|)))) +(let ((?x232 (+ (+ (+ (* ?x24 |v17:0|) (* ?x135 |v4:13|)) (* ?x228 |v17:0|)) (* ?x88 |v1:16|)))) +(let ((?x117 (- 19))) +(let ((?x220 (* ?x117 |v2:15|))) +(let (($x222 (<= (+ (+ (+ (* ?x121 |v17:0|) (* ?x190 |v5:12|)) (* ?x190 |v7:10|)) ?x220) ?x104))) +(let ((?x114 (- 1))) +(let ((?x115 (* ?x114 |v1:16|))) +(let ((?x212 (+ (+ (* 0 |v15:2|) (* 5 |v8:9|)) (* ?x110 |v10:7|)))) +(let (($x244 (and (and (<= (+ ?x212 ?x115) ?x10) $x222) (and (<= ?x232 ?x233) (<= ?x241 ?x228))))) +(let ((?x128 2)) +(let ((?x202 (+ (+ (+ (* ?x195 |v10:7|) (* ?x121 |v10:7|)) (* ?x135 |v4:13|)) (* 17 |v12:5|)))) +(let (($x193 (<= (+ (+ (+ (* ?x151 |v12:5|) (* ?x114 |v4:13|)) ?x187) (* ?x190 |v12:5|)) ?x110))) +(let ((?x181 (+ (+ (+ (* ?x110 |v6:11|) (* ?x164 |v15:2|)) (* ?x177 |v11:6|)) (* ?x10 |v9:8|)))) +(let (($x173 (<= (+ (+ (+ (* ?x164 |v10:7|) |v9:8|) (* ?x104 |v5:12|)) (* ?x170 |v6:11|)) ?x24))) +(let ((?x161 14)) +(let ((?x160 (+ (+ (+ (* ?x151 |v8:9|) (* ?x128 |v16:1|)) (* ?x14 |v12:5|)) (* ?x158 |v0:17|)))) +(let (($x206 (and (<= ?x160 ?x161) (or (or $x173 (<= ?x181 ?x158)) (and $x193 (<= ?x202 ?x128)))))) +(let ((?x144 (+ (+ (+ (* ?x135 |v1:16|) (* ?x14 |v4:13|)) (* ?x10 |v12:5|)) (* 0 |v17:0|)))) +(let ((?x132 (+ (+ (+ (* ?x121 |v8:9|) (* 5 |v17:0|)) (* ?x128 |v13:4|)) (* 13 |v13:4|)))) +(let (($x118 (<= (+ (+ (+ (* ?x104 |v15:2|) (* ?x41 |v7:10|)) (* ?x110 |v6:11|)) ?x115) ?x117))) +(let ((?x98 (* ?x97 |v14:3|))) +(let ((?x99 (+ (+ (+ (* ?x85 |v17:0|) (* ?x88 |v15:2|)) (* 0 |v1:16|)) ?x98))) +(let ((?x78 (+ (+ (+ (* ?x14 |v7:10|) (* (- 7) |v0:17|)) |v3:14|) (* (- 12) |v17:0|)))) +(let ((?x61 (+ (+ (+ (* ?x49 |v8:9|) (* ?x52 |v10:7|)) (* ?x24 |v1:16|)) (* ?x59 |v1:16|)))) +(let ((?x36 13)) +(let (($x44 (<= (+ (+ (+ (* ?x10 |v11:6|) ?x33) (* ?x36 |v15:2|)) (* ?x41 |v2:15|)) ?x36))) +(let ((?x26 (+ (+ (+ (* ?x10 |v16:1|) (* ?x14 |v5:12|)) (* 17 |v10:7|)) (* ?x24 |v13:4|)))) +(let (($x148 (or (and (and (<= ?x26 ?x27) $x44) (and (<= ?x61 ?x62) (<= ?x78 ?x79))) (or (and (<= ?x99 ?x100) $x118) (and (<= ?x132 ?x41) (<= ?x144 ?x104)))))) +(or (and (and $x148 $x206) (and (or $x244 $x281) $x338)) (and $x419 (or $x485 (and $x515 $x542))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +) +) +) +) +) +) +) +) +) +) +) +) +) +) +) +) +) +) +(check-sat) +(exit) diff --git a/test/regress/regress1/quantifiers/qe-partial.smt2 b/test/regress/regress1/quantifiers/qe-partial.smt2 new file mode 100644 index 000000000..6f414fb2c --- /dev/null +++ b/test/regress/regress1/quantifiers/qe-partial.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: +; SCRUBBER: sed -e 's/(not (>= (+ .* (\* (- 1) .*)) 1))$/(not (>= (+ TERMA (\* (- 1) TERMB)) 1))/' +; EXPECT: (not (>= (+ TERMA (* (- 1) TERMB)) 1)) +(set-logic LIA) +(set-info :status unsat) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(get-qe-disjunct (exists ((x Int)) (and (<= a x) (or (<= x b) (<= x c))))) diff --git a/test/regress/regress1/quantifiers/qe.smt2 b/test/regress/regress1/quantifiers/qe.smt2 new file mode 100644 index 000000000..673ece05b --- /dev/null +++ b/test/regress/regress1/quantifiers/qe.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: +; EXPECT: (not (>= (+ a (* (- 1) b)) 1)) +(set-logic LIA) +(set-info :status unsat) +(declare-fun a () Int) +(declare-fun b () Int) +(get-qe (exists ((x Int)) (and (<= a x) (<= x b)))) -- 2.30.2