summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/nl_model.cpp4
-rw-r--r--src/theory/arith/theory_arith_private.cpp4
-rw-r--r--src/theory/builtin/kinds4
-rw-r--r--src/theory/builtin/theory_builtin.cpp2
-rw-r--r--src/theory/builtin/theory_builtin_rewriter.cpp2
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h12
-rw-r--r--src/theory/quantifiers/bv_inverter.cpp8
-rw-r--r--src/theory/quantifiers/bv_inverter.h6
-rw-r--r--src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp8
-rw-r--r--src/theory/quantifiers/cegqi/ceg_instantiator.cpp6
-rw-r--r--src/theory/quantifiers/cegqi/ceg_instantiator.h2
-rw-r--r--src/theory/quantifiers/fmf/bounded_integers.cpp6
-rw-r--r--src/theory/quantifiers/fmf/bounded_integers.h2
-rw-r--r--src/theory/sets/theory_sets_private.cpp2
-rw-r--r--src/theory/strings/theory_strings.cpp4
-rw-r--r--src/theory/theory_model.cpp4
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback