Renamed operator CHOICE to WITNESS (#4207)

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

7 files changed, 19 insertions, 19 deletions

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 3756c6b4b..5417ce455 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -85,7 +85,7 @@ Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m)
     {
       Node x = m->getBoundVariable(tn);
       Node ccond = new_cond.substitute(solve_var, x);
-      c = nm->mkNode(kind::CHOICE, nm->mkNode(BOUND_VAR_LIST, x), ccond);
+      c = nm->mkNode(kind::WITNESS, nm->mkNode(BOUND_VAR_LIST, x), ccond);
       Trace("cegqi-bv-skvinv")
           << "SKVINV : Make " << c << " for " << new_cond << std::endl;
     }
@@ -397,9 +397,9 @@ Node BvInverter::solveBvLit(Node sv,
 
     if (!ic.isNull())
     {
-      /* We generate a choice term (choice x0. ic => x0 <k> s <litk> t) for
-       * x <k> s <litk> t. When traversing down, this choice term determines
-       * the value for x <k> s = (choice x0. ic => x0 <k> s <litk> t), i.e.,
+      /* We generate a witness term (witness x0. ic => x0 <k> s <litk> t) for
+       * x <k> s <litk> t. When traversing down, this witness term determines
+       * the value for x <k> s = (witness x0. ic => x0 <k> s <litk> t), i.e.,
        * from here on, the propagated literal is a positive equality. */
       litk = EQUAL;
       pol = true;
diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index 746bfba9a..2afb505a8 100644
--- a/src/theory/quantifiers/bv_inverter.h
+++ b/src/theory/quantifiers/bv_inverter.h
@@ -85,8 +85,8 @@ class BvInverter
    * non-null node t, then sv = t is the solved form of lit.
    *
    * If the BvInverterQuery provided to this function call is null, then
-   * the solution returned by this call will not contain CHOICE expressions.
-   * If the solved form for lit requires introducing a CHOICE expression,
+   * the solution returned by this call will not contain WITNESS expressions.
+   * If the solved form for lit requires introducing a WITNESS expression,
    * then this call will return null.
    */
   Node solveBvLit(Node sv,
@@ -112,7 +112,7 @@ class BvInverter
    * is a BV tautology where x is getSolveVariable( tn ).
    *
    * It returns a term of the form:
-   *   (choice y. cond { x -> y })
+   *   (witness y. cond { x -> y })
    * where y is a bound variable and x is getSolveVariable( tn ).
    *
    * In some cases, we may return a term t if cond implies an equality on
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index 2d43e63dc..fd06f9be4 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -407,7 +407,7 @@ Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci,
       }
       else
       {
-        if (cur.getKind() == CHOICE)
+        if (cur.getKind() == WITNESS)
         {
           // must replace variables of choice functions
           // with new variables to avoid variable
@@ -418,7 +418,7 @@ Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci,
           Assert(curr_subs.find(cur[0][0]) == curr_subs.end());
           curr_subs[cur[0][0]] = bv;
           // we cannot cache the results of subterms
-          // of this choice expression since we are
+          // of this witness expression since we are
           // now in the context { cur[0][0] -> bv },
           // hence we push a context here
           visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>());
@@ -483,8 +483,8 @@ Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci,
         visited_contains_pv[ret] = contains_pv;
       }
 
-      // if was choice, pop context
-      if (cur.getKind() == CHOICE)
+      // if was witness, pop context
+      if (cur.getKind() == WITNESS)
       {
         Assert(curr_subs.find(cur[0][0]) != curr_subs.end());
         curr_subs.erase(cur[0][0]);
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 6b625fc73..186024219 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -207,7 +207,7 @@ CegInstantiator::~CegInstantiator() {
 void CegInstantiator::computeProgVars( Node n ){
   if( d_prog_var.find( n )==d_prog_var.end() ){
     d_prog_var[n].clear();
-    if (n.getKind() == kind::CHOICE)
+    if (n.getKind() == kind::WITNESS)
     {
       Assert(d_prog_var.find(n[0][0]) == d_prog_var.end());
       d_prog_var[n[0][0]].clear();
@@ -235,7 +235,7 @@ void CegInstantiator::computeProgVars( Node n ){
     {
       d_prog_var[n].insert(n);
     }
-    if (n.getKind() == kind::CHOICE)
+    if (n.getKind() == kind::WITNESS)
     {
       d_prog_var.erase(n[0][0]);
     }
@@ -284,7 +284,7 @@ CegHandledStatus CegInstantiator::isCbqiTerm(Node n)
       visited.insert(cur);
       if (cur.getKind() != BOUND_VARIABLE && TermUtil::hasBoundVarAttr(cur))
       {
-        if (cur.getKind() == FORALL || cur.getKind() == CHOICE)
+        if (cur.getKind() == FORALL || cur.getKind() == WITNESS)
         {
           visit.push_back(cur[1]);
         }
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index b4aa38c07..7351e60f0 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -276,7 +276,7 @@ class CegInstantiator {
    *
    * This gets the next (canonical) bound variable of
    * type tn. This can be used for instance when
-   * constructing instantiations that involve choice expressions.
+   * constructing instantiations that involve witness expressions.
    */
   Node getBoundVariable(TypeNode tn);
   /** has this assertion been marked as solved? */
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 601452c1f..ef572ace7 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -670,7 +670,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
       choices.pop_back();
       Node bvl = nm->mkNode(BOUND_VAR_LIST, choice_i);
       Node cMinCard = nm->mkNode(LEQ, srCardN, nm->mkConst(Rational(i)));
-      choice_i = nm->mkNode(CHOICE, bvl, nm->mkNode(OR, cMinCard, cBody));
+      choice_i = nm->mkNode(WITNESS, bvl, nm->mkNode(OR, cMinCard, cBody));
       d_setm_choice[sro].push_back(choice_i);
     }
     Assert(i < d_setm_choice[sro].size());
@@ -690,8 +690,8 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
   //   e.g.
   // singleton(0) union singleton(1)
   //   becomes
-  // C1 union ( choice y. card(S)<=1 OR ( y in S AND distinct( y, C1 ) ) )
-  // where C1 = ( choice x. card(S)<=0 OR x in S ).
+  // C1 union ( witness y. card(S)<=1 OR ( y in S AND distinct( y, C1 ) ) )
+  // where C1 = ( witness x. card(S)<=0 OR x in S ).
   Trace("bound-int-rsi") << "...reconstructed " << nsr << std::endl;
   return nsr;
 }
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 1333af61c..2180a7270 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -72,7 +72,7 @@ private:
    *
    * For each set S and integer n, d_setm_choice[S][n] is the canonical
    * representation for the (n+1)^th member of set S. It is of the form:
-   * choice x. (|S| <= n OR ( x in S AND
+   * witness x. (|S| <= n OR ( x in S AND
    *   distinct( x, d_setm_choice[S][0], ..., d_setm_choice[S][n-1] ) ) )
    */
   std::map<Node, std::vector<Node> > d_setm_choice;