From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 8 Aug 2017 07:40:00 +0000 (-0500)
Subject: Use cache for datatypes cycle check, add regression.
X-Git-Tag: cvc5-1.0.0~5690
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=090093bb54af936c79109bbfd162028fd896139e;p=cvc5.git

Use cache for datatypes cycle check, add regression.
---

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 874f49f1e..d2592c842 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -179,7 +179,9 @@ void TheoryDatatypes::check(Effort e) {
     Assert( d_pending.empty() && d_pending_merge.empty() );
     do {
       d_addedFact = false;
+      Trace("datatypes-proc") << "Check cycles..." << std::endl;
       checkCycles();
+      Trace("datatypes-proc") << "...finish check cycles" << std::endl;
       flushPendingFacts();
       if( d_conflict || d_addedLemma ){
         return;
@@ -1791,7 +1793,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
 }
 
 void TheoryDatatypes::checkCycles() {
-  Debug("datatypes-cycle-check") << "Check cycles" << std::endl;
+  Trace("datatypes-cycle-check") << "Check acyclicity" << std::endl;
   std::vector< Node > cdt_eqc;
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ){
@@ -1802,14 +1804,18 @@ void TheoryDatatypes::checkCycles() {
         if( options::dtCyclic() ){
           //do cycle checks
           std::map< TNode, bool > visited;
+          std::map< TNode, bool > proc;
           std::vector< TNode > expl;
-          Node cn = searchForCycle( eqc, eqc, visited, expl );
+          Trace("datatypes-cycle-check") << "...search for cycle starting at " << eqc << std::endl;
+          Node cn = searchForCycle( eqc, eqc, visited, proc, expl );
+          Trace("datatypes-cycle-check") << "...finish." << std::endl;
           //if we discovered a different cycle while searching this one
           if( !cn.isNull() && cn!=eqc ){
             visited.clear();
+            proc.clear();
             expl.clear();
             Node prev = cn;
-            cn = searchForCycle( cn, cn, visited, expl );
+            cn = searchForCycle( cn, cn, visited, proc, expl );
             Assert( prev==cn );
           }
 
@@ -1829,6 +1835,7 @@ void TheoryDatatypes::checkCycles() {
     }
     ++eqcs_i;
   }
+  Trace("datatypes-cycle-check") << "Check uniqueness" << std::endl;
   //process codatatypes
   if( cdt_eqc.size()>1 && options::cdtBisimilar() ){
     printModelDebug("dt-cdt-debug");
@@ -1991,9 +1998,9 @@ void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector<
 
 //postcondition: if cycle detected, explanation is why n is a subterm of on
 Node TheoryDatatypes::searchForCycle( TNode n, TNode on,
-                                      std::map< TNode, bool >& visited,
+                                      std::map< TNode, bool >& visited, std::map< TNode, bool >& proc,
                                       std::vector< TNode >& explanation, bool firstTime ) {
-  Debug("datatypes-cycle-check") << "Search for cycle " << n << " " << on << endl;
+  Trace("datatypes-cycle-check2") << "Search for cycle " << n << " " << on << endl;
   TNode ncons;
   TNode nn;
   if( !firstTime ){
@@ -2003,14 +2010,19 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on,
       return on;
     }
   }else{
-    nn = n;
+    nn = getRepresentative( n );
+  }
+  if( proc.find( nn )!=proc.end() ){
+    return Node::null();
   }
+  Trace("datatypes-cycle-check2") << "...representative : " << nn << " " << ( visited.find( nn ) == visited.end() ) << " " << visited.size() << std::endl;
   if( visited.find( nn ) == visited.end() ) {
+    Trace("datatypes-cycle-check2") << "  visit : " << nn << std::endl;
     visited[nn] = true;
     TNode ncons = getEqcConstructor( nn );
     if( ncons.getKind()==APPLY_CONSTRUCTOR ) {
-      for( int i=0; i<(int)ncons.getNumChildren(); i++ ) {
-        TNode cn = searchForCycle( ncons[i], on, visited, explanation, false );
+      for( unsigned i=0; i<ncons.getNumChildren(); i++ ) {
+        TNode cn = searchForCycle( ncons[i], on, visited, proc, explanation, false );
         if( cn==on ) {
           //if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, ncons[i] ) ){
           //  Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << ncons[i] << "!!!!" << std::endl;
@@ -2025,6 +2037,8 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on,
         }
       }
     }
+    Trace("datatypes-cycle-check2") << "  unvisit : " << nn << std::endl;
+    proc[nn] = true;
     visited.erase( nn );
     return Node::null();
   }else{
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index a0333ed8b..5166e118e 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -289,7 +289,7 @@ private:
   /** for checking if cycles exist */
   void checkCycles();
   Node searchForCycle( TNode n, TNode on,
-                       std::map< TNode, bool >& visited,
+                       std::map< TNode, bool >& visited, std::map< TNode, bool >& proc,
                        std::vector< TNode >& explanation, bool firstTime = true );
   /** for checking whether two codatatype terms must be equal */
   void separateBisimilar( std::vector< Node >& part, std::vector< std::vector< Node > >& part_out,
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 572e2790d..bdbbca706 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -81,7 +81,8 @@ TESTS =	\
 	dt-color-2.6.smt2 \
 	dt-match-pat-param-2.6.smt2 \
 	tuple-no-clash.cvc \
-	jsat-2.6.smt2
+	jsat-2.6.smt2 \
+	acyclicity-sr-ground096.smt2
 
 # rec5 -- no longer support subrange types
 FAILING_TESTS = \
diff --git a/test/regress/regress0/datatypes/acyclicity-sr-ground096.smt2 b/test/regress/regress0/datatypes/acyclicity-sr-ground096.smt2
new file mode 100644
index 000000000..1da69b279
--- /dev/null
+++ b/test/regress/regress0/datatypes/acyclicity-sr-ground096.smt2
@@ -0,0 +1,78 @@
+(set-logic QF_DT)
+(set-info :status unsat)
+(declare-datatypes ((T 0)) (( (f0) (f1 (proj0f1 T) (proj1f1 T) (proj2f1 T) (proj3f1 T)) (f2 (proj0f2 T) (proj1f2 T) (proj2f2 T)) (f3 (proj0f3 T) (proj1f3 T)) )))
+(declare-fun uc0 () T)
+(declare-fun uc1 () T)
+(declare-fun uc2 () T)
+(declare-fun uc3 () T)
+(declare-fun uc4 () T)
+(declare-fun uc5 () T)
+(declare-fun uc6 () T)
+(declare-fun uc7 () T)
+(declare-fun uc8 () T)
+(declare-fun uc9 () T)
+(declare-fun uc10 () T)
+(declare-fun uc11 () T)
+(declare-fun uc12 () T)
+(declare-fun uc13 () T)
+(declare-fun uc14 () T)
+(declare-fun uc15 () T)
+(declare-fun uc16 () T)
+(declare-fun uc17 () T)
+(declare-fun uc18 () T)
+(declare-fun uc19 () T)
+(declare-fun uc20 () T)
+(declare-fun uc21 () T)
+(declare-fun uc22 () T)
+(declare-fun uc23 () T)
+(declare-fun uc24 () T)
+(declare-fun uc25 () T)
+(declare-fun uc26 () T)
+(declare-fun uc27 () T)
+(declare-fun uc28 () T)
+(declare-fun uc29 () T)
+(declare-fun uc30 () T)
+(declare-fun uc31 () T)
+(declare-fun uc32 () T)
+(declare-fun uc33 () T)
+(declare-fun uc34 () T)
+(declare-fun uc35 () T)
+(declare-fun uc36 () T)
+(declare-fun uc37 () T)
+(declare-fun uc38 () T)
+(declare-fun uc39 () T)
+(declare-fun uc40 () T)
+(declare-fun uc41 () T)
+(declare-fun uc42 () T)
+(declare-fun uc43 () T)
+(declare-fun uc44 () T)
+(declare-fun uc45 () T)
+(declare-fun uc46 () T)
+(declare-fun uc47 () T)
+(declare-fun uc48 () T)
+(declare-fun uc49 () T)
+(declare-fun uc50 () T)
+(declare-fun uc51 () T)
+(declare-fun uc52 () T)
+(declare-fun uc53 () T)
+(declare-fun uc54 () T)
+(declare-fun uc55 () T)
+(declare-fun uc56 () T)
+(declare-fun uc57 () T)
+(declare-fun uc58 () T)
+(declare-fun uc59 () T)
+(declare-fun uc60 () T)
+(declare-fun uc61 () T)
+(declare-fun uc62 () T)
+(declare-fun uc63 () T)
+(declare-fun uc64 () T)
+(declare-fun uc65 () T)
+(declare-fun uc66 () T)
+(declare-fun uc67 () T)
+(declare-fun uc68 () T)
+(declare-fun uc69 () T)
+(declare-fun uc70 () T)
+(declare-fun uc71 () T)
+(declare-fun uc72 () T)
+(assert (or (and (= uc0 (f2 (f2 uc1 uc1 uc1) (f1 uc1 (f3 (f1 uc1 uc1 uc1 uc1) uc1) uc1 (f1 uc1 uc1 uc1 uc1)) (f3 uc1 (f3 (f2 uc1 uc1 uc1) (f2 uc1 uc1 uc1))))) (= uc1 (f1 uc2 (f1 (f3 uc2 uc2) (f2 uc2 uc2 uc2) (f3 uc2 uc2) (f3 uc2 uc2)) uc2 (f2 uc2 (f3 uc2 uc2) (f3 uc2 uc2)))) (= uc2 (f2 (f3 uc3 uc3) (f2 (f2 uc3 uc3 uc3) uc3 (f3 uc3 uc3)) (f2 uc3 uc3 uc3))) (= uc3 (f1 uc4 (f3 (f1 uc4 uc4 uc4 uc4) uc4) (f1 uc4 uc4 uc4 uc4) (f3 uc4 uc4))) (= uc4 (f1 (f2 uc5 uc5 uc5) (f2 uc5 uc5 uc5) (f1 uc5 uc5 uc5 uc5) uc5)) (= uc5 (f3 (f2 uc6 (f3 uc6 uc6) (f2 uc6 uc6 uc6)) uc6)) (= uc6 (f3 (f2 (f2 uc7 uc7 uc7) (f1 uc7 uc7 uc7 uc7) (f3 uc7 uc7)) uc7)) (= uc7 (f1 (f1 uc8 (f2 uc8 uc8 uc8) (f3 uc8 uc8) uc8) (f3 (f1 uc8 uc8 uc8 uc8) uc8) (f1 (f1 uc8 uc8 uc8 uc8) (f3 uc8 uc8) uc8 uc8) uc8)) (= uc8 (f3 (f2 (f3 uc9 uc9) uc9 (f1 uc9 uc9 uc9 uc9)) uc9)) (= uc9 (f1 (f1 (f1 uc10 uc10 uc10 uc10) (f2 uc10 uc10 uc10) (f3 uc10 uc10) (f1 uc10 uc10 uc10 uc10)) uc10 uc10 (f3 uc10 (f2 uc10 uc10 uc10)))) (= uc10 (f2 (f2 (f3 uc11 uc11) uc11 uc11) uc11 (f2 (f1 (f3 uc11 uc11) (f3 uc11 uc11) uc11 uc11) (f3 (f3 uc11 uc11) (f1 uc11 uc11 uc11 uc11)) (f3 uc11 (f1 uc11 uc11 uc11 uc11))))) (= uc11 (f3 (f3 uc12 (f2 uc12 uc12 uc12)) uc12)) (= uc12 (f3 (f1 (f2 uc0 uc0 uc0) uc0 (f3 uc0 uc0) (f1 uc0 uc0 uc0 uc0)) (f2 (f2 uc0 uc0 uc0) (f1 uc0 uc0 uc0 (f1 uc0 uc0 uc0 uc0)) (f1 uc0 uc0 uc0 uc0))))) (and (= uc13 (f1 (f1 uc14 uc14 uc14 uc14) (f3 uc14 uc14) (f3 uc14 uc14) (f3 uc14 uc14))) (= uc14 (f3 uc15 uc15)) (= uc15 (f3 uc16 (f2 uc16 uc16 uc16))) (= uc16 (f3 (f3 uc17 uc17) uc17)) (= uc17 (f3 (f3 uc18 uc18) (f1 uc18 uc18 uc18 uc18))) (= uc18 (f3 (f3 uc19 uc19) (f3 uc19 uc19))) (= uc19 (f1 (f1 uc20 uc20 uc20 uc20) uc20 (f3 uc20 uc20) (f2 uc20 uc20 uc20))) (= uc20 (f1 (f1 uc13 (f3 uc13 uc13) uc13 uc13) (f2 uc13 uc13 uc13) (f2 uc13 (f1 uc13 uc13 uc13 uc13) (f1 uc13 uc13 uc13 uc13)) uc13))) (and (= uc21 (f3 uc22 uc22)) (= uc22 (f2 uc23 (f2 (f1 uc23 uc23 uc23 (f3 uc23 uc23)) (f2 uc23 uc23 (f1 uc23 uc23 uc23 uc23)) (f3 uc23 uc23)) (f2 (f3 (f3 uc23 uc23) (f1 uc23 uc23 uc23 uc23)) (f1 (f3 uc23 uc23) (f2 uc23 uc23 uc23) uc23 (f2 uc23 uc23 uc23)) uc23))) (= uc23 (f1 (f2 uc21 uc21 uc21) (f2 uc21 uc21 uc21) (f3 uc21 uc21) uc21))) (and (= uc24 (f3 uc25 uc25)) (= uc25 (f3 (f3 (f3 uc26 uc26) (f3 uc26 uc26)) (f1 (f3 uc26 uc26) uc26 uc26 (f2 uc26 uc26 uc26)))) (= uc26 (f1 uc27 uc27 uc27 uc27)) (= uc27 (f2 (f3 uc28 uc28) (f2 (f2 (f1 uc28 uc28 uc28 uc28) (f1 uc28 uc28 uc28 uc28) (f2 uc28 uc28 uc28)) (f3 (f3 uc28 uc28) uc28) (f3 (f3 uc28 uc28) (f2 uc28 uc28 uc28))) uc28)) (= uc28 (f1 (f3 uc29 uc29) (f1 uc29 (f1 (f1 uc29 uc29 uc29 uc29) (f1 uc29 uc29 uc29 uc29) uc29 (f1 uc29 uc29 uc29 uc29)) uc29 (f3 uc29 (f3 uc29 uc29))) (f3 (f2 uc29 uc29 uc29) (f2 uc29 uc29 uc29)) (f2 (f1 (f1 uc29 uc29 uc29 uc29) uc29 (f3 uc29 uc29) uc29) (f3 (f3 uc29 uc29) (f1 uc29 uc29 uc29 uc29)) uc29))) (= uc29 (f2 uc30 (f1 uc30 uc30 uc30 uc30) uc30)) (= uc30 (f2 (f3 uc31 uc31) (f3 uc31 uc31) uc31)) (= uc31 (f1 (f3 uc32 uc32) (f3 uc32 uc32) (f2 uc32 uc32 uc32) uc32)) (= uc32 (f1 (f1 uc33 uc33 uc33 uc33) uc33 uc33 uc33)) (= uc33 (f3 (f3 uc34 uc34) (f1 (f1 uc34 uc34 uc34 uc34) (f1 uc34 uc34 uc34 uc34) (f3 uc34 uc34) uc34))) (= uc34 (f2 uc35 (f3 uc35 uc35) (f2 uc35 uc35 uc35))) (= uc35 (f3 uc36 (f3 uc36 (f3 uc36 uc36)))) (= uc36 (f3 (f3 uc37 uc37) uc37)) (= uc37 (f1 uc38 (f3 uc38 uc38) uc38 (f1 uc38 uc38 uc38 uc38))) (= uc38 (f2 (f3 uc39 uc39) (f2 uc39 uc39 uc39) uc39)) (= uc39 (f2 (f2 (f3 uc24 (f1 uc24 uc24 uc24 uc24)) (f2 (f1 uc24 uc24 uc24 uc24) (f1 uc24 uc24 uc24 uc24) (f1 uc24 uc24 uc24 uc24)) uc24) (f1 (f3 uc24 (f1 uc24 uc24 uc24 uc24)) (f1 uc24 uc24 uc24 uc24) (f1 uc24 uc24 uc24 uc24) uc24) (f1 uc24 uc24 uc24 uc24)))) (and (= uc40 (f3 uc41 uc41)) (= uc41 (f1 uc42 uc42 uc42 uc42)) (= uc42 (f1 (f1 (f2 uc43 uc43 uc43) (f2 uc43 uc43 uc43) uc43 uc43) (f3 uc43 uc43) (f3 uc43 (f2 uc43 uc43 uc43)) uc43)) (= uc43 (f1 (f3 uc44 uc44) uc44 uc44 (f3 uc44 (f3 uc44 uc44)))) (= uc44 (f2 uc45 uc45 uc45)) (= uc45 (f3 uc46 (f3 (f3 (f1 uc46 uc46 uc46 uc46) uc46) (f1 uc46 uc46 uc46 uc46)))) (= uc46 (f3 (f1 (f3 uc47 uc47) uc47 (f1 uc47 uc47 uc47 uc47) (f2 uc47 uc47 uc47)) (f3 (f2 uc47 uc47 uc47) (f2 uc47 uc47 uc47)))) (= uc47 (f1 (f2 (f1 uc48 uc48 uc48 uc48) (f1 uc48 uc48 uc48 uc48) uc48) (f3 (f1 uc48 uc48 uc48 uc48) (f2 uc48 uc48 uc48)) uc48 uc48)) (= uc48 (f2 uc49 (f1 (f3 uc49 uc49) (f3 uc49 uc49) (f1 uc49 uc49 uc49 uc49) (f1 uc49 uc49 uc49 uc49)) (f1 (f1 uc49 uc49 uc49 uc49) (f2 uc49 uc49 uc49) uc49 (f1 (f3 uc49 uc49) (f3 uc49 uc49) (f2 uc49 uc49 uc49) (f3 uc49 uc49))))) (= uc49 (f2 uc50 uc50 (f1 (f1 (f1 uc50 uc50 uc50 uc50) uc50 uc50 uc50) (f3 uc50 uc50) uc50 uc50))) (= uc50 (f1 (f1 uc51 uc51 uc51 uc51) uc51 (f3 uc51 uc51) (f2 uc51 uc51 uc51))) (= uc51 (f1 uc52 uc52 uc52 uc52)) (= uc52 (f1 (f3 (f1 uc40 uc40 uc40 uc40) (f3 (f1 uc40 uc40 uc40 uc40) (f2 uc40 uc40 uc40))) (f1 (f2 uc40 (f2 uc40 uc40 uc40) (f2 uc40 uc40 uc40)) uc40 (f2 uc40 uc40 uc40) (f2 (f2 uc40 uc40 uc40) uc40 uc40)) (f1 uc40 uc40 uc40 uc40) (f3 (f3 (f1 uc40 uc40 uc40 uc40) (f3 uc40 uc40)) (f3 uc40 uc40))))) (and (= uc53 (f1 uc54 uc54 (f1 uc54 uc54 uc54 uc54) (f2 uc54 uc54 uc54))) (= uc54 (f1 uc55 (f2 uc55 uc55 uc55) uc55 (f2 (f3 uc55 uc55) (f2 uc55 uc55 uc55) (f1 uc55 uc55 uc55 uc55)))) (= uc55 (f2 (f1 uc56 uc56 uc56 uc56) (f1 uc56 uc56 uc56 uc56) (f3 uc56 uc56))) (= uc56 (f2 (f1 (f1 uc57 uc57 uc57 uc57) uc57 (f2 uc57 uc57 uc57) (f1 uc57 uc57 uc57 uc57)) (f1 (f1 (f2 uc57 uc57 uc57) uc57 (f1 uc57 uc57 uc57 uc57) (f1 uc57 uc57 uc57 uc57)) (f1 uc57 uc57 uc57 (f2 uc57 uc57 uc57)) uc57 (f1 uc57 uc57 uc57 uc57)) (f2 uc57 uc57 (f3 (f1 uc57 uc57 uc57 uc57) uc57)))) (= uc57 (f3 uc58 (f2 uc58 (f3 uc58 uc58) (f2 uc58 uc58 uc58)))) (= uc58 (f2 (f2 uc59 (f1 (f1 uc59 uc59 uc59 uc59) (f1 uc59 uc59 uc59 uc59) (f2 uc59 uc59 uc59) (f2 uc59 uc59 uc59)) (f3 (f3 uc59 uc59) uc59)) (f1 uc59 uc59 uc59 uc59) uc59)) (= uc59 (f3 uc60 (f2 uc60 (f3 uc60 uc60) uc60))) (= uc60 (f3 uc61 (f2 uc61 uc61 uc61))) (= uc61 (f2 (f2 (f1 uc62 uc62 uc62 uc62) uc62 (f3 uc62 uc62)) (f1 uc62 uc62 uc62 uc62) uc62)) (= uc62 (f1 uc63 (f1 uc63 uc63 uc63 (f3 uc63 uc63)) (f3 uc63 uc63) (f1 uc63 uc63 uc63 uc63))) (= uc63 (f1 (f2 uc64 uc64 uc64) (f2 uc64 uc64 uc64) uc64 uc64)) (= uc64 (f1 (f3 (f1 uc65 uc65 uc65 uc65) uc65) (f2 uc65 uc65 uc65) (f2 uc65 uc65 uc65) (f2 uc65 (f1 (f2 uc65 uc65 uc65) uc65 (f2 uc65 uc65 uc65) (f2 uc65 uc65 uc65)) (f1 uc65 uc65 uc65 uc65)))) (= uc65 (f1 uc66 uc66 uc66 uc66)) (= uc66 (f3 (f1 uc67 uc67 uc67 uc67) (f1 uc67 uc67 uc67 uc67))) (= uc67 (f1 (f2 uc68 uc68 (f1 uc68 uc68 uc68 uc68)) uc68 (f1 uc68 uc68 uc68 uc68) (f3 (f1 uc68 uc68 uc68 uc68) uc68))) (= uc68 (f1 (f1 (f3 (f3 uc69 uc69) (f3 uc69 uc69)) (f3 uc69 uc69) uc69 uc69) (f3 (f3 uc69 (f2 uc69 uc69 uc69)) uc69) (f2 (f3 (f3 uc69 uc69) (f1 uc69 uc69 uc69 uc69)) (f1 uc69 (f3 uc69 uc69) uc69 uc69) (f2 uc69 uc69 uc69)) (f1 (f1 (f1 uc69 uc69 uc69 uc69) (f1 uc69 uc69 uc69 uc69) uc69 (f1 uc69 uc69 uc69 uc69)) (f2 (f2 uc69 uc69 uc69) (f2 uc69 uc69 uc69) uc69) uc69 uc69))) (= uc69 (f3 uc70 uc70)) (= uc70 (f1 uc71 (f1 (f1 uc71 uc71 uc71 uc71) (f1 uc71 uc71 uc71 uc71) (f1 uc71 uc71 uc71 uc71) (f1 uc71 uc71 uc71 uc71)) (f2 uc71 uc71 uc71) (f3 uc71 uc71))) (= uc71 (f3 (f3 uc72 (f3 uc72 uc72)) (f3 (f3 uc72 uc72) (f1 uc72 uc72 uc72 uc72)))) (= uc72 (f1 uc53 uc53 uc53 uc53)))))
+(check-sat)