diff options
Diffstat (limited to 'src/theory/quantifiers/ematching/inst_strategy.h')
-rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy.h | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index cbe6e341b..9d304368c 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.h +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -24,11 +24,12 @@ namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { +namespace inst { +class TriggerDatabase; +} + class QuantifiersState; class QuantifiersInferenceManager; class QuantifiersRegistry; @@ -49,7 +50,7 @@ enum class InstStrategyStatus class InstStrategy { public: - InstStrategy(QuantifiersEngine* qe, + InstStrategy(inst::TriggerDatabase& td, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, @@ -70,8 +71,8 @@ class InstStrategy * maintained by the quantifiers state. */ options::UserPatMode getInstUserPatMode() const; - /** reference to the instantiation engine */ - QuantifiersEngine* d_quantEngine; + /** reference to the trigger database */ + inst::TriggerDatabase& d_td; /** The quantifiers state object */ QuantifiersState& d_qstate; /** The quantifiers inference manager object */ |