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 /src/printer | |
| 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 'src/printer')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index b5e137b4d..4013cbd08 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -741,7 +741,8 @@ void Smt2Printer::toStream(std::ostream& out, case kind::INSERT: case kind::SET_TYPE: case kind::SINGLETON: - case kind::COMPLEMENT: out << smtKindString(k, d_variant) << " "; break; + case kind::COMPLEMENT: + case kind::CHOOSE: out << smtKindString(k, d_variant) << " "; break; case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break; // fp theory @@ -1134,6 +1135,7 @@ static string smtKindString(Kind k, Variant v) case kind::COMPLEMENT: return "complement"; case kind::CARD: return "card"; case kind::COMPREHENSION: return "comprehension"; + case kind::CHOOSE: return "choose"; case kind::JOIN: return "join"; case kind::PRODUCT: return "product"; case kind::TRANSPOSE: return "transpose"; |