diff options
Diffstat (limited to 'src/theory/theory_model.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 4cc25a887..0c14f329a 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -40,7 +40,7 @@ TheoryModel::TheoryModel(Env& env, std::string name, bool enableFuncModels) d_enableFuncModels(enableFuncModels) { // must use function models when ufHo is enabled - Assert(d_enableFuncModels || !d_env.getLogicInfo().isHigherOrder()); + Assert(d_enableFuncModels || !logicInfo().isHigherOrder()); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); } @@ -53,7 +53,7 @@ void TheoryModel::finishInit(eq::EqualityEngine* ee) d_equalityEngine = ee; // The kinds we are treating as function application in congruence d_equalityEngine->addFunctionKind( - kind::APPLY_UF, false, d_env.getLogicInfo().isHigherOrder()); + kind::APPLY_UF, false, logicInfo().isHigherOrder()); d_equalityEngine->addFunctionKind(kind::HO_APPLY); d_equalityEngine->addFunctionKind(kind::SELECT); // d_equalityEngine->addFunctionKind(kind::STORE); @@ -294,8 +294,7 @@ Node TheoryModel::getModelValue(TNode n) const // return the representative of the term in the equality engine, if it exists TypeNode t = ret.getType(); bool eeHasTerm; - if (!d_env.getLogicInfo().isHigherOrder() - && (t.isFunction() || t.isPredicate())) + if (!logicInfo().isHigherOrder() && (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 @@ -694,7 +693,7 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { Trace("model-builder") << " Assigning function (" << f << ") to (" << f_def << ")" << endl; Assert(d_uf_models.find(f) == d_uf_models.end()); - if (d_env.getLogicInfo().isHigherOrder()) + if (logicInfo().isHigherOrder()) { //we must rewrite the function value since the definition needs to be a constant value f_def = Rewriter::rewrite( f_def ); @@ -708,7 +707,7 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { d_uf_models[f] = f_def; } - if (d_env.getLogicInfo().isHigherOrder() && d_equalityEngine->hasTerm(f)) + if (logicInfo().isHigherOrder() && d_equalityEngine->hasTerm(f)) { Trace("model-builder-debug") << " ...function is first-class member of equality engine" << std::endl; // assign to representative if higher-order @@ -743,7 +742,7 @@ std::vector< Node > TheoryModel::getFunctionsToAssign() { Assert(d_env.getTopLevelSubstitutions().apply(n) == n); if( !hasAssignedFunctionDefinition( n ) ){ Trace("model-builder-fun-debug") << "Look at function : " << n << std::endl; - if (d_env.getLogicInfo().isHigherOrder()) + if (logicInfo().isHigherOrder()) { // if in higher-order mode, assign function definitions modulo equality Node r = getRepresentative( n ); |