cvc4-1.4
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

◆ ExprIndex

typedef size_t CVC3::ExprIndex

Definition at line 244 of file cvc3_compat.h.

◆ FormulaValue

◆ Op

typedef Expr CVC3::Op

Definition at line 309 of file cvc3_compat.h.

◆ QueryResult

◆ Statistics

Definition at line 462 of file cvc3_compat.h.

◆ TypecheckException

◆ Unsigned

typedef size_t CVC3::Unsigned

Definition at line 246 of file cvc3_compat.h.

Enumeration Type Documentation

◆ 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.

◆ CVC3CardinalityKind

Enumerator
CARD_FINITE 
CARD_INFINITE 
CARD_UNKNOWN 

Definition at line 254 of file cvc3_compat.h.

◆ FormulaValue

Enumerator
TRUE_VAL 
FALSE_VAL 
UNKNOWN_VAL 

Definition at line 493 of file cvc3_compat.h.

◆ QueryResult

Enumerator
SATISFIABLE 
INVALID 
VALID 
UNSATISFIABLE 
ABORT 
UNKNOWN 

Definition at line 476 of file cvc3_compat.h.

Function Documentation

◆ compare()

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

◆ int2string()

std::string CVC3::int2string ( int  n)

◆ isArrayLiteral()

bool CVC3::isArrayLiteral ( const Expr )

◆ operator!=() [1/2]

bool CVC3::operator!= ( const Cardinality c,
CVC3CardinalityKind  d 
)

◆ operator!=() [2/2]

bool CVC3::operator!= ( CVC3CardinalityKind  d,
const Cardinality c 
)

◆ operator<<() [1/4]

std::ostream& CVC3::operator<< ( std::ostream &  out,
CLFlagType  clft 
)

◆ operator<<() [2/4]

std::ostream& CVC3::operator<< ( std::ostream &  out,
CVC3CardinalityKind  c 
)

◆ operator<<() [3/4]

std::ostream& CVC3::operator<< ( std::ostream &  out,
QueryResult  qr 
)

◆ operator<<() [4/4]

std::ostream& CVC3::operator<< ( std::ostream &  out,
FormulaValue  fv 
)

◆ operator==() [1/2]

bool CVC3::operator== ( const Cardinality c,
CVC3CardinalityKind  d 
)

◆ operator==() [2/2]

bool CVC3::operator== ( CVC3CardinalityKind  d,
const Cardinality c 
)

◆ QueryResultToString()

std::string CVC3::QueryResultToString ( QueryResult  query_result)

Variable Documentation

◆ BVCONST

const CVC4::Kind CVC3::BVCONST

Definition at line 83 of file cvc3_compat.h.

◆ BVGE

const CVC4::Kind CVC3::BVGE

Definition at line 80 of file cvc3_compat.h.

◆ BVGT

const CVC4::Kind CVC3::BVGT

Definition at line 79 of file cvc3_compat.h.

◆ BVLE

const CVC4::Kind CVC3::BVLE

Definition at line 78 of file cvc3_compat.h.

◆ BVLT

const CVC4::Kind CVC3::BVLT

Definition at line 77 of file cvc3_compat.h.

◆ BVPLUS

const CVC4::Kind CVC3::BVPLUS

Definition at line 81 of file cvc3_compat.h.

◆ BVSUB

const CVC4::Kind CVC3::BVSUB

Definition at line 82 of file cvc3_compat.h.

◆ CONCAT

const CVC4::Kind CVC3::CONCAT

Definition at line 85 of file cvc3_compat.h.

◆ DIVIDE

const CVC4::Kind CVC3::DIVIDE

Definition at line 76 of file cvc3_compat.h.

◆ EQ

const CVC4::Kind CVC3::EQ

Definition at line 73 of file cvc3_compat.h.

◆ EXTRACT

const CVC4::Kind CVC3::EXTRACT

Definition at line 84 of file cvc3_compat.h.

◆ GE

const CVC4::Kind CVC3::GE

Definition at line 75 of file cvc3_compat.h.

◆ LE

const CVC4::Kind CVC3::LE

Definition at line 74 of file cvc3_compat.h.