From df1ea6b9cdc1f424073151d0f7fda639d4405622 Mon Sep 17 00:00:00 2001
From: mudathirmahgoub <mudathir-mahgoubyahia@uiowa.edu>
Date: Wed, 8 Apr 2020 18:24:16 -0500
Subject: 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.
---
 src/parser/cvc/Cvc.g     | 10 +++++++++-
 src/parser/smt2/smt2.cpp |  1 +
 2 files changed, 10 insertions(+), 1 deletion(-)

(limited to 'src/parser')

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 32604d03f..3f03ca43d 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -205,6 +205,9 @@ tokens {
   BVSLE_TOK = 'BVSLE';
   BVSGE_TOK = 'BVSGE';
 
+  // Sets
+  SETS_CHOOSE_TOK = 'CHOOSE';
+
   // Relations
   JOIN_TOK = 'JOIN';
   TRANSPOSE_TOK = 'TRANSPOSE';
@@ -327,7 +330,8 @@ int getOperatorPrecedence(int type) {
   case PRODUCT_TOK:
   case IDEN_TOK:
   case JOIN_IMAGE_TOK:
-  case TRANSCLOSURE_TOK: return 24;
+  case TRANSCLOSURE_TOK:
+  case SETS_CHOOSE_TOK: return 24;
   case LEQ_TOK:
   case LT_TOK:
   case GEQ_TOK:
@@ -367,10 +371,12 @@ api::Kind getOperatorKind(int type, bool& negate) {
   case XOR_TOK: return api::XOR;
   case AND_TOK: return api::AND;
 
+  case SETS_CHOOSE_TOK: return api::CHOOSE;
   case PRODUCT_TOK: return api::PRODUCT;
   case JOIN_TOK: return api::JOIN;
   case JOIN_IMAGE_TOK: return api::JOIN_IMAGE;
 
+
     // comparisonBinop
   case EQUAL_TOK: return api::EQUAL;
   case DISEQUAL_TOK: negate = true; return api::EQUAL;
@@ -2097,6 +2103,8 @@ setsTerm[CVC4::api::Term& f]
     /* Sets prefix operators */
   : SETS_CARD_TOK LPAREN formula[f] RPAREN
     { f = MK_TERM(CVC4::api::CARD, f); }
+  | SETS_CHOOSE_TOK LPAREN formula[f] RPAREN
+        { f = MK_TERM(CVC4::api::CHOOSE, f); }
   | simpleTerm[f]
   ;
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 3233ee7e8..2405b3402 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -670,6 +670,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     addOperator(api::INSERT, "insert");
     addOperator(api::CARD, "card");
     addOperator(api::COMPLEMENT, "complement");
+    addOperator(api::CHOOSE, "choose");
     addOperator(api::JOIN, "join");
     addOperator(api::PRODUCT, "product");
     addOperator(api::TRANSPOSE, "transpose");
-- 
cgit v1.2.3