From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 22 Dec 2015 11:03:10 +0000 (+0100)
Subject: Bug fix for cbqi, do not use model values for terms involving non-enumerable sorts.
X-Git-Tag: cvc5-1.0.0~6134
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bd6a13bbb46c272561c01b7783f62ff7be091c2c;p=cvc5.git

Bug fix for cbqi, do not use model values for terms involving non-enumerable sorts.
---

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)