diff options
Diffstat (limited to 'src/theory/theory_model_builder.cpp')
| -rw-r--r-- | src/theory/theory_model_builder.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 23a76d273..bbe1588d6 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -130,7 +130,7 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n) { // selectors are always assignable (where we guarantee that they are not // evaluatable here) - if (!d_env.getLogicInfo().isHigherOrder()) + if (!logicInfo().isHigherOrder()) { Assert(!n.getType().isFunction()); return true; @@ -152,7 +152,7 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n) else { // non-function variables, and fully applied functions - if (!d_env.getLogicInfo().isHigherOrder()) + if (!logicInfo().isHigherOrder()) { // no functions exist, all functions are fully applied Assert(n.getKind() != kind::HO_APPLY); @@ -1229,7 +1229,7 @@ bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m) void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) { - Assert(!d_env.getLogicInfo().isHigherOrder()); + Assert(!logicInfo().isHigherOrder()); uf::UfModelTree ufmt(f); Node default_v; for (size_t i = 0; i < m->d_uf_terms[f].size(); i++) @@ -1274,7 +1274,7 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f) { - Assert(d_env.getLogicInfo().isHigherOrder()); + Assert(logicInfo().isHigherOrder()); TypeNode type = f.getType(); std::vector<TypeNode> argTypes = type.getArgTypes(); std::vector<Node> args; @@ -1398,7 +1398,7 @@ void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m) Trace("model-builder") << "Assigning function values..." << std::endl; std::vector<Node> funcs_to_assign = m->getFunctionsToAssign(); - if (d_env.getLogicInfo().isHigherOrder()) + if (logicInfo().isHigherOrder()) { // sort based on type size if higher-order Trace("model-builder") << "Sort functions by type..." << std::endl; @@ -1425,7 +1425,7 @@ void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m) Trace("model-builder") << " Function #" << k << " is " << f << std::endl; // std::map< Node, std::vector< Node > >::iterator itht = // m->d_ho_uf_terms.find( f ); - if (!d_env.getLogicInfo().isHigherOrder()) + if (!logicInfo().isHigherOrder()) { Trace("model-builder") << " Assign function value for " << f << " based on APPLY_UF" << std::endl; |