From a7b5b506a1b84b23bdb4263150590d15af8193fa Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 11 Dec 2014 14:09:54 +0100
Subject: [PATCH] Option to enable/disable cyclicity check in datatypes.

---
 src/theory/datatypes/options              |  2 ++
 src/theory/datatypes/theory_datatypes.cpp | 40 ++++++++++++-----------
 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
-- 
2.30.2