From a96fbfe33c05bea0b94d5387dda65c2ae343f66b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 23 May 2018 15:44:50 -0500 Subject: [PATCH] Add notions of evaluated kinds in TheoryModel (#1947) --- src/options/theory_options.toml | 17 ++ src/options/uf_options.toml | 9 - src/smt/smt_engine.cpp | 12 + src/theory/bv/theory_bv.cpp | 10 + src/theory/bv/theory_bv.h | 2 + src/theory/quantifiers/fmf/ambqi_builder.cpp | 5 + .../quantifiers/fmf/full_model_check.cpp | 6 + src/theory/quantifiers/fmf/model_builder.cpp | 5 + src/theory/quantifiers/theory_quantifiers.cpp | 9 + src/theory/quantifiers/theory_quantifiers.h | 2 + src/theory/theory_engine.cpp | 3 +- src/theory/theory_model.cpp | 283 ++++++++++-------- src/theory/theory_model.h | 50 ++++ src/theory/theory_model_builder.cpp | 9 +- src/theory/uf/theory_uf.cpp | 4 + 15 files changed, 289 insertions(+), 137 deletions(-) diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml index 2b1f75072..3509f408d 100644 --- a/src/options/theory_options.toml +++ b/src/options/theory_options.toml @@ -23,3 +23,20 @@ header = "options/theory_options.h" notifies = ["notifyUseTheoryList"] read_only = true help = "use alternate theory implementation NAME (--use-theory=help for a list). This option may be repeated or a comma separated list." + +[[option]] + name = "assignFunctionValues" + category = "regular" + long = "assign-function-values" + type = "bool" + default = "true" + help = "assign values for uninterpreted functions in models" + +[[option]] + name = "condenseFunctionValues" + category = "regular" + long = "condense-function-values" + type = "bool" + default = "true" + read_only = true + help = "condense values for functions in models rather than explicitly representing them" diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml index 791b6e0bb..73a2be9ff 100644 --- a/src/options/uf_options.toml +++ b/src/options/uf_options.toml @@ -11,15 +11,6 @@ header = "options/uf_options.h" default = "true" help = "use UF symmetry breaker (Deharbe et al., CADE 2011)" -[[option]] - name = "condenseFunctionValues" - category = "regular" - long = "condense-function-values" - type = "bool" - default = "true" - read_only = true - help = "condense models for functions rather than explicitly representing them" - [[option]] name = "ufssRegions" category = "regular" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 114527334..9d4462210 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1313,6 +1313,11 @@ void SmtEngine::setDefaults() { { options::cbqiMidpoint.set(true); } + // do not assign function values (optimization) + if (!options::assignFunctionValues.wasSetByUser()) + { + options::assignFunctionValues.set(false); + } } else { @@ -5189,6 +5194,13 @@ Model* SmtEngine::getModel() { Dump("benchmark") << GetModelCommand(); } + if (!options::assignFunctionValues()) + { + const char* msg = + "Cannot get the model when --assign-function-values is false."; + throw RecoverableModalException(msg); + } + if(d_status.isNull() || d_status.asSatisfiabilityResult() == Result::UNSAT || d_problemExtended) { diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 2041b0805..107cb9672 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -187,6 +187,16 @@ Node TheoryBV::getBVDivByZero(Kind k, unsigned width) { Unreachable(); } +void TheoryBV::finishInit() +{ + // these kinds are semi-evaluated in getModelValue (applications of this + // kind are treated as variables) + TheoryModel* tm = d_valuation.getModel(); + Assert(tm != nullptr); + tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV); + tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM); +} + Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl; diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 13469d562..603823ff0 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -66,6 +66,8 @@ public: void setMasterEqualityEngine(eq::EqualityEngine* eq) override; + void finishInit() override; + Node expandDefinition(LogicRequest& logicRequest, Node node) override; void preRegisterTerm(TNode n) override; diff --git a/src/theory/quantifiers/fmf/ambqi_builder.cpp b/src/theory/quantifiers/fmf/ambqi_builder.cpp index cedd2a2ed..52ce4407a 100644 --- a/src/theory/quantifiers/fmf/ambqi_builder.cpp +++ b/src/theory/quantifiers/fmf/ambqi_builder.cpp @@ -744,6 +744,11 @@ QModelBuilder( c, qe ){ //------------------------model construction---------------------------- bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) { + if (!m->areFunctionValuesEnabled()) + { + // nothing to do if no functions + return true; + } Trace("ambqi-debug") << "process build model " << std::endl; FirstOrderModel* f = (FirstOrderModel*)m; FirstOrderModelAbs* fm = f->asFirstOrderModelAbs(); diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 0ec8b00b2..e97f716cb 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/fmf/full_model_check.h" #include "options/quantifiers_options.h" +#include "options/theory_options.h" #include "options/uf_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" @@ -370,6 +371,11 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) { } bool FullModelChecker::processBuildModel(TheoryModel* m){ + if (!m->areFunctionValuesEnabled()) + { + // nothing to do if no functions + return true; + } FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); Trace("fmc") << "---Full Model Check reset() " << std::endl; d_quant_models.clear(); diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index 9e7961172..055bee231 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -183,6 +183,11 @@ Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std:: */ bool QModelBuilderIG::processBuildModel( TheoryModel* m ) { + if (!m->areFunctionValuesEnabled()) + { + // nothing to do if no functions + return true; + } FirstOrderModel* f = (FirstOrderModel*)m; FirstOrderModelIG* fm = f->asFirstOrderModelIG(); Trace("model-engine-debug") << "Process build model " << optUseModel() << std::endl; diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 74d8269f9..5016bd87f 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -73,6 +73,15 @@ void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) { } +void TheoryQuantifiers::finishInit() +{ + // quantifiers are not evaluated in getModelValue + TheoryModel* tm = d_valuation.getModel(); + Assert(tm != nullptr); + tm->setUnevaluatedKind(EXISTS); + tm->setUnevaluatedKind(FORALL); +} + void TheoryQuantifiers::preRegisterTerm(TNode n) { Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl; if( n.getKind()==FORALL ){ diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 4bb28fe79..4f0302bf3 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -42,6 +42,8 @@ class TheoryQuantifiers : public Theory { void setMasterEqualityEngine(eq::EqualityEngine* eq) override; void addSharedTerm(TNode t) override; void notifyEq(TNode lhs, TNode rhs); + /** finish initialization */ + void finishInit() override; void preRegisterTerm(TNode n) override; void presolve() override; void ppNotifyAssertions(const std::vector& assertions) override; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 08d33fe6c..4d78482c5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -232,7 +232,8 @@ void TheoryEngine::finishInit() { d_curr_model_builder = d_quantEngine->getModelBuilder(); d_curr_model = d_quantEngine->getModel(); } else { - d_curr_model = new theory::TheoryModel(d_userContext, "DefaultModel", true); + d_curr_model = new theory::TheoryModel( + d_userContext, "DefaultModel", options::assignFunctionValues()); d_aloc_curr_model = true; } //make the default builder, e.g. in the case that the quantifiers engine does not have a model builder 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 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().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::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 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::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 argTypes = t.getArgTypes(); + vector 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().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 argTypes = t.getArgTypes(); - vector 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(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; diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index b6d1288ae..cee39b542 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -161,6 +161,50 @@ public: * 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 ( 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 ( 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 ( t1...tn ) where k is a kind of this category, we + * check whether ( 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 ( 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 @@ -217,6 +261,8 @@ public: 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? */ @@ -245,6 +291,10 @@ public: std::map d_approximations; /** list of all approximations */ std::vector > d_approx_list; + /** a set of kinds that are not evaluated */ + std::unordered_set d_not_evaluated_kinds; + /** a set of kinds that are semi-evaluated */ + std::unordered_set d_semi_evaluated_kinds; /** map of representatives of equality engine to used representatives in * representative set */ std::map d_reps; diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index e88d1e3be..f91a413e3 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -930,7 +930,10 @@ bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m) bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m) { - assignFunctions(m); + if (m->areFunctionValuesEnabled()) + { + assignFunctions(m); + } return true; } @@ -1098,6 +1101,10 @@ struct sortTypeSize void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m) { + if (!options::assignFunctionValues()) + { + return; + } Trace("model-builder") << "Assigning function values..." << std::endl; std::vector funcs_to_assign = m->getFunctionsToAssign(); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index f5748549e..851f43582 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -75,6 +75,10 @@ void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) { } void TheoryUF::finishInit() { + // combined cardinality constraints are not evaluated in getModelValue + TheoryModel* tm = d_valuation.getModel(); + Assert(tm != nullptr); + tm->setUnevaluatedKind(kind::COMBINED_CARDINALITY_CONSTRAINT); // initialize the strong solver if (options::finiteModelFind() && options::ufssMode()!=UF_SS_NONE) { d_thss = new StrongSolverTheoryUF(getSatContext(), getUserContext(), *d_out, this); -- 2.30.2