cvc4-1.4
|
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 |
Functions | |
std::ostream & | operator<< (std::ostream &out, const UninterpretedConstant &uc) |
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 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 &os, const Rational &n) |
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, AscriptionType at) |
An output routine for AscriptionTypes. More... | |
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 String &s) |
std::ostream & | operator<< (std::ostream &os, const RegExp &s) |
std::ostream & | operator<< (std::ostream &out, const ArrayStoreAll &asa) |
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 EmptySet &es) |
std::ostream & | operator<< (std::ostream &os, const Integer &n) |
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 AbstractValue &val) |
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 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 &out, const Predicate &p) |
std::ostream & | operator<< (std::ostream &out, const SExpr &sexpr) |
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 &os, const Divisible &d) |
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, 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 LogicInfo &logic) |
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) |
Definition at line 165 of file language.h.
typedef ::CVC4::kind::Kind_t CVC4::Kind |
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.
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.
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 simplification modes (when to simplify).
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 |
|
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().
|
inline |
Definition at line 146 of file exception.h.
References CVC4_PUBLIC, and DebugCheckArgument().
|
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().
|
inline |
Definition at line 161 of file exception.h.
::CVC4::AbstractValue const& CVC4::Expr::getConst< ::CVC4::AbstractValue > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::ArrayStoreAll const& CVC4::Expr::getConst< ::CVC4::ArrayStoreAll > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::AscriptionType const& CVC4::Expr::getConst< ::CVC4::AscriptionType > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::BitVector const& CVC4::Expr::getConst< ::CVC4::BitVector > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::BitVectorBitOf const& CVC4::Expr::getConst< ::CVC4::BitVectorBitOf > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::BitVectorExtract const& CVC4::Expr::getConst< ::CVC4::BitVectorExtract > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::BitVectorRepeat const& CVC4::Expr::getConst< ::CVC4::BitVectorRepeat > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::BitVectorRotateLeft const& CVC4::Expr::getConst< ::CVC4::BitVectorRotateLeft > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::BitVectorRotateRight const& CVC4::Expr::getConst< ::CVC4::BitVectorRotateRight > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::BitVectorSignExtend const& CVC4::Expr::getConst< ::CVC4::BitVectorSignExtend > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::BitVectorSize const& CVC4::Expr::getConst< ::CVC4::BitVectorSize > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::BitVectorZeroExtend const& CVC4::Expr::getConst< ::CVC4::BitVectorZeroExtend > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::Chain const& CVC4::Expr::getConst< ::CVC4::Chain > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::Datatype const& CVC4::Expr::getConst< ::CVC4::Datatype > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::Divisible const& CVC4::Expr::getConst< ::CVC4::Divisible > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::EmptySet const& CVC4::Expr::getConst< ::CVC4::EmptySet > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::IntToBitVector const& CVC4::Expr::getConst< ::CVC4::IntToBitVector > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::Kind const& CVC4::Expr::getConst< ::CVC4::Kind > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::Predicate const& CVC4::Expr::getConst< ::CVC4::Predicate > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::Rational const& CVC4::Expr::getConst< ::CVC4::Rational > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::Record const& CVC4::Expr::getConst< ::CVC4::Record > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::RecordSelect const& CVC4::Expr::getConst< ::CVC4::RecordSelect > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::RecordUpdate const& CVC4::Expr::getConst< ::CVC4::RecordUpdate > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::RegExp const& CVC4::Expr::getConst< ::CVC4::RegExp > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::String const& CVC4::Expr::getConst< ::CVC4::String > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::SubrangeBounds const& CVC4::Expr::getConst< ::CVC4::SubrangeBounds > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::TupleSelect const& CVC4::Expr::getConst< ::CVC4::TupleSelect > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::TupleUpdate const& CVC4::Expr::getConst< ::CVC4::TupleUpdate > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::TypeConstant const& CVC4::Expr::getConst< ::CVC4::TypeConstant > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
::CVC4::UninterpretedConstant const& CVC4::Expr::getConst< ::CVC4::UninterpretedConstant > | ( | ) | const |
Referenced by CVC4::expr::ExprSetLanguage::Scope::~Scope().
|
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, |
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 | ||
) |
|
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 | ( | ||
) |
|
inline |
Definition at line 56 of file divisible.h.
References CVC4::Divisible::k.
|
inline |
An output routine for AscriptionTypes.
Definition at line 56 of file ascription_type.h.
References CVC4::AscriptionType::getType(), and CVC4::options::out.
|
inline |
Definition at line 62 of file tuple.h.
References CVC4::TupleSelect::getIndex().
|
inline |
Definition at line 66 of file tuple.h.
References CVC4::TupleUpdate::getIndex().
std::ostream& CVC4::operator<< | ( | std::ostream & | out, |
BenchmarkStatus | status | ||
) | |||
throw | ( | ||
) |
|
inline |
Definition at line 67 of file record.h.
References CVC4::RecordSelect::getField().
std::ostream& CVC4::operator<< | ( | std::ostream & | out, |
const AbstractValue & | val | ||
) |
|
inline |
Definition at line 71 of file record.h.
References CVC4::RecordUpdate::getField().
std::ostream& CVC4::operator<< | ( | std::ostream & | out, |
const UninterpretedConstant & | uc | ||
) |
Referenced by CVC4::Chain::getOperator(), CVC4::IllegalArgumentException::IllegalArgumentException(), CVC4::LogicInfo::isComparableTo(), CVC4::Result::operator!=(), CVC4::SExpr::operator!=(), CVC4::DivisibleHashFunction::operator()(), CVC4::TupleUpdateHashFunction::operator()(), CVC4::RecordUpdateHashFunction::operator()(), CVC4::RecordHashFunction::operator()(), CVC4::SubrangeBoundsHashFunction::operator()(), CVC4::strings::StringHashFunction::operator()(), CVC4::RegExpHashFunction::operator()(), CVC4::RationalHashFunction::operator()(), CVC4::UnsignedHashFunction< T >::operator()(), CVC4::IntegerHashFunction::operator()(), CVC4::DatatypeHashFunction::operator()(), operator<<(), CVC4::AbstractValue::operator>=(), CVC4::UninterpretedConstant::operator>=(), CVC4::EmptySet::operator>=(), CVC4::ArrayStoreAll::operator>=(), CVC4::Cardinality::operator^(), and CVC4::CommandPrintSuccess::Scope::~Scope().
std::ostream& CVC4::operator<< | ( | std::ostream & | out, |
const EmptySet & | es | ||
) |
std::ostream& CVC4::operator<< | ( | std::ostream & | out, |
const Type & | t | ||
) |
Output operator for types.
out | the stream to output to |
t | the type to output |
std::ostream& CVC4::operator<< | ( | std::ostream & | out, |
const ArrayStoreAll & | asa | ||
) |
|
inline |
Definition at line 125 of file exception.h.
References CheckArgument(), CVC4_PUBLIC, and CVC4::Exception::toStream().
|
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.
out | the stream to output to |
e | the expression to output |
|
inline |
Definition at line 245 of file subrange_bound.h.
References CVC4_PUBLIC, CVC4::SubrangeBound::getBound(), CVC4::SubrangeBound::hasBound(), operator<<(), and CVC4::options::out.
|
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 & | 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 Rational & | n | ||
) |
std::ostream& CVC4::operator<< | ( | std::ostream & | os, |
const RegExp & | s | ||
) |
|
inline |
Definition at line 511 of file bitvector.h.
References CVC4_PUBLIC, operator<<(), and CVC4::BitVector::toString().
|
inline |
Definition at line 516 of file bitvector.h.
References CVC4_PUBLIC, CVC4::BitVectorExtract::high, CVC4::BitVectorExtract::low, and operator<<().
|
inline |
Definition at line 521 of file bitvector.h.
References CVC4::BitVectorBitOf::bitIndex, CVC4_PUBLIC, and operator<<().
|
inline |
Definition at line 521 of file integer_cln_imp.h.
References CVC4::Integer::toString().
|
inline |
Definition at line 526 of file bitvector.h.
References CVC4::IntToBitVector::size.
|
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 | ( | ||
) |