From aaf1bbbdc6e42910e07db64441885ee3476d86df Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 26 Oct 2015 11:26:13 +0100 Subject: [PATCH] Extend counterexample-guided instantiation to extended theory of Int/Real, mixed Int/Real. Bug fixes. Updates to quantifiers rewriter. --- src/theory/quantifiers/ceg_instantiator.cpp | 61 +++- src/theory/quantifiers/ceg_instantiator.h | 8 +- .../quantifiers/inst_strategy_e_matching.cpp | 4 - .../quantifiers/instantiation_engine.cpp | 14 +- src/theory/quantifiers/instantiation_engine.h | 3 +- .../quantifiers/quantifiers_rewriter.cpp | 339 +++++++++++------- src/theory/quantifiers/quantifiers_rewriter.h | 9 +- src/theory/quantifiers_engine.cpp | 15 +- src/theory/quantifiers_engine.h | 2 + test/regress/regress0/quantifiers/Makefile.am | 12 +- .../quantifiers/array-unsat-simp3.smt2.expect | 1 - test/regress/regress0/quantifiers/bug291.smt2 | 1 + .../regress0/quantifiers/bug291.smt2.expect | 3 +- test/regress/regress0/quantifiers/floor.smt2 | 4 + test/regress/regress0/quantifiers/is-int.smt2 | 4 + 15 files changed, 309 insertions(+), 171 deletions(-) delete mode 100644 test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect create mode 100755 test/regress/regress0/quantifiers/floor.smt2 create mode 100755 test/regress/regress0/quantifiers/is-int.smt2 diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 90639d68c..c7bf61eab 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -125,7 +125,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve 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 @@ -171,7 +171,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve 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 ); } @@ -210,7 +210,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve 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 ){ @@ -325,7 +325,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve //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() ){ @@ -470,6 +470,20 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve } 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(); + 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 ); @@ -607,7 +621,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve 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() ){ @@ -624,7 +638,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve 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; @@ -643,7 +657,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve int rr = upper_first ? (1-r) : r; for( unsigned j=0; j& su } } -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 ) ); @@ -935,10 +949,26 @@ Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std: 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; imkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/coeff[i].getConst() ) ) )); + }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 ) ){ @@ -999,8 +1029,12 @@ Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std: } } -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 @@ -1008,6 +1042,7 @@ Node CegInstantiator::getModelBasedProjectionValue( Node t, bool isLower, Node c 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() ){ @@ -1019,7 +1054,7 @@ Node CegInstantiator::getModelBasedProjectionValue( Node t, bool isLower, Node c 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 ); diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 7dd6ef12b..38bb12e5b 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -107,12 +107,12 @@ private: unsigned j, std::map< Node, Node >& cons ); bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ); Node constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons ); - Node applySubstitution( Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) { - return applySubstitution( n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff ); + Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) { + return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff ); } - Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, + Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ); - Node getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta, + Node getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ); void processAssertions(); void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index eb1ce56ef..9330bac7e 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -122,8 +122,6 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){ } if( usable ){ Trace("user-pat") << "Add user pattern: " << pat << " for " << f << std::endl; - //extend to literal matching - d_quantEngine->getPhaseReqTerms( f, nodes ); //check match option int matchOption = 0; if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){ @@ -260,8 +258,6 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor } Trace("auto-gen-trigger") << std::endl; } - //extend to literal matching (if applicable) - d_quantEngine->getPhaseReqTerms( f, patTermsF ); //sort into single/multi triggers std::map< Node, std::vector< Node > > varContains; d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains ); diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index b32f27d8f..f5333dbe1 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -56,7 +56,7 @@ void InstantiationEngine::finishInit(){ d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine ); d_instStrategies.push_back( d_i_ag ); } - + //counterexample-based quantifier instantiation if( options::cbqi() ){ if( options::cbqiSplx() ){ @@ -164,7 +164,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ - if( !options::cbqi() || !TermDb::hasInstConstAttr(q) ){ + if( !options::cbqi() || !TermDb::hasInstConstAttr( q ) ){ quantActive = true; } d_quants.push_back( q ); @@ -198,6 +198,15 @@ bool InstantiationEngine::checkComplete() { } } + +void InstantiationEngine::preRegisterQuantifier( Node q ) { + if( options::cbqi() ){ + if( d_i_cbqi->doCbqi( q ) ){ + d_quantEngine->setOwner( q, this ); + } + } +} + void InstantiationEngine::registerQuantifier( Node f ){ if( d_quantEngine->hasOwnership( f, this ) ){ for( unsigned i=0; i& 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; i1 ); - if( pol ){ - for( unsigned i=0; imkNode( 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() ){ @@ -507,74 +463,213 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){ 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 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; i1 ); + if( pol ){ + for( unsigned i=0; imkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] ); + addEntailedCond( t, false, currCond, new_cond ); + } } }else{ - for( unsigned j=0; jmkNode( 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 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; jmkNode( 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(); + 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; imkNode( 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; @@ -584,16 +679,18 @@ Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol, s 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() ); @@ -610,27 +707,6 @@ Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol, s 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; imkNode( 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; @@ -641,13 +717,16 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& //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; } @@ -1201,12 +1280,11 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption 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 ){ @@ -1241,11 +1319,18 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp 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 ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 828099984..98a83b7de 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -44,8 +44,11 @@ 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, std::map< Node, bool >& currCond ); - static Node computeProcessIte2( Node body ); + //cache is dependent upon currCond, icache is not, new_conds are negated conditions + static Node 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 ); + static Node computeProcessIte( 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 ); static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); @@ -56,8 +59,8 @@ private: COMPUTE_MINISCOPING, COMPUTE_AGGRESSIVE_MINISCOPING, COMPUTE_NNF, + COMPUTE_PROCESS_TERMS, COMPUTE_PROCESS_ITE, - COMPUTE_PROCESS_ITE_2, COMPUTE_PRENEX, COMPUTE_VAR_ELIMINATION, //COMPUTE_FLATTEN_ARGS_UF, diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 28a4d4c6b..913d9b0c6 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -128,7 +128,7 @@ d_presolve_cache_wic(u){ d_sg_gen = NULL; } //maintain invariant : either InstantiationEngine or ModelEngine must be in d_modules - if( !options::finiteModelFind() || options::fmfInstEngine() ){ + if( !options::finiteModelFind() || options::fmfInstEngine() || options::cbqi() ){ d_inst_engine = new quantifiers::InstantiationEngine( this ); d_modules.push_back( d_inst_engine ); if( options::cbqi() && options::cbqiModel() ){ @@ -201,7 +201,7 @@ d_presolve_cache_wic(u){ }else{ d_rel_dom = NULL; } - + if( needsBuilder ){ Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl; if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || @@ -344,7 +344,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } } - + d_hasAddedLemma = false; bool setIncomplete = false; if( e==Theory::EFFORT_LAST_CALL ){ @@ -355,7 +355,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } bool usedModelBuilder = false; - + Trace("quant-engine-debug") << "Quantifiers Engine call to check, level = " << e << std::endl; if( needsCheck ){ Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl; @@ -479,7 +479,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ }else{ Trace("quant-engine") << "Quantifiers Engine does not need check." << std::endl; } - + //SAT case if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){ if( options::produceModels() ){ @@ -554,6 +554,9 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ //make instantiation constants for f d_term_db->makeInstantiationConstantsFor( f ); d_term_db->computeAttributes( f ); + for( unsigned i=0; ipreRegisterQuantifier( f ); + } QuantifiersModule * qm = getOwner( f ); if( qm!=NULL ){ Trace("quant") << " Owner : " << qm->identify() << std::endl; @@ -563,7 +566,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ d_quant_rel->registerQuantifier( f ); } //register with each module - for( int i=0; i<(int)d_modules.size(); i++ ){ + for( unsigned i=0; iregisterQuantifier( f ); } Node ceBody = d_term_db->getInstConstantBody( f ); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 30c4dabdf..76fb920bb 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -68,6 +68,8 @@ public: /* check was complete (e.g. no lemmas implies a model) */ virtual bool checkComplete() { return false; } /* Called for new quantifiers */ + virtual void preRegisterQuantifier( Node q ) {} + /* Called for new quantifiers after owners are finalized */ virtual void registerQuantifier( Node q ) = 0; virtual void assertNode( Node n ) = 0; virtual void propagate( Theory::Effort level ){} diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 0592bdeab..73fa07bf9 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -22,7 +22,6 @@ TESTS = \ bug269.smt2 \ bug290.smt2 \ bug291.smt2 \ - ex3.smt2 \ Arrays_Q1-noinfer.smt2 \ bignum_quant.smt2 \ bug269.smt2 \ @@ -55,8 +54,10 @@ TESTS = \ RND-small.smt2 \ clock-3.smt2 \ 006-cbqi-ite.smt2 \ - cbqi-lia-dt-simp.smt2 - + cbqi-lia-dt-simp.smt2 \ + is-int.smt2 \ + floor.smt2 \ + array-unsat-simp3.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine @@ -64,17 +65,12 @@ TESTS = \ # removed because they take more than 20s -# ex1.smt2 \ -# ex6.smt2 \ -# ex7.smt2 \ -# array-unsat-simp3.smt2are # javafe.ast.ArrayInit.35.smt2 \ # javafe.ast.StandardPrettyPrint.319.smt2 \ # javafe.ast.StmtVec.009.smt2 \ # javafe.ast.WhileStmt.447.smt2 \ # javafe.tc.CheckCompilationUnit.001.smt2 \ # javafe.tc.FlowInsensitiveChecks.682.smt2 \ -# array-unsat-simp3.smt2 \ # clock-10.smt2 # diff --git a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect deleted file mode 100644 index b4ea773f0..000000000 --- a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect +++ /dev/null @@ -1 +0,0 @@ -% EXPECT: unsat diff --git a/test/regress/regress0/quantifiers/bug291.smt2 b/test/regress/regress0/quantifiers/bug291.smt2 index dbc230599..b39e415a8 100644 --- a/test/regress/regress0/quantifiers/bug291.smt2 +++ b/test/regress/regress0/quantifiers/bug291.smt2 @@ -10,4 +10,5 @@ (declare-fun store2 (Int) Int) (assert (forall ((?A Int) (?o Int) (?f Int) (?p Int) (?g Int) (?v Int)) (=> (not (= ?o ?p)) (= (select2 (store2 ?A)) (select2 ?A))))) (check-sat) +(get-info :reason-unknown) (exit) diff --git a/test/regress/regress0/quantifiers/bug291.smt2.expect b/test/regress/regress0/quantifiers/bug291.smt2.expect index 7856f23b4..f97ed61b6 100644 --- a/test/regress/regress0/quantifiers/bug291.smt2.expect +++ b/test/regress/regress0/quantifiers/bug291.smt2.expect @@ -1 +1,2 @@ -% EXPECT: sat +% EXPECT: unknown +% EXPECT: (:reason-unknown incomplete) \ No newline at end of file diff --git a/test/regress/regress0/quantifiers/floor.smt2 b/test/regress/regress0/quantifiers/floor.smt2 new file mode 100755 index 000000000..cb20c1056 --- /dev/null +++ b/test/regress/regress0/quantifiers/floor.smt2 @@ -0,0 +1,4 @@ +(set-logic LIRA) +(set-info :status unsat) +(assert (forall ((X Real)) (not (>= (+ (to_int (* 2 X)) (* (- 2) (to_int X))) 1)) )) +(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/quantifiers/is-int.smt2 b/test/regress/regress0/quantifiers/is-int.smt2 new file mode 100755 index 000000000..07e8dd246 --- /dev/null +++ b/test/regress/regress0/quantifiers/is-int.smt2 @@ -0,0 +1,4 @@ +(set-logic LIRA) +(set-info :status unsat) +(assert (forall ((X Real) (Y Real)) (or (not (is_int X)) (not (>= (+ X (* (- (/ 2 3)) Y)) (- (/ 1 6)))) (not (>= (+ (* (- 1) X) (* (- (/ 1 4)) Y)) (- (/ 61 8)))) (not (>= (+ (* (- 1) X) (* (/ 5 2) Y)) 13))) )) +(check-sat) \ No newline at end of file -- 2.30.2