diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-16 17:18:05 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-16 17:18:05 -0500 |
| commit | 54abd196cb43422c77a74cb139f3aaebaa695639 (patch) | |
| tree | 2a65e959b8d17d06fc953320ae15575133b95d17 /src/theory/quantifiers_engine.h | |
| parent | 9c4d548af9a14c18a6d69b41bba3e36054d37c0c (diff) | |
Remove equality inference option for quantifiers (#3282)
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 0a534d090..e1fc742af 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -25,7 +25,6 @@ #include "expr/attribute.h" #include "expr/term_canonize.h" #include "theory/quantifiers/ematching/trigger.h" -#include "theory/quantifiers/equality_infer.h" #include "theory/quantifiers/equality_query.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_builder.h" @@ -106,8 +105,6 @@ public: inst::TriggerTrie* getTriggerDatabase() const; //---------------------- end utilities //---------------------- utilities (TODO move these utilities #1163) - /** get the equality inference */ - quantifiers::EqualityInference* getEqualityInference() const; /** get relevant domain */ quantifiers::RelevantDomain* getRelevantDomain() const; //---------------------- end utilities @@ -228,9 +225,6 @@ public: void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); /** notification when master equality engine is updated */ void eqNotifyNewClass(TNode t); - void eqNotifyPreMerge(TNode t1, TNode t2); - void eqNotifyPostMerge(TNode t1, TNode t2); - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); /** use model equality engine */ bool usingModelEqualityEngine() const { return d_useModelEe; } /** debug print equality engine */ @@ -316,8 +310,6 @@ public: //------------- quantifiers utilities /** equality query class */ std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query; - /** equality inference class */ - std::unique_ptr<quantifiers::EqualityInference> d_eq_inference; /** all triggers will be stored in this trie */ std::unique_ptr<inst::TriggerTrie> d_tr_trie; /** extended model object */ |