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/regress1/fmf | |
| 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/regress1/fmf')
| -rw-r--r-- | test/regress/regress1/fmf/agree466.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/fmf/agree467.smt2 | 2 |
2 files changed, 2 insertions, 2 deletions
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)))) |