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

diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options
index 5fc59b54939546575f18d54e6761cb96c97aa1ae..7e56b4d7a77d72480f2d1711418c3a343d99d9ad 100644 (file)
--- 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 65514180dd67b5fa3847bfa6285e3d9433d791a4..d3f0dac9baadfe6ae6fb547a2c5d0be951e41225 100644 (file)
--- 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 7d9fa3344994887e1753c739ac66241966b16325..05e33c7b2cb487f71a191757551f318bec5fbd53 100644 (file)
--- 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 4855083a894577bdf4685e2573dbe6589338ca0e..c1ad62cd995692c27c5a51d4fb03d4fee35ba79e 100644 (file)
--- 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 9e07c746a7c5585d6f5282c4eca3f5e8db19cef8..f0704520afeaa40789746c741cdf36c6bf2f1b7a 100644 (file)
--- 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;
   }