diff options
| -rw-r--r-- | src/theory/quantifiers/ceg_instantiator.cpp | 6 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 7 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 5 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 21 | ||||
| -rwxr-xr-x | test/regress/regress0/fmf/forall_unit_data.smt2 | 13 |
5 files changed, 43 insertions, 9 deletions
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; i<d_quantEngine->getModel()->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<Node, NodeHashFunction> 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<dt.getNumConstructors(); i++ ){ + for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ + TypeNode ctn = TypeNode::fromType( ((SelectorType)dt[i][j].getSelector().getType()).getRangeType() ); + if( tn!=ctn && !isClosedEnumerableType( ctn ) ){ + ret = false; + break; + } + } + if( !ret ){ + break; + } + } }else{ - //TODO: all subfields must be closed enumerable? + //TODO: all subfields must be closed enumerable } d_typ_closed_enum[tn] = ret; return ret; diff --git a/test/regress/regress0/fmf/forall_unit_data.smt2 b/test/regress/regress0/fmf/forall_unit_data.smt2 new file mode 100755 index 000000000..7e0897d14 --- /dev/null +++ b/test/regress/regress0/fmf/forall_unit_data.smt2 @@ -0,0 +1,13 @@ +; cvc4 --lang smt
+
+; This problem returns "unsat", but it is in fact "sat", by interpreting "a" with a domain of
+; cardinality 1. The issue arises irrespective of the "--finite-model-find" option.
+
+(set-option :produce-models true)
+(set-option :interactive-mode true)
+(set-logic ALL_SUPPORTED)
+(declare-sort a 0)
+(declare-datatypes () ((w (Wrap (unw a)))))
+(declare-fun x () w)
+(assert (forall ((y w)) (= x y)))
+(check-sat)
|