CVC3 Namespace Reference

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 Documentation

typedef size_t CVC3::ExprIndex

Definition at line 244 of file cvc3_compat.h.

typedef enum CVC3::FormulaValue CVC3::FormulaValue

typedef Expr CVC3::Op

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.

typedef CVC4::TypeCheckingException CVC3::TypecheckException

Definition at line 245 of file cvc3_compat.h.

typedef size_t CVC3::Unsigned

Definition at line 246 of file cvc3_compat.h.

Enumeration Type Documentation

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.

enum CVC3::CVC3CardinalityKind

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.

Function Documentation

int CVC3::compare	(	const Expr &	e1,
		const Expr &	e2
	)

Referenced by CVC4::Rational::cmp(), CVC3::ExprHashMap< T >::insert(), and CVC4::Cardinality::operator^().

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

)

Variable Documentation

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.