diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-24 01:06:15 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-24 01:06:15 +0000 |
| commit | 5ebe47d38892131b96521a729c915365a3369110 (patch) | |
| tree | 59e8f2f3b9de3a9f81e178de7d18124ddc4f3c32 /src/theory/quantifiers_engine.cpp | |
| parent | 304404e3709ff7e95156c87f65a3e2647d9f3441 (diff) | |
efficient e-matching now specific to rewrite rules
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a44a3ff1f..486e6721b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -25,6 +25,7 @@ #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" +#include "theory/rewriterules/efficient_e_matching.h" using namespace std; using namespace CVC4; @@ -39,6 +40,7 @@ d_quant_rel( false ){ //currently do not care about relevance d_eq_query = new EqualityQueryQuantifiersEngine( this ); d_term_db = new quantifiers::TermDb( this ); d_tr_trie = new inst::TriggerTrie; + d_eem = new EfficientEMatcher( this ); d_hasAddedLemma = false; //the model object @@ -194,8 +196,7 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){ std::set< Node > added; getTermDatabase()->addTerm( n, added, withinQuant ); if( options::efficientEMatching() ){ - uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)getInstantiator( THEORY_UF ); - d_ith->newTerms(added); + d_eem->newTerms( added ); } //added contains also the Node that just have been asserted in this branch for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){ |