From bd6a13bbb46c272561c01b7783f62ff7be091c2c Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 22 Dec 2015 12:03:10 +0100 Subject: [PATCH] Bug fix for cbqi, do not use model values for terms involving non-enumerable sorts. --- src/theory/quantifiers/ceg_instantiator.cpp | 6 +++--- src/theory/quantifiers/inst_strategy_cbqi.cpp | 7 +++++-- src/theory/quantifiers/inst_strategy_cbqi.h | 5 +++-- src/theory/quantifiers/term_database.cpp | 21 +++++++++++++++++-- .../regress0/fmf/forall_unit_data.smt2 | 13 ++++++++++++ 5 files changed, 43 insertions(+), 9 deletions(-) create mode 100755 test/regress/regress0/fmf/forall_unit_data.smt2 diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index cea90621d..3ff0cda92 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -679,7 +679,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve //[4] resort to using value in model // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype - if( ( effort>0 || pvtn.isBoolean() || !curr_var.empty() ) && !pvtn.isSort() ){ + if( ( effort>0 || pvtn.isBoolean() || !curr_var.empty() ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){ Node mv = getModelValue( pv ); Node pv_coeff_m; Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl; @@ -1108,7 +1108,7 @@ Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower bool CegInstantiator::check() { if( d_qe->getTheoryEngine()->needCheck() ){ - Trace("cegqi-engine") << " CEGQI instantiator : wait until all ground theories are finished." << std::endl; + Trace("cbqi-engine") << " CEGQI instantiator : wait until all ground theories are finished." << std::endl; return false; } processAssertions(); @@ -1125,7 +1125,7 @@ bool CegInstantiator::check() { return true; } } - Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; + Trace("cbqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; return false; } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index a4632398d..5790fc34a 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -56,6 +56,7 @@ unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) { void InstStrategyCbqi::reset_round( Theory::Effort effort ) { d_cbqi_set_quant_inactive = false; + d_incomplete_check = false; //check if any cbqi lemma has not been added yet for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); @@ -133,7 +134,7 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) { } bool InstStrategyCbqi::checkComplete() { - if( !options::cbqiSat() && d_cbqi_set_quant_inactive ){ + if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){ return false; }else{ return true; @@ -590,7 +591,9 @@ void InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { CegInstantiator * cinst = getInstantiator( f ); Trace("inst-alg") << "-> Run cegqi for " << f << std::endl; d_curr_quant = f; - cinst->check(); + if( !cinst->check() ){ + d_incomplete_check = true; + } d_curr_quant = Node::null(); }else if( e==1 ){ //minimize the free delta heuristically on demand diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index b8bc25c6a..2105007e2 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -36,10 +36,11 @@ class InstStrategyCbqi : public QuantifiersModule { typedef context::CDHashSet NodeSet; protected: bool d_cbqi_set_quant_inactive; + bool d_incomplete_check; /** whether we have added cbqi lemma */ NodeSet d_added_cbqi_lemma; /** whether to do cbqi for this quantified formula */ - std::map< Node, bool > d_do_cbqi; + std::map< Node, bool > d_do_cbqi; /** register ce lemma */ virtual void registerCounterexampleLemma( Node q, Node lem ); /** has added cbqi lemma */ @@ -138,7 +139,7 @@ protected: void registerCounterexampleLemma( Node q, Node lem ); public: InstStrategyCegqi( QuantifiersEngine * qe ); - ~InstStrategyCegqi() throw(); + ~InstStrategyCegqi() throw(); bool addInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index e6478440d..5ccb794f7 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -775,7 +775,7 @@ Node TermDb::getRemoveQuantifiers( Node n ) { return getRemoveQuantifiers2( n, visited ); } -//quantified simplify +//quantified simplify Node TermDb::getQuantSimplify( Node n ) { std::vector< Node > bvs; getBoundVars( n, bvs ); @@ -1029,11 +1029,28 @@ Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) { bool TermDb::isClosedEnumerableType( TypeNode tn ) { std::map< TypeNode, bool >::iterator it = d_typ_closed_enum.find( tn ); if( it==d_typ_closed_enum.end() ){ + d_typ_closed_enum[tn] = false; bool ret = true; if( tn.isArray() || tn.isSort() || tn.isCodatatype() ){ ret = false; + }else if( tn.isSet() ){ + ret = isClosedEnumerableType( tn.getSetElementType() ); + }else if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + for( unsigned i=0; i