Namespaces
	context

	expr

	kind

	language

	options

	parser

	prop

	smt

	stats

	strings

	theory

Data Structures
class	AbstractValue

struct	AbstractValueHashFunction
	Hash function for the BitVector constants. More...

class	ArrayStoreAll

struct	ArrayStoreAllHashFunction
	Hash function for the ArrayStoreAll constants. More...

class	ArrayType
	Class encapsulating an array type. More...

class	AscriptionType
	A class used to parameterize a type ascription. More...

struct	AscriptionTypeHashFunction
	A hash function for type ascription operators. More...

class	AssertCommand

class	BitVector

struct	BitVectorBitOf
	The structure representing the extraction of one Boolean bit. More...

struct	BitVectorBitOfHashFunction
	Hash function for the BitVectorBitOf objects. More...

struct	BitVectorExtract
	The structure representing the extraction operation for bit-vectors. More...

struct	BitVectorExtractHashFunction
	Hash function for the BitVectorExtract objects. More...

struct	BitVectorHashFunction
	Hash function for the BitVector constants. More...

struct	BitVectorRepeat

struct	BitVectorRotateLeft

struct	BitVectorRotateRight

struct	BitVectorSignExtend

struct	BitVectorSize

class	BitVectorType
	Class encapsulating the bit-vector type. More...

struct	BitVectorZeroExtend

class	BooleanType
	Singleton class encapsulating the Boolean type. More...

struct	BoolHashFunction

class	Cardinality
	A simple representation of a cardinality. More...

class	CardinalityBeth
	Representation for a Beth number, used only to construct Cardinality objects. More...

class	CardinalityUnknown
	Representation for an unknown cardinality. More...

class	Chain
	A class to represent a chained, built-in operator. More...

struct	ChainHashFunction

class	CheckSatCommand

class	Command

class	CommandFailure

class	CommandPrintSuccess
	IOStream manipulator to print success messages or not. More...

class	CommandSequence

class	CommandStatus

class	CommandSuccess

class	CommandUnsupported

class	CommentCommand

class	Configuration
	Represents the (static) configuration of CVC4. More...

class	ConstructorType
	Class encapsulating the constructor type. More...

class	Datatype
	The representation of an inductive datatype. More...

class	DatatypeConstructor
	A constructor for a Datatype. More...

class	DatatypeConstructorArg
	A Datatype constructor argument (i.e., a Datatype field). More...

class	DatatypeConstructorArgIterator

class	DatatypeConstructorIterator

class	DatatypeDeclarationCommand

struct	DatatypeHashFunction
	A hash function for Datatypes. More...

class	DatatypeResolutionException
	An exception that is thrown when a datatype resolution fails. More...

class	DatatypeSelfType
	A holder type (used in calls to DatatypeConstructor::addArg()) to allow a Datatype to refer to itself. More...

class	DatatypeType
	Class encapsulating the datatype type. More...

class	DatatypeUnresolvedType
	An unresolved type (used in calls to DatatypeConstructor::addArg()) to allow a Datatype to refer to itself or to other mutually-recursive Datatypes. More...

class	DeclarationDefinitionCommand

class	DeclarationSequence

class	DeclareFunctionCommand

class	DeclareTypeCommand

class	DefineFunctionCommand

class	DefineNamedFunctionCommand
	This differs from DefineFunctionCommand only in that it instructs the SmtEngine to "remember" this function for later retrieval with getAssignment(). More...

class	DefineTypeCommand

struct	Divisible
	The structure representing the divisibility-by-k predicate. More...

struct	DivisibleHashFunction
	Hash function for the Divisible objects. More...

class	EchoCommand

class	EmptyCommand
	EmptyCommands are the residue of a command after the parser handles them (and there's nothing left to do). More...

class	EmptySet

struct	EmptySetHashFunction

class	Exception

class	ExpandDefinitionsCommand

class	ExportUnsupportedException
	Exception thrown in case of failure to export. More...

class	Expr
	Class encapsulating CVC4 expressions and methods for constructing new expressions. More...

struct	ExprHashFunction

class	ExprManager

struct	ExprManagerMapCollection

class	ExprStream
	A pure-virtual stream interface for expressions. More...

class	FunctionType
	Class encapsulating a function type. More...

class	GetAssertionsCommand

class	GetAssignmentCommand

class	GetInfoCommand

class	GetInstantiationsCommand

class	GetModelCommand

class	GetOptionCommand

class	GetProofCommand

class	GetUnsatCoreCommand

class	GetValueCommand

class	IllegalArgumentException

class	Integer

struct	IntegerHashFunction

class	IntegerType
	Singleton class encapsulating the integer type. More...

struct	IntToBitVector

class	LemmaInputChannel

class	LemmaOutputChannel
	This interface describes a mechanism for the propositional and theory engines to communicate with the "outside world" about new lemmas being discovered. More...

class	LogicException

class	LogicInfo
	A LogicInfo instance describes a collection of theory modules and some basic configuration about them. More...

class	ModalException

class	NodeTemplate

class	OptionException
	Class representing an option-parsing exception such as badly-typed or missing arguments, arguments out of bounds, etc. More...

class	Options

struct	PairHashFunction

class	PopCommand

class	Predicate

struct	PredicateHashFunction

class	Proof

class	PropagateRuleCommand

class	PushCommand

class	QueryCommand

class	QuitCommand

class	Rational
	A multi-precision rational constant. More...

class	RationalFromDoubleException

struct	RationalHashFunction

class	RealType
	Singleton class encapsulating the real type. More...

class	Record

struct	RecordHashFunction

class	RecordSelect

struct	RecordSelectHashFunction

class	RecordType
	Class encapsulating a record type. More...

class	RecordUpdate

struct	RecordUpdateHashFunction

class	RegExp

struct	RegExpHashFunction
	Hash function for the RegExp constants. More...

class	Result
	Three-valued SMT result, with optional explanation. More...

class	RewriteRuleCommand

class	ScopeException

class	SelectorType
	Class encapsulating the Selector type. More...

class	SetBenchmarkLogicCommand

class	SetBenchmarkStatusCommand

class	SetInfoCommand

class	SetOptionCommand

class	SetType
	Class encapsulating an set type. More...

class	SetUserAttributeCommand
	The command when an attribute is set by a user. More...

class	SExpr
	A simple S-expression. More...

class	SExprKeyword

class	SExprType
	Class encapsulating a tuple type. More...

class	SharedChannel

class	SimplifyCommand

class	SmtEngine

class	SortConstructorType
	Class encapsulating a user-defined sort constructor. More...

class	SortType
	Class encapsulating a user-defined sort. More...

class	Statistics

class	StatisticsBase

class	String

struct	StringHashFunction

class	StringType
	Singleton class encapsulating the string type. More...

class	SubrangeBound
	Representation of a subrange bound. More...

class	SubrangeBounds

struct	SubrangeBoundsHashFunction

class	SubrangeType
	Class encapsulating an integer subrange type. More...

class	SymbolTable
	A convenience class for handling scoped declarations. More...

class	SynchronizedSharedChannel

class	TesterType
	Class encapsulating the Tester type. More...

class	TupleSelect

struct	TupleSelectHashFunction

class	TupleType
	Class encapsulating a tuple type. More...

class	TupleUpdate

struct	TupleUpdateHashFunction

class	Type
	Class encapsulating CVC4 expression types. More...

class	TypeCheckingException
	Exception thrown in the case of type-checking errors. More...

struct	TypeConstantHashFunction
	We hash the constants with their values. More...

struct	TypeHashFunction
	Hash function for Types. More...

class	UninterpretedConstant

struct	UninterpretedConstantHashFunction
	Hash function for the BitVector constants. More...

class	UnrecognizedOptionException
	Class representing an exception in option processing due to an unrecognized or unsupported option key. More...

struct	UnsignedHashFunction

class	VariableTypeMap

Typedefs
typedef language::input::Language	InputLanguage

typedef language::output::Language	OutputLanguage

typedef __gnu_cxx::hash_map< uint64_t, uint64_t >	VarMap

typedef NodeTemplate< true >	Node

typedef NodeTemplate< false >	TNode

typedef ::CVC4::kind::Kind_t	Kind

Enumerations
enum	ArithPropagationMode { NO_PROP, UNATE_PROP, BOUND_INFERENCE_PROP, BOTH_PROP }

enum	ErrorSelectionRule { VAR_ORDER, MINIMUM_AMOUNT, MAXIMUM_AMOUNT, SUM_METRIC }

enum	ArithUnateLemmaMode { NO_PRESOLVE_LEMMAS, INEQUALITY_PRESOLVE_LEMMAS, EQUALITY_PRESOLVE_LEMMAS, ALL_PRESOLVE_LEMMAS }

enum	ModelFormatMode { MODEL_FORMAT_MODE_DEFAULT, MODEL_FORMAT_MODE_TABLE }
	Enumeration of model_format modes (how to print models from get-model command). More...

enum	InstFormatMode { INST_FORMAT_MODE_DEFAULT, INST_FORMAT_MODE_SZS }
	Enumeration of inst_format modes (how to print models from get-model command). More...

enum	BenchmarkStatus { SMT_SATISFIABLE, SMT_UNSATISFIABLE, SMT_UNKNOWN }
	The status an SMT benchmark can have. More...

enum	SimplificationMode { SIMPLIFICATION_MODE_INCREMENTAL, SIMPLIFICATION_MODE_BATCH, SIMPLIFICATION_MODE_NONE }
	Enumeration of simplification modes (when to simplify). More...

enum	TypeConstant { BUILTIN_OPERATOR_TYPE, BOOLEAN_TYPE, REAL_TYPE, INTEGER_TYPE, STRING_TYPE, REGEXP_TYPE, BOUND_VAR_LIST_TYPE, INST_PATTERN_TYPE, INST_PATTERN_LIST_TYPE, RRHB_TYPE, LAST_TYPE }
	The enumeration for the built-in atomic types. More...

Functions
std::ostream &	operator<< (std::ostream &out, ArithPropagationMode rule)

std::ostream &	operator<< (std::ostream &out, ErrorSelectionRule rule)

std::ostream &	operator<< (std::ostream &out, ArithUnateLemmaMode rule)

std::ostream &	operator<< (std::ostream &out, const LogicInfo &logic)

std::ostream &	operator<< (std::ostream &os, const Datatype &dt)

std::ostream &	operator<< (std::ostream &os, const DatatypeConstructor &ctor)

std::ostream &	operator<< (std::ostream &os, const DatatypeConstructorArg &arg)

std::ostream &	operator<< (std::ostream &os, const Integer &n)

std::ostream &	operator<< (std::ostream &out, const Predicate &p)

std::ostream &	operator<< (std::ostream &os, const String &s)

std::ostream &	operator<< (std::ostream &os, const RegExp &s)

std::ostream &	operator<< (std::ostream &os, const Rational &n)

std::ostream &	operator<< (std::ostream &out, const UninterpretedConstant &uc)

size_t	gmpz_hash (const mpz_t toHash)
	Hashes the gmp integer primitive in a word by word fashion. More...

std::ostream &	operator<< (std::ostream &out, const EmptySet &es)

std::ostream &	operator<< (std::ostream &out, const AbstractValue &val)

std::ostream &	operator<< (std::ostream &out, const Result &r)

std::ostream &	operator<< (std::ostream &out, enum Result::Sat s)

std::ostream &	operator<< (std::ostream &out, enum Result::Validity v)

std::ostream &	operator<< (std::ostream &out, enum Result::UnknownExplanation e)

bool	operator== (enum Result::Sat s, const Result &r) throw ()

bool	operator== (enum Result::Validity v, const Result &r) throw ()

bool	operator!= (enum Result::Sat s, const Result &r) throw ()

bool	operator!= (enum Result::Validity v, const Result &r) throw ()

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

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

std::ostream &	operator<< (std::ostream &out, AscriptionType at)
	An output routine for AscriptionTypes. More...

std::ostream &	operator<< (std::ostream &out, const SExpr &sexpr)

std::ostream &	operator<< (std::ostream &os, const BitVector &bv)

std::ostream &	operator<< (std::ostream &os, const BitVectorExtract &bv)

std::ostream &	operator<< (std::ostream &os, const BitVectorBitOf &bv)

std::ostream &	operator<< (std::ostream &os, const IntToBitVector &bv)

std::ostream &	operator<< (std::ostream &out, const Chain &ch)

std::ostream &	operator<< (std::ostream &out, const SubrangeBound &bound) throw ()

std::ostream &	operator<< (std::ostream &out, const SubrangeBounds &bounds) throw ()

std::ostream &	operator<< (std::ostream &out, const TupleSelect &t)

std::ostream &	operator<< (std::ostream &out, const TupleUpdate &t)

std::ostream &	operator<< (std::ostream &os, const Divisible &d)

std::ostream &	operator<< (std::ostream &out, const ArrayStoreAll &asa)

std::ostream &	operator<< (std::ostream &out, const RecordSelect &t)

std::ostream &	operator<< (std::ostream &out, const RecordUpdate &t)

std::ostream &	operator<< (std::ostream &os, const Record &r)

std::ostream &	operator<< (std::ostream &os, const Exception &e) throw ()

template<class T >
void	CheckArgument (bool cond, const T &arg, const char *fmt,...)

template<class T >
void	CheckArgument (bool cond, const T &arg)

template<class T >
void	DebugCheckArgument (bool cond, const T &arg, const char *fmt,...)

template<class T >
void	DebugCheckArgument (bool cond, const T &arg)

std::ostream &	operator<< (std::ostream &out, ModelFormatMode mode)

std::ostream &	operator<< (std::ostream &out, InstFormatMode mode)

std::ostream &	operator<< (std::ostream &, const Command &) throw ()

std::ostream &	operator<< (std::ostream &, const Command *) throw ()

std::ostream &	operator<< (std::ostream &, const CommandStatus &) throw ()

std::ostream &	operator<< (std::ostream &, const CommandStatus *) throw ()

std::ostream &	operator<< (std::ostream &out, BenchmarkStatus status) throw ()

std::ostream &	operator<< (std::ostream &out, CommandPrintSuccess cps) throw ()
	Sets the default print-success setting when pretty-printing an Expr to an ostream. More...

std::ostream &	operator<< (std::ostream &out, const Type &t)
	Output operator for types. More...

std::ostream &	operator<< (std::ostream &out, SimplificationMode mode)

std::ostream &	operator<< (std::ostream &out, const TypeCheckingException &e)

std::ostream &	operator<< (std::ostream &out, const Expr &e)
	Output operator for expressions. More...

template<>
::CVC4::UninterpretedConstant const &	Expr::getConst< ::CVC4::UninterpretedConstant > () const

template<>
::CVC4::AbstractValue const &	Expr::getConst< ::CVC4::AbstractValue > () const

template<>
::CVC4::Kind const &	Expr::getConst< ::CVC4::Kind > () const

template<>
::CVC4::Chain const &	Expr::getConst< ::CVC4::Chain > () const

template<>
::CVC4::TypeConstant const &	Expr::getConst< ::CVC4::TypeConstant > () const

template<>
::CVC4::Predicate const &	Expr::getConst< ::CVC4::Predicate > () const

template<>
::CVC4::Divisible const &	Expr::getConst< ::CVC4::Divisible > () const

template<>
::CVC4::SubrangeBounds const &	Expr::getConst< ::CVC4::SubrangeBounds > () const

template<>
::CVC4::Rational const &	Expr::getConst< ::CVC4::Rational > () const

template<>
::CVC4::BitVectorSize const &	Expr::getConst< ::CVC4::BitVectorSize > () const

template<>
::CVC4::BitVector const &	Expr::getConst< ::CVC4::BitVector > () const

template<>
::CVC4::BitVectorBitOf const &	Expr::getConst< ::CVC4::BitVectorBitOf > () const

template<>
::CVC4::BitVectorExtract const &	Expr::getConst< ::CVC4::BitVectorExtract > () const

template<>
::CVC4::BitVectorRepeat const &	Expr::getConst< ::CVC4::BitVectorRepeat > () const

template<>
::CVC4::BitVectorZeroExtend const &	Expr::getConst< ::CVC4::BitVectorZeroExtend > () const

template<>
::CVC4::BitVectorSignExtend const &	Expr::getConst< ::CVC4::BitVectorSignExtend > () const

template<>
::CVC4::BitVectorRotateLeft const &	Expr::getConst< ::CVC4::BitVectorRotateLeft > () const

template<>
::CVC4::BitVectorRotateRight const &	Expr::getConst< ::CVC4::BitVectorRotateRight > () const

template<>
::CVC4::IntToBitVector const &	Expr::getConst< ::CVC4::IntToBitVector > () const

template<>
::CVC4::ArrayStoreAll const &	Expr::getConst< ::CVC4::ArrayStoreAll > () const

template<>
::CVC4::Datatype const &	Expr::getConst< ::CVC4::Datatype > () const

template<>
::CVC4::AscriptionType const &	Expr::getConst< ::CVC4::AscriptionType > () const

template<>
::CVC4::TupleSelect const &	Expr::getConst< ::CVC4::TupleSelect > () const

template<>
::CVC4::TupleUpdate const &	Expr::getConst< ::CVC4::TupleUpdate > () const

template<>
::CVC4::Record const &	Expr::getConst< ::CVC4::Record > () const

template<>
::CVC4::RecordSelect const &	Expr::getConst< ::CVC4::RecordSelect > () const

template<>
::CVC4::RecordUpdate const &	Expr::getConst< ::CVC4::RecordUpdate > () const

template<>
::CVC4::EmptySet const &	Expr::getConst< ::CVC4::EmptySet > () const

template<>
::CVC4::String const &	Expr::getConst< ::CVC4::String > () const

template<>
::CVC4::RegExp const &	Expr::getConst< ::CVC4::RegExp > () const

std::ostream &	operator<< (std::ostream &out, TypeConstant typeConstant)

Typedef Documentation

typedef language::input::Language CVC4::InputLanguage

Definition at line 165 of file language.h.

typedef ::CVC4::kind::Kind_t CVC4::Kind

Definition at line 279 of file kind.h.

typedef NodeTemplate<true> CVC4::Node

Definition at line 46 of file smt_engine.h.

typedef language::output::Language CVC4::OutputLanguage

Definition at line 166 of file language.h.

typedef NodeTemplate<false> CVC4::TNode

Definition at line 48 of file smt_engine.h.

typedef __gnu_cxx::hash_map<uint64_t, uint64_t> CVC4::VarMap

Definition at line 52 of file variable_type_map.h.

Enumeration Type Documentation

enum CVC4::ArithPropagationMode

Enumerator
NO_PROP
UNATE_PROP
BOUND_INFERENCE_PROP
BOTH_PROP

Definition at line 27 of file arith_propagation_mode.h.

enum CVC4::ArithUnateLemmaMode

Enumerator
NO_PRESOLVE_LEMMAS
INEQUALITY_PRESOLVE_LEMMAS
EQUALITY_PRESOLVE_LEMMAS
ALL_PRESOLVE_LEMMAS

Definition at line 27 of file arith_unate_lemma_mode.h.

enum CVC4::BenchmarkStatus

The status an SMT benchmark can have.

Enumerator
SMT_SATISFIABLE	Benchmark is satisfiable.
SMT_UNSATISFIABLE	Benchmark is unsatisfiable.
SMT_UNKNOWN	The status of the benchmark is unknown.

Definition at line 52 of file command.h.

enum CVC4::ErrorSelectionRule

Enumerator
VAR_ORDER
MINIMUM_AMOUNT
MAXIMUM_AMOUNT
SUM_METRIC

Definition at line 27 of file arith_heuristic_pivot_rule.h.

enum CVC4::InstFormatMode

Enumeration of inst_format modes (how to print models from get-model command).

Enumerator
INST_FORMAT_MODE_DEFAULT	default mode (print expressions in the output language format)
INST_FORMAT_MODE_SZS	print as SZS proof

Definition at line 36 of file modes.h.

enum CVC4::ModelFormatMode

Enumeration of model_format modes (how to print models from get-model command).

Enumerator
MODEL_FORMAT_MODE_DEFAULT	default mode (print expressions in the output language format)
MODEL_FORMAT_MODE_TABLE	print functional values in a table format

Definition at line 28 of file modes.h.

enum CVC4::SimplificationMode

Enumeration of simplification modes (when to simplify).

Enumerator
SIMPLIFICATION_MODE_INCREMENTAL	Simplify the assertions as they come in.
SIMPLIFICATION_MODE_BATCH	Simplify the assertions all together once a check is requested.
SIMPLIFICATION_MODE_NONE	Don't do simplification.

Definition at line 28 of file simplification_mode.h.

enum CVC4::TypeConstant

The enumeration for the built-in atomic types.

Enumerator
BUILTIN_OPERATOR_TYPE	the type for built-in operators
BOOLEAN_TYPE	Boolean type.
REAL_TYPE	real type
INTEGER_TYPE	integer type
STRING_TYPE	String type.
REGEXP_TYPE	RegExp type.
BOUND_VAR_LIST_TYPE	the type of bound variable lists
INST_PATTERN_TYPE	instantiation pattern type
INST_PATTERN_LIST_TYPE	the type of instantiation pattern lists
RRHB_TYPE	head and body of the rule type (for rewrite-rules theory)
LAST_TYPE

Definition at line 543 of file kind.h.

Function Documentation

template<class T >

void CVC4::CheckArgument	(	bool	cond,
		const T &	arg,
		const char *	fmt,
			...
	)

inline

Definition at line 140 of file exception.h.

References CVC4_PUBLIC.

Referenced by CVC4::AbstractValue::AbstractValue(), CVC4::LogicInfo::areIntegersUsed(), CVC4::LogicInfo::areRealsUsed(), CVC4::BitVector::arithRightShift(), CVC4::ArrayStoreAll::ArrayStoreAll(), CVC4::BitVector::BitVector(), CVC4::Cardinality::Cardinality(), CVC4::CardinalityBeth::CardinalityBeth(), CVC4::Cardinality::getBethNumber(), CVC4::SubrangeBound::getBound(), CVC4::SExpr::getChildren(), CVC4::Cardinality::getFiniteCardinality(), CVC4::Record::getIndex(), CVC4::SExpr::getIntegerValue(), CVC4::Integer::getLong(), CVC4::Datatype::getParameter(), CVC4::Datatype::getParameters(), CVC4::SExpr::getRationalValue(), CVC4::Integer::getUnsignedLong(), CVC4::SExpr::getValue(), CVC4::LogicInfo::hasCardinalityConstraints(), CVC4::LogicInfo::hasEverything(), CVC4::LogicInfo::hasNothing(), CVC4::BitVector::isBitSet(), CVC4::LogicInfo::isDifferenceLogic(), CVC4::LogicInfo::isLinear(), CVC4::LogicInfo::isPure(), CVC4::LogicInfo::isQuantified(), CVC4::LogicInfo::isSharingEnabled(), CVC4::LogicInfo::isTheoryEnabled(), CVC4::BitVector::leftShift(), CVC4::BitVector::logicalRightShift(), CVC4::BitVector::operator&(), CVC4::BitVector::operator*(), CVC4::BitVector::operator+(), CVC4::BitVector::operator-(), operator<<(), CVC4::LogicInfo::operator<=(), CVC4::LogicInfo::operator==(), CVC4::LogicInfo::operator>=(), CVC4::Record::operator[](), CVC4::BitVector::operator^(), CVC4::BitVector::operator|(), CVC4::Result::Result(), CVC4::BitVector::setBit(), CVC4::BitVector::signedLessThan(), CVC4::BitVector::signedLessThanEq(), CVC4::SubrangeBounds::SubrangeBounds(), CVC4::UninterpretedConstant::UninterpretedConstant(), CVC4::BitVector::unsignedDivTotal(), CVC4::BitVector::unsignedLessThan(), CVC4::BitVector::unsignedLessThanEq(), CVC4::BitVector::unsignedRemTotal(), and CVC4::Result::whyUnknown().

template<class T >

void CVC4::CheckArgument	(	bool	cond,
		const T &	arg
	)

inline

Definition at line 146 of file exception.h.

References CVC4_PUBLIC, and DebugCheckArgument().

template<class T >

void CVC4::DebugCheckArgument	(	bool	cond,
		const T &	arg,
		const char *	fmt,
			...
	)

inline

Definition at line 155 of file exception.h.

References CVC4_PUBLIC.

Referenced by CheckArgument(), CVC4::Integer::exactQuotient(), CVC4::SubrangeBounds::join(), and CVC4::Integer::oneExtend().

template<class T >

void CVC4::DebugCheckArgument	(	bool	cond,
		const T &	arg
	)

inline

Definition at line 161 of file exception.h.

template<>

::CVC4::AbstractValue const& CVC4::Expr::getConst< ::CVC4::AbstractValue > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::ArrayStoreAll const& CVC4::Expr::getConst< ::CVC4::ArrayStoreAll > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::AscriptionType const& CVC4::Expr::getConst< ::CVC4::AscriptionType > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::BitVector const& CVC4::Expr::getConst< ::CVC4::BitVector > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::BitVectorBitOf const& CVC4::Expr::getConst< ::CVC4::BitVectorBitOf > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::BitVectorExtract const& CVC4::Expr::getConst< ::CVC4::BitVectorExtract > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::BitVectorRepeat const& CVC4::Expr::getConst< ::CVC4::BitVectorRepeat > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::BitVectorRotateLeft const& CVC4::Expr::getConst< ::CVC4::BitVectorRotateLeft > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::BitVectorRotateRight const& CVC4::Expr::getConst< ::CVC4::BitVectorRotateRight > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::BitVectorSignExtend const& CVC4::Expr::getConst< ::CVC4::BitVectorSignExtend > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::BitVectorSize const& CVC4::Expr::getConst< ::CVC4::BitVectorSize > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::BitVectorZeroExtend const& CVC4::Expr::getConst< ::CVC4::BitVectorZeroExtend > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::Chain const& CVC4::Expr::getConst< ::CVC4::Chain > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::Datatype const& CVC4::Expr::getConst< ::CVC4::Datatype > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::Divisible const& CVC4::Expr::getConst< ::CVC4::Divisible > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::EmptySet const& CVC4::Expr::getConst< ::CVC4::EmptySet > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::IntToBitVector const& CVC4::Expr::getConst< ::CVC4::IntToBitVector > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::Kind const& CVC4::Expr::getConst< ::CVC4::Kind > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::Predicate const& CVC4::Expr::getConst< ::CVC4::Predicate > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::Rational const& CVC4::Expr::getConst< ::CVC4::Rational > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::Record const& CVC4::Expr::getConst< ::CVC4::Record > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::RecordSelect const& CVC4::Expr::getConst< ::CVC4::RecordSelect > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::RecordUpdate const& CVC4::Expr::getConst< ::CVC4::RecordUpdate > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::RegExp const& CVC4::Expr::getConst< ::CVC4::RegExp > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::String const& CVC4::Expr::getConst< ::CVC4::String > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::SubrangeBounds const& CVC4::Expr::getConst< ::CVC4::SubrangeBounds > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::TupleSelect const& CVC4::Expr::getConst< ::CVC4::TupleSelect > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::TupleUpdate const& CVC4::Expr::getConst< ::CVC4::TupleUpdate > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::TypeConstant const& CVC4::Expr::getConst< ::CVC4::TypeConstant > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

template<>

::CVC4::UninterpretedConstant const& CVC4::Expr::getConst< ::CVC4::UninterpretedConstant > ( ) const

Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().

size_t CVC4::gmpz_hash ( const mpz_t toHash )

inline

Hashes the gmp integer primitive in a word by word fashion.

Definition at line 28 of file gmp_util.h.

Referenced by CVC4::Rational::hash(), and CVC4::Integer::hash().

bool CVC4::operator!=	(	enum Result::Sat	s,
		const Result &	r
	)
throw	(
	)

Referenced by CVC4::Type::getTypeNode(), CVC4::Result::operator!=(), CVC4::SExpr::SExpr(), and CVC4::Result::whyUnknown().

bool CVC4::operator!=	(	enum Result::Validity	v,
		const Result &	r
	)
throw	(
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		const Predicate &	p
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		const Result &	r
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		ErrorSelectionRule	rule
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		ArithPropagationMode	rule
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		ArithUnateLemmaMode	rule
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		SimplificationMode	mode
	)

std::ostream & CVC4::operator<<	(	std::ostream &	out,
		const Chain &	ch
	)

inline

Definition at line 39 of file chain.h.

References CVC4::Chain::getOperator().

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		ModelFormatMode	mode
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		InstFormatMode	mode
	)

std::ostream& CVC4::operator<<	(	std::ostream &	,
		const Command &
	)
throw	(
	)

std::ostream& CVC4::operator<<	(	std::ostream &	,
		const Command *
	)
throw	(
	)

std::ostream& CVC4::operator<<	(	std::ostream &	,
		const CommandStatus &
	)
throw	(
	)

std::ostream& CVC4::operator<<	(	std::ostream &	,
		const CommandStatus *
	)
throw	(
	)

std::ostream & CVC4::operator<<	(	std::ostream &	os,
		const Divisible &	d
	)

inline

Definition at line 56 of file divisible.h.

References CVC4::Divisible::k.

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		AscriptionType	at
	)

inline

An output routine for AscriptionTypes.

Definition at line 56 of file ascription_type.h.

References CVC4::AscriptionType::getType(), and CVC4::options::out.

std::ostream & CVC4::operator<<	(	std::ostream &	out,
		const TupleSelect &	t
	)

inline

Definition at line 62 of file tuple.h.

References CVC4::TupleSelect::getIndex().

std::ostream & CVC4::operator<<	(	std::ostream &	out,
		const TupleUpdate &	t
	)

inline

Definition at line 66 of file tuple.h.

References CVC4::TupleUpdate::getIndex().

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		BenchmarkStatus	status
	)
throw	(
	)

std::ostream & CVC4::operator<<	(	std::ostream &	out,
		const RecordSelect &	t
	)

inline

Definition at line 67 of file record.h.

References CVC4::RecordSelect::getField().

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		const AbstractValue &	val
	)

std::ostream & CVC4::operator<<	(	std::ostream &	out,
		const RecordUpdate &	t
	)

inline

Definition at line 71 of file record.h.

References CVC4::RecordUpdate::getField().

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		const UninterpretedConstant &	uc
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		const EmptySet &	es
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		const Type &	t
	)

Output operator for types.

Parameters

out	the stream to output to
t	the type to output

Returns: the stream

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		const ArrayStoreAll &	asa
	)

std::ostream & CVC4::operator<<	(	std::ostream &	os,
		const Exception &	e
	)
throw	(
	)

inline

Definition at line 125 of file exception.h.

References CheckArgument(), CVC4_PUBLIC, and CVC4::Exception::toStream().

std::ostream & CVC4::operator<<	(	std::ostream &	out,
		CommandPrintSuccess	cps
	)
throw	(
	)

inline

Sets the default print-success setting when pretty-printing an Expr to an ostream.

Use like this:

// let out be an ostream, e an Expr out << Expr::setdepth(n) << e << endl;

The depth stays permanently (until set again) with the stream.

Definition at line 147 of file command.h.

References CVC4::CommandPrintSuccess::applyPrintSuccess(), and CVC4::options::out.

std::ostream& CVC4::operator<<	(	std::ostream &	os,
		const Record &	r
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		enum Result::Sat	s
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		enum Result::Validity	v
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		enum Result::UnknownExplanation	e
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		const TypeCheckingException &	e
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		const Expr &	e
	)

Output operator for expressions.

Parameters

out	the stream to output to
e	the expression to output

Returns: the stream

std::ostream & CVC4::operator<<	(	std::ostream &	out,
		const SubrangeBound &	bound
	)
throw	(
	)

inline

Definition at line 245 of file subrange_bound.h.

References CVC4_PUBLIC, CVC4::SubrangeBound::getBound(), CVC4::SubrangeBound::hasBound(), operator<<(), and CVC4::options::out.

std::ostream & CVC4::operator<<	(	std::ostream &	out,
		const SubrangeBounds &	bounds
	)
throw	(
	)

inline

Definition at line 259 of file subrange_bound.h.

References CVC4::SubrangeBounds::lower, CVC4::options::out, and CVC4::SubrangeBounds::upper.

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		CardinalityBeth	b
	)
throw	(
	)

Print an element of the InfiniteCardinality enumeration.

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		const Cardinality &	c
	)
throw	(
	)

Print a cardinality in a human-readable fashion.

std::ostream& CVC4::operator<<	(	std::ostream &	os,
		const String &	s
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		const SExpr &	sexpr
	)

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		const LogicInfo &	logic
	)

std::ostream& CVC4::operator<<	(	std::ostream &	os,
		const RegExp &	s
	)

std::ostream & CVC4::operator<<	(	std::ostream &	os,
		const Rational &	n
	)

std::ostream & CVC4::operator<<	(	std::ostream &	os,
		const BitVector &	bv
	)

inline

Definition at line 511 of file bitvector.h.

References CVC4_PUBLIC, operator<<(), and CVC4::BitVector::toString().

std::ostream & CVC4::operator<<	(	std::ostream &	os,
		const Integer &	n
	)

inline

Definition at line 514 of file integer_gmp_imp.h.

References CVC4::Integer::toString().

std::ostream & CVC4::operator<<	(	std::ostream &	os,
		const BitVectorExtract &	bv
	)

inline

Definition at line 516 of file bitvector.h.

References CVC4_PUBLIC, CVC4::BitVectorExtract::high, CVC4::BitVectorExtract::low, and operator<<().

std::ostream & CVC4::operator<<	(	std::ostream &	os,
		const BitVectorBitOf &	bv
	)

inline

Definition at line 521 of file bitvector.h.

References CVC4::BitVectorBitOf::bitIndex, CVC4_PUBLIC, and operator<<().

std::ostream & CVC4::operator<<	(	std::ostream &	os,
		const IntToBitVector &	bv
	)

inline

Definition at line 526 of file bitvector.h.

References CVC4::IntToBitVector::size.

std::ostream& CVC4::operator<<	(	std::ostream &	out,
		TypeConstant	typeConstant
	)

inline

Definition at line 568 of file kind.h.

References BOOLEAN_TYPE, BOUND_VAR_LIST_TYPE, BUILTIN_OPERATOR_TYPE, INST_PATTERN_LIST_TYPE, INST_PATTERN_TYPE, INTEGER_TYPE, CVC4::options::out, REAL_TYPE, REGEXP_TYPE, RRHB_TYPE, and STRING_TYPE.

std::ostream& CVC4::operator<<	(	std::ostream &	os,
		const Datatype &	dt
	)

std::ostream& CVC4::operator<<	(	std::ostream &	os,
		const DatatypeConstructor &	ctor
	)

std::ostream& CVC4::operator<<	(	std::ostream &	os,
		const DatatypeConstructorArg &	arg
	)

bool CVC4::operator==	(	enum Result::Sat	s,
		const Result &	r
	)
throw	(
	)

Referenced by CVC4::Type::getTypeNode(), CVC4::Result::operator!=(), CVC4::SExpr::SExpr(), and CVC4::Result::whyUnknown().

bool CVC4::operator==	(	enum Result::Validity	v,
		const Result &	r
	)
throw	(
	)

Namespaces

Data Structures

Typedefs

Enumerations

Functions

Typedef Documentation

Enumeration Type Documentation

Function Documentation