From 7c3790db478c4f06e65ef0f777317a4c6a803059 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 26 Aug 2015 15:49:23 +0200 Subject: [PATCH] Minor improvements to cbqi, fix bug in solving with vts symbols, round up for integer lower bounds. Add presolve infrastructure to quantifiers engine, modify --cbqi-prereg-inst. --- src/smt/smt_engine.cpp | 3 + .../quantifiers/ce_guided_single_inv.cpp | 3 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 76 ++++++++++++------- src/theory/quantifiers/inst_strategy_cbqi.h | 14 ++-- .../quantifiers/instantiation_engine.cpp | 5 ++ src/theory/quantifiers/instantiation_engine.h | 4 +- src/theory/quantifiers/options | 2 +- src/theory/quantifiers/theory_quantifiers.cpp | 3 + src/theory/quantifiers_engine.cpp | 8 ++ src/theory/quantifiers_engine.h | 4 + 10 files changed, 85 insertions(+), 37 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8fdec25c2..498b2ee12 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1428,6 +1428,9 @@ void SmtEngine::setDefaults() { if( !options::macrosQuant.wasSetByUser()) { options::macrosQuant.set( false ); } + if( !options::cbqiPreRegInst.wasSetByUser()) { + options::cbqiPreRegInst.set( true ); + } } //cbqi options diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 398415ca8..f122c63bb 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -453,7 +453,8 @@ void CegConjectureSingleInv::initialize( Node q ) { exit( 0 ); } }else{ - if( options::cbqiSingleInvPreRegInst() && d_single_inv.getKind()==FORALL ){ + if( options::cbqiPreRegInst() && d_single_inv.getKind()==FORALL ){ + //just invoke the presolve now d_cinst->presolve( d_single_inv ); } } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index ddf032ac1..41c0e276b 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -64,10 +64,10 @@ void CegInstantiator::computeProgVars( Node n ){ } bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node theta, - unsigned i, unsigned effort ){ + std::vector< Node >& coeff, std::vector< int >& btyp, + std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort ){ if( i==d_vars.size() ){ - return addInstantiationCoeff( subs, vars, coeff, has_coeff, 0 ); + return addInstantiationCoeff( subs, vars, coeff, btyp, has_coeff, 0 ); }else{ std::map< Node, std::map< Node, bool > > subs_proc; //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]]; @@ -114,7 +114,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< if( proc ){ //try the substitution subs_proc[ns][pv_coeff] = true; - if( addInstantiationInc( ns, pv, pv_coeff, subs, vars, coeff, has_coeff, theta, i, effort ) ){ + if( addInstantiationInc( ns, pv, pv_coeff, 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort ) ){ return true; } } @@ -197,7 +197,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node val = veq[1]; if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){ subs_proc[val][veq_c] = true; - if( addInstantiationInc( val, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){ + if( addInstantiationInc( val, pv, veq_c, 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort ) ){ return true; } } @@ -288,9 +288,16 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< //negate if coefficient on variable is positive std::map< Node, Node >::iterator itv = msum.find( pv ); if( itv!=msum.end() ){ - if( itv->second.isNull() || itv->second.getConst().sgn()==1 ){ + //multiply by the coefficient we will isolate for + if( itv->second.isNull() ){ vts_coeff[t] = QuantArith::negate(vts_coeff[t]); - Trace("cbqi-inst-debug") << "negate vts[" << t<< "] coefficient." << std::endl; + }else{ + if( !pvtn.isInteger() ){ + vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst() ), vts_coeff[t] ); + vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] ); + }else if( itv->second.getConst().sgn()==1 ){ + vts_coeff[t] = QuantArith::negate(vts_coeff[t]); + } } } Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; @@ -403,7 +410,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< //try this bound if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){ subs_proc[uval][veq_c] = true; - if( addInstantiationInc( uval, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){ + if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, subs, vars, coeff, btyp, has_coeff, theta, i, effort ) ){ return true; } } @@ -439,7 +446,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< val = NodeManager::currentNM()->mkNode( UMINUS, val ); val = Rewriter::rewrite( val ); } - if( addInstantiationInc( val, pv, Node::null(), subs, vars, coeff, has_coeff, theta, i, effort ) ){ + if( addInstantiationInc( val, pv, Node::null(), 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort ) ){ return true; } } @@ -528,12 +535,12 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Trace("cbqi-bound") << std::endl; best_used[rr] = (unsigned)best; Node val = mbp_bounds[rr][best]; - val = getModelBasedProjectionValue( val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta, + val = getModelBasedProjectionValue( val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta, mbp_vts_coeff[rr][0][best], vts_sym[0], mbp_vts_coeff[rr][1][best], vts_sym[1] ); if( !val.isNull() ){ if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){ subs_proc[val][mbp_coeff[rr][best]] = true; - if( addInstantiationInc( val, pv, mbp_coeff[rr][best], subs, vars, coeff, has_coeff, theta, i, effort ) ){ + if( addInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, subs, vars, coeff, btyp, has_coeff, theta, i, effort ) ){ return true; } } @@ -549,7 +556,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< if( !val.isNull() ){ if( subs_proc[val].find( c )==subs_proc[val].end() ){ subs_proc[val][c] = true; - if( addInstantiationInc( val, pv, c, subs, vars, coeff, has_coeff, theta, i, effort ) ){ + if( addInstantiationInc( val, pv, c, 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort ) ){ return true; } } @@ -564,12 +571,12 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< int rr = upper_first ? (1-r) : r; for( unsigned j=0; j& subs, std::vector< //we only resort to values in the case of booleans Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() ); #endif - if( addInstantiationInc( mv, pv, pv_coeff_m, subs, vars, coeff, has_coeff, theta, i, new_effort ) ){ + if( addInstantiationInc( mv, pv, pv_coeff_m, 0, subs, vars, coeff, btyp, has_coeff, theta, i, new_effort ) ){ return true; } } @@ -601,8 +608,9 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } -bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort ) { +bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< int >& btyp, + std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort ) { if( Trace.isOn("cbqi-inst") ){ for( unsigned j=0; j& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, unsigned j ) { + std::vector< Node >& coeff, std::vector< int >& btyp, std::vector< Node >& has_coeff, unsigned j ) { if( j==has_coeff.size() ){ return addInstantiation( subs, vars ); }else{ @@ -738,8 +748,9 @@ bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vec 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 ){ + Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl; + //intger division rounding up if from a lower bound + if( btyp[index]==1 ){ subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], NodeManager::currentNM()->mkNode( ITE, NodeManager::currentNM()->mkNode( EQUAL, @@ -748,10 +759,9 @@ bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vec d_zero, d_one ) ); } - */ } Trace("cbqi-inst-debug") << "...normalize integers : " << subs[index] << std::endl; - if( addInstantiationCoeff( subs, vars, coeff, has_coeff, j+1 ) ){ + if( addInstantiationCoeff( subs, vars, coeff, btyp, has_coeff, j+1 ) ){ return true; } } @@ -772,7 +782,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< 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 ) { + 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; @@ -853,7 +863,7 @@ Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std: } } -Node CegInstantiator::getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta, +Node CegInstantiator::getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ) { Node val = t; Trace("cbqi-bound2") << "Value : " << val << std::endl; @@ -917,10 +927,11 @@ bool CegInstantiator::check() { std::vector< Node > subs; std::vector< Node > vars; std::vector< Node > coeff; + std::vector< int > btyp; std::vector< Node > has_coeff; Node theta; //try to add an instantiation - if( addInstantiation( subs, vars, coeff, has_coeff, theta, 0, r==0 ? 0 : 2 ) ){ + if( addInstantiation( subs, vars, coeff, btyp, has_coeff, theta, 0, r==0 ? 0 : 2 ) ){ return true; } } @@ -1585,9 +1596,16 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { } void InstStrategyCegqi::registerQuantifier( Node q ) { - if( options::cbqiSingleInvPreRegInst() ){ - CegInstantiator * cinst = getInstantiator( q ); - cinst->presolve( q ); + if( options::cbqiPreRegInst() ){ + //just get the instantiator + getInstantiator( q ); } } +void InstStrategyCegqi::presolve() { + if( options::cbqiPreRegInst() ){ + for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){ + it->second->presolve( it->first ); + } + } +} diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index c7c046e51..0056671be 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -69,13 +69,15 @@ private: 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, Node theta, + std::vector< Node >& coeff, std::vector< int >& btyp, + std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort ); - bool addInstantiationInc( Node n, Node pv, Node pv_coeff, std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort ); + bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< int >& btyp, + std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort ); bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, - unsigned j ); + std::vector< Node >& coeff, std::vector< int >& btyp, + std::vector< Node >& has_coeff, unsigned j ); bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars ); 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 ); @@ -178,6 +180,8 @@ public: CegInstantiator * getInstantiator( Node q ); //register quantifier void registerQuantifier( Node q ); + //presolve + void presolve(); }; } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 6cf64407f..492b2dedf 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -77,6 +77,11 @@ void InstantiationEngine::finishInit(){ } } +void InstantiationEngine::presolve() { + for( unsigned i=0; ipresolve(); + } +} bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ unsigned lastWaiting = d_quantEngine->d_lemmas_waiting.size(); diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index d6cde9e7f..1f321917b 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -43,6 +43,8 @@ protected: public: InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){} virtual ~InstStrategy(){} + /** presolve */ + virtual void presolve() {} /** reset instantiation */ virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; /** process method, returns a status */ @@ -98,7 +100,7 @@ public: ~InstantiationEngine(); /** initialize */ void finishInit(); - + void presolve(); bool needsCheck( Theory::Effort e ); unsigned needsModel( Theory::Effort e ); void reset_round( Theory::Effort e ); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index c693adef5..ec71e5348 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -244,7 +244,7 @@ option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false use integer infinity for vts in counterexample-based quantifier instantiation option cbqiUseInfReal --cbqi-use-inf-real bool :read-write :default false use real infinity for vts in counterexample-based quantifier instantiation -option cbqiSingleInvPreRegInst --cbqi-prereg-inst bool :default false +option cbqiPreRegInst --cbqi-prereg-inst bool :read-write :default false preregister ground instantiations in counterexample-based quantifier instantiation option cbqiMinBounds --cbqi-min-bounds bool :default false use minimally constrained lower/upper bound for counterexample-based quantifier instantiation diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 373a8a0da..48891732b 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -77,6 +77,9 @@ void TheoryQuantifiers::preRegisterTerm(TNode n) { void TheoryQuantifiers::presolve() { Debug("quantifiers-presolve") << "TheoryQuantifiers::presolve()" << endl; + if( getQuantifiersEngine() ){ + getQuantifiersEngine()->presolve(); + } } Node TheoryQuantifiers::getValue(TNode n) { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ca16d2ab1..1a5be5a57 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -252,6 +252,7 @@ Valuation& QuantifiersEngine::getValuation(){ } void QuantifiersEngine::finishInit(){ + Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl; for( int i=0; i<(int)d_modules.size(); i++ ){ d_modules[i]->finishInit(); } @@ -281,6 +282,13 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) { return mo==m || mo==NULL; } +void QuantifiersEngine::presolve() { + Trace("quant-engine-debug") << "QuantifiersEngine : presolve " << std::endl; + for( unsigned i=0; ipresolve(); + } +} + void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_time); if( !getMasterEqualityEngine()->consistent() ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 101aa43cd..2658d09f0 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -53,6 +53,8 @@ public: QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; } /** initialize */ virtual void finishInit() {} + /** presolve */ + virtual void presolve() {} /* whether this module needs to check this round */ virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } /* whether this module needs a model built */ @@ -251,6 +253,8 @@ public: public: /** initialize */ void finishInit(); + /** presolve */ + void presolve(); /** check at level */ void check( Theory::Effort e ); /** register quantifier */ -- 2.30.2