Fix strategy for datatypes solver involving acyclicity (cvc5#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

@@ -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")

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

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)