From 5ebe47d38892131b96521a729c915365a3369110 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 24 Oct 2012 01:06:15 +0000 Subject: efficient e-matching now specific to rewrite rules --- src/theory/quantifiers/term_database.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'src/theory/quantifiers/term_database.cpp') 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; } -- cgit v1.2.3