From a127a898b3b15406aa3adfd851d047e1c3b93fdf Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 25 Jul 2024 12:29:18 -0500
Subject: [PATCH] Fix strategy for datatypes solver involving acyclicity
 (#11094)

This fixes model soundness issues in the quantifier-free datatypes
solver. cvc5 could fail to recognize there is a conflict due to an
acyclicity inference. The issue occurs as early as cvc5 0.0.2.

The issue was caused by the strategy for the datatypes theory solver
using 2 separate loops for checking for cycles and instantiate (i.e.
inferring an equality based on a tester). The latter could introduce a
fact that should then lead to us checking need to check for cycles
again. However, we could terminate with "sat" if there was nothing else
to do. The solver has always had this structure, I suspect that a change
to the fact vs lemma policy made this design incorrect.

Adds a regression exhibiting the issue that is fixed now.
---
 src/theory/datatypes/theory_datatypes.cpp        | 15 ++++++++-------
 test/regress/cli/CMakeLists.txt                  |  1 +
 .../cli/regress0/datatypes/yoni-cyclic.smt2      | 16 ++++++++++++++++
 3 files changed, 25 insertions(+), 7 deletions(-)
 create mode 100644 test/regress/cli/regress0/datatypes/yoni-cyclic.smt2

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index c0ce917aa36..48f83c08005 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -202,20 +202,20 @@ void TheoryDatatypes::postCheck(Effort level)
     Assert(!d_im.hasPendingFact());
     do {
       d_im.reset();
-      Trace("datatypes-proc") << "Check cycles..." << std::endl;
+      Trace("datatypes-check") << "Check cycles..." << std::endl;
       checkCycles();
-      Trace("datatypes-proc") << "...finish check cycles" << std::endl;
+      Trace("datatypes-check") << "...finish check cycles" << std::endl;
       d_im.process();
       if (d_state.isInConflict() || d_im.hasSentLemma())
       {
         return;
       }
-    } while (d_im.hasSentFact());
-
-    //check for splits
-    Trace("datatypes-debug") << "Check for splits " << endl;
-    do {
+      else if (d_im.hasSentFact())
+      {
+        continue;
+      }
       d_im.reset();
+      Trace("datatypes-check") << "Check for splits " << endl;
       // check for splits
       checkSplit();
       if (d_im.hasSentLemma())
@@ -231,6 +231,7 @@ void TheoryDatatypes::postCheck(Effort level)
         Trace("datatypes-debug") << "Flush pending facts..." << std::endl;
         d_im.process();
       }
+      Trace("datatypes-check") << "...finish check splits" << std::endl;
     } while (!d_state.isInConflict() && !d_im.hasSentLemma()
              && d_im.hasSentFact());
     Trace("datatypes-debug")
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 2cdfbc7e70e..be4d31b0b85 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -743,6 +743,7 @@ set(regress_0_tests
   regress0/datatypes/v3l60006.cvc.smt2
   regress0/datatypes/v5l30058.cvc.smt2
   regress0/datatypes/wrong-sel-simp.cvc.smt2
+  regress0/datatypes/yoni-cyclic.smt2
   regress0/dd.bad-conv-rewrite.smt2
   regress0/decision/aufbv-fuzz01.smtv1.smt2
   regress0/decision/bitvec0.delta01.smtv1.smt2
diff --git a/test/regress/cli/regress0/datatypes/yoni-cyclic.smt2 b/test/regress/cli/regress0/datatypes/yoni-cyclic.smt2
new file mode 100644
index 00000000000..2b8b07e6e4d
--- /dev/null
+++ b/test/regress/cli/regress0/datatypes/yoni-cyclic.smt2
@@ -0,0 +1,16 @@
+; EXPECT: unsat
+(set-logic ALL)
+
+(declare-datatypes ((T1 0)(T2 0))
+ (((cons1 (id1 Int) (tail1 T2)))
+ ((Nil) (cons2 (id2 Int) (tail2 T1))))
+)
+
+(declare-const x T1)
+(declare-const y T2)
+
+(assert (= x (tail2 y)))
+(assert (= y (tail1 x)))
+(assert (not (= Nil y)))
+
+(check-sat)