cvc4-1.4
|
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... | |
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.