From 08077fa4c45c95b17eb557610a3950352f9d8a20 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 10 Oct 2014 13:32:49 +0200 Subject: Add owner map to better manage QuantifiersModules. Initial infrastructure for cegqi. --- src/theory/quantifiers/instantiation_engine.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/theory/quantifiers/instantiation_engine.cpp') diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 7207ceefb..9c3673bc2 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -215,7 +215,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine - if( TermDb::isRewriteRule( n ) ){ + if( !d_quantEngine->hasOwnership( n, this ) ){ d_quant_active[n] = false; }else if( !d_quantEngine->getModel()->isQuantifierActive( n ) ){ d_quant_active[n] = false; @@ -300,7 +300,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ } void InstantiationEngine::registerQuantifier( Node f ){ - if( !TermDb::isRewriteRule( f ) ){ + if( d_quantEngine->hasOwnership( f, this ) ){ //Notice() << "do cbqi " << f << " ? " << std::endl; if( options::cbqi() ){ Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); -- cgit v1.2.3