Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/cardinality.h	Lines:	25	25	100.0 %
Date:	2021-09-18	Branches:	12	22	54.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Tim King, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * Representation of cardinality.
 *
 * Simple class to represent a cardinality; used by the cvc5 type system
 * give the cardinality of sorts.
 */

#include "cvc5_public.h"

#ifndef CVC5__CARDINALITY_H
#define CVC5__CARDINALITY_H

#include <iosfwd>

#include "util/integer.h"

namespace cvc5 {

/**
 * Representation for a Beth number, used only to construct
 * Cardinality objects.
 */
class CardinalityBeth
{
  Integer d_index;

 public:
  CardinalityBeth(const Integer& beth);

  const Integer& getNumber() const { return d_index; }

}; /* class CardinalityBeth */

/**
 * Representation for an unknown cardinality.
 */
class CardinalityUnknown
{
 public:
  CardinalityUnknown() {}
  ~CardinalityUnknown() {}
}; /* class CardinalityUnknown */

/**
 * A simple representation of a cardinality.  We store an
 * arbitrary-precision integer for finite cardinalities, and we
 * distinguish infinite cardinalities represented as Beth numbers.
 */
class Cardinality
{
  /** Cardinality of the integers */
  static const Integer s_intCard;

  /** Cardinality of the reals */
  static const Integer s_realCard;

  /** A representation for unknown cardinality */
  static const Integer s_unknownCard;

  /** A representation for large, finite cardinality */
  static const Integer s_largeFiniteCard;

  /**
   * In the case of finite cardinality, this is > 0, and is equal to
   * the cardinality+1.  If infinite, it is < 0, and is Beth[|card|-1].
   * That is, "-1" means Beth 0 == |Z|, "-2" means Beth 1 == |R|, etc.
   * If this field is 0, the cardinality is unknown.
   *
   * We impose a ceiling on finite cardinalities of 2^64.  If this field
   * is >= 2^64 + 1, we consider it at "ceiling" cardinality, and
   * comparisons between all such cardinalities result in "unknown."
   */
  Integer d_card;

 public:
  /** The cardinality of the set of integers. */
  static const Cardinality INTEGERS;

  /** The cardinality of the set of real numbers. */
  static const Cardinality REALS;

  /** The unknown cardinality */
  static const Cardinality UNKNOWN_CARD;

  /** Used as a result code for Cardinality::compare(). */
  enum CardinalityComparison
  {
    LESS,
    EQUAL,
    GREATER,
    UNKNOWN
  }; /* enum CardinalityComparison */

  /**
   * Construct a finite cardinality equal to the integer argument.
   * The argument must be nonnegative.  If we change this to an
   * "unsigned" argument to enforce the restriction, we mask some
   * errors that automatically convert, like "Cardinality(-1)".
   */
  Cardinality(long card);

  /**
   * Construct a finite cardinality equal to the integer argument.
   * The argument must be nonnegative.
   */
  Cardinality(const Integer& card);

  /**
   * Construct an infinite cardinality equal to the given Beth number.
   */
  Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) {}

  /**
   * Construct an unknown cardinality.
   */
  Cardinality(CardinalityUnknown) : d_card(0) {}

  /**
   * Returns true iff this cardinality is unknown.  "Unknown" in this
   * sense means that the cardinality is completely unknown; it might
   * be finite, or infinite---anything.  Large, finite cardinalities
   * at the "ceiling" return "false" for isUnknown() and true for
   * isFinite() and isLargeFinite().
   */
  bool isUnknown() const { return d_card == 0; }

  /** Returns true iff this cardinality is finite. */
  bool isFinite() const { return d_card > 0; }
  /** Returns true iff this cardinality is one */
  bool isOne() const { return d_card == 2; }
  /**
   * Returns true iff this cardinality is finite and large (i.e.,
   * at the ceiling of representable finite cardinalities).
   */
  bool isLargeFinite() const { return d_card >= s_largeFiniteCard; }

  /** Returns true iff this cardinality is infinite. */
  bool isInfinite() const { return d_card < 0; }

  /**
   * Returns true iff this cardinality is finite or countably
   * infinite.
   */
  bool isCountable() const { return isFinite() || d_card == s_intCard; }

  /**
   * In the case that this cardinality is finite, return its
   * cardinality.  (If this cardinality is infinite, this function
   * throws an IllegalArgumentException.)
   */
  Integer getFiniteCardinality() const;

  /**
   * In the case that this cardinality is infinite, return its Beth
   * number.  (If this cardinality is finite, this function throws an
   * IllegalArgumentException.)
   */
  Integer getBethNumber() const;

  /** Assigning addition of this cardinality with another. */
  Cardinality& operator+=(const Cardinality& c);

  /** Assigning multiplication of this cardinality with another. */
  Cardinality& operator*=(const Cardinality& c);

  /** Assigning exponentiation of this cardinality with another. */
  Cardinality& operator^=(const Cardinality& c);

  /** Add two cardinalities. */
  Cardinality operator+(const Cardinality& c) const {
    Cardinality card(*this);
    card += c;
    return card;
  }

  /** Multiply two cardinalities. */
  Cardinality operator*(const Cardinality& c) const {
    Cardinality card(*this);
    card *= c;
    return card;
  }

  /**
   * Exponentiation of two cardinalities.
   */
  Cardinality operator^(const Cardinality& c) const {
    Cardinality card(*this);
    card ^= c;
    return card;
  }

  /**
   * Compare two cardinalities.  This can return UNKNOWN if two
   * finite cardinalities are at the ceiling (and thus not precisely
   * represented), or if one or the other is the special "unknown"
   * cardinality.
   */
  Cardinality::CardinalityComparison compare(const Cardinality& c) const;

  /**
   * Return a string representation of this cardinality.
   */
  std::string toString() const;

  /**
   * Compare two cardinalities and if it is known that the current
   * cardinality is smaller or equal to c, it returns true.
   */
  bool knownLessThanOrEqual(const Cardinality& c) const;
}; /* class Cardinality */

/** Print an element of the InfiniteCardinality enumeration. */
std::ostream& operator<<(std::ostream& out, CardinalityBeth b);

/** Print a cardinality in a human-readable fashion. */
std::ostream& operator<<(std::ostream& out, const Cardinality& c);

}  // namespace cvc5

#endif /* CVC5__CARDINALITY_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Tim King, Mathias Preiner
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Representation of cardinality.
14		*
15		* Simple class to represent a cardinality; used by the cvc5 type system
16		* give the cardinality of sorts.
17		*/
18
19		#include "cvc5_public.h"
20
21		#ifndef CVC5__CARDINALITY_H
22		#define CVC5__CARDINALITY_H
23
24		#include <iosfwd>
25
26		#include "util/integer.h"
27
28		namespace cvc5 {
29
30		/**
31		* Representation for a Beth number, used only to construct
32		* Cardinality objects.
33		*/
34	19717	class CardinalityBeth
35		{
36		Integer d_index;
37
38		public:
39		CardinalityBeth(const Integer& beth);
40
41	19717	const Integer& getNumber() const { return d_index; }
42
43		}; /* class CardinalityBeth */
44
45		/**
46		* Representation for an unknown cardinality.
47		*/
48		class CardinalityUnknown
49		{
50		public:
51	15460	CardinalityUnknown() {}
52	15460	~CardinalityUnknown() {}
53		}; /* class CardinalityUnknown */
54
55		/**
56		* A simple representation of a cardinality. We store an
57		* arbitrary-precision integer for finite cardinalities, and we
58		* distinguish infinite cardinalities represented as Beth numbers.
59		*/
60	170451	class Cardinality
61		{
62		/** Cardinality of the integers */
63		static const Integer s_intCard;
64
65		/** Cardinality of the reals */
66		static const Integer s_realCard;
67
68		/** A representation for unknown cardinality */
69		static const Integer s_unknownCard;
70
71		/** A representation for large, finite cardinality */
72		static const Integer s_largeFiniteCard;
73
74		/**
75		* In the case of finite cardinality, this is > 0, and is equal to
76		* the cardinality+1. If infinite, it is < 0, and is Beth[\|card\|-1].
77		* That is, "-1" means Beth 0 == \|Z\|, "-2" means Beth 1 == \|R\|, etc.
78		* If this field is 0, the cardinality is unknown.
79		*
80		* We impose a ceiling on finite cardinalities of 2^64. If this field
81		* is >= 2^64 + 1, we consider it at "ceiling" cardinality, and
82		* comparisons between all such cardinalities result in "unknown."
83		*/
84		Integer d_card;
85
86		public:
87		/** The cardinality of the set of integers. */
88		static const Cardinality INTEGERS;
89
90		/** The cardinality of the set of real numbers. */
91		static const Cardinality REALS;
92
93		/** The unknown cardinality */
94		static const Cardinality UNKNOWN_CARD;
95
96		/** Used as a result code for Cardinality::compare(). */
97		enum CardinalityComparison
98		{
99		LESS,
100		EQUAL,
101		GREATER,
102		UNKNOWN
103		}; /* enum CardinalityComparison */
104
105		/**
106		* Construct a finite cardinality equal to the integer argument.
107		* The argument must be nonnegative. If we change this to an
108		* "unsigned" argument to enforce the restriction, we mask some
109		* errors that automatically convert, like "Cardinality(-1)".
110		*/
111		Cardinality(long card);
112
113		/**
114		* Construct a finite cardinality equal to the integer argument.
115		* The argument must be nonnegative.
116		*/
117		Cardinality(const Integer& card);
118
119		/**
120		* Construct an infinite cardinality equal to the given Beth number.
121		*/
122	19716	Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) {}
123
124		/**
125		* Construct an unknown cardinality.
126		*/
127	15460	Cardinality(CardinalityUnknown) : d_card(0) {}
128
129		/**
130		* Returns true iff this cardinality is unknown. "Unknown" in this
131		* sense means that the cardinality is completely unknown; it might
132		* be finite, or infinite---anything. Large, finite cardinalities
133		* at the "ceiling" return "false" for isUnknown() and true for
134		* isFinite() and isLargeFinite().
135		*/
136	77516	bool isUnknown() const { return d_card == 0; }
137
138		/** Returns true iff this cardinality is finite. */
139	114887	bool isFinite() const { return d_card > 0; }
140		/** Returns true iff this cardinality is one */
141	108	bool isOne() const { return d_card == 2; }
142		/**
143		* Returns true iff this cardinality is finite and large (i.e.,
144		* at the ceiling of representable finite cardinalities).
145		*/
146	104526	bool isLargeFinite() const { return d_card >= s_largeFiniteCard; }
147
148		/** Returns true iff this cardinality is infinite. */
149	45171	bool isInfinite() const { return d_card < 0; }
150
151		/**
152		* Returns true iff this cardinality is finite or countably
153		* infinite.
154		*/
155	6	bool isCountable() const { return isFinite() \|\| d_card == s_intCard; }
156
157		/**
158		* In the case that this cardinality is finite, return its
159		* cardinality. (If this cardinality is infinite, this function
160		* throws an IllegalArgumentException.)
161		*/
162		Integer getFiniteCardinality() const;
163
164		/**
165		* In the case that this cardinality is infinite, return its Beth
166		* number. (If this cardinality is finite, this function throws an
167		* IllegalArgumentException.)
168		*/
169		Integer getBethNumber() const;
170
171		/** Assigning addition of this cardinality with another. */
172		Cardinality& operator+=(const Cardinality& c);
173
174		/** Assigning multiplication of this cardinality with another. */
175		Cardinality& operator*=(const Cardinality& c);
176
177		/** Assigning exponentiation of this cardinality with another. */
178		Cardinality& operator^=(const Cardinality& c);
179
180		/** Add two cardinalities. */
181	8	Cardinality operator+(const Cardinality& c) const {
182	8	Cardinality card(*this);
183	8	card += c;
184	8	return card;
185		}
186
187		/** Multiply two cardinalities. */
188	8	Cardinality operator*(const Cardinality& c) const {
189	8	Cardinality card(*this);
190	8	card *= c;
191	8	return card;
192		}
193
194		/**
195		* Exponentiation of two cardinalities.
196		*/
197	688	Cardinality operator^(const Cardinality& c) const {
198	688	Cardinality card(*this);
199	688	card ^= c;
200	688	return card;
201		}
202
203		/**
204		* Compare two cardinalities. This can return UNKNOWN if two
205		* finite cardinalities are at the ceiling (and thus not precisely
206		* represented), or if one or the other is the special "unknown"
207		* cardinality.
208		*/
209		Cardinality::CardinalityComparison compare(const Cardinality& c) const;
210
211		/**
212		* Return a string representation of this cardinality.
213		*/
214		std::string toString() const;
215
216		/**
217		* Compare two cardinalities and if it is known that the current
218		* cardinality is smaller or equal to c, it returns true.
219		*/
220		bool knownLessThanOrEqual(const Cardinality& c) const;
221		}; /* class Cardinality */
222
223		/** Print an element of the InfiniteCardinality enumeration. */
224		std::ostream& operator<<(std::ostream& out, CardinalityBeth b);
225
226		/** Print a cardinality in a human-readable fashion. */
227		std::ostream& operator<<(std::ostream& out, const Cardinality& c);
228
229		} // namespace cvc5
230
231		#endif /* CVC5__CARDINALITY_H */