diff options
Diffstat (limited to 'test/regress/regress0/decision')
7 files changed, 1 insertions, 132 deletions
diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am index ccf86e8b4..b70ee1575 100644 --- a/test/regress/regress0/decision/Makefile.am +++ b/test/regress/regress0/decision/Makefile.am @@ -23,7 +23,6 @@ TESTS = \ bitvec0.smt \ bitvec0.delta01.smt \ bitvec5.smt \ - quant-Arrays_Q1-noinfer.smt2 \ quant-ex1.smt2 \ uflia-xs-09-16-3-4-1-5.delta03.smt \ aufbv-fuzz01.smt \ @@ -46,17 +45,14 @@ EXTRA_DIST = $(TESTS) \ uflia-xs-09-16-3-4-1-5.delta03.smt.expect \ bitvec0.smt.expect \ bitvec5.smt.expect \ - quant-Arrays_Q1-noinfer.smt2.expect \ wchains010ue.delta02.smt.expect \ bug347.smt.expect \ bug374a.smt.expect \ bug374b.smt2.expect \ - quant-ex1.disable_miniscope.smt2.expect \ wchains010ue.smt.expect \ just_sat.expect \ quant-ex1.smt2.expect \ - just_unsat.expect \ - quant-symmetric_unsat_7.smt2.expect + just_unsat.expect #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/regress/regress0/decision/quant-Arrays_Q1-noinfer.smt2 b/test/regress/regress0/decision/quant-Arrays_Q1-noinfer.smt2 deleted file mode 100644 index 3398f5f84..000000000 --- a/test/regress/regress0/decision/quant-Arrays_Q1-noinfer.smt2 +++ /dev/null @@ -1,73 +0,0 @@ -(set-logic AUFLIA) -(set-info :source | - Boogie/Spec# benchmarks. - This benchmark was translated by Michal Moskal. -|) -(set-info :smt-lib-version 2.0) -(set-info :category "industrial") -(set-info :status unsat) -(declare-fun InRange (Int Int) Bool) -(declare-fun o () Int) -(declare-fun q () Int) -(declare-fun int_18446744073709551615 () Int) -(declare-fun Smt.false () Int) -(declare-fun anyEqual (Int Int) Int) -(declare-fun y () Int) -(declare-fun select1 (Int Int) Int) -(declare-fun select2 (Int Int Int) Int) -(declare-fun CONCVARSYM (Int) Int) -(declare-fun divides (Int Int) Int) -(declare-fun intAtMost (Int Int) Int) -(declare-fun subtypes (Int Int) Bool) -(declare-fun store1 (Int Int Int) Int) -(declare-fun store2 (Int Int Int Int) Int) -(declare-fun B_0 () Int) -(declare-fun B_1 () Int) -(declare-fun intAtLeast (Int Int) Int) -(declare-fun int_2147483647 () Int) -(declare-fun boolOr (Int Int) Int) -(declare-fun ReallyLastGeneratedExit_correct () Int) -(declare-fun int_m9223372036854775808 () Int) -(declare-fun Smt.true () Int) -(declare-fun int_4294967295 () Int) -(declare-fun start_correct () Int) -(declare-fun B () Int) -(declare-fun F () Int) -(declare-fun G () Int) -(declare-fun boolAnd (Int Int) Int) -(declare-fun boolNot (Int) Int) -(declare-fun k_0 () Int) -(declare-fun intLess (Int Int) Int) -(declare-fun intGreater (Int Int) Int) -(declare-fun anyNeq (Int Int) Int) -(declare-fun is (Int Int) Int) -(declare-fun int_m2147483648 () Int) -(declare-fun modulo (Int Int) Int) -(declare-fun boolImplies (Int Int) Int) -(declare-fun boolIff (Int Int) Int) -(declare-fun int_9223372036854775807 () Int) -(assert true) -(assert true) -(assert (forall ((?A Int) (?i Int) (?v Int)) (= (select1 (store1 ?A ?i ?v) ?i) ?v))) -(assert (forall ((?A Int) (?i Int) (?j Int) (?v Int)) (=> (not (= ?i ?j)) (= (select1 (store1 ?A ?i ?v) ?j) (select1 ?A ?j))))) -(assert (forall ((?A Int) (?o Int) (?f Int) (?v Int)) (= (select2 (store2 ?A ?o ?f ?v) ?o ?f) ?v))) -(assert (forall ((?A Int) (?o Int) (?f Int) (?p Int) (?g Int) (?v Int)) (=> (not (= ?o ?p)) (= (select2 (store2 ?A ?o ?f ?v) ?p ?g) (select2 ?A ?p ?g))))) -(assert (forall ((?A Int) (?o Int) (?f Int) (?p Int) (?g Int) (?v Int)) (=> (not (= ?f ?g)) (= (select2 (store2 ?A ?o ?f ?v) ?p ?g) (select2 ?A ?p ?g))))) -(assert (forall ((?x Int) (?y Int)) (= (= (boolIff ?x ?y) Smt.true) (= (= ?x Smt.true) (= ?y Smt.true))))) -(assert (forall ((?x Int) (?y Int)) (= (= (boolImplies ?x ?y) Smt.true) (=> (= ?x Smt.true) (= ?y Smt.true))))) -(assert (forall ((?x Int) (?y Int)) (= (= (boolAnd ?x ?y) Smt.true) (and (= ?x Smt.true) (= ?y Smt.true))))) -(assert (forall ((?x Int) (?y Int)) (= (= (boolOr ?x ?y) Smt.true) (or (= ?x Smt.true) (= ?y Smt.true))))) -(assert (forall ((?x Int)) (! (= (= (boolNot ?x) Smt.true) (not (= ?x Smt.true))) :pattern ((boolNot ?x)) ))) -(assert (forall ((?x Int) (?y Int)) (= (= (anyEqual ?x ?y) Smt.true) (= ?x ?y)))) -(assert (forall ((?x Int) (?y Int)) (! (= (= (anyNeq ?x ?y) Smt.true) (not (= ?x ?y))) :pattern ((anyNeq ?x ?y)) ))) -(assert (forall ((?x Int) (?y Int)) (= (= (intLess ?x ?y) Smt.true) (< ?x ?y)))) -(assert (forall ((?x Int) (?y Int)) (= (= (intAtMost ?x ?y) Smt.true) (<= ?x ?y)))) -(assert (forall ((?x Int) (?y Int)) (= (= (intAtLeast ?x ?y) Smt.true) (>= ?x ?y)))) -(assert (forall ((?x Int) (?y Int)) (= (= (intGreater ?x ?y) Smt.true) (> ?x ?y)))) -(assert (distinct Smt.false Smt.true)) -(assert (forall ((?t Int)) (! (subtypes ?t ?t) :pattern ((subtypes ?t ?t)) ))) -(assert (forall ((?t Int) (?u Int) (?v Int)) (! (=> (and (subtypes ?t ?u) (subtypes ?u ?v)) (subtypes ?t ?v)) :pattern ((subtypes ?t ?u) (subtypes ?u ?v)) ))) -(assert (forall ((?t Int) (?u Int)) (! (=> (and (subtypes ?t ?u) (subtypes ?u ?t)) (= ?t ?u)) :pattern ((subtypes ?t ?u) (subtypes ?u ?t)) ))) -(assert (let ((?v_0 (forall ((?p Int) (?f Int)) (or (= (select2 B_1 ?p ?f) (select2 B ?p ?f)) (and (= ?p o) (= ?f F))))) (?v_1 (= ReallyLastGeneratedExit_correct Smt.true)) (?v_2 (= start_correct Smt.true))) (not (=> (=> (=> true (=> (= k_0 (select2 B q G)) (=> (= B_0 (store2 B o F (+ y (select2 B o F)))) (=> (= B_1 (store2 B_0 q G k_0)) (=> (=> (=> true (and ?v_0 (=> ?v_0 (=> true true)))) ?v_1) ?v_1))))) ?v_2) ?v_2)))) -(check-sat) -(exit) diff --git a/test/regress/regress0/decision/quant-Arrays_Q1-noinfer.smt2.expect b/test/regress/regress0/decision/quant-Arrays_Q1-noinfer.smt2.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress0/decision/quant-Arrays_Q1-noinfer.smt2.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat diff --git a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 deleted file mode 100644 index 20230a6fa..000000000 --- a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 +++ /dev/null @@ -1,13 +0,0 @@ -(set-logic AUFLIRA) -(set-info :smt-lib-version 2.0) -(set-info :category "industrial") -(set-info :status sat) -(declare-sort U 0) -(declare-fun a () U) -(declare-fun b () U) -(declare-fun f (U) U) -(declare-fun p () Bool) -(assert (and (= a b) (forall ((x U)) (=> (and (= (f x) a) (not (= (f x) b))) p)))) -(check-sat) -(get-info :reason-unknown) -(exit) diff --git a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect deleted file mode 100644 index 064291040..000000000 --- a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --decision=justification --disable-miniscope-quant-fv --disable-miniscope-quant -% EXPECT: unknown -% EXPECT: (:reason-unknown incomplete) diff --git a/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2 b/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2 deleted file mode 100644 index 6acf4a3c6..000000000 --- a/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -(set-logic AUFLIRA) -(set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods. - -It was translated to SMT-LIB by Leonardo de Moura |) -(set-info :smt-lib-version 2.0) -(set-info :category "crafted") -(set-info :status unsat) -(declare-fun symmetric ((Array Int (Array Int Real)) Int) Bool) -(declare-fun n () Int) -(declare-fun a0 () (Array Int (Array Int Real))) -(declare-fun e0 () Real) -(declare-fun a1 () (Array Int (Array Int Real))) -(declare-fun e1 () Real) -(declare-fun a2 () (Array Int (Array Int Real))) -(declare-fun e2 () Real) -(declare-fun a3 () (Array Int (Array Int Real))) -(declare-fun e3 () Real) -(declare-fun a4 () (Array Int (Array Int Real))) -(declare-fun e4 () Real) -(declare-fun a5 () (Array Int (Array Int Real))) -(declare-fun e5 () Real) -(declare-fun a6 () (Array Int (Array Int Real))) -(declare-fun e6 () Real) -(assert (forall ((?a (Array Int (Array Int Real))) (?n Int)) (= (symmetric ?a ?n) (forall ((?i Int) (?j Int)) (=> (and (<= 1 ?i) (<= ?i ?n) (<= 1 ?j) (<= ?j ?n)) (= (select (select ?a ?i) ?j) (select (select ?a ?j) ?i))))))) -(assert (symmetric a0 n)) -(assert (= a1 (store a0 0 (store (select a0 0) 0 e0)))) -(assert (= a2 (store a1 1 (store (select a1 1) 1 e1)))) -(assert (= a3 (store a2 2 (store (select a2 2) 2 e2)))) -(assert (= a4 (store a3 3 (store (select a3 3) 3 e3)))) -(assert (= a5 (store a4 4 (store (select a4 4) 4 e4)))) -(assert (= a6 (store a5 5 (store (select a5 5) 5 e5)))) -(assert (not (symmetric a6 n))) -(check-sat) -(exit) diff --git a/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2.expect b/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat |