{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},
{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},
*/
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 --------------------------------------------------------------- */
/**
* 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
/**
* 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
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;
}
/**
* 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.
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
FORALL_TOK = 'FORALL';
EXISTS_TOK = 'EXISTS';
- CHOICE_TOK = 'CHOICE';
PATTERN_TOK = 'PATTERN';
LAMBDA_TOK = 'LAMBDA';
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;
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) {
}
: EXISTS_TOK { $kind = api::EXISTS; }
| FORALL_TOK { $kind = api::FORALL; }
- | CHOICE_TOK { $kind = api::CHOICE; }
;
/**
// 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';
: 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");
FORALL_TOK : '!';
EXISTS_TOK : '?';
LAMBDA_TOK : '^';
-CHOICE_TOK : '@+';
+WITNESS_TOK : '@+';
DEF_DESC_TOK : '@-';
AND_TOK : '&';
IFF_TOK : '<=>';
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:
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 "+";
}
}
}
- 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)
{
// 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);
}
}
* 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.
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(
}
}
// 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++)
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
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;
}
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 \
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
// 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
}
return RewriteResponse(REWRITE_DONE, node);
}
- else if (node.getKind() == kind::CHOICE)
+ else if (node.getKind() == kind::WITNESS)
{
if (node[1].getKind() == kind::EQUAL)
{
}
};/* class LambdaTypeRule */
-class ChoiceTypeRule
+class WitnessTypeRule
{
public:
inline static TypeNode computeType(NodeManager* nodeManager,
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)
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:
{
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;
}
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;
* 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,
* 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
}
else
{
- if (cur.getKind() == CHOICE)
+ if (cur.getKind() == WITNESS)
{
// must replace variables of choice functions
// with new variables to avoid variable
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>());
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]);
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();
{
d_prog_var[n].insert(n);
}
- if (n.getKind() == kind::CHOICE)
+ if (n.getKind() == kind::WITNESS)
{
d_prog_var.erase(n[0][0]);
}
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]);
}
*
* 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? */
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());
// 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;
}
*
* 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;
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;
}
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()));
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)));
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;
}
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
-; 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)
+++ /dev/null
-% 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
+++ /dev/null
-(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)
-
-; 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)
projects / cvc5.git / commitdiff