Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/cardinality.cpp	Lines:	114	144	79.2 %
Date:	2021-08-16	Branches:	223	462	48.3 %


/******************************************************************************
 * 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.
 *
 * Implementation of a simple class to represent a cardinality.
 */

#include "util/cardinality.h"

#include <ostream>
#include <sstream>

#include "base/check.h"
#include "base/exception.h"

namespace cvc5 {

const Integer Cardinality::s_unknownCard(0);
const Integer Cardinality::s_intCard(-1);
const Integer Cardinality::s_realCard(-2);
const Integer Cardinality::s_largeFiniteCard(
    Integer("18446744073709551617"));  // 2^64 + 1

const Cardinality Cardinality::INTEGERS(CardinalityBeth(0));
const Cardinality Cardinality::REALS(CardinalityBeth(1));
const Cardinality Cardinality::UNKNOWN_CARD((CardinalityUnknown()));

CardinalityBeth::CardinalityBeth(const Integer& beth) : d_index(beth) {
  PrettyCheckArgument(beth >= 0, beth,
                      "Beth index must be a nonnegative integer, not %s.",
                      beth.toString().c_str());
}

Cardinality::Cardinality(long card) : d_card(card) {
  PrettyCheckArgument(card >= 0, card,
                      "Cardinality must be a nonnegative integer, not %ld.",
                      card);
  d_card += 1;
}

Cardinality::Cardinality(const Integer& card) : d_card(card) {
  PrettyCheckArgument(card >= 0, card,
                      "Cardinality must be a nonnegative integer, not %s.",
                      card.toString().c_str());
  d_card += 1;
}

Integer Cardinality::getFiniteCardinality() const {
  PrettyCheckArgument(isFinite(), *this, "This cardinality is not finite.");
  PrettyCheckArgument(
      !isLargeFinite(), *this,
      "This cardinality is finite, but too large to represent.");
  return d_card - 1;
}

Integer Cardinality::getBethNumber() const {
  PrettyCheckArgument(!isFinite() && !isUnknown(), *this,
                      "This cardinality is not infinite (or is unknown).");
  return -d_card - 1;
}

Cardinality& Cardinality::operator+=(const Cardinality& c) {
  if (isUnknown()) {
    return *this;
  } else if (c.isUnknown()) {
    d_card = s_unknownCard;
    return *this;
  }

  if (c.isFinite() && isLargeFinite()) {
    return *this;
  } else if (isFinite() && c.isLargeFinite()) {
    d_card = s_largeFiniteCard;
    return *this;
  }

  if (isFinite() && c.isFinite()) {
    d_card += c.d_card - 1;
    return *this;
  }
  if (compare(c) == LESS) {
    return *this = c;
  } else {
    return *this;
  }

  Unreachable();
}

/** Assigning multiplication of this cardinality with another. */
Cardinality& Cardinality::operator*=(const Cardinality& c) {
  if (isUnknown()) {
    return *this;
  } else if (c.isUnknown()) {
    d_card = s_unknownCard;
    return *this;
  }

  if (c.isFinite() && isLargeFinite()) {
    return *this;
  } else if (isFinite() && c.isLargeFinite()) {
    d_card = s_largeFiniteCard;
    return *this;
  }

  if (compare(0) == EQUAL || c.compare(0) == EQUAL) {
    return *this = 0;
  } else if (!isFinite() || !c.isFinite()) {
    if (compare(c) == LESS) {
      return *this = c;
    } else {
      return *this;
    }
  } else {
    d_card -= 1;
    d_card *= c.d_card - 1;
    d_card += 1;
    return *this;
  }

  Unreachable();
}

/** Assigning exponentiation of this cardinality with another. */
Cardinality& Cardinality::operator^=(const Cardinality& c) {
  if (isUnknown()) {
    return *this;
  } else if (c.isUnknown()) {
    d_card = s_unknownCard;
    return *this;
  }

  if (c.isFinite() && isLargeFinite()) {
    return *this;
  } else if (isFinite() && c.isLargeFinite()) {
    d_card = s_largeFiniteCard;
    return *this;
  }

  if (c.compare(0) == EQUAL) {
    // (anything) ^ 0 == 1
    d_card = 2;  // remember, +1 for finite cardinalities
    return *this;
  } else if (compare(0) == EQUAL) {
    // 0 ^ (>= 1) == 0
    return *this;
  } else if (compare(1) == EQUAL) {
    // 1 ^ (>= 1) == 1
    return *this;
  } else if (c.compare(1) == EQUAL) {
    // (anything) ^ 1 == (that thing)
    return *this;
  } else if (isFinite() && c.isFinite()) {
    // finite ^ finite == finite
    try {
      // Note: can throw an assertion if c is too big for
      // exponentiation
      if (d_card - 1 >= 2 && c.d_card - 1 >= 64) {
        // don't bother, it's too large anyways
        d_card = s_largeFiniteCard;
      } else {
        d_card = (d_card - 1).pow(c.d_card.getUnsignedLong() - 1) + 1;
      }
    } catch (IllegalArgumentException&) {
      d_card = s_largeFiniteCard;
    }
    return *this;
  } else if (!isFinite() && c.isFinite()) {
    // inf ^ finite == inf
    return *this;
  } else {
    Assert(compare(2) != LESS && !c.isFinite())
        << "fall-through case not as expected:\n"
        << this << "\n"
        << c;
    // (>= 2) ^ beth_k == beth_(k+1)
    // unless the base is already > the exponent
    if (compare(c) == GREATER) {
      return *this;
    }
    d_card = c.d_card - 1;
    return *this;
  }

  Unreachable();
}

Cardinality::CardinalityComparison Cardinality::compare(
    const Cardinality& c) const {
  if (isUnknown() || c.isUnknown()) {
    return UNKNOWN;
  } else if (isLargeFinite()) {
    if (c.isLargeFinite()) {
      return UNKNOWN;
    } else if (c.isFinite()) {
      return GREATER;
    } else {
      Assert(c.isInfinite());
      return LESS;
    }
  } else if (c.isLargeFinite()) {
    if (isLargeFinite()) {
      return UNKNOWN;
    } else if (isFinite()) {
      return LESS;
    } else {
      Assert(isInfinite());
      return GREATER;
    }
  } else if (isInfinite()) {
    if (c.isFinite()) {
      return GREATER;
    } else {
      return d_card < c.d_card ? GREATER : (d_card == c.d_card ? EQUAL : LESS);
    }
  } else if (c.isInfinite()) {
    Assert(isFinite());
    return LESS;
  } else {
    Assert(isFinite() && !isLargeFinite());
    Assert(c.isFinite() && !c.isLargeFinite());
    return d_card < c.d_card ? LESS : (d_card == c.d_card ? EQUAL : GREATER);
  }

  Unreachable();
}

bool Cardinality::knownLessThanOrEqual(const Cardinality& c) const {
  CardinalityComparison cmp = this->compare(c);
  return cmp == LESS || cmp == EQUAL;
}

std::string Cardinality::toString() const {
  std::stringstream ss;
  ss << *this;
  return ss.str();
}

std::ostream& operator<<(std::ostream& out, CardinalityBeth b) {
  out << "beth[" << b.getNumber() << ']';

  return out;
}

std::ostream& operator<<(std::ostream& out, const Cardinality& c) {
  if (c.isUnknown()) {
    out << "Cardinality::UNKNOWN";
  } else if (c.isFinite()) {
    out << c.getFiniteCardinality();
  } else {
    out << CardinalityBeth(c.getBethNumber());
  }

  return out;
}

}  // namespace cvc5


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		* Implementation of a simple class to represent a cardinality.
16		*/
17
18		#include "util/cardinality.h"
19
20		#include <ostream>
21		#include <sstream>
22
23		#include "base/check.h"
24		#include "base/exception.h"
25
26		namespace cvc5 {
27
28	9780	const Integer Cardinality::s_unknownCard(0);
29	9780	const Integer Cardinality::s_intCard(-1);
30	9780	const Integer Cardinality::s_realCard(-2);
31	9780	const Integer Cardinality::s_largeFiniteCard(
32		Integer("18446744073709551617")); // 2^64 + 1
33
34	9780	const Cardinality Cardinality::INTEGERS(CardinalityBeth(0));
35	9780	const Cardinality Cardinality::REALS(CardinalityBeth(1));
36	9780	const Cardinality Cardinality::UNKNOWN_CARD((CardinalityUnknown()));
37
38	19561	CardinalityBeth::CardinalityBeth(const Integer& beth) : d_index(beth) {
39	19561	PrettyCheckArgument(beth >= 0, beth,
40		"Beth index must be a nonnegative integer, not %s.",
41		beth.toString().c_str());
42	19561	}
43
44	38852	Cardinality::Cardinality(long card) : d_card(card) {
45	38848	PrettyCheckArgument(card >= 0, card,
46		"Cardinality must be a nonnegative integer, not %ld.",
47		card);
48	38844	d_card += 1;
49	38844	}
50
51	2554	Cardinality::Cardinality(const Integer& card) : d_card(card) {
52	2552	PrettyCheckArgument(card >= 0, card,
53		"Cardinality must be a nonnegative integer, not %s.",
54		card.toString().c_str());
55	2550	d_card += 1;
56	2550	}
57
58	1213	Integer Cardinality::getFiniteCardinality() const {
59	1213	PrettyCheckArgument(isFinite(), *this, "This cardinality is not finite.");
60	1209	PrettyCheckArgument(
61		!isLargeFinite(), *this,
62		"This cardinality is finite, but too large to represent.");
63	1207	return d_card - 1;
64		}
65
66	29	Integer Cardinality::getBethNumber() const {
67	29	PrettyCheckArgument(!isFinite() && !isUnknown(), *this,
68		"This cardinality is not infinite (or is unknown).");
69	15	return -d_card - 1;
70		}
71
72	13987	Cardinality& Cardinality::operator+=(const Cardinality& c) {
73	13987	if (isUnknown()) {
74		return *this;
75	13987	} else if (c.isUnknown()) {
76		d_card = s_unknownCard;
77		return *this;
78		}
79
80	13987	if (c.isFinite() && isLargeFinite()) {
81		return *this;
82	13987	} else if (isFinite() && c.isLargeFinite()) {
83		d_card = s_largeFiniteCard;
84		return *this;
85		}
86
87	13987	if (isFinite() && c.isFinite()) {
88	13499	d_card += c.d_card - 1;
89	13499	return *this;
90		}
91	488	if (compare(c) == LESS) {
92	243	return *this = c;
93		} else {
94	245	return *this;
95		}
96
97		Unreachable();
98		}
99
100		/** Assigning multiplication of this cardinality with another. */
101	5408	Cardinality& Cardinality::operator*=(const Cardinality& c) {
102	5408	if (isUnknown()) {
103		return *this;
104	5408	} else if (c.isUnknown()) {
105		d_card = s_unknownCard;
106		return *this;
107		}
108
109	5408	if (c.isFinite() && isLargeFinite()) {
110		return *this;
111	5408	} else if (isFinite() && c.isLargeFinite()) {
112		d_card = s_largeFiniteCard;
113		return *this;
114		}
115
116	5408	if (compare(0) == EQUAL \|\| c.compare(0) == EQUAL) {
117	6	return *this = 0;
118	5402	} else if (!isFinite() \|\| !c.isFinite()) {
119	696	if (compare(c) == LESS) {
120	397	return *this = c;
121		} else {
122	299	return *this;
123		}
124		} else {
125	4706	d_card -= 1;
126	4706	d_card *= c.d_card - 1;
127	4706	d_card += 1;
128	4706	return *this;
129		}
130
131		Unreachable();
132		}
133
134		/** Assigning exponentiation of this cardinality with another. */
135	690	Cardinality& Cardinality::operator^=(const Cardinality& c) {
136	690	if (isUnknown()) {
137		return *this;
138	690	} else if (c.isUnknown()) {
139		d_card = s_unknownCard;
140		return *this;
141		}
142
143	690	if (c.isFinite() && isLargeFinite()) {
144		return *this;
145	690	} else if (isFinite() && c.isLargeFinite()) {
146		d_card = s_largeFiniteCard;
147		return *this;
148		}
149
150	690	if (c.compare(0) == EQUAL) {
151		// (anything) ^ 0 == 1
152	12	d_card = 2; // remember, +1 for finite cardinalities
153	12	return *this;
154	678	} else if (compare(0) == EQUAL) {
155		// 0 ^ (>= 1) == 0
156	8	return *this;
157	670	} else if (compare(1) == EQUAL) {
158		// 1 ^ (>= 1) == 1
159	16	return *this;
160	654	} else if (c.compare(1) == EQUAL) {
161		// (anything) ^ 1 == (that thing)
162	6	return *this;
163	648	} else if (isFinite() && c.isFinite()) {
164		// finite ^ finite == finite
165		try {
166		// Note: can throw an assertion if c is too big for
167		// exponentiation
168	296	if (d_card - 1 >= 2 && c.d_card - 1 >= 64) {
169		// don't bother, it's too large anyways
170	10	d_card = s_largeFiniteCard;
171		} else {
172	286	d_card = (d_card - 1).pow(c.d_card.getUnsignedLong() - 1) + 1;
173		}
174		} catch (IllegalArgumentException&) {
175		d_card = s_largeFiniteCard;
176		}
177	296	return *this;
178	352	} else if (!isFinite() && c.isFinite()) {
179		// inf ^ finite == inf
180	28	return *this;
181		} else {
182	324	Assert(compare(2) != LESS && !c.isFinite())
183		<< "fall-through case not as expected:\n"
184		<< this << "\n"
185		<< c;
186		// (>= 2) ^ beth_k == beth_(k+1)
187		// unless the base is already > the exponent
188	324	if (compare(c) == GREATER) {
189	16	return *this;
190		}
191	308	d_card = c.d_card - 1;
192	308	return *this;
193		}
194
195		Unreachable();
196		}
197
198	18291	Cardinality::CardinalityComparison Cardinality::compare(
199		const Cardinality& c) const {
200	18291	if (isUnknown() \|\| c.isUnknown()) {
201		return UNKNOWN;
202	18291	} else if (isLargeFinite()) {
203	112	if (c.isLargeFinite()) {
204	10	return UNKNOWN;
205	102	} else if (c.isFinite()) {
206	74	return GREATER;
207		} else {
208	28	Assert(c.isInfinite());
209	28	return LESS;
210		}
211	18179	} else if (c.isLargeFinite()) {
212	12	if (isLargeFinite()) {
213		return UNKNOWN;
214	12	} else if (isFinite()) {
215	4	return LESS;
216		} else {
217	8	Assert(isInfinite());
218	8	return GREATER;
219		}
220	18167	} else if (isInfinite()) {
221	3486	if (c.isFinite()) {
222	2725	return GREATER;
223		} else {
224	761	return d_card < c.d_card ? GREATER : (d_card == c.d_card ? EQUAL : LESS);
225		}
226	14681	} else if (c.isInfinite()) {
227	728	Assert(isFinite());
228	728	return LESS;
229		} else {
230	13953	Assert(isFinite() && !isLargeFinite());
231	13953	Assert(c.isFinite() && !c.isLargeFinite());
232	13953	return d_card < c.d_card ? LESS : (d_card == c.d_card ? EQUAL : GREATER);
233		}
234
235		Unreachable();
236		}
237
238	15	bool Cardinality::knownLessThanOrEqual(const Cardinality& c) const {
239	15	CardinalityComparison cmp = this->compare(c);
240	15	return cmp == LESS \|\| cmp == EQUAL;
241		}
242
243		std::string Cardinality::toString() const {
244		std::stringstream ss;
245		ss << *this;
246		return ss.str();
247		}
248
249	1	std::ostream& operator<<(std::ostream& out, CardinalityBeth b) {
250	1	out << "beth[" << b.getNumber() << ']';
251
252	1	return out;
253		}
254
255	1	std::ostream& operator<<(std::ostream& out, const Cardinality& c) {
256	1	if (c.isUnknown()) {
257		out << "Cardinality::UNKNOWN";
258	1	} else if (c.isFinite()) {
259		out << c.getFiniteCardinality();
260		} else {
261	1	out << CardinalityBeth(c.getBethNumber());
262		}
263
264	1	return out;
265		}
266
267	29340	} // namespace cvc5