diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-25 13:17:30 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-25 18:17:30 +0000 |
| commit | 8a3876f74f377817345af405aebfceebc7896059 (patch) | |
| tree | 82474f0df4b65274e6fbbb8a2d3f56ec42815a40 /src/theory/quantifiers/ematching/ho_trigger.cpp | |
| parent | f9e3d2dccd5018e07df1c2cd323c5e192b020819 (diff) | |
Refactor construction of triggers (#6209)
This PR centralizes our utilities for generating triggers. It also splits the statistics class from quantifiers off from quantifiers engine.
Diffstat (limited to 'src/theory/quantifiers/ematching/ho_trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 4cdce940e..a2885cdec 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -34,7 +34,6 @@ namespace quantifiers { namespace inst { HigherOrderTrigger::HigherOrderTrigger( - QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, @@ -42,7 +41,7 @@ HigherOrderTrigger::HigherOrderTrigger( Node q, std::vector<Node>& nodes, std::map<Node, std::vector<Node> >& ho_apps) - : Trigger(qe, qs, qim, qr, tr, q, nodes), d_ho_var_apps(ho_apps) + : Trigger(qs, qim, qr, tr, q, nodes), d_ho_var_apps(ho_apps) { NodeManager* nm = NodeManager::currentNM(); // process the higher-order variable applications |