d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
d_eeContext->push();
+ // do not interpret APPLY_UF if we are not assigning function values
+ if (!enableFuncModels)
+ {
+ setSemiEvaluatedKind(kind::APPLY_UF);
+ }
+ setUnevaluatedKind(kind::BOUND_VARIABLE);
}
TheoryModel::~TheoryModel()
}
Debug("model-getvalue-debug") << "Get model value " << n << " ... ";
Debug("model-getvalue-debug") << d_equalityEngine->hasTerm(n) << std::endl;
+ if (n.isConst())
+ {
+ d_modelCache[n] = n;
+ return n;
+ }
+
Node ret = n;
- if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ) {
- // We should have terms, thanks to TheoryQuantifiers::collectModelInfo().
- // However, if the Decision Engine stops us early, there might be a
- // quantifier that isn't assigned. In conjunction with miniscoping, this
- // might lead to a perfectly good model. Think of
- // ASSERT FORALL(x) : p OR x=5
- // The p is pulled out by miniscoping, and set to TRUE by the decision
- // engine, then the quantifier's value in the model doesn't matter, so the
- // Decision Engine stops. So even though the top-level quantifier was
- // asserted, it can't be checked directly: first, it doesn't "exist" in
- // non-miniscoped form, and second, no quantifiers have been asserted, so
- // none is in the model. We used to fail an assertion here, but that's
- // no good. Instead, return the quantifier itself. If we're in
- // checkModel(), and the quantifier actually matters, we'll get an
- // assert-fail since the quantifier isn't a constant.
- Node nr = Rewriter::rewrite(n);
- if(!d_equalityEngine->hasTerm(nr)) {
- d_modelCache[n] = ret;
- return ret;
- } else {
- ret = nr;
+ Kind nk = n.getKind();
+ NodeManager* nm = NodeManager::currentNM();
+
+ // if it is an evaluated kind, compute model values for children and evaluate
+ if (n.getNumChildren() > 0
+ && d_not_evaluated_kinds.find(nk) == d_not_evaluated_kinds.end())
+ {
+ Debug("model-getvalue-debug")
+ << "Get model value children " << n << std::endl;
+ std::vector<Node> children;
+ if (n.getKind() == APPLY_UF)
+ {
+ Node op = getModelValue(n.getOperator(), hasBoundVars);
+ Debug("model-getvalue-debug") << " operator : " << op << std::endl;
+ children.push_back(op);
}
- } else {
- // FIXME : special case not necessary? (also address BV_ACKERMANNIZE
- // functions below), github issue #1116
- if(n.getKind() == kind::LAMBDA) {
- NodeManager* nm = NodeManager::currentNM();
- Node body = getModelValue(n[1], true);
- body = Rewriter::rewrite(body);
- ret = nm->mkNode(kind::LAMBDA, n[0], body);
- ret = Rewriter::rewrite( ret );
- d_modelCache[n] = ret;
- return ret;
+ else if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ children.push_back(n.getOperator());
+ }
+ // evaluate the children
+ for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; ++i)
+ {
+ ret = getModelValue(n[i], hasBoundVars);
+ Debug("model-getvalue-debug")
+ << " " << n << "[" << i << "] is " << ret << std::endl;
+ children.push_back(ret);
}
- if(n.isConst() || (hasBoundVars && n.getKind() == kind::BOUND_VARIABLE)) {
+ ret = nm->mkNode(n.getKind(), children);
+ Debug("model-getvalue-debug") << "ret (pre-rewrite): " << ret << std::endl;
+ ret = Rewriter::rewrite(ret);
+ Debug("model-getvalue-debug") << "ret (post-rewrite): " << ret << std::endl;
+ // special cases
+ if (ret.getKind() == kind::CARDINALITY_CONSTRAINT)
+ {
+ Debug("model-getvalue-debug")
+ << "get cardinality constraint " << ret[0].getType() << std::endl;
+ ret = nm->mkConst(
+ getCardinality(ret[0].getType().toType()).getFiniteCardinality()
+ <= ret[1].getConst<Rational>().getNumerator());
+ }
+ else if (ret.getKind() == kind::CARDINALITY_VALUE)
+ {
+ Debug("model-getvalue-debug")
+ << "get cardinality value " << ret[0].getType() << std::endl;
+ ret = nm->mkConst(Rational(
+ getCardinality(ret[0].getType().toType()).getFiniteCardinality()));
+ }
+ d_modelCache[n] = ret;
+ return ret;
+ }
+ // must rewrite the term at this point
+ ret = Rewriter::rewrite(n);
+ // return the representative of the term in the equality engine, if it exists
+ TypeNode t = ret.getType();
+ bool eeHasTerm;
+ if (!options::ufHo() && (t.isFunction() || t.isPredicate()))
+ {
+ // functions are in the equality engine, but *not* as first-class members
+ // when higher-order is disabled. In this case, we cannot query
+ // representatives for functions since they are "internal" nodes according
+ // to the equality engine despite hasTerm returning true. However, they are
+ // first class members when higher-order is enabled. Hence, the special
+ // case here.
+ eeHasTerm = false;
+ }
+ else
+ {
+ eeHasTerm = d_equalityEngine->hasTerm(ret);
+ }
+ if (eeHasTerm)
+ {
+ Debug("model-getvalue-debug")
+ << "get value from representative " << ret << "..." << std::endl;
+ ret = d_equalityEngine->getRepresentative(ret);
+ Assert(d_reps.find(ret) != d_reps.end());
+ std::map<Node, Node>::const_iterator it2 = d_reps.find(ret);
+ if (it2 != d_reps.end())
+ {
+ ret = it2->second;
d_modelCache[n] = ret;
return ret;
}
+ }
- if (n.getNumChildren() > 0
- && n.getKind() != kind::BITVECTOR_ACKERMANNIZE_UDIV
- && n.getKind() != kind::BITVECTOR_ACKERMANNIZE_UREM)
+ // if we are a evaluated or semi-evaluated kind, return an arbitrary value
+ // if we are not in the d_not_evaluated_kinds map, we are evaluated
+ // if we are in the d_semi_evaluated_kinds, we are semi-evaluated
+ if (d_not_evaluated_kinds.find(nk) == d_not_evaluated_kinds.end()
+ || d_semi_evaluated_kinds.find(nk) != d_semi_evaluated_kinds.end())
+ {
+ if (t.isFunction() || t.isPredicate())
{
- Debug("model-getvalue-debug") << "Get model value children " << n << std::endl;
- std::vector<Node> children;
- if (n.getKind() == APPLY_UF) {
- Node op = getModelValue(n.getOperator(), hasBoundVars);
- Debug("model-getvalue-debug") << " operator : " << op << std::endl;
- children.push_back(op);
- }
- else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
- children.push_back(n.getOperator());
- }
- //evaluate the children
- for (unsigned i = 0; i < n.getNumChildren(); ++i) {
- ret = getModelValue(n[i], hasBoundVars);
- Debug("model-getvalue-debug") << " " << n << "[" << i << "] is " << ret << std::endl;
- children.push_back(ret);
+ if (d_enableFuncModels)
+ {
+ std::map<Node, Node>::const_iterator it = d_uf_models.find(n);
+ if (it != d_uf_models.end())
+ {
+ // Existing function
+ ret = it->second;
+ d_modelCache[n] = ret;
+ return ret;
+ }
+ // Unknown function symbol: return LAMBDA x. c, where c is the first
+ // constant in the enumeration of the range type
+ vector<TypeNode> argTypes = t.getArgTypes();
+ vector<Node> args;
+ NodeManager* nm = NodeManager::currentNM();
+ for (unsigned i = 0, size = argTypes.size(); i < size; ++i)
+ {
+ args.push_back(nm->mkBoundVar(argTypes[i]));
+ }
+ Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args);
+ TypeEnumerator te(t.getRangeType());
+ ret = nm->mkNode(kind::LAMBDA, boundVarList, *te);
}
- ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
- Debug("model-getvalue-debug") << "ret (pre-rewrite): " << ret << std::endl;
- ret = Rewriter::rewrite(ret);
- Debug("model-getvalue-debug") << "ret (post-rewrite): " << ret << std::endl;
- if(ret.getKind() == kind::CARDINALITY_CONSTRAINT) {
- Debug("model-getvalue-debug") << "get cardinality constraint " << ret[0].getType() << std::endl;
- ret = NodeManager::currentNM()->mkConst(getCardinality(ret[0].getType().toType()).getFiniteCardinality() <= ret[1].getConst<Rational>().getNumerator());
- }else if(ret.getKind() == kind::CARDINALITY_VALUE) {
- Debug("model-getvalue-debug") << "get cardinality value " << ret[0].getType() << std::endl;
- ret = NodeManager::currentNM()->mkConst(Rational(getCardinality(ret[0].getType().toType()).getFiniteCardinality()));
+ else
+ {
+ // if func models not enabled, throw an error
+ Unreachable();
}
- d_modelCache[n] = ret;
- return ret;
}
-
- Debug("model-getvalue-debug") << "Handling special cases for types..." << std::endl;
- TypeNode t = n.getType();
- bool eeHasTerm;
- if( !options::ufHo() && (t.isFunction() || t.isPredicate()) ){
- // functions are in the equality engine, but *not* as first-class members
- // when higher-order is disabled. In this case, we cannot query representatives for functions
- // since they are "internal" nodes according to the equality engine despite hasTerm returning true.
- // However, they are first class members when higher-order is enabled. Hence, the special
- // case here.
- eeHasTerm = false;
- }else{
- eeHasTerm = d_equalityEngine->hasTerm(n);
+ else if (!t.isFirstClass())
+ {
+ // this is the class for regular expressions
+ // we simply invoke the rewriter on them
+ ret = Rewriter::rewrite(ret);
}
- // if the term does not exist in the equality engine, return an arbitrary value
- if (!eeHasTerm) {
- if (t.isFunction() || t.isPredicate()) {
- if (d_enableFuncModels) {
- std::map< Node, Node >::const_iterator it = d_uf_models.find(n);
- if (it != d_uf_models.end()) {
- // Existing function
- ret = it->second;
- d_modelCache[n] = ret;
- return ret;
- }
- // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type
- vector<TypeNode> argTypes = t.getArgTypes();
- vector<Node> args;
- NodeManager* nm = NodeManager::currentNM();
- for (unsigned i = 0; i < argTypes.size(); ++i) {
- args.push_back(nm->mkBoundVar(argTypes[i]));
- }
- Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args);
- TypeEnumerator te(t.getRangeType());
- ret = nm->mkNode(kind::LAMBDA, boundVarList, *te);
- }else{
- // TODO: if func models not enabled, throw an error?
- Unreachable();
- }
- }
- else if (!t.isFirstClass())
+ else
+ {
+ if (options::omitDontCares() && useDontCares)
{
- // this is the class for regular expressions
- // we simply invoke the rewriter on them
- ret = Rewriter::rewrite(ret);
- } else {
- if (options::omitDontCares() && useDontCares) {
- return Node();
- }
- // Unknown term - return first enumerated value for this type
- TypeEnumerator te(n.getType());
- ret = *te;
+ return Node();
}
- d_modelCache[n] = ret;
- return ret;
+ // Unknown term - return first enumerated value for this type
+ TypeEnumerator te(n.getType());
+ ret = *te;
}
+ d_modelCache[n] = ret;
+ return ret;
}
- Debug("model-getvalue-debug") << "get value from representative " << ret << "..." << std::endl;
- ret = d_equalityEngine->getRepresentative(ret);
- Assert(d_reps.find(ret) != d_reps.end());
- std::map< Node, Node >::const_iterator it2 = d_reps.find( ret );
- if (it2 != d_reps.end()) {
- ret = it2->second;
- } else {
- ret = Node::null();
- }
- d_modelCache[n] = ret;
- return ret;
+
+ d_modelCache[n] = n;
+ return n;
}
/** add substitution */
d_approx_list.push_back(std::pair<Node, Node>(n, pred));
}
+void TheoryModel::setUnevaluatedKind(Kind k)
+{
+ d_not_evaluated_kinds.insert(k);
+}
+
+void TheoryModel::setSemiEvaluatedKind(Kind k)
+{
+ d_not_evaluated_kinds.insert(k);
+ d_semi_evaluated_kinds.insert(k);
+}
+
bool TheoryModel::hasTerm(TNode a)
{
return d_equalityEngine->hasTerm( a );
}
}
+bool TheoryModel::areFunctionValuesEnabled() const
+{
+ return d_enableFuncModels;
+}
+
void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) {
Assert( d_uf_models.find( f )==d_uf_models.end() );
Trace("model-builder") << " Assigning function (" << f << ") to (" << f_def << ")" << endl;
* construction process.
*/
void recordApproximation(TNode n, TNode pred);
+ /** set unevaluate/semi-evaluated kind
+ *
+ * This informs this model how it should interpret applications of terms with
+ * kind k in getModelValue. We distinguish four categories of kinds:
+ *
+ * [1] "Evaluated"
+ * This includes (standard) interpreted symbols like NOT, PLUS, UNION, etc.
+ * These operators can be characterized by the invariant that they are
+ * "evaluatable". That is, if they are applied to only constants, the rewriter
+ * is guaranteed to rewrite the application to a constant. When getting
+ * the model value of <k>( t1...tn ) where k is a kind of this category, we
+ * compute the (constant) value of t1...tn, say this returns c1...cn, we
+ * return the (constant) result of rewriting <k>( c1...cn ).
+ *
+ * [2] "Unevaluated"
+ * This includes interpreted symbols like FORALL, EXISTS,
+ * CARDINALITY_CONSTRAINT, that are not evaluatable. When getting a model
+ * value for a term <k>( t1...tn ) where k is a kind of this category, we
+ * check whether <k>( t1...tn ) exists in the equality engine of this model.
+ * If it does, we return its representative, otherwise we return the term
+ * itself.
+ *
+ * [3] "Semi-evaluated"
+ * This includes kinds like BITVECTOR_ACKERMANNIZE_UDIV and others, typically
+ * those that correspond to abstractions. Like unevaluated kinds, these
+ * kinds do not have an evaluator. In contrast to unevaluated kinds, we
+ * interpret a term <k>( t1...tn ) not appearing in the equality engine as an
+ * arbitrary value instead of the term itself.
+ *
+ * [4] APPLY_UF, where getting the model value depends on an internally
+ * constructed representation of a lambda model value (d_uf_models).
+ * It is optional whether this kind is "evaluated" or "semi-evaluated".
+ * In the case that it is "evaluated", get model rewrites the application
+ * of the lambda model value of its operator to its evaluated arguments.
+ *
+ * By default, all kinds are considered "evaluated". The following methods
+ * change the interpretation of various (non-APPLY_UF) kinds to one of the
+ * above categories and should be called by the theories that own the kind
+ * during Theory::finishInit. We set APPLY_UF to be semi-interpreted when
+ * this model does not enabled function values (this is the case for the model
+ * of TheoryEngine when the option assignFunctionValues is set to false).
+ */
+ void setUnevaluatedKind(Kind k);
+ void setSemiEvaluatedKind(Kind k);
//---------------------------- end building the model
// ------------------- general equality queries
std::map< Node, std::vector< Node > > d_uf_terms;
/** a map from functions f to a list of all HO_APPLY terms with first argument f */
std::map< Node, std::vector< Node > > d_ho_uf_terms;
+ /** are function values enabled? */
+ bool areFunctionValuesEnabled() const;
/** assign function value f to definition f_def */
void assignFunctionDefinition( Node f, Node f_def );
/** have we assigned function f? */
std::map<Node, Node> d_approximations;
/** list of all approximations */
std::vector<std::pair<Node, Node> > d_approx_list;
+ /** a set of kinds that are not evaluated */
+ std::unordered_set<Kind, kind::KindHashFunction> d_not_evaluated_kinds;
+ /** a set of kinds that are semi-evaluated */
+ std::unordered_set<Kind, kind::KindHashFunction> d_semi_evaluated_kinds;
/** map of representatives of equality engine to used representatives in
* representative set */
std::map<Node, Node> d_reps;
projects / cvc5.git / commitdiff