Do not throw error when codatatype is not well-founded. Add option for disabling codatatype reasoning. Minor cleanup.

5 files changed, 12 insertions, 5 deletions

diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options
index 5fc59b549..7e56b4d7a 100644
--- a/src/theory/datatypes/options
+++ b/src/theory/datatypes/options
@@ -13,5 +13,7 @@ expert-option dtRewriteErrorSel --dt-rewrite-error-sel bool :default false
  rewrite incorrectly applied selectors to arbitrary ground term
 option dtForceAssignment --dt-force-assignment bool :default false :read-write
  force the datatypes solver to give specific values to all datatypes terms before answering sat
+option cdtBisimilar --cdt-bisimilar bool :default true
+ do bisimilarity check for co-datatypes
  
 endmodule
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 65514180d..d3f0dac9b 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1501,7 +1501,7 @@ void TheoryDatatypes::checkCycles() {
     ++eqcs_i;
   }
   //process codatatypes
-  if( cod_eqc.size()>1 ){
+  if( cod_eqc.size()>1 && options::cdtBisimilar() ){
     Trace("dt-cod-debug") << "Process " << cod_eqc.size() << " co-datatypes" << std::endl;
     std::vector< std::vector< Node > > part_out;
     std::vector< TNode > exp;
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 7d9fa3344..05e33c7b2 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -39,7 +39,7 @@ struct PrioritySort {
 
 RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) {
   d_true = NodeManager::currentNM()->mkConst( true );
-  d_needsSort = true;
+  d_needsSort = false;
 }
 
 double RewriteEngine::getPriority( Node f ) {
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 4855083a8..c1ad62cd9 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -186,6 +186,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
     Trace("quant-engine-debug") << std::endl;
     Trace("quant-engine-debug") << "  # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
+    Trace("quant-engine-debug") << "  Theory engine finished : " << !d_te->needCheck() << std::endl;
 
     if( !getMasterEqualityEngine()->consistent() ){
       Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl;
@@ -229,7 +230,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
     for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_MODEL; quant_e++ ){
       for( int i=0; i<(int)qm.size(); i++ ){
-        Trace("quant-engine-debug") << "Check " << d_modules[i]->identify().c_str() << "..." << std::endl;
+        Trace("quant-engine-debug") << "Check " << qm[i]->identify().c_str() << " at effort " << quant_e << "..." << std::endl;
         qm[i]->check( e, quant_e );
       }
       //flush all current lemmas
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 9e07c746a..f0704520a 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -299,8 +299,12 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
     }
   }
   if( groundTerm.isNull() ){
-    // if we get all the way here, we aren't well-founded
-    CheckArgument(false, *this, "this datatype is not well-founded, cannot construct a ground term!");
+    if( !d_isCo ){
+      // if we get all the way here, we aren't well-founded
+      CheckArgument(false, *this, "this datatype is not well-founded, cannot construct a ground term!");
+    }else{
+      return groundTerm;
+    }
   }else{
     return groundTerm;
   }