diff options
Diffstat (limited to 'src/theory/quantifiers/ematching/ho_trigger.cpp')
-rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.cpp | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 0ab2988d2..4c606a273 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -17,7 +17,6 @@ #include "theory/quantifiers/ematching/ho_trigger.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/uf/theory_uf_rewriter.h" #include "util/hash.h" @@ -31,10 +30,11 @@ namespace inst { HigherOrderTrigger::HigherOrderTrigger( QuantifiersEngine* qe, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, Node q, std::vector<Node>& nodes, std::map<Node, std::vector<Node> >& ho_apps) - : Trigger(qe, qim, q, nodes), d_ho_var_apps(ho_apps) + : Trigger(qe, qim, qr, q, nodes), d_ho_var_apps(ho_apps) { NodeManager* nm = NodeManager::currentNM(); // process the higher-order variable applications @@ -201,11 +201,10 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) // get substitution corresponding to m std::vector<TNode> vars; std::vector<TNode> subs; - quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil(); for (unsigned i = 0, size = d_quant[0].getNumChildren(); i < size; i++) { subs.push_back(m.d_vals[i]); - vars.push_back(tutil->getInstantiationConstant(d_quant, i)); + vars.push_back(d_qreg.getInstantiationConstant(d_quant, i)); } Trace("ho-unif-debug") << "Run higher-order unification..." << std::endl; |