summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_propagator.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/inst_propagator.h')
-rw-r--r--src/theory/quantifiers/inst_propagator.h13
1 files changed, 11 insertions, 2 deletions
diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
index 580923fc9..b8ea2c49e 100644
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -113,14 +113,23 @@ private:
InstPropagator& d_ip;
public:
InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}
- virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {
+ virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
+ Node q,
+ Node lem,
+ std::vector<Node>& terms,
+ Node body)
+ {
return d_ip.notifyInstantiation( quant_e, q, lem, terms, body );
}
virtual void filterInstantiations() { d_ip.filterInstantiations(); }
};
InstantiationNotifyInstPropagator d_notify;
/** notify instantiation method */
- bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body );
+ bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
+ Node q,
+ Node lem,
+ std::vector<Node>& terms,
+ Node body);
/** remove instance ids */
void filterInstantiations();
/** allocate instantiation */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback