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.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 30c4dabdf..76fb920bb 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -68,6 +68,8 @@ public:
/* check was complete (e.g. no lemmas implies a model) */
virtual bool checkComplete() { return false; }
/* Called for new quantifiers */
+ virtual void preRegisterQuantifier( Node q ) {}
+ /* Called for new quantifiers after owners are finalized */
virtual void registerQuantifier( Node q ) = 0;
virtual void assertNode( Node n ) = 0;
virtual void propagate( Theory::Effort level ){}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback