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 );
}
}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() ){
#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
#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) );
+//new implementation
+
bool CegqiOutputInstStrategy::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) {
return d_out->addInstantiation( subs, subs_typ );
}
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 ) );
}
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;
}
}
*/
- 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 ) {
#include "theory/arith/arithvar.h"
#include "util/statistics_registry.h"
-#include "theory/quantifiers/ce_guided_single_inv.h"
namespace CVC4 {
namespace theory {
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:
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"); }
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{
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;
/** 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 */
/** 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 */
}
}
-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]++;
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());
//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;
/** 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 */
/** 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 */
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 ) );
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" );
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 );
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 );
}
}
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);
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 */
}
}*/
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";
}
}
}
}
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);
}
}
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);
}
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
--- /dev/null
+(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
projects / cvc5.git / commitdiff