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.cpp | |
parent | 9c4d548af9a14c18a6d69b41bba3e36054d37c0c (diff) |
Remove equality inference option for quantifiers (#3282)
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 27 |
1 files changed, 0 insertions, 27 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a6ec1c077..507d938b4 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -188,7 +188,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, TheoryEngine* te) : d_te(te), d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)), - d_eq_inference(nullptr), d_tr_trie(new inst::TriggerTrie), d_model(nullptr), d_rel_dom(nullptr), @@ -237,9 +236,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_instantiate->addNotify(d_private->d_inst_prop->getInstantiationNotify()); } - if( options::inferArithTriggerEq() ){ - d_eq_inference.reset(new quantifiers::EqualityInference(c, false)); - } d_util.push_back(d_instantiate.get()); @@ -328,10 +324,6 @@ EqualityQuery* QuantifiersEngine::getEqualityQuery() const { return d_eq_query.get(); } -quantifiers::EqualityInference* QuantifiersEngine::getEqualityInference() const -{ - return d_eq_inference.get(); -} quantifiers::RelevantDomain* QuantifiersEngine::getRelevantDomain() const { return d_rel_dom.get(); @@ -1040,25 +1032,6 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within void QuantifiersEngine::eqNotifyNewClass(TNode t) { addTermToDatabase( t ); - if( d_eq_inference ){ - d_eq_inference->eqNotifyNewClass( t ); - } -} - -void QuantifiersEngine::eqNotifyPreMerge(TNode t1, TNode t2) { - if( d_eq_inference ){ - d_eq_inference->eqNotifyMerge( t1, t2 ); - } -} - -void QuantifiersEngine::eqNotifyPostMerge(TNode t1, TNode t2) { - -} - -void QuantifiersEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { - //if( d_qcf ){ - // d_qcf->assertDisequal( t1, t2 ); - //} } bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ |