diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-03-06 09:37:48 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-06 09:37:48 -0800 |
| commit | aa3807f28b47abaa26573439f4dafca0258e4b6b (patch) | |
| tree | ec265cc8ff82df819d8c6acf49902f2be9317b1b /src/theory/quantifiers/equality_query.h | |
| parent | 9bf97a2ac3c923d08cce93ca7eda4360b19dfdec (diff) | |
| parent | e2d714a0839fb80d9a40e9b6fdd8a6fe325a1664 (diff) | |
Merge branch 'master' into cleanup_outputcleanup_output
Diffstat (limited to 'src/theory/quantifiers/equality_query.h')
| -rw-r--r-- | src/theory/quantifiers/equality_query.h | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index 0048cc14f..0b28f53c6 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -50,26 +50,26 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery EqualityQueryQuantifiersEngine(context::Context* c, QuantifiersEngine* qe); virtual ~EqualityQueryQuantifiersEngine(); /** reset */ - virtual bool reset(Theory::Effort e); + bool reset(Theory::Effort e) override; /* Called for new quantifiers */ - virtual void registerQuantifier(Node q) {} + void registerQuantifier(Node q) override {} /** identify */ - virtual std::string identify() const { return "EqualityQueryQE"; } + std::string identify() const override { return "EqualityQueryQE"; } /** does the equality engine have term a */ - bool hasTerm(Node a); + bool hasTerm(Node a) override; /** get the representative of a */ - Node getRepresentative(Node a); + Node getRepresentative(Node a) override; /** are a and b equal? */ - bool areEqual(Node a, Node b); + bool areEqual(Node a, Node b) override; /** are a and b disequal? */ - bool areDisequal(Node a, Node b); + bool areDisequal(Node a, Node b) override; /** get equality engine * This may either be the master equality engine or the model's equality * engine. */ - eq::EqualityEngine* getEngine(); + eq::EqualityEngine* getEngine() override; /** get list of members in the equivalence class of a */ - void getEquivalenceClass(Node a, std::vector<Node>& eqc); + void getEquivalenceClass(Node a, std::vector<Node>& eqc) override; /** get congruent term * If possible, returns a term n such that: * (1) n is a term in the equality engine from getEngine(). @@ -80,7 +80,7 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery * Notice that f should be a "match operator", returned by * TermDb::getMatchOperator. */ - TNode getCongruentTerm(Node f, std::vector<TNode>& args); + TNode getCongruentTerm(Node f, std::vector<TNode>& args) override; /** gets the current best representative in the equivalence * class of a, based on some heuristic. Currently, the default heuristic * chooses terms that were previously chosen as representatives |