diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-31 17:44:42 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-01 09:46:59 -0500 |
commit | 2cadfe31cfddaff7eff4cd220273d0bab3d2792d (patch) | |
tree | 5a519bf9fe2da10e03ec2a4faf167c09ae1792f7 /src/theory/quantifiers/inst_strategy_cbqi.cpp | |
parent | 07c4b6c27aac497c74695dd559adfee0d9e8e83f (diff) |
Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly.
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 417 |
1 files changed, 331 insertions, 86 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index b9a415e46..f3061f575 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -21,6 +21,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/theory_engine.h" using namespace std; @@ -34,9 +35,13 @@ using namespace CVC4::theory::arith; #define ARITH_INSTANTIATOR_USE_MINUS_DELTA InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) - : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ) + : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), +d_elim_quants( qe->getSatContext() ), +d_nested_qe_waitlist_size( qe->getUserContext() ), +d_nested_qe_waitlist_proc( qe->getUserContext() ) //, d_added_inst( qe->getUserContext() ) { + d_qid_count = 0; } InstStrategyCbqi::~InstStrategyCbqi() throw(){} @@ -55,6 +60,103 @@ unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) { return QuantifiersEngine::QEFFORT_NONE; } +bool InstStrategyCbqi::registerCbqiLemma( Node q ) { + if( !hasAddedCbqiLemma( q ) ){ + d_added_cbqi_lemma.insert( q ); + Trace("cbqi-debug") << "Do cbqi for " << q << std::endl; + //add cbqi lemma + //get the counterexample literal + Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); + Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( q ); + if( !ceBody.isNull() ){ + //add counterexample lemma + Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); + //require any decision on cel to be phase=true + d_quantEngine->addRequirePhase( ceLit, true ); + Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; + //add counterexample lemma + lem = Rewriter::rewrite( lem ); + Trace("cbqi-lemma") << "Counterexample lemma : " << lem << std::endl; + registerCounterexampleLemma( q, lem ); + + //totality lemmas for EPR + QuantEPR * qepr = d_quantEngine->getQuantEPR(); + if( qepr!=NULL ){ + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + TypeNode tn = q[0][i].getType(); + if( tn.isSort() ){ + if( qepr->isEPR( tn ) ){ + //add totality lemma + std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn ); + if( itc!=qepr->d_consts.end() ){ + Assert( !itc->second.empty() ); + Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ); + std::vector< Node > disj; + for( unsigned j=0; j<itc->second.size(); j++ ){ + disj.push_back( ic.eqNode( itc->second[j] ) ); + } + Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ); + Trace("cbqi-lemma") << "EPR totality lemma : " << tlem << std::endl; + d_quantEngine->getOutputChannel().lemma( tlem ); + }else{ + Assert( false ); + } + }else{ + Assert( !options::cbqiAll() ); + } + } + } + } + + //compute dependencies between quantified formulas + if( options::cbqiLitDepend() || options::cbqiInnermost() ){ + std::vector< Node > ics; + TermDb::computeVarContains( q, ics ); + d_parent_quant[q].clear(); + d_children_quant[q].clear(); + std::vector< Node > dep; + for( unsigned i=0; i<ics.size(); i++ ){ + Node qi = ics[i].getAttribute(InstConstantAttribute()); + if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){ + d_parent_quant[q].push_back( qi ); + d_children_quant[qi].push_back( q ); + Node qicel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( qi ); + dep.push_back( qi ); + dep.push_back( qicel ); + } + } + if( !dep.empty() ){ + Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) ); + Trace("cbqi-lemma") << "Counterexample dependency lemma : " << dep_lemma << std::endl; + d_quantEngine->getOutputChannel().lemma( dep_lemma ); + } + } + + //must register all sub-quantifiers of counterexample lemma, register their lemmas + std::vector< Node > quants; + TermDb::computeQuantContains( lem, quants ); + for( unsigned i=0; i<quants.size(); i++ ){ + if( doCbqi( quants[i] ) ){ + registerCbqiLemma( quants[i] ); + } + if( options::cbqiNestedQE() ){ + //record these as counterexample quantifiers + QAttributes qa; + TermDb::computeQuantAttributes( quants[i], qa ); + if( qa.d_qid_num!=-1 ){ + d_id_to_ce_quant[ qa.d_qid_num ] = quants[i]; + d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num; + Trace("cbqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl; + } + } + } + } + return true; + }else{ + return false; + } +} + void InstStrategyCbqi::reset_round( Theory::Effort effort ) { d_cbqi_set_quant_inactive = false; d_incomplete_check = false; @@ -64,77 +166,8 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine if( doCbqi( q ) ){ - if( !hasAddedCbqiLemma( q ) ){ - d_added_cbqi_lemma.insert( q ); - Trace("cbqi") << "Do cbqi for " << q << std::endl; - //add cbqi lemma - //get the counterexample literal - Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); - Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( q ); - if( !ceBody.isNull() ){ - //add counterexample lemma - Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); - //require any decision on cel to be phase=true - d_quantEngine->addRequirePhase( ceLit, true ); - Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; - //add counterexample lemma - lem = Rewriter::rewrite( lem ); - Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; - registerCounterexampleLemma( q, lem ); - - //totality lemmas for EPR - QuantEPR * qepr = d_quantEngine->getQuantEPR(); - if( qepr!=NULL ){ - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - TypeNode tn = q[0][i].getType(); - if( tn.isSort() ){ - if( qepr->isEPR( tn ) ){ - //add totality lemma - std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn ); - if( itc!=qepr->d_consts.end() ){ - Assert( !itc->second.empty() ); - Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ); - std::vector< Node > disj; - for( unsigned j=0; j<itc->second.size(); j++ ){ - disj.push_back( ic.eqNode( itc->second[j] ) ); - } - Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ); - Trace("cbqi") << "EPR totality lemma : " << tlem << std::endl; - d_quantEngine->getOutputChannel().lemma( tlem ); - }else{ - Assert( false ); - } - }else{ - Assert( !options::cbqiAll() ); - } - } - } - } - - //compute dependencies between quantified formulas - if( options::cbqiLitDepend() || options::cbqiInnermost() ){ - std::vector< Node > ics; - TermDb::computeVarContains( q, ics ); - d_parent_quant[q].clear(); - d_children_quant[q].clear(); - std::vector< Node > dep; - for( unsigned i=0; i<ics.size(); i++ ){ - Node qi = ics[i].getAttribute(InstConstantAttribute()); - if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){ - d_parent_quant[q].push_back( qi ); - d_children_quant[qi].push_back( q ); - Node qicel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( qi ); - dep.push_back( qi ); - dep.push_back( qicel ); - } - } - if( !dep.empty() ){ - Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) ); - Trace("cbqi") << "Counterexample dependency lemma : " << dep_lemma << std::endl; - d_quantEngine->getOutputChannel().lemma( dep_lemma ); - } - } - } + if( registerCbqiLemma( q ) ){ + Debug("cbqi-debug") << "Registered cbqi lemma." << std::endl; //set inactive the quantified formulas whose CE literals are asserted false }else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ d_active_quant[q] = true; @@ -147,9 +180,24 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { if( d_quantEngine->getValuation().isDecision( cel ) ){ Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl; }else{ + Trace("cbqi") << "Inactive : " << q << std::endl; d_quantEngine->getModel()->setQuantifierActive( q, false ); d_cbqi_set_quant_inactive = true; d_active_quant.erase( q ); + d_elim_quants.insert( q ); + Trace("cbqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl; + //process from waitlist + while( d_nested_qe_waitlist_proc[q]<d_nested_qe_waitlist_size[q] ){ + int index = d_nested_qe_waitlist_proc[q]; + Assert( index>=0 ); + Assert( index<(int)d_nested_qe_waitlist[q].size() ); + Node nq = d_nested_qe_waitlist[q][index]; + Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts ); + Node dqelem = nq.iffNode( nqeqn ); + Trace("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl; + d_quantEngine->getOutputChannel().lemma( dqelem ); + d_nested_qe_waitlist_proc[q] = index + 1; + } } } }else{ @@ -204,9 +252,15 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) { // if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ Node q = it->first; - process( q, e, ee ); - if( d_quantEngine->inConflict() ){ - break; + Trace("cbqi") << "CBQI : Process " << q << " at effort " << ee << std::endl; + if( d_nested_qe.find( q )==d_nested_qe.end() ){ + process( q, e, ee ); + if( d_quantEngine->inConflict() ){ + break; + } + }else{ + Trace("cbqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl; + Assert( false ); } } if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ @@ -231,11 +285,79 @@ bool InstStrategyCbqi::checkComplete() { } } +Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ){ + std::map< Node, Node >::iterator it = visited.find( n ); + if( it==visited.end() ){ + Node ret = n; + if( n.getKind()==FORALL ){ + QAttributes qa; + TermDb::computeQuantAttributes( n, qa ); + if( qa.d_qid_num==-1 ){ + std::vector< Node > rc; + rc.push_back( n[0] ); + rc.push_back( getIdMarkedQuantNode( n[1], visited ) ); + Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() ); + QuantIdNumAttribute ida; + avar.setAttribute(ida,d_qid_count); + d_qid_count++; + std::vector< Node > iplc; + iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) ); + if( n.getNumChildren()==3 ){ + for( unsigned i=0; i<n[2].getNumChildren(); i++ ){ + iplc.push_back( n[2][i] ); + } + } + rc.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) ); + ret = NodeManager::currentNM()->mkNode( FORALL, rc ); + } + }else if( n.getNumChildren()>0 ){ + std::vector< Node > children; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + bool childChanged = false; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nc = getIdMarkedQuantNode( n[i], visited ); + childChanged = childChanged || nc!=n[i]; + children.push_back( nc ); + } + if( childChanged ){ + ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); + } + } + visited[n] = ret; + return ret; + }else{ + return it->second; + } +} + void InstStrategyCbqi::preRegisterQuantifier( Node q ) { if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){ if( !options::cbqiAll() && !options::cbqiSplx() ){ //take full ownership of the quantified formula d_quantEngine->setOwner( q, this ); + + //mark all nested quantifiers with id + if( options::cbqiNestedQE() ){ + std::map< Node, Node > visited; + Node mq = getIdMarkedQuantNode( q[1], visited ); + if( mq!=q[1] ){ + //do not do cbqi + d_do_cbqi[q] = false; + //instead do reduction + std::vector< Node > qqc; + qqc.push_back( q[0] ); + qqc.push_back( mq ); + if( q.getNumChildren()==3 ){ + qqc.push_back( q[2] ); + } + Node qq = NodeManager::currentNM()->mkNode( FORALL, qqc ); + Node mlem = NodeManager::currentNM()->mkNode( IMPLIES, q, qq ); + Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl; + d_quantEngine->getOutputChannel().lemma( mlem ); + } + } } } } @@ -244,6 +366,97 @@ void InstStrategyCbqi::registerQuantifier( Node q ) { } +Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ) { + // there is a nested quantified formula (forall y. nq[y,x]) such that + // q is (forall y. nq[y,t]) for ground terms t, + // ceq is (forall y. nq[y,e]) for CE variables e. + // we call this function when we know (exists e. ceq[e,k]) is equivalent to quantifier-free formula C[k]. + // in this case, q is equivalent to the quantifier-free formula C[t]. + if( d_nested_qe.find( ceq )==d_nested_qe.end() ){ + d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq ); + Trace("cbqi-nqe") << "CE quantifier elimination : " << std::endl; + Trace("cbqi-nqe") << " " << ceq << std::endl; + Trace("cbqi-nqe") << " " << d_nested_qe[ceq] << std::endl; + //should not contain quantifiers + Assert( !QuantifiersRewriter::containsQuantifiers( d_nested_qe[ceq] ) ); + } + Assert( d_quantEngine->getTermDatabase()->d_inst_constants[q].size()==inst_terms.size() ); + //replace inst constants with instantiation + Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermDatabase()->d_inst_constants[q].begin(), + d_quantEngine->getTermDatabase()->d_inst_constants[q].end(), + inst_terms.begin(), inst_terms.end() ); + if( doVts ){ + //do virtual term substitution + ret = Rewriter::rewrite( ret ); + ret = d_quantEngine->getTermDatabase()->rewriteVtsSymbols( ret ); + } + Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl; + Trace("cbqi-nqe") << " " << n << std::endl; + Trace("cbqi-nqe") << " " << ret << std::endl; + return ret; +} + +Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ) { + std::map< Node, Node >::iterator it = visited.find( n ); + if( visited.find( n )==visited.end() ){ + Node ret = n; + if( n.getKind()==FORALL ){ + QAttributes qa; + TermDb::computeQuantAttributes( n, qa ); + if( qa.d_qid_num!=-1 ){ + //if it has an id, check whether we have done quantifier elimination for this id + std::map< int, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num ); + if( it!=d_id_to_ce_quant.end() ){ + Node ceq = it->second; + bool doNestedQe = d_elim_quants.contains( ceq ); + if( doNestedQe ){ + ret = doNestedQENode( q, ceq, n, inst_terms, doVts ); + }else{ + Trace("cbqi-nqe") << "Add to nested qe waitlist : " << std::endl; + Node nr = Rewriter::rewrite( n ); + Trace("cbqi-nqe") << " " << ceq << std::endl; + Trace("cbqi-nqe") << " " << nr << std::endl; + int wlsize = d_nested_qe_waitlist_size[ceq] + 1; + d_nested_qe_waitlist_size[ceq] = wlsize; + if( wlsize<(int)d_nested_qe_waitlist[ceq].size() ){ + d_nested_qe_waitlist[ceq][wlsize] = nr; + }else{ + d_nested_qe_waitlist[ceq].push_back( nr ); + } + d_nested_qe_info[nr].d_q = q; + d_nested_qe_info[nr].d_inst_terms.clear(); + d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() ); + d_nested_qe_info[nr].d_doVts = doVts; + } + } + } + }else if( n.getNumChildren()>0 ){ + std::vector< Node > children; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + bool childChanged = false; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nc = doNestedQERec( q, n[i], visited, inst_terms, doVts ); + childChanged = childChanged || nc!=n[i]; + children.push_back( nc ); + } + if( childChanged ){ + ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); + } + } + visited[n] = ret; + return ret; + }else{ + return n; + } +} + +Node InstStrategyCbqi::doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ) { + std::map< Node, Node > visited; + return doNestedQERec( q, lem, visited, inst_terms, doVts ); +} + void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){ Trace("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; d_quantEngine->addLemma( lem, false ); @@ -299,14 +512,17 @@ int InstStrategyCbqi::hasNonCbqiVariable( Node q ){ bool InstStrategyCbqi::doCbqi( Node q ){ std::map< Node, bool >::iterator it = d_do_cbqi.find( q ); if( it==d_do_cbqi.end() ){ - bool ret = false; - if( d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){ - ret = true; - }else{ + bool ret = true; + if( !d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){ //if has an instantiation pattern, don't do it if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){ - ret = false; - }else{ + for( unsigned i=0; i<q[2].getNumChildren(); i++ ){ + if( q[2][i].getKind()==INST_PATTERN ){ + ret = false; + } + } + } + if( ret ){ if( options::cbqiAll() ){ ret = true; }else{ @@ -320,11 +536,13 @@ bool InstStrategyCbqi::doCbqi( Node q ){ }else if( ncbqiv==0 ){ std::map< Node, bool > visited; ret = !hasNonCbqiOperator( q[1], visited ); + }else{ + ret = false; } } } } - Trace("cbqi") << "doCbqi " << q << " returned " << ret << std::endl; + Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl; d_do_cbqi[q] = ret; return ret; }else{ @@ -332,10 +550,20 @@ bool InstStrategyCbqi::doCbqi( Node q ){ } } -Node InstStrategyCbqi::getNextDecisionRequest(){ - // all counterexample literals that are not asserted - for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); +Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ) { + if( proc.find( q )==proc.end() ){ + proc[q] = true; + //first check children + std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( q ); + if( itc!=d_children_quant.end() ){ + for( unsigned j=0; j<itc->second.size(); j++ ){ + Node d = getNextDecisionRequestProc( itc->second[j], proc ); + if( !d.isNull() ){ + return d; + } + } + } + //then check self if( hasAddedCbqiLemma( q ) ){ Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); bool value; @@ -343,6 +571,18 @@ Node InstStrategyCbqi::getNextDecisionRequest(){ Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl; return cel; } + } + } + return Node::null(); +} + +Node InstStrategyCbqi::getNextDecisionRequest(){ + std::map< Node, bool > proc; + for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + Node d = getNextDecisionRequestProc( q, proc ); + if( !d.isNull() ){ + return d; } } return Node::null(); @@ -755,6 +995,9 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { //d_added_inst.insert( d_curr_quant ); return true; }else{ + //this should never happen for monotonic selection strategies + Trace("cbqi-warn") << "Existing instantiation" << std::endl; + Assert( !options::cbqiNestedQE() || options::cbqiAll() ); return false; } } @@ -827,7 +1070,9 @@ void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) { void InstStrategyCegqi::presolve() { if( options::cbqiPreRegInst() ){ for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){ + Trace("cbqi-presolve") << "Presolve " << it->first << std::endl; it->second->presolve( it->first ); } } } + |