summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/instantiation_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.h')
-rw-r--r--src/theory/quantifiers/instantiation_engine.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 44612a85c..d6cde9e7f 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -49,6 +49,8 @@ public:
virtual int process( Node f, Theory::Effort effort, int e ) = 0;
/** identify */
virtual std::string identify() const { return std::string("Unknown"); }
+ /** register quantifier */
+ virtual void registerQuantifier( Node q ) {}
};/* class InstStrategy */
class InstantiationEngine : public QuantifiersModule
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback