diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-10 10:31:47 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-10 10:33:24 -0500 |
commit | c431410d0bd4a688d5d446f906d80634424dcd53 (patch) | |
tree | 8b13a5598a0ed201744e0a44669f8ade1eac2af3 /test | |
parent | fccff6adcc0a69273a54110596214f7927a96033 (diff) |
Add support for cardinality constraints logic UFC. Add regressions in fmf/. Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/bug512.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt | 2 | ||||
-rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 11 | ||||
-rw-r--r-- | test/regress/regress0/fmf/QEpres-uf.855035.smt | 2 | ||||
-rwxr-xr-x | test/regress/regress0/fmf/fc-pigeonhole19.smt2 | 20 | ||||
-rwxr-xr-x | test/regress/regress0/fmf/fc-simple.smt2 | 12 | ||||
-rwxr-xr-x | test/regress/regress0/fmf/fc-unsat-pent.smt2 | 20 | ||||
-rwxr-xr-x | test/regress/regress0/fmf/fc-unsat-tot-2.smt2 | 14 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/bug269.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/burns13.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/rewriterules/Makefile.am | 6 | ||||
-rwxr-xr-x | test/regress/regress0/rewriterules/read5.smt2 | 35 | ||||
-rw-r--r-- | test/regress/regress0/tptp/Makefile.am | 2 |
13 files changed, 120 insertions, 10 deletions
diff --git a/test/regress/regress0/bug512.smt2 b/test/regress/regress0/bug512.smt2 index b0c970f37..1c8a0626a 100644 --- a/test/regress/regress0/bug512.smt2 +++ b/test/regress/regress0/bug512.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --tlimit-per 2500 -iq ; EXPECT: unknown -; EXPECT: (:reason-unknown timeout) +; EXPECT: (:reason-unknown incomplete) ; EXPECT: unsat (set-option :print-success false) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt index 536bc241f..f62f057e4 100644 --- a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt +++ b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt @@ -1,4 +1,4 @@ -% COMMAND-LINE: --finite-model-find +% COMMAND-LINE: --finite-model-find --mbqi=gen-ev % EXPECT: unsat (benchmark Isabelle :status sat diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index b9a87231f..395054d67 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -23,18 +23,23 @@ TESTS = \ agree466.smt2 \ ALG008-1.smt2 \ german169.smt2 \ - Hoare-z3.931718.smt \ QEpres-uf.855035.smt \ agree467.smt2 \ Arrow_Order-smtlib.778341.smt \ german73.smt2 \ PUZ001+1.smt2 \ refcount24.cvc.smt2 \ - bug0909.smt2 \ - fmf-bound-int.smt2 + fmf-bound-int.smt2 \ + fc-simple.smt2 \ + fc-unsat-tot-2.smt2 \ + fc-unsat-pent.smt2 \ + fc-pigeonhole19.smt2 EXTRA_DIST = $(TESTS) +# disabled for now : +# Hoare-z3.931718.smt bug0909.smt2 + #if CVC4_BUILD_PROFILE_COMPETITION #else #TESTS += \ diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smt b/test/regress/regress0/fmf/QEpres-uf.855035.smt index 980e5fd49..2945c8f4d 100644 --- a/test/regress/regress0/fmf/QEpres-uf.855035.smt +++ b/test/regress/regress0/fmf/QEpres-uf.855035.smt @@ -1,4 +1,4 @@ -% COMMAND-LINE: --finite-model-find +% COMMAND-LINE: --finite-model-find --mbqi=gen-ev % EXPECT: sat (benchmark Isabelle :status sat diff --git a/test/regress/regress0/fmf/fc-pigeonhole19.smt2 b/test/regress/regress0/fmf/fc-pigeonhole19.smt2 new file mode 100755 index 000000000..15c36682c --- /dev/null +++ b/test/regress/regress0/fmf/fc-pigeonhole19.smt2 @@ -0,0 +1,20 @@ +(set-logic UFC)
+(set-info :status unsat)
+
+(declare-sort P 0)
+(declare-sort H 0)
+
+(declare-fun p () P)
+(declare-fun h () H)
+
+; pigeonhole using native cardinality constraints
+(assert (fmf.card p 19))
+(assert (not (fmf.card p 18)))
+(assert (fmf.card h 18))
+(assert (not (fmf.card h 17)))
+
+; each pigeon has different holes
+(declare-fun f (P) H)
+(assert (forall ((p1 P) (p2 P)) (=> (not (= p1 p2)) (not (= (f p1) (f p2))))))
+
+(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/fmf/fc-simple.smt2 b/test/regress/regress0/fmf/fc-simple.smt2 new file mode 100755 index 000000000..d1fd2301c --- /dev/null +++ b/test/regress/regress0/fmf/fc-simple.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_UFC) +(set-info :status unsat) + +(declare-sort U 0) + +(declare-fun a () U) +(declare-fun c () U) + +(assert (fmf.card c 2)) +(assert (not (fmf.card a 4))) + +(check-sat) diff --git a/test/regress/regress0/fmf/fc-unsat-pent.smt2 b/test/regress/regress0/fmf/fc-unsat-pent.smt2 new file mode 100755 index 000000000..f1721cb04 --- /dev/null +++ b/test/regress/regress0/fmf/fc-unsat-pent.smt2 @@ -0,0 +1,20 @@ +(set-logic QF_UFC)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(declare-fun e () U)
+
+(assert (not (= a b)))
+(assert (not (= b c)))
+(assert (not (= c d)))
+(assert (not (= d e)))
+(assert (not (= e a)))
+
+(assert (fmf.card c 2))
+
+(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 new file mode 100755 index 000000000..d946974ed --- /dev/null +++ b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 @@ -0,0 +1,14 @@ +(set-logic UFC)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+
+(assert (not (fmf.card a 2)))
+
+(assert (forall ((x U)) (or (= x a) (= x b))))
+
+(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/quantifiers/bug269.smt2 b/test/regress/regress0/quantifiers/bug269.smt2 index 0d5aedbb3..2e50030d1 100644 --- a/test/regress/regress0/quantifiers/bug269.smt2 +++ b/test/regress/regress0/quantifiers/bug269.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat (set-logic LRA) (set-info :status unsat) (declare-fun x4 () Real) diff --git a/test/regress/regress0/quantifiers/burns13.smt2 b/test/regress/regress0/quantifiers/burns13.smt2 index ad970a2b2..3424c161e 100644 --- a/test/regress/regress0/quantifiers/burns13.smt2 +++ b/test/regress/regress0/quantifiers/burns13.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant --decision=internal +; EXPECT: unsat (set-logic AUFLIA) (set-info :source | Burns mutual exclusion protocol. This is a benchmark of the haRVey theorem prover. It was translated to SMT-LIB by Leonardo de Moura |) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am index 3a3a097bd..31f99905c 100644 --- a/test/regress/regress0/rewriterules/Makefile.am +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -23,16 +23,16 @@ MAKEFLAGS = -k # put it below in "TESTS +=" TESTS = \ length_trick.smt2 \ - length_trick2.smt2 \ length_gen_020.smt2 \ datatypes.smt2 \ datatypes_sat.smt2 \ reachability_back_to_the_future.smt2 \ relation.smt2 \ simulate_rewriting.smt2 \ - native_arrays.smt2 + native_arrays.smt2 \ + read5.smt2 -# reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2 +# length_trick2.smt2 reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/rewriterules/read5.smt2 b/test/regress/regress0/rewriterules/read5.smt2 new file mode 100755 index 000000000..e66df7c7e --- /dev/null +++ b/test/regress/regress0/rewriterules/read5.smt2 @@ -0,0 +1,35 @@ +(set-logic AUF) +(set-info :source | +Translated from old SVC processor verification benchmarks. Contact Clark +Barrett at barrett@cs.nyu.edu for more information. + +This benchmark was automatically translated into SMT-LIB format from +CVC format using CVC Lite +|) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-sort Index 0) +(declare-sort Element 0)(declare-sort Arr 0)(declare-fun aselect (Arr Index) Element)(declare-fun astore (Arr Index Element) Arr)(declare-fun k (Arr Arr) Index) +(declare-fun a () Index) +(declare-fun aaa () Index) +(declare-fun aa () Index) +(declare-fun S () Arr) +(declare-fun vvv () Element) +(declare-fun v () Element) +(declare-fun vv () Element) +(declare-fun bbb () Index) +(declare-fun www () Element) +(declare-fun bb () Index) +(declare-fun ww () Element) +(declare-fun b () Index) +(declare-fun w () Element) +(declare-fun SS () Arr) +(assert (let ((?v_3 (ite (= a aa) false true)) (?v_4 (ite (= aa aaa) false true)) (?v_1 (astore (astore (astore S a v) aa vv) aaa vvv)) (?v_0 (astore S aaa vvv)) (?v_2 (astore S aa vv))) (not (ite (ite (ite (ite (= a aaa) false true) (ite ?v_3 ?v_4 false) false) (ite (= (astore (astore ?v_0 a v) aa vv) ?v_1) (ite (= (astore (astore ?v_0 aa vv) a v) ?v_1) (ite (= (astore (astore ?v_2 a v) aaa vvv) ?v_1) (= (astore (astore ?v_2 aaa vvv) a v) ?v_1) false) false) false) true) (ite (ite (= ?v_1 (astore (astore (astore S bbb www) bb ww) b w)) (ite (ite ?v_3 (ite ?v_4 (ite (ite (= aa b) false true) (ite (ite (= aa bb) false true) (ite (= aa bbb) false true) false) false) false) false) (= (aselect S aa) vv) true) true) (ite (= S (astore SS a v)) (= S (astore SS a (aselect S a))) true) false) false)))) +; rewrite rule definition of arrays theory +(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (=> (not (= ?i ?j)) (= (aselect (astore ?x ?i ?e) ?j) (aselect ?x ?j))) :rewrite-rule))) +(assert (forall ((?x Arr) (?i Index) (?e Element)) (! (=> true (= (aselect (astore ?x ?i ?e) ?i) ?e)) :rewrite-rule))) +(assert (forall ((?x Arr) (?y Arr)) (! (=> (not (= ?x ?y)) (not (= (aselect ?x (k ?x ?y)) (aselect ?y (k ?x ?y))))) :rewrite-rule))) +(assert (forall ((?x Arr) (?y Arr)) (! (! (=> true (or (= ?x ?y) (not (= ?x ?y)))) :pattern (?x)) :rewrite-rule))) +(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (! (=> true (or (= ?i ?j) (not (= ?i ?j)))) :pattern ((aselect (astore ?x ?i ?e) ?j))) :rewrite-rule)))(check-sat) +(exit) diff --git a/test/regress/regress0/tptp/Makefile.am b/test/regress/regress0/tptp/Makefile.am index e0c8a2b48..e9274d2ee 100644 --- a/test/regress/regress0/tptp/Makefile.am +++ b/test/regress/regress0/tptp/Makefile.am @@ -35,7 +35,6 @@ TESTS = \ tff0.p \ tff0-arith.p \ ARI086$(equals)1.p \ - BOO003-4.p \ DAT001$(equals)1.p \ KRS018+1.p \ KRS063+1.p \ @@ -62,6 +61,7 @@ TEST_DEPS_DIST = \ EXTRA_DIST = $(TESTS) \ $(TEST_DEPS_DIST) \ BOO027-1.p \ + BOO003-4.p \ MGT031-1.p \ NLP114-1.p \ SYN075+1.p |