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; i<n.getNumChildren(); i++ ){
+ getInstantiationConstants( n[i], ics );
+ }
+ }
+}
+
+
void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){
Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
d_instRows.clear();
ArithVar x = *vi;
if( d_th->d_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<ics.size(); i++ ){
+
+ NodeBuilder<> 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; i<d_quantEngine->getTermDatabase()->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;
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; j<d_quantEngine->getTermDatabase()->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;
}
}
// 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{
}
}
-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<Rational>() );
+ Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[ic][x][var].getConst<Rational>() );
instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );
}
}
projects / cvc5.git / commitdiff