while( !d_eq.isFinished() ){
Node n = (*d_eq);
++d_eq;
- if( n.getType().isSubtypeOf( d_match_pattern[0].getType() ) ){
+ if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){
//an equivalence class with the same type as the pattern, return reflexive equality
return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
}
while( !d_eq.isFinished() ){
TNode n = (*d_eq);
++d_eq;
- if( n.getType().isSubtypeOf( d_match_pattern_type ) ){
+ if( n.getType().isComparableTo( d_match_pattern_type ) ){
TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n );
if( !nh.isNull() ){
if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
//[3] directly look at assertions
Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl;
- Node vts_sym[2];
- vts_sym[0] = d_qe->getTermDatabase()->getVtsInfinity( pvtn, false, false );
- vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta( false, false );
+ d_vts_sym[0] = d_qe->getTermDatabase()->getVtsInfinity( pvtn, false, false );
+ d_vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta( false, false );
std::vector< Node > mbp_bounds[2];
std::vector< Node > mbp_coeff[2];
std::vector< Node > mbp_vts_coeff[2][2];
std::vector< Node > mbp_lit[2];
+ //std::vector< MbpBounds > mbp_bounds[2];
unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
for( unsigned r=0; r<rmax; r++ ){
TheoryId tid = r==0 ? Theory::theoryOf( pv ) : Theory::theoryOf( pv.getType() );
//if( !d_qe->getTermDatabase()->containsVtsInfinity( atom_lhs ) ){
Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl;
Trace("cbqi-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl;
- std::map< Node, Node > msum;
- if( QuantArith::getMonomialSumLit( satom, msum ) ){
- if( Trace.isOn("cbqi-inst-debug") ){
- Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl;
- QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
- }
- //get the coefficient of infinity and remove it from msum
- Node vts_coeff[2];
- for( unsigned t=0; t<2; t++ ){
- if( !vts_sym[t].isNull() ){
- std::map< Node, Node >::iterator itminf = msum.find( vts_sym[t] );
- if( itminf!=msum.end() ){
- vts_coeff[t] = itminf->second;
- if( vts_coeff[t].isNull() ){
- vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) );
- }
- //negate if coefficient on variable is positive
- std::map< Node, Node >::iterator itv = msum.find( pv );
- if( itv!=msum.end() ){
- //multiply by the coefficient we will isolate for
- if( itv->second.isNull() ){
- vts_coeff[t] = QuantArith::negate(vts_coeff[t]);
- }else{
- if( !pvtn.isInteger() ){
- vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst<Rational>() ), vts_coeff[t] );
- vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] );
- }else if( itv->second.getConst<Rational>().sgn()==1 ){
- vts_coeff[t] = QuantArith::negate(vts_coeff[t]);
- }
- }
- }
- Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl;
- msum.erase( vts_sym[t] );
- }
- }
- }
-
- Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl;
- Node vatom;
- //isolate pv in the inequality
- int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true );
- if( ires!=0 ){
- Trace("cbqi-inst-debug") << "...isolated atom " << vatom << "." << std::endl;
- Node val = vatom[ ires==1 ? 1 : 0 ];
- Node pvm = vatom[ ires==1 ? 0 : 1 ];
- //get monomial
- Node veq_c;
- if( pvm!=pv ){
- Node veq_v;
- if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){
- Assert( veq_v==pv );
- }
- }
-
- //disequalities are either strict upper or lower bounds
- unsigned rmax = ( atom.getKind()==GEQ && options::cbqiModel() ) ? 1 : 2;
- for( unsigned r=0; r<rmax; r++ ){
- int uires = ires;
- Node uval = val;
- if( atom.getKind()==GEQ ){
- //push negation downwards
- if( !pol ){
- uires = -ires;
- if( pvtn.isInteger() ){
- uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
- uval = Rewriter::rewrite( uval );
- }else{
- Assert( pvtn.isReal() );
- //now is strict inequality
- uires = uires*2;
- }
- }
- }else{
- bool is_upper = ( r==0 );
- if( options::cbqiModel() ){
- // disequality is a disjunction : only consider the bound in the direction of the model
- //first check if there is an infinity...
- if( !vts_coeff[0].isNull() ){
- //coefficient or val won't make a difference, just compare with zero
- Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff[0] << std::endl;
- Assert( vts_coeff[0].isConst() );
- is_upper = ( vts_coeff[0].getConst<Rational>().sgn()==1 );
- }else{
- Node rhs_value = getModelValue( val );
- Node lhs_value = pv_value;
- if( !veq_c.isNull() ){
- lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c );
- lhs_value = Rewriter::rewrite( lhs_value );
- }
- Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl;
- Assert( lhs_value!=rhs_value );
- Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
- cmp = Rewriter::rewrite( cmp );
- Assert( cmp.isConst() );
- is_upper = ( cmp!=d_true );
- }
- }
- Assert( atom.getKind()==EQUAL && !pol );
+ Node vts_coeff_inf;
+ Node vts_coeff_delta;
+ Node val;
+ Node veq_c;
+ //isolate pv in the inequality
+ int ires = isolate( pv, satom, veq_c, 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;
+ for( unsigned r=0; r<rmax; r++ ){
+ int uires = ires;
+ Node uval = val;
+ if( atom.getKind()==GEQ ){
+ //push negation downwards
+ if( !pol ){
+ uires = -ires;
if( pvtn.isInteger() ){
- uires = is_upper ? -1 : 1;
uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
uval = Rewriter::rewrite( uval );
}else{
Assert( pvtn.isReal() );
- uires = is_upper ? -2 : 2;
+ //now is strict inequality
+ uires = uires*2;
}
}
- Trace("cbqi-bound-inf") << "From " << lit << ", got : ";
- if( !veq_c.isNull() ){
- Trace("cbqi-bound-inf") << veq_c << " * ";
- }
- Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl;
- //take into account delta
- if( d_use_vts_delta && ( uires==2 || uires==-2 ) ){
- if( options::cbqiModel() ){
- Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) );
- if( vts_coeff[1].isNull() ){
- vts_coeff[1] = delta_coeff;
- }else{
- vts_coeff[1] = NodeManager::currentNM()->mkNode( PLUS, vts_coeff[1], delta_coeff );
- vts_coeff[1] = Rewriter::rewrite( vts_coeff[1] );
- }
+ }else{
+ bool is_upper = ( r==0 );
+ if( options::cbqiModel() ){
+ // disequality is a disjunction : only consider the bound in the direction of the model
+ //first check if there is an infinity...
+ if( !vts_coeff_inf.isNull() ){
+ //coefficient or val won't make a difference, just compare with zero
+ Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl;
+ Assert( vts_coeff_inf.isConst() );
+ is_upper = ( vts_coeff_inf.getConst<Rational>().sgn()==1 );
}else{
- Node delta = d_qe->getTermDatabase()->getVtsDelta();
- uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta );
- uval = Rewriter::rewrite( uval );
+ Node rhs_value = getModelValue( val );
+ Node lhs_value = pv_value;
+ if( !veq_c.isNull() ){
+ lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c );
+ lhs_value = Rewriter::rewrite( lhs_value );
+ }
+ Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl;
+ Assert( lhs_value!=rhs_value );
+ Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
+ cmp = Rewriter::rewrite( cmp );
+ Assert( cmp.isConst() );
+ is_upper = ( cmp!=d_true );
}
}
+ Assert( atom.getKind()==EQUAL && !pol );
+ if( pvtn.isInteger() ){
+ uires = is_upper ? -1 : 1;
+ uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
+ uval = Rewriter::rewrite( uval );
+ }else{
+ Assert( pvtn.isReal() );
+ uires = is_upper ? -2 : 2;
+ }
+ }
+ Trace("cbqi-bound-inf") << "From " << lit << ", got : ";
+ if( !veq_c.isNull() ){
+ Trace("cbqi-bound-inf") << veq_c << " * ";
+ }
+ Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl;
+ //take into account delta
+ if( d_use_vts_delta && ( uires==2 || uires==-2 ) ){
if( options::cbqiModel() ){
- //just store bounds, will choose based on tighest bound
- if( pvtn.isInteger() && !veq_c.isNull() && !veq_c.getType().isInteger() ){
- Trace("cbqi-bound2") << "Non-integer coefficient : " << veq_c << " for " << pv << std::endl;
- Assert( veq_c.isConst() );
- //multiply everything by denominator of coefficient
- Rational r = veq_c.getConst<Rational>();
- Node den = NodeManager::currentNM()->mkConst( Rational(r.getDenominator()) );
- uval = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, den, uval ) );
- veq_c = NodeManager::currentNM()->mkConst( Rational(r.getNumerator()) );
- for( unsigned t=0; t<2; t++ ){
- if( !vts_coeff[t].isNull() ){
- vts_coeff[t] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, den, vts_coeff[t] ) );
- }
- }
- }
- unsigned index = uires>0 ? 0 : 1;
- mbp_bounds[index].push_back( uval );
- mbp_coeff[index].push_back( veq_c );
- for( unsigned t=0; t<2; t++ ){
- mbp_vts_coeff[index][t].push_back( vts_coeff[t] );
+ Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) );
+ if( vts_coeff_delta.isNull() ){
+ vts_coeff_delta = delta_coeff;
+ }else{
+ vts_coeff_delta = NodeManager::currentNM()->mkNode( PLUS, vts_coeff_delta, delta_coeff );
+ vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta );
}
- mbp_lit[index].push_back( lit );
}else{
- //try this bound
- if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
- subs_proc[uval][veq_c] = true;
- if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
- return true;
- }
+ Node delta = d_qe->getTermDatabase()->getVtsDelta();
+ uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta );
+ uval = Rewriter::rewrite( uval );
+ }
+ }
+ if( options::cbqiModel() ){
+ //just store bounds, will choose based on tighest bound
+ unsigned index = uires>0 ? 0 : 1;
+ mbp_bounds[index].push_back( uval );
+ mbp_coeff[index].push_back( veq_c );
+ for( unsigned t=0; t<2; t++ ){
+ mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta );
+ }
+ mbp_lit[index].push_back( lit );
+ }else{
+ //try this bound
+ if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
+ subs_proc[uval][veq_c] = true;
+ if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ return true;
}
}
}
best_used[rr] = (unsigned)best;
Node val = mbp_bounds[rr][best];
val = getModelBasedProjectionValue( pv, val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta,
- mbp_vts_coeff[rr][0][best], vts_sym[0], mbp_vts_coeff[rr][1][best], vts_sym[1] );
+ mbp_vts_coeff[rr][0][best], mbp_vts_coeff[rr][1][best] );
if( !val.isNull() ){
if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){
subs_proc[val][mbp_coeff[rr][best]] = true;
if( !use_inf && mbp_bounds[0].empty() && mbp_bounds[1].empty() ){
Node val = d_zero;
Node c; //null (one) coefficient
- val = getModelBasedProjectionValue( pv, val, true, c, pv_value, d_zero, theta, Node::null(), vts_sym[0], Node::null(), vts_sym[1] );
+ val = getModelBasedProjectionValue( pv, val, true, c, pv_value, d_zero, theta, Node::null(), Node::null() );
if( !val.isNull() ){
if( subs_proc[val].find( c )==subs_proc[val].end() ){
subs_proc[val][c] = true;
for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){
if( j!=best_used[rr] ){
Node val = getModelBasedProjectionValue( pv, mbp_bounds[rr][j], rr==0, mbp_coeff[rr][j], pv_value, t_values[rr][j], theta,
- mbp_vts_coeff[rr][0][j], vts_sym[0], mbp_vts_coeff[rr][1][j], vts_sym[1] );
+ mbp_vts_coeff[rr][0][j], mbp_vts_coeff[rr][1][j] );
if( !val.isNull() ){
if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){
subs_proc[val][mbp_coeff[rr][j]] = true;
subs.push_back( n );
}
}
+ if( !d_var_order_index.empty() ){
+ std::vector< Node > subs_orig;
+ subs_orig.insert( subs_orig.end(), subs.begin(), subs.end() );
+ subs.clear();
+ for( unsigned i=0; i<subs_orig.size(); i++ ){
+ subs.push_back( subs_orig[d_var_order_index[i]] );
+ }
+ }
bool ret = d_out->addInstantiation( subs );
#ifdef MBP_STRICT_ASSERTIONS
Assert( ret );
}
}
-Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta,
- Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ) {
+Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) {
+ /*
if( e.getType().isInteger() && !t.getType().isInteger() ){
//TODO : round up/down this bound?
return Node::null();
}
+ */
Node val = t;
Trace("cbqi-bound2") << "Value : " << val << std::endl;
//add rho value
}
if( !new_theta.isNull() && e.getType().isInteger() ){
Node rho;
+ //if( !mt.getType().isInteger() ){
+ //round up/down
+ //mt = NodeManager::currentNM()->mkNode(
+ //}
if( isLower ){
rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt );
}else{
Trace("cbqi-bound2") << "(after rho) : " << val << std::endl;
}
if( !inf_coeff.isNull() ){
- Assert( !vts_inf.isNull() );
- val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, vts_inf ) );
+ Assert( !d_vts_sym[0].isNull() );
+ val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, d_vts_sym[0] ) );
val = Rewriter::rewrite( val );
}
if( !delta_coeff.isNull() ){
//create delta here if necessary
- if( vts_delta.isNull() ){
- vts_delta = d_qe->getTermDatabase()->getVtsDelta();
+ if( d_vts_sym[1].isNull() ){
+ d_vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta();
}
- val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, vts_delta ) );
+ val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, d_vts_sym[1] ) );
val = Rewriter::rewrite( val );
}
return val;
}
}
+struct sortCegVarOrder {
+ bool operator() (Node i, Node j) {
+ TypeNode it = i.getType();
+ TypeNode jt = j.getType();
+ return ( it!=jt && jt.isSubtypeOf( it ) ) || ( it==jt && i<j );
+ }
+};
+
+
void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
Assert( d_vars.empty() );
d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() );
+
+ //determine variable order: must do Reals before Ints
+ if( !d_vars.empty() ){
+ TypeNode tn0 = d_vars[0].getType();
+ bool doSort = false;
+ std::map< Node, unsigned > voo;
+ for( unsigned i=0; i<d_vars.size(); i++ ){
+ voo[d_vars[i]] = i;
+ d_var_order_index.push_back( 0 );
+ if( d_vars[i].getType()!=tn0 ){
+ doSort = true;
+ }
+ }
+ if( doSort ){
+ Trace("cbqi-debug") << "Sort variables based on ordering." << std::endl;
+ sortCegVarOrder scvo;
+ std::sort( d_vars.begin(), d_vars.end(), scvo );
+ Trace("cbqi-debug") << "Consider variables in this order : " << std::endl;
+ for( unsigned i=0; i<d_vars.size(); i++ ){
+ d_var_order_index[voo[d_vars[i]]] = i;
+ Trace("cbqi-debug") << " " << d_vars[i] << " : " << d_vars[i].getType() << ", index was : " << voo[d_vars[i]] << std::endl;
+ }
+ Trace("cbqi-debug") << std::endl;
+ }else{
+ d_var_order_index.clear();
+ }
+ }
+
+ //remove ITEs
IteSkolemMap iteSkolemMap;
d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
Assert( d_aux_vars.empty() );
collectCeAtoms( lems[i], visited );
}
}
+
+//this isolates the monomial sum into solved form (pv k t), ensures t is Int if pv is Int, and t does not contain vts symbols
+int CegInstantiator::isolate( Node pv, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta ) {
+ int ires = 0;
+ Trace("cbqi-inst-debug") << "isolate for " << pv << " in " << atom << std::endl;
+ std::map< Node, Node > msum;
+ if( QuantArith::getMonomialSumLit( atom, msum ) ){
+ Trace("cbqi-inst-debug") << "got monomial sum: " << std::endl;
+ if( Trace.isOn("cbqi-inst-debug") ){
+ QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
+ }
+ TypeNode pvtn = pv.getType();
+ //remove vts symbols from polynomial
+ Node vts_coeff[2];
+ for( unsigned t=0; t<2; t++ ){
+ if( !d_vts_sym[t].isNull() ){
+ std::map< Node, Node >::iterator itminf = msum.find( d_vts_sym[t] );
+ if( itminf!=msum.end() ){
+ vts_coeff[t] = itminf->second;
+ if( vts_coeff[t].isNull() ){
+ vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) );
+ }
+ //negate if coefficient on variable is positive
+ std::map< Node, Node >::iterator itv = msum.find( pv );
+ if( itv!=msum.end() ){
+ //multiply by the coefficient we will isolate for
+ if( itv->second.isNull() ){
+ vts_coeff[t] = QuantArith::negate(vts_coeff[t]);
+ }else{
+ if( !pvtn.isInteger() ){
+ vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst<Rational>() ), vts_coeff[t] );
+ vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] );
+ }else if( itv->second.getConst<Rational>().sgn()==1 ){
+ vts_coeff[t] = QuantArith::negate(vts_coeff[t]);
+ }
+ }
+ }
+ Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl;
+ msum.erase( d_vts_sym[t] );
+ }
+ }
+ }
+
+ ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() );
+ if( ires!=0 ){
+ Node realPart;
+ Trace("cbqi-inst-debug") << "Isolate : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
+ if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){
+ //redo, split integer/non-integer parts
+ bool useCoeff = false;
+ Integer coeff = d_one.getConst<Rational>().getNumerator();
+ for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+ if( it->first.isNull() || it->first.getType().isInteger() ){
+ if( !it->second.isNull() ){
+ coeff = coeff.lcm( it->second.getConst<Rational>().getDenominator() );
+ useCoeff = true;
+ }
+ }
+ }
+ //multiply everything by this coefficient
+ Node rcoeff = NodeManager::currentNM()->mkConst( Rational( coeff ) );
+ std::vector< Node > real_part;
+ for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+ if( useCoeff ){
+ if( it->second.isNull() ){
+ msum[it->first] = rcoeff;
+ }else{
+ msum[it->first] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, it->second, rcoeff ) );
+ }
+ }
+ if( !it->first.isNull() && !it->first.getType().isInteger() ){
+ real_part.push_back( msum[it->first].isNull() ? it->first : NodeManager::currentNM()->mkNode( MULT, msum[it->first], it->first ) );
+ }
+ }
+ for( unsigned t=0; t<2; t++ ){
+ if( !vts_coeff[t].isNull() ){
+ vts_coeff[t] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[t] ) );
+ }
+ }
+ realPart = real_part.empty() ? d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) );
+ Assert( d_out->isEligibleForInstantiation( realPart ) );
+ //re-isolate
+ ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() );
+ Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
+ Trace("cbqi-inst-debug") << " real part : " << realPart << std::endl;
+ if( ires!=0 ){
+ val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires==-1 ? PLUS : MINUS,
+ NodeManager::currentNM()->mkNode( ires==-1 ? MINUS : PLUS, val, realPart ),
+ NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) );
+ Trace("cbqi-inst-debug") << "result : " << val << std::endl;
+ Assert( val.getType().isInteger() );
+ }
+ }
+ }
+ vts_coeff_inf = vts_coeff[0];
+ vts_coeff_delta = vts_coeff[1];
+ }
+
+ return ires;
+}
Node d_true;
bool d_use_vts_delta;
bool d_use_vts_inf;
+ Node d_vts_sym[2];
//program variable contains cache
std::map< Node, std::map< Node, bool > > d_prog_var;
std::map< Node, bool > d_inelig;
std::map< Node, std::map< Node, Node > > d_aux_eq;
//the CE variables
std::vector< Node > d_vars;
+ //index of variables reported in instantiation
+ std::vector< unsigned > d_var_order_index;
//atoms of the CE lemma
bool d_is_nested_quant;
std::vector< Node > d_ce_atoms;
}
}
};
+ /*
+ class MbpBound {
+ public:
+ Node d_bound;
+ Node d_coeff;
+ Node d_vts_coeff[2];
+ Node d_lit;
+ };
+ */
// effort=0 : do not use model value, 1: use model value, 2: one must use model value
bool addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
}
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 getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta,
- Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta );
+ Node getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff );
void processAssertions();
void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r );
//get model value
Node getModelValue( Node n );
+private:
+ int isolate( Node v, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta );
public:
CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true );
//check : add instantiations based on valuation of d_vars
t = d_cg->getNextCandidate();
Trace("matching-debug2") << "Matching candidate : " << t << std::endl;
//if t not null, try to fit it into match m
- if( !t.isNull() && t.getType().isSubtypeOf( d_match_pattern_type ) ){
+ if( !t.isNull() ){
+ Assert( t.getType().isComparableTo( d_match_pattern_type ) );
success = getMatch( f, t, m, qe );
}
}while( !success && !t.isNull() );
d_var_num[0] = var.getAttribute(InstVarNumAttribute());
}
-bool VarMatchGeneratorBooleanTerm::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) {
+bool VarMatchGeneratorBooleanTerm::getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) {
if( !d_eq_class.isNull() ){
Node s = NodeManager::currentNM()->mkConst(qe->getEqualityQuery()->areEqual( d_eq_class, d_pattern ));
d_eq_class = Node::null();
if( !m.set( qe, d_var_num[0], s ) ){
return false;
}else{
- if( continueNextMatch( f, m, qe ) ){
+ if( continueNextMatch( q, m, qe ) ){
return true;
}
}
VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) :
InstMatchGenerator(), d_var( var ), d_subs( subs ), d_rm_prev( false ){
d_var_num[0] = d_var.getAttribute(InstVarNumAttribute());
+ d_var_type = d_var.getType();
}
-bool VarMatchGeneratorTermSubs::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) {
+bool VarMatchGeneratorTermSubs::getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) {
if( !d_eq_class.isNull() ){
Trace("var-trigger-matching") << "Matching " << d_eq_class << " against " << d_var << " in " << d_subs << std::endl;
Node s = d_subs.substitute( d_var, d_eq_class );
s = Rewriter::rewrite( s );
Trace("var-trigger-matching") << "...got " << s << std::endl;
d_eq_class = Node::null();
- if( s.getType().isSubtypeOf( d_var.getType() ) ){
- d_rm_prev = m.get( d_var_num[0] ).isNull();
- if( !m.set( qe, d_var_num[0], s ) ){
- return false;
- }else{
- if( continueNextMatch( f, m, qe ) ){
- return true;
- }
- }
+ //if( s.getType().isSubtypeOf( d_var_type ) ){
+ d_rm_prev = m.get( d_var_num[0] ).isNull();
+ if( !m.set( qe, d_var_num[0], s ) ){
+ return false;
}else{
- Trace("var-trigger-matching") << "Violates type requirement." << std::endl;
+ if( continueNextMatch( q, m, qe ) ){
+ return true;
+ }
}
}
if( d_rm_prev ){
}
/** constructors */
-InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe ) :
-d_f( f ){
- Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl;
+InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) :
+d_f( q ){
+ Debug("smart-multi-trigger") << "Making smart multi-trigger for " << q << std::endl;
std::map< Node, std::vector< Node > > var_contains;
- qe->getTermDatabase()->getVarContains( f, pats, var_contains );
+ qe->getTermDatabase()->getVarContains( q, pats, var_contains );
//convert to indicies
for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: ";
for( int i=0; i<(int)pats.size(); i++ ){
Node n = pats[i];
//make the match generator
- d_children.push_back( InstMatchGenerator::mkInstMatchGenerator(f, n, qe ) );
+ d_children.push_back( InstMatchGenerator::mkInstMatchGenerator(q, n, qe ) );
//compute unique/shared variables
std::vector< int > unique_vars;
std::map< int, bool > shared_vars;
}
}
-int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
+int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){
int addedLemmas = 0;
Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl;
for( int i=0; i<(int)d_children.size(); i++ ){
Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl;
std::vector< InstMatch > newMatches;
- InstMatch m( f );
- while( d_children[i]->getNextMatch( f, m, qe ) ){
+ InstMatch m( q );
+ while( d_children[i]->getNextMatch( q, m, qe ) ){
//m.makeRepresentative( qe );
newMatches.push_back( InstMatch( &m ) );
m.clear();
}
}
-int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){
+int InstMatchGeneratorMulti::addTerm( Node q, Node t, QuantifiersEngine* qe ){
Assert( options::eagerInstQuant() );
int addedLemmas = 0;
for( int i=0; i<(int)d_children.size(); i++ ){
Node t_op = qe->getTermDatabase()->getOperator( t );
if( ((InstMatchGenerator*)d_children[i])->d_match_pattern_op==t_op ){
- InstMatch m( f );
+ InstMatch m( q );
//if it produces a match, then process it with the rest
- if( ((InstMatchGenerator*)d_children[i])->getMatch( f, t, m, qe ) ){
+ if( ((InstMatchGenerator*)d_children[i])->getMatch( q, t, m, qe ) ){
processNewMatch( qe, m, i, addedLemmas );
}
}
return addedLemmas;
}
-InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ) {
+InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat ) : d_f( q ), d_match_pattern( pat ) {
for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
if( d_match_pattern[i].getKind()==INST_CONSTANT ){
- if( !options::cbqi() || quantifiers::TermDb::getInstConstAttr(d_match_pattern[i])==f ){
+ if( !options::cbqi() || quantifiers::TermDb::getInstConstAttr(d_match_pattern[i])==q ){
d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
}else{
d_var_num[i] = -1;
d_op = qe->getTermDatabase()->getOperator( d_match_pattern );
}
-int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
- InstMatch m( f );
+int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){
+ InstMatch m( q );
m.add( baseMatch );
int addedLemmas = 0;
Node t = it->first;
Node prev = m.get( v );
//using representatives, just check if equal
- if( ( prev.isNull() || prev==t ) && t.getType().isSubtypeOf( d_match_pattern_arg_types[argIndex] ) ){
+ Assert( t.getType().isComparableTo( d_match_pattern_arg_types[argIndex] ) );
+ if( prev.isNull() || prev==t ){
m.setValue( v, t);
addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
m.setValue( v, prev);
}
}
-int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){
+int InstMatchGeneratorSimple::addTerm( Node q, Node t, QuantifiersEngine* qe ){
Assert( options::eagerInstQuant() );
- InstMatch m( f );
+ InstMatch m( q );
for( int i=0; i<(int)t.getNumChildren(); i++ ){
if( d_match_pattern[i].getKind()==INST_CONSTANT ){
m.setValue(d_var_num[i], t[i]);
return 0;
}
}
- return qe->addInstantiation( f, m, false ) ? 1 : 0;
+ return qe->addInstantiation( q, m, false ) ? 1 : 0;
}
}/* CVC4::theory::inst namespace */
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;
/** get the next match. must call reset( eqc ) before this function. */
- virtual bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) = 0;
+ virtual bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) = 0;
/** add instantiations directly */
- virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
+ virtual int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
/** add ground term t, called when t is added to term db */
- virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) { return 0; }
+ virtual int addTerm( Node q, Node t, QuantifiersEngine* qe ) { return 0; }
/** set active add */
virtual void setActiveAdd( bool val ) {}
};/* class IMGenerator */
/** children types 0 : variable, 1 : child term, -1 : ground term */
std::vector< int > d_children_types;
/** continue */
- bool continueNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
+ bool continueNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
public:
enum {
//options for producing matches
d_match_pattern and t should have the same shape.
only valid for use where !d_match_pattern.isNull().
*/
- bool getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe );
+ bool getMatch( Node q, Node t, InstMatch& m, QuantifiersEngine* qe );
/** constructors */
InstMatchGenerator( Node pat );
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
void reset( Node eqc, QuantifiersEngine* qe );
/** get the next match. must call reset( eqc ) before this function. */
- bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
+ bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
/** add instantiations */
- int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
+ int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
/** add ground term t */
- int addTerm( Node f, Node t, QuantifiersEngine* qe );
+ int addTerm( Node q, Node t, QuantifiersEngine* qe );
bool d_active_add;
void setActiveAdd( bool val );
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
void reset( Node eqc, QuantifiersEngine* qe ){ d_eq_class = eqc; }
/** get the next match. must call reset( eqc ) before this function. */
- bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
+ bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
/** add instantiations directly */
- int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ return 0; }
+ int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){ return 0; }
};
//match generator for purified terms (matched term is substituted into d_subs)
VarMatchGeneratorTermSubs( Node var, Node subs );
~VarMatchGeneratorTermSubs() throw() {}
TNode d_var;
+ TypeNode d_var_type;
Node d_subs;
bool d_rm_prev;
/** reset instantiation round (call this at beginning of instantiation round) */
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
void reset( Node eqc, QuantifiersEngine* qe ){ d_eq_class = eqc; }
/** get the next match. must call reset( eqc ) before this function. */
- bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
+ bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
/** add instantiations directly */
- int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) { return 0; }
+ int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ) { return 0; }
};
/** smart multi-trigger implementation */
void calculateMatches( QuantifiersEngine* qe );
public:
/** constructors */
- InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe );
+ InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe );
/** destructor */
~InstMatchGeneratorMulti() throw() {}
/** reset instantiation round (call this whenever equivalence classes have changed) */
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
void reset( Node eqc, QuantifiersEngine* qe );
/** get the next match. must call reset( eqc ) before this function. (not implemented) */
- bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; }
+ bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; }
/** add instantiations */
- int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
+ int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
/** add ground term t */
- int addTerm( Node f, Node t, QuantifiersEngine* qe );
+ int addTerm( Node q, Node t, QuantifiersEngine* qe );
};/* class InstMatchGeneratorMulti */
/** smart (single)-trigger implementation */
void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );
public:
/** constructors */
- InstMatchGeneratorSimple( Node f, Node pat );
+ InstMatchGeneratorSimple( Node q, Node pat );
/** destructor */
~InstMatchGeneratorSimple() throw() {}
/** reset instantiation round (call this whenever equivalence classes have changed) */
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
void reset( Node eqc, QuantifiersEngine* qe ) {}
/** get the next match. must call reset( eqc ) before this function. (not implemented) */
- bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; }
+ bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; }
/** add instantiations */
- int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
+ int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
/** add ground term t, possibly add instantiations */
- int addTerm( Node f, Node t, QuantifiersEngine* qe );
+ int addTerm( Node q, Node t, QuantifiersEngine* qe );
};/* class InstMatchGeneratorSimple */
}
if( it != d_qn[index]->d_data.end() ) {
d_qni.push_back( it );
//set the match
- if( it->first.getType().isSubtypeOf( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first ) ){
+ if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first ) ){
Debug("qcf-match-debug") << " Binding variable" << std::endl;
if( d_qn.size()<d_qni_size ){
d_qn.push_back( &it->second );
return 0;
}
+int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) {
+ Node vatom;
+ //isolate pv in the inequality
+ int ires = isolate( v, msum, vatom, k, true );
+ if( ires!=0 ){
+ val = vatom[ ires==1 ? 1 : 0 ];
+ Node pvm = vatom[ ires==1 ? 0 : 1 ];
+ //get monomial
+ if( pvm!=v ){
+ Node veq_v;
+ if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){
+ Assert( veq_v==v );
+ }
+ }
+ }
+ return ires;
+}
+
Node QuantArith::negate( Node t ) {
Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t );
tt = Rewriter::rewrite( tt );
static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum );
//return 1 : solved on LHS, return -1 : solved on RHS, return 0: failed
static int isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff = false );
+ static int isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k );
static Node negate( Node t );
static Node offset( Node t, int i );
static void debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c );
return containsTerms( n, t );
}
+Node TermDb::mkNodeType( Node n, TypeNode tn ) {
+ TypeNode ntn = n.getType();
+ Assert( ntn.isComparableTo( tn ) );
+ if( ntn.isSubtypeOf( tn ) ){
+ return n;
+ }else{
+ if( tn.isInteger() ){
+ return NodeManager::currentNM()->mkNode( TO_INTEGER, n );
+ }
+ return Node::null();
+ }
+}
+
bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) {
if( n==t ){
return true;
bool containsVtsTerm( std::vector< Node >& n, bool isFree = false );
/** simple check for contains term */
bool containsVtsInfinity( Node n, bool isFree = false );
+ /** make type */
+ static Node mkNodeType( Node n, TypeNode tn );
private:
//helper for contains term
++(qe->d_statistics.d_simple_triggers);
}
}else{
- Trace("multi-trigger") << "Multi-trigger " << (*this) << " for " << f << std::endl;
+ Trace("multi-trigger") << "Multi-trigger ";
+ debugPrint("multi-trigger");
+ Trace("multi-trigger") << " for " << f << std::endl;
//Notice() << "Multi-trigger for " << f << " : " << std::endl;
//Notice() << " " << (*this) << std::endl;
++(qe->d_statistics.d_multi_triggers);
/** get all variables that E-matching can possibly handle */
static void getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars );
- inline void toStream(std::ostream& out) const {
- /*
- out << "TRIGGER( ";
- for( int i=0; i<(int)d_nodes.size(); i++ ){
- if( i>0 ){ out << ", "; }
- out << d_nodes[i];
- }
- out << " )";
- */
- }
void debugPrint( const char * c ) {
Trace(c) << "TRIGGER( ";
for( int i=0; i<(int)d_nodes.size(); i++ ){
}
};
-inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) {
- tr.toStream(out);
- return out;
-}
-
-
/** a trie of triggers */
class TriggerTrie {
private:
}
}
-bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){
+bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){
Assert( f.getKind()==FORALL );
Assert( vars.size()==terms.size() );
Node body = getInstantiation( f, vars, terms );
Assert( terms.size()==q[0].getNumChildren() );
Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl;
for( unsigned i=0; i<terms.size(); i++ ){
- Trace("inst-add-debug") << " " << q[0][i] << " -> " << terms[i] << std::endl;
+ Trace("inst-add-debug") << " " << q[0][i] << " -> " << terms[i];
//make it representative, this is helpful for recognizing duplication
if( mkRep ){
//pick the best possible representative for instantiation, based on past use and simplicity of term
terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i );
+ }else{
+ //ensure the type is correct
+ terms[i] = quantifiers::TermDb::mkNodeType( terms[i], q[0][i].getType() );
}
+ Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
+ Assert( !terms[i].isNull() );
}
//check based on instantiation level
//add the instantiation
Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
- bool addedInst = addInstantiation( q, d_term_db->d_vars[q], terms, doVts );
+ bool addedInst = addInstantiationInternal( q, d_term_db->d_vars[q], terms, doVts );
//report the result
if( addedInst ){
Trace("inst-add-debug") << " -> Success." << std::endl;
if( i>0 ) Trace("internal-rep-select") << ", ";
Trace("internal-rep-select") << eqc[i];
}
- Trace("internal-rep-select") << " } " << std::endl;
+ Trace("internal-rep-select") << " }, type = " << v_tn << std::endl;
int r_best_score = -1;
for( size_t i=0; i<eqc.size(); i++ ){
int score = getRepScore( eqc[i], f, index, v_tn );
d_rep_score[ r_best ] = d_reset_count;
}
Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
+ Assert( r_best.getType().isSubtypeOf( v_tn ) );
d_int_rep[v_tn][r] = r_best;
if( r_best!=a ){
Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
/** compute term vector */
void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
/** instantiate f with arguments terms */
- bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
+ bool addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
/** set instantiation level attr */
static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
/** flush lemmas */
cbqi-lia-dt-simp.smt2 \
is-int.smt2 \
floor.smt2 \
- array-unsat-simp3.smt2
+ array-unsat-simp3.smt2 \
+ mix-simp.smt2 \
+ mix-coeff.smt2 \
+ mix-match.smt2
# regression can be solved with --finite-model-find --fmf-inst-engine
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(assert (forall ((x Int) (y Int) (a Real) (z Int)) (or (> x (+ a (* (/ 2 3) y) (* (/ 4 5) z))) (< x (+ 10 (* 3 a) (* (/ 2 5) y) (* (/ 4 7) z))))))
+(check-sat)
\ No newline at end of file
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-fun P (Real) Bool)
+(assert (forall ((x Int)) (P x)))
+
+(declare-fun a () Real)
+(assert (is_int a))
+(assert (not (P a)))
+
+(check-sat)
\ No newline at end of file
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(assert (forall ((x Real)) (exists ((y Int)) (and (>= y x) (< y (+ x 1))))))
+(check-sat)
projects / cvc5.git / commitdiff