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/term_database.cpp | |
parent | 304404e3709ff7e95156c87f65a3e2647d9f3441 (diff) |
efficient e-matching now specific to rewrite rules
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 43548f021..493b9e931 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -18,6 +18,7 @@ #include "theory/theory_engine.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/options.h" +#include "theory/rewriterules/efficient_e_matching.h" using namespace std; using namespace CVC4; @@ -82,11 +83,11 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ addTerm( n[i], added, withinQuant ); if( options::efficientEMatching() ){ - uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF ); + EfficientEMatcher* eem = d_quantEngine->getEfficientEMatcher(); if( d_parents[n[i]][op].empty() ){ //must add parent to equivalence class info - Node nir = ith->getRepresentative( n[i] ); - uf::EqClassInfo* eci_nir = ith->getEquivalenceClassInfo( nir ); + Node nir = d_quantEngine->getEqualityQuery()->getRepresentative( n[i] ); + EqClassInfo* eci_nir = eem->getEquivalenceClassInfo( nir ); if( eci_nir ){ eci_nir->d_pfuns[ op ] = true; } |