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 +++++++++++++++++----------- 1 file changed, 108 insertions(+), 71 deletions(-) (limited to 'src/theory/quantifiers/ceg_instantiator.cpp') 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; -- cgit v1.2.3