summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r--src/theory/quantifiers_engine.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 4c7cb4a2f..60666c4a9 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -48,6 +48,7 @@ class InstantiationNotify {
public:
InstantiationNotify(){}
virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
+ virtual void filterInstantiations() = 0;
};
namespace quantifiers {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback