Add cardinality class definition (#6302)

This is work towards correcting our computation of whether a type is finite. Currently, arrays/functions with uninterpreted sorts as element/range types are always considered infinite. This is incorrect if finite model finding is enabled, since the interpretation of the uninterpreted sort can be one. This leads to errors during model building due to exhausted values (#4260, #6100).

This PR adds a new concept of a cardinality class, which is required for properly categorizing types with/without finite model finding.

A followup PR will replace TypeNode::isFinite with TypeNode::getCardinalityClass. Calls to TypeNode::isFinite will be replaced by calls to TheoryState::isTypeFinite, which will properly take cardinality classes into account.

1 files changed, 67 insertions, 0 deletions

diff --git a/src/util/cardinality_class.cpp b/src/util/cardinality_class.cpp
new file mode 100644
index 000000000..32390a97c
--- /dev/null
+++ b/src/util/cardinality_class.cpp
@@ -0,0 +1,67 @@
+/*********************                                                        */
+/*! \file cardinality_class.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utilities for cardinality classes
+ **/
+
+#include "util/cardinality_class.h"
+
+#include <iostream>
+
+namespace cvc5 {
+
+const char* toString(CardinalityClass c)
+{
+  switch (c)
+  {
+    case CardinalityClass::ONE: return "ONE";
+    case CardinalityClass::INTERPRETED_ONE: return "INTERPRETED_ONE";
+    case CardinalityClass::FINITE: return "FINITE";
+    case CardinalityClass::INTERPRETED_FINITE: return "INTERPRETED_FINITE";
+    case CardinalityClass::INFINITE: return "INFINITE";
+    case CardinalityClass::UNKNOWN: return "UNKNOWN";
+    default: return "?CardinalityClass?";
+  }
+}
+
+std::ostream& operator<<(std::ostream& out, CardinalityClass c)
+{
+  out << toString(c);
+  return out;
+}
+
+CardinalityClass minCardinalityClass(CardinalityClass c1, CardinalityClass c2)
+{
+  return c1 < c2 ? c1 : c2;
+}
+
+CardinalityClass maxCardinalityClass(CardinalityClass c1, CardinalityClass c2)
+{
+  return c1 > c2 ? c1 : c2;
+}
+
+bool isCardinalityClassFinite(CardinalityClass c, bool fmfEnabled)
+{
+  if (c == CardinalityClass::ONE || c == CardinalityClass::FINITE)
+  {
+    return true;
+  }
+  if (fmfEnabled)
+  {
+    // if finite model finding is enabled, interpreted one/finite are also
+    // considered finite.
+    return c == CardinalityClass::INTERPRETED_ONE
+           || c == CardinalityClass::INTERPRETED_FINITE;
+  }
+  return false;
+}
+
+}  // namespace cvc5