diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-23 15:44:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-23 15:44:50 -0500 |
commit | a96fbfe33c05bea0b94d5387dda65c2ae343f66b (patch) | |
tree | a3b1e28dc45f05ef218331217ed072e842d6dfd3 /src/theory/theory_model.cpp | |
parent | 4c2138a14c4abba2431bc8ba51359d3a565baf05 (diff) |
Add notions of evaluated kinds in TheoryModel (#1947)
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 283 |
1 files changed, 157 insertions, 126 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 35ada798c..0258e65cc 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -48,6 +48,12 @@ TheoryModel::TheoryModel(context::Context* c, 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() @@ -160,148 +166,157 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c } 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 */ @@ -477,6 +492,17 @@ void TheoryModel::recordApproximation(TNode n, TNode pred) 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 ); @@ -546,6 +572,11 @@ void TheoryModel::printRepresentative( std::ostream& out, Node r ){ } } +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; |