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 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'src/parser/cvc/Cvc.g')

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) {
-- 
cgit v1.2.3