From ebc7d0ffafe9736ecab5649d2a3957e55e06c515 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 22 Jun 2022 13:16:00 -0500
Subject: [PATCH] Fix sort inference for equality over finite types (#8897)

Sort inference for equality was not considering equality over some finite types, leading to potential solution soundness.

Fixes #8883.
---
 src/theory/sort_inference.cpp                 | 28 +++++++++----------
 src/theory/sort_inference.h                   |  2 +-
 test/regress/cli/CMakeLists.txt               |  1 +
 .../datatypes/issue8883-sort-inf.smt2         |  8 ++++++
 4 files changed, 24 insertions(+), 15 deletions(-)
 create mode 100644 test/regress/cli/regress0/datatypes/issue8883-sort-inf.smt2

diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index 52a333cc3..91d8b2a15 100644
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -426,19 +426,16 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map<
     Trace("sort-inference-debug") << "...Process " << n << std::endl;
 
     int retType;
-    if( n.getKind()==kind::EQUAL && !n[0].getType().isBoolean() ){
+    // we only do this for non-finite types, as finite types have cardinality
+    // restrictions.
+    if (n.getKind() == kind::EQUAL
+        && !isCardinalityClassFinite(n[0].getType().getCardinalityClass(),
+                                     false))
+    {
       Trace("sort-inference-debug") << "For equality " << n << ", set equal types from : " << n[0].getType() << " " << n[1].getType() << std::endl;
-      //if original types are mixed (e.g. Int/Real), don't commit type equality in either direction
-      if( n[0].getType()!=n[1].getType() ){
-        //for now, assume the original types
-        for( unsigned i=0; i<2; i++ ){
-          int ct = getIdForType( n[i].getType() );
-          setEqual( child_types[i], ct );
-        }
-      }else{
-        //we only require that the left and right hand side must be equal
-        setEqual( child_types[0], child_types[1] );
-      }
+      Assert(n[0].getType() == n[1].getType());
+      // we only require that the left and right hand side must be equal
+      setEqual(child_types[0], child_types[1]);
       d_equality_types[n] = child_types[0];
       retType = getIdForType( n.getType() );
     }
@@ -689,7 +686,9 @@ Node SortInference::simplifyNode(
           tnnc = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() );
           Assert(!tnnc.isNull());
         }
-        else if (n.getKind() == kind::EQUAL && !n[0].getType().isBoolean()
+        else if (n.getKind() == kind::EQUAL
+                 && !isCardinalityClassFinite(
+                     n[0].getType().getCardinalityClass(), false)
                  && i == 0)
         {
           Assert(d_equality_types.find(n) != d_equality_types.end());
@@ -880,7 +879,8 @@ bool SortInference::isWellSorted( Node n ) {
   }
 }
 
-bool SortInference::isMonotonic( TypeNode tn ) {
+bool SortInference::isMonotonic(TypeNode tn) const
+{
   Assert(tn.isUninterpretedSort());
   return d_non_monotonic_sorts_orig.find( tn )==d_non_monotonic_sorts_orig.end();
 }
diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h
index 7fe0f588b..00256e32f 100644
--- a/src/theory/sort_inference.h
+++ b/src/theory/sort_inference.h
@@ -149,7 +149,7 @@ private:
    */
   void computeMonotonicity(const std::vector<Node>& assertions);
   /** return true if tn was inferred to be monotonic */
-  bool isMonotonic(TypeNode tn);
+  bool isMonotonic(TypeNode tn) const;
   //get sort id for term n
   int getSortId( Node n );
   //get sort id for variable of quantified formula f
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index c131860e7..45eb213b8 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -541,6 +541,7 @@ set(regress_0_tests
   regress0/datatypes/issue2838.cvc.smt2
   regress0/datatypes/issue4393-cdt-model.smt2
   regress0/datatypes/issue5280-no-nrec.smt2
+  regress0/datatypes/issue8883-sort-inf.smt2
   regress0/datatypes/jsat-2.6.smt2
   regress0/datatypes/list-bool.smt2
   regress0/datatypes/list-update.smt2
diff --git a/test/regress/cli/regress0/datatypes/issue8883-sort-inf.smt2 b/test/regress/cli/regress0/datatypes/issue8883-sort-inf.smt2
new file mode 100644
index 000000000..678b0bd2f
--- /dev/null
+++ b/test/regress/cli/regress0/datatypes/issue8883-sort-inf.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --sort-inference
+; EXPECT: unsat
+(set-logic ALL)
+(declare-datatypes ((Data 1)) ((par (T) ((data)))))
+(declare-fun p2 () (Data Bool))
+(declare-fun p3 () (Data Bool))
+(assert (not (= p2 p3)))
+(check-sat)
-- 
2.30.2