Node pv = d_vars[i];
TypeNode pvtn = pv.getType();
Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "]" << std::endl;
+ Node pv_value;
+ if( options::cbqiModel() ){
+ pv_value = d_qe->getModel()->getValue( pv );
+ Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
+ }
//if in effort=2, we must choose at least one model value
if( (i+1)<d_vars.size() || effort!=2 ){
-
+
//[1] easy case : pv is in the equivalence class as another term not containing pv
Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl;
std::map< Node, Node >::iterator itr = d_curr_rep.find( pv );
}
Node eq = eq_lhs.eqNode( eq_rhs );
eq = Rewriter::rewrite( eq );
- //cannot contain infinity
- if( !d_qe->getTermDatabase()->containsVtsInfinity( eq ) ){
- Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl;
- std::map< Node, Node > msum;
- if( QuantArith::getMonomialSumLit( eq, msum ) ){
- if( Trace.isOn("cbqi-inst-debug") ){
- Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl;
- QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
- Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl;
- }
- Node veq;
- if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){
- Trace("cbqi-inst-debug") << "...isolated equality " << veq << "." << std::endl;
- Node veq_c;
- if( veq[0]!=pv ){
- Node veq_v;
- if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
- Assert( veq_v==pv );
- }
- }
- Node val = veq[1];
- //eliminate coefficient if real
- if( !pvtn.isInteger() && !veq_c.isNull() ){
- val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
- val = Rewriter::rewrite( val );
- veq_c = Node::null();
+ //cannot contain infinity?
+ //if( !d_qe->getTermDatabase()->containsVtsInfinity( eq ) ){
+ Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl;
+ std::map< Node, Node > msum;
+ if( QuantArith::getMonomialSumLit( eq, msum ) ){
+ if( Trace.isOn("cbqi-inst-debug") ){
+ Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl;
+ QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
+ Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl;
+ }
+ Node veq;
+ if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){
+ Trace("cbqi-inst-debug") << "...isolated equality " << veq << "." << std::endl;
+ Node veq_c;
+ if( veq[0]!=pv ){
+ Node veq_v;
+ if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
+ Assert( veq_v==pv );
}
- if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
- subs_proc[val][veq_c] = true;
- if( addInstantiationInc( val, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){
- return true;
- }
+ }
+ Node val = veq[1];
+ //eliminate coefficient if real
+ if( !pvtn.isInteger() && !veq_c.isNull() ){
+ val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
+ val = Rewriter::rewrite( val );
+ veq_c = Node::null();
+ }
+ if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
+ subs_proc[val][veq_c] = true;
+ if( addInstantiationInc( val, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){
+ return true;
}
}
}
//if it contains pv, not infinity
if( !atom_lhs.isNull() && d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){
Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
- //cannot contain infinity
- 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" );
- 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 );
- }
- }
- //eliminate coefficient if real
- if( !pvtn.isInteger() && !veq_c.isNull() ){
- val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
- val = Rewriter::rewrite( val );
- veq_c = Node::null();
+ //cannot contain infinity?
+ //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" );
+ 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 );
}
+ }
+ //eliminate coefficient if real
+ if( !pvtn.isInteger() && !veq_c.isNull() ){
+ val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
+ val = Rewriter::rewrite( val );
+ veq_c = Node::null();
+ }
- //disequalities are both strict upper and lower bounds
- unsigned rmax = atom.getKind()==GEQ ? 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{
- Assert( atom.getKind()==EQUAL && !pol );
+ //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 = r==0 ? -1 : 1;
uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
uval = Rewriter::rewrite( uval );
}else{
Assert( pvtn.isReal() );
- uires = r==0 ? -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;
+ }else{
+ unsigned use_r = r;
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 );
- mbp_strict[index].push_back( uires==2 || uires==-2 );
- mbp_lit[index].push_back( lit );
+ // disequality is a disjunction : only consider the bound in the direction of the model
+ Node rhs_value = d_qe->getModel()->getValue( 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 );
+ }
+ Assert( lhs_value!=rhs_value );
+ Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
+ cmp = Rewriter::rewrite( cmp );
+ Assert( cmp.isConst() );
+ use_r = cmp==d_true ? 1 : 0;
+ }
+ Assert( atom.getKind()==EQUAL && !pol );
+ if( pvtn.isInteger() ){
+ uires = use_r==0 ? -1 : 1;
+ uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
+ uval = Rewriter::rewrite( uval );
}else{
- //take into account delta
- if( uires==2 || uires==-2 ){
- if( d_use_vts_delta ){
- Node delta = d_qe->getTermDatabase()->getVtsDelta();
- uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta );
- uval = Rewriter::rewrite( uval );
- }
+ Assert( pvtn.isReal() );
+ uires = use_r==0 ? -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;
+ 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 );
+ mbp_strict[index].push_back( uires==2 || uires==-2 );
+ mbp_lit[index].push_back( lit );
+ }else{
+ //take into account delta
+ if( uires==2 || uires==-2 ){
+ if( d_use_vts_delta ){
+ Node delta = d_qe->getTermDatabase()->getVtsDelta();
+ uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta );
+ uval = Rewriter::rewrite( uval );
}
- if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
- subs_proc[uval][veq_c] = true;
- if( addInstantiationInc( uval, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){
- return true;
- }
- }else{
- Trace("cbqi-inst-debug") << "...already processed." << std::endl;
+ }
+ if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
+ subs_proc[uval][veq_c] = true;
+ if( addInstantiationInc( uval, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){
+ return true;
}
+ }else{
+ Trace("cbqi-inst-debug") << "...already processed." << std::endl;
}
}
}
bool upper_first = false;
unsigned best_used[2];
std::vector< Node > t_values[2];
- Node pv_value = d_qe->getModel()->getValue( pv );
- Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
//try optimal bounds
for( unsigned r=0; r<2; r++ ){
int rr = upper_first ? (1-r) : r;
if( mbp_bounds[rr].empty() ){
- if( d_use_vts_inf ){
+ if( d_use_vts_inf && ( pvtn.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ) ){
Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << pvtn << ")" << std::endl;
//no bounds, we do +- infinity
Node val = d_qe->getTermDatabase()->getVtsInfinity( pvtn );
int new_effort = pvtn.isBoolean() ? effort : 1;
#ifdef MBP_STRICT_ASSERTIONS
//we only resort to values in the case of booleans
- Assert( !options::cbqiUseInf() || pvtn.isBoolean() );
+ Assert( !options::cbqiUseInfInt() || !options::cbqiUseInfReal() || pvtn.isBoolean() );
#endif
if( addInstantiationInc( mv, pv, pv_coeff_m, subs, vars, coeff, has_coeff, theta, i, new_effort ) ){
return true;
bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, std::vector< Node >& subs, std::vector< Node >& vars,
std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort ) {
if( Trace.isOn("cbqi-inst") ){
- for( unsigned i=0; i<subs.size(); i++ ){
+ for( unsigned j=0; j<subs.size(); j++ ){
Trace("cbqi-inst") << " ";
}
- Trace("cbqi-inst") << "i: ";
+ Trace("cbqi-inst") << subs.size() << ": ";
if( !pv_coeff.isNull() ){
Trace("cbqi-inst") << pv_coeff << " * ";
}
if( !pv_coeff.isNull() ){
has_coeff.push_back( pv );
}
- Trace("cbqi-inst-debug") << i << ": ";
- if( !pv_coeff.isNull() ){
- Trace("cbqi-inst-debug") << pv_coeff << "*";
- }
- Trace("cbqi-inst-debug") << pv << " -> " << n << std::endl;
Node new_theta = theta;
if( !pv_coeff.isNull() ){
if( new_theta.isNull() ){
d_curr_eqc.clear();
d_curr_rep.clear();
d_curr_arith_eqc.clear();
-
+
eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
//to eliminate identified illegal terms
std::map< Node, Node > aux_uf;
std::map< Node, Node > aux_subs;
std::map< Node, bool > aux_subs_inelig;
-
+
//for each variable
bool has_arith_var = false;
for( unsigned i=0; i<d_vars.size(); i++ ){
Node lit = (*it).assertion;
d_curr_asserts[tid].push_back( lit );
Trace("cbqi-proc-debug") << "...add : " << lit << std::endl;
+ if( lit.getKind()==EQUAL ){
+ std::map< Node, std::map< Node, Node > >::iterator itae = d_aux_eq.find( lit );
+ if( itae!=d_aux_eq.end() ){
+ for( std::map< Node, Node >::iterator itae2 = itae->second.begin(); itae2 != itae->second.end(); ++itae2 ){
+ aux_subs[ itae2->first ] = itae2->second;
+ Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl;
+ }
+ }
+ }
+ /*
if( lit.getKind()==EQUAL ){
//check if it is an auxiliary variable (for instance, from ITE removal). If so, solve for it.
for( unsigned k=0; k<2; k++ ){
}
}
}
+ */
}
}
}
while( !eqcs_i.isFinished() ){
Node r = *eqcs_i;
TypeNode rtn = r.getType();
- if( rtn.isInteger() || rtn.isReal() ){
+ if( rtn.isInteger() || rtn.isReal() ){
Trace("cbqi-proc-debug") << "...arith eqc: " << r << std::endl;
d_curr_arith_eqc.push_back( r );
if( d_curr_eqc.find( r )==d_curr_eqc.end() ){
if( it!=aux_subs.end() ){
addToAuxVarSubstitution( subs_lhs, subs_rhs, l, it->second );
}else{
+ Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << l << "!!!" << std::endl;
#ifdef MBP_STRICT_ASSERTIONS
Assert( false );
#endif
- Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << l << "!!!" << std::endl;
}
- }
+ }
+
-
//apply substitutions to everything, if necessary
if( !subs_lhs.empty() ){
Trace("cbqi-proc") << "Applying substitution : " << std::endl;
for( unsigned i=0; i<subs_lhs.size(); i++ ){
Trace("cbqi-proc") << " " << subs_lhs[i] << " -> " << subs_rhs[i] << std::endl;
}
-
+
for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){
for( unsigned i=0; i<it->second.size(); i++ ){
Node lit = it->second[i];
if( d_inelig.find( n )==d_inelig.end() ){
//must contain at least one variable
if( !d_prog_var[n].empty() ){
+ Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl;
akeep.push_back( n );
}else{
Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains no relevant variables." << std::endl;
it->second.clear();
it->second.insert( it->second.end(), akeep.begin(), akeep.end() );
}
-
+
//remove duplicate terms from eqc
for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){
std::vector< Node > new_eqc;
void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ) {
r = r.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
-
+
std::vector< Node > cl;
cl.push_back( l );
std::vector< Node > cr;
nr = Rewriter::rewrite( nr );
subs_rhs[i] = nr;
}
-
+
subs_lhs.push_back( l );
subs_rhs.push_back( r );
}
if( e<1 ){
return STATUS_UNFINISHED;
}else if( e==1 ){
- CegInstantiator * cinst;
- std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f );
- if( it==d_cinst.end() ){
- cinst = new CegInstantiator( d_quantEngine, d_out, true, options::cbqiUseInf() );
- for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
- cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) );
- }
- std::map< Node, std::vector< Node > >::iterator itav = d_aux_variables.find( f );
- if( itav!=d_aux_variables.end() ){
- cinst->d_aux_vars.insert( cinst->d_aux_vars.begin(), itav->second.begin(), itav->second.end() );
- }
- d_cinst[f] = cinst;
- }else{
- cinst = it->second;
- }
+ CegInstantiator * cinst = getInstantiator( f );
Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
d_curr_quant = f;
bool addedLemma = cinst->check();
}
}
-void InstStrategyCegqi::setAuxiliaryVariables( Node q, std::vector< Node >& vars ) {
+CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( q );
- if( it!=d_cinst.end() ){
- Assert( it->second->d_aux_vars.empty() );
- it->second->d_aux_vars.insert( it->second->d_aux_vars.end(), vars.begin(), vars.end() );
+ if( it==d_cinst.end() ){
+ CegInstantiator * cinst = new CegInstantiator( d_quantEngine, d_out, true, true );
+ for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){
+ cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) );
+ }
+ d_cinst[q] = cinst;
+ return cinst;
}else{
- Assert( d_aux_variables.find( q )==d_aux_variables.end() );
- d_aux_variables[q].insert( d_aux_variables[q].end(), vars.begin(), vars.end() );
+ return it->second;
}
}
-
-
std::vector< Node > d_vars;
//auxiliary variables
std::vector< Node > d_aux_vars;
+ //literals to equalities for aux vars
+ std::map< Node, std::map< Node, Node > > d_aux_eq;
//check : add instantiations based on valuation of d_vars
bool check();
};
private:
CegqiOutputInstStrategy * d_out;
std::map< Node, CegInstantiator * > d_cinst;
- std::map< Node, std::vector< Node > > d_aux_variables;
Node d_small_const;
Node d_curr_quant;
bool d_check_vts_lemma_lc;
/** identify */
std::string identify() const { return std::string("Cegqi"); }
- //set auxiliary variables
- void setAuxiliaryVariables( Node q, std::vector< Node >& vars );
+ //get instantiator for quantifier
+ CegInstantiator * getInstantiator( Node q );
};
}
std::vector< Node > lems;
lems.push_back( lem );
d_quantEngine->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
- std::vector< Node > aux_vars;
- for( unsigned i=0; i<lems.size(); i++ ){
- Trace("cbqi-debug") << "Counterexample lemma (processed) " << i << " : " << lems[i] << std::endl;
- d_quantEngine->addLemma( lems[i], false );
- }
- for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
- Trace("cbqi-debug") << " Auxiliary var (from ITE) : " << i->first << std::endl;
- aux_vars.push_back( i->first );
- }
- //record the auxiliary variables in the inst strategy
+ CegInstantiator * cinst = NULL;
if( d_i_cegqi ){
- d_i_cegqi->setAuxiliaryVariables( f, aux_vars );
+ cinst = d_i_cegqi->getInstantiator( f );
+ Assert( cinst->d_aux_vars.empty() );
+ for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
+ Trace("cbqi-debug") << " Auxiliary var (from ITE) : " << i->first << std::endl;
+ cinst->d_aux_vars.push_back( i->first );
+ }
+ }
+ for( unsigned i=0; i<lems.size(); i++ ){
+ Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite) " << i << " : " << lems[i] << std::endl;
+ if( !cinst ){
+ d_quantEngine->addLemma( lems[i], false );
+ }else{
+ Node rlem = lems[i];
+ rlem = Rewriter::rewrite( rlem );
+ Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
+ d_quantEngine->addLemma( rlem, false );
+ //record the literals that imply auxiliary variables to be equal to terms
+ if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){
+ if( lems[i][1].getKind()==EQUAL && lems[i][2].getKind()==EQUAL && lems[i][1][0]==lems[i][2][0] ){
+ if( std::find( cinst->d_aux_vars.begin(), cinst->d_aux_vars.end(), lems[i][1][0] )!=cinst->d_aux_vars.end() ){
+ Node v = lems[i][1][0];
+ for( unsigned r=1; r<=2; r++ ){
+ cinst->d_aux_eq[rlem[r]][v] = lems[i][r][1];
+ Trace("cbqi-debug") << " " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl;
+ }
+ }
+ }
+ }
+ }
}
addedLemma = true;
# ( forall x. P( x ) ) V Q
option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
disable miniscope quantifiers for ground subformulas
-# Whether to prenex (nested universal) quantifiers
+option clauseSplit --clause-split bool :default true
+ apply clause splitting to quantified formulas
option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h"
prenex mode for quantified formulas
# Whether to variable-eliminate quantifiers.
# Whether to CNF quantifier bodies
# option cnfQuant --cnf-quant bool :default false
# apply CNF conversion to quantified formulas
-# Whether to NNF quantifier bodies
option nnfQuant --nnf-quant bool :default true
apply NNF conversion to quantified formulas
-option clauseSplit --clause-split bool :default true
- apply clause splitting to quantified formulas
# Whether to pre-skolemize quantifier bodies.
# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
# forall x. P( x ) => f( S( x ) ) = x
apply skolemization to nested quantified formulass
option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true
apply skolemization to quantified formulas aggressively
-# Whether to perform agressive miniscoping
option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
perform aggressive miniscoping for quantifiers
-# Whether to CNF quantifier bodies
option elimTautQuant --elim-taut-quant bool :default true
eliminate tautological disjuncts of quantified formulas
answer sat when quantifiers are asserted with counterexample-based quantifier instantiation
option cbqiModel --cbqi-model bool :read-write :default true
guide instantiations by model values for counterexample-based quantifier instantiation
-option cbqiUseInf --cbqi-use-inf bool :read-write :default false
- use infinity for vts in counterexample-based quantifier instantiation
+option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false
+ use integer infinity for vts in counterexample-based quantifier instantiation
+option cbqiUseInfReal --cbqi-use-inf-real bool :read-write :default false
+ use real infinity for vts in counterexample-based quantifier instantiation
+
### local theory extensions options
}
void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
- newHasPol = hasPol;
- newPol = pol;
- if( n.getKind()==NOT || ( n.getKind()==IMPLIES && child==0 ) ){
+ if( n.getKind()==AND || n.getKind()==OR ){
+ newHasPol = hasPol;
+ newPol = pol;
+ }else if( n.getKind()==IMPLIES ){
+ newHasPol = hasPol;
+ newPol = child==0 ? !pol : pol;
+ }else if( n.getKind()==NOT ){
+ newHasPol = hasPol;
newPol = !pol;
- }else if( n.getKind()==IFF || n.getKind()==XOR ){
- newHasPol = false;
}else if( n.getKind()==ITE ){
- if( child==0 ){
- newHasPol = false;
- }
+ newHasPol = (child!=0) && hasPol;
+ newPol = pol;
+ }else{
+ newHasPol = false;
+ newPol = pol;
}
}
}
}
-Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) {
- if( body.getType().isBoolean() ){
- if( body.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){
- for( size_t i=0; i<2; i++ ){
- if( body[i].getKind()==ITE ){
- Node no = i==0 ? body[1] : body[0];
- if( no.getKind()!=ITE ){
- bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL;
- std::vector< Node > children;
- children.push_back( body[i][0] );
- for( size_t j=1; j<=2; j++ ){
- //check if it rewrites to a constant
- Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] );
- nn = Rewriter::rewrite( nn );
- children.push_back( nn );
- if( nn.isConst() ){
- doRewrite = true;
- }
- }
- if( doRewrite ){
- return NodeManager::currentNM()->mkNode( ITE, children );
+Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond ) {
+ if( body.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){
+ for( size_t i=0; i<2; i++ ){
+ if( body[i].getKind()==ITE ){
+ Node no = i==0 ? body[1] : body[0];
+ if( no.getKind()!=ITE ){
+ bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL;
+ std::vector< Node > children;
+ children.push_back( body[i][0] );
+ for( size_t j=1; j<=2; j++ ){
+ //check if it rewrites to a constant
+ Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] );
+ nn = Rewriter::rewrite( nn );
+ children.push_back( nn );
+ if( nn.isConst() ){
+ doRewrite = true;
}
}
+ if( doRewrite ){
+ return NodeManager::currentNM()->mkNode( ITE, children );
+ }
}
}
- }else if( body.getKind()==ITE && hasPol ){
- if( options::iteCondVarSplitQuant() ){
- Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl;
- for( unsigned r=0; r<2; r++ ){
- //check if there is a variable elimination
- Node b = r==0 ? body[0] : body[0].negate();
- QuantPhaseReq qpr( b );
- std::vector< Node > vars;
- std::vector< Node > subs;
- Trace("quantifiers-rewrite-ite-debug") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl;
- for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
- Trace("quantifiers-rewrite-ite-debug") << "phase req " << it->first << " -> " << it->second << std::endl;
- if( it->second ){
- if( it->first.getKind()==EQUAL ){
- for( unsigned i=0; i<2; i++ ){
- if( it->first[i].getKind()==BOUND_VARIABLE ){
- unsigned j = i==0 ? 1 : 0;
- if( !hasArg1( it->first[i], it->first[j] ) ){
- vars.push_back( it->first[i] );
- subs.push_back( it->first[j] );
- break;
- }
+ }
+ }else if( body.getKind()==ITE ){
+ if( body.getType().isBoolean() && hasPol && options::iteCondVarSplitQuant() ){
+ Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl;
+ for( unsigned r=0; r<2; r++ ){
+ //check if there is a variable elimination
+ Node b = r==0 ? body[0] : body[0].negate();
+ QuantPhaseReq qpr( b );
+ std::vector< Node > vars;
+ std::vector< Node > subs;
+ Trace("quantifiers-rewrite-ite-debug") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl;
+ for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
+ Trace("quantifiers-rewrite-ite-debug") << "phase req " << it->first << " -> " << it->second << std::endl;
+ if( it->second ){
+ if( it->first.getKind()==EQUAL ){
+ for( unsigned i=0; i<2; i++ ){
+ if( it->first[i].getKind()==BOUND_VARIABLE ){
+ unsigned j = i==0 ? 1 : 0;
+ if( !hasArg1( it->first[i], it->first[j] ) ){
+ vars.push_back( it->first[i] );
+ subs.push_back( it->first[j] );
+ break;
}
}
}
}
}
- if( !vars.empty() ){
- //bool cpol = (r==1);
- Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
- //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- //pos = Rewriter::rewrite( pos );
- Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
- Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl;
- Trace("quantifiers-rewrite-ite") << " " << pos << std::endl;
- Trace("quantifiers-rewrite-ite") << " " << neg << std::endl;
- return NodeManager::currentNM()->mkNode( AND, pos, neg );
- }
+ }
+ if( !vars.empty() ){
+ //bool cpol = (r==1);
+ Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
+ //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+ //pos = Rewriter::rewrite( pos );
+ Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
+ Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl;
+ Trace("quantifiers-rewrite-ite") << " " << pos << std::endl;
+ Trace("quantifiers-rewrite-ite") << " " << neg << std::endl;
+ return NodeManager::currentNM()->mkNode( AND, pos, neg );
}
}
}
- if( body.getKind()!=EQUAL && body.getKind()!=APPLY_UF ){
- bool changed = false;
- std::vector< Node > children;
- for( size_t i=0; i<body.getNumChildren(); i++ ){
- bool newHasPol;
- bool newPol;
- QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
- Node nn = computeProcessIte( body[i], newHasPol, newPol );
- children.push_back( nn );
- changed = changed || nn!=body[i];
- }
- if( changed ){
- return NodeManager::currentNM()->mkNode( body.getKind(), children );
+ }
+ bool changed = false;
+ std::vector< Node > children;
+ for( size_t i=0; i<body.getNumChildren(); i++ ){
+ bool newHasPol;
+ bool newPol;
+ QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
+ if( body.getKind()==ITE && i>0 ){
+ currCond[children[0]] = (i==1);
+ }
+ Node nn = computeProcessIte( body[i], newHasPol, newPol, currCond );
+ if( body.getKind()==ITE && i==0 ){
+ std::map< Node, bool >::iterator itc = currCond.find( nn );
+ if( itc!=currCond.end() ){
+ if( itc->second ){
+ return computeProcessIte( body[1], hasPol, pol, currCond );
+ }else{
+ return computeProcessIte( body[2], hasPol, pol, currCond );
+ }
}
}
+ children.push_back( nn );
+ changed = changed || nn!=body[i];
+ }
+ if( body.getKind()==ITE ){
+ currCond.erase( children[0] );
+ }
+ if( changed ){
+ if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.insert( children.begin(), body.getOperator() );
+ }
+ return NodeManager::currentNM()->mkNode( body.getKind(), children );
+ }else{
+ return body;
}
- return body;
}
Node QuantifiersRewriter::computeProcessIte2( Node body ){
}else if( computeOption==COMPUTE_NNF ){
return options::nnfQuant();
}else if( computeOption==COMPUTE_PROCESS_ITE ){
- return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
+ //always eliminate redundant conditions in ITE
+ return true;
+ //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
}else if( computeOption==COMPUTE_PROCESS_ITE_2 ){
return options::iteDtTesterSplitQuant();
}else if( computeOption==COMPUTE_PRENEX ){
}else if( computeOption==COMPUTE_NNF ){
n = computeNNF( n );
}else if( computeOption==COMPUTE_PROCESS_ITE ){
- n = computeProcessIte( n, true, true );
+ std::map< Node, bool > curr_cond;
+ n = computeProcessIte( n, true, true, curr_cond );
}else if( computeOption==COMPUTE_PROCESS_ITE_2 ){
n = computeProcessIte2( n );
}else if( computeOption==COMPUTE_PRENEX ){
static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl );
static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
static Node computeNNF( Node body );
- static Node computeProcessIte( Node body, bool hasPol, bool pol );
+ static Node computeProcessIte( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond );
static Node computeProcessIte2( Node body );
static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
Trace("quant-engine-ee") << "Equality engine : " << std::endl;
debugPrintEqualityEngine( "quant-engine-ee" );
}
+ if( Trace.isOn("quant-engine-assert") ){
+ Trace("quant-engine-assert") << "Assertions : " << std::endl;
+ getTheoryEngine()->printAssertions("quant-engine-assert");
+ }
//reset relevant information
d_conflict = false;
/** Visitor for collecting shared terms */
SharedTermsVisitor d_sharedTermsVisitor;
- /** Prints the assertions to the debug stream */
- void printAssertions(const char* tag);
-
/** Dump the assertions to the dump */
void dumpAssertions(const char* tag);
RemoveITE* getIteRemover() { return &d_iteRemover; }
SortInference* getSortInference() { return &d_sortInfer; }
+
+ /** Prints the assertions to the debug stream */
+ void printAssertions(const char* tag);
+
private:
std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
public:
//add splitting lemma for cardinality constraint
Assert( !d_cardinality_term.isNull() );
Node lem = getCardinalityLiteral( d_aloc_cardinality );
+ Trace("uf-ss-lemma") << "*** Cardinality split on : " << lem << std::endl;
lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() );
d_cardinality_lemma[ d_aloc_cardinality ] = lem;
//add as lemma to output channel
--- /dev/null
+(set-logic LIA)
+(set-info :status unsat)
+(declare-fun W_S2_V6 () Bool)
+(declare-fun W_S2_V4 () Bool)
+(declare-fun W_S2_V2 () Bool)
+(declare-fun W_S2_V3 () Bool)
+(declare-fun W_S2_V1 () Bool)
+(declare-fun W_S1_V6 () Bool)
+(declare-fun W_S1_V5 () Bool)
+(declare-fun W_S1_V2 () Bool)
+(declare-fun W_S1_V3 () Bool)
+(declare-fun W_S1_V1 () Bool)
+(declare-fun R_S1_V1 () Bool)
+(declare-fun R_S2_V6 () Bool)
+(declare-fun R_S2_V4 () Bool)
+(declare-fun R_S2_V5 () Bool)
+(declare-fun R_S2_V2 () Bool)
+(declare-fun R_S2_V3 () Bool)
+(declare-fun R_S2_V1 () Bool)
+(declare-fun R_E1_V6 () Bool)
+(declare-fun R_E1_V4 () Bool)
+(declare-fun R_E1_V5 () Bool)
+(declare-fun R_E1_V2 () Bool)
+(declare-fun R_E1_V3 () Bool)
+(declare-fun R_E1_V1 () Bool)
+(declare-fun DISJ_W_S2_R_E1 () Bool)
+(declare-fun DISJ_W_S2_R_S2 () Bool)
+(declare-fun R_S1_V6 () Bool)
+(declare-fun R_S1_V4 () Bool)
+(declare-fun R_S1_V5 () Bool)
+(declare-fun R_S1_V2 () Bool)
+(declare-fun R_S1_V3 () Bool)
+(declare-fun DISJ_W_S2_R_S1 () Bool)
+(declare-fun DISJ_W_S1_W_S2 () Bool)
+(declare-fun DISJ_W_S1_R_E1 () Bool)
+(declare-fun DISJ_W_S1_R_S2 () Bool)
+(declare-fun DISJ_W_S1_R_S1 () Bool)
+(declare-fun W_S2_V5 () Bool)
+(declare-fun W_S1_V4 () Bool)
+(assert
+ (let
+ (($x1615
+ (forall
+ ((V1_0 Int) (V3_0 Int)
+ (V2_0 Int) (V5_0 Int)
+ (V4_0 Int) (V6_0 Int)
+ (MW_S1_V1 Bool) (MW_S1_V3 Bool)
+ (MW_S1_V2 Bool) (MW_S1_V5 Bool)
+ (MW_S1_V4 Bool) (MW_S1_V6 Bool)
+ (MW_S2_V1 Bool) (MW_S2_V3 Bool)
+ (MW_S2_V2 Bool) (MW_S2_V5 Bool)
+ (MW_S2_V4 Bool) (MW_S2_V6 Bool)
+ (S1_V1_!158 Int) (S1_V1_!171 Int)
+ (S2_V5_!167 Int) (S2_V5_!180 Int)
+ (S1_V3_!159 Int) (S1_V3_!172 Int)
+ (S1_V2_!160 Int) (S1_V2_!173 Int)
+ (E1_!157 Int) (E1_!170 Int)
+ (E1_!183 Int) (S2_V4_!168 Int)
+ (S2_V4_!181 Int) (S2_V6_!169 Int)
+ (S2_V6_!182 Int) (S1_V5_!161 Int)
+ (S1_V5_!174 Int) (S2_V1_!164 Int)
+ (S2_V1_!177 Int) (S1_V4_!162 Int)
+ (S1_V4_!175 Int) (S2_V3_!165 Int)
+ (S2_V3_!178 Int) (S2_V2_!166 Int)
+ (S2_V2_!179 Int) (S1_V6_!163 Int)
+ (S1_V6_!176 Int))
+ (let ((?x1431 (ite MW_S1_V6 S1_V6_!176 V6_0)))
+ (let ((?x1432 (ite MW_S2_V6 S2_V6_!182 ?x1431)))
+ (let ((?x1433 (ite MW_S1_V6 S1_V6_!163 V6_0)))
+ (let ((?x1434 (ite MW_S2_V6 S2_V6_!169 ?x1433)))
+ (let (($x1435 (= ?x1434 ?x1432)))
+ (let ((?x1436 (ite MW_S1_V4 S1_V4_!175 V4_0)))
+ (let ((?x1437 (ite MW_S2_V4 S2_V4_!181 ?x1436)))
+ (let ((?x1438 (ite MW_S1_V4 S1_V4_!162 V4_0)))
+ (let ((?x1439 (ite MW_S2_V4 S2_V4_!168 ?x1438)))
+ (let (($x1440 (= ?x1439 ?x1437)))
+ (let ((?x1441 (ite MW_S1_V5 S1_V5_!174 V5_0)))
+ (let ((?x1442 (ite MW_S2_V5 S2_V5_!180 ?x1441)))
+ (let ((?x1444 (ite MW_S1_V5 S1_V5_!161 V5_0)))
+ (let ((?x1445 (ite MW_S2_V5 S2_V5_!167 ?x1444)))
+ (let (($x1446 (= ?x1445 ?x1442)))
+ (let ((?x1447 (ite MW_S1_V2 S1_V2_!173 V2_0)))
+ (let ((?x1448 (ite MW_S2_V2 S2_V2_!179 ?x1447)))
+ (let ((?x1449 (ite MW_S1_V2 S1_V2_!160 V2_0)))
+ (let ((?x1450 (ite MW_S2_V2 S2_V2_!166 ?x1449)))
+ (let (($x1451 (= ?x1450 ?x1448)))
+ (let ((?x1467 (ite MW_S1_V3 S1_V3_!159 V3_0)))
+ (let ((?x1468 (+ 1 ?x1467)))
+ (let ((?x1458 (ite MW_S2_V3 S2_V3_!165 ?x1468)))
+ (let
+ (($x1459
+ (= ?x1458
+ (+ (ite MW_S2_V3 S2_V3_!178 (ite MW_S1_V3 S1_V3_!172 V3_0)) ?x1448
+ (* (- 1) E1_!183)))))
+ (let ((?x1460 (ite MW_S1_V1 S1_V1_!171 E1_!170)))
+ (let ((?x1487 (ite MW_S2_V1 S2_V1_!177 ?x1460)))
+ (let ((?x1453 (ite MW_S1_V1 S1_V1_!158 E1_!157)))
+ (let ((?x1489 (ite MW_S2_V1 S2_V1_!164 ?x1453)))
+ (let (($x1289 (= ?x1489 ?x1487)))
+ (let ((?x1455 (+ (- 1) ?x1448)))
+ (let (($x1376 (>= ?x1487 ?x1455)))
+ (let (($x1377 (<= V2_0 E1_!170)))
+ (let (($x1379 (not $x1377)))
+ (let ((?x1380 (+ (- 1) ?x1450)))
+ (let (($x1381 (>= ?x1489 ?x1380)))
+ (let (($x1479 (<= V2_0 E1_!157)))
+ (let (($x1456 (not $x1479)))
+ (let (($x1499 (and $x1456 $x1381 $x1379 $x1376)))
+ (let (($x1500 (not $x1499)))
+ (let (($x1502 (not MW_S2_V6)))
+ (let (($x1503 (or $x1502 W_S2_V6)))
+ (let (($x1504 (not MW_S2_V4)))
+ (let (($x1505 (or $x1504 W_S2_V4)))
+ (let (($x1508 (not MW_S2_V2)))
+ (let (($x1509 (or $x1508 W_S2_V2)))
+ (let (($x1510 (not MW_S2_V3)))
+ (let (($x1511 (or $x1510 W_S2_V3)))
+ (let (($x1512 (not MW_S2_V1)))
+ (let (($x1513 (or $x1512 W_S2_V1)))
+ (let (($x1514 (not MW_S1_V6)))
+ (let (($x1515 (or $x1514 W_S1_V6)))
+ (let (($x1518 (not MW_S1_V5)))
+ (let (($x1519 (or $x1518 W_S1_V5)))
+ (let (($x1520 (not MW_S1_V2)))
+ (let (($x1521 (or $x1520 W_S1_V2)))
+ (let (($x1522 (not MW_S1_V3)))
+ (let (($x1523 (or $x1522 W_S1_V3)))
+ (let (($x1524 (not MW_S1_V1)))
+ (let (($x1525 (or $x1524 W_S1_V1)))
+ (let (($x1527 (= S1_V6_!176 S1_V6_!163)))
+ (let (($x1528 (= E1_!170 E1_!157)))
+ (let (($x228 (not R_S1_V1)))
+ (let (($x1529 (or $x228 $x1528)))
+ (let (($x1530 (not $x1529)))
+ (let (($x1531 (or $x1530 $x1527)))
+ (let (($x1532 (= S2_V2_!179 S2_V2_!166)))
+ (let (($x1533 (= ?x1431 ?x1433)))
+ (let (($x253 (not R_S2_V6)))
+ (let (($x1534 (or $x253 $x1533)))
+ (let (($x1535 (= ?x1436 ?x1438)))
+ (let (($x251 (not R_S2_V4)))
+ (let (($x1536 (or $x251 $x1535)))
+ (let (($x1537 (= ?x1441 ?x1444)))
+ (let (($x249 (not R_S2_V5)))
+ (let (($x1538 (or $x249 $x1537)))
+ (let (($x1539 (= ?x1447 ?x1449)))
+ (let (($x247 (not R_S2_V2)))
+ (let (($x1540 (or $x247 $x1539)))
+ (let ((?x1462 (ite MW_S1_V3 S1_V3_!172 V3_0)))
+ (let (($x1541 (= ?x1462 ?x1468)))
+ (let (($x245 (not R_S2_V3)))
+ (let (($x1542 (or $x245 $x1541)))
+ (let (($x1543 (= ?x1460 ?x1453)))
+ (let (($x243 (not R_S2_V1)))
+ (let (($x1544 (or $x243 $x1543)))
+ (let (($x1545 (and $x1544 $x1542 $x1540 $x1538 $x1536 $x1534)))
+ (let (($x1546 (not $x1545)))
+ (let (($x1547 (or $x1546 $x1532)))
+ (let (($x1548 (= S2_V3_!165 S2_V3_!178)))
+ (let (($x1549 (= ?x1433 ?x1431)))
+ (let (($x1550 (or $x253 $x1549)))
+ (let (($x1551 (= ?x1438 ?x1436)))
+ (let (($x1552 (or $x251 $x1551)))
+ (let (($x1553 (= ?x1444 ?x1441)))
+ (let (($x1554 (or $x249 $x1553)))
+ (let (($x1555 (= ?x1449 ?x1447)))
+ (let (($x1556 (or $x247 $x1555)))
+ (let ((?x1557 (+ (- 1) ?x1462)))
+ (let (($x1558 (= ?x1467 ?x1557)))
+ (let (($x1559 (or $x245 $x1558)))
+ (let (($x1560 (= ?x1453 ?x1460)))
+ (let (($x1561 (or $x243 $x1560)))
+ (let (($x1562 (and $x1561 $x1559 $x1556 $x1554 $x1552 $x1550)))
+ (let (($x1563 (not $x1562)))
+ (let (($x1564 (or $x1563 $x1548)))
+ (let (($x1565 (= S1_V4_!175 S1_V4_!162)))
+ (let (($x1566 (or $x1530 $x1565)))
+ (let (($x1567 (= S2_V1_!177 S2_V1_!164)))
+ (let (($x1568 (or $x1546 $x1567)))
+ (let (($x1569 (= S1_V5_!174 S1_V5_!161)))
+ (let (($x1570 (or $x1530 $x1569)))
+ (let (($x1571 (= S2_V6_!182 S2_V6_!169)))
+ (let (($x1572 (or $x1546 $x1571)))
+ (let (($x1573 (= S2_V4_!168 S2_V4_!181)))
+ (let (($x1574 (or $x1563 $x1573)))
+ (let (($x1575 (= E1_!170 E1_!183)))
+ (let (($x1576 (= V6_0 ?x1432)))
+ (let (($x177 (not R_E1_V6)))
+ (let (($x1577 (or $x177 $x1576)))
+ (let (($x1578 (= V4_0 ?x1437)))
+ (let (($x175 (not R_E1_V4)))
+ (let (($x1579 (or $x175 $x1578)))
+ (let (($x1580 (= V5_0 ?x1442)))
+ (let (($x173 (not R_E1_V5)))
+ (let (($x1581 (or $x173 $x1580)))
+ (let (($x1582 (= V2_0 ?x1448)))
+ (let (($x171 (not R_E1_V2)))
+ (let (($x1583 (or $x171 $x1582)))
+ (let ((?x1463 (ite MW_S2_V3 S2_V3_!178 ?x1462)))
+ (let (($x1584 (= V3_0 ?x1463)))
+ (let (($x169 (not R_E1_V3)))
+ (let (($x1585 (or $x169 $x1584)))
+ (let ((?x1586 (+ 1 ?x1487)))
+ (let (($x1587 (= V1_0 ?x1586)))
+ (let (($x167 (not R_E1_V1)))
+ (let (($x1588 (or $x167 $x1587)))
+ (let (($x1589 (and $x1588 $x1585 $x1583 $x1581 $x1579 $x1577)))
+ (let (($x1590 (not $x1589)))
+ (let (($x1591 (or $x1590 $x1575)))
+ (let (($x1592 (= E1_!157 E1_!183)))
+ (let (($x1593 (or $x1590 $x1592)))
+ (let (($x1594 (= E1_!157 E1_!170)))
+ (let (($x1595 (= S1_V2_!173 S1_V2_!160)))
+ (let (($x1596 (or $x1530 $x1595)))
+ (let (($x1597 (= S1_V3_!159 S1_V3_!172)))
+ (let (($x1598 (or $x228 $x1594)))
+ (let (($x1599 (not $x1598)))
+ (let (($x1600 (or $x1599 $x1597)))
+ (let (($x1601 (= S2_V5_!180 S2_V5_!167)))
+ (let (($x1602 (or $x1546 $x1601)))
+ (let (($x1603 (= S1_V1_!158 S1_V1_!171)))
+ (let (($x1604 (or $x1599 $x1603)))
+ (let
+ (($x1612
+ (and $x1604 $x1602 $x1600 $x1596 $x1594 $x1593 $x1591 $x1574 $x1572
+ $x1570 $x1568 $x1566 $x1564 $x1547 $x1531 $x1525 $x1523 $x1521 $x1519
+ $x1515 $x1513 $x1511 $x1509 $x1505 $x1503)))
+ (let (($x1613 (not $x1612)))
+ (or $x1613 $x1500 (and $x1289 $x1459 $x1451 $x1446 $x1440 $x1435)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+ (let (($x103 (and W_S2_V6 R_E1_V6)))
+ (let (($x102 (and W_S2_V4 R_E1_V4)))
+ (let (($x100 (and W_S2_V2 R_E1_V2)))
+ (let (($x99 (and W_S2_V3 R_E1_V3)))
+ (let (($x98 (and W_S2_V1 R_E1_V1)))
+ (let (($x128 (or $x98 $x99 $x100 R_E1_V5 $x102 $x103)))
+ (let (($x129 (not $x128)))
+ (let (($x130 (= DISJ_W_S2_R_E1 $x129)))
+ (let (($x93 (and W_S2_V6 R_S2_V6)))
+ (let (($x92 (and W_S2_V4 R_S2_V4)))
+ (let (($x90 (and W_S2_V2 R_S2_V2)))
+ (let (($x89 (and W_S2_V3 R_S2_V3)))
+ (let (($x88 (and W_S2_V1 R_S2_V1)))
+ (let (($x125 (or $x88 $x89 $x90 R_S2_V5 $x92 $x93)))
+ (let (($x126 (not $x125)))
+ (let (($x127 (= DISJ_W_S2_R_S2 $x126)))
+ (let (($x83 (and W_S2_V6 R_S1_V6)))
+ (let (($x82 (and W_S2_V4 R_S1_V4)))
+ (let (($x80 (and W_S2_V2 R_S1_V2)))
+ (let (($x79 (and W_S2_V3 R_S1_V3)))
+ (let (($x78 (and W_S2_V1 R_S1_V1)))
+ (let (($x122 (or $x78 $x79 $x80 R_S1_V5 $x82 $x83)))
+ (let (($x123 (not $x122)))
+ (let (($x124 (= DISJ_W_S2_R_S1 $x123)))
+ (let (($x73 (and W_S1_V6 W_S2_V6)))
+ (let (($x68 (and W_S1_V2 W_S2_V2)))
+ (let (($x66 (and W_S1_V3 W_S2_V3)))
+ (let (($x64 (and W_S1_V1 W_S2_V1)))
+ (let (($x119 (or $x64 $x66 $x68 W_S1_V5 W_S2_V4 $x73)))
+ (let (($x120 (not $x119)))
+ (let (($x121 (= DISJ_W_S1_W_S2 $x120)))
+ (let (($x58 (and W_S1_V6 R_E1_V6)))
+ (let (($x54 (and W_S1_V5 R_E1_V5)))
+ (let (($x52 (and W_S1_V2 R_E1_V2)))
+ (let (($x50 (and W_S1_V3 R_E1_V3)))
+ (let (($x48 (and W_S1_V1 R_E1_V1)))
+ (let (($x116 (or $x48 $x50 $x52 $x54 R_E1_V4 $x58)))
+ (let (($x117 (not $x116)))
+ (let (($x118 (= DISJ_W_S1_R_E1 $x117)))
+ (let (($x42 (and W_S1_V6 R_S2_V6)))
+ (let (($x38 (and W_S1_V5 R_S2_V5)))
+ (let (($x36 (and W_S1_V2 R_S2_V2)))
+ (let (($x34 (and W_S1_V3 R_S2_V3)))
+ (let (($x32 (and W_S1_V1 R_S2_V1)))
+ (let (($x113 (or $x32 $x34 $x36 $x38 R_S2_V4 $x42)))
+ (let (($x114 (not $x113)))
+ (let (($x115 (= DISJ_W_S1_R_S2 $x114)))
+ (let (($x26 (and W_S1_V6 R_S1_V6)))
+ (let (($x21 (and W_S1_V5 R_S1_V5)))
+ (let (($x18 (and W_S1_V2 R_S1_V2)))
+ (let (($x15 (and W_S1_V3 R_S1_V3)))
+ (let (($x12 (and W_S1_V1 R_S1_V1)))
+ (let (($x110 (or $x12 $x15 $x18 $x21 R_S1_V4 $x26)))
+ (let (($x111 (not $x110)))
+ (let (($x112 (= DISJ_W_S1_R_S1 $x111)))
+ (and W_S1_V4 W_S2_V5 $x112 $x115 $x118 $x121 $x124 $x127 $x130 $x1615))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(assert
+ (let (($x1192 (not W_S2_V2)))
+ (let (($x1189 (not W_S2_V3)))
+ (let (($x1186 (not W_S2_V1)))
+ (let (($x1091 (not W_S1_V2)))
+ (let (($x1078 (not W_S1_V1)))
+ (let (($x245 (not R_S2_V3)))
+ (let (($x167 (not R_E1_V1)))
+ (let
+ (($x1647
+ (and $x167 $x245 $x1078 $x1091 $x1186 $x1189 $x1192 DISJ_W_S1_R_E1
+ DISJ_W_S2_R_E1))) (not $x1647))))))))))
+(check-sat)
+
nested-delta.smt2 \
nested-inf.smt2 \
RND-small.smt2 \
- clock-10.smt2
+ clock-10.smt2 \
+ 006-cbqi-ite.smt2
projects / cvc5.git / commitdiff