diff options
33 files changed, 95 insertions, 91 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index b27cc48b4..5c0c4a750 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -76,7 +76,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {CONSTANT, CVC4::Kind::VARIABLE}, {VARIABLE, CVC4::Kind::BOUND_VARIABLE}, {LAMBDA, CVC4::Kind::LAMBDA}, - {CHOICE, CVC4::Kind::CHOICE}, + {WITNESS, CVC4::Kind::WITNESS}, /* Boolean ------------------------------------------------------------- */ {CONST_BOOLEAN, CVC4::Kind::CONST_BOOLEAN}, {NOT, CVC4::Kind::NOT}, @@ -309,7 +309,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::VARIABLE, CONSTANT}, {CVC4::Kind::BOUND_VARIABLE, VARIABLE}, {CVC4::Kind::LAMBDA, LAMBDA}, - {CVC4::Kind::CHOICE, CHOICE}, + {CVC4::Kind::WITNESS, WITNESS}, /* Boolean --------------------------------------------------------- */ {CVC4::Kind::CONST_BOOLEAN, CONST_BOOLEAN}, {CVC4::Kind::NOT, NOT}, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 6c1a2256b..05423a952 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -134,15 +134,42 @@ enum CVC4_PUBLIC Kind : int32_t */ LAMBDA, /** - * Hilbert choice (epsilon) expression. + * The syntax of a witness term is similar to a quantified formula except that + * only one bound variable is allowed. + * The term (witness ((x T)) F) returns an element x of type T + * and asserts F. + * + * The witness operator behaves like the description operator + * (see https://planetmath.org/hilbertsvarepsilonoperator) if there is no x + * that satisfies F. But if such x exists, the witness operator does not + * enforce the axiom that ensures uniqueness up to logical equivalence: + * forall x. F \equiv G => witness x. F = witness x. G + * + * For example if there are 2 elements of type T that satisfy F, then the + * following formula is satisfiable: + * (distinct + * (witness ((x Int)) F) + * (witness ((x Int)) F)) + * + * This kind is primarily used internally, but may be returned in models + * (e.g. for arithmetic terms in non-linear queries). However, it is not + * supported by the parser. Moreover, the user of the API should be cautious + * when using this operator. In general, all witness terms + * (witness ((x Int)) F) should be such that (exists ((x Int)) F) is a valid + * formula. If this is not the case, then the semantics in formulas that use + * witness terms may be unintuitive. For example, the following formula is + * unsatisfiable: + * (or (= (witness ((x Int)) false) 0) (not (= (witness ((x Int)) false) 0)) + * whereas notice that (or (= z 0) (not (= z 0))) is true for any z. + * * Parameters: 2 * -[1]: BOUND_VAR_LIST - * -[2]: Hilbert choice body + * -[2]: Witness body * Create with: * mkTerm(Kind kind, Term child1, Term child2) * mkTerm(Kind kind, const std::vector<Term>& children) */ - CHOICE, + WITNESS, /* Boolean --------------------------------------------------------------- */ diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 0fd5bb4fa..16d66cf6a 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -523,7 +523,7 @@ private: /** * Create a new, fresh variable for use in a binder expression - * (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or CHOICE). It is + * (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or WITNESS). It is * an error for this bound variable to exist outside of a binder, * and it should also only be used in a single binder expression. * That is, two distinct FORALL expressions should use entirely @@ -542,7 +542,7 @@ private: /** * Create a (nameless) new, fresh variable for use in a binder - * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or CHOICE). + * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or WITNESS). * It is an error for this bound variable to exist outside of a * binder, and it should also only be used in a single binder * expression. That is, two distinct FORALL expressions should use diff --git a/src/expr/node.h b/src/expr/node.h index 8ded28f07..2f9d0b0ac 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -468,7 +468,7 @@ public: inline bool isClosure() const { assertTNodeNotExpired(); return getKind() == kind::LAMBDA || getKind() == kind::FORALL - || getKind() == kind::EXISTS || getKind() == kind::CHOICE + || getKind() == kind::EXISTS || getKind() == kind::WITNESS || getKind() == kind::COMPREHENSION || getKind() == kind::MATCH_BIND_CASE; } diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index e47029284..5e042d591 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -78,7 +78,7 @@ bool hasFreeVar(TNode n); /** * Returns true iff the node n contains a closure, that is, a node - * whose kind is FORALL, EXISTS, CHOICE, LAMBDA, or any other closure currently + * whose kind is FORALL, EXISTS, WITNESS, LAMBDA, or any other closure currently * supported. * @param n The node under investigation * @return true iff this node contains a closure. diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 9f9d58aad..6ac5b0289 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -394,9 +394,9 @@ header = "options/smt_options.h" help = "in models, output uninterpreted sorts as datatype enumerations" [[option]] - name = "modelWitnessChoice" + name = "modelWitnessValue" category = "regular" - long = "model-witness-choice" + long = "model-witness-value" type = "bool" default = "false" read_only = true 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) { diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 35227e7ce..d591c29de 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2254,7 +2254,6 @@ quantOp[CVC4::api::Kind& kind] } : EXISTS_TOK { $kind = api::EXISTS; } | FORALL_TOK { $kind = api::FORALL; } - | CHOICE_TOK { $kind = api::CHOICE; } ; /** @@ -2625,7 +2624,6 @@ ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level'; // operators (NOTE: theory symbols go here) EXISTS_TOK : 'exists'; FORALL_TOK : 'forall'; -CHOICE_TOK : { !PARSER_STATE->strictModeEnabled() }? 'choice'; EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp'; CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char'; diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 2568101c4..c2f4675b1 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -926,7 +926,10 @@ thfQuantifier[CVC4::api::Kind& kind] : FORALL_TOK { kind = api::FORALL; } | EXISTS_TOK { kind = api::EXISTS; } | LAMBDA_TOK { kind = api::LAMBDA; } - | CHOICE_TOK { kind = api::CHOICE; } + | CHOICE_TOK + { + UNSUPPORTED("Choice operator"); + } | DEF_DESC_TOK { UNSUPPORTED("Description quantifier"); @@ -1627,7 +1630,7 @@ NOT_TOK : '~'; FORALL_TOK : '!'; EXISTS_TOK : '?'; LAMBDA_TOK : '^'; -CHOICE_TOK : '@+'; +WITNESS_TOK : '@+'; DEF_DESC_TOK : '@-'; AND_TOK : '&'; IFF_TOK : '<=>'; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 9edc73acd..0c0c4c3a8 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -545,7 +545,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::MATCH_CASE: // do nothing break; - case kind::CHOICE: out << smtKindString(k, d_variant) << " "; break; + case kind::WITNESS: out << smtKindString(k, d_variant) << " "; break; // arith theory case kind::PLUS: @@ -1032,7 +1032,7 @@ static string smtKindString(Kind k, Variant v) case kind::LAMBDA: return "lambda"; case kind::MATCH: return "match"; - case kind::CHOICE: return "choice"; + case kind::WITNESS: return "witness"; // arith theory case kind::PLUS: return "+"; diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index d37ed05e1..1ae125e03 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -138,9 +138,9 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output, } } } - else if (node.getKind() == kind::CHOICE) + else if (node.getKind() == kind::WITNESS) { - // If a Hilbert choice function, witness the choice. + // If a witness choice // For details on this operator, see // http://planetmath.org/hilbertsvarepsilonoperator. if (!inQuant) @@ -150,15 +150,15 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output, { // Make the skolem to witness the choice skolem = nodeManager->mkSkolem( - "choiceK", + "witnessK", nodeType, - "a skolem introduced due to term-level Hilbert choice removal"); + "a skolem introduced due to term-level witness removal"); d_skolem_cache.insert(node, skolem); Assert(node[0].getNumChildren() == 1); // The new assertion is the assumption that the body - // of the choice operator holds for the Skolem + // of the witness operator holds for the Skolem newAssertion = node[1].substitute(node[0][0], skolem); } } diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index b6456bda6..3b72b46a5 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -112,7 +112,7 @@ public: * This is sometimes called "lambda lifting" * * As an example of (4): - * (choice x. P( x ) ) = t + * (witness x. P( x ) ) = t * becomes * P( k ) ^ k = t * where k is a fresh skolem constant. 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; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9f9f36c8f..336bbdd32 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -616,8 +616,6 @@ set(regress_0_tests regress0/parser/as.smt2 regress0/parser/bv_arity_smt2.6.smt2 regress0/parser/bv_nat.smt2 - regress0/parser/choice.cvc - regress0/parser/choice.smt2 regress0/parser/constraint.smt2 regress0/parser/declarefun-emptyset-uf.smt2 regress0/parser/force_logic_set_logic.smt2 diff --git a/test/regress/regress0/nl/sqrt2-value.smt2 b/test/regress/regress0/nl/sqrt2-value.smt2 index 649a792be..6c3cd378a 100644 --- a/test/regress/regress0/nl/sqrt2-value.smt2 +++ b/test/regress/regress0/nl/sqrt2-value.smt2 @@ -1,6 +1,6 @@ -; SCRUBBER: sed -e 's/choice.*/choice/' +; SCRUBBER: sed -e 's/witness.*/witness/' ; EXPECT: sat -; EXPECT: ((x (choice +; EXPECT: ((x (witness (set-option :produce-models true) (set-logic ALL) (declare-fun x () Real) diff --git a/test/regress/regress0/parser/choice.cvc b/test/regress/regress0/parser/choice.cvc deleted file mode 100644 index e0ebac051..000000000 --- a/test/regress/regress0/parser/choice.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: sat - -a : INT; -b : INT; -c : INT; - -ASSERT (CHOICE(x: INT): x = a) = 1; -ASSERT (CHOICE(x: INT): x = b) = 2; - -CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/parser/choice.smt2 b/test/regress/regress0/parser/choice.smt2 deleted file mode 100644 index 19763e222..000000000 --- a/test/regress/regress0/parser/choice.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -(set-logic ALL) -(set-info :status sat) -(declare-fun a () Int) -(declare-fun b () Int) -(declare-fun c () Int) -(assert (= (choice ((x Int)) (= x a)) 1)) -(assert (= (choice ((x Int)) (= x b)) 2)) -;(assert (let ((x (choice ((x Int)) true))) (and (distinct a b x)(= x c)))) -(check-sat) - diff --git a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 index 9bc47f925..3a4332176 100644 --- a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 +++ b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 @@ -1,5 +1,5 @@ -; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/; s/((x (choice ((BOUND_VARIABLE Real)) (or (= BOUND_VARIABLE.*/SUCCESS/' -; COMMAND-LINE: --produce-models --model-witness-choice --no-check-models +; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/; s/((x (witness ((BOUND_VARIABLE Real)) (or (= BOUND_VARIABLE.*/SUCCESS/' +; COMMAND-LINE: --produce-models --model-witness-value --no-check-models ; EXPECT: sat ; EXPECT: SUCCESS (set-logic QF_NRA) |