From c8f149fa83fa16f821f37687fedfa778808809bd Mon Sep 17 00:00:00 2001
From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Tue, 19 May 2020 16:24:59 -0500
Subject: Renamed operator CHOICE to WITNESS (#4207)

Renamed operator CHOICE to WITNESS, and removed it from the front end
---
 src/parser/cvc/Cvc.g   | 6 ++----
 src/parser/smt2/Smt2.g | 2 --
 src/parser/tptp/Tptp.g | 7 +++++--
 3 files changed, 7 insertions(+), 8 deletions(-)

(limited to 'src/parser')

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 3f03ca43d..7babf2e56 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -114,7 +114,6 @@ tokens {
 
   FORALL_TOK = 'FORALL';
   EXISTS_TOK = 'EXISTS';
-  CHOICE_TOK = 'CHOICE';
   PATTERN_TOK = 'PATTERN';
 
   LAMBDA_TOK = 'LAMBDA';
@@ -348,8 +347,7 @@ int getOperatorPrecedence(int type) {
   case IMPLIES_TOK: return 30;// right-to-left
   case IFF_TOK: return 31;
   case FORALL_TOK:
-  case EXISTS_TOK:
-  case CHOICE_TOK: return 32;
+  case EXISTS_TOK:return 32;
   case ASSIGN_TOK:
   case IN_TOK: return 33;
 
@@ -1471,7 +1469,7 @@ prefixFormula[CVC4::api::Term& f]
   api::Term ipl;
 }
     /* quantifiers */
-  : ( FORALL_TOK { k = api::FORALL; } | EXISTS_TOK { k = api::EXISTS; } | CHOICE_TOK { k = api::CHOICE; } )
+  : ( FORALL_TOK { k = api::FORALL; } | EXISTS_TOK { k = api::EXISTS; } )
     { PARSER_STATE->pushScope(); } LPAREN
     boundVarDecl[ids,t]
     { for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) {
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 35227e7ce..d591c29de 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2254,7 +2254,6 @@ quantOp[CVC4::api::Kind& kind]
 }
   : EXISTS_TOK    { $kind = api::EXISTS; }
   | FORALL_TOK    { $kind = api::FORALL; }
-  | CHOICE_TOK    { $kind = api::CHOICE; }
   ;
 
 /**
@@ -2625,7 +2624,6 @@ ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level';
 // operators (NOTE: theory symbols go here)
 EXISTS_TOK        : 'exists';
 FORALL_TOK        : 'forall';
-CHOICE_TOK        : { !PARSER_STATE->strictModeEnabled() }? 'choice';
 
 EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp';
 CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char';
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 2568101c4..c2f4675b1 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -926,7 +926,10 @@ thfQuantifier[CVC4::api::Kind& kind]
   : FORALL_TOK { kind = api::FORALL; }
   | EXISTS_TOK { kind = api::EXISTS; }
   | LAMBDA_TOK { kind = api::LAMBDA; }
-  | CHOICE_TOK { kind = api::CHOICE; }
+  | CHOICE_TOK
+    {
+        UNSUPPORTED("Choice operator");
+    }
   | DEF_DESC_TOK
     {
       UNSUPPORTED("Description quantifier");
@@ -1627,7 +1630,7 @@ NOT_TOK        : '~';
 FORALL_TOK     : '!';
 EXISTS_TOK     : '?';
 LAMBDA_TOK     : '^';
-CHOICE_TOK     : '@+';
+WITNESS_TOK     : '@+';
 DEF_DESC_TOK   : '@-';
 AND_TOK        : '&';
 IFF_TOK        : '<=>';
-- 
cgit v1.2.3