diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-28 09:13:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-28 09:13:13 -0500 |
commit | 34e84a25a044e3af192bb69089467c2125911900 (patch) | |
tree | 924a3ae0894bfec136f91949a1bf55e19c4125da /src/theory/quantifiers/inst_propagator.h | |
parent | 675e82e32a34911163f9de0e6389eb107be5b0f1 (diff) |
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
Diffstat (limited to 'src/theory/quantifiers/inst_propagator.h')
-rw-r--r-- | src/theory/quantifiers/inst_propagator.h | 12 |
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; } }; |