cvc4-1.4
|
Data Structures | |
class | CLFlag |
class | CLFlags |
class | Expr |
Expr class for CVC3 compatibility layer. More... | |
class | ExprHashMap |
class | ExprManager |
class | ExprMap |
class | Proof |
class | Theorem |
class | Type |
class | ValidityChecker |
CVC3 API (compatibility layer for CVC4) More... | |
Typedefs | |
typedef size_t | ExprIndex |
typedef CVC4::TypeCheckingException | TypecheckException |
typedef size_t | Unsigned |
typedef Expr | Op |
typedef CVC4::Statistics | Statistics |
typedef enum CVC3::QueryResult | QueryResult |
typedef enum CVC3::FormulaValue | FormulaValue |
Enumerations | |
enum | CLFlagType { CLFLAG_NULL, CLFLAG_BOOL, CLFLAG_INT, CLFLAG_STRING, CLFLAG_STRVEC } |
Different types of command line flags. More... | |
enum | CVC3CardinalityKind { CARD_FINITE, CARD_INFINITE, CARD_UNKNOWN } |
enum | QueryResult { SATISFIABLE, INVALID, VALID, UNSATISFIABLE, ABORT, UNKNOWN } |
enum | FormulaValue { TRUE_VAL, FALSE_VAL, UNKNOWN_VAL } |
Functions | |
std::string | int2string (int n) |
std::ostream & | operator<< (std::ostream &out, CLFlagType clft) |
std::ostream & | operator<< (std::ostream &out, CVC3CardinalityKind c) |
bool | operator== (const Cardinality &c, CVC3CardinalityKind d) |
bool | operator== (CVC3CardinalityKind d, const Cardinality &c) |
bool | operator!= (const Cardinality &c, CVC3CardinalityKind d) |
bool | operator!= (CVC3CardinalityKind d, const Cardinality &c) |
bool | isArrayLiteral (const Expr &) |
std::ostream & | operator<< (std::ostream &out, QueryResult qr) |
std::string | QueryResultToString (QueryResult query_result) |
std::ostream & | operator<< (std::ostream &out, FormulaValue fv) |
int | compare (const Expr &e1, const Expr &e2) |
Variables | |
const CVC4::Kind | EQ |
const CVC4::Kind | LE |
const CVC4::Kind | GE |
const CVC4::Kind | DIVIDE |
const CVC4::Kind | BVLT |
const CVC4::Kind | BVLE |
const CVC4::Kind | BVGT |
const CVC4::Kind | BVGE |
const CVC4::Kind | BVPLUS |
const CVC4::Kind | BVSUB |
const CVC4::Kind | BVCONST |
const CVC4::Kind | EXTRACT |
const CVC4::Kind | CONCAT |
typedef size_t CVC3::ExprIndex |
Definition at line 244 of file cvc3_compat.h.
typedef enum CVC3::FormulaValue CVC3::FormulaValue |
Definition at line 309 of file cvc3_compat.h.
typedef enum CVC3::QueryResult CVC3::QueryResult |
typedef CVC4::Statistics CVC3::Statistics |
Definition at line 462 of file cvc3_compat.h.
Definition at line 245 of file cvc3_compat.h.
typedef size_t CVC3::Unsigned |
Definition at line 246 of file cvc3_compat.h.
enum CVC3::CLFlagType |
Different types of command line flags.
Enumerator | |
---|---|
CLFLAG_NULL | |
CLFLAG_BOOL | |
CLFLAG_INT | |
CLFLAG_STRING | |
CLFLAG_STRVEC |
Vector of pair<string, bool> |
Definition at line 90 of file cvc3_compat.h.
Enumerator | |
---|---|
CARD_FINITE | |
CARD_INFINITE | |
CARD_UNKNOWN |
Definition at line 254 of file cvc3_compat.h.
enum CVC3::FormulaValue |
Enumerator | |
---|---|
TRUE_VAL | |
FALSE_VAL | |
UNKNOWN_VAL |
Definition at line 493 of file cvc3_compat.h.
enum CVC3::QueryResult |
Enumerator | |
---|---|
SATISFIABLE | |
INVALID | |
VALID | |
UNSATISFIABLE | |
ABORT | |
UNKNOWN |
Definition at line 476 of file cvc3_compat.h.
Referenced by CVC4::Rational::cmp().
std::string CVC3::int2string | ( | int | n | ) |
bool CVC3::isArrayLiteral | ( | const Expr & | ) |
bool CVC3::operator!= | ( | const Cardinality & | c, |
CVC3CardinalityKind | d | ||
) |
bool CVC3::operator!= | ( | CVC3CardinalityKind | d, |
const Cardinality & | c | ||
) |
std::ostream& CVC3::operator<< | ( | std::ostream & | out, |
CLFlagType | clft | ||
) |
std::ostream& CVC3::operator<< | ( | std::ostream & | out, |
CVC3CardinalityKind | c | ||
) |
std::ostream& CVC3::operator<< | ( | std::ostream & | out, |
QueryResult | qr | ||
) |
std::ostream& CVC3::operator<< | ( | std::ostream & | out, |
FormulaValue | fv | ||
) |
bool CVC3::operator== | ( | const Cardinality & | c, |
CVC3CardinalityKind | d | ||
) |
bool CVC3::operator== | ( | CVC3CardinalityKind | d, |
const Cardinality & | c | ||
) |
std::string CVC3::QueryResultToString | ( | QueryResult | query_result | ) |
const CVC4::Kind CVC3::BVCONST |
Definition at line 83 of file cvc3_compat.h.
const CVC4::Kind CVC3::BVGE |
Definition at line 80 of file cvc3_compat.h.
const CVC4::Kind CVC3::BVGT |
Definition at line 79 of file cvc3_compat.h.
const CVC4::Kind CVC3::BVLE |
Definition at line 78 of file cvc3_compat.h.
const CVC4::Kind CVC3::BVLT |
Definition at line 77 of file cvc3_compat.h.
const CVC4::Kind CVC3::BVPLUS |
Definition at line 81 of file cvc3_compat.h.
const CVC4::Kind CVC3::BVSUB |
Definition at line 82 of file cvc3_compat.h.
const CVC4::Kind CVC3::CONCAT |
Definition at line 85 of file cvc3_compat.h.
const CVC4::Kind CVC3::DIVIDE |
Definition at line 76 of file cvc3_compat.h.
const CVC4::Kind CVC3::EQ |
Definition at line 73 of file cvc3_compat.h.
const CVC4::Kind CVC3::EXTRACT |
Definition at line 84 of file cvc3_compat.h.
const CVC4::Kind CVC3::GE |
Definition at line 75 of file cvc3_compat.h.
const CVC4::Kind CVC3::LE |
Definition at line 74 of file cvc3_compat.h.