cvc4-1.4
CVC4 Namespace Reference

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 NodeTemplate< true > Node
 
typedef NodeTemplate< false > TNode
 
typedef language::input::Language InputLanguage
 
typedef language::output::Language OutputLanguage
 
typedef __gnu_cxx::hash_map< uint64_t, uint64_t > VarMap
 
typedef ::CVC4::kind::Kind_t Kind
 

Enumerations

enum  SimplificationMode { SIMPLIFICATION_MODE_INCREMENTAL, SIMPLIFICATION_MODE_BATCH, SIMPLIFICATION_MODE_NONE }
 Enumeration of simplification modes (when to simplify). More...
 
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  ArithPropagationMode { NO_PROP, UNATE_PROP, BOUND_INFERENCE_PROP, BOTH_PROP }
 
enum  ArithUnateLemmaMode { NO_PRESOLVE_LEMMAS, INEQUALITY_PRESOLVE_LEMMAS, EQUALITY_PRESOLVE_LEMMAS, ALL_PRESOLVE_LEMMAS }
 
enum  ErrorSelectionRule { VAR_ORDER, MINIMUM_AMOUNT, MAXIMUM_AMOUNT, SUM_METRIC }
 
enum  BenchmarkStatus { SMT_SATISFIABLE, SMT_UNSATISFIABLE, SMT_UNKNOWN }
 The status an SMT benchmark can have. 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, SimplificationMode mode)
 
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 &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 &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 Divisible &d)
 
std::ostream & operator<< (std::ostream &out, const SExpr &sexpr)
 
std::ostream & operator<< (std::ostream &out, const UninterpretedConstant &uc)
 
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, const EmptySet &es)
 
std::ostream & operator<< (std::ostream &out, const TupleSelect &t)
 
std::ostream & operator<< (std::ostream &out, const TupleUpdate &t)
 
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 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 &out, const Chain &ch)
 
std::ostream & operator<< (std::ostream &out, const Predicate &p)
 
std::ostream & operator<< (std::ostream &os, const Integer &n)
 
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 &os, const String &s)
 
std::ostream & operator<< (std::ostream &os, const RegExp &s)
 
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 &os, const Rational &n)
 
std::ostream & operator<< (std::ostream &out, const ArrayStoreAll &asa)
 
std::ostream & operator<< (std::ostream &out, AscriptionType at)
 An output routine for AscriptionTypes. More...
 
std::ostream & operator<< (std::ostream &out, ModelFormatMode mode)
 
std::ostream & operator<< (std::ostream &out, InstFormatMode mode)
 
std::ostream & operator<< (std::ostream &out, const LogicInfo &logic)
 
std::ostream & operator<< (std::ostream &out, ArithPropagationMode rule)
 
std::ostream & operator<< (std::ostream &out, ArithUnateLemmaMode rule)
 
std::ostream & operator<< (std::ostream &out, ErrorSelectionRule rule)
 
std::ostream & operator<< (std::ostream &out, const Type &t)
 Output operator for types. More...
 
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 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

Definition at line 165 of file language.h.

Definition at line 279 of file kind.h.

typedef NodeTemplate<true> CVC4::Node

Definition at line 46 of file smt_engine.h.

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

Enumerator
NO_PROP 
UNATE_PROP 
BOUND_INFERENCE_PROP 
BOTH_PROP 

Definition at line 27 of file arith_propagation_mode.h.

Enumerator
NO_PRESOLVE_LEMMAS 
INEQUALITY_PRESOLVE_LEMMAS 
EQUALITY_PRESOLVE_LEMMAS 
ALL_PRESOLVE_LEMMAS 

Definition at line 27 of file arith_unate_lemma_mode.h.

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.

Enumerator
VAR_ORDER 
MINIMUM_AMOUNT 
MAXIMUM_AMOUNT 
SUM_METRIC 

Definition at line 27 of file arith_heuristic_pivot_rule.h.

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.

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.

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.

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.

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-(), 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.

template<class T >
void CVC4::DebugCheckArgument ( bool  cond,
const T &  arg,
const char *  fmt,
  ... 
)
inline
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
template<>
::CVC4::ArrayStoreAll const& CVC4::Expr::getConst< ::CVC4::ArrayStoreAll > ( ) const
template<>
::CVC4::BitVector const& CVC4::Expr::getConst< ::CVC4::BitVector > ( ) const
template<>
::CVC4::BitVectorSize const& CVC4::Expr::getConst< ::CVC4::BitVectorSize > ( ) const
template<>
::CVC4::Chain const& CVC4::Expr::getConst< ::CVC4::Chain > ( ) const
template<>
::CVC4::Datatype const& CVC4::Expr::getConst< ::CVC4::Datatype > ( ) const
template<>
::CVC4::Divisible const& CVC4::Expr::getConst< ::CVC4::Divisible > ( ) const
template<>
::CVC4::EmptySet const& CVC4::Expr::getConst< ::CVC4::EmptySet > ( ) const
template<>
::CVC4::Kind const& CVC4::Expr::getConst< ::CVC4::Kind > ( ) const
template<>
::CVC4::Predicate const& CVC4::Expr::getConst< ::CVC4::Predicate > ( ) const
template<>
::CVC4::Rational const& CVC4::Expr::getConst< ::CVC4::Rational > ( ) const
template<>
::CVC4::Record const& CVC4::Expr::getConst< ::CVC4::Record > ( ) const
template<>
::CVC4::RecordSelect const& CVC4::Expr::getConst< ::CVC4::RecordSelect > ( ) const
template<>
::CVC4::RecordUpdate const& CVC4::Expr::getConst< ::CVC4::RecordUpdate > ( ) const
template<>
::CVC4::RegExp const& CVC4::Expr::getConst< ::CVC4::RegExp > ( ) const
template<>
::CVC4::String const& CVC4::Expr::getConst< ::CVC4::String > ( ) const
template<>
::CVC4::TupleSelect const& CVC4::Expr::getConst< ::CVC4::TupleSelect > ( ) const
template<>
::CVC4::TupleUpdate const& CVC4::Expr::getConst< ::CVC4::TupleUpdate > ( ) const
template<>
::CVC4::TypeConstant const& CVC4::Expr::getConst< ::CVC4::TypeConstant > ( ) const
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 (
)
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,
ArithPropagationMode  rule 
)
std::ostream& CVC4::operator<< ( std::ostream &  out,
ArithUnateLemmaMode  rule 
)
std::ostream& CVC4::operator<< ( std::ostream &  out,
ErrorSelectionRule  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 RecordUpdate t 
)
inline

Definition at line 71 of file record.h.

References CVC4::RecordUpdate::getField().

std::ostream& CVC4::operator<< ( std::ostream &  out,
const AbstractValue val 
)
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
outthe stream to output to
tthe 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.

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::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
outthe stream to output to
ethe 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::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::options::out.

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 &  out,
const SExpr sexpr 
)
std::ostream& CVC4::operator<< ( std::ostream &  os,
const String s 
)
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::BitVector::toString().

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

Definition at line 516 of file bitvector.h.

References CVC4::BitVectorExtract::high, and CVC4::BitVectorExtract::low.

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

Definition at line 521 of file bitvector.h.

References CVC4::BitVectorBitOf::bitIndex.

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

Definition at line 521 of file integer_cln_imp.h.

References CVC4::Integer::toString().

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
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 (
)
bool CVC4::operator== ( enum Result::Validity  v,
const Result r 
)
throw (
)