Document term db (#1220)

* Document TermDb and related classes. Minor changes to quantifiers utils and their interface.  Address some comments left over from PR 1206.

* Minor

* Minor

* Change namespace style.

* Address review

* Fix incorrectly merged portion that led to regression failures.

* New clang format, fully document relevant domain.

* Clang format again.

* Minor

1 files changed, 8 insertions, 4 deletions

diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
index 6c058c258..580923fc9 100644
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -38,9 +38,11 @@ public:
   EqualityQueryInstProp( QuantifiersEngine* qe );
   ~EqualityQueryInstProp(){};
   /** reset */
-  bool reset( Theory::Effort e );
+  virtual bool reset(Theory::Effort e);
+  /* Called for new quantifiers */
+  virtual void registerQuantifier(Node q) {}
   /** identify */
-  std::string identify() const { return "EqualityQueryInstProp"; }
+  virtual std::string identify() const { return "EqualityQueryInstProp"; }
   /** extends engine */
   bool extendsEngine() { return true; }
   /** contains term */
@@ -161,9 +163,11 @@ public:
   InstPropagator( QuantifiersEngine* qe );
   ~InstPropagator(){}
   /** reset */
-  bool reset( Theory::Effort e );
+  virtual bool reset(Theory::Effort e) override;
+  /* Called for new quantifiers */
+  virtual void registerQuantifier(Node q) override {}
   /** identify */
-  std::string identify() const { return "InstPropagator"; }
+  virtual std::string identify() const override { return "InstPropagator"; }
   /** get the notify mechanism */
   InstantiationNotify* getInstantiationNotify() { return &d_notify; }
 };