\r
#include "theory/quantifiers/ambqi_builder.h"\r
#include "theory/quantifiers/term_database.h"\r
-\r
+#include "theory/quantifiers/options.h"\r
\r
using namespace std;\r
using namespace CVC4;\r
}\r
\r
bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth ) {\r
- if( d_value==1 ){\r
- //instantiations are all true : ignore this\r
- return true;\r
- }else{\r
- if( depth==q[0].getNumChildren() ){\r
- if( qe->addInstantiation( q, terms ) ){\r
- Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl;\r
- inst++;\r
- return true;\r
- }else{\r
- Trace("ambqi-inst-debug") << "-> Failed to add instantiation." << std::endl;\r
- //we are incomplete\r
- return false;\r
- }\r
+ if( inst==0 || !options::fmfOneInstPerRound() ){\r
+ if( d_value==1 ){\r
+ //instantiations are all true : ignore this\r
+ return true;\r
}else{\r
- bool osuccess = true;\r
- TypeNode tn = m->getVariable( q, depth ).getType();\r
- for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){\r
- //get witness term\r
- unsigned index = 0;\r
- bool success;\r
- do {\r
- success = false;\r
- index = getId( it->first, index );\r
- if( index<32 ){\r
- Assert( index<m->d_rep_set.d_type_reps[tn].size() );\r
- terms[m->d_var_order[q][depth]] = m->d_rep_set.d_type_reps[tn][index];\r
- //terms[depth] = m->d_rep_set.d_type_reps[tn][index];\r
- if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){\r
- //if we are incomplete, and have not yet added an instantiation, keep trying\r
- index++;\r
- Trace("ambqi-inst-debug") << "At depth " << depth << ", failed branch, no instantiations and incomplete, increment index : " << index << std::endl;\r
- }else{\r
- success = true;\r
+ if( depth==q[0].getNumChildren() ){\r
+ if( qe->addInstantiation( q, terms ) ){\r
+ Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl;\r
+ inst++;\r
+ return true;\r
+ }else{\r
+ Trace("ambqi-inst-debug") << "-> Failed to add instantiation." << std::endl;\r
+ //we are incomplete\r
+ return false;\r
+ }\r
+ }else{\r
+ bool osuccess = true;\r
+ TypeNode tn = m->getVariable( q, depth ).getType();\r
+ for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){\r
+ //get witness term\r
+ unsigned index = 0;\r
+ bool success;\r
+ do {\r
+ success = false;\r
+ index = getId( it->first, index );\r
+ if( index<32 ){\r
+ Assert( index<m->d_rep_set.d_type_reps[tn].size() );\r
+ terms[m->d_var_order[q][depth]] = m->d_rep_set.d_type_reps[tn][index];\r
+ //terms[depth] = m->d_rep_set.d_type_reps[tn][index];\r
+ if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){\r
+ //if we are incomplete, and have not yet added an instantiation, keep trying\r
+ index++;\r
+ Trace("ambqi-inst-debug") << "At depth " << depth << ", failed branch, no instantiations and incomplete, increment index : " << index << std::endl;\r
+ }else{\r
+ success = true;\r
+ }\r
}\r
- }\r
- }while( !success && index<32 );\r
- //mark if we are incomplete\r
- osuccess = osuccess && success;\r
+ }while( !success && index<32 );\r
+ //mark if we are incomplete\r
+ osuccess = osuccess && success;\r
+ }\r
+ return osuccess;\r
}\r
- return osuccess;\r
}\r
+ }else{\r
+ return true;\r
}\r
}\r
\r
InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) :
InstStrategy( ie ), d_th( th ), d_counter( 0 ){
d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );
+ d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
}
bool InstStrategySimplex::calculateShouldProcess( Node f ){
ArithVariables::var_iterator vi, vend;
for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
ArithVar x = *vi;
- if( d_th->d_internal->d_partialModel.hasEitherBound( x ) ){
- Node n = avnm.asNode(x);
-
- //collect instantiation constants
- std::vector< Node > ics;
- getInstantiationConstants( n, ics );
- for( unsigned i=0; i<ics.size(); i++ ){
+ Node n = avnm.asNode(x);
- 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 );
- }
- 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[ics[i]][x] = NodeManager::currentNM()->mkConst( Rational(0) );
- }else if( t.getNumChildren()==1 ){
- d_tableaux_term[ics[i]][x] = t.getChild( 0 );
- }else{
- d_tableaux_term[ics[i]][x] = 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 );
+ }
+ 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[ics[i]][x] = d_zero;
+ }else if( t.getNumChildren()==1 ){
+ d_tableaux_term[ics[i]][x] = t.getChild( 0 );
+ }else{
+ d_tableaux_term[ics[i]][x] = t;
}
}
}
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;
+ //the point instantiation
+ InstMatch m_point( f );
+ bool m_point_valid = true;
+ int lem = 0;
+ //scan over all instantiation rows
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;
+ if( Debug.isOn("quant-arith-simplex") ){
+ Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl;
+ Debug("quant-arith-simplex") << " ";
+ for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){
+ if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
+ Debug("quant-arith-simplex") << it->first << " * " << it->second;
+ }
+ Debug("quant-arith-simplex") << " = ";
+ Node v = getTableauxValue( x, false );
+ Debug("quant-arith-simplex") << v << std::endl;
+ Debug("quant-arith-simplex") << " term : " << d_tableaux_term[ic][x] << std::endl;
+ Debug("quant-arith-simplex") << " ce-term : ";
+ for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){
+ if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
+ Debug("quant-arith-simplex") << it->first << " * " << it->second;
+ }
+ Debug("quant-arith-simplex") << 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( f );
+ for( unsigned k=0; k<f[0].getNumChildren(); k++ ){
+ if( f[0][k].getType().isInteger() ){
+ m.setValue( k, d_zero );
+ }
+ }
//By default, choose the first instantiation constant to be e_i.
Node var = d_ceTableaux[ic][x].begin()->first;
+ //if it is integer, we need to find variable with coefficent +/- 1
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 = it->first;
}
}
- //otherwise, try one that divides all ground term coefficients? DO_THIS
+ //Otherwise, try one that divides all ground term coefficients?
+ // Might be futile, if rewrite ensures gcd of coeffs is 1.
}
if( !var.isNull() ){
+ //add to point instantiation if applicable
+ if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){
+ Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl;
+ Node v = getTableauxValue( x, false );
+ if( !var.getType().isInteger() || v.getType().isInteger() ){
+ m_point.setValue( i, v );
+ }else{
+ m_point_valid = false;
+ }
+ }
Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
- doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var );
+ if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){
+ lem++;
+ }
}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 );
}
}
}
+ if( lem==0 && m_point_valid ){
+ if( d_quantEngine->addInstantiation( f, m_point ) ){
+ Debug("quant-arith-simplex") << "...added point instantiation." << std::endl;
+ }
+ }
}
return STATUS_UNKNOWN;
}
bool InstStrategySimplex::doInstantiation2( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){
// make term ( beta - term )/coeff
+ bool vIsInteger = var.getType().isInteger();
Node beta = getTableauxValue( x, minus_delta );
- Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );
- if( !d_ceTableaux[ic][x][var].isNull() ){
- if( var.getType().isInteger() ){
- 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[ic][x][var].getConst<Rational>() );
- instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );
+ if( !vIsInteger || beta.getType().isInteger() ){
+ Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );
+ if( !d_ceTableaux[ic][x][var].isNull() ){
+ if( vIsInteger ){
+ 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[ic][x][var].getConst<Rational>() );
+ instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );
+ }
}
+ instVal = Rewriter::rewrite( instVal );
+ //use as instantiation value for var
+ int vn = var.getAttribute(InstVarNumAttribute());
+ m.setValue( vn, instVal );
+ Debug("quant-arith") << "Add instantiation " << m << std::endl;
+ return d_quantEngine->addInstantiation( f, m );
+ }else{
+ return false;
}
- instVal = Rewriter::rewrite( instVal );
- //use as instantiation value for var
- int vn = var.getAttribute(InstVarNumAttribute());
- m.setValue( vn, instVal );
- Debug("quant-arith") << "Add instantiation " << m << std::endl;
- return d_quantEngine->addInstantiation( f, m );
}
-
+/*
Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){
if( d_th->d_internal->d_partialModel.hasArithVar(n) ){
ArithVar v = d_th->d_internal->d_partialModel.asArithVar( n );
return NodeManager::currentNM()->mkConst( Rational(0) );
}
}
-
+*/
Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
const Rational& delta = d_th->d_internal->d_partialModel.getDelta();
DeltaRational drv = d_th->d_internal->d_partialModel.getAssignment( v );
projects / cvc5.git / commitdiff