diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-09 16:14:31 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-09 16:14:42 -0600 |
commit | 19697d530ae6eaf0165270bc3628f76124a45953 (patch) | |
tree | baa129ef51cc45295dc9f2f7cc176ca27768f4f9 /test/regress/regress0/quantifiers | |
parent | b3f5d2860747c2608c0d765d105c8dd32ee57e1d (diff) |
More complete guess instantiation strategy, cvc4 now typically times out instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc
Diffstat (limited to 'test/regress/regress0/quantifiers')
-rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/ex1.smt2 | 13 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/ex1.smt2.expect | 2 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/ex7.smt2 | 13 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/ex7.smt2.expect | 2 |
5 files changed, 0 insertions, 32 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 93d513d9f..c478248da 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -28,10 +28,8 @@ TESTS = \ bug269.smt2 \ burns13.smt2 \ burns4.smt2 \ - ex1.smt2 \ ex3.smt2 \ ex6.smt2 \ - ex7.smt2 \ opisavailable-12.smt2 \ ricart-agrawala6.smt2 \ set8.smt2 \ diff --git a/test/regress/regress0/quantifiers/ex1.smt2 b/test/regress/regress0/quantifiers/ex1.smt2 deleted file mode 100644 index 20230a6fa..000000000 --- a/test/regress/regress0/quantifiers/ex1.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/quantifiers/ex1.smt2.expect b/test/regress/regress0/quantifiers/ex1.smt2.expect deleted file mode 100644 index 2bd8349de..000000000 --- a/test/regress/regress0/quantifiers/ex1.smt2.expect +++ /dev/null @@ -1,2 +0,0 @@ -% EXPECT: unknown -% EXPECT: (:reason-unknown incomplete) diff --git a/test/regress/regress0/quantifiers/ex7.smt2 b/test/regress/regress0/quantifiers/ex7.smt2 deleted file mode 100644 index 11a83fdc4..000000000 --- a/test/regress/regress0/quantifiers/ex7.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 c () U) -(declare-fun f (U) U) -(assert (and (= a b) (forall ((x U)) (=> (or (= (f x) c) (= x a)) (= x b))))) -(check-sat) -(get-info :reason-unknown) -(exit) diff --git a/test/regress/regress0/quantifiers/ex7.smt2.expect b/test/regress/regress0/quantifiers/ex7.smt2.expect deleted file mode 100644 index 2bd8349de..000000000 --- a/test/regress/regress0/quantifiers/ex7.smt2.expect +++ /dev/null @@ -1,2 +0,0 @@ -% EXPECT: unknown -% EXPECT: (:reason-unknown incomplete) |