From: Andrew Reynolds Date: Mon, 22 Jul 2013 22:59:47 +0000 (-0500) Subject: initial modifications for per-ic cbqi X-Git-Tag: cvc5-1.0.0~7287^2~38 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fc34e25ce2df4c0fb41b7521cc033afd688e0295;p=cvc5.git initial modifications for per-ic cbqi --- diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index a5031a061..4fe4072a3 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -41,6 +41,19 @@ bool InstStrategySimplex::calculateShouldProcess( Node f ){ return false; } +void getInstantiationConstants( Node n, std::vector< Node >& ics ){ + if( n.getKind()==INST_CONSTANT ){ + if( std::find( ics.begin(), ics.end(), n )==ics.end() ){ + ics.push_back( n ); + } + }else{ + for( unsigned i=0; id_internal->d_partialModel.hasEitherBound( x ) ){ Node n = avnm.asNode(x); - Node f; - NodeBuilder<> t(kind::PLUS); - if( n.getKind()==PLUS ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - addTermToRow( x, n[i], f, t ); + + //collect instantiation constants + std::vector< Node > ics; + getInstantiationConstants( n, ics ); + for( unsigned i=0; i t(kind::PLUS); + if( n.getKind()==PLUS ){ + for( int j=0; j<(int)n.getNumChildren(); j++ ){ + addTermToRow( ics[i], x, n[j], t ); + } + }else{ + addTermToRow( ics[i], x, n, t ); } - }else{ - addTermToRow( x, n, f, t ); - } - if( f!=Node::null() ){ - d_instRows[f].push_back( x ); + d_instRows[ics[i]].push_back( x ); //this theory has constraints from f + Node f = TermDb::getInstConstAttr(ics[i]); Debug("quant-arith") << "Has constraints from " << f << std::endl; //set that we should process it d_quantActive[ f ] = true; //set tableaux term if( t.getNumChildren()==0 ){ - d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) ); + d_tableaux_term[ics[i]][x] = NodeManager::currentNM()->mkConst( Rational(0) ); }else if( t.getNumChildren()==1 ){ - d_tableaux_term[x] = t.getChild( 0 ); + d_tableaux_term[ics[i]][x] = t.getChild( 0 ); }else{ - d_tableaux_term[x] = t; + d_tableaux_term[ics[i]][x] = t; } } } } //print debug + Debug("quant-arith-debug") << std::endl; debugPrint( "quant-arith-debug" ); d_counter++; } -int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ - if( e<2 ){ - return STATUS_UNFINISHED; - }else if( e==2 ){ - //Notice() << f << std::endl; - //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl; - //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl; - Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_instRows[f].size() << std::endl; - for( int j=0; j<(int)d_instRows[f].size(); j++ ){ - ArithVar x = d_instRows[f][j]; - if( !d_ceTableaux[x].empty() ){ - Debug("quant-arith-simplex") << "Check row " << x << std::endl; - //instantiation row will be A*e + B*t = beta, - // where e is a vector of terms , and t is vector of ground terms. - // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant - // We will construct the term ( beta - B*t)/coeff to use for e_i. - InstMatch m; - //By default, choose the first instantiation constant to be e_i. - Node var = d_ceTableaux[x].begin()->first; - if( var.getType().isInteger() ){ - std::map< Node, Node >::iterator it = d_ceTableaux[x].begin(); - //try to find coefficent that is +/- 1 - while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){ - ++it; - if( it==d_ceTableaux[x].end() ){ - var = Node::null(); - }else{ - var = it->first; - } - } - //otherwise, try one that divides all ground term coefficients? DO_THIS - } - if( !var.isNull() ){ - Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl; - doInstantiation( f, d_tableaux_term[x], x, m, var ); - }else{ - Debug("quant-arith-simplex") << "Could not find var." << std::endl; - } - ////choose a new variable based on alternation strategy - //int index = d_counter%(int)d_th->d_ceTableaux[x].size(); - //Node var; - //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){ - // if( index==0 ){ - // var = it->first; - // break; - // } - // index--; - //} - //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var ); - } - } - } - return STATUS_UNKNOWN; -} - - -void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){ +void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<>& t ){ if( n.getKind()==MULT ){ if( TermDb::hasInstConstAttr(n[1]) ){ - f = TermDb::getInstConstAttr(n[1]); - if( n[1].getKind()==INST_CONSTANT ){ - d_ceTableaux[x][ n[1] ] = n[0]; + if( n[1]==i ){ + d_ceTableaux[i][x][ n[1] ] = n[0]; }else{ - d_tableaux_ce_term[x][ n[1] ] = n[0]; + d_tableaux_ce_term[i][x][ n[1] ] = n[0]; } }else{ - d_tableaux[x][ n[1] ] = n[0]; + d_tableaux[i][x][ n[1] ] = n[0]; t << n; } }else{ if( TermDb::hasInstConstAttr(n) ){ - f = TermDb::getInstConstAttr(n); - if( n.getKind()==INST_CONSTANT ){ - d_ceTableaux[x][ n ] = Node::null(); + if( n==i ){ + d_ceTableaux[i][x][ n ] = Node::null(); }else{ - d_tableaux_ce_term[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); + d_tableaux_ce_term[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); } }else{ - d_tableaux[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); + d_tableaux[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); t << n; } } } +int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ + if( e<2 ){ + return STATUS_UNFINISHED; + }else if( e==2 ){ + //Notice() << f << std::endl; + //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl; + //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl; + for( int i=0; igetTermDatabase()->getNumInstantiationConstants( f ); i++ ){ + Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); + Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl; + for( int j=0; j<(int)d_instRows[ic].size(); j++ ){ + ArithVar x = d_instRows[ic][j]; + if( !d_ceTableaux[ic][x].empty() ){ + Debug("quant-arith-simplex") << "Check row " << ic << " " << x << std::endl; + //instantiation row will be A*e + B*t = beta, + // where e is a vector of terms , and t is vector of ground terms. + // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant + // We will construct the term ( beta - B*t)/coeff to use for e_i. + InstMatch m; + //By default, choose the first instantiation constant to be e_i. + Node var = d_ceTableaux[ic][x].begin()->first; + if( var.getType().isInteger() ){ + std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); + //try to find coefficent that is +/- 1 + while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){ + ++it; + if( it==d_ceTableaux[ic][x].end() ){ + var = Node::null(); + }else{ + var = it->first; + } + } + //otherwise, try one that divides all ground term coefficients? DO_THIS + } + if( !var.isNull() ){ + Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl; + doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ); + }else{ + Debug("quant-arith-simplex") << "Could not find var." << std::endl; + } + ////choose a new variable based on alternation strategy + //int index = d_counter%(int)d_th->d_ceTableaux[x].size(); + //Node var; + //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){ + // if( index==0 ){ + // var = it->first; + // break; + // } + // index--; + //} + //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var ); + } + } + } + } + return STATUS_UNKNOWN; +} + + void InstStrategySimplex::debugPrint( const char* c ){ ArithVariables& avnm = d_th->d_internal->d_partialModel; ArithVariables::var_iterator vi, vend; @@ -218,14 +238,17 @@ void InstStrategySimplex::debugPrint( const char* c ){ Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); } Debug(c) << std::endl; - Debug(c) << " Instantiation rows: "; - for( int i=0; i<(int)d_instRows[f].size(); i++ ){ - if( i>0 ){ - Debug(c) << ", "; + for( int j=0; jgetTermDatabase()->getNumInstantiationConstants( f ); j++ ){ + Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j ); + Debug(c) << " Instantiation rows for " << ic << " : "; + for( int i=0; i<(int)d_instRows[ic].size(); i++ ){ + if( i>0 ){ + Debug(c) << ", "; + } + Debug(c) << d_instRows[ic][i]; } - Debug(c) << d_instRows[f][i]; + Debug(c) << std::endl; } - Debug(c) << std::endl; } } @@ -234,15 +257,15 @@ void InstStrategySimplex::debugPrint( const char* c ){ // t[e] is a vector of terms containing instantiation constants from f, // and term is a ground term (c1*t1 + ... + cn*tn). // We construct the term ( beta - term )/coeff to use as an instantiation for var. -bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){ +bool InstStrategySimplex::doInstantiation( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var ){ //first try +delta - if( doInstantiation2( f, term, x, m, var ) ){ + if( doInstantiation2( f, ic, term, x, m, var ) ){ ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith); return true; }else{ #ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA //otherwise try -delta - if( doInstantiation2( f, term, x, m, var, true ) ){ + if( doInstantiation2( f, ic, term, x, m, var, true ) ){ ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith_minus); return true; }else{ @@ -254,16 +277,16 @@ bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMa } } -bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){ +bool InstStrategySimplex::doInstantiation2( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){ // make term ( beta - term )/coeff Node beta = getTableauxValue( x, minus_delta ); Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term ); - if( !d_ceTableaux[x][var].isNull() ){ + if( !d_ceTableaux[ic][x][var].isNull() ){ if( var.getType().isInteger() ){ - Assert( d_ceTableaux[x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) ); - instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[x][var], instVal ); + Assert( d_ceTableaux[ic][x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) ); + instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[ic][x][var], instVal ); }else{ - Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[x][var].getConst() ); + Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[ic][x][var].getConst() ); instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal ); } } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index a45318489..821beeae0 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -49,19 +49,19 @@ private: /** for each quantifier, simplex rows */ std::map< Node, std::vector< arith::ArithVar > > d_instRows; /** tableaux */ - std::map< arith::ArithVar, Node > d_tableaux_term; - std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux_ce_term; - std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux; + std::map< Node, std::map< arith::ArithVar, Node > > d_tableaux_term; + std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux_ce_term; + std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux; /** ce tableaux */ - std::map< arith::ArithVar, std::map< Node, Node > > d_ceTableaux; + std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_ceTableaux; /** get value */ Node getTableauxValue( Node n, bool minus_delta = false ); Node getTableauxValue( arith::ArithVar v, bool minus_delta = false ); /** do instantiation */ - bool doInstantiation( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var ); - bool doInstantiation2( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false ); + bool doInstantiation( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var ); + bool doInstantiation2( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false ); /** add term to row */ - void addTermToRow( arith::ArithVar x, Node n, Node& f, NodeBuilder<>& t ); + void addTermToRow( Node ic, arith::ArithVar x, Node n, NodeBuilder<>& t ); /** print debug */ void debugPrint( const char* c ); private: