//must be an eligible term
if( isEligible( n ) ){
Node ns;
- Node pv_coeff; //coefficient of pv in the equality we solve (null is 1)
+ TermProperties pv_prop; //coefficient of pv in the equality we solve (null is 1)
bool proc = false;
if( !d_prog_var[n].empty() ){
- ns = applySubstitution( pvtn, n, sf, pv_coeff, false );
+ ns = applySubstitution( pvtn, n, sf, pv_prop, false );
if( !ns.isNull() ){
computeProgVars( ns );
//substituted version must be new and cannot contain pv
proc = true;
}
if( proc ){
- if( vinst->processEqualTerm( this, sf, pv, pv_coeff, ns, effort ) ){
+ if( vinst->processEqualTerm( this, sf, pv, pv_prop, ns, effort ) ){
return true;
}
}
std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r );
std::vector< Node > lhs;
std::vector< bool > lhs_v;
- std::vector< Node > lhs_coeff;
+ std::vector< TermProperties > lhs_prop;
Assert( it_reqc!=d_curr_eqc.end() );
for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){
Node n = it_reqc->second[kk];
//must be an eligible term
if( isEligible( n ) ){
Node ns;
- Node pv_coeff;
+ TermProperties pv_prop;
if( !d_prog_var[n].empty() ){
- ns = applySubstitution( pvtn, n, sf, pv_coeff );
+ ns = applySubstitution( pvtn, n, sf, pv_prop );
if( !ns.isNull() ){
computeProgVars( ns );
}
if( !ns.isNull() ){
bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end();
Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl;
- std::vector< Node > term_coeffs;
+ std::vector< TermProperties > term_props;
std::vector< Node > terms;
- term_coeffs.push_back( pv_coeff );
+ term_props.push_back( pv_prop );
terms.push_back( ns );
for( unsigned j=0; j<lhs.size(); j++ ){
//if this term or the another has pv in it, try to solve for it
if( hasVar || lhs_v[j] ){
Trace("cbqi-inst-debug") << "... " << i << "...try based on equality " << lhs[j] << " = " << ns << std::endl;
- //processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { return false; }
- term_coeffs.push_back( lhs_coeff[j] );
+ term_props.push_back( lhs_prop[j] );
terms.push_back( lhs[j] );
- if( vinst->processEquality( this, sf, pv, term_coeffs, terms, effort ) ){
+ if( vinst->processEquality( this, sf, pv, term_props, terms, effort ) ){
return true;
}
- term_coeffs.pop_back();
+ term_props.pop_back();
terms.pop_back();
}
}
lhs.push_back( ns );
lhs_v.push_back( hasVar );
- lhs_coeff.push_back( pv_coeff );
+ lhs_prop.push_back( pv_prop );
}else{
Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible after substitution." << std::endl;
}
}
#endif
Node mv = getModelValue( pv );
- Node pv_coeff_m;
+ TermProperties pv_prop_m;
Trace("cbqi-inst-debug") << "[5] " << i << "...try model value " << mv << std::endl;
int new_effort = use_model_value ? effort : 1;
- if( doAddInstantiationInc( pv, mv, pv_coeff_m, 0, sf, new_effort ) ){
+ if( doAddInstantiationInc( pv, mv, pv_prop_m, sf, new_effort ) ){
return true;
}
}
d_stack_vars.pop_back();
}
-bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int bt, SolvedForm& sf, unsigned effort ) {
- if( d_curr_subs_proc[pv][n].find( pv_coeff )==d_curr_subs_proc[pv][n].end() ){
- d_curr_subs_proc[pv][n][pv_coeff] = true;
+bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv_prop, SolvedForm& sf, unsigned effort ) {
+ Node cnode = pv_prop.getCacheNode();
+ if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){
+ d_curr_subs_proc[pv][n][cnode] = true;
if( Trace.isOn("cbqi-inst") ){
for( unsigned j=0; j<sf.d_subs.size(); j++ ){
Trace("cbqi-inst") << " ";
}
Trace("cbqi-inst") << sf.d_subs.size() << ": ";
- if( !pv_coeff.isNull() ){
- Trace("cbqi-inst") << pv_coeff << " * ";
+ if( !pv_prop.d_coeff.isNull() ){
+ Trace("cbqi-inst") << pv_prop.d_coeff << " * ";
}
Trace("cbqi-inst") << pv << " -> " << n << std::endl;
Assert( n.getType().isSubtypeOf( pv.getType() ) );
a_subs.push_back( n );
std::vector< Node > a_var;
a_var.push_back( pv );
- std::vector< Node > a_coeff;
+ std::vector< TermProperties > a_prop;
std::vector< Node > a_has_coeff;
- if( !pv_coeff.isNull() ){
- a_coeff.push_back( pv_coeff );
+ if( !pv_prop.d_coeff.isNull() ){
+ a_prop.push_back( pv_prop );
a_has_coeff.push_back( pv );
}
bool success = true;
std::map< int, Node > prev_subs;
- std::map< int, Node > prev_coeff;
+ std::map< int, TermProperties > prev_prop;
std::map< int, Node > prev_sym_subs;
std::vector< Node > new_has_coeff;
Trace("cbqi-inst-debug2") << "Applying substitutions..." << std::endl;
prev_subs[j] = sf.d_subs[j];
TNode tv = pv;
TNode ts = n;
- Node a_pv_coeff;
- Node new_subs = applySubstitution( sf.d_vars[j].getType(), sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true );
+ TermProperties a_pv_prop;
+ Node new_subs = applySubstitution( sf.d_vars[j].getType(), sf.d_subs[j], a_subs, a_prop, a_has_coeff, a_var, a_pv_prop, true );
if( !new_subs.isNull() ){
sf.d_subs[j] = new_subs;
- if( !a_pv_coeff.isNull() ){
- prev_coeff[j] = sf.d_coeff[j];
- if( sf.d_coeff[j].isNull() ){
+ if( !a_pv_prop.d_coeff.isNull() ){
+ prev_prop[j] = sf.d_props[j];
+ if( sf.d_props[j].d_coeff.isNull() ){
Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), sf.d_vars[j] )==sf.d_has_coeff.end() );
//now has coefficient
new_has_coeff.push_back( sf.d_vars[j] );
sf.d_has_coeff.push_back( sf.d_vars[j] );
- sf.d_coeff[j] = a_pv_coeff;
+ sf.d_props[j].d_coeff = a_pv_prop.d_coeff;
}else{
- sf.d_coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[j], a_pv_coeff ) );
+ sf.d_props[j].d_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_props[j].d_coeff, a_pv_prop.d_coeff ) );
}
}
if( sf.d_subs[j]!=prev_subs[j] ){
}
if( success ){
Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl;
- sf.push_back( pv, n, pv_coeff, bt );
+ sf.push_back( pv, n, pv_prop );
Node prev_theta = sf.d_theta;
Node new_theta = sf.d_theta;
- if( !pv_coeff.isNull() ){
+ if( !pv_prop.d_coeff.isNull() ){
if( new_theta.isNull() ){
- new_theta = pv_coeff;
+ new_theta = pv_prop.d_coeff;
}else{
- new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, pv_coeff );
+ new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, pv_prop.d_coeff );
new_theta = Rewriter::rewrite( new_theta );
}
}
sf.d_theta = prev_theta;
if( !success ){
Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl;
- sf.pop_back( pv, n, pv_coeff, bt );
+ sf.pop_back( pv, n, pv_prop );
}
}
if( success ){
for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){
sf.d_subs[it->first] = it->second;
}
- for( std::map< int, Node >::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){
- sf.d_coeff[it->first] = it->second;
+ for( std::map< int, TermProperties >::iterator it = prev_prop.begin(); it != prev_prop.end(); it++ ){
+ sf.d_props[it->first] = it->second;
}
for( unsigned i=0; i<new_has_coeff.size(); i++ ){
sf.d_has_coeff.pop_back();
return ret;
}
-Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff,
- std::vector< Node >& vars, Node& pv_coeff, bool try_coeff ) {
+Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< TermProperties >& prop, std::vector< Node >& has_coeff,
+ std::vector< Node >& vars, TermProperties& pv_prop, bool try_coeff ) {
Assert( d_prog_var.find( n )!=d_prog_var.end() );
Assert( n==Rewriter::rewrite( n ) );
bool req_coeff = false;
std::vector< Node > nvars;
std::vector< Node > nsubs;
for( unsigned i=0; i<vars.size(); i++ ){
- if( !coeff[i].isNull() ){
+ if( !prop[i].d_coeff.isNull() ){
Assert( vars[i].getType().isInteger() );
- Assert( coeff[i].isConst() );
- Node nn =NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/coeff[i].getConst<Rational>() ) );
+ Assert( prop[i].d_coeff.isConst() );
+ Node nn =NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/prop[i].d_coeff.getConst<Rational>() ) );
nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn );
nn = Rewriter::rewrite( nn );
nsubs.push_back( nn );
std::vector< Node >::iterator its = std::find( vars.begin(), vars.end(), it->first );
if( its!=vars.end() ){
int index = its-vars.begin();
- if( coeff[index].isNull() ){
+ if( prop[index].d_coeff.isNull() ){
//apply substitution
msum_term[it->first] = subs[index];
}else{
//apply substitution, multiply to ensure no divisibility conflict
msum_term[it->first] = subs[index];
//relative coefficient
- msum_coeff[it->first] = coeff[index];
- if( pv_coeff.isNull() ){
- pv_coeff = coeff[index];
+ msum_coeff[it->first] = prop[index].d_coeff;
+ if( pv_prop.d_coeff.isNull() ){
+ pv_prop.d_coeff = prop[index].d_coeff;
}else{
- pv_coeff = NodeManager::currentNM()->mkNode( MULT, pv_coeff, coeff[index] );
+ pv_prop.d_coeff = NodeManager::currentNM()->mkNode( MULT, pv_prop.d_coeff, prop[index].d_coeff );
}
}
}else{
}
}
//make sum with normalized coefficient
- if( !pv_coeff.isNull() ){
- pv_coeff = Rewriter::rewrite( pv_coeff );
- Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_coeff << std::endl;
+ if( !pv_prop.d_coeff.isNull() ){
+ pv_prop.d_coeff = Rewriter::rewrite( pv_prop.d_coeff );
+ Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_prop.d_coeff << std::endl;
std::vector< Node > children;
for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
Node c_coeff;
if( !msum_coeff[it->first].isNull() ){
- c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_coeff.getConst<Rational>() / msum_coeff[it->first].getConst<Rational>() ) );
+ c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_prop.d_coeff.getConst<Rational>() / msum_coeff[it->first].getConst<Rational>() ) );
}else{
- c_coeff = pv_coeff;
+ c_coeff = pv_prop.d_coeff;
}
if( !it->second.isNull() ){
c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second );
nret = Rewriter::rewrite( nret );
//ensure that nret does not contain vars
if( !TermDb::containsTerms( nret, vars ) ){
- //result is ( nret / pv_coeff )
+ //result is ( nret / pv_prop.d_coeff )
return nret;
}else{
Trace("cegqi-si-apply-subs-debug") << "Failed, since result " << nret << " contains free variable." << std::endl;
}
-bool Instantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) {
- return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort );
+bool Instantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ) {
+ pv_prop.d_type = 0;
+ return ci->doAddInstantiationInc( pv, n, pv_prop, sf, effort );
}
class Instantiator;
-
-//TODO: refactor pv_coeff to pv_prop throughout
-//generic class that stores properties for a variable to solve for in CEGQI
+//stores properties for a variable to solve for in CEGQI
+// For LIA, this includes the coefficient of the variable, and the bound type for the variable
class TermProperties {
public:
- TermProperties() : d_type(-1) {}
+ TermProperties() : d_type(0) {}
+ // type of property for a term
+ // for arithmetic this corresponds to bound type (0:equal, 1:upper bound, -1:lower bound)
int d_type;
// for arithmetic
Node d_coeff;
+ // get cache node
+ // we consider terms + TermProperties that are unique up to their cache node (see doAddInstantiationInc)
+ Node getCacheNode() { return d_coeff; }
};
//solved form, involves substitution with coefficients
public:
std::vector< Node > d_vars;
std::vector< Node > d_subs;
- //TODO: refactor below coeff -> prop;
- std::vector< Node > d_coeff;
- std::vector< int > d_btyp;
- //std::vector< TermProperties > d_props;
+ std::vector< TermProperties > d_props;
std::vector< Node > d_has_coeff;
- //std::vector< Node > d_has_prop;
Node d_theta;
void copy( SolvedForm& sf ){
d_vars.insert( d_vars.end(), sf.d_vars.begin(), sf.d_vars.end() );
d_subs.insert( d_subs.end(), sf.d_subs.begin(), sf.d_subs.end() );
- d_coeff.insert( d_coeff.end(), sf.d_coeff.begin(), sf.d_coeff.end() );
- d_btyp.insert( d_btyp.end(), sf.d_btyp.begin(), sf.d_btyp.end() );
+ d_props.insert( d_props.end(), sf.d_props.begin(), sf.d_props.end() );
d_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() );
d_theta = sf.d_theta;
}
- void push_back( Node pv, Node n, Node pv_coeff, int bt ){
+ void push_back( Node pv, Node n, TermProperties& pv_prop ){
d_vars.push_back( pv );
d_subs.push_back( n );
- d_coeff.push_back( pv_coeff );
- d_btyp.push_back( bt );
- if( !pv_coeff.isNull() ){
+ d_props.push_back( pv_prop );
+ if( !pv_prop.d_coeff.isNull() ){
d_has_coeff.push_back( pv );
}
}
- void pop_back( Node pv, Node n, Node pv_coeff, int bt ){
+ void pop_back( Node pv, Node n, TermProperties& pv_prop ){
d_vars.pop_back();
d_subs.pop_back();
- d_coeff.pop_back();
- d_btyp.pop_back();
- if( !pv_coeff.isNull() ){
+ d_props.pop_back();
+ if( !pv_prop.d_coeff.isNull() ){
d_has_coeff.pop_back();
}
}
public:
void pushStackVariable( Node v );
void popStackVariable();
- bool doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int bt, SolvedForm& sf, unsigned effort );
+ bool doAddInstantiationInc( Node pv, Node n, TermProperties& pv_prop, SolvedForm& sf, unsigned effort );
Node getModelValue( Node n );
// TODO: move to solved form?
- Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, Node& pv_coeff, bool try_coeff = true ) {
- return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, sf.d_vars, pv_coeff, try_coeff );
+ Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, TermProperties& pv_prop, bool try_coeff = true ) {
+ return applySubstitution( tn, n, sf.d_subs, sf.d_props, sf.d_has_coeff, sf.d_vars, pv_prop, try_coeff );
}
- Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff,
- std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true );
+ Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< TermProperties >& prop, std::vector< Node >& has_coeff,
+ std::vector< Node >& vars, TermProperties& pv_prop, bool try_coeff = true );
public:
unsigned getNumCEAtoms() { return d_ce_atoms.size(); }
Node getCEAtom( unsigned i ) { return d_ce_atoms[i]; }
virtual ~Instantiator(){}
virtual void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {}
- //called when pv_coeff * pv = n, and n is eligible for instantiation
- virtual bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort );
+ //called when pv_prop.d_coeff * pv = n, and n is eligible for instantiation
+ virtual bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort );
//eqc is the equivalence class of pv
virtual bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { return false; }
virtual bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
- //term_coeffs.size() = terms.size() = 2, called when term_coeff[0] * terms[0] = term_coeff[1] * terms[1], terms are eligible, and at least one of these terms contains pv
+ //term_props.size() = terms.size() = 2
+ // called when terms[0] = terms[1], terms are eligible, and at least one of these terms contains pv
// returns true if an instantiation was successfully added via a recursive call
- virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { return false; }
+ virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) { return false; }
virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { return false; }
std::string identify() const { return "ModelValue"; }
};
-
}
}
}
}
}
-bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) {
+bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) {
Node eq_lhs = terms[0];
Node eq_rhs = terms[1];
- Node lhs_coeff = term_coeffs[0];
- Node rhs_coeff = term_coeffs[1];
+ Node lhs_coeff = term_props[0].d_coeff;
+ Node rhs_coeff = term_props[1].d_coeff;
//make the same coefficient
if( rhs_coeff!=lhs_coeff ){
if( !rhs_coeff.isNull() ){
Node eq = eq_lhs.eqNode( eq_rhs );
eq = Rewriter::rewrite( eq );
Node val;
- Node veq_c;
+ TermProperties pv_prop;
Node vts_coeff_inf;
Node vts_coeff_delta;
//isolate pv in the equality
- int ires = solve_arith( ci, pv, eq, veq_c, val, vts_coeff_inf, vts_coeff_delta );
+ int ires = solve_arith( ci, pv, eq, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta );
if( ires!=0 ){
- if( ci->doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){
+ pv_prop.d_type = 0;
+ if( ci->doAddInstantiationInc( pv, val, pv_prop, sf, effort ) ){
return true;
}
}
//must be an eligible term
if( ci->isEligible( atom_lhs ) ){
//apply substitution to LHS of atom
- Node atom_lhs_coeff;
- atom_lhs = ci->applySubstitution( d_type, atom_lhs, sf, atom_lhs_coeff );
+ TermProperties atom_lhs_prop;
+ atom_lhs = ci->applySubstitution( d_type, atom_lhs, sf, atom_lhs_prop );
if( !atom_lhs.isNull() ){
- if( !atom_lhs_coeff.isNull() ){
- atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) );
+ if( !atom_lhs_prop.d_coeff.isNull() ){
+ atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_prop.d_coeff, atom_rhs ) );
}
}
//if it contains pv, not infinity
Node vts_coeff_inf;
Node vts_coeff_delta;
Node val;
- Node veq_c;
+ TermProperties pv_prop;
//isolate pv in the inequality
- int ires = solve_arith( ci, pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta );
+ int ires = solve_arith( ci, pv, satom, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta );
if( ires!=0 ){
//disequalities are either strict upper or lower bounds
unsigned rmax = ( atom.getKind()==GEQ || options::cbqiModel() ) ? 1 : 2;
}else{
Node rhs_value = ci->getModelValue( val );
Node lhs_value = pv_value;
- if( !veq_c.isNull() ){
- lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c );
+ if( !pv_prop.d_coeff.isNull() ){
+ lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, pv_prop.d_coeff );
lhs_value = Rewriter::rewrite( lhs_value );
}
Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl;
}
}
Trace("cbqi-bound-inf") << "From " << lit << ", got : ";
- if( !veq_c.isNull() ){
- Trace("cbqi-bound-inf") << veq_c << " * ";
+ if( !pv_prop.d_coeff.isNull() ){
+ Trace("cbqi-bound-inf") << pv_prop.d_coeff << " * ";
}
Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl;
//take into account delta
//just store bounds, will choose based on tighest bound
unsigned index = uires>0 ? 0 : 1;
d_mbp_bounds[index].push_back( uval );
- d_mbp_coeff[index].push_back( veq_c );
- Trace("cbqi-inst-debug") << "Store bound " << index << " " << uval << " " << veq_c << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl;
+ d_mbp_coeff[index].push_back( pv_prop.d_coeff );
+ Trace("cbqi-inst-debug") << "Store bound " << index << " " << uval << " " << pv_prop.d_coeff << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl;
for( unsigned t=0; t<2; t++ ){
d_mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta );
}
d_mbp_lit[index].push_back( lit );
}else{
//try this bound
- if( ci->doAddInstantiationInc( pv, uval, veq_c, uires>0 ? 1 : -1, sf, effort ) ){
+ pv_prop.d_type = uires>0 ? 1 : -1;
+ if( ci->doAddInstantiationInc( pv, uval, pv_prop, sf, effort ) ){
return true;
}
}
val = NodeManager::currentNM()->mkNode( UMINUS, val );
val = Rewriter::rewrite( val );
}
- if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){
+ TermProperties pv_prop_no_bound;
+ if( ci->doAddInstantiationInc( pv, val, pv_prop_no_bound, sf, effort ) ){
return true;
}
}
val = getModelBasedProjectionValue( ci, pv, val, rr==0, d_mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.d_theta,
d_mbp_vts_coeff[rr][0][best], d_mbp_vts_coeff[rr][1][best] );
if( !val.isNull() ){
- if( ci->doAddInstantiationInc( pv, val, d_mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, effort ) ){
+ TermProperties pv_prop_bound;
+ pv_prop_bound.d_coeff = d_mbp_coeff[rr][best];
+ pv_prop_bound.d_type = rr==0 ? 1 : -1;
+ if( ci->doAddInstantiationInc( pv, val, pv_prop_bound, sf, effort ) ){
return true;
}
}
//if not using infinity, use model value of zero
if( !use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty() ){
Node val = zero;
- Node c; //null (one) coefficient
- val = getModelBasedProjectionValue( ci, pv, val, true, c, pv_value, zero, sf.d_theta, Node::null(), Node::null() );
+ TermProperties pv_prop_zero;
+ val = getModelBasedProjectionValue( ci, pv, val, true, pv_prop_zero.d_coeff, pv_value, zero, sf.d_theta, Node::null(), Node::null() );
if( !val.isNull() ){
- if( ci->doAddInstantiationInc( pv, val, c, 0, sf, effort ) ){
+ if( ci->doAddInstantiationInc( pv, val, pv_prop_zero, sf, effort ) ){
return true;
}
}
}
Trace("cbqi-bound") << "Midpoint value : " << val << std::endl;
if( !val.isNull() ){
- if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){
+ TermProperties pv_prop_midpoint;
+ if( ci->doAddInstantiationInc( pv, val, pv_prop_midpoint, sf, effort ) ){
return true;
}
}
Node val = getModelBasedProjectionValue( ci, pv, d_mbp_bounds[rr][j], rr==0, d_mbp_coeff[rr][j], pv_value, t_values[rr][j], sf.d_theta,
d_mbp_vts_coeff[rr][0][j], d_mbp_vts_coeff[rr][1][j] );
if( !val.isNull() ){
- if( ci->doAddInstantiationInc( pv, val, d_mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, effort ) ){
+ TermProperties pv_prop_nopt_bound;
+ pv_prop_nopt_bound.d_coeff = d_mbp_coeff[rr][j];
+ pv_prop_nopt_bound.d_type = rr==0 ? 1 : -1;
+ if( ci->doAddInstantiationInc( pv, val, pv_prop_nopt_bound, sf, effort ) ){
return true;
}
}
Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), pv )!=sf.d_has_coeff.end() );
Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )!=sf.d_vars.end() );
unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )-sf.d_vars.begin();
- Assert( !sf.d_coeff[index].isNull() );
- Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << sf.d_vars[index] << " = " << sf.d_subs[index] << std::endl;
+ Assert( !sf.d_props[index].d_coeff.isNull() );
+ Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_props[index].d_coeff << " * ";
+ Trace("cbqi-inst-debug") << sf.d_vars[index] << " = " << sf.d_subs[index] << std::endl;
Assert( sf.d_vars[index].getType().isInteger() );
//must ensure that divisibility constraints are met
//solve updated rewritten equality for vars[index], if coefficient is one, then we are successful
- Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], sf.d_vars[index] );
+ Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_props[index].d_coeff, sf.d_vars[index] );
Node eq_rhs = sf.d_subs[index];
Node eq = eq_lhs.eqNode( eq_rhs );
eq = Rewriter::rewrite( eq );
sf.d_subs[index] = veq[1];
if( !veq_c.isNull() ){
sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c );
- Trace("cbqi-inst-debug") << "...bound type is : " << sf.d_btyp[index] << std::endl;
+ Trace("cbqi-inst-debug") << "...bound type is : " << sf.d_props[index].d_type << std::endl;
//intger division rounding up if from a lower bound
- if( sf.d_btyp[index]==1 && options::cbqiRoundUpLowerLia() ){
+ if( sf.d_props[index].d_type==1 && options::cbqiRoundUpLowerLia() ){
sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index],
NodeManager::currentNM()->mkNode( ITE,
NodeManager::currentNM()->mkNode( EQUAL,
children.push_back( c );
}
Node val = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
- if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){
+ TermProperties pv_prop_dt;
+ if( ci->doAddInstantiationInc( pv, val, pv_prop_dt, sf, effort ) ){
return true;
}else{
//cleanup
return false;
}
-bool DtInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) {
+bool DtInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) {
Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] );
if( !val.isNull() ){
- Node veq_c;
- if( ci->doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){
+ TermProperties pv_prop;
+ if( ci->doAddInstantiationInc( pv, val, pv_prop, sf, effort ) ){
return true;
}
}
d_equal_terms.clear();
}
-bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) {
+bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ) {
if( options::quantEprMatching() ){
- Assert( pv_coeff.isNull() );
+ Assert( pv_prop.d_coeff.isNull() );
d_equal_terms.push_back( n );
return false;
}else{
- return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort );
+ pv_prop.d_type = 0;
+ return ci->doAddInstantiationInc( pv, n, pv_prop, sf, effort );
}
}
}
//sort by match score
std::sort( d_equal_terms.begin(), d_equal_terms.end(), setm );
- Node pv_coeff;
+ TermProperties pv_prop;
+ pv_prop.d_type = 0;
for( unsigned i=0; i<d_equal_terms.size(); i++ ){
- if( ci->doAddInstantiationInc( pv, d_equal_terms[i], pv_coeff, 0, sf, effort ) ){
+ if( ci->doAddInstantiationInc( pv, d_equal_terms[i], pv_prop, sf, effort ) ){
return true;
}
}
if( d_inelig.find( atom[1-t] )==d_inelig.end() ){
//only ground terms TODO: more
if( d_prog_var[atom[1-t]].empty() ){
- Node veq_c;
+ TermProperties pv_prop;
Node uval;
if( ( !pol && atom.getKind()==BITVECTOR_ULT ) || ( pol && atom.getKind()==BITVECTOR_ULE ) ){
uval = atom[1-t];
uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t],
bv::utils::mkConst(pvtn.getConst<BitVectorSize>(), 1) );
}
- if( doAddInstantiationInc( pv, uval, veq_c, 0, sf, effort ) ){
+ if( doAddInstantiationInc( pv, uval, pv_prop, sf, effort ) ){
return true;
}
}
*/
}
-bool BvInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) {
+bool BvInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) {
//processLiteral( ci, sf, pv, terms[0].eqNode( terms[1] ), effort );
return false;
}
virtual ~ArithInstantiator(){}
void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
- bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort );
+ bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort );
bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort );
bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
- bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort );
+ bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort );
std::string identify() const { return "Dt"; }
};
EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
virtual ~EprInstantiator(){}
void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
- bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort );
+ bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort );
bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort );
std::string identify() const { return "Epr"; }
};
virtual ~BvInstantiator(){}
void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
- bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort );
+ bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort );
bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
projects / cvc5.git / commitdiff