diff options
author | mudathirmahgoub <mudathir-mahgoubyahia@uiowa.edu> | 2020-01-07 18:13:07 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-07 18:13:07 -0600 |
commit | 7ce64c96d655d675778bc70d424fd72f82db589f (patch) | |
tree | ad43650d7c2cc82d8c96098530fb04485e63defc /test/regress | |
parent | b38ffa21717d220e98581854e2af1ee9d13ce5b7 (diff) |
Universe set cardinality for finite types with finite cardinality (#3392)
* rewrote set cardinality for finite-types
* small changes and format
Diffstat (limited to 'test/regress')
18 files changed, 269 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a53201e3e..22848ff97 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1583,6 +1583,22 @@ set(regress_1_tests regress1/sets/comp-pos-member.smt2 regress1/sets/copy_check_heap_access_33_4.smt2 regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 + regress1/sets/finite-type/sets-card-arrcolor.smt2 + regress1/sets/finite-type/sets-card-arrunit.smt2 + regress1/sets/finite-type/sets-card-bool-1.smt2 + regress1/sets/finite-type/sets-card-bool-2.smt2 + regress1/sets/finite-type/sets-card-bool-3.smt2 + regress1/sets/finite-type/sets-card-bool-4.smt2 + regress1/sets/finite-type/sets-card-bool-rec.smt2 + regress1/sets/finite-type/sets-card-bv-1.smt2 + regress1/sets/finite-type/sets-card-bv-2.smt2 + regress1/sets/finite-type/sets-card-bv-3.smt2 + regress1/sets/finite-type/sets-card-bv-4.smt2 + regress1/sets/finite-type/sets-card-color.smt2 + regress1/sets/finite-type/sets-card-color-sat.smt2 + regress1/sets/finite-type/sets-card-datatype-1.smt2 + regress1/sets/finite-type/sets-card-datatype-2.smt2 + regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 regress1/sets/fuzz14418.smt2 regress1/sets/fuzz15201.smt2 regress1/sets/fuzz31811.smt2 @@ -2277,6 +2293,7 @@ set(regression_disabled_tests regress1/rewriterules/test_guards.smt2 regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 regress1/sets/setofsets-disequal.smt2 + regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 regress1/simple-rdl-definefun.smt2 # does not solve after minor modification to search regress1/sygus/car_3.lus.sy diff --git a/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2 b/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2 new file mode 100644 index 000000000..2c7acf282 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_ALL) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-datatype Color ((Red) (Green) (Blue))) +(declare-fun A () (Set (Array Color Color))) +(declare-fun B () (Set (Array Color Color))) +(assert (> (card A) 25)) +(assert (> (card B) 25)) +(assert (distinct A B)) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2 b/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2 new file mode 100644 index 000000000..95d363397 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_ALL) +(set-info :status unsat) +(set-option :sets-ext true) +(declare-datatype Unit ((mkUnit))) + +(declare-fun S () (Set (Array Int Unit))) + +(assert (> (card S) 1)) + +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 new file mode 100644 index 000000000..c455caa28 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set Bool)) +(declare-fun B () (Set Bool)) +(declare-fun universe () (Set Bool)) +(assert (= (card A) 2)) +(assert (= (card B) 2)) +(assert (= (intersection A B) (as emptyset (Set Bool)))) +(assert (= universe (as univset (Set Bool)))) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 new file mode 100644 index 000000000..977bf3795 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set Bool)) +(declare-fun universe () (Set Bool)) +(assert (= (card A) 2)) +(assert (= universe (as univset (Set Bool)))) +(check-sat) + diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 new file mode 100644 index 000000000..623376e37 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set Bool)) +(declare-fun B () (Set Bool)) +(declare-fun universe () (Set Bool)) +(assert (= (card A) 2)) +(assert (= (card B) 2)) +(assert (= universe (as univset (Set Bool)))) +(check-sat) + diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2 new file mode 100644 index 000000000..1e18597dc --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_ALL) +(set-info :status sat) +(set-option :sets-ext true) +(set-option :produce-models true) +(declare-fun A () (Set Bool)) +(declare-fun x () Bool) +(assert (member (member x A) A)) +(assert (> (card A) 1)) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2 new file mode 100644 index 000000000..150dd5cff --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_ALL) +(set-info :status sat) +(set-option :sets-ext true) +(declare-fun A () (Set Bool)) +(declare-fun x () Bool) +(assert (member (member x A) A)) +(assert (> (card A) 1)) +(declare-fun U () (Set Bool)) +(assert (= U (as univset (Set Bool)))) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 new file mode 100644 index 000000000..1388b9bfa --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set (_ BitVec 3))) +(declare-fun universe () (Set (_ BitVec 3))) +(assert (= (card A) 3)) +(assert (= universe (as univset (Set (_ BitVec 3))))) +(check-sat) + diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 new file mode 100644 index 000000000..26ee05f3c --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 @@ -0,0 +1,16 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set (_ BitVec 3))) +(declare-fun B () (Set (_ BitVec 3))) +(declare-fun universe () (Set (_ BitVec 3))) +(assert (= (card A) 5)) +(assert (= (card B) 5)) +(assert (not (= A B))) +(assert (= (card (intersection A B)) 2)) +(assert (= (card (setminus A B)) 3)) +(assert (= (card (setminus B A)) 3)) +(assert (= universe (as univset (Set (_ BitVec 3))))) +(check-sat) + diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 new file mode 100644 index 000000000..8c92d1c6b --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 @@ -0,0 +1,19 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set (_ BitVec 3))) +(declare-fun B () (Set (_ BitVec 3))) +(declare-fun universe () (Set (_ BitVec 3))) +(declare-fun x () (_ BitVec 3)) +(assert (= (card A) 3)) +(assert (= (card B) 3)) +(assert (not (= A B))) +(assert (= (card (intersection A B)) 1)) +(assert (= (card (setminus A B)) 2)) +(assert (= (card (setminus B A)) 2)) +(assert (not (member x A))) +(assert (not (member x B))) +(assert (= universe (as univset (Set (_ BitVec 3))))) +(check-sat) + diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 new file mode 100644 index 000000000..d2c8a744d --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 @@ -0,0 +1,18 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set (_ BitVec 3))) +(declare-fun B () (Set (_ BitVec 3))) +(declare-fun universe () (Set (_ BitVec 3))) +(declare-fun x () (_ BitVec 3)) +(assert (= (card A) 5)) +(assert (= (card B) 5)) +(assert (not (= A B))) +(assert (= (card (intersection A B)) 2)) +(assert (= (card (setminus A B)) 3)) +(assert (= (card (setminus B A)) 3)) +(assert (= universe (as univset (Set (_ BitVec 3))))) +(assert (not (member x A))) +(assert (not (member x B))) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2 b/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2 new file mode 100644 index 000000000..ca8015622 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_BVDTLIAFS) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-datatype Color ((Red) (Green) (Blue) (Purple))) +(declare-fun A () (Set Color)) +(declare-fun B () (Set Color)) +(assert (> (card A) (card B) )) +(assert (member Red B)) +(declare-fun d () Color) +(assert (not (= d Red))) +(assert (member d B)) +(assert (not (member Green A))) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-color.smt2 b/test/regress/regress1/sets/finite-type/sets-card-color.smt2 new file mode 100644 index 000000000..4fe3f0428 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-color.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_BVDTLIAFS) +(set-info :status unsat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-datatype Color ((Red) (Green) (Blue))) +(declare-fun A () (Set Color)) +(declare-fun B () (Set Color)) +(assert (> (card A) (card B) )) +(assert (member Red B)) +(declare-fun d () Color) +(assert (not (= d Red))) +(assert (member d B)) +(assert (not (member Green A))) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 new file mode 100644 index 000000000..0121479e9 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 @@ -0,0 +1,14 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-datatype Rec ((mkRec (r1 (_ BitVec 2)) (r2 (_ BitVec 2))))) +(declare-fun A () (Set Rec)) +(declare-fun B () (Set Rec)) +(declare-fun universe () (Set Rec)) +(declare-fun x () Rec) +(assert (= (card A) 5)) +(assert (= (card B) 5)) +(assert (= (card (intersection A B)) 1)) +(assert (= universe (as univset (Set Rec)))) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 new file mode 100644 index 000000000..708ebb2ca --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-datatype Rec ((mkRec (r1 (_ BitVec 2)) (r2 (_ BitVec 2))))) +(declare-fun A () (Set Rec)) +(declare-fun B () (Set Rec)) +(declare-fun universe () (Set Rec)) +(assert (= (card A) 9)) +(assert (= (card B) 9)) +(assert (= (card (intersection A B)) 1)) +(assert (= universe (as univset (Set Rec)))) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 new file mode 100644 index 000000000..b4bd97f1d --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 @@ -0,0 +1,30 @@ +(set-logic QF_ALL) +(set-info :status unsat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set (_ BitVec 2))) +(declare-fun B () (Set (_ BitVec 2))) +(declare-fun C () (Set (_ BitVec 2))) +(declare-fun D () (Set (_ BitVec 2))) + +(declare-fun x () (_ BitVec 2)) +(assert (not (member x A))) +(assert (not (member x B))) +(assert (not (member x C))) +(assert (not (member x D))) +(declare-fun y () (_ BitVec 2)) +(assert (not (member y A))) +(assert (not (member y B))) +(assert (not (member y C))) +(assert (not (member y D))) +(declare-fun z () (_ BitVec 2)) +(assert (not (member z A))) +(assert (not (member z B))) +(assert (not (member z C))) +(assert (not (member z D))) + +(assert (distinct x y z)) + +(assert (= (card (union A (union B (union C D)))) 2)) + +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 new file mode 100644 index 000000000..88825a600 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 @@ -0,0 +1,30 @@ +(set-logic QF_ALL) +(set-info :status unsat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set (_ BitVec 3))) +(declare-fun B () (Set (_ BitVec 3))) +(declare-fun C () (Set (_ BitVec 3))) +(declare-fun D () (Set (_ BitVec 3))) + +(declare-fun x () (_ BitVec 3)) +(assert (not (member x A))) +(assert (not (member x B))) +(assert (not (member x C))) +(assert (not (member x D))) +(declare-fun y () (_ BitVec 3)) +(assert (not (member y A))) +(assert (not (member y B))) +(assert (not (member y C))) +(assert (not (member y D))) +(declare-fun z () (_ BitVec 3)) +(assert (not (member z A))) +(assert (not (member z B))) +(assert (not (member z C))) +(assert (not (member z D))) + +(assert (distinct x y z)) + +(assert (= (card (union A (union B (union C D)))) 6)) + +(check-sat) |