summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ematching/inst_strategy.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/ematching/inst_strategy.h')
-rw-r--r--src/theory/quantifiers/ematching/inst_strategy.h6
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h
index b9d0aa745..1455ce0c5 100644
--- a/src/theory/quantifiers/ematching/inst_strategy.h
+++ b/src/theory/quantifiers/ematching/inst_strategy.h
@@ -31,6 +31,7 @@ namespace quantifiers {
class QuantifiersState;
class QuantifiersInferenceManager;
+class QuantifiersRegistry;
/** A status response to process */
enum class InstStrategyStatus
@@ -49,7 +50,8 @@ class InstStrategy
public:
InstStrategy(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim);
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr);
virtual ~InstStrategy();
/** presolve */
virtual void presolve();
@@ -72,6 +74,8 @@ class InstStrategy
QuantifiersState& d_qstate;
/** The quantifiers inference manager object */
QuantifiersInferenceManager& d_qim;
+ /** The quantifiers registry */
+ QuantifiersRegistry& d_qreg;
}; /* class InstStrategy */
} // namespace quantifiers
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback