diff options
author | mudathirmahgoub <mudathir-mahgoubyahia@uiowa.edu> | 2020-04-08 18:24:16 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-08 18:24:16 -0500 |
commit | df1ea6b9cdc1f424073151d0f7fda639d4405622 (patch) | |
tree | f28bd734c6f78e7399f91e92d517343a779c09c3 /test/regress | |
parent | a48cafdd09c3ff8cb9984bad930343958c30ce56 (diff) |
Added CHOOSE operator for sets (#4211)
This PR enables THEORY_UF by default for sets and adds the operator CHOOSE for sets which returns an element from a given set. The semantics is as follows:
If a set A = {x}, then the term (choose A) is equivalent to the term x.
If the set is empty, then (choose A) is an arbitrary value.
If the set has cardinality > 1, then (choose A) will deterministically return an element in A.
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 5 | ||||
-rw-r--r-- | test/regress/regress1/fmf/agree466.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress1/fmf/agree467.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress1/sets/choose.cvc | 11 | ||||
-rw-r--r-- | test/regress/regress1/sets/choose1.smt2 | 11 | ||||
-rw-r--r-- | test/regress/regress1/sets/choose2.smt2 | 6 | ||||
-rw-r--r-- | test/regress/regress1/sets/choose3.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress1/sets/choose4.smt2 | 13 |
8 files changed, 55 insertions, 2 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 649178f91..c5dbd38f8 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1644,6 +1644,11 @@ set(regress_1_tests regress1/sep/wand-simp-sat.smt2 regress1/sep/wand-simp-sat2.smt2 regress1/sep/wand-simp-unsat.smt2 + regress1/sets/choose.cvc + regress1/sets/choose1.smt2 + regress1/sets/choose2.smt2 + regress1/sets/choose3.smt2 + regress1/sets/choose4.smt2 regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 diff --git a/test/regress/regress1/fmf/agree466.smt2 b/test/regress/regress1/fmf/agree466.smt2 index d17a663c6..bfbc50c9d 100644 --- a/test/regress/regress1/fmf/agree466.smt2 +++ b/test/regress/regress1/fmf/agree466.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --finite-model-find --lang=smt2.5 ; EXPECT: sat ; Preamble -------------- -(set-logic ALL_SUPPORTED) +(set-logic AUFDTLIA) (set-info :status sat) (declare-datatypes () ((UNIT (Unit)))) (declare-datatypes () ((BOOL (Truth) (Falsity)))) diff --git a/test/regress/regress1/fmf/agree467.smt2 b/test/regress/regress1/fmf/agree467.smt2 index 07180cf4f..b2ac3364e 100644 --- a/test/regress/regress1/fmf/agree467.smt2 +++ b/test/regress/regress1/fmf/agree467.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --finite-model-find --lang=smt2.5 ; EXPECT: unsat ; Preamble -------------- -(set-logic ALL_SUPPORTED) +(set-logic AUFDTLIA) (set-info :status unsat) (declare-datatypes () ((UNIT (Unit)))) (declare-datatypes () ((BOOL (Truth) (Falsity)))) diff --git a/test/regress/regress1/sets/choose.cvc b/test/regress/regress1/sets/choose.cvc new file mode 100644 index 000000000..2112e702b --- /dev/null +++ b/test/regress/regress1/sets/choose.cvc @@ -0,0 +1,11 @@ +% COMMAND-LINE: --no-check-models +% EXPECT: sat + +A : SET OF INT; +a : INT; + +ASSERT NOT (A = {} :: SET OF INT); +ASSERT CHOOSE (A) = 10; +ASSERT CHOOSE (A) = a; + +CHECKSAT; diff --git a/test/regress/regress1/sets/choose1.smt2 b/test/regress/regress1/sets/choose1.smt2 new file mode 100644 index 000000000..420a0fde0 --- /dev/null +++ b/test/regress/regress1/sets/choose1.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --no-check-models +(set-logic ALL) +(set-info :status sat) +(set-option :produce-models true) +(declare-fun A () (Set Int)) +(declare-fun a () Int) +(assert (not (= A (as emptyset (Set Int))))) +(assert (= (choose A) 10)) +(assert (= a (choose A))) +(assert (exists ((x Int)) (and (= x (choose A)) (= x a)))) +(check-sat) diff --git a/test/regress/regress1/sets/choose2.smt2 b/test/regress/regress1/sets/choose2.smt2 new file mode 100644 index 000000000..85a5d18d3 --- /dev/null +++ b/test/regress/regress1/sets/choose2.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-info :status unsat) +(set-option :produce-models true) +(declare-fun A () (Set Int)) +(assert (distinct (choose A) (choose A))) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/sets/choose3.smt2 b/test/regress/regress1/sets/choose3.smt2 new file mode 100644 index 000000000..744192496 --- /dev/null +++ b/test/regress/regress1/sets/choose3.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :produce-models true) +(declare-fun A () (Set Int)) +(assert (= (choose A) 10)) +(assert (= A (as emptyset (Set Int)))) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/sets/choose4.smt2 b/test/regress/regress1/sets/choose4.smt2 new file mode 100644 index 000000000..df7c510d3 --- /dev/null +++ b/test/regress/regress1/sets/choose4.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --no-check-models +(set-logic ALL) +(set-info :status sat) +(set-option :produce-models true) +(declare-fun A () (Set Int)) +(declare-fun a () Int) +(assert (not (= A (as emptyset (Set Int))))) +(assert (member 10 A)) +; this line raises an assertion error +(assert (= a (choose A))) +; this line raises an assertion error +;(assert (exists ((x Int)) (and (= x (choose A)) (= x a)))) +(check-sat)
\ No newline at end of file |