diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/nl_model.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 4 | ||||
-rw-r--r-- | src/theory/builtin/kinds | 4 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 2 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 12 | ||||
-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 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 4 |
16 files changed, 38 insertions, 38 deletions
diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp index abb2a7921..0d47c8874 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl_model.cpp @@ -1296,7 +1296,7 @@ void NlModel::getModelValueRepair( pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); Trace("nl-model") << v << " approximated as " << pred << std::endl; Node witness; - if (options::modelWitnessChoice()) + if (options::modelWitnessValue()) { // witness is the midpoint witness = nm->mkNode( @@ -1314,7 +1314,7 @@ void NlModel::getModelValueRepair( } } // Also record the exact values we used. An exact value can be seen as a - // special kind approximation of the form (choice x. x = exact_value). + // special kind approximation of the form (witness x. x = exact_value). // Notice that the above term gets rewritten such that the choice function // is eliminated. for (size_t i = 0, num = d_check_model_vars.size(); i < num; i++) diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 374de8562..0f2f4bbf4 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -5151,7 +5151,7 @@ Node TheoryArithPrivate::expandDefinition(Node node) kind::AND, nm->mkNode(kind::MULT, var, var).eqNode(node[0]), uf); // sqrt(x) reduces to: - // choice y. ite(x >= 0.0, y * y = x ^ Uf(x), Uf(x)) + // witness y. ite(x >= 0.0, y * y = x ^ Uf(x), Uf(x)) // // Uf(x) makes sure that the reduction still behaves like a function, // otherwise the reduction of (x = 1) ^ (sqrt(x) != sqrt(1)) would be @@ -5202,7 +5202,7 @@ Node TheoryArithPrivate::expandDefinition(Node node) lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0])); } Assert(!lem.isNull()); - Node ret = nm->mkNode(CHOICE, nm->mkNode(BOUND_VAR_LIST, var), lem); + Node ret = nm->mkNode(WITNESS, nm->mkNode(BOUND_VAR_LIST, var), lem); d_nlin_inverse_skolem[node] = ret; return ret; } 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: 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; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index d6eec3821..fbf1e6fcf 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1510,7 +1510,7 @@ Node TheorySetsPrivate::expandDefinition(Node node) Node memberAndEqual = member.andNode(equal); Node ite = nm->mkNode(kind::ITE, isEmpty, equal, memberAndEqual); Node witnessVariables = nm->mkNode(BOUND_VAR_LIST, witnessVariable); - Node witness = nm->mkNode(CHOICE, witnessVariables, ite); + Node witness = nm->mkNode(WITNESS, witnessVariables, ite); return witness; } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5b7c38361..b98bd1dea 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -580,7 +580,7 @@ Node TheoryStrings::expandDefinition(Node node) if (node.getKind() == STRING_FROM_CODE) { // str.from_code(t) ---> - // choice k. ite(0 <= t < |A|, t = str.to_code(k), k = "") + // witness k. ite(0 <= t < |A|, t = str.to_code(k), k = "") NodeManager* nm = NodeManager::currentNM(); Node t = node[0]; Node card = nm->mkConst(Rational(utils::getAlphabetCardinality())); @@ -590,7 +590,7 @@ Node TheoryStrings::expandDefinition(Node node) Node bvl = nm->mkNode(BOUND_VAR_LIST, k); Node emp = Word::mkEmptyWord(node.getType()); node = nm->mkNode( - CHOICE, + WITNESS, bvl, nm->mkNode( ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp))); diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 10e57e794..f24e4fc66 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -266,10 +266,10 @@ Node TheoryModel::getModelValue(TNode n) const if (ita != d_approximations.end()) { // If the value of n is approximate based on predicate P(n), we return - // choice z. P(z). + // witness z. P(z). Node v = nm->mkBoundVar(n.getType()); Node bvl = nm->mkNode(BOUND_VAR_LIST, v); - Node answer = nm->mkNode(CHOICE, bvl, ita->second.substitute(n, v)); + Node answer = nm->mkNode(WITNESS, bvl, ita->second.substitute(n, v)); d_modelCache[n] = answer; return answer; } |