summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ceg_instantiator.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2017-09-25 19:43:27 -0500
committerAndres Noetzli <andres.noetzli@gmail.com>2017-09-25 17:43:27 -0700
commit25e598ed369ee2cc6227dbfb67f7d38303a7144a (patch)
tree0ac0eab8b3c6990c5918ec02a03cd0399338238d /src/theory/quantifiers/ceg_instantiator.cpp
parent1a6f5f0ceaf9360fd1645f9162949d17a8250309 (diff)
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)
Diffstat (limited to 'src/theory/quantifiers/ceg_instantiator.cpp')
-rw-r--r--src/theory/quantifiers/ceg_instantiator.cpp179
1 files changed, 108 insertions, 71 deletions
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; 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() );
@@ -391,20 +393,21 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv
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] );
@@ -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<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;
}
@@ -493,33 +484,33 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& 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.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
@@ -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<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 );
@@ -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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback