Node pv_coeff; //coefficient of pv in the equality we solve (null is 1)
bool proc = false;
if( !d_prog_var[n].empty() ){
- ns = applySubstitution( n, sf, vars, pv_coeff, false );
+ ns = applySubstitution( pvtn, n, sf, vars, pv_coeff, false );
if( !ns.isNull() ){
computeProgVars( ns );
//substituted version must be new and cannot contain pv
Node ns;
Node pv_coeff;
if( !d_prog_var[n].empty() ){
- ns = applySubstitution( n, sf, vars, pv_coeff );
+ ns = applySubstitution( pvtn, n, sf, vars, pv_coeff );
if( !ns.isNull() ){
computeProgVars( ns );
}
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;
+ Trace("cbqi-inst-debug") << "isolate for " << pv << " : " << pv.getType() << "..." << std::endl;
}
Node veq;
if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){
//apply substitution to LHS of atom
if( !d_prog_var[atom_lhs].empty() ){
Node atom_lhs_coeff;
- atom_lhs = applySubstitution( atom_lhs, sf, vars, atom_lhs_coeff );
+ atom_lhs = applySubstitution( pvtn, atom_lhs, sf, vars, atom_lhs_coeff );
if( !atom_lhs.isNull() ){
computeProgVars( atom_lhs );
if( !atom_lhs_coeff.isNull() ){
}
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 );
Trace("cbqi-bound") << std::endl;
best_used[rr] = (unsigned)best;
Node val = mbp_bounds[rr][best];
- val = getModelBasedProjectionValue( val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta,
+ 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] );
if( !val.isNull() ){
if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){
if( !use_inf && mbp_bounds[0].empty() && mbp_bounds[1].empty() ){
Node val = d_zero;
Node c; //null (one) coefficient
- val = getModelBasedProjectionValue( 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(), vts_sym[0], Node::null(), vts_sym[1] );
if( !val.isNull() ){
if( subs_proc[val].find( c )==subs_proc[val].end() ){
subs_proc[val][c] = true;
int rr = upper_first ? (1-r) : r;
for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){
if( j!=best_used[rr] ){
- Node val = getModelBasedProjectionValue( mbp_bounds[rr][j], rr==0, mbp_coeff[rr][j], pv_value, t_values[rr][j], theta,
+ 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] );
if( !val.isNull() ){
if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){
TNode tv = pv;
TNode ts = n;
Node a_pv_coeff;
- Node new_subs = applySubstitution( sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true );
+ Node new_subs = applySubstitution( vars[j].getType(), sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true );
if( !new_subs.isNull() ){
sf.d_subs[j] = new_subs;
if( !a_pv_coeff.isNull() ){
}
}
-Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff,
+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 ) {
Assert( d_prog_var.find( n )!=d_prog_var.end() );
Assert( n==Rewriter::rewrite( n ) );
if( n!=nret ){
nret = Rewriter::rewrite( nret );
}
- //result is nret
return nret;
}else{
- if( try_coeff ){
+ if( !tn.isInteger() ){
+ //can do basic substitution instead with divisions
+ std::vector< Node > nvars;
+ std::vector< Node > nsubs;
+ for( unsigned i=0; i<vars.size(); i++ ){
+ if( !coeff[i].isNull() ){
+ Assert( coeff[i].isConst() );
+ nsubs.push_back( Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/coeff[i].getConst<Rational>() ) ) ));
+ }else{
+ nsubs.push_back( subs[i] );
+ }
+ }
+ Node nret = n.substitute( vars.begin(), vars.end(), nsubs.begin(), nsubs.end() );
+ if( n!=nret ){
+ nret = Rewriter::rewrite( nret );
+ }
+ return nret;
+ }else if( try_coeff ){
//must convert to monomial representation
std::map< Node, Node > msum;
if( QuantArith::getMonomialSum( n, msum ) ){
}
}
-Node CegInstantiator::getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta,
+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 ) {
+ 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
Node ceValue = me;
Node new_theta = theta;
if( !c.isNull() ){
+ Assert( c.getType().isInteger() );
ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c );
ceValue = Rewriter::rewrite( ceValue );
if( new_theta.isNull() ){
Trace("cbqi-bound2") << "...c*e = " << ceValue << std::endl;
Trace("cbqi-bound2") << "...theta = " << new_theta << std::endl;
}
- if( !new_theta.isNull() ){
+ if( !new_theta.isNull() && e.getType().isInteger() ){
Node rho;
if( isLower ){
rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt );
}
}
-bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
- std::map< Node, bool >::iterator it = currCond.find( n );
- if( it==currCond.end() ){
- Trace("quantifiers-rewrite-ite-debug") << "ITE cond : " << n << " -> " << pol << std::endl;
- new_cond.push_back( n );
- currCond[n] = pol;
- return true;
- }else{
- Assert( it->second==pol );
- return false;
- }
-}
-
-void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
- if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- setEntailedCond( n[i], pol, currCond, new_cond );
- }
- }else if( n.getKind()==NOT ){
- setEntailedCond( n[0], !pol, currCond, new_cond );
- }
- if( addEntailedCond( n, pol, currCond, new_cond ) ){
- if( n.getKind()==APPLY_TESTER ){
- const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
- unsigned index = Datatype::indexOf(n.getOperator().toExpr());
- Assert( dt.getNumConstructors()>1 );
- if( pol ){
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- if( i!=index ){
- Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] );
- addEntailedCond( t, false, currCond, new_cond );
- }
- }
- }else{
- if( dt.getNumConstructors()==2 ){
- int oindex = 1-index;
- Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[oindex].getTester() ), n[0] );
- addEntailedCond( t, true, currCond, new_cond );
- }
- }
- }
- }
-}
-
int getEntailedCond( Node n, std::map< Node, bool >& currCond ){
std::map< Node, bool >::iterator it = currCond.find( n );
if( it!=currCond.end() ){
return 0;
}
-Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond ) {
- bool changed = false;
- std::vector< Node > children;
- for( size_t i=0; i<body.getNumChildren(); i++ ){
- std::vector< Node > new_cond;
- if( body.getKind()==ITE && i>0 ){
- setEntailedCond( children[0], i==1, currCond, new_cond );
- }
- bool newHasPol;
- bool newPol;
- QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
- Node nn = computeProcessIte( body[i], newHasPol, newPol, currCond );
- if( body.getKind()==ITE ){
- if( i==0 ){
- int res = getEntailedCond( nn, currCond );
- if( res==1 ){
- return computeProcessIte( body[1], hasPol, pol, currCond );
- }else if( res==-1 ){
- return computeProcessIte( body[2], hasPol, pol, currCond );
+bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
+ std::map< Node, bool >::iterator it = currCond.find( n );
+ if( it==currCond.end() ){
+ Trace("quantifiers-rewrite-ite-debug") << "ITE cond : " << n << " -> " << pol << std::endl;
+ new_cond.push_back( n );
+ currCond[n] = pol;
+ return true;
+ }else{
+ Assert( it->second==pol );
+ return false;
+ }
+}
+
+void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
+ if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ setEntailedCond( n[i], pol, currCond, new_cond );
+ }
+ }else if( n.getKind()==NOT ){
+ setEntailedCond( n[0], !pol, currCond, new_cond );
+ }else if( n.getKind()==ITE ){
+ int pol = getEntailedCond( n, currCond );
+ if( pol==1 ){
+ setEntailedCond( n[1], pol, currCond, new_cond );
+ }else if( pol==-1 ){
+ setEntailedCond( n[2], pol, currCond, new_cond );
+ }
+ }
+ if( addEntailedCond( n, pol, currCond, new_cond ) ){
+ if( n.getKind()==APPLY_TESTER ){
+ const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
+ unsigned index = Datatype::indexOf(n.getOperator().toExpr());
+ Assert( dt.getNumConstructors()>1 );
+ if( pol ){
+ for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+ if( i!=index ){
+ Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] );
+ addEntailedCond( t, false, currCond, new_cond );
+ }
}
}else{
- for( unsigned j=0; j<new_cond.size(); j++ ){
- currCond.erase( new_cond[j] );
+ if( dt.getNumConstructors()==2 ){
+ int oindex = 1-index;
+ Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[oindex].getTester() ), n[0] );
+ addEntailedCond( t, true, currCond, new_cond );
}
}
}
- children.push_back( nn );
- changed = changed || nn!=body[i];
}
- if( changed ){
- if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.insert( children.begin(), body.getOperator() );
+}
+
+Node QuantifiersRewriter::computeProcessTerms( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
+ std::map< Node, Node >& cache, std::map< Node, Node >& icache,
+ std::vector< Node >& new_vars, std::vector< Node >& new_conds ) {
+ Node ret;
+ std::map< Node, Node >::iterator iti = cache.find( body );
+ if( iti!=cache.end() ){
+ ret = iti->second;
+ }else{
+ bool do_ite = false;
+ if( body.getKind()==ITE && nCurrCond<8 ){
+ do_ite = true;
+ nCurrCond = nCurrCond + 1;
+ }
+ bool changed = false;
+ std::vector< Node > children;
+ for( size_t i=0; i<body.getNumChildren(); i++ ){
+ std::vector< Node > new_cond;
+ if( do_ite && i>0 ){
+ setEntailedCond( children[0], i==1, currCond, new_cond );
+ cache.clear();
+ }
+ bool newHasPol;
+ bool newPol;
+ QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
+ Node nn = computeProcessTerms( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+ if( body.getKind()==ITE ){
+ if( i==0 ){
+ int res = getEntailedCond( nn, currCond );
+ if( res==1 ){
+ ret = computeProcessTerms( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+ break;
+ }else if( res==-1 ){
+ ret = computeProcessTerms( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+ break;
+ }
+ }else{
+ for( unsigned j=0; j<new_cond.size(); j++ ){
+ currCond.erase( new_cond[j] );
+ }
+ cache.clear();
+ }
+ }
+ children.push_back( nn );
+ changed = changed || nn!=body[i];
+ }
+ if( ret.isNull() && changed ){
+ if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.insert( children.begin(), body.getOperator() );
+ }
+ ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
+ }else{
+ ret = body;
}
- body = NodeManager::currentNM()->mkNode( body.getKind(), children );
+ cache[body] = ret;
}
- 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;
+ iti = icache.find( ret );
+ if( iti!=icache.end() ){
+ return iti->second;
+ }else{
+ Node prev = ret;
+ if( ret.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){
+ for( size_t i=0; i<2; i++ ){
+ if( ret[i].getKind()==ITE ){
+ Node no = i==0 ? ret[1] : ret[0];
+ if( no.getKind()!=ITE ){
+ bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL;
+ std::vector< Node > children;
+ children.push_back( ret[i][0] );
+ for( size_t j=1; j<=2; j++ ){
+ //check if it rewrites to a constant
+ Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, ret[i][j] );
+ nn = Rewriter::rewrite( nn );
+ children.push_back( nn );
+ if( nn.isConst() ){
+ doRewrite = true;
+ }
+ }
+ if( doRewrite ){
+ ret = NodeManager::currentNM()->mkNode( ITE, children );
+ break;
}
}
- if( doRewrite ){
- return NodeManager::currentNM()->mkNode( ITE, children );
+ }
+ }
+ }else if( ret.getKind()==INTS_DIVISION_TOTAL || ret.getKind()==INTS_MODULUS_TOTAL ){
+ Node num = ret[0];
+ Node den = ret[1];
+ if(den.isConst()) {
+ const Rational& rat = den.getConst<Rational>();
+ Assert(!num.isConst());
+ if(rat != 0) {
+ Node intVar = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+ new_vars.push_back( intVar );
+ Node cond;
+ if(rat > 0) {
+ cond = NodeManager::currentNM()->mkNode(kind::AND,
+ NodeManager::currentNM()->mkNode(kind::LEQ, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar), num),
+ NodeManager::currentNM()->mkNode(kind::LT, num,
+ NodeManager::currentNM()->mkNode(kind::MULT, den, NodeManager::currentNM()->mkNode(kind::PLUS, intVar, NodeManager::currentNM()->mkConst(Rational(1))))));
+ } else {
+ cond = NodeManager::currentNM()->mkNode(kind::AND,
+ NodeManager::currentNM()->mkNode(kind::LEQ, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar), num),
+ NodeManager::currentNM()->mkNode(kind::LT, num,
+ NodeManager::currentNM()->mkNode(kind::MULT, den, NodeManager::currentNM()->mkNode(kind::PLUS, intVar, NodeManager::currentNM()->mkConst(Rational(-1))))));
}
+ new_conds.push_back( cond.negate() );
+ if( ret.getKind()==INTS_DIVISION_TOTAL ){
+ ret = intVar;
+ }else{
+ ret = NodeManager::currentNM()->mkNode(kind::MINUS, num, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar));
+ }
+ }
+ }
+ }else if( ret.getKind()==TO_INTEGER || ret.getKind()==IS_INTEGER ){
+ Node intVar = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+ new_vars.push_back( intVar );
+ new_conds.push_back(NodeManager::currentNM()->mkNode(kind::AND,
+ NodeManager::currentNM()->mkNode(kind::LT,
+ NodeManager::currentNM()->mkNode(kind::MINUS, ret[0], NodeManager::currentNM()->mkConst(Rational(1))), intVar),
+ NodeManager::currentNM()->mkNode(kind::LEQ, intVar, ret[0])).negate());
+ if( ret.getKind()==TO_INTEGER ){
+ ret = intVar;
+ }else{
+ ret = ret[0].eqNode( intVar );
+ }
+ }
+ icache[prev] = ret;
+ return ret;
+ }
+}
+
+Node QuantifiersRewriter::computeProcessIte( Node body ){
+ if( body.getKind()==ITE ){
+ if( options::iteDtTesterSplitQuant() ){
+ Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl;
+ std::map< Node, Node > pcons;
+ std::map< Node, std::map< int, Node > > ncons;
+ std::vector< Node > conj;
+ computeDtTesterIteSplit( body, pcons, ncons, conj );
+ Assert( !conj.empty() );
+ if( conj.size()>1 ){
+ Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl;
+ for( unsigned i=0; i<conj.size(); i++ ){
+ Trace("quantifiers-rewrite-ite") << " " << conj[i] << std::endl;
}
+ return NodeManager::currentNM()->mkNode( AND, conj );
}
}
- }else if( body.getKind()==ITE ){
- if( body.getType().isBoolean() && hasPol && options::iteCondVarSplitQuant() ){
+ if( options::iteCondVarSplitQuant() ){
Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl;
+ bool do_split = false;
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->first[i].getKind()==BOUND_VARIABLE ){
unsigned j = i==0 ? 1 : 0;
if( !TermDb::containsTerm( it->first[j], it->first[i] ) ){
- vars.push_back( it->first[i] );
- subs.push_back( it->first[j] );
+ do_split = true;
break;
}
}
}
}
}
+ if( do_split ){
+ break;
+ }
}
- if( !vars.empty() ){
+ if( do_split ){
//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() );
return body;
}
-Node QuantifiersRewriter::computeProcessIte2( Node body ){
- if( body.getKind()==ITE ){
- if( options::iteDtTesterSplitQuant() ){
- Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl;
- std::map< Node, Node > pcons;
- std::map< Node, std::map< int, Node > > ncons;
- std::vector< Node > conj;
- computeDtTesterIteSplit( body, pcons, ncons, conj );
- Assert( !conj.empty() );
- if( conj.size()>1 ){
- Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl;
- for( unsigned i=0; i<conj.size(); i++ ){
- Trace("quantifiers-rewrite-ite") << " " << conj[i] << std::endl;
- }
- return NodeManager::currentNM()->mkNode( AND, conj );
- }
- }
- }
- return body;
-}
-
Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl;
//Notice() << " " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
if( it->first.getKind()==EQUAL ){
if( it->second && options::varElimQuant() ){
+ TypeNode types[2];
+ for( int i=0; i<2; i++ ){
+ types[i] = it->first[i].getType();
+ }
for( int i=0; i<2; i++ ){
- int j = i==0 ? 1 : 0;
std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[i] );
if( ita!=args.end() ){
- if( !TermDb::containsTerm( it->first[j], it->first[i] ) ){
+ if( !TermDb::containsTerm( it->first[1-i], it->first[i] ) && types[1-i].isSubtypeOf( types[i] ) ){
vars.push_back( it->first[i] );
- subs.push_back( it->first[j] );
+ subs.push_back( it->first[1-i] );
args.erase( ita );
break;
}
return options::aggressiveMiniscopeQuant();
}else if( computeOption==COMPUTE_NNF ){
return options::nnfQuant();
- }else if( computeOption==COMPUTE_PROCESS_ITE ){
- //always eliminate redundant conditions in ITE
+ }else if( computeOption==COMPUTE_PROCESS_TERMS ){
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_PROCESS_ITE ){
+ return options::iteDtTesterSplitQuant() || options::iteCondVarSplitQuant();
}else if( computeOption==COMPUTE_PRENEX ){
return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
}else if( computeOption==COMPUTE_VAR_ELIMINATION ){
return computeAggressiveMiniscoping( args, n );
}else if( computeOption==COMPUTE_NNF ){
n = computeNNF( n );
- }else if( computeOption==COMPUTE_PROCESS_ITE ){
+ }else if( computeOption==COMPUTE_PROCESS_TERMS ){
std::map< Node, bool > curr_cond;
- n = computeProcessIte( n, true, true, curr_cond );
- }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){
- n = computeProcessIte2( n );
+ std::map< Node, Node > cache;
+ std::map< Node, Node > icache;
+ std::vector< Node > new_conds;
+ n = computeProcessTerms( n, true, true, curr_cond, 0, cache, icache, args, new_conds );
+ if( !new_conds.empty() ){
+ new_conds.push_back( n );
+ n = NodeManager::currentNM()->mkNode( OR, new_conds );
+ }
+ }else if( computeOption==COMPUTE_PROCESS_ITE ){
+ n = computeProcessIte( n );
}else if( computeOption==COMPUTE_PRENEX ){
n = computePrenex( n, args, true );
}else if( computeOption==COMPUTE_VAR_ELIMINATION ){
projects / cvc5.git / commitdiff