Option to enable/disable cyclicity check in datatypes.

2 files changed, 23 insertions, 19 deletions

diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options
index bc7552862..592e9e67e 100644
--- a/src/theory/datatypes/options
+++ b/src/theory/datatypes/options
@@ -17,5 +17,7 @@ option dtBinarySplit --dt-binary-split bool :default false
  do binary splits for datatype constructor types
 option cdtBisimilar --cdt-bisimilar bool :default true
  do bisimilarity check for co-datatypes
+option dtCyclic --dt-cyclic bool :default true
+ do cyclicity check for datatypes
  
 endmodule
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 5436ab632..edb548ca4 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1479,26 +1479,28 @@ void TheoryDatatypes::checkCycles() {
     if( DatatypesRewriter::isTypeDatatype( tn ) ) {
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
       if( !dt.isCodatatype() ){
-        //do cycle checks
-        std::map< TNode, bool > visited;
-        std::vector< TNode > expl;
-        Node cn = searchForCycle( eqc, eqc, visited, expl );
-        //if we discovered a different cycle while searching this one
-        if( !cn.isNull() && cn!=eqc ){
-          visited.clear();
-          expl.clear();
-          Node prev = cn;
-          cn = searchForCycle( cn, cn, visited, expl );
-          Assert( prev==cn );
-        }
+        if( options::dtCyclic() ){
+          //do cycle checks
+          std::map< TNode, bool > visited;
+          std::vector< TNode > expl;
+          Node cn = searchForCycle( eqc, eqc, visited, expl );
+          //if we discovered a different cycle while searching this one
+          if( !cn.isNull() && cn!=eqc ){
+            visited.clear();
+            expl.clear();
+            Node prev = cn;
+            cn = searchForCycle( cn, cn, visited, expl );
+            Assert( prev==cn );
+          }
 
-        if( !cn.isNull() ) {
-          Assert( expl.size()>0 );
-          d_conflictNode = mkAnd( expl );
-          Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl;
-          d_out->conflict( d_conflictNode );
-          d_conflict = true;
-          return;
+          if( !cn.isNull() ) {
+            Assert( expl.size()>0 );
+            d_conflictNode = mkAnd( expl );
+            Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl;
+            d_out->conflict( d_conflictNode );
+            d_conflict = true;
+            return;
+          }
         }
       }else{
         //indexing