Renamed operator CHOICE to WITNESS (#4207)

Renamed operator CHOICE to WITNESS, and removed it from the front end

4 files changed, 10 insertions, 10 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 4d5e95119..a11354b1a 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -298,7 +298,7 @@ operator SEXPR 0: "a symbolic expression (any arity)"
 
 operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body"
 
-operator CHOICE 2 "a Hilbert choice (epsilon) expression; first parameter is a BOUND_VAR_LIST, second is the Hilbert choice body"
+operator WITNESS 2 "a witness expression; first parameter is a BOUND_VAR_LIST, second is the witness body"
 
 constant TYPE_CONSTANT \
     ::CVC4::TypeConstant \
@@ -329,7 +329,7 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
 typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
-typerule CHOICE ::CVC4::theory::builtin::ChoiceTypeRule
+typerule WITNESS ::CVC4::theory::builtin::WitnessTypeRule
 
 # lambda expressions that are isomorphic to array constants can be considered constants
 construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index b9d05b833..1667e5505 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -46,7 +46,7 @@ void TheoryBuiltin::finishInit()
   // choice nodes are not evaluated in getModelValue
   TheoryModel* theoryModel = d_valuation.getModel();
   Assert(theoryModel != nullptr);
-  theoryModel->setUnevaluatedKind(kind::CHOICE);
+  theoryModel->setUnevaluatedKind(kind::WITNESS);
 }
 
 }  // namespace builtin
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index dd6d434ca..d8175dd60 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -92,7 +92,7 @@ RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) {
     }
     return RewriteResponse(REWRITE_DONE, node);
   }
-  else if (node.getKind() == kind::CHOICE)
+  else if (node.getKind() == kind::WITNESS)
   {
     if (node[1].getKind() == kind::EQUAL)
     {
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index a3d1776e1..28d6c9037 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -159,7 +159,7 @@ class LambdaTypeRule {
   }
 };/* class LambdaTypeRule */
 
-class ChoiceTypeRule
+class WitnessTypeRule
 {
  public:
   inline static TypeNode computeType(NodeManager* nodeManager,
@@ -169,14 +169,14 @@ class ChoiceTypeRule
     if (n[0].getType(check) != nodeManager->boundVarListType())
     {
       std::stringstream ss;
-      ss << "expected a bound var list for CHOICE expression, got `"
+      ss << "expected a bound var list for WITNESS expression, got `"
          << n[0].getType().toString() << "'";
       throw TypeCheckingExceptionPrivate(n, ss.str());
     }
     if (n[0].getNumChildren() != 1)
     {
       std::stringstream ss;
-      ss << "expected a bound var list with one argument for CHOICE expression";
+      ss << "expected a bound var list with one argument for WITNESS expression";
       throw TypeCheckingExceptionPrivate(n, ss.str());
     }
     if (check)
@@ -185,14 +185,14 @@ class ChoiceTypeRule
       if (!rangeType.isBoolean())
       {
         std::stringstream ss;
-        ss << "expected a body of a CHOICE expression to have Boolean type";
+        ss << "expected a body of a WITNESS expression to have Boolean type";
         throw TypeCheckingExceptionPrivate(n, ss.str());
       }
     }
-    // The type of a choice function is the type of its bound variable.
+    // The type of a witness function is the type of its bound variable.
     return n[0][0].getType();
   }
-}; /* class ChoiceTypeRule */
+}; /* class WitnessTypeRule */
 
 class SortProperties {
  public: