From 25e598ed369ee2cc6227dbfb67f7d38303a7144a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 25 Sep 2017 19:43:27 -0500 Subject: Cegqi refactor substitutions (#1129) This refactors the apply substitution mechanism for counterexample-guided quantifier instantiation (CEGQI). Improvements to the code: (1) Methods have been added to the TermProperties class that summarize their theory-independent behavior (including "getModifiedTerm", "isBasic" etc.). For now, I have not made a "TermPropertiesArith" class yet since this will require more fundamental refactoring. (2) The terminology "has_coeff" is replaced "is_non_basic" throughout. (3) Added the applySubstitutionToLiteral method. (4) Both applySubstitution and applySubstitutionToLiteral are now private within CegInstantiator. This means that theory-specific instantiators do not need to implement custom ways of applying substitutions (previously the arithmetic instantiator was). (5) applySubstitutionToLiteral is automatically called on all literals (see line 297 of ceg_instantiator.cpp). This means that BvInstantiator::processAssertion is now called on substituted literals. So for instance if our context contains two literals: x = bv2, bvmul(x,y) = bv4 Say we are asked to solve for x first, and return the substitution {x -> bv2}, then if we are later asked to solve for y, we will call processAssertion for the literal bvmul(bv2,y)=bv4 (6) LIA-specific information "d_theta" in SolvedForm is encapsulated inside the class (with the understanding that this will be made virtual). This commit has no impact on quantified LIA / LRA: https://www.starexec.org/starexec/secure/details/job.jsp?id=24480 (see CVC4-092217-cegqiRefactorSubs) --- src/theory/quantifiers/ceg_instantiator.cpp | 179 +++++++++++------- src/theory/quantifiers/ceg_instantiator.h | 136 +++++++++++--- src/theory/quantifiers/ceg_t_instantiator.cpp | 254 ++++++++++++-------------- 3 files changed, 330 insertions(+), 239 deletions(-) (limited to 'src') diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 42394122e..9375ffb74 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -123,8 +123,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e } if( needsPostprocess ){ //must make copy so that backtracking reverts sf - SolvedForm sf_tmp; - sf_tmp.copy( sf ); + SolvedForm sf_tmp = sf; bool postProcessSuccess = true; for( std::map< Instantiator *, Node >::iterator itp = pp_inst.begin(); itp != pp_inst.end(); ++itp ){ if( !itp->first->postProcessInstantiation( this, sf_tmp, itp->second, effort ) ){ @@ -293,13 +292,18 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e Node lit = ita->second[j]; if( std::find( lits.begin(), lits.end(), lit )==lits.end() ){ lits.push_back( lit ); - //if( vinst->hasProcessAssertion( this, sf, pv, lit, effort ) ){ - // apply substitutions check if eligible and contains pv - // TODO - if( vinst->processAssertion( this, sf, pv, lit, effort ) ){ - return true; + if( vinst->hasProcessAssertion( this, sf, pv, lit, effort ) ){ + // apply substitutions + Node slit = applySubstitutionToLiteral( lit, sf ); + if( !slit.isNull() ){ + // check if contains pv + if( hasVariable( slit, pv ) ){ + if( vinst->processAssertion( this, sf, pv, slit, effort ) ){ + return true; + } + } } - //} + } } } } @@ -356,10 +360,8 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv Trace("cbqi-inst") << " "; } Trace("cbqi-inst") << sf.d_subs.size() << ": "; - if( !pv_prop.d_coeff.isNull() ){ - Trace("cbqi-inst") << pv_prop.d_coeff << " * "; - } - Trace("cbqi-inst") << pv << " -> " << n << std::endl; + Node mod_pv = pv_prop.getModifiedTerm( pv ); + Trace("cbqi-inst") << mod_pv << " -> " << n << std::endl; Assert( n.getType().isSubtypeOf( pv.getType() ) ); } //must ensure variables have been computed for n @@ -372,17 +374,17 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv std::vector< Node > a_var; a_var.push_back( pv ); std::vector< TermProperties > a_prop; - std::vector< Node > a_has_coeff; - if( !pv_prop.d_coeff.isNull() ){ - a_prop.push_back( pv_prop ); - a_has_coeff.push_back( pv ); + a_prop.push_back( pv_prop ); + std::vector< Node > a_non_basic; + if( !pv_prop.isBasic() ){ + a_non_basic.push_back( pv ); } bool success = true; std::map< int, Node > prev_subs; 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; + std::vector< Node > new_non_basic; + Trace("cbqi-inst-debug2") << "Applying substitutions to previous substitution terms..." << std::endl; for( unsigned j=0; jmkNode( MULT, sf.d_props[j].d_coeff, a_pv_prop.d_coeff ) ); + // if previously was basic, becomes non-basic + if( sf.d_props[j].isBasic() ){ + Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), sf.d_vars[j] )==sf.d_non_basic.end() ); + new_non_basic.push_back( sf.d_vars[j] ); + sf.d_non_basic.push_back( sf.d_vars[j] ); } + // now combine the property + sf.d_props[j].combineProperty( a_pv_prop ); + Assert( !sf.d_props[j].isBasic() ); } if( sf.d_subs[j]!=prev_subs[j] ){ computeProgVars( sf.d_subs[j] ); @@ -423,21 +426,9 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv if( success ){ Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl; sf.push_back( pv, n, pv_prop ); - Node prev_theta = sf.d_theta; - Node new_theta = sf.d_theta; - if( !pv_prop.d_coeff.isNull() ){ - if( new_theta.isNull() ){ - new_theta = pv_prop.d_coeff; - }else{ - new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, pv_prop.d_coeff ); - new_theta = Rewriter::rewrite( new_theta ); - } - } - sf.d_theta = new_theta; Trace("cbqi-inst-debug2") << "Recurse..." << std::endl; unsigned i = d_curr_index[pv]; success = doAddInstantiation( sf, d_stack_vars.empty() ? i+1 : i, effort ); - sf.d_theta = prev_theta; if( !success ){ Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl; sf.pop_back( pv, n, pv_prop ); @@ -454,8 +445,8 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv 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< TermProperties >& prop, std::vector< Node >& has_coeff, - std::vector< Node >& vars, TermProperties& pv_prop, bool try_coeff ) { +bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){ Assert( d_prog_var.find( n )!=d_prog_var.end() ); - Assert( n==Rewriter::rewrite( n ) ); - bool req_coeff = false; - if( !has_coeff.empty() ){ + if( !non_basic.empty() ){ for( std::map< Node, bool >::iterator it = d_prog_var[n].begin(); it != d_prog_var[n].end(); ++it ){ - if( std::find( has_coeff.begin(), has_coeff.end(), it->first )!=has_coeff.end() ){ - req_coeff = true; - break; + if( std::find( non_basic.begin(), non_basic.end(), it->first )!=non_basic.end() ){ + return false; } } } + return true; +} + +Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, + std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff ) { + computeProgVars( n ); + Assert( n==Rewriter::rewrite( n ) ); + bool is_basic = canApplyBasicSubstitution( n, non_basic ); if( Trace.isOn("cegqi-si-apply-subs-debug") ){ - Trace("cegqi-si-apply-subs-debug") << "req_coeff = " << req_coeff << " " << tn << std::endl; + Trace("cegqi-si-apply-subs-debug") << "is_basic = " << is_basic << " " << tn << std::endl; for( unsigned i=0; i " << subs[i] << " types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl; Assert( subs[i].getType().isSubtypeOf( vars[i].getType() ) ); } } - - if( !req_coeff ){ - Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - if( n!=nret ){ - nret = Rewriter::rewrite( nret ); - } - return nret; + Node nret; + if( is_basic ){ + nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); }else{ if( !tn.isInteger() ){ //can do basic substitution instead with divisions @@ -529,7 +520,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node if( !prop[i].d_coeff.isNull() ){ Assert( vars[i].getType().isInteger() ); Assert( prop[i].d_coeff.isConst() ); - Node nn =NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/prop[i].d_coeff.getConst() ) ); + 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 ); @@ -537,11 +528,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node 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; + nret = n.substitute( vars.begin(), vars.end(), nsubs.begin(), nsubs.end() ); }else if( try_coeff ){ //must convert to monomial representation std::map< Node, Node > msum; @@ -596,14 +583,14 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node children.push_back( c ); Trace("cegqi-si-apply-subs-debug") << "Add child : " << c << std::endl; } - Node nret = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children ); - nret = Rewriter::rewrite( nret ); + Node nretc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children ); + nretc = Rewriter::rewrite( nretc ); //ensure that nret does not contain vars - if( !TermDb::containsTerms( nret, vars ) ){ + if( !TermDb::containsTerms( nretc, vars ) ){ //result is ( nret / pv_prop.d_coeff ) - return nret; + nret = nretc; }else{ - Trace("cegqi-si-apply-subs-debug") << "Failed, since result " << nret << " contains free variable." << std::endl; + Trace("cegqi-si-apply-subs-debug") << "Failed, since result " << nretc << " contains free variable." << std::endl; } }else{ //implies that we have a monomial that has a free variable @@ -613,11 +600,61 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl; } } - // failed to apply the substitution - return Node::null(); } + if( n!=nret && !nret.isNull() ){ + nret = Rewriter::rewrite( nret ); + } + return nret; } +Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& vars, std::vector< Node >& subs, + std::vector< TermProperties >& prop, std::vector< Node >& non_basic ) { + computeProgVars( lit ); + bool is_basic = canApplyBasicSubstitution( lit, non_basic ); + Node lret; + if( is_basic ){ + lret = lit.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + }else{ + Node atom = lit.getKind()==NOT ? lit[0] : lit; + bool pol = lit.getKind()!=NOT; + //arithmetic inequalities and disequalities + if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){ + Assert( atom.getKind()!=GEQ || atom[1].isConst() ); + Node atom_lhs; + Node atom_rhs; + if( atom.getKind()==GEQ ){ + atom_lhs = atom[0]; + atom_rhs = atom[1]; + }else{ + atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); + atom_lhs = Rewriter::rewrite( atom_lhs ); + atom_rhs = getQuantifiersEngine()->getTermDatabase()->d_zero; + } + //must be an eligible term + if( isEligible( atom_lhs ) ){ + //apply substitution to LHS of atom + TermProperties atom_lhs_prop; + atom_lhs = applySubstitution( NodeManager::currentNM()->realType(), atom_lhs, vars, subs, prop, non_basic, atom_lhs_prop ); + if( !atom_lhs.isNull() ){ + if( !atom_lhs_prop.d_coeff.isNull() ){ + atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_prop.d_coeff, atom_rhs ) ); + } + lret = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); + if( !pol ){ + lret = lret.negate(); + } + } + } + }else{ + // don't know how to apply substitution to literal + } + } + if( lit!=lret && !lret.isNull() ){ + lret = Rewriter::rewrite( lret ); + } + return lret; +} + bool CegInstantiator::check() { if( d_qe->getTheoryEngine()->needCheck() ){ Trace("cbqi-engine") << " CEGQI instantiator : wait until all ground theories are finished." << std::endl; diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index bf555916f..8ffba8d7b 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -52,38 +52,81 @@ public: 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; } + virtual Node getCacheNode() const { return d_coeff; } + // is non-basic + virtual bool isBasic() const { return d_coeff.isNull(); } + // get modified term + virtual Node getModifiedTerm( Node pv ) const { + if( !d_coeff.isNull() ){ + return NodeManager::currentNM()->mkNode( kind::MULT, d_coeff, pv ); + }else{ + return pv; + } + } + // combine property + virtual void combineProperty( TermProperties& p ){ + if( !p.d_coeff.isNull() ){ + if( d_coeff.isNull() ){ + d_coeff = p.d_coeff; + }else{ + d_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, d_coeff, p.d_coeff ) ); + } + } + } }; -//solved form, involves substitution with coefficients +//Solved form +// This specifies a substitution: +// { d_props[i].getModifiedTerm(d_vars[i]) -> d_subs[i] | i = 0...|d_vars| } class SolvedForm { public: + // list of variables std::vector< Node > d_vars; + // list of terms that they are substituted to std::vector< Node > d_subs; + // properties for each variable std::vector< TermProperties > d_props; - std::vector< Node > d_has_coeff; - 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_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; - } + // the variables that have non-basic information regarding how they are substituted + // an example is for linear arithmetic, we store "substitution with coefficients". + std::vector< Node > d_non_basic; + // push the substitution pv_prop.getModifiedTerm(pv) -> n void push_back( Node pv, Node n, TermProperties& pv_prop ){ d_vars.push_back( pv ); d_subs.push_back( n ); d_props.push_back( pv_prop ); - if( !pv_prop.d_coeff.isNull() ){ - d_has_coeff.push_back( pv ); + if( !pv_prop.isBasic() ){ + d_non_basic.push_back( pv ); + // update theta value + Node new_theta = getTheta(); + if( new_theta.isNull() ){ + new_theta = pv_prop.d_coeff; + }else{ + new_theta = NodeManager::currentNM()->mkNode( kind::MULT, new_theta, pv_prop.d_coeff ); + new_theta = Rewriter::rewrite( new_theta ); + } + d_theta.push_back( new_theta ); } } + // pop the substitution pv_prop.getModifiedTerm(pv) -> n void pop_back( Node pv, Node n, TermProperties& pv_prop ){ d_vars.pop_back(); d_subs.pop_back(); d_props.pop_back(); - if( !pv_prop.d_coeff.isNull() ){ - d_has_coeff.pop_back(); + if( !pv_prop.isBasic() ){ + d_non_basic.pop_back(); + // update theta value + d_theta.pop_back(); + } + } +public: + // theta values (for LIA, see Section 4 of Reynolds/King/Kuncak FMSD 2017) + std::vector< Node > d_theta; + // get the current value for theta (for LIA, see Section 4 of Reynolds/King/Kuncak FMSD 2017) + Node getTheta() { + if( d_theta.empty() ){ + return Node::null(); + }else{ + return d_theta[d_theta.size()-1]; } } }; @@ -138,6 +181,32 @@ private: //process void processAssertions(); void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); +private: + /** can use basic substitution */ + bool canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ); + /** apply substitution + * We wish to process the substitution: + * ( pv = n * sf ) + * where pv is a variable with type tn, and * denotes application of substitution. + * The return value "ret" and pv_prop is such that the above equality is equivalent to + * ( pv_prop.getModifiedTerm(pv) = ret ) + */ + Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, TermProperties& pv_prop, bool try_coeff = true ) { + return applySubstitution( tn, n, sf.d_vars, sf.d_subs, sf.d_props, sf.d_non_basic, pv_prop, try_coeff ); + } + /** apply substitution, with solved form expanded to subs/prop/non_basic/vars */ + Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, + std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff = true ); + /** apply substitution to literal lit + * The return value is equivalent to ( lit * sf ) + * where * denotes application of substitution. + */ + Node applySubstitutionToLiteral( Node lit, SolvedForm& sf ) { + return applySubstitutionToLiteral( lit, sf.d_vars, sf.d_subs, sf.d_props, sf.d_non_basic ); + } + /** apply substitution to literal lit, with solved form expanded to subs/prop/non_basic/vars */ + Node applySubstitutionToLiteral( Node lit, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, + std::vector< Node >& non_basic ); public: CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true ); virtual ~CegInstantiator(); @@ -158,12 +227,6 @@ public: void popStackVariable(); 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, 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< 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]; } @@ -188,30 +251,43 @@ public: virtual ~Instantiator(){} virtual void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {} - //called when pv_prop.d_coeff * pv = n, and n is eligible for instantiation + // Called when the entailment: + // E |= pv_prop.getModifiedTerm(pv) = n + // holds in the current context E, 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 + // Called about process equal term, where eqc is the list of eligible terms in the equivalence class of pv virtual bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { return false; } + // whether the instantiator implements processEquality virtual bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } - //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 + // term_props.size() = terms.size() = 2 + // Called when the entailment: + // E ^ term_props[0].getModifiedTerm(x0) = terms[0] ^ term_props[1].getModifiedTerm(x1) = terms[1] |= x0 = x1 + // holds in current context E for fresh variables xi, terms[i] are eligible, and at least one terms[i] contains pv for i = 0,1. + // Notice in the basic case, E |= terms[0] = terms[1]. + // Returns true if an instantiation was successfully added via a recursive call virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) { return false; } + // whether the instantiator implements processAssertion for any literal virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } + // whether the instantiator implements processAssertion for literal lit virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { return false; } - //called when assertion lit holds. note that lit is unsubstituted, first must substitute/solve/check eligible - // returns true if an instantiation was successfully added via a recursive call + // Called when the entailment: + // E |= lit + // holds in current context E. Typically, lit belongs to the list of current assertions. + // Returns true if an instantiation was successfully added via a recursive call virtual bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { return false; } + // Called after processAssertion is called for each literal asserted to the instantiator. virtual bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { return false; } - //do we allow instantiation for the model value of pv + //do we use the model value as instantiation for pv virtual bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } + //do we allow the model value as instantiation for pv virtual bool allowModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return d_closed_enum_type; } - //do we need to postprocess the solved form? did we successfully postprocess + //do we need to postprocess the solved form for pv? virtual bool needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } + // propocess the solved form for pv, returns true if we successfully postprocessed virtual bool postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } /** Identify this module (for debugging) */ diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index 130d73af6..6f94249ef 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -271,136 +271,109 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node atom = lit.getKind()==NOT ? lit[0] : lit; bool pol = lit.getKind()!=NOT; //arithmetic inequalities and disequalities - if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){ - Assert( atom.getKind()!=GEQ || atom[1].isConst() ); - Node atom_lhs; - Node atom_rhs; - if( atom.getKind()==GEQ ){ - atom_lhs = atom[0]; - atom_rhs = atom[1]; - }else{ - atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); - atom_lhs = Rewriter::rewrite( atom_lhs ); - atom_rhs = ci->getQuantifiersEngine()->getTermDatabase()->d_zero; - } - //must be an eligible term - if( ci->isEligible( atom_lhs ) ){ - //apply substitution to LHS of atom - TermProperties atom_lhs_prop; - atom_lhs = ci->applySubstitution( d_type, atom_lhs, sf, atom_lhs_prop ); - if( !atom_lhs.isNull() ){ - if( !atom_lhs_prop.d_coeff.isNull() ){ - atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_prop.d_coeff, atom_rhs ) ); + Assert( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ); + // get model value for pv + Node pv_value = ci->getModelValue( pv ); + //cannot contain infinity? + Trace("cbqi-inst-debug") << "..[3] Substituted assertion : " << atom << ", pol = " << pol << std::endl; + Node vts_coeff_inf; + Node vts_coeff_delta; + Node val; + TermProperties pv_prop; + //isolate pv in the inequality + int ires = solve_arith( ci, pv, atom, 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; + for( unsigned r=0; rmkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else{ + Assert( d_type.isReal() ); + //now is strict inequality + uires = uires*2; + } } - } - //if it contains pv, not infinity - if( !atom_lhs.isNull() && ci->hasVariable( atom_lhs, pv ) ){ - Node pv_value = ci->getModelValue( pv ); - Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); - //cannot contain infinity? - Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl; - Trace("cbqi-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; - Node vts_coeff_inf; - Node vts_coeff_delta; - Node val; - TermProperties pv_prop; - //isolate pv in the inequality - 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; - for( unsigned r=0; rmkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else{ - Assert( d_type.isReal() ); - //now is strict inequality - uires = uires*2; - } - } - }else{ - bool is_upper; - 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 rhs_value = ci->getModelValue( val ); - Node lhs_value = pv_value; - 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; - 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!=ci->getQuantifiersEngine()->getTermDatabase()->d_true ); - } - }else{ - is_upper = (r==0); - } - Assert( atom.getKind()==EQUAL && !pol ); - if( d_type.isInteger() ){ - uires = is_upper ? -1 : 1; - uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else{ - Assert( d_type.isReal() ); - uires = is_upper ? -2 : 2; - } - } - Trace("cbqi-bound-inf") << "From " << lit << ", got : "; - 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 - if( ci->useVtsDelta() && ( uires==2 || uires==-2 ) ){ - if( options::cbqiModel() ){ - 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 ); - } - }else{ - Node delta = ci->getQuantifiersEngine()->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; - d_mbp_bounds[index].push_back( uval ); - 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 - pv_prop.d_type = uires>0 ? 1 : -1; - if( ci->doAddInstantiationInc( pv, uval, pv_prop, sf, effort ) ){ - return true; - } + }else{ + bool is_upper; + 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 rhs_value = ci->getModelValue( val ); + Node lhs_value = pv_prop.getModifiedTerm( pv_value ); + if( !pv_prop.isBasic() ){ + lhs_value = pv_prop.getModifiedTerm( pv_value ); + 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!=ci->getQuantifiersEngine()->getTermDatabase()->d_true ); } + }else{ + is_upper = (r==0); + } + Assert( atom.getKind()==EQUAL && !pol ); + if( d_type.isInteger() ){ + uires = is_upper ? -1 : 1; + uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else{ + Assert( d_type.isReal() ); + uires = is_upper ? -2 : 2; + } + } + if( Trace.isOn("cbqi-bound-inf") ){ + Node pvmod = pv_prop.getModifiedTerm( pv ); + Trace("cbqi-bound-inf") << "From " << lit << ", got : "; + Trace("cbqi-bound-inf") << pvmod << " -> " << uval << ", styp = " << uires << std::endl; + } + //take into account delta + if( ci->useVtsDelta() && ( uires==2 || uires==-2 ) ){ + if( options::cbqiModel() ){ + 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 ); + } + }else{ + Node delta = ci->getQuantifiersEngine()->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; + d_mbp_bounds[index].push_back( uval ); + 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 + pv_prop.d_type = uires>0 ? 1 : -1; + if( ci->doAddInstantiationInc( pv, uval, pv_prop, sf, effort ) ){ + return true; } } } @@ -528,7 +501,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, //if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict if( !options::cbqiMidpoint() || d_type.isInteger() || d_mbp_vts_coeff[rr][1][best].isNull() ){ Node val = d_mbp_bounds[rr][best]; - val = getModelBasedProjectionValue( ci, pv, val, rr==0, d_mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.d_theta, + val = getModelBasedProjectionValue( ci, pv, val, rr==0, d_mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.getTheta(), d_mbp_vts_coeff[rr][0][best], d_mbp_vts_coeff[rr][1][best] ); if( !val.isNull() ){ TermProperties pv_prop_bound; @@ -546,7 +519,8 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, if( !use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty() ){ Node val = zero; 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() ); + Node theta = sf.getTheta(); + val = getModelBasedProjectionValue( ci, pv, val, true, pv_prop_zero.d_coeff, pv_value, zero, sf.getTheta(), Node::null(), Node::null() ); if( !val.isNull() ){ if( ci->doAddInstantiationInc( pv, val, pv_prop_zero, sf, effort ) ){ return true; @@ -563,7 +537,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, bothBounds = false; }else{ vals[rr] = d_mbp_bounds[rr][best]; - vals[rr] = getModelBasedProjectionValue( ci, pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], sf.d_theta, + vals[rr] = getModelBasedProjectionValue( ci, pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], sf.getTheta(), d_mbp_vts_coeff[rr][0][best], Node::null() ); } Trace("cbqi-bound") << "Bound : " << vals[rr] << std::endl; @@ -605,7 +579,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, int rr = upper_first ? (1-r) : r; for( unsigned j=0; j