From: Andrew Reynolds Date: Tue, 19 Sep 2017 11:31:22 +0000 (-0500) Subject: Refactor cegqi instantiation infrastructure so that it is more independent of instant... X-Git-Tag: cvc5-1.0.0~5630 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=324eafcb6d243312e366009d140758c40527db54;p=cvc5.git Refactor cegqi instantiation infrastructure so that it is more independent of instantiation for LIA. (#1111) --- diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index db283ccfc..42394122e 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -192,10 +192,10 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e //must be an eligible term if( isEligible( n ) ){ Node ns; - Node pv_coeff; //coefficient of pv in the equality we solve (null is 1) + TermProperties pv_prop; //coefficient of pv in the equality we solve (null is 1) bool proc = false; if( !d_prog_var[n].empty() ){ - ns = applySubstitution( pvtn, n, sf, pv_coeff, false ); + ns = applySubstitution( pvtn, n, sf, pv_prop, false ); if( !ns.isNull() ){ computeProgVars( ns ); //substituted version must be new and cannot contain pv @@ -206,7 +206,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e proc = true; } if( proc ){ - if( vinst->processEqualTerm( this, sf, pv, pv_coeff, ns, effort ) ){ + if( vinst->processEqualTerm( this, sf, pv, pv_prop, ns, effort ) ){ return true; } } @@ -229,7 +229,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r ); std::vector< Node > lhs; std::vector< bool > lhs_v; - std::vector< Node > lhs_coeff; + std::vector< TermProperties > lhs_prop; Assert( it_reqc!=d_curr_eqc.end() ); for( unsigned kk=0; kksecond.size(); kk++ ){ Node n = it_reqc->second[kk]; @@ -237,9 +237,9 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e //must be an eligible term if( isEligible( n ) ){ Node ns; - Node pv_coeff; + TermProperties pv_prop; if( !d_prog_var[n].empty() ){ - ns = applySubstitution( pvtn, n, sf, pv_coeff ); + ns = applySubstitution( pvtn, n, sf, pv_prop ); if( !ns.isNull() ){ computeProgVars( ns ); } @@ -249,27 +249,26 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e if( !ns.isNull() ){ bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl; - std::vector< Node > term_coeffs; + std::vector< TermProperties > term_props; std::vector< Node > terms; - term_coeffs.push_back( pv_coeff ); + term_props.push_back( pv_prop ); terms.push_back( ns ); for( unsigned j=0; j " << n << std::endl; Assert( n.getType().isSubtypeOf( pv.getType() ) ); @@ -371,15 +371,15 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int a_subs.push_back( n ); std::vector< Node > a_var; a_var.push_back( pv ); - std::vector< Node > a_coeff; + std::vector< TermProperties > a_prop; std::vector< Node > a_has_coeff; - if( !pv_coeff.isNull() ){ - a_coeff.push_back( pv_coeff ); + if( !pv_prop.d_coeff.isNull() ){ + a_prop.push_back( pv_prop ); a_has_coeff.push_back( pv ); } bool success = true; std::map< int, Node > prev_subs; - std::map< int, Node > prev_coeff; + std::map< int, TermProperties > prev_prop; std::map< int, Node > prev_sym_subs; std::vector< Node > new_has_coeff; Trace("cbqi-inst-debug2") << "Applying substitutions..." << std::endl; @@ -390,20 +390,20 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int prev_subs[j] = sf.d_subs[j]; TNode tv = pv; TNode ts = n; - Node a_pv_coeff; - Node new_subs = applySubstitution( sf.d_vars[j].getType(), sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true ); + TermProperties a_pv_prop; + Node new_subs = applySubstitution( sf.d_vars[j].getType(), sf.d_subs[j], a_subs, a_prop, a_has_coeff, a_var, a_pv_prop, true ); if( !new_subs.isNull() ){ sf.d_subs[j] = new_subs; - if( !a_pv_coeff.isNull() ){ - prev_coeff[j] = sf.d_coeff[j]; - if( sf.d_coeff[j].isNull() ){ + if( !a_pv_prop.d_coeff.isNull() ){ + prev_prop[j] = sf.d_props[j]; + if( sf.d_props[j].d_coeff.isNull() ){ Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), sf.d_vars[j] )==sf.d_has_coeff.end() ); //now has coefficient new_has_coeff.push_back( sf.d_vars[j] ); sf.d_has_coeff.push_back( sf.d_vars[j] ); - sf.d_coeff[j] = a_pv_coeff; + sf.d_props[j].d_coeff = a_pv_prop.d_coeff; }else{ - sf.d_coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[j], a_pv_coeff ) ); + sf.d_props[j].d_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_props[j].d_coeff, a_pv_prop.d_coeff ) ); } } if( sf.d_subs[j]!=prev_subs[j] ){ @@ -422,14 +422,14 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int } if( success ){ Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl; - sf.push_back( pv, n, pv_coeff, bt ); + sf.push_back( pv, n, pv_prop ); Node prev_theta = sf.d_theta; Node new_theta = sf.d_theta; - if( !pv_coeff.isNull() ){ + if( !pv_prop.d_coeff.isNull() ){ if( new_theta.isNull() ){ - new_theta = pv_coeff; + new_theta = pv_prop.d_coeff; }else{ - new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, pv_coeff ); + new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, pv_prop.d_coeff ); new_theta = Rewriter::rewrite( new_theta ); } } @@ -440,7 +440,7 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int sf.d_theta = prev_theta; if( !success ){ Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl; - sf.pop_back( pv, n, pv_coeff, bt ); + sf.pop_back( pv, n, pv_prop ); } } if( success ){ @@ -451,8 +451,8 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){ sf.d_subs[it->first] = it->second; } - for( std::map< int, Node >::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){ - sf.d_coeff[it->first] = it->second; + for( std::map< int, TermProperties >::iterator it = prev_prop.begin(); it != prev_prop.end(); it++ ){ + sf.d_props[it->first] = it->second; } for( unsigned i=0; i& subs, std::vector return ret; } -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 ) { +Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< TermProperties >& prop, std::vector< Node >& has_coeff, + std::vector< Node >& vars, TermProperties& pv_prop, bool try_coeff ) { Assert( d_prog_var.find( n )!=d_prog_var.end() ); Assert( n==Rewriter::rewrite( n ) ); bool req_coeff = false; @@ -526,10 +526,10 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node std::vector< Node > nvars; std::vector< Node > nsubs; for( unsigned i=0; imkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/coeff[i].getConst() ) ); + Assert( prop[i].d_coeff.isConst() ); + Node nn =NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/prop[i].d_coeff.getConst() ) ); nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn ); nn = Rewriter::rewrite( nn ); nsubs.push_back( nn ); @@ -553,18 +553,18 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node std::vector< Node >::iterator its = std::find( vars.begin(), vars.end(), it->first ); if( its!=vars.end() ){ int index = its-vars.begin(); - if( coeff[index].isNull() ){ + if( prop[index].d_coeff.isNull() ){ //apply substitution msum_term[it->first] = subs[index]; }else{ //apply substitution, multiply to ensure no divisibility conflict msum_term[it->first] = subs[index]; //relative coefficient - msum_coeff[it->first] = coeff[index]; - if( pv_coeff.isNull() ){ - pv_coeff = coeff[index]; + msum_coeff[it->first] = prop[index].d_coeff; + if( pv_prop.d_coeff.isNull() ){ + pv_prop.d_coeff = prop[index].d_coeff; }else{ - pv_coeff = NodeManager::currentNM()->mkNode( MULT, pv_coeff, coeff[index] ); + pv_prop.d_coeff = NodeManager::currentNM()->mkNode( MULT, pv_prop.d_coeff, prop[index].d_coeff ); } } }else{ @@ -572,16 +572,16 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node } } //make sum with normalized coefficient - if( !pv_coeff.isNull() ){ - pv_coeff = Rewriter::rewrite( pv_coeff ); - Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_coeff << std::endl; + if( !pv_prop.d_coeff.isNull() ){ + pv_prop.d_coeff = Rewriter::rewrite( pv_prop.d_coeff ); + Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_prop.d_coeff << std::endl; std::vector< Node > children; for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ Node c_coeff; if( !msum_coeff[it->first].isNull() ){ - c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_coeff.getConst() / msum_coeff[it->first].getConst() ) ); + c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_prop.d_coeff.getConst() / msum_coeff[it->first].getConst() ) ); }else{ - c_coeff = pv_coeff; + c_coeff = pv_prop.d_coeff; } if( !it->second.isNull() ){ c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second ); @@ -600,7 +600,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node nret = Rewriter::rewrite( nret ); //ensure that nret does not contain vars if( !TermDb::containsTerms( nret, vars ) ){ - //result is ( nret / pv_coeff ) + //result is ( nret / pv_prop.d_coeff ) return nret; }else{ Trace("cegqi-si-apply-subs-debug") << "Failed, since result " << nret << " contains free variable." << std::endl; @@ -1032,8 +1032,9 @@ Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ) } -bool Instantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) { - return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort ); +bool Instantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ) { + pv_prop.d_type = 0; + return ci->doAddInstantiationInc( pv, n, pv_prop, sf, effort ); } diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index c260486ff..bf555916f 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -40,15 +40,19 @@ public: class Instantiator; - -//TODO: refactor pv_coeff to pv_prop throughout -//generic class that stores properties for a variable to solve for in CEGQI +//stores properties for a variable to solve for in CEGQI +// For LIA, this includes the coefficient of the variable, and the bound type for the variable class TermProperties { public: - TermProperties() : d_type(-1) {} + TermProperties() : d_type(0) {} + // type of property for a term + // for arithmetic this corresponds to bound type (0:equal, 1:upper bound, -1:lower bound) int d_type; // for arithmetic Node d_coeff; + // get cache node + // we consider terms + TermProperties that are unique up to their cache node (see doAddInstantiationInc) + Node getCacheNode() { return d_coeff; } }; //solved form, involves substitution with coefficients @@ -56,36 +60,29 @@ class SolvedForm { public: std::vector< Node > d_vars; std::vector< Node > d_subs; - //TODO: refactor below coeff -> prop; - std::vector< Node > d_coeff; - std::vector< int > d_btyp; - //std::vector< TermProperties > d_props; + std::vector< TermProperties > d_props; std::vector< Node > d_has_coeff; - //std::vector< Node > d_has_prop; Node d_theta; void copy( SolvedForm& sf ){ d_vars.insert( d_vars.end(), sf.d_vars.begin(), sf.d_vars.end() ); d_subs.insert( d_subs.end(), sf.d_subs.begin(), sf.d_subs.end() ); - d_coeff.insert( d_coeff.end(), sf.d_coeff.begin(), sf.d_coeff.end() ); - d_btyp.insert( d_btyp.end(), sf.d_btyp.begin(), sf.d_btyp.end() ); + d_props.insert( d_props.end(), sf.d_props.begin(), sf.d_props.end() ); d_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() ); d_theta = sf.d_theta; } - void push_back( Node pv, Node n, Node pv_coeff, int bt ){ + void push_back( Node pv, Node n, TermProperties& pv_prop ){ d_vars.push_back( pv ); d_subs.push_back( n ); - d_coeff.push_back( pv_coeff ); - d_btyp.push_back( bt ); - if( !pv_coeff.isNull() ){ + d_props.push_back( pv_prop ); + if( !pv_prop.d_coeff.isNull() ){ d_has_coeff.push_back( pv ); } } - void pop_back( Node pv, Node n, Node pv_coeff, int bt ){ + void pop_back( Node pv, Node n, TermProperties& pv_prop ){ d_vars.pop_back(); d_subs.pop_back(); - d_coeff.pop_back(); - d_btyp.pop_back(); - if( !pv_coeff.isNull() ){ + d_props.pop_back(); + if( !pv_prop.d_coeff.isNull() ){ d_has_coeff.pop_back(); } } @@ -159,14 +156,14 @@ public: public: void pushStackVariable( Node v ); void popStackVariable(); - bool doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int bt, SolvedForm& sf, unsigned effort ); + bool doAddInstantiationInc( Node pv, Node n, TermProperties& pv_prop, SolvedForm& sf, unsigned effort ); Node getModelValue( Node n ); // TODO: move to solved form? - Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, Node& pv_coeff, bool try_coeff = true ) { - return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, sf.d_vars, pv_coeff, try_coeff ); + Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, TermProperties& pv_prop, bool try_coeff = true ) { + return applySubstitution( tn, n, sf.d_subs, sf.d_props, sf.d_has_coeff, sf.d_vars, pv_prop, try_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 applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< TermProperties >& prop, std::vector< Node >& has_coeff, + std::vector< Node >& vars, TermProperties& pv_prop, bool try_coeff = true ); public: unsigned getNumCEAtoms() { return d_ce_atoms.size(); } Node getCEAtom( unsigned i ) { return d_ce_atoms[i]; } @@ -191,15 +188,16 @@ public: virtual ~Instantiator(){} virtual void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {} - //called when pv_coeff * pv = n, and n is eligible for instantiation - virtual bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ); + //called when pv_prop.d_coeff * pv = n, and n is eligible for instantiation + virtual bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ); //eqc is the equivalence class of pv virtual bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { return false; } virtual bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } - //term_coeffs.size() = terms.size() = 2, called when term_coeff[0] * terms[0] = term_coeff[1] * terms[1], terms are eligible, and at least one of these terms contains pv + //term_props.size() = terms.size() = 2 + // called when terms[0] = terms[1], terms are eligible, and at least one of these terms contains pv // returns true if an instantiation was successfully added via a recursive call - virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { return false; } + virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) { return false; } virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { return false; } @@ -228,7 +226,6 @@ public: std::string identify() const { return "ModelValue"; } }; - } } } diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index fa7dbabab..130d73af6 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -223,11 +223,11 @@ void ArithInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, un } } -bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { +bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) { Node eq_lhs = terms[0]; Node eq_rhs = terms[1]; - Node lhs_coeff = term_coeffs[0]; - Node rhs_coeff = term_coeffs[1]; + Node lhs_coeff = term_props[0].d_coeff; + Node rhs_coeff = term_props[1].d_coeff; //make the same coefficient if( rhs_coeff!=lhs_coeff ){ if( !rhs_coeff.isNull() ){ @@ -244,13 +244,14 @@ bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, N Node eq = eq_lhs.eqNode( eq_rhs ); eq = Rewriter::rewrite( eq ); Node val; - Node veq_c; + TermProperties pv_prop; Node vts_coeff_inf; Node vts_coeff_delta; //isolate pv in the equality - int ires = solve_arith( ci, pv, eq, veq_c, val, vts_coeff_inf, vts_coeff_delta ); + int ires = solve_arith( ci, pv, eq, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta ); if( ires!=0 ){ - if( ci->doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){ + pv_prop.d_type = 0; + if( ci->doAddInstantiationInc( pv, val, pv_prop, sf, effort ) ){ return true; } } @@ -285,11 +286,11 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, //must be an eligible term if( ci->isEligible( atom_lhs ) ){ //apply substitution to LHS of atom - Node atom_lhs_coeff; - atom_lhs = ci->applySubstitution( d_type, atom_lhs, sf, atom_lhs_coeff ); + TermProperties atom_lhs_prop; + atom_lhs = ci->applySubstitution( d_type, atom_lhs, sf, atom_lhs_prop ); if( !atom_lhs.isNull() ){ - if( !atom_lhs_coeff.isNull() ){ - atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) ); + if( !atom_lhs_prop.d_coeff.isNull() ){ + atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_prop.d_coeff, atom_rhs ) ); } } //if it contains pv, not infinity @@ -302,9 +303,9 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node vts_coeff_inf; Node vts_coeff_delta; Node val; - Node veq_c; + TermProperties pv_prop; //isolate pv in the inequality - int ires = solve_arith( ci, pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta ); + int ires = solve_arith( ci, pv, satom, pv_prop.d_coeff, 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; @@ -337,8 +338,8 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, }else{ Node rhs_value = ci->getModelValue( val ); Node lhs_value = pv_value; - if( !veq_c.isNull() ){ - lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c ); + if( !pv_prop.d_coeff.isNull() ){ + lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, pv_prop.d_coeff ); lhs_value = Rewriter::rewrite( lhs_value ); } Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl; @@ -362,8 +363,8 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, } } Trace("cbqi-bound-inf") << "From " << lit << ", got : "; - if( !veq_c.isNull() ){ - Trace("cbqi-bound-inf") << veq_c << " * "; + if( !pv_prop.d_coeff.isNull() ){ + Trace("cbqi-bound-inf") << pv_prop.d_coeff << " * "; } Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl; //take into account delta @@ -386,15 +387,16 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, //just store bounds, will choose based on tighest bound unsigned index = uires>0 ? 0 : 1; d_mbp_bounds[index].push_back( uval ); - d_mbp_coeff[index].push_back( veq_c ); - Trace("cbqi-inst-debug") << "Store bound " << index << " " << uval << " " << veq_c << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl; + d_mbp_coeff[index].push_back( pv_prop.d_coeff ); + Trace("cbqi-inst-debug") << "Store bound " << index << " " << uval << " " << pv_prop.d_coeff << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl; for( unsigned t=0; t<2; t++ ){ d_mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta ); } d_mbp_lit[index].push_back( lit ); }else{ //try this bound - if( ci->doAddInstantiationInc( pv, uval, veq_c, uires>0 ? 1 : -1, sf, effort ) ){ + pv_prop.d_type = uires>0 ? 1 : -1; + if( ci->doAddInstantiationInc( pv, uval, pv_prop, sf, effort ) ){ return true; } } @@ -434,7 +436,8 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, val = NodeManager::currentNM()->mkNode( UMINUS, val ); val = Rewriter::rewrite( val ); } - if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ + TermProperties pv_prop_no_bound; + if( ci->doAddInstantiationInc( pv, val, pv_prop_no_bound, sf, effort ) ){ return true; } } @@ -528,7 +531,10 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, val = getModelBasedProjectionValue( ci, pv, val, rr==0, d_mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.d_theta, d_mbp_vts_coeff[rr][0][best], d_mbp_vts_coeff[rr][1][best] ); if( !val.isNull() ){ - if( ci->doAddInstantiationInc( pv, val, d_mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, effort ) ){ + TermProperties pv_prop_bound; + pv_prop_bound.d_coeff = d_mbp_coeff[rr][best]; + pv_prop_bound.d_type = rr==0 ? 1 : -1; + if( ci->doAddInstantiationInc( pv, val, pv_prop_bound, sf, effort ) ){ return true; } } @@ -539,10 +545,10 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, //if not using infinity, use model value of zero if( !use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty() ){ Node val = zero; - Node c; //null (one) coefficient - val = getModelBasedProjectionValue( ci, pv, val, true, c, pv_value, zero, sf.d_theta, Node::null(), Node::null() ); + TermProperties pv_prop_zero; + val = getModelBasedProjectionValue( ci, pv, val, true, pv_prop_zero.d_coeff, pv_value, zero, sf.d_theta, Node::null(), Node::null() ); if( !val.isNull() ){ - if( ci->doAddInstantiationInc( pv, val, c, 0, sf, effort ) ){ + if( ci->doAddInstantiationInc( pv, val, pv_prop_zero, sf, effort ) ){ return true; } } @@ -583,7 +589,8 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, } Trace("cbqi-bound") << "Midpoint value : " << val << std::endl; if( !val.isNull() ){ - if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ + TermProperties pv_prop_midpoint; + if( ci->doAddInstantiationInc( pv, val, pv_prop_midpoint, sf, effort ) ){ return true; } } @@ -601,7 +608,10 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, Node val = getModelBasedProjectionValue( ci, pv, d_mbp_bounds[rr][j], rr==0, d_mbp_coeff[rr][j], pv_value, t_values[rr][j], sf.d_theta, d_mbp_vts_coeff[rr][0][j], d_mbp_vts_coeff[rr][1][j] ); if( !val.isNull() ){ - if( ci->doAddInstantiationInc( pv, val, d_mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, effort ) ){ + TermProperties pv_prop_nopt_bound; + pv_prop_nopt_bound.d_coeff = d_mbp_coeff[rr][j]; + pv_prop_nopt_bound.d_type = rr==0 ? 1 : -1; + if( ci->doAddInstantiationInc( pv, val, pv_prop_nopt_bound, sf, effort ) ){ return true; } } @@ -621,12 +631,13 @@ bool ArithInstantiator::postProcessInstantiation( CegInstantiator * ci, SolvedFo Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), pv )!=sf.d_has_coeff.end() ); Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )!=sf.d_vars.end() ); unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )-sf.d_vars.begin(); - Assert( !sf.d_coeff[index].isNull() ); - Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << sf.d_vars[index] << " = " << sf.d_subs[index] << std::endl; + Assert( !sf.d_props[index].d_coeff.isNull() ); + Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_props[index].d_coeff << " * "; + Trace("cbqi-inst-debug") << sf.d_vars[index] << " = " << sf.d_subs[index] << std::endl; Assert( sf.d_vars[index].getType().isInteger() ); //must ensure that divisibility constraints are met //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful - Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], sf.d_vars[index] ); + Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_props[index].d_coeff, sf.d_vars[index] ); Node eq_rhs = sf.d_subs[index]; Node eq = eq_lhs.eqNode( eq_rhs ); eq = Rewriter::rewrite( eq ); @@ -645,9 +656,9 @@ bool ArithInstantiator::postProcessInstantiation( CegInstantiator * ci, SolvedFo sf.d_subs[index] = veq[1]; if( !veq_c.isNull() ){ sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c ); - Trace("cbqi-inst-debug") << "...bound type is : " << sf.d_btyp[index] << std::endl; + Trace("cbqi-inst-debug") << "...bound type is : " << sf.d_props[index].d_type << std::endl; //intger division rounding up if from a lower bound - if( sf.d_btyp[index]==1 && options::cbqiRoundUpLowerLia() ){ + if( sf.d_props[index].d_type==1 && options::cbqiRoundUpLowerLia() ){ sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index], NodeManager::currentNM()->mkNode( ITE, NodeManager::currentNM()->mkNode( EQUAL, @@ -732,7 +743,8 @@ bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, No children.push_back( c ); } Node val = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); - if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ + TermProperties pv_prop_dt; + if( ci->doAddInstantiationInc( pv, val, pv_prop_dt, sf, effort ) ){ return true; }else{ //cleanup @@ -746,11 +758,11 @@ bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, No return false; } -bool DtInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { +bool DtInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) { Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] ); if( !val.isNull() ){ - Node veq_c; - if( ci->doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){ + TermProperties pv_prop; + if( ci->doAddInstantiationInc( pv, val, pv_prop, sf, effort ) ){ return true; } } @@ -761,13 +773,14 @@ void EprInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsi d_equal_terms.clear(); } -bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) { +bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ) { if( options::quantEprMatching() ){ - Assert( pv_coeff.isNull() ); + Assert( pv_prop.d_coeff.isNull() ); d_equal_terms.push_back( n ); return false; }else{ - return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort ); + pv_prop.d_type = 0; + return ci->doAddInstantiationInc( pv, n, pv_prop, sf, effort ); } } @@ -832,9 +845,10 @@ bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, N } //sort by match score std::sort( d_equal_terms.begin(), d_equal_terms.end(), setm ); - Node pv_coeff; + TermProperties pv_prop; + pv_prop.d_type = 0; for( unsigned i=0; idoAddInstantiationInc( pv, d_equal_terms[i], pv_coeff, 0, sf, effort ) ){ + if( ci->doAddInstantiationInc( pv, d_equal_terms[i], pv_prop, sf, effort ) ){ return true; } } @@ -1023,7 +1037,7 @@ void BvInstantiator::processLiteral( CegInstantiator * ci, SolvedForm& sf, Node if( d_inelig.find( atom[1-t] )==d_inelig.end() ){ //only ground terms TODO: more if( d_prog_var[atom[1-t]].empty() ){ - Node veq_c; + TermProperties pv_prop; Node uval; if( ( !pol && atom.getKind()==BITVECTOR_ULT ) || ( pol && atom.getKind()==BITVECTOR_ULE ) ){ uval = atom[1-t]; @@ -1031,7 +1045,7 @@ void BvInstantiator::processLiteral( CegInstantiator * ci, SolvedForm& sf, Node uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t], bv::utils::mkConst(pvtn.getConst(), 1) ); } - if( doAddInstantiationInc( pv, uval, veq_c, 0, sf, effort ) ){ + if( doAddInstantiationInc( pv, uval, pv_prop, sf, effort ) ){ return true; } } @@ -1042,7 +1056,7 @@ void BvInstantiator::processLiteral( CegInstantiator * ci, SolvedForm& sf, Node */ } -bool BvInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { +bool BvInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) { //processLiteral( ci, sf, pv, terms[0].eqNode( terms[1] ), effort ); return false; } diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h index dfb7921c8..a24878caf 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.h +++ b/src/theory/quantifiers/ceg_t_instantiator.h @@ -40,7 +40,7 @@ public: virtual ~ArithInstantiator(){} void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } - bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ); + bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ); bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); @@ -59,7 +59,7 @@ public: void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ); bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } - bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ); + bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ); std::string identify() const { return "Dt"; } }; @@ -74,7 +74,7 @@ public: EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} virtual ~EprInstantiator(){} void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); - bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ); + bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ); bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ); std::string identify() const { return "Epr"; } }; @@ -135,7 +135,7 @@ public: virtual ~BvInstantiator(){} void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } - bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ); + bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ); bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );