diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-21 10:07:12 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-21 10:07:19 +0200 |
commit | fb746fdd4e60e7d166b0fa1e5788bea925d22ee7 (patch) | |
tree | 1a8b8dc8c2b4f57352ab10365e2b2765c06285c9 /src/theory | |
parent | 60f6d09d7ad9e37f5a23e6a2b0e47a7b0e47df81 (diff) |
Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. Enable redundant ITE branch elimination in quantifiers rewriter.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 318 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 41 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 15 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 21 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 159 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 7 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 1 |
10 files changed, 317 insertions, 258 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 9d49f3d72..bf0168c64 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -74,10 +74,15 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< 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 ); @@ -169,38 +174,37 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } 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; } } } @@ -264,97 +268,111 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< //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; } } } @@ -371,13 +389,11 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< 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 ); @@ -459,7 +475,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< 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; @@ -474,10 +490,10 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< 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 << " * "; } @@ -540,11 +556,6 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, std:: 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() ){ @@ -829,13 +840,13 @@ void CegInstantiator::processAssertions() { 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++ ){ @@ -857,6 +868,16 @@ void CegInstantiator::processAssertions() { 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++ ){ Node s = lit[k]; @@ -881,6 +902,7 @@ void CegInstantiator::processAssertions() { } } } + */ } } } @@ -910,7 +932,7 @@ void CegInstantiator::processAssertions() { 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() ){ @@ -935,21 +957,21 @@ void CegInstantiator::processAssertions() { 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]; @@ -979,6 +1001,7 @@ void CegInstantiator::processAssertions() { 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; @@ -990,7 +1013,7 @@ void CegInstantiator::processAssertions() { 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; @@ -1006,7 +1029,7 @@ void CegInstantiator::processAssertions() { 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; @@ -1016,7 +1039,7 @@ void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, st nr = Rewriter::rewrite( nr ); subs_rhs[i] = nr; } - + subs_lhs.push_back( l ); subs_rhs.push_back( r ); } @@ -1369,21 +1392,7 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { 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(); @@ -1434,14 +1443,17 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { } } -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; } } @@ -1453,5 +1465,3 @@ void InstStrategyCegqi::setAuxiliaryVariables( Node q, std::vector< Node >& vars - - diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 64303e1f3..f7cb290b2 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -88,6 +88,8 @@ public: 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(); }; @@ -153,7 +155,6 @@ class InstStrategyCegqi : public InstStrategy { 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; @@ -170,8 +171,8 @@ public: /** 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 ); }; } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index b12c822ef..3dad74044 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -108,18 +108,37 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ 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; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index b573ebd67..66de51f39 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -17,7 +17,8 @@ option miniscopeQuant --miniscope-quant bool :default true :read-write # ( 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. @@ -37,11 +38,8 @@ option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default fal # 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 @@ -51,10 +49,8 @@ option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default 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 @@ -246,8 +242,11 @@ option cbqiSat --cbqi-sat bool :read-write :default true 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 diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 2c65b62b3..938245871 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -313,15 +313,20 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int } 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; } } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index d6cbe386c..c32aeeb78 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -415,89 +415,105 @@ void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node } } -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 ){ @@ -1140,7 +1156,9 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption }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 ){ @@ -1182,7 +1200,8 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp }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 ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index d01677171..7db80c84b 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -46,7 +46,7 @@ private: 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 ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 13c408d85..d1a268950 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -329,6 +329,10 @@ void QuantifiersEngine::check( Theory::Effort e ){ 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; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 96a99763d..b28a73b9d 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -798,9 +798,6 @@ private: /** 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); @@ -834,6 +831,10 @@ public: 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: diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index c15074d8c..d913cb76a 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1047,6 +1047,7 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ //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 |