Fixes and improvements for datatypes properties and splitting.

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 45a7447aac1790e3366ef83ec3c4f475bab58b39..b52ceb856295334744ae10ad7f6b9effeaa71005 100644 (file)
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -306,10 +306,11 @@ bool Datatype::isUFinite() const throw(IllegalArgumentException) {
   if(self.getAttribute(DatatypeUFiniteComputedAttr())) {
     return self.getAttribute(DatatypeUFiniteAttr());
   }
+  //start by assuming it is not
+  self.setAttribute(DatatypeUFiniteComputedAttr(), true);
+  self.setAttribute(DatatypeUFiniteAttr(), false);
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
     if(! (*i).isUFinite()) {
-      self.setAttribute(DatatypeUFiniteComputedAttr(), true);
-      self.setAttribute(DatatypeUFiniteAttr(), false);
       return false;
     }
   }
@@ -838,7 +839,7 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
     return self.getAttribute(DatatypeFiniteAttr());
   }
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    if(! SelectorType((*i).getSelector().getType()).getRangeType().getCardinality().isFinite()) {
+    if(! (*i).getRangeType().getCardinality().isFinite()) {
       self.setAttribute(DatatypeFiniteComputedAttr(), true);
       self.setAttribute(DatatypeFiniteAttr(), false);
       return false;
@@ -858,9 +859,18 @@ bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) {
   if(self.getAttribute(DatatypeUFiniteComputedAttr())) {
     return self.getAttribute(DatatypeUFiniteAttr());
   }
+  bool success = true;
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    Type t = SelectorType((*i).getSelector().getType()).getRangeType();
-    if(!t.isSort() && !t.getCardinality().isFinite()) {
+    Type t = (*i).getRangeType();
+    if( t.isDatatype() ){
+      const Datatype& dt = ((DatatypeType)t).getDatatype();
+      if( !dt.isUFinite() ){
+        success = false;
+      }
+    }else if(!t.isSort() && !t.getCardinality().isFinite()) {
+      success = false;
+    }
+    if(!success ){
       self.setAttribute(DatatypeUFiniteComputedAttr(), true);
       self.setAttribute(DatatypeUFiniteAttr(), false);
       return false;

diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index e874ee5b845b8057097be7c16acf8e8f7c92e29d..1ae1c3c5f690996f0a08749600cd0379ac3b173d 100644 (file)
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -48,11 +48,11 @@ void QuantDSplit::preRegisterQuantifier( Node q ) {
       }else{
         int score = -1;
         if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
-          score = dt.isFinite() ? 1 : -1;
-        }else if(  options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
+          score = dt.isUFinite() ? 1 : -1;
+        }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
           score = dt.isUFinite() ? 1 : -1;
         }
-        Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << std::endl;
+        Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isUFinite() << " " << dt.isFinite() << ")" << std::endl;
         if( score>max_score ){
           max_index = i;
           max_score = score;
@@ -70,11 +70,12 @@ void QuantDSplit::preRegisterQuantifier( Node q ) {
 
 /* whether this module needs to check this round */
 bool QuantDSplit::needsCheck( Theory::Effort e ) {
-  return e>=Theory::EFFORT_FULL;
+  return e>=Theory::EFFORT_FULL && !d_quant_to_reduce.empty();
 }
+
 /* Call during quantifier engine's check */
 void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) {
-  //flush lemmas ASAP (they are a reduction)
+  //add lemmas ASAP (they are a reduction)
   if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){
     std::vector< Node > lemmas;
     for(std::map< Node, int >::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); ++it) {
@@ -92,6 +93,7 @@ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) {
         TNode svar = q[0][it->second];
         TypeNode tn = svar.getType();
         if( tn.isDatatype() ){
+          std::vector< Node > cons;
           const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
           for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
             std::vector< Node > vars;
@@ -110,8 +112,10 @@ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) {
             if( !bvs_cmb.empty() ){
               body = NodeManager::currentNM()->mkNode( kind::FORALL, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bvs_cmb ), body );
             }
-            disj.push_back( body );
+            cons.push_back( body );
           }
+          Node conc = cons.size()==1 ? cons[0] : NodeManager::currentNM()->mkNode( kind::AND, cons );
+          disj.push_back( conc );
         }else{
           Assert( false );
         }
@@ -124,6 +128,7 @@ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) {
       Trace("quant-dsplit") << "QuantDSplit lemma : " << lemmas[i] << std::endl;
       d_quantEngine->addLemma( lemmas[i], false );
     }
+    d_quant_to_reduce.clear();
   }
 }
 

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index cfb3fda94baeaee17238a5a0c6804e1a7eda015d..bbc41278e4d8fe8ab1e68490538dd52abf0a177c 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -241,7 +241,7 @@ void QuantifiersEngine::finishInit(){
     d_modules.push_back( d_lte_part_inst );
   }
   if( ( options::finiteModelFind() && options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ) || 
-      options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_AGG ){
+      options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
     d_qsplit = new quantifiers::QuantDSplit( this, c );
     d_modules.push_back( d_qsplit );
   }
@@ -365,10 +365,10 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
   bool usedModelBuilder = false;
 
-  Trace("quant-engine-debug") << "Quantifiers Engine call to check, level = " << e << std::endl;
+  Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
   if( needsCheck ){
-    Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
     if( Trace.isOn("quant-engine-debug") ){
+      Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
       Trace("quant-engine-debug") << "  modules to check : ";
       for( unsigned i=0; i<qm.size(); i++ ){
         Trace("quant-engine-debug") << qm[i]->identify() << " ";
@@ -484,9 +484,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
         }
       }
     }
-    Trace("quant-engine") << "Finished quantifiers engine check." << std::endl;
+    Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl;
   }else{
-    Trace("quant-engine") << "Quantifiers Engine does not need check." << std::endl;
+    Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl;
   }
 
   //SAT case

diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index a3ff2fcc7379ad33ff65b1a456bc287f3210dfff..aa350879833c4eb1ba1c7861a31cf83d62c99a79 100644 (file)
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -51,7 +51,8 @@ TESTS =       \
        fmc_unsound_model.smt2 \
        am-bad-model.cvc \
        nun-0208-to.smt2 \
-       datatypes-ufinite.smt2
+       datatypes-ufinite.smt2 \
+       datatypes-ufinite-nested.smt2
 
 
 EXTRA_DIST = $(TESTS)

diff --git a/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2 b/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2
new file mode 100644 (file)
index 0000000..3ffc36d
--- /dev/null
+++ b/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(declare-sort U 0)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(assert (distinct a b c))
+(declare-sort V 0)
+(declare-datatypes () ((ufin1 (cons1 (s11 U) (s13 ufin2))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3))))
+(declare-fun P (ufin1 ufin2) Bool)
+(declare-fun Q (ufin1 ufin1) Bool)
+(assert (forall ((x ufin1) (y ufin2) (z ufin1)) (or (P x y) (Q x z))))
+(assert (not (P (cons1 a cons3) cons3)))
+(assert (not (Q (cons1 b cons3) (cons1 a cons3))))
+(check-sat)

diff --git a/test/regress/regress0/fmf/datatypes-ufinite.smt2 b/test/regress/regress0/fmf/datatypes-ufinite.smt2
index d802930fde497ca201a472dae997e11cf335b9ea..3564bff8be1072efb20aa6e95a0b3a08c356635f 100644 (file)
--- a/test/regress/regress0/fmf/datatypes-ufinite.smt2
+++ b/test/regress/regress0/fmf/datatypes-ufinite.smt2
@@ -8,10 +8,10 @@
 (declare-fun d () U)
 (assert (distinct a b c))
 (declare-sort V 0)
-(declare-datatypes () ((ufin1 (cons1 (s11 U) (s12 U) (s13 U))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3))))
+(declare-datatypes () ((ufin1 (cons1 (s11 U) (s12 U))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3))))
 (declare-fun P (ufin1 ufin2) Bool)
 (declare-fun Q (ufin1 ufin1) Bool)
 (assert (forall ((x ufin1) (y ufin2) (z ufin1)) (or (P x y) (Q x z))))
-(assert (not (P (cons1 a a a) cons3)))
-(assert (not (Q (cons1 a d a) (cons1 a b c))))
+(assert (not (P (cons1 a a) cons3)))
+(assert (not (Q (cons1 a d) (cons1 a b))))
 (check-sat)