diff options
Diffstat (limited to 'src/theory/quantifiers/ematching/ho_trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index cdfb9c85c..6d13ef2ee 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -231,7 +231,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) d_lchildren.clear(); d_arg_to_arg_rep.clear(); d_arg_vector.clear(); - EqualityQuery* eq = d_quantEngine->getEqualityQuery(); + quantifiers::QuantifiersState& qs = d_quantEngine->getState(); for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs) { TNode var = ha.first; @@ -283,10 +283,10 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) } else if (!itf->second.isNull()) { - if (!eq->areEqual(itf->second, args[k])) + if (!qs.areEqual(itf->second, args[k])) { if (!d_quantEngine->getTermDatabase()->isEntailed( - itf->second.eqNode(args[k]), true, eq)) + itf->second.eqNode(args[k]), true)) { fixed_vals[k] = Node::null(); } @@ -318,7 +318,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) { if (!itf->second.isNull()) { - Node r = eq->getRepresentative(itf->second); + Node r = qs.getRepresentative(itf->second); std::map<Node, unsigned>::iterator itfr = arg_to_rep.find(r); if (itfr != arg_to_rep.end()) { |