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.

diff --git a/src/util/cardinality_class.cpp b/src/util/cardinality_class.cpp
new file mode 100644 (file)
index 0000000..32390a9
--- /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

diff --git a/src/util/cardinality_class.h b/src/util/cardinality_class.h
new file mode 100644 (file)
index 0000000..c468975
--- /dev/null
+++ b/src/util/cardinality_class.h
@@ -0,0 +1,97 @@
+/*********************                                                        */
+/*! \file cardinality_class.h
+ ** \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 "cvc4_private.h"
+
+#ifndef CVC4__UTIL__CARDINALITY_CLASS_H
+#define CVC4__UTIL__CARDINALITY_CLASS_H
+
+#include <iosfwd>
+
+namespace cvc5 {
+
+/**
+ * Cardinality classes. A type has exactly one cardinality class. The
+ * cardinality class of a type is independent of the state of solver.
+ *
+ * The purposes of these classifications is solely to determine whether or not
+ * a type should be considered finite. This includes use cases for when
+ * finite model finding is enabled or disabled.
+ *
+ * Note that the order of this enum is important for the implementation of
+ * minCardinalityClass and maxCardinalityClass below.
+ */
+enum class CardinalityClass : uint64_t
+{
+  // the type has cardinality one in all interpretations
+  //
+  // Examples: unit datatypes, arrays with unit datatype elements
+  ONE,
+  // the type has cardinality one under the assumption that uninterpreted
+  // sorts have cardinality one
+  //
+  // Examples: uninterpreted sorts, arrays with uninterpreted sort elements
+  INTERPRETED_ONE,
+  // the type is finite in all interpretations, and does not fit any of the
+  // above classifications
+  //
+  // Examples: Booleans, bitvectors, floating points, sets of Bools
+  FINITE,
+  // the type is finite under the assumption that uninterpreted sorts have
+  // cardinality one, and does not fit any of the above classifications
+  //
+  // Examples: sets of uninterpreted sorts, arrays whose index types are
+  // uninterpreted sorts and element sorts are finite
+  INTERPRETED_FINITE,
+  // the type is infinite in all interpretations
+  //
+  // Examples: integers, reals, strings, sequences, bags
+  INFINITE,
+  // the cardinality is unknown
+  UNKNOWN
+};
+
+/**
+ * Converts a cardinality class to a string.
+ *
+ * @param c The proof rule
+ * @return The name of the proof rule
+ */
+const char* toString(CardinalityClass c);
+
+/**
+ * Writes a cardinality class name to a stream.
+ *
+ * @param out The stream to write to
+ * @param c The cardinality class to write to the stream
+ * @return The stream
+ */
+std::ostream& operator<<(std::ostream& out, CardinalityClass c);
+
+/** Take the min class of c1 and c2 */
+CardinalityClass minCardinalityClass(CardinalityClass c1, CardinalityClass c2);
+/** Take the max class of c1 and c2 */
+CardinalityClass maxCardinalityClass(CardinalityClass c1, CardinalityClass c2);
+/**
+ * Is a type with the given cardinality class finite?
+ *
+ * If fmfEnabled is true, then this method assumes that uninterpreted sorts
+ * have cardinality one. If fmfEnabled is false, then this method assumes that
+ * uninterpreted sorts have infinite cardinality.
+ */
+bool isCardinalityClassFinite(CardinalityClass c, bool fmfEnabled);
+
+}  // namespace cvc5
+
+#endif