cardinality.h File Reference

Representation of cardinality. More...

#include "cvc4_public.h"
#include <iostream>
#include <utility>
#include "util/integer.h"
#include "util/exception.h"

Go to the source code of this file.

Data Structures
class	CVC4::CardinalityBeth
	Representation for a Beth number, used only to construct Cardinality objects. More...
class	CVC4::CardinalityUnknown
	Representation for an unknown cardinality. More...
class	CVC4::Cardinality
	A simple representation of a cardinality. More...

Namespaces
	CVC4

Functions
std::ostream &	CVC4::operator<< (std::ostream &out, CardinalityBeth b) throw ()
	Print an element of the InfiniteCardinality enumeration. More...
std::ostream &	CVC4::operator<< (std::ostream &out, const Cardinality &c) throw ()
	Print a cardinality in a human-readable fashion. More...

Detailed Description

Representation of cardinality.

** Original author: Morgan Deters
** Major contributors: none
** Minor contributors (to current version): Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014  New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.

Simple class to represent a cardinality; used by the CVC4 type system give the cardinality of sorts.

Definition in file cardinality.h.