Add cardinality constraint utilities (#7286)

This class will be used to replace the `fmf.card` operator with a 0-ary indexed parameterized nullary predicate for representing cardinality constraints for UF.

This is in preparation for eliminating hacks in the core of theory combination for e.g. not considering the dummy arguments of cardinality constraints to be shared terms.

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 437f0b54fc8c153b12f6347cabe33c9a52bd7028..e73960676591d3091912ab6f89e7a7a1e45529ec 100644 (file)
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -24,6 +24,8 @@ libcvc5_add_sources(
   attribute_unique_id.h
   bound_var_manager.cpp
   bound_var_manager.h
+  cardinality_constraint.cpp
+  cardinality_constraint.h
   emptyset.cpp
   emptyset.h
   emptybag.cpp

diff --git a/src/expr/cardinality_constraint.cpp b/src/expr/cardinality_constraint.cpp
new file mode 100644 (file)
index 0000000..3841228
--- /dev/null
+++ b/src/expr/cardinality_constraint.cpp
@@ -0,0 +1,101 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 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.
+ * ****************************************************************************
+ *
+ * The cardinality constraint operator
+ */
+
+#include "expr/cardinality_constraint.h"
+
+#include <iostream>
+
+#include "expr/type_node.h"
+
+namespace cvc5 {
+
+CardinalityConstraint::CardinalityConstraint(const TypeNode& type,
+                                             const Integer& ub)
+    : d_type(new TypeNode(type)), d_ubound(ub)
+{
+  AlwaysAssert(type.isSort())
+      << "Unexpected cardinality constraints for " << type;
+}
+
+CardinalityConstraint::CardinalityConstraint(const CardinalityConstraint& other)
+    : d_type(new TypeNode(other.getType())), d_ubound(other.getUpperBound())
+{
+}
+
+CardinalityConstraint::~CardinalityConstraint() {}
+
+const TypeNode& CardinalityConstraint::getType() const { return *d_type; }
+
+const Integer& CardinalityConstraint::getUpperBound() const { return d_ubound; }
+
+bool CardinalityConstraint::operator==(const CardinalityConstraint& cc) const
+{
+  return getType() == cc.getType() && getUpperBound() == cc.getUpperBound();
+}
+
+bool CardinalityConstraint::operator!=(const CardinalityConstraint& cc) const
+{
+  return !(*this == cc);
+}
+
+std::ostream& operator<<(std::ostream& out, const CardinalityConstraint& cc)
+{
+  return out << "fmf.card(" << cc.getType() << ", " << cc.getUpperBound()
+             << ')';
+}
+
+CombinedCardinalityConstraint::CombinedCardinalityConstraint(const Integer& ub)
+    : d_ubound(ub)
+{
+}
+
+CombinedCardinalityConstraint::CombinedCardinalityConstraint(
+    const CombinedCardinalityConstraint& other)
+    : d_ubound(other.getUpperBound())
+{
+}
+
+CombinedCardinalityConstraint::~CombinedCardinalityConstraint() {}
+
+const Integer& CombinedCardinalityConstraint::getUpperBound() const
+{
+  return d_ubound;
+}
+
+bool CombinedCardinalityConstraint::operator==(
+    const CombinedCardinalityConstraint& cc) const
+{
+  return getUpperBound() == cc.getUpperBound();
+}
+
+bool CombinedCardinalityConstraint::operator!=(
+    const CombinedCardinalityConstraint& cc) const
+{
+  return !(*this == cc);
+}
+
+std::ostream& operator<<(std::ostream& out,
+                         const CombinedCardinalityConstraint& cc)
+{
+  return out << "fmf.card(" << cc.getUpperBound() << ')';
+}
+
+size_t CombinedCardinalityConstraintHashFunction::operator()(
+    const CombinedCardinalityConstraint& cc) const
+{
+  return cc.getUpperBound().hash();
+}
+
+}  // namespace cvc5

diff --git a/src/expr/cardinality_constraint.h b/src/expr/cardinality_constraint.h
new file mode 100644 (file)
index 0000000..a51ba54
--- /dev/null
+++ b/src/expr/cardinality_constraint.h
@@ -0,0 +1,105 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 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.
+ * ****************************************************************************
+ *
+ * The cardinality constraint operator
+ */
+
+#include "cvc5_public.h"
+
+#ifndef CVC5__EXPR__CARDINALITY_CONSTRAINT_H
+#define CVC5__EXPR__CARDINALITY_CONSTRAINT_H
+
+#include <iosfwd>
+#include <memory>
+
+#include "util/integer.h"
+#include "util/hash.h"
+
+namespace cvc5 {
+
+class TypeNode;
+
+/**
+ * A cardinality constraint, handled in the cardinality extension of the UF
+ * solver, used for finite model finding.
+ */
+class CardinalityConstraint
+{
+ public:
+  /**
+   * Constructs a cardinality constraint of the specified type, which should
+   * be an uninterpreted sort.
+   */
+  CardinalityConstraint(const TypeNode& ufType, const Integer& ub);
+  ~CardinalityConstraint();
+  CardinalityConstraint(const CardinalityConstraint& other);
+
+  /** Get the type of the cardinality constraint */
+  const TypeNode& getType() const;
+  /** Get the upper bound value of the cardinality constraint */
+  const Integer& getUpperBound() const;
+
+  bool operator==(const CardinalityConstraint& cc) const;
+  bool operator!=(const CardinalityConstraint& cc) const;
+
+ private:
+  /** The type that the cardinality constraint is for */
+  std::unique_ptr<TypeNode> d_type;
+  /** The upper bound on the cardinality of the above type */
+  const Integer d_ubound;
+};
+
+std::ostream& operator<<(std::ostream& out, const CardinalityConstraint& cc);
+
+using CardinalityConstraintHashFunction = PairHashFunction<TypeNode,
+                                                           Integer,
+                                                           std::hash<TypeNode>,
+                                                           IntegerHashFunction>;
+
+/**
+ * A combined cardinality constraint, handled in the cardinality extension of
+ * the UF solver, used for finite model finding for bounding the sum of
+ * cardinalities of all uninterpreted sorts.
+ */
+class CombinedCardinalityConstraint
+{
+ public:
+  /**
+   * Constructs a cardinality constraint of the specified type, which should
+   * be an uninterpreted sort.
+   */
+  CombinedCardinalityConstraint(const Integer& ub);
+  ~CombinedCardinalityConstraint();
+  CombinedCardinalityConstraint(const CombinedCardinalityConstraint& other);
+
+  /** Get the upper bound value of the cardinality constraint */
+  const Integer& getUpperBound() const;
+
+  bool operator==(const CombinedCardinalityConstraint& cc) const;
+  bool operator!=(const CombinedCardinalityConstraint& cc) const;
+
+ private:
+  /** The upper bound on the cardinality of the above type */
+  const Integer d_ubound;
+};
+
+std::ostream& operator<<(std::ostream& out,
+                         const CombinedCardinalityConstraint& cc);
+
+struct CombinedCardinalityConstraintHashFunction
+{
+  size_t operator()(const CombinedCardinalityConstraint& cc) const;
+};
+
+}  // namespace cvc5
+
+#endif