From 5bc200446b4165814db47e6e3639972af31ad0a6 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 31 Oct 2015 10:00:52 +0100 Subject: [PATCH] Improvements to handling of mixed Int/Real quantifiers. --- .../quantifiers/candidate_generator.cpp | 4 +- src/theory/quantifiers/ceg_instantiator.cpp | 405 +++++++++++------- src/theory/quantifiers/ceg_instantiator.h | 17 +- .../quantifiers/inst_match_generator.cpp | 66 +-- src/theory/quantifiers/inst_match_generator.h | 41 +- .../quantifiers/quant_conflict_find.cpp | 2 +- src/theory/quantifiers/quant_util.cpp | 18 + src/theory/quantifiers/quant_util.h | 1 + src/theory/quantifiers/term_database.cpp | 13 + src/theory/quantifiers/term_database.h | 2 + src/theory/quantifiers/trigger.cpp | 4 +- src/theory/quantifiers/trigger.h | 16 - src/theory/quantifiers_engine.cpp | 14 +- src/theory/quantifiers_engine.h | 2 +- test/regress/regress0/quantifiers/Makefile.am | 5 +- .../regress0/quantifiers/mix-coeff.smt2 | 4 + .../regress0/quantifiers/mix-match.smt2 | 10 + .../regress0/quantifiers/mix-simp.smt2 | 4 + 18 files changed, 389 insertions(+), 239 deletions(-) create mode 100644 test/regress/regress0/quantifiers/mix-coeff.smt2 create mode 100644 test/regress/regress0/quantifiers/mix-match.smt2 create mode 100644 test/regress/regress0/quantifiers/mix-simp.smt2 diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 4619d74e5..0e7b02b53 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -142,7 +142,7 @@ Node CandidateGeneratorQELitEq::getNextCandidate(){ while( !d_eq.isFinished() ){ Node n = (*d_eq); ++d_eq; - if( n.getType().isSubtypeOf( d_match_pattern[0].getType() ) ){ + if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){ //an equivalence class with the same type as the pattern, return reflexive equality return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n ); } @@ -199,7 +199,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() { while( !d_eq.isFinished() ){ TNode n = (*d_eq); ++d_eq; - if( n.getType().isSubtypeOf( d_match_pattern_type ) ){ + if( n.getType().isComparableTo( d_match_pattern_type ) ){ TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n ); if( !nh.isNull() ){ if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){ diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index c7bf61eab..5ae8905d1 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -285,13 +285,13 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve //[3] directly look at assertions Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl; - Node vts_sym[2]; - vts_sym[0] = d_qe->getTermDatabase()->getVtsInfinity( pvtn, false, false ); - vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta( false, false ); + d_vts_sym[0] = d_qe->getTermDatabase()->getVtsInfinity( pvtn, false, false ); + d_vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta( false, false ); std::vector< Node > mbp_bounds[2]; std::vector< Node > mbp_coeff[2]; std::vector< Node > mbp_vts_coeff[2][2]; std::vector< Node > mbp_lit[2]; + //std::vector< MbpBounds > mbp_bounds[2]; unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2; for( unsigned r=0; rgetTermDatabase()->containsVtsInfinity( atom_lhs ) ){ Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl; Trace("cbqi-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( satom, msum ) ){ - if( Trace.isOn("cbqi-inst-debug") ){ - Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" ); - } - //get the coefficient of infinity and remove it from msum - Node vts_coeff[2]; - for( unsigned t=0; t<2; t++ ){ - if( !vts_sym[t].isNull() ){ - std::map< Node, Node >::iterator itminf = msum.find( vts_sym[t] ); - if( itminf!=msum.end() ){ - vts_coeff[t] = itminf->second; - if( vts_coeff[t].isNull() ){ - vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) ); - } - //negate if coefficient on variable is positive - std::map< Node, Node >::iterator itv = msum.find( pv ); - if( itv!=msum.end() ){ - //multiply by the coefficient we will isolate for - if( itv->second.isNull() ){ - vts_coeff[t] = QuantArith::negate(vts_coeff[t]); - }else{ - if( !pvtn.isInteger() ){ - vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst() ), vts_coeff[t] ); - vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] ); - }else if( itv->second.getConst().sgn()==1 ){ - vts_coeff[t] = QuantArith::negate(vts_coeff[t]); - } - } - } - Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; - msum.erase( vts_sym[t] ); - } - } - } - - Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl; - Node vatom; - //isolate pv in the inequality - int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true ); - if( ires!=0 ){ - Trace("cbqi-inst-debug") << "...isolated atom " << vatom << "." << std::endl; - Node val = vatom[ ires==1 ? 1 : 0 ]; - Node pvm = vatom[ ires==1 ? 0 : 1 ]; - //get monomial - Node veq_c; - if( pvm!=pv ){ - Node veq_v; - if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ - Assert( veq_v==pv ); - } - } - - //disequalities are either strict upper or lower bounds - unsigned rmax = ( atom.getKind()==GEQ && options::cbqiModel() ) ? 1 : 2; - for( unsigned r=0; rmkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else{ - Assert( pvtn.isReal() ); - //now is strict inequality - uires = uires*2; - } - } - }else{ - bool is_upper = ( r==0 ); - if( options::cbqiModel() ){ - // disequality is a disjunction : only consider the bound in the direction of the model - //first check if there is an infinity... - if( !vts_coeff[0].isNull() ){ - //coefficient or val won't make a difference, just compare with zero - Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff[0] << std::endl; - Assert( vts_coeff[0].isConst() ); - is_upper = ( vts_coeff[0].getConst().sgn()==1 ); - }else{ - Node rhs_value = getModelValue( val ); - Node lhs_value = pv_value; - if( !veq_c.isNull() ){ - lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c ); - lhs_value = Rewriter::rewrite( lhs_value ); - } - Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl; - Assert( lhs_value!=rhs_value ); - Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value ); - cmp = Rewriter::rewrite( cmp ); - Assert( cmp.isConst() ); - is_upper = ( cmp!=d_true ); - } - } - Assert( atom.getKind()==EQUAL && !pol ); + Node vts_coeff_inf; + Node vts_coeff_delta; + Node val; + Node veq_c; + //isolate pv in the inequality + int ires = isolate( pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta ); + if( ires!=0 ){ + //disequalities are either strict upper or lower bounds + unsigned rmax = ( atom.getKind()==GEQ && options::cbqiModel() ) ? 1 : 2; + for( unsigned r=0; rmkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); uval = Rewriter::rewrite( uval ); }else{ Assert( pvtn.isReal() ); - uires = is_upper ? -2 : 2; + //now is strict inequality + uires = uires*2; } } - Trace("cbqi-bound-inf") << "From " << lit << ", got : "; - if( !veq_c.isNull() ){ - Trace("cbqi-bound-inf") << veq_c << " * "; - } - Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl; - //take into account delta - if( d_use_vts_delta && ( uires==2 || uires==-2 ) ){ - if( options::cbqiModel() ){ - Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) ); - if( vts_coeff[1].isNull() ){ - vts_coeff[1] = delta_coeff; - }else{ - vts_coeff[1] = NodeManager::currentNM()->mkNode( PLUS, vts_coeff[1], delta_coeff ); - vts_coeff[1] = Rewriter::rewrite( vts_coeff[1] ); - } + }else{ + bool is_upper = ( r==0 ); + if( options::cbqiModel() ){ + // disequality is a disjunction : only consider the bound in the direction of the model + //first check if there is an infinity... + if( !vts_coeff_inf.isNull() ){ + //coefficient or val won't make a difference, just compare with zero + Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl; + Assert( vts_coeff_inf.isConst() ); + is_upper = ( vts_coeff_inf.getConst().sgn()==1 ); }else{ - Node delta = d_qe->getTermDatabase()->getVtsDelta(); - uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta ); - uval = Rewriter::rewrite( uval ); + Node rhs_value = getModelValue( val ); + Node lhs_value = pv_value; + if( !veq_c.isNull() ){ + lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c ); + lhs_value = Rewriter::rewrite( lhs_value ); + } + Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl; + Assert( lhs_value!=rhs_value ); + Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value ); + cmp = Rewriter::rewrite( cmp ); + Assert( cmp.isConst() ); + is_upper = ( cmp!=d_true ); } } + Assert( atom.getKind()==EQUAL && !pol ); + if( pvtn.isInteger() ){ + uires = is_upper ? -1 : 1; + uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else{ + Assert( pvtn.isReal() ); + uires = is_upper ? -2 : 2; + } + } + Trace("cbqi-bound-inf") << "From " << lit << ", got : "; + if( !veq_c.isNull() ){ + Trace("cbqi-bound-inf") << veq_c << " * "; + } + Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl; + //take into account delta + if( d_use_vts_delta && ( uires==2 || uires==-2 ) ){ if( options::cbqiModel() ){ - //just store bounds, will choose based on tighest bound - if( pvtn.isInteger() && !veq_c.isNull() && !veq_c.getType().isInteger() ){ - Trace("cbqi-bound2") << "Non-integer coefficient : " << veq_c << " for " << pv << std::endl; - Assert( veq_c.isConst() ); - //multiply everything by denominator of coefficient - Rational r = veq_c.getConst(); - Node den = NodeManager::currentNM()->mkConst( Rational(r.getDenominator()) ); - uval = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, den, uval ) ); - veq_c = NodeManager::currentNM()->mkConst( Rational(r.getNumerator()) ); - for( unsigned t=0; t<2; t++ ){ - if( !vts_coeff[t].isNull() ){ - vts_coeff[t] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, den, vts_coeff[t] ) ); - } - } - } - unsigned index = uires>0 ? 0 : 1; - mbp_bounds[index].push_back( uval ); - mbp_coeff[index].push_back( veq_c ); - for( unsigned t=0; t<2; t++ ){ - mbp_vts_coeff[index][t].push_back( vts_coeff[t] ); + Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) ); + if( vts_coeff_delta.isNull() ){ + vts_coeff_delta = delta_coeff; + }else{ + vts_coeff_delta = NodeManager::currentNM()->mkNode( PLUS, vts_coeff_delta, delta_coeff ); + vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta ); } - mbp_lit[index].push_back( lit ); }else{ - //try this bound - if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){ - subs_proc[uval][veq_c] = true; - if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } + Node delta = d_qe->getTermDatabase()->getVtsDelta(); + uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta ); + uval = Rewriter::rewrite( uval ); + } + } + if( options::cbqiModel() ){ + //just store bounds, will choose based on tighest bound + unsigned index = uires>0 ? 0 : 1; + mbp_bounds[index].push_back( uval ); + mbp_coeff[index].push_back( veq_c ); + for( unsigned t=0; t<2; t++ ){ + mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta ); + } + mbp_lit[index].push_back( lit ); + }else{ + //try this bound + if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){ + subs_proc[uval][veq_c] = true; + if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + return true; } } } @@ -622,7 +560,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve best_used[rr] = (unsigned)best; Node val = mbp_bounds[rr][best]; val = getModelBasedProjectionValue( pv, val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta, - mbp_vts_coeff[rr][0][best], vts_sym[0], mbp_vts_coeff[rr][1][best], vts_sym[1] ); + mbp_vts_coeff[rr][0][best], mbp_vts_coeff[rr][1][best] ); if( !val.isNull() ){ if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){ subs_proc[val][mbp_coeff[rr][best]] = true; @@ -638,7 +576,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( pv, val, true, c, pv_value, d_zero, theta, Node::null(), vts_sym[0], Node::null(), vts_sym[1] ); + val = getModelBasedProjectionValue( pv, val, true, c, pv_value, d_zero, theta, Node::null(), Node::null() ); if( !val.isNull() ){ if( subs_proc[val].find( c )==subs_proc[val].end() ){ subs_proc[val][c] = true; @@ -658,7 +596,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve for( unsigned j=0; j& subs, std::vector< subs.push_back( n ); } } + if( !d_var_order_index.empty() ){ + std::vector< Node > subs_orig; + subs_orig.insert( subs_orig.end(), subs.begin(), subs.end() ); + subs.clear(); + for( unsigned i=0; iaddInstantiation( subs ); #ifdef MBP_STRICT_ASSERTIONS Assert( ret ); @@ -1029,12 +975,13 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node } } -Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, - Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ) { +Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) { + /* if( e.getType().isInteger() && !t.getType().isInteger() ){ //TODO : round up/down this bound? return Node::null(); } + */ Node val = t; Trace("cbqi-bound2") << "Value : " << val << std::endl; //add rho value @@ -1056,6 +1003,10 @@ Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower } if( !new_theta.isNull() && e.getType().isInteger() ){ Node rho; + //if( !mt.getType().isInteger() ){ + //round up/down + //mt = NodeManager::currentNM()->mkNode( + //} if( isLower ){ rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt ); }else{ @@ -1073,16 +1024,16 @@ Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower Trace("cbqi-bound2") << "(after rho) : " << val << std::endl; } if( !inf_coeff.isNull() ){ - Assert( !vts_inf.isNull() ); - val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, vts_inf ) ); + Assert( !d_vts_sym[0].isNull() ); + val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, d_vts_sym[0] ) ); val = Rewriter::rewrite( val ); } if( !delta_coeff.isNull() ){ //create delta here if necessary - if( vts_delta.isNull() ){ - vts_delta = d_qe->getTermDatabase()->getVtsDelta(); + if( d_vts_sym[1].isNull() ){ + d_vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta(); } - val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, vts_delta ) ); + val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, d_vts_sym[1] ) ); val = Rewriter::rewrite( val ); } return val; @@ -1399,9 +1350,47 @@ void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) } } +struct sortCegVarOrder { + bool operator() (Node i, Node j) { + TypeNode it = i.getType(); + TypeNode jt = j.getType(); + return ( it!=jt && jt.isSubtypeOf( it ) ) || ( it==jt && i& lems, std::vector< Node >& ce_vars ) { Assert( d_vars.empty() ); d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() ); + + //determine variable order: must do Reals before Ints + if( !d_vars.empty() ){ + TypeNode tn0 = d_vars[0].getType(); + bool doSort = false; + std::map< Node, unsigned > voo; + for( unsigned i=0; igetTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap); Assert( d_aux_vars.empty() ); @@ -1435,3 +1424,103 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st collectCeAtoms( lems[i], visited ); } } + +//this isolates the monomial sum into solved form (pv k t), ensures t is Int if pv is Int, and t does not contain vts symbols +int CegInstantiator::isolate( Node pv, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta ) { + int ires = 0; + Trace("cbqi-inst-debug") << "isolate for " << pv << " in " << atom << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( atom, msum ) ){ + Trace("cbqi-inst-debug") << "got monomial sum: " << std::endl; + if( Trace.isOn("cbqi-inst-debug") ){ + QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" ); + } + TypeNode pvtn = pv.getType(); + //remove vts symbols from polynomial + Node vts_coeff[2]; + for( unsigned t=0; t<2; t++ ){ + if( !d_vts_sym[t].isNull() ){ + std::map< Node, Node >::iterator itminf = msum.find( d_vts_sym[t] ); + if( itminf!=msum.end() ){ + vts_coeff[t] = itminf->second; + if( vts_coeff[t].isNull() ){ + vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) ); + } + //negate if coefficient on variable is positive + std::map< Node, Node >::iterator itv = msum.find( pv ); + if( itv!=msum.end() ){ + //multiply by the coefficient we will isolate for + if( itv->second.isNull() ){ + vts_coeff[t] = QuantArith::negate(vts_coeff[t]); + }else{ + if( !pvtn.isInteger() ){ + vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst() ), vts_coeff[t] ); + vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] ); + }else if( itv->second.getConst().sgn()==1 ){ + vts_coeff[t] = QuantArith::negate(vts_coeff[t]); + } + } + } + Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; + msum.erase( d_vts_sym[t] ); + } + } + } + + ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); + if( ires!=0 ){ + Node realPart; + Trace("cbqi-inst-debug") << "Isolate : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; + if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){ + //redo, split integer/non-integer parts + bool useCoeff = false; + Integer coeff = d_one.getConst().getNumerator(); + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if( it->first.isNull() || it->first.getType().isInteger() ){ + if( !it->second.isNull() ){ + coeff = coeff.lcm( it->second.getConst().getDenominator() ); + useCoeff = true; + } + } + } + //multiply everything by this coefficient + Node rcoeff = NodeManager::currentNM()->mkConst( Rational( coeff ) ); + std::vector< Node > real_part; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if( useCoeff ){ + if( it->second.isNull() ){ + msum[it->first] = rcoeff; + }else{ + msum[it->first] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, it->second, rcoeff ) ); + } + } + if( !it->first.isNull() && !it->first.getType().isInteger() ){ + real_part.push_back( msum[it->first].isNull() ? it->first : NodeManager::currentNM()->mkNode( MULT, msum[it->first], it->first ) ); + } + } + for( unsigned t=0; t<2; t++ ){ + if( !vts_coeff[t].isNull() ){ + vts_coeff[t] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[t] ) ); + } + } + realPart = real_part.empty() ? d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) ); + Assert( d_out->isEligibleForInstantiation( realPart ) ); + //re-isolate + ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); + Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; + Trace("cbqi-inst-debug") << " real part : " << realPart << std::endl; + if( ires!=0 ){ + val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires==-1 ? PLUS : MINUS, + NodeManager::currentNM()->mkNode( ires==-1 ? MINUS : PLUS, val, realPart ), + NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) ); + Trace("cbqi-inst-debug") << "result : " << val << std::endl; + Assert( val.getType().isInteger() ); + } + } + } + vts_coeff_inf = vts_coeff[0]; + vts_coeff_delta = vts_coeff[1]; + } + + return ires; +} diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 38bb12e5b..9504bd407 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -48,6 +48,7 @@ private: Node d_true; bool d_use_vts_delta; bool d_use_vts_inf; + Node d_vts_sym[2]; //program variable contains cache std::map< Node, std::map< Node, bool > > d_prog_var; std::map< Node, bool > d_inelig; @@ -61,6 +62,8 @@ private: std::map< Node, std::map< Node, Node > > d_aux_eq; //the CE variables std::vector< Node > d_vars; + //index of variables reported in instantiation + std::vector< unsigned > d_var_order_index; //atoms of the CE lemma bool d_is_nested_quant; std::vector< Node > d_ce_atoms; @@ -95,6 +98,15 @@ private: } } }; + /* + class MbpBound { + public: + Node d_bound; + Node d_coeff; + Node d_vts_coeff[2]; + Node d_lit; + }; + */ // effort=0 : do not use model value, 1: use model value, 2: one must use model value bool addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, @@ -112,12 +124,13 @@ private: } Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ); - Node getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, - Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ); + Node getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ); void processAssertions(); void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); //get model value Node getModelValue( Node n ); +private: + int isolate( Node v, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta ); public: CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true ); //check : add instantiations based on valuation of d_vars diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index f7dc709d9..47e838f1c 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -341,7 +341,8 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* t = d_cg->getNextCandidate(); Trace("matching-debug2") << "Matching candidate : " << t << std::endl; //if t not null, try to fit it into match m - if( !t.isNull() && t.getType().isSubtypeOf( d_match_pattern_type ) ){ + if( !t.isNull() ){ + Assert( t.getType().isComparableTo( d_match_pattern_type ) ); success = getMatch( f, t, m, qe ); } }while( !success && !t.isNull() ); @@ -431,7 +432,7 @@ VarMatchGeneratorBooleanTerm::VarMatchGeneratorBooleanTerm( Node var, Node comp d_var_num[0] = var.getAttribute(InstVarNumAttribute()); } -bool VarMatchGeneratorBooleanTerm::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { +bool VarMatchGeneratorBooleanTerm::getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { if( !d_eq_class.isNull() ){ Node s = NodeManager::currentNM()->mkConst(qe->getEqualityQuery()->areEqual( d_eq_class, d_pattern )); d_eq_class = Node::null(); @@ -439,7 +440,7 @@ bool VarMatchGeneratorBooleanTerm::getNextMatch( Node f, InstMatch& m, Quantifie if( !m.set( qe, d_var_num[0], s ) ){ return false; }else{ - if( continueNextMatch( f, m, qe ) ){ + if( continueNextMatch( q, m, qe ) ){ return true; } } @@ -454,26 +455,24 @@ bool VarMatchGeneratorBooleanTerm::getNextMatch( Node f, InstMatch& m, Quantifie VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) : InstMatchGenerator(), d_var( var ), d_subs( subs ), d_rm_prev( false ){ d_var_num[0] = d_var.getAttribute(InstVarNumAttribute()); + d_var_type = d_var.getType(); } -bool VarMatchGeneratorTermSubs::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { +bool VarMatchGeneratorTermSubs::getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { if( !d_eq_class.isNull() ){ Trace("var-trigger-matching") << "Matching " << d_eq_class << " against " << d_var << " in " << d_subs << std::endl; Node s = d_subs.substitute( d_var, d_eq_class ); s = Rewriter::rewrite( s ); Trace("var-trigger-matching") << "...got " << s << std::endl; d_eq_class = Node::null(); - if( s.getType().isSubtypeOf( d_var.getType() ) ){ - d_rm_prev = m.get( d_var_num[0] ).isNull(); - if( !m.set( qe, d_var_num[0], s ) ){ - return false; - }else{ - if( continueNextMatch( f, m, qe ) ){ - return true; - } - } + //if( s.getType().isSubtypeOf( d_var_type ) ){ + d_rm_prev = m.get( d_var_num[0] ).isNull(); + if( !m.set( qe, d_var_num[0], s ) ){ + return false; }else{ - Trace("var-trigger-matching") << "Violates type requirement." << std::endl; + if( continueNextMatch( q, m, qe ) ){ + return true; + } } } if( d_rm_prev ){ @@ -484,11 +483,11 @@ bool VarMatchGeneratorTermSubs::getNextMatch( Node f, InstMatch& m, QuantifiersE } /** constructors */ -InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe ) : -d_f( f ){ - Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl; +InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) : +d_f( q ){ + Debug("smart-multi-trigger") << "Making smart multi-trigger for " << q << std::endl; std::map< Node, std::vector< Node > > var_contains; - qe->getTermDatabase()->getVarContains( f, pats, var_contains ); + qe->getTermDatabase()->getVarContains( q, pats, var_contains ); //convert to indicies for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){ Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: "; @@ -503,7 +502,7 @@ d_f( f ){ for( int i=0; i<(int)pats.size(); i++ ){ Node n = pats[i]; //make the match generator - d_children.push_back( InstMatchGenerator::mkInstMatchGenerator(f, n, qe ) ); + d_children.push_back( InstMatchGenerator::mkInstMatchGenerator(q, n, qe ) ); //compute unique/shared variables std::vector< int > unique_vars; std::map< int, bool > shared_vars; @@ -561,14 +560,14 @@ void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){ } } -int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ +int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){ int addedLemmas = 0; Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl; for( int i=0; i<(int)d_children.size(); i++ ){ Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl; std::vector< InstMatch > newMatches; - InstMatch m( f ); - while( d_children[i]->getNextMatch( f, m, qe ) ){ + InstMatch m( q ); + while( d_children[i]->getNextMatch( q, m, qe ) ){ //m.makeRepresentative( qe ); newMatches.push_back( InstMatch( &m ) ); m.clear(); @@ -684,15 +683,15 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, } } -int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){ +int InstMatchGeneratorMulti::addTerm( Node q, Node t, QuantifiersEngine* qe ){ Assert( options::eagerInstQuant() ); int addedLemmas = 0; for( int i=0; i<(int)d_children.size(); i++ ){ Node t_op = qe->getTermDatabase()->getOperator( t ); if( ((InstMatchGenerator*)d_children[i])->d_match_pattern_op==t_op ){ - InstMatch m( f ); + InstMatch m( q ); //if it produces a match, then process it with the rest - if( ((InstMatchGenerator*)d_children[i])->getMatch( f, t, m, qe ) ){ + if( ((InstMatchGenerator*)d_children[i])->getMatch( q, t, m, qe ) ){ processNewMatch( qe, m, i, addedLemmas ); } } @@ -700,10 +699,10 @@ int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){ return addedLemmas; } -InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ) { +InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat ) : d_f( q ), d_match_pattern( pat ) { for( unsigned i=0; igetTermDatabase()->getOperator( d_match_pattern ); } -int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ - InstMatch m( f ); +int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){ + InstMatch m( q ); m.add( baseMatch ); int addedLemmas = 0; @@ -749,7 +748,8 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin Node t = it->first; Node prev = m.get( v ); //using representatives, just check if equal - if( ( prev.isNull() || prev==t ) && t.getType().isSubtypeOf( d_match_pattern_arg_types[argIndex] ) ){ + Assert( t.getType().isComparableTo( d_match_pattern_arg_types[argIndex] ) ); + if( prev.isNull() || prev==t ){ m.setValue( v, t); addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); m.setValue( v, prev); @@ -766,9 +766,9 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin } } -int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){ +int InstMatchGeneratorSimple::addTerm( Node q, Node t, QuantifiersEngine* qe ){ Assert( options::eagerInstQuant() ); - InstMatch m( f ); + InstMatch m( q ); for( int i=0; i<(int)t.getNumChildren(); i++ ){ if( d_match_pattern[i].getKind()==INST_CONSTANT ){ m.setValue(d_var_num[i], t[i]); @@ -776,7 +776,7 @@ int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){ return 0; } } - return qe->addInstantiation( f, m, false ) ? 1 : 0; + return qe->addInstantiation( q, m, false ) ? 1 : 0; } }/* CVC4::theory::inst namespace */ diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index aae6d4e73..75adeb2d8 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -39,11 +39,11 @@ public: /** reset, eqc is the equivalence class to search in (any if eqc=null) */ virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0; /** get the next match. must call reset( eqc ) before this function. */ - virtual bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) = 0; + virtual bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) = 0; /** add instantiations directly */ - virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0; + virtual int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0; /** add ground term t, called when t is added to term db */ - virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) { return 0; } + virtual int addTerm( Node q, Node t, QuantifiersEngine* qe ) { return 0; } /** set active add */ virtual void setActiveAdd( bool val ) {} };/* class IMGenerator */ @@ -72,7 +72,7 @@ protected: /** children types 0 : variable, 1 : child term, -1 : ground term */ std::vector< int > d_children_types; /** continue */ - bool continueNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ); + bool continueNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ); public: enum { //options for producing matches @@ -85,7 +85,7 @@ public: d_match_pattern and t should have the same shape. only valid for use where !d_match_pattern.isNull(). */ - bool getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ); + bool getMatch( Node q, Node t, InstMatch& m, QuantifiersEngine* qe ); /** constructors */ InstMatchGenerator( Node pat ); @@ -108,11 +108,11 @@ public: /** reset, eqc is the equivalence class to search in (any if eqc=null) */ void reset( Node eqc, QuantifiersEngine* qe ); /** get the next match. must call reset( eqc ) before this function. */ - bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ); + bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ); /** add instantiations */ - int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); + int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ); /** add ground term t */ - int addTerm( Node f, Node t, QuantifiersEngine* qe ); + int addTerm( Node q, Node t, QuantifiersEngine* qe ); bool d_active_add; void setActiveAdd( bool val ); @@ -133,9 +133,9 @@ public: /** reset, eqc is the equivalence class to search in (any if eqc=null) */ void reset( Node eqc, QuantifiersEngine* qe ){ d_eq_class = eqc; } /** get the next match. must call reset( eqc ) before this function. */ - bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ); + bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ); /** add instantiations directly */ - int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ return 0; } + int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){ return 0; } }; //match generator for purified terms (matched term is substituted into d_subs) @@ -144,6 +144,7 @@ public: VarMatchGeneratorTermSubs( Node var, Node subs ); ~VarMatchGeneratorTermSubs() throw() {} TNode d_var; + TypeNode d_var_type; Node d_subs; bool d_rm_prev; /** reset instantiation round (call this at beginning of instantiation round) */ @@ -151,9 +152,9 @@ public: /** reset, eqc is the equivalence class to search in (any if eqc=null) */ void reset( Node eqc, QuantifiersEngine* qe ){ d_eq_class = eqc; } /** get the next match. must call reset( eqc ) before this function. */ - bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ); + bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ); /** add instantiations directly */ - int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) { return 0; } + int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ) { return 0; } }; /** smart multi-trigger implementation */ @@ -188,7 +189,7 @@ private: void calculateMatches( QuantifiersEngine* qe ); public: /** constructors */ - InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe ); + InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ); /** destructor */ ~InstMatchGeneratorMulti() throw() {} /** reset instantiation round (call this whenever equivalence classes have changed) */ @@ -196,11 +197,11 @@ public: /** reset, eqc is the equivalence class to search in (any if eqc=null) */ void reset( Node eqc, QuantifiersEngine* qe ); /** get the next match. must call reset( eqc ) before this function. (not implemented) */ - bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; } + bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; } /** add instantiations */ - int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); + int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ); /** add ground term t */ - int addTerm( Node f, Node t, QuantifiersEngine* qe ); + int addTerm( Node q, Node t, QuantifiersEngine* qe ); };/* class InstMatchGeneratorMulti */ /** smart (single)-trigger implementation */ @@ -220,7 +221,7 @@ private: void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ); public: /** constructors */ - InstMatchGeneratorSimple( Node f, Node pat ); + InstMatchGeneratorSimple( Node q, Node pat ); /** destructor */ ~InstMatchGeneratorSimple() throw() {} /** reset instantiation round (call this whenever equivalence classes have changed) */ @@ -228,11 +229,11 @@ public: /** reset, eqc is the equivalence class to search in (any if eqc=null) */ void reset( Node eqc, QuantifiersEngine* qe ) {} /** get the next match. must call reset( eqc ) before this function. (not implemented) */ - bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; } + bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; } /** add instantiations */ - int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); + int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ); /** add ground term t, possibly add instantiations */ - int addTerm( Node f, Node t, QuantifiersEngine* qe ); + int addTerm( Node q, Node t, QuantifiersEngine* qe ); };/* class InstMatchGeneratorSimple */ } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 9e13ef5eb..a1af1313d 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1524,7 +1524,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { if( it != d_qn[index]->d_data.end() ) { d_qni.push_back( it ); //set the match - if( it->first.getType().isSubtypeOf( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first ) ){ + if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first ) ){ Debug("qcf-match-debug") << " Binding variable" << std::endl; if( d_qn.size()second ); diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 026293e02..0b212d696 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -137,6 +137,24 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind return 0; } +int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) { + Node vatom; + //isolate pv in the inequality + int ires = isolate( v, msum, vatom, k, true ); + if( ires!=0 ){ + val = vatom[ ires==1 ? 1 : 0 ]; + Node pvm = vatom[ ires==1 ? 0 : 1 ]; + //get monomial + if( pvm!=v ){ + Node veq_v; + if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ + Assert( veq_v==v ); + } + } + } + return ires; +} + Node QuantArith::negate( Node t ) { Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t ); tt = Rewriter::rewrite( tt ); diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 2186e03fd..f65163415 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -38,6 +38,7 @@ public: static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum ); //return 1 : solved on LHS, return -1 : solved on RHS, return 0: failed static int isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff = false ); + static int isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ); static Node negate( Node t ); static Node offset( Node t, int i ); static void debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 2c9430876..bfeacf044 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1481,6 +1481,19 @@ bool TermDb::containsVtsInfinity( Node n, bool isFree ) { return containsTerms( n, t ); } +Node TermDb::mkNodeType( Node n, TypeNode tn ) { + TypeNode ntn = n.getType(); + Assert( ntn.isComparableTo( tn ) ); + if( ntn.isSubtypeOf( tn ) ){ + return n; + }else{ + if( tn.isInteger() ){ + return NodeManager::currentNM()->mkNode( TO_INTEGER, n ); + } + return Node::null(); + } +} + bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) { if( n==t ){ return true; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 1b0b72bf9..3e38897d1 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -377,6 +377,8 @@ public: bool containsVtsTerm( std::vector< Node >& n, bool isFree = false ); /** simple check for contains term */ bool containsVtsInfinity( Node n, bool isFree = false ); + /** make type */ + static Node mkNodeType( Node n, TypeNode tn ); private: //helper for contains term diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 5706c789e..de3c503b5 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -62,7 +62,9 @@ d_quantEngine( qe ), d_f( f ){ ++(qe->d_statistics.d_simple_triggers); } }else{ - Trace("multi-trigger") << "Multi-trigger " << (*this) << " for " << f << std::endl; + Trace("multi-trigger") << "Multi-trigger "; + debugPrint("multi-trigger"); + Trace("multi-trigger") << " for " << f << std::endl; //Notice() << "Multi-trigger for " << f << " : " << std::endl; //Notice() << " " << (*this) << std::endl; ++(qe->d_statistics.d_multi_triggers); diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index bd4c19dba..1817ebe56 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -120,16 +120,6 @@ public: /** get all variables that E-matching can possibly handle */ static void getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars ); - inline void toStream(std::ostream& out) const { - /* - out << "TRIGGER( "; - for( int i=0; i<(int)d_nodes.size(); i++ ){ - if( i>0 ){ out << ", "; } - out << d_nodes[i]; - } - out << " )"; - */ - } void debugPrint( const char * c ) { Trace(c) << "TRIGGER( "; for( int i=0; i<(int)d_nodes.size(); i++ ){ @@ -140,12 +130,6 @@ public: } }; -inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) { - tr.toStream(out); - return out; -} - - /** a trie of triggers */ class TriggerTrie { private: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 9ae3b1d40..41e560557 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -696,7 +696,7 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No } } -bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){ +bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){ Assert( f.getKind()==FORALL ); Assert( vars.size()==terms.size() ); Node body = getInstantiation( f, vars, terms ); @@ -920,12 +920,17 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo Assert( terms.size()==q[0].getNumChildren() ); Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl; for( unsigned i=0; i " << terms[i] << std::endl; + Trace("inst-add-debug") << " " << q[0][i] << " -> " << terms[i]; //make it representative, this is helpful for recognizing duplication if( mkRep ){ //pick the best possible representative for instantiation, based on past use and simplicity of term terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i ); + }else{ + //ensure the type is correct + terms[i] = quantifiers::TermDb::mkNodeType( terms[i], q[0][i].getType() ); } + Trace("inst-add-debug") << " -> " << terms[i] << std::endl; + Assert( !terms[i].isNull() ); } //check based on instantiation level @@ -974,7 +979,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo //add the instantiation Trace("inst-add-debug") << "Constructing instantiation..." << std::endl; - bool addedInst = addInstantiation( q, d_term_db->d_vars[q], terms, doVts ); + bool addedInst = addInstantiationInternal( q, d_term_db->d_vars[q], terms, doVts ); //report the result if( addedInst ){ Trace("inst-add-debug") << " -> Success." << std::endl; @@ -1276,7 +1281,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, if( i>0 ) Trace("internal-rep-select") << ", "; Trace("internal-rep-select") << eqc[i]; } - Trace("internal-rep-select") << " } " << std::endl; + Trace("internal-rep-select") << " }, type = " << v_tn << std::endl; int r_best_score = -1; for( size_t i=0; i& vars, std::vector< Node >& terms ); /** instantiate f with arguments terms */ - bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false ); + bool addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false ); /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level ); /** flush lemmas */ diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 73fa07bf9..89dcc0a26 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -57,7 +57,10 @@ TESTS = \ cbqi-lia-dt-simp.smt2 \ is-int.smt2 \ floor.smt2 \ - array-unsat-simp3.smt2 + array-unsat-simp3.smt2 \ + mix-simp.smt2 \ + mix-coeff.smt2 \ + mix-match.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/mix-coeff.smt2 b/test/regress/regress0/quantifiers/mix-coeff.smt2 new file mode 100644 index 000000000..a20867b1c --- /dev/null +++ b/test/regress/regress0/quantifiers/mix-coeff.smt2 @@ -0,0 +1,4 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(assert (forall ((x Int) (y Int) (a Real) (z Int)) (or (> x (+ a (* (/ 2 3) y) (* (/ 4 5) z))) (< x (+ 10 (* 3 a) (* (/ 2 5) y) (* (/ 4 7) z)))))) +(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/quantifiers/mix-match.smt2 b/test/regress/regress0/quantifiers/mix-match.smt2 new file mode 100644 index 000000000..c6ac3b56f --- /dev/null +++ b/test/regress/regress0/quantifiers/mix-match.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-fun P (Real) Bool) +(assert (forall ((x Int)) (P x))) + +(declare-fun a () Real) +(assert (is_int a)) +(assert (not (P a))) + +(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/quantifiers/mix-simp.smt2 b/test/regress/regress0/quantifiers/mix-simp.smt2 new file mode 100644 index 000000000..0b8c5067d --- /dev/null +++ b/test/regress/regress0/quantifiers/mix-simp.smt2 @@ -0,0 +1,4 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(assert (forall ((x Real)) (exists ((y Int)) (and (>= y x) (< y (+ x 1)))))) +(check-sat) -- 2.30.2