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)
}
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 ) ){
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;
+ }
+ }
}
- //}
+ }
}
}
}
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
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; j<sf.d_subs.size(); j++ ){
Trace("cbqi-inst-debug2") << " Apply for " << sf.d_subs[j] << std::endl;
Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() );
TNode tv = pv;
TNode ts = n;
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 );
+ Node new_subs = applySubstitution( sf.d_vars[j].getType(), sf.d_subs[j], a_var, a_subs, a_prop, a_non_basic, a_pv_prop, true );
if( !new_subs.isNull() ){
sf.d_subs[j] = new_subs;
- if( !a_pv_prop.d_coeff.isNull() ){
+ // the substitution apply to this term resulted in a non-basic substitution relationship
+ if( !a_pv_prop.isBasic() ){
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_props[j].d_coeff = a_pv_prop.d_coeff;
- }else{
- sf.d_props[j].d_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkNode( 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] );
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 );
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<new_has_coeff.size(); i++ ){
- sf.d_has_coeff.pop_back();
+ for( unsigned i=0; i<new_non_basic.size(); i++ ){
+ sf.d_non_basic.pop_back();
}
return false;
}
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.size(); i++ ){
Trace("cegqi-si-apply-subs-debug") << " " << vars[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
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<Rational>() ) );
+ Node nn = NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/prop[i].d_coeff.getConst<Rational>() ) );
nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn );
nn = Rewriter::rewrite( nn );
nsubs.push_back( nn );
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;
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
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;
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];
}
}
};
//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();
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]; }
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) */
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; r<rmax; r++ ){
+ int uires = ires;
+ Node uval = val;
+ if( atom.getKind()==GEQ ){
+ //push negation downwards
+ if( !pol ){
+ uires = -ires;
+ if( d_type.isInteger() ){
+ uval = NodeManager::currentNM()->mkNode( 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; r<rmax; r++ ){
- int uires = ires;
- Node uval = val;
- if( atom.getKind()==GEQ ){
- //push negation downwards
- if( !pol ){
- uires = -ires;
- if( d_type.isInteger() ){
- uval = NodeManager::currentNM()->mkNode( 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<Rational>().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<Rational>().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;
}
}
}
//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;
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;
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;
int rr = upper_first ? (1-r) : r;
for( unsigned j=0; j<d_mbp_bounds[rr].size(); j++ ){
if( (int)j!=best_used[rr] && ( !options::cbqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull() ) ){
- 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,
+ Node val = getModelBasedProjectionValue( ci, pv, d_mbp_bounds[rr][j], rr==0, d_mbp_coeff[rr][j], pv_value, t_values[rr][j], sf.getTheta(),
d_mbp_vts_coeff[rr][0][j], d_mbp_vts_coeff[rr][1][j] );
if( !val.isNull() ){
TermProperties pv_prop_nopt_bound;
}
bool ArithInstantiator::needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
- return std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), pv )!=sf.d_has_coeff.end();
+ return std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end();
}
bool ArithInstantiator::postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
- Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), pv )!=sf.d_has_coeff.end() );
+ Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.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_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_props[index].isBasic() );
+ Node eq_lhs = sf.d_props[index].getModifiedTerm( sf.d_vars[index] );
+ if( Trace.isOn("cbqi-inst-debug") ){
+ Trace("cbqi-inst-debug") << "Normalize substitution for ";
+ Trace("cbqi-inst-debug") << eq_lhs << " = " << 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_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 );
bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ) {
if( options::quantEprMatching() ){
- Assert( pv_prop.d_coeff.isNull() );
+ Assert( pv_prop.isBasic() );
d_equal_terms.push_back( n );
return false;
}else{
}
bool BvInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) {
+ Assert( term_props[0].isBasic() );
+ Assert( term_props[1].isBasic() );
//processLiteral( ci, sf, pv, terms[0].eqNode( terms[1] ), effort );
return false;
}
projects / cvc5.git / commitdiff