diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-05-19 16:24:59 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-19 16:24:59 -0500 |
commit | c8f149fa83fa16f821f37687fedfa778808809bd (patch) | |
tree | 8808ec522b58c0d8273280923b984a72e0b7bb29 /src/theory/quantifiers | |
parent | 6bb98062a5578d126db6a3e8cdca083881893b32 (diff) |
Renamed operator CHOICE to WITNESS (#4207)
Renamed operator CHOICE to WITNESS, and removed it from the front end
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/bv_inverter.h | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.h | 2 |
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; |