diff options
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 699 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.h | 53 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 767 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 54 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 97 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 17 | ||||
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 22 | ||||
| -rw-r--r-- | src/theory/quantifiers_engine.h | 6 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 14 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.h | 2 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 6 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 6 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/delta-simp.smt2 | 5 |
14 files changed, 953 insertions, 798 deletions
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index ef2e3005e..4308e5172 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -32,699 +32,6 @@ using namespace std; namespace CVC4 { -CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out ) : d_qe( qe ), d_out( out ){ - d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); - d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); - d_true = NodeManager::currentNM()->mkConst( true ); -} - -void CegInstantiator::computeProgVars( Node n ){ - if( d_prog_var.find( n )==d_prog_var.end() ){ - d_prog_var[n].clear(); - if( std::find( d_vars.begin(), d_vars.end(), n )!=d_vars.end() ){ - d_prog_var[n][n] = true; - }else if( !d_out->isEligibleForInstantiation( n ) ){ - d_inelig[n] = true; - return; - } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - computeProgVars( n[i] ); - if( d_inelig.find( n[i] )!=d_inelig.end() ){ - d_inelig[n] = true; - return; - } - if( d_has_delta.find( n[i] )!=d_has_delta.end() ){ - d_has_delta[n] = true; - } - for( std::map< Node, bool >::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){ - d_prog_var[n][it->first] = true; - } - } - if( n==d_n_delta ){ - d_has_delta[n] = true; - } - } -} - -bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned i, unsigned effort ){ - if( i==d_vars.size() ){ - return addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, 0 ); - }else{ - eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine(); - std::map< int, std::map< Node, std::map< Node, bool > > > subs_proc; - //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]]; - Node pv = d_vars[i]; - TypeNode pvtn = pv.getType(); - - if( (i+1)<d_vars.size() || effort!=2 ){ - //[1] easy case : pv is in the equivalence class as another term not containing pv - if( ee->hasTerm( pv ) ){ - Node pvr = ee->getRepresentative( pv ); - eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee ); - while( !eqc_i.isFinished() ){ - Node n = *eqc_i; - if( n!=pv ){ - Trace("cegqi-si-inst-debug") << "[1] " << i << "...try based on equal term " << n << std::endl; - //compute d_subs_fv, which program variables are contained in n - computeProgVars( n ); - //must be an eligible term - if( d_inelig.find( n )==d_inelig.end() ){ - Node ns; - Node pv_coeff; //coefficient of pv in the equality we solve (null is 1) - bool proc = false; - if( !d_prog_var[n].empty() ){ - ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff, false ); - if( !ns.isNull() ){ - computeProgVars( ns ); - //substituted version must be new and cannot contain pv - proc = subs_proc[0][pv_coeff].find( ns )==subs_proc[0][pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end(); - } - }else{ - ns = n; - proc = true; - } - if( d_has_delta.find( ns )!=d_has_delta.end() ){ - //also must set delta to zero - ns = ns.substitute( (TNode)d_n_delta, (TNode)d_zero ); - ns = Rewriter::rewrite( ns ); - computeProgVars( ns ); - } - if( proc ){ - //try the substitution - subs_proc[0][ns][pv_coeff] = true; - if( addInstantiationInc( ns, pv, pv_coeff, 0, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){ - return true; - } - } - } - } - ++eqc_i; - } - } - - //[2] : we can solve an equality for pv - ///iterate over equivalence classes to find cases where we can solve for the variable - if( pvtn.isInteger() || pvtn.isReal() ){ - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); - while( !eqcs_i.isFinished() ){ - Node r = *eqcs_i; - TypeNode rtn = r.getType(); - if( rtn.isInteger() || rtn.isReal() ){ - std::vector< Node > lhs; - std::vector< bool > lhs_v; - std::vector< Node > lhs_coeff; - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); - while( !eqc_i.isFinished() ){ - Node n = *eqc_i; - computeProgVars( n ); - //must be an eligible term - if( d_inelig.find( n )==d_inelig.end() ){ - Node ns; - Node pv_coeff; - if( !d_prog_var[n].empty() ){ - ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff ); - if( !ns.isNull() ){ - computeProgVars( ns ); - } - }else{ - ns = n; - } - if( !ns.isNull() ){ - bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); - for( unsigned j=0; j<lhs.size(); j++ ){ - //if this term or the another has pv in it, try to solve for it - if( hasVar || lhs_v[j] ){ - Trace("cegqi-si-inst-debug") << "[2] " << i << "...try based on equality " << lhs[j] << " " << ns << std::endl; - Node eq_lhs = lhs[j]; - Node eq_rhs = ns; - //make the same coefficient - if( pv_coeff!=lhs_coeff[j] ){ - if( !pv_coeff.isNull() ){ - Trace("cegqi-si-inst-debug") << "...mult lhs by " << pv_coeff << std::endl; - eq_lhs = NodeManager::currentNM()->mkNode( MULT, pv_coeff, eq_lhs ); - eq_lhs = Rewriter::rewrite( eq_lhs ); - } - if( !lhs_coeff[j].isNull() ){ - Trace("cegqi-si-inst-debug") << "...mult rhs by " << lhs_coeff[j] << std::endl; - eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff[j], eq_rhs ); - eq_rhs = Rewriter::rewrite( eq_rhs ); - } - } - Node eq = eq_lhs.eqNode( eq_rhs ); - eq = Rewriter::rewrite( eq ); - Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( eq, msum ) ){ - if( !d_n_delta.isNull() ){ - msum.erase( d_n_delta ); - } - if( Trace.isOn("cegqi-si-inst-debug") ){ - Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); - Trace("cegqi-si-inst-debug") << "isolate for " << pv << "..." << std::endl; - } - Node veq; - if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){ - Trace("cegqi-si-inst-debug") << "...isolated equality " << veq << "." << std::endl; - Node veq_c; - if( veq[0]!=pv ){ - Node veq_v; - if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ - Assert( veq_v==pv ); - } - } - if( subs_proc[0][veq[1]].find( veq_c )==subs_proc[0][veq[1]].end() ){ - subs_proc[0][veq[1]][veq_c] = true; - if( addInstantiationInc( veq[1], pv, veq_c, 0, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){ - return true; - } - } - } - } - } - } - lhs.push_back( ns ); - lhs_v.push_back( hasVar ); - lhs_coeff.push_back( pv_coeff ); - } - } - ++eqc_i; - } - } - ++eqcs_i; - } - } - - //[3] directly look at assertions - unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2; - for( unsigned r=0; r<rmax; r++ ){ - TheoryId tid = r==0 ? Theory::theoryOf( pv ) : Theory::theoryOf( pv.getType() ); - Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid ); - Trace("cegqi-si-inst-debug2") << "Theory of " << pv << " (r=" << r << ") is " << tid << std::endl; - if (theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid)) { - Trace("cegqi-si-inst-debug2") << "Look at assertions of " << tid << std::endl; - context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); - for (unsigned j = 0; it != it_end; ++ it, ++j) { - Node lit = (*it).assertion; - Trace("cegqi-si-inst-debug2") << " look at " << lit << std::endl; - 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().isInteger() || 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 = d_zero; - } - - computeProgVars( atom_lhs ); - //must be an eligible term - if( d_inelig.find( atom_lhs )==d_inelig.end() ){ - //apply substitution to LHS of atom - if( !d_prog_var[atom_lhs].empty() ){ - Node atom_lhs_coeff; - atom_lhs = applySubstitution( atom_lhs, subs, vars, coeff, has_coeff, atom_lhs_coeff ); - if( !atom_lhs.isNull() ){ - computeProgVars( atom_lhs ); - if( !atom_lhs_coeff.isNull() ){ - atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) ); - } - } - } - //if it contains pv - if( !atom_lhs.isNull() && d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){ - Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); - Trace("cegqi-si-inst-debug") << "[3] From assertion : " << atom << ", pol = " << pol << std::endl; - Trace("cegqi-si-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( satom, msum ) ){ - if( !d_n_delta.isNull() ){ - msum.erase( d_n_delta ); - } - if( Trace.isOn("cegqi-si-inst-debug") ){ - Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); - Trace("cegqi-si-inst-debug") << "isolate for " << pv << "..." << std::endl; - } - Node vatom; - //isolate pv in the inequality - int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true ); - if( ires!=0 ){ - Trace("cegqi-si-inst-debug") << "...isolated atom " << vatom << "." << std::endl; - Node val = vatom[ ires==1 ? 1 : 0 ]; - Node pvm = vatom[ ires==1 ? 0 : 1 ]; - //get monomial - Node veq_c; - if( pvm!=pv ){ - Node veq_v; - if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ - Assert( veq_v==pv ); - } - } - //disequalities are both strict upper and lower bounds - unsigned rmax = atom.getKind()==GEQ ? 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( pvtn.isInteger() ){ - uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else if( pvtn.isReal() ){ - //now is strict inequality - uires = uires*2; - }else{ - Assert( false ); - } - } - }else{ - Assert( atom.getKind()==EQUAL && !pol ); - if( pvtn.isInteger() ){ - uires = r==0 ? -1 : 1; - uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else if( pvtn.isReal() ){ - uires = r==0 ? -2 : 2; - }else{ - Assert( false ); - } - } - if( subs_proc[uires][uval].find( veq_c )==subs_proc[uires][uval].end() ){ - subs_proc[uires][uval][veq_c] = true; - if( addInstantiationInc( uval, pv, veq_c, uires, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){ - return true; - } - }else{ - Trace("cegqi-si-inst-debug") << "...already processed." << std::endl; - } - } - } - } - } - } - } - } - } - } - } - - //[4] resort to using value in model - if( effort>0 ){ - Node mv = d_qe->getModel()->getValue( pv ); - Node pv_coeff_m; - Trace("cegqi-si-inst-debug") << i << "[4] ...try model value " << mv << std::endl; - return addInstantiationInc( mv, pv, pv_coeff_m, 9, subs, vars, coeff, has_coeff, subs_typ, i, 1 ); - }else{ - return false; - } - } -} - - -bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned i, unsigned effort ) { - //must ensure variables have been computed for n - computeProgVars( n ); - //substitute into previous substitutions, when applicable - std::vector< Node > a_subs; - a_subs.push_back( n ); - std::vector< Node > a_var; - a_var.push_back( pv ); - std::vector< Node > a_coeff; - std::vector< Node > a_has_coeff; - if( !pv_coeff.isNull() ){ - a_coeff.push_back( pv_coeff ); - a_has_coeff.push_back( pv ); - } - - bool success = true; - std::map< int, Node > prev_subs; - std::map< int, Node > prev_coeff; - std::vector< Node > new_has_coeff; - for( unsigned j=0; j<subs.size(); j++ ){ - Assert( d_prog_var.find( subs[j] )!=d_prog_var.end() ); - if( d_prog_var[subs[j]].find( pv )!=d_prog_var[subs[j]].end() ){ - prev_subs[j] = subs[j]; - TNode tv = pv; - TNode ts = n; - Node a_pv_coeff; - Node new_subs = applySubstitution( subs[j], a_subs, a_var, a_coeff, a_has_coeff, a_pv_coeff, true ); - if( !new_subs.isNull() ){ - subs[j] = new_subs; - if( !a_pv_coeff.isNull() ){ - prev_coeff[j] = coeff[j]; - if( coeff[j].isNull() ){ - Assert( std::find( has_coeff.begin(), has_coeff.end(), vars[j] )==has_coeff.end() ); - //now has coefficient - new_has_coeff.push_back( vars[j] ); - has_coeff.push_back( vars[j] ); - coeff[j] = a_pv_coeff; - }else{ - coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, coeff[j], a_pv_coeff ) ); - } - } - if( subs[j]!=prev_subs[j] ){ - computeProgVars( subs[j] ); - } - }else{ - success = false; - break; - } - } - } - if( success ){ - subs.push_back( n ); - vars.push_back( pv ); - coeff.push_back( pv_coeff ); - if( !pv_coeff.isNull() ){ - has_coeff.push_back( pv ); - } - subs_typ.push_back( styp ); - Trace("cegqi-si-inst-debug") << i << ": "; - if( !pv_coeff.isNull() ){ - Trace("cegqi-si-inst-debug") << pv_coeff << "*"; - } - Trace("cegqi-si-inst-debug") << pv << " -> " << n << std::endl; - success = addInstantiation( subs, vars, coeff, has_coeff, subs_typ, i+1, effort ); - if( !success ){ - subs.pop_back(); - vars.pop_back(); - coeff.pop_back(); - if( !pv_coeff.isNull() ){ - has_coeff.pop_back(); - } - subs_typ.pop_back(); - } - } - if( success ){ - return true; - }else{ - //revert substitution information - for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){ - subs[it->first] = it->second; - } - for( std::map< int, Node >::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){ - coeff[it->first] = it->second; - } - for( unsigned i=0; i<new_has_coeff.size(); i++ ){ - has_coeff.pop_back(); - } - return false; - } -} - -bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, unsigned j ) { - if( j==has_coeff.size() ){ - return addInstantiation( subs, vars, subs_typ ); - }else{ - Assert( std::find( vars.begin(), vars.end(), has_coeff[j] )!=vars.end() ); - unsigned index = std::find( vars.begin(), vars.end(), has_coeff[j] )-vars.begin(); - Node prev = subs[index]; - Assert( !coeff[index].isNull() ); - Trace("cegqi-si-inst-debug") << "Normalize substitution for " << coeff[index] << " * " << vars[index] << " = " << subs[index] << ", stype = " << subs_typ[index] << std::endl; - if( 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, coeff[index], vars[index] ); - Node eq_rhs = subs[index]; - Node eq = eq_lhs.eqNode( eq_rhs ); - eq = Rewriter::rewrite( eq ); - Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( eq, msum ) ){ - Node veq; - if( QuantArith::isolate( vars[index], msum, veq, EQUAL, true )!=0 ){ - Node veq_c; - if( veq[0]!=vars[index] ){ - Node veq_v; - if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ - Assert( veq_v==vars[index] ); - } - } - subs[index] = veq[1]; - if( !veq_c.isNull() ){ - subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c ); - if( subs_typ[index]>=1 && subs_typ[index]<=2 ){ - subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], - NodeManager::currentNM()->mkNode( ITE, - NodeManager::currentNM()->mkNode( EQUAL, - NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), - d_zero ), - d_zero, d_one ) - ); - } - } - Trace("cegqi-si-inst-debug") << "...normalize integers : " << subs[index] << std::endl; - if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){ - return true; - } - //equalities are both upper and lower bounds - /* - if( subs_typ[index]==0 && !veq_c.isNull() ){ - subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], - NodeManager::currentNM()->mkNode( ITE, - NodeManager::currentNM()->mkNode( EQUAL, - NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), - NodeManager::currentNM()->mkConst( Rational( 0 ) ) ), - NodeManager::currentNM()->mkConst( Rational( 0 ) ), - NodeManager::currentNM()->mkConst( Rational( 1 ) ) ) - ); - if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){ - return true; - } - } - */ - } - } - }else if( vars[index].getType().isReal() ){ - // can always invert - subs[index] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / coeff[index].getConst<Rational>() ), subs[index] ); - subs[index] = Rewriter::rewrite( subs[index] ); - Trace("cegqi-si-inst-debug") << "...success, reals : " << subs[index] << std::endl; - if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){ - return true; - } - }else{ - Assert( false ); - } - subs[index] = prev; - Trace("cegqi-si-inst-debug") << "...failed." << std::endl; - return false; - } -} - -bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ ) { - // do delta rationals - std::map< int, Node > prev; - for( unsigned i=0; i<subs.size(); i++ ){ - if( subs_typ[i]==2 || subs_typ[i]==-2 ){ - prev[i] = subs[i]; - if( d_n_delta.isNull() ){ - d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", vars[i].getType(), "delta for cegqi" ); - Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, d_zero ); - d_qe->getOutputChannel().lemma( delta_lem ); - } - subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], d_n_delta ); - d_used_delta = true; - } - } - //check if we have already added this instantiation - bool success = d_out->addInstantiation( subs, subs_typ ); - if( !success ){ - //revert the substitution - for( std::map< int, Node >::iterator it = prev.begin(); it != prev.end(); ++it ){ - subs[it->first] = it->second; - } - } - return success; -} - - -Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff ) { - Assert( d_prog_var.find( n )!=d_prog_var.end() ); - Assert( n==Rewriter::rewrite( n ) ); - bool req_coeff = false; - if( !has_coeff.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( !req_coeff ){ - Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - if( n!=nret ){ - nret = Rewriter::rewrite( nret ); - } - //result is nret - return nret; - }else{ - if( try_coeff ){ - //must convert to monomial representation - std::map< Node, Node > msum; - if( QuantArith::getMonomialSum( n, msum ) ){ - std::map< Node, Node > msum_coeff; - std::map< Node, Node > msum_term; - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - //check if in substitution - std::vector< Node >::iterator its = std::find( vars.begin(), vars.end(), it->first ); - if( its!=vars.end() ){ - int index = its-vars.begin(); - if( coeff[index].isNull() ){ - //apply substitution - msum_term[it->first] = subs[index]; - }else{ - //apply substitution, multiply to ensure no divisibility conflict - msum_term[it->first] = subs[index]; - //relative coefficient - msum_coeff[it->first] = coeff[index]; - if( pv_coeff.isNull() ){ - pv_coeff = coeff[index]; - }else{ - pv_coeff = NodeManager::currentNM()->mkNode( MULT, pv_coeff, coeff[index] ); - } - } - }else{ - msum_term[it->first] = it->first; - } - } - //make sum with normalized coefficient - Assert( !pv_coeff.isNull() ); - pv_coeff = Rewriter::rewrite( pv_coeff ); - Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_coeff << std::endl; - std::vector< Node > children; - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - Node c_coeff; - if( !msum_coeff[it->first].isNull() ){ - c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_coeff.getConst<Rational>() / msum_coeff[it->first].getConst<Rational>() ) ); - }else{ - c_coeff = pv_coeff; - } - if( !it->second.isNull() ){ - c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second ); - } - Node c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] ); - 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 ); - //result is ( nret / pv_coeff ) - return nret; - }else{ - Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl; - } - } - // failed to apply the substitution - return Node::null(); - } -} - -//check if delta has a lower bound L -// if so, add lemma L>0 => L>d -void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) { - return; - /* disable for now - if( !d_n_delta.isNull() ){ - Theory* theory = d_qe->getTheoryEngine()->theoryOf( THEORY_ARITH ); - if( theory && d_qe->getTheoryEngine()->isTheoryEnabled( THEORY_ARITH ) ){ - context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); - for (unsigned j = 0; it != it_end; ++ it, ++j) { - Node lit = (*it).assertion; - Node atom = lit.getKind()==NOT ? lit[0] : lit; - bool pol = lit.getKind()!=NOT; - if( atom.getKind()==GEQ || ( pol && atom.getKind()==EQUAL ) ){ - 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 = d_zero; - } - computeProgVars( atom_lhs ); - //must be an eligible term with delta - if( d_inelig.find( atom_lhs )==d_inelig.end() && d_has_delta.find( atom_lhs )!=d_has_delta.end() ){ - Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); - Trace("cegqi-delta") << "Delta assertion : " << atom << ", pol = " << pol << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( satom, msum ) ){ - Node vatom; - //isolate delta in the inequality - int ires = QuantArith::isolate( d_n_delta, msum, vatom, atom.getKind(), true ); - if( ((ires==1)==pol) || ( ires!=0 && lit.getKind()==EQUAL ) ){ - Node val = vatom[ ires==1 ? 1 : 0 ]; - Node pvm = vatom[ ires==1 ? 0 : 1 ]; - //get monomial - if( pvm!=d_n_delta ){ - Node veq_c; - Node veq_v; - if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ - Assert( veq_v==d_n_delta ); - val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) ); - val = Rewriter::rewrite( val ); - }else{ - val = Node::null(); - } - } - if( !val.isNull() ){ - Node lem1 = NodeManager::currentNM()->mkNode( GT, val, d_zero ); - lem1 = Rewriter::rewrite( lem1 ); - if( !lem1.isConst() || lem1==d_true ){ - Node lem2 = NodeManager::currentNM()->mkNode( GT, val, d_n_delta ); - Node lem = lem1==d_true ? lem2 : NodeManager::currentNM()->mkNode( OR, lem1.negate(), lem2 ); - lems.push_back( lem ); - Trace("cegqi-delta") << "...lemma : " << lem << std::endl; - } - } - }else{ - Trace("cegqi-delta") << "...wrong polarity." << std::endl; - } - } - } - } - } - } - } - */ -} - -bool CegInstantiator::check() { - - for( unsigned r=0; r<2; r++ ){ - std::vector< Node > subs; - std::vector< Node > vars; - std::vector< Node > coeff; - std::vector< Node > has_coeff; - std::vector< int > subs_typ; - //try to add an instantiation - if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, r==0 ? 0 : 2 ) ){ - return true; - } - } - Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; - return false; -} - - bool CegqiOutputSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) { return d_out->addInstantiation( subs, subs_typ ); } @@ -1411,6 +718,12 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v }else{ Trace("cegqi-engine") << siss.str() << std::endl; Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() ); + Node delta = d_qe->getTermDatabase()->getVtsDelta( false, false ); + if( !delta.isNull() && TermDb::containsTerm( lem, delta ) ){ + Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl; + lem = d_qe->getTermDatabase()->rewriteVtsSymbols( lem ); + } + Trace("cegqi-engine-debug") << "Rewrite..." << std::endl; lem = Rewriter::rewrite( lem ); Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl; if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){ diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index f0d00b61c..69981791f 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -21,64 +21,13 @@ #include "context/cdchunk_list.h" #include "theory/quantifiers_engine.h" #include "theory/quantifiers/ce_guided_single_inv_sol.h" +#include "theory/quantifiers/inst_strategy_cbqi.h" namespace CVC4 { namespace theory { namespace quantifiers { class CegConjecture; - -class CegqiOutput -{ -public: - virtual ~CegqiOutput() {} - virtual bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) = 0; - virtual bool isEligibleForInstantiation( Node n ) = 0; - virtual bool addLemma( Node lem ) = 0; -}; - -class CegInstantiator -{ -private: - Node d_zero; - Node d_one; - Node d_true; - QuantifiersEngine * d_qe; - CegqiOutput * d_out; - //program variable contains cache - std::map< Node, std::map< Node, bool > > d_prog_var; - std::map< Node, bool > d_inelig; - std::map< Node, bool > d_has_delta; -private: - //for adding instantiations during check - void computeProgVars( Node n ); - // effort=0 : do not use model value, 1: use model value, 2: one must use model value - bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned i, unsigned effort ); - bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned i, unsigned effort ); - bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned j ); - bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ ); - Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true ); -public: - CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out ); - //the CE variables - std::vector< Node > d_vars; - //delta - Node d_n_delta; - bool d_used_delta; - //check : add instantiations based on valuation of d_vars - bool check(); - // get delta lemmas : on-demand force minimality of d_n_delta - void getDeltaLemmas( std::vector< Node >& lems ); -}; - - class CegConjectureSingleInv; class CegqiOutputSingleInv : public CegqiOutput diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index dab32af71..0c4648e51 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -32,6 +32,700 @@ using namespace CVC4::theory::datatypes; #define ARITH_INSTANTIATOR_USE_MINUS_DELTA + + + +CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out ) : d_qe( qe ), d_out( out ){ + d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); + d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); + d_true = NodeManager::currentNM()->mkConst( true ); +} + +void CegInstantiator::computeProgVars( Node n ){ + if( d_prog_var.find( n )==d_prog_var.end() ){ + d_prog_var[n].clear(); + if( std::find( d_vars.begin(), d_vars.end(), n )!=d_vars.end() ){ + d_prog_var[n][n] = true; + }else if( !d_out->isEligibleForInstantiation( n ) ){ + d_inelig[n] = true; + return; + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + computeProgVars( n[i] ); + if( d_inelig.find( n[i] )!=d_inelig.end() ){ + d_inelig[n] = true; + return; + } + if( d_has_delta.find( n[i] )!=d_has_delta.end() ){ + d_has_delta[n] = true; + } + for( std::map< Node, bool >::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){ + d_prog_var[n][it->first] = true; + } + } + if( n==d_n_delta ){ + d_has_delta[n] = true; + } + } +} + +bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, + unsigned i, unsigned effort ){ + if( i==d_vars.size() ){ + return addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, 0 ); + }else{ + eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine(); + std::map< int, std::map< Node, std::map< Node, bool > > > subs_proc; + //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]]; + Node pv = d_vars[i]; + TypeNode pvtn = pv.getType(); + + if( (i+1)<d_vars.size() || effort!=2 ){ + //[1] easy case : pv is in the equivalence class as another term not containing pv + if( ee->hasTerm( pv ) ){ + Node pvr = ee->getRepresentative( pv ); + eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee ); + while( !eqc_i.isFinished() ){ + Node n = *eqc_i; + if( n!=pv ){ + Trace("cegqi-si-inst-debug") << "[1] " << i << "...try based on equal term " << n << std::endl; + //compute d_subs_fv, which program variables are contained in n + computeProgVars( n ); + //must be an eligible term + if( d_inelig.find( n )==d_inelig.end() ){ + Node ns; + Node pv_coeff; //coefficient of pv in the equality we solve (null is 1) + bool proc = false; + if( !d_prog_var[n].empty() ){ + ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff, false ); + if( !ns.isNull() ){ + computeProgVars( ns ); + //substituted version must be new and cannot contain pv + proc = subs_proc[0][pv_coeff].find( ns )==subs_proc[0][pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end(); + } + }else{ + ns = n; + proc = true; + } + if( d_has_delta.find( ns )!=d_has_delta.end() ){ + //also must set delta to zero + ns = ns.substitute( (TNode)d_n_delta, (TNode)d_zero ); + ns = Rewriter::rewrite( ns ); + computeProgVars( ns ); + } + if( proc ){ + //try the substitution + subs_proc[0][ns][pv_coeff] = true; + if( addInstantiationInc( ns, pv, pv_coeff, 0, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){ + return true; + } + } + } + } + ++eqc_i; + } + } + + //[2] : we can solve an equality for pv + ///iterate over equivalence classes to find cases where we can solve for the variable + if( pvtn.isInteger() || pvtn.isReal() ){ + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); + while( !eqcs_i.isFinished() ){ + Node r = *eqcs_i; + TypeNode rtn = r.getType(); + if( rtn.isInteger() || rtn.isReal() ){ + std::vector< Node > lhs; + std::vector< bool > lhs_v; + std::vector< Node > lhs_coeff; + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( !eqc_i.isFinished() ){ + Node n = *eqc_i; + computeProgVars( n ); + //must be an eligible term + if( d_inelig.find( n )==d_inelig.end() ){ + Node ns; + Node pv_coeff; + if( !d_prog_var[n].empty() ){ + ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff ); + if( !ns.isNull() ){ + computeProgVars( ns ); + } + }else{ + ns = n; + } + if( !ns.isNull() ){ + bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); + for( unsigned j=0; j<lhs.size(); j++ ){ + //if this term or the another has pv in it, try to solve for it + if( hasVar || lhs_v[j] ){ + Trace("cegqi-si-inst-debug") << "[2] " << i << "...try based on equality " << lhs[j] << " " << ns << std::endl; + Node eq_lhs = lhs[j]; + Node eq_rhs = ns; + //make the same coefficient + if( pv_coeff!=lhs_coeff[j] ){ + if( !pv_coeff.isNull() ){ + Trace("cegqi-si-inst-debug") << "...mult lhs by " << pv_coeff << std::endl; + eq_lhs = NodeManager::currentNM()->mkNode( MULT, pv_coeff, eq_lhs ); + eq_lhs = Rewriter::rewrite( eq_lhs ); + } + if( !lhs_coeff[j].isNull() ){ + Trace("cegqi-si-inst-debug") << "...mult rhs by " << lhs_coeff[j] << std::endl; + eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff[j], eq_rhs ); + eq_rhs = Rewriter::rewrite( eq_rhs ); + } + } + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( eq, msum ) ){ + if( !d_n_delta.isNull() ){ + msum.erase( d_n_delta ); + } + if( Trace.isOn("cegqi-si-inst-debug") ){ + Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); + Trace("cegqi-si-inst-debug") << "isolate for " << pv << "..." << std::endl; + } + Node veq; + if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){ + Trace("cegqi-si-inst-debug") << "...isolated equality " << veq << "." << std::endl; + Node veq_c; + if( veq[0]!=pv ){ + Node veq_v; + if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ + Assert( veq_v==pv ); + } + } + if( subs_proc[0][veq[1]].find( veq_c )==subs_proc[0][veq[1]].end() ){ + subs_proc[0][veq[1]][veq_c] = true; + if( addInstantiationInc( veq[1], pv, veq_c, 0, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){ + return true; + } + } + } + } + } + } + lhs.push_back( ns ); + lhs_v.push_back( hasVar ); + lhs_coeff.push_back( pv_coeff ); + } + } + ++eqc_i; + } + } + ++eqcs_i; + } + } + + //[3] directly look at assertions + unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2; + for( unsigned r=0; r<rmax; r++ ){ + TheoryId tid = r==0 ? Theory::theoryOf( pv ) : Theory::theoryOf( pv.getType() ); + Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid ); + Trace("cegqi-si-inst-debug2") << "Theory of " << pv << " (r=" << r << ") is " << tid << std::endl; + if (theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid)) { + Trace("cegqi-si-inst-debug2") << "Look at assertions of " << tid << std::endl; + context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); + for (unsigned j = 0; it != it_end; ++ it, ++j) { + Node lit = (*it).assertion; + Trace("cegqi-si-inst-debug2") << " look at " << lit << std::endl; + 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().isInteger() || 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 = d_zero; + } + + computeProgVars( atom_lhs ); + //must be an eligible term + if( d_inelig.find( atom_lhs )==d_inelig.end() ){ + //apply substitution to LHS of atom + if( !d_prog_var[atom_lhs].empty() ){ + Node atom_lhs_coeff; + atom_lhs = applySubstitution( atom_lhs, subs, vars, coeff, has_coeff, atom_lhs_coeff ); + if( !atom_lhs.isNull() ){ + computeProgVars( atom_lhs ); + if( !atom_lhs_coeff.isNull() ){ + atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) ); + } + } + } + //if it contains pv + if( !atom_lhs.isNull() && d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){ + Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); + Trace("cegqi-si-inst-debug") << "[3] From assertion : " << atom << ", pol = " << pol << std::endl; + Trace("cegqi-si-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( satom, msum ) ){ + if( !d_n_delta.isNull() ){ + msum.erase( d_n_delta ); + } + if( Trace.isOn("cegqi-si-inst-debug") ){ + Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); + Trace("cegqi-si-inst-debug") << "isolate for " << pv << "..." << std::endl; + } + Node vatom; + //isolate pv in the inequality + int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true ); + if( ires!=0 ){ + Trace("cegqi-si-inst-debug") << "...isolated atom " << vatom << "." << std::endl; + Node val = vatom[ ires==1 ? 1 : 0 ]; + Node pvm = vatom[ ires==1 ? 0 : 1 ]; + //get monomial + Node veq_c; + if( pvm!=pv ){ + Node veq_v; + if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ + Assert( veq_v==pv ); + } + } + //disequalities are both strict upper and lower bounds + unsigned rmax = atom.getKind()==GEQ ? 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( pvtn.isInteger() ){ + uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else if( pvtn.isReal() ){ + //now is strict inequality + uires = uires*2; + }else{ + Assert( false ); + } + } + }else{ + Assert( atom.getKind()==EQUAL && !pol ); + if( pvtn.isInteger() ){ + uires = r==0 ? -1 : 1; + uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else if( pvtn.isReal() ){ + uires = r==0 ? -2 : 2; + }else{ + Assert( false ); + } + } + if( subs_proc[uires][uval].find( veq_c )==subs_proc[uires][uval].end() ){ + subs_proc[uires][uval][veq_c] = true; + if( addInstantiationInc( uval, pv, veq_c, uires, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){ + return true; + } + }else{ + Trace("cegqi-si-inst-debug") << "...already processed." << std::endl; + } + } + } + } + } + } + } + } + } + } + } + + //[4] resort to using value in model + if( effort>0 ){ + Node mv = d_qe->getModel()->getValue( pv ); + Node pv_coeff_m; + Trace("cegqi-si-inst-debug") << i << "[4] ...try model value " << mv << std::endl; + return addInstantiationInc( mv, pv, pv_coeff_m, 9, subs, vars, coeff, has_coeff, subs_typ, i, 1 ); + }else{ + return false; + } + } +} + + +bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, + unsigned i, unsigned effort ) { + //must ensure variables have been computed for n + computeProgVars( n ); + //substitute into previous substitutions, when applicable + std::vector< Node > a_subs; + a_subs.push_back( n ); + std::vector< Node > a_var; + a_var.push_back( pv ); + std::vector< Node > a_coeff; + std::vector< Node > a_has_coeff; + if( !pv_coeff.isNull() ){ + a_coeff.push_back( pv_coeff ); + a_has_coeff.push_back( pv ); + } + + bool success = true; + std::map< int, Node > prev_subs; + std::map< int, Node > prev_coeff; + std::vector< Node > new_has_coeff; + for( unsigned j=0; j<subs.size(); j++ ){ + Assert( d_prog_var.find( subs[j] )!=d_prog_var.end() ); + if( d_prog_var[subs[j]].find( pv )!=d_prog_var[subs[j]].end() ){ + prev_subs[j] = subs[j]; + TNode tv = pv; + TNode ts = n; + Node a_pv_coeff; + Node new_subs = applySubstitution( subs[j], a_subs, a_var, a_coeff, a_has_coeff, a_pv_coeff, true ); + if( !new_subs.isNull() ){ + subs[j] = new_subs; + if( !a_pv_coeff.isNull() ){ + prev_coeff[j] = coeff[j]; + if( coeff[j].isNull() ){ + Assert( std::find( has_coeff.begin(), has_coeff.end(), vars[j] )==has_coeff.end() ); + //now has coefficient + new_has_coeff.push_back( vars[j] ); + has_coeff.push_back( vars[j] ); + coeff[j] = a_pv_coeff; + }else{ + coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, coeff[j], a_pv_coeff ) ); + } + } + if( subs[j]!=prev_subs[j] ){ + computeProgVars( subs[j] ); + } + }else{ + success = false; + break; + } + } + } + if( success ){ + subs.push_back( n ); + vars.push_back( pv ); + coeff.push_back( pv_coeff ); + if( !pv_coeff.isNull() ){ + has_coeff.push_back( pv ); + } + subs_typ.push_back( styp ); + Trace("cegqi-si-inst-debug") << i << ": "; + if( !pv_coeff.isNull() ){ + Trace("cegqi-si-inst-debug") << pv_coeff << "*"; + } + Trace("cegqi-si-inst-debug") << pv << " -> " << n << std::endl; + success = addInstantiation( subs, vars, coeff, has_coeff, subs_typ, i+1, effort ); + if( !success ){ + subs.pop_back(); + vars.pop_back(); + coeff.pop_back(); + if( !pv_coeff.isNull() ){ + has_coeff.pop_back(); + } + subs_typ.pop_back(); + } + } + if( success ){ + return true; + }else{ + //revert substitution information + for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){ + subs[it->first] = it->second; + } + for( std::map< int, Node >::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){ + coeff[it->first] = it->second; + } + for( unsigned i=0; i<new_has_coeff.size(); i++ ){ + has_coeff.pop_back(); + } + return false; + } +} + +bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, unsigned j ) { + if( j==has_coeff.size() ){ + return addInstantiation( subs, vars, subs_typ ); + }else{ + Assert( std::find( vars.begin(), vars.end(), has_coeff[j] )!=vars.end() ); + unsigned index = std::find( vars.begin(), vars.end(), has_coeff[j] )-vars.begin(); + Node prev = subs[index]; + Assert( !coeff[index].isNull() ); + Trace("cegqi-si-inst-debug") << "Normalize substitution for " << coeff[index] << " * " << vars[index] << " = " << subs[index] << ", stype = " << subs_typ[index] << std::endl; + if( 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, coeff[index], vars[index] ); + Node eq_rhs = subs[index]; + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( eq, msum ) ){ + Node veq; + if( QuantArith::isolate( vars[index], msum, veq, EQUAL, true )!=0 ){ + Node veq_c; + if( veq[0]!=vars[index] ){ + Node veq_v; + if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ + Assert( veq_v==vars[index] ); + } + } + subs[index] = veq[1]; + if( !veq_c.isNull() ){ + subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c ); + if( subs_typ[index]>=1 && subs_typ[index]<=2 ){ + subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], + NodeManager::currentNM()->mkNode( ITE, + NodeManager::currentNM()->mkNode( EQUAL, + NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), + d_zero ), + d_zero, d_one ) + ); + } + } + Trace("cegqi-si-inst-debug") << "...normalize integers : " << subs[index] << std::endl; + if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){ + return true; + } + //equalities are both upper and lower bounds + /* + if( subs_typ[index]==0 && !veq_c.isNull() ){ + subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], + NodeManager::currentNM()->mkNode( ITE, + NodeManager::currentNM()->mkNode( EQUAL, + NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), + NodeManager::currentNM()->mkConst( Rational( 0 ) ) ), + NodeManager::currentNM()->mkConst( Rational( 0 ) ), + NodeManager::currentNM()->mkConst( Rational( 1 ) ) ) + ); + if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){ + return true; + } + } + */ + } + } + }else if( vars[index].getType().isReal() ){ + // can always invert + subs[index] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / coeff[index].getConst<Rational>() ), subs[index] ); + subs[index] = Rewriter::rewrite( subs[index] ); + Trace("cegqi-si-inst-debug") << "...success, reals : " << subs[index] << std::endl; + if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){ + return true; + } + }else{ + Assert( false ); + } + subs[index] = prev; + Trace("cegqi-si-inst-debug") << "...failed." << std::endl; + return false; + } +} + +bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ ) { + // do delta rationals + std::map< int, Node > prev; + for( unsigned i=0; i<subs.size(); i++ ){ + if( subs_typ[i]==2 || subs_typ[i]==-2 ){ + prev[i] = subs[i]; + Node delta = d_qe->getTermDatabase()->getVtsDelta(); + d_n_delta = delta; + subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], delta ); + } + } + //check if we have already added this instantiation + bool success = d_out->addInstantiation( subs, subs_typ ); + if( !success ){ + //revert the substitution + for( std::map< int, Node >::iterator it = prev.begin(); it != prev.end(); ++it ){ + subs[it->first] = it->second; + } + } + return success; +} + + +Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff ) { + Assert( d_prog_var.find( n )!=d_prog_var.end() ); + Assert( n==Rewriter::rewrite( n ) ); + bool req_coeff = false; + if( !has_coeff.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( !req_coeff ){ + Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + if( n!=nret ){ + nret = Rewriter::rewrite( nret ); + } + //result is nret + return nret; + }else{ + if( try_coeff ){ + //must convert to monomial representation + std::map< Node, Node > msum; + if( QuantArith::getMonomialSum( n, msum ) ){ + std::map< Node, Node > msum_coeff; + std::map< Node, Node > msum_term; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + //check if in substitution + std::vector< Node >::iterator its = std::find( vars.begin(), vars.end(), it->first ); + if( its!=vars.end() ){ + int index = its-vars.begin(); + if( coeff[index].isNull() ){ + //apply substitution + msum_term[it->first] = subs[index]; + }else{ + //apply substitution, multiply to ensure no divisibility conflict + msum_term[it->first] = subs[index]; + //relative coefficient + msum_coeff[it->first] = coeff[index]; + if( pv_coeff.isNull() ){ + pv_coeff = coeff[index]; + }else{ + pv_coeff = NodeManager::currentNM()->mkNode( MULT, pv_coeff, coeff[index] ); + } + } + }else{ + msum_term[it->first] = it->first; + } + } + //make sum with normalized coefficient + Assert( !pv_coeff.isNull() ); + pv_coeff = Rewriter::rewrite( pv_coeff ); + Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_coeff << std::endl; + std::vector< Node > children; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + Node c_coeff; + if( !msum_coeff[it->first].isNull() ){ + c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_coeff.getConst<Rational>() / msum_coeff[it->first].getConst<Rational>() ) ); + }else{ + c_coeff = pv_coeff; + } + if( !it->second.isNull() ){ + c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second ); + } + Node c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] ); + 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 ); + //result is ( nret / pv_coeff ) + return nret; + }else{ + Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl; + } + } + // failed to apply the substitution + return Node::null(); + } +} + +//check if delta has a lower bound L +// if so, add lemma L>0 => L>d +void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) { + return; + /* disable for now + if( !d_n_delta.isNull() ){ + Theory* theory = d_qe->getTheoryEngine()->theoryOf( THEORY_ARITH ); + if( theory && d_qe->getTheoryEngine()->isTheoryEnabled( THEORY_ARITH ) ){ + context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); + for (unsigned j = 0; it != it_end; ++ it, ++j) { + Node lit = (*it).assertion; + Node atom = lit.getKind()==NOT ? lit[0] : lit; + bool pol = lit.getKind()!=NOT; + if( atom.getKind()==GEQ || ( pol && atom.getKind()==EQUAL ) ){ + 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 = d_zero; + } + computeProgVars( atom_lhs ); + //must be an eligible term with delta + if( d_inelig.find( atom_lhs )==d_inelig.end() && d_has_delta.find( atom_lhs )!=d_has_delta.end() ){ + Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); + Trace("cegqi-delta") << "Delta assertion : " << atom << ", pol = " << pol << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( satom, msum ) ){ + Node vatom; + //isolate delta in the inequality + int ires = QuantArith::isolate( d_n_delta, msum, vatom, atom.getKind(), true ); + if( ((ires==1)==pol) || ( ires!=0 && lit.getKind()==EQUAL ) ){ + Node val = vatom[ ires==1 ? 1 : 0 ]; + Node pvm = vatom[ ires==1 ? 0 : 1 ]; + //get monomial + if( pvm!=d_n_delta ){ + Node veq_c; + Node veq_v; + if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ + Assert( veq_v==d_n_delta ); + val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) ); + val = Rewriter::rewrite( val ); + }else{ + val = Node::null(); + } + } + if( !val.isNull() ){ + Node lem1 = NodeManager::currentNM()->mkNode( GT, val, d_zero ); + lem1 = Rewriter::rewrite( lem1 ); + if( !lem1.isConst() || lem1==d_true ){ + Node lem2 = NodeManager::currentNM()->mkNode( GT, val, d_n_delta ); + Node lem = lem1==d_true ? lem2 : NodeManager::currentNM()->mkNode( OR, lem1.negate(), lem2 ); + lems.push_back( lem ); + Trace("cegqi-delta") << "...lemma : " << lem << std::endl; + } + } + }else{ + Trace("cegqi-delta") << "...wrong polarity." << std::endl; + } + } + } + } + } + } + } + */ +} + +bool CegInstantiator::check() { + + for( unsigned r=0; r<2; r++ ){ + std::vector< Node > subs; + std::vector< Node > vars; + std::vector< Node > coeff; + std::vector< Node > has_coeff; + std::vector< int > subs_typ; + //try to add an instantiation + if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, r==0 ? 0 : 2 ) ){ + return true; + } + } + Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; + return false; +} + + +//old implementation + InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) : InstStrategy( ie ), d_th( th ), d_counter( 0 ){ d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) ); @@ -350,6 +1044,8 @@ Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){ +//new implementation + bool CegqiOutputInstStrategy::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) { return d_out->addInstantiation( subs, subs_typ ); } @@ -380,15 +1076,6 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f ); if( it==d_cinst.end() ){ cinst = new CegInstantiator( d_quantEngine, d_out ); - if( d_n_delta.isNull() ){ - d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for cegqi inst strategy" ); - Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); - d_quantEngine->getOutputChannel().lemma( delta_lem ); - d_n_delta_ub = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) ); - Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub ); - d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); - } - cinst->d_n_delta = d_n_delta; for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) ); } @@ -397,37 +1084,47 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { cinst = it->second; } if( d_check_delta_lemma ){ + //minimize the free delta heuristically Trace("inst-alg") << "-> Get delta lemmas for cegqi..." << std::endl; - d_check_delta_lemma = false; - std::vector< Node > dlemmas; - cinst->getDeltaLemmas( dlemmas ); - Trace("inst-alg") << "...got " << dlemmas.size() << " delta lemmas." << std::endl; - if( !dlemmas.empty() ){ - bool addedLemma = false; - for( unsigned i=0; i<dlemmas.size(); i++ ){ - if( addLemma( dlemmas[i] ) ){ - addedLemma = true; - } + Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false ); + if( !delta.isNull() ){ + if( d_n_delta_ub.isNull() ){ + d_n_delta_ub = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) ); } - if( addedLemma ){ - return STATUS_UNKNOWN; + d_check_delta_lemma = false; + std::vector< Node > dlemmas; + cinst->getDeltaLemmas( dlemmas ); + Trace("inst-alg") << "...got " << dlemmas.size() << " delta lemmas." << std::endl; + if( !dlemmas.empty() ){ + bool addedLemma = false; + for( unsigned i=0; i<dlemmas.size(); i++ ){ + if( addLemma( dlemmas[i] ) ){ + addedLemma = true; + } + } + if( addedLemma ){ + return STATUS_UNKNOWN; + } } } } Trace("inst-alg") << "-> Run cegqi for " << f << std::endl; d_curr_quant = f; bool addedLemma = cinst->check(); - d_used_delta = d_used_delta || cinst->d_used_delta; d_curr_quant = Node::null(); return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED; }else if( e==2 ){ - if( d_check_delta_lemma_lc && d_used_delta ){ - d_check_delta_lemma_lc = false; - d_n_delta_ub = NodeManager::currentNM()->mkNode( MULT, d_n_delta_ub, d_n_delta_ub ); - d_n_delta_ub = Rewriter::rewrite( d_n_delta_ub ); - Trace("cegqi") << "Delta lemma for " << d_n_delta_ub << std::endl; - Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub ); - d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); + //minimize the free delta heuristically on demand + if( d_check_delta_lemma_lc ){ + Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false ); + if( !delta.isNull() ){ + d_check_delta_lemma_lc = false; + d_n_delta_ub = NodeManager::currentNM()->mkNode( MULT, d_n_delta_ub, d_n_delta_ub ); + d_n_delta_ub = Rewriter::rewrite( d_n_delta_ub ); + Trace("cegqi") << "Delta lemma for " << d_n_delta_ub << std::endl; + Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_n_delta_ub ); + d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); + } } } return STATUS_UNKNOWN; @@ -446,7 +1143,17 @@ bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs, std::vector } } */ - return d_quantEngine->addInstantiation( d_curr_quant, subs, false ); + //check if we need virtual term substitution (if used delta) + bool used_delta = false; + Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( false, false ); + if( !delta.isNull() ){ + for( unsigned i=0; i<subs.size(); i++ ){ + if( TermDb::containsTerm( subs[i], delta ) ){ + used_delta = true; + } + } + } + return d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_delta ); } bool InstStrategyCegqi::addLemma( Node lem ) { diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index d59690c84..99c048013 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -22,7 +22,6 @@ #include "theory/arith/arithvar.h" #include "util/statistics_registry.h" -#include "theory/quantifiers/ce_guided_single_inv.h" namespace CVC4 { namespace theory { @@ -37,6 +36,53 @@ namespace datatypes { namespace quantifiers { +class CegqiOutput +{ +public: + virtual ~CegqiOutput() {} + virtual bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) = 0; + virtual bool isEligibleForInstantiation( Node n ) = 0; + virtual bool addLemma( Node lem ) = 0; +}; + +class CegInstantiator +{ +private: + Node d_zero; + Node d_one; + Node d_true; + Node d_n_delta; + QuantifiersEngine * d_qe; + CegqiOutput * d_out; + //program variable contains cache + std::map< Node, std::map< Node, bool > > d_prog_var; + std::map< Node, bool > d_inelig; + std::map< Node, bool > d_has_delta; +private: + //for adding instantiations during check + void computeProgVars( Node n ); + // effort=0 : do not use model value, 1: use model value, 2: one must use model value + bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, + unsigned i, unsigned effort ); + bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, + unsigned i, unsigned effort ); + bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, + unsigned j ); + bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ ); + Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true ); +public: + CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out ); + //the CE variables + std::vector< Node > d_vars; + //check : add instantiations based on valuation of d_vars + bool check(); + // get delta lemmas : on-demand force minimality of d_n_delta + void getDeltaLemmas( std::vector< Node >& lems ); +}; class InstStrategySimplex : public InstStrategy{ private: @@ -99,21 +145,19 @@ class InstStrategyCegqi : public InstStrategy { private: CegqiOutputInstStrategy * d_out; std::map< Node, CegInstantiator * > d_cinst; - Node d_n_delta; Node d_n_delta_ub; Node d_curr_quant; bool d_check_delta_lemma; bool d_check_delta_lemma_lc; - bool d_used_delta; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); int process( Node f, Theory::Effort effort, int e ); public: InstStrategyCegqi( QuantifiersEngine * qe ); ~InstStrategyCegqi() throw() {} - + bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ); - bool isEligibleForInstantiation( Node n ); + bool isEligibleForInstantiation( Node n ); bool addLemma( Node lem ); /** identify */ std::string identify() const { return std::string("Cegqi"); } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index c6115195d..37c7a4d57 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -81,6 +81,8 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ), d_op_id_count( 0 ), d_typ_id_count( 0 ) { d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); + d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); + d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); if( options::ceGuidedInst() ){ d_sygus_tdb = new TermDbSygus; }else{ @@ -1308,6 +1310,101 @@ Node TermDb::getCanonicalTerm( TNode n, bool apply_torder ){ return getCanonicalTerm( n, var_count, subs, apply_torder ); } + +Node TermDb::getVtsDelta( bool isFree, bool create ) { + if( create ){ + if( d_vts_delta_free.isNull() ){ + d_vts_delta_free = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "free delta for virtual term substitution" ); + Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); + d_quantEngine->getOutputChannel().lemma( delta_lem ); + } + if( d_vts_delta.isNull() ){ + d_vts_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for virtual term substitution" ); + } + } + return isFree ? d_vts_delta_free : d_vts_delta; +} + +Node TermDb::getVtsInfinity( bool isFree, bool create ) { + if( create ){ + if( d_vts_inf_free.isNull() ){ + d_vts_inf_free = NodeManager::currentNM()->mkSkolem( "inf", NodeManager::currentNM()->realType(), "free infinity for virtual term substitution" ); + } + if( d_vts_inf.isNull() ){ + d_vts_inf = NodeManager::currentNM()->mkSkolem( "inf", NodeManager::currentNM()->realType(), "infinity for virtual term substitution" ); + } + } + return isFree ? d_vts_inf_free : d_vts_inf; +} + +Node TermDb::rewriteVtsSymbols( Node n ) { + Assert( !d_vts_delta_free.isNull() ); + Assert( !d_vts_delta.isNull() ); + if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) && containsTerm( n, d_vts_delta ) ){ + Trace("quant-vts-debug") << "VTS : process " << n << std::endl; + if( n.getKind()==EQUAL ){ + return d_false; + }else{ + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( n, msum ) ){ + if( Trace.isOn("quant-vts-debug") ){ + Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" ); + } + Node iso_n; + int res = QuantArith::isolate( d_vts_delta, msum, iso_n, n.getKind(), true ); + if( res!=0 ){ + Trace("quant-vts-debug") << "VTS isolated : -> " << iso_n << ", res = " << res << std::endl; + int index = res==1 ? 0 : 1; + Node slv = iso_n[res==1 ? 1 : 0]; + if( iso_n[index]!=d_vts_delta ){ + if( iso_n[index].getKind()==MULT && iso_n[index].getNumChildren()==2 && iso_n[index][0].isConst() && iso_n[index][1]==d_vts_delta ){ + slv = NodeManager::currentNM()->mkNode( MULT, slv, NodeManager::currentNM()->mkConst( Rational(1)/iso_n[index][0].getConst<Rational>() ) ); + }else{ + return n; + } + } + Node nlit; + if( res==1 ){ + nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv ); + }else{ + nlit = NodeManager::currentNM()->mkNode( GT, slv, d_zero ); + } + Trace("quant-vts-debug") << "Return " << nlit << std::endl; + return nlit; + } + } + return n; + } + }else if( n.getKind()==FORALL ){ + //cannot traverse beneath quantifiers + std::vector< Node > delta; + delta.push_back( d_vts_delta ); + std::vector< Node > delta_free; + delta_free.push_back( d_vts_delta_free ); + n = n.substitute( delta.begin(), delta.end(), delta_free.begin(), delta_free.end() ); + return n; + }else{ + bool childChanged = false; + std::vector< Node > children; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nn = rewriteVtsSymbols( n[i] ); + children.push_back( nn ); + childChanged = childChanged || nn!=n[i]; + } + if( childChanged ){ + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.insert( children.begin(), n.getOperator() ); + } + Node ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); + Trace("quant-vts-debug") << "...make node " << ret << std::endl; + return ret; + }else{ + return n; + } + } +} + bool TermDb::containsTerm( Node n, Node t ) { if( n==t ){ return true; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 1ffe0e29e..ad206b470 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -145,6 +145,9 @@ public: /** boolean terms */ Node d_true; Node d_false; + /** constants */ + Node d_zero; + Node d_one; /** ground terms */ unsigned getNumGroundTerms( Node f ); /** count number of non-redundant ground terms per operator */ @@ -352,6 +355,20 @@ public: /** get canonical term */ Node getCanonicalTerm( TNode n, bool apply_torder = false ); +//for virtual term substitution +private: + Node d_vts_delta; + Node d_vts_inf; + Node d_vts_delta_free; + Node d_vts_inf_free; +public: + /** get vts delta */ + Node getVtsDelta( bool isFree = false, bool create = true ); + /** get vts infinity */ + Node getVtsInfinity( bool isFree = false, bool create = true ); + /** rewrite delta */ + Node rewriteVtsSymbols( Node n ); + //general utilities public: /** simple check for contains term */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 54f2a16fe..06fc8898b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -599,15 +599,21 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No } } -bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){ +bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){ Assert( f.getKind()==FORALL ); Assert( vars.size()==terms.size() ); Node body = getInstantiation( f, vars, terms ); + //do virtual term substitution + if( doVts ){ + body = Rewriter::rewrite( body ); + Trace("inst-debug") << "Rewrite vts symbols in " << body << std::endl; + Node body_r = d_term_db->rewriteVtsSymbols( body ); + Trace("inst-debug") << " ...result: " << body_r << std::endl; + body = body_r; + } Trace("inst-assert") << "(assert " << body << ")" << std::endl; //make the lemma - NodeBuilder<> nb(kind::OR); - nb << f.notNode() << body; - Node lem = nb; + Node lem = NodeManager::currentNM()->mkNode( kind::OR, f.negate(), body ); //check for duplication if( addLemma( lem ) ){ d_total_inst_debug[f]++; @@ -805,13 +811,13 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ d_phase_req_waiting[lit] = req; } -bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){ +bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst, bool doVts ){ std::vector< Node > terms; m.getTerms( this, f, terms ); - return addInstantiation( f, terms, mkRep, modEq, modInst ); + return addInstantiation( f, terms, mkRep, modEq, modInst, doVts ); } -bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst ) { +bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst, bool doVts ) { // For resource-limiting (also does a time check). getOutputChannel().safePoint(options::quantifierStep()); @@ -875,7 +881,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo //add the instantiation Trace("inst-add-debug") << "Constructing instantiation..." << std::endl; - bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms ); + bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms, doVts ); //report the result if( addedInst ){ Trace("inst-add-debug") << " -> Success." << std::endl; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 54f63bfe0..c9a3a8027 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -264,7 +264,7 @@ private: /** compute term vector */ void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ); /** instantiate f with arguments terms */ - bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); + bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false ); /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level ); /** flush lemmas */ @@ -283,9 +283,9 @@ public: /** add require phase */ void addRequirePhase( Node lit, bool req ); /** do instantiation specified by m */ - bool addInstantiation( Node f, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false ); + bool addInstantiation( Node f, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false ); /** add instantiation */ - bool addInstantiation( Node f, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false ); + bool addInstantiation( Node f, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false ); /** split on node n */ bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true ); /** add split equality */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index e8985e074..af6d92ee5 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -156,9 +156,9 @@ Node TheoryStrings::getLengthTerm( Node t ) { return length_term; } -Node TheoryStrings::getLength( Node t ) { +Node TheoryStrings::getLength( Node t, bool use_t ) { Node retNode; - if(t.isConst()) { + if(t.isConst() || use_t) { retNode = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t ); } else { retNode = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) ); @@ -1463,6 +1463,13 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal std::vector< Node > temp_exp; temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); temp_exp.push_back(length_eq); + //must add explanation for length terms + if( !normal_forms[i][index_i].isConst() && length_term_i[0]!=normal_forms[i][index_i] ){ + temp_exp.push_back( length_term_i[0].eqNode( normal_forms[i][index_i] ) ); + } + if( !normal_forms[j][index_j].isConst() && length_term_j[0]!=normal_forms[j][index_j] ){ + temp_exp.push_back( length_term_j[0].eqNode( normal_forms[j][index_j] ) ); + } Node eq_exp = temp_exp.empty() ? d_true : temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp ); sendInfer( eq_exp, eq, "LengthEq" ); @@ -1905,6 +1912,7 @@ void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) { if( conc.isNull() || conc == d_false ) { d_out->conflict(ant); Trace("strings-conflict") << "Strings::Conflict : " << ant << std::endl; + Trace("strings-assert") << "(assert (not " << ant << ")) ; conflict" << std::endl; d_conflict = true; } else { Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc ); @@ -1912,6 +1920,7 @@ void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) { lem = conc; } Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl; + Trace("strings-assert") << "(assert " << lem << ") ; lemma " << c << std::endl; d_lemma_cache.push_back( lem ); } } @@ -1922,6 +1931,7 @@ void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) { sendLemma( eq_exp, eq, c ); } else { Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl; + Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq << ")) ; infer " << c << std::endl; d_pending.push_back( eq ); d_pending_exp[eq] = eq_exp; d_infer.push_back(eq); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 2003bcd54..d83df2a31 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -138,7 +138,7 @@ private: bool areEqual( Node a, Node b ); bool areDisequal( Node a, Node b ); Node getLengthTerm( Node t ); - Node getLength( Node t ); + Node getLength( Node t, bool use_t = false ); private: /** The notify class */ diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 12b6bc53b..8978372e3 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -552,11 +552,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { } }*/ if( t!=retNode ){ - Trace("strings-preprocess") << "StringsPreprocess::simplify returns: " << retNode << std::endl; + Trace("strings-preprocess-debug") << "StringsPreprocess::simplify: " << t << " -> " << retNode << std::endl; if(!new_nodes.empty()) { - Trace("strings-preprocess") << " ... new nodes (" << new_nodes.size() << "):\n"; + Trace("strings-preprocess-debug") << " ... new nodes (" << new_nodes.size() << "):\n"; for(unsigned int i=0; i<new_nodes.size(); ++i) { - Trace("strings-preprocess") << "\t" << new_nodes[i] << "\n"; + Trace("strings-preprocess-debug") << "\t" << new_nodes[i] << "\n"; } } } diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index b5e741edd..7023f7c41 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1115,6 +1115,9 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } Trace("strings-postrewrite") << "Strings::postRewrite returning " << retNode << std::endl; + if( orig!=retNode ){ + Trace("strings-rewrite-debug") << "Strings: post-rewrite " << orig << " to " << retNode << std::endl; + } return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode); } @@ -1291,5 +1294,8 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { } Trace("strings-prerewrite") << "Strings::preRewrite returning " << retNode << std::endl; + if( orig!=retNode ){ + Trace("strings-rewrite-debug") << "Strings: pre-rewrite " << orig << " to " << retNode << std::endl; + } return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode); } diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index ff3607b5b..09ca6710d 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -48,7 +48,8 @@ TESTS = \ stream-x2014-09-18-unsat.smt2 \ simp-len.smt2 \ is-even.smt2 \ - is-even-pred.smt2 + is-even-pred.smt2 \ + delta-simp.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 diff --git a/test/regress/regress0/quantifiers/delta-simp.smt2 b/test/regress/regress0/quantifiers/delta-simp.smt2 new file mode 100644 index 000000000..f18a4fbd9 --- /dev/null +++ b/test/regress/regress0/quantifiers/delta-simp.smt2 @@ -0,0 +1,5 @@ +(set-logic LRA) +(set-info :status sat) +(declare-fun c () Real) +(assert (forall ((x Real)) (or (<= x 0) (>= x (+ c 3))))) +(check-sat)
\ No newline at end of file |