Classes

class HashString

Public Member Functions

Translator (ExprManager *em, const bool &translate, const bool &real2int, const bool &convertArith, const std::string &convertToDiff, bool iteLiftArith, const std::string &expResult, const std::string &category, bool convertArray, bool combineAssump, int convertToBV)
~Translator ()
bool start (const std::string &dumpFile)
void dump (const Expr &e, bool dumpOnly=false)
bool dumpAssertion (const Expr &e)
bool dumpQuery (const Expr &e)
void dumpQueryResult (QueryResult qres)
void finish ()
void setTheoryCore (TheoryCore *theoryCore)
void setTheoryUF (TheoryUF *theoryUF)
void setTheoryArith (TheoryArith *theoryArith)
void setTheoryArray (TheoryArray *theoryArray)
void setTheoryQuant (TheoryQuant *theoryQuant)
void setTheoryRecords (TheoryRecords *theoryRecords)
void setTheorySimulate (TheorySimulate *theorySimulate)
void setTheoryBitvector (TheoryBitvector *theoryBitvector)
void setTheoryDatatype (TheoryDatatype *theoryDatatype)
void setBenchName (std::string name)
std::string benchName ()
void setStatus (std::string status)
std::string status ()
void setSource (std::string source)
std::string source ()
void setCategory (std::string category)
std::string category ()
const std::string fixConstName (const std::string &s)
const std::string escapeSymbol (const std::string &s)
const std::string quoteAnnotation (const std::string &s)
bool printArrayExpr (ExprStream &os, const Expr &e)
Returns true if expression has been printed.
Expr zeroVar ()

Private Member Functions

std::string fileToSMTLIBIdentifier (const std::string &filename)
Expr preprocessRec (const Expr &e, ExprMap< Expr > &cache)
Expr preprocess (const Expr &e, ExprMap< Expr > &cache)
Expr preprocess2Rec (const Expr &e, ExprMap< Expr > &cache, Type desiredType)
Expr preprocess2 (const Expr &e, ExprMap< Expr > &cache)
bool containsArray (const Expr &e)
Expr processType (const Expr &e)

Private Attributes

ExprManager * d_em
const bool & d_translate
const bool & d_real2int
const bool & d_convertArith
const std::string & d_convertToDiff
bool d_iteLiftArith
const std::string & d_expResult
std::string d_category
bool d_convertArray
bool d_combineAssump
std::hash_map< std::string,
std::string, HashString > d_replaceSymbols
std::ostream * d_osdump
The log file for top-level API calls in the CVC3 input language.
std::ofstream d_osdumpFile
std::ifstream d_tmpFile
bool d_dump
bool d_dumpFileOpen
bool d_intIntArray
bool d_intRealArray
bool d_intIntRealArray
bool d_ax
bool d_unknown
bool d_realUsed
bool d_intUsed
bool d_intConstUsed
ArithLang d_langUsed
bool d_UFIDL_ok
bool d_arithUsed
Expr * d_zeroVar
int d_convertToBV
TheoryCore * d_theoryCore
TheoryUF * d_theoryUF
TheoryArith * d_theoryArith
TheoryArray * d_theoryArray
TheoryQuant * d_theoryQuant
TheoryRecords * d_theoryRecords
TheorySimulate * d_theorySimulate
TheoryBitvector * d_theoryBitvector
TheoryDatatype * d_theoryDatatype
std::vector< Expr > d_dumpExprs
std::map< std::string, Type > * d_arrayConvertMap
Type * d_indexType
Type * d_elementType
Type * d_arrayType
std::vector< Expr > d_equalities
std::string d_benchName
std::string d_status
std::string d_source

Detailed Description

Definition at line 60 of file translator.h.

Constructor & Destructor Documentation

Translator::Translator	(	ExprManager *	em,
		const bool &	translate,
		const bool &	real2int,
		const bool &	convertArith,
		const std::string &	convertToDiff,
		bool	iteLiftArith,
		const std::string &	expResult,
		const std::string &	category,
		bool	convertArray,
		bool	combineAssump,
		int	convertToBV
	)

Definition at line 808 of file translator.cpp.

References d_arrayConvertMap.

Translator::~Translator ( )

Definition at line 839 of file translator.cpp.

References d_arrayConvertMap.

Member Function Documentation

string Translator::fileToSMTLIBIdentifier ( const std::string & filename ) [private]

Definition at line 45 of file translator.cpp.

Referenced by start().

Expr Translator::preprocessRec	(	const Expr &	e,
		ExprMap< Expr > &	cache
	)		`[private]`

Definition at line 72 of file translator.cpp.

References APPLY, CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVMULT, CVC3::BVPLUS, CVC3::BVSLE, CVC3::BVSLT, CVC3::BVSUB, CVC3::BVUMINUS, CVC3::Expr::containsTermITE(), DebugAssert, CVC3::DIFF_ONLY, CVC3::DIVIDE, CVC3::Expr::end(), CVC3::ExprMap< Data >::end(), EQ, FatalAssert, CVC3::ExprMap< Data >::find(), CVC3::GE, CVC3::Expr::getBody(), CVC3::Expr::getKids(), CVC3::Expr::getKind(), CVC3::Expr::getName(), CVC3::Rational::getNumerator(), CVC3::Expr::getOp(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getRational(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Expr::getVars(), CVC3::GT, CVC3::INTDIV, CVC3::IS_INTEGER, CVC3::Expr::isClosure(), CVC3::isInt(), CVC3::Rational::isInteger(), CVC3::Expr::isPropAtom(), CVC3::Expr::isRational(), CVC3::isRational(), CVC3::Expr::isVar(), ITE, CVC3::Expr::iteExpr(), LAMBDA, CVC3::LE, CVC3::LINEAR, CVC3::LT, CVC3::MINUS, CVC3::MOD, CVC3::MULT, CVC3::NONLINEAR, NOT, CVC3::NOT_USED, CVC3::PLUS, CVC3::POW, CVC3::pow(), RATIONAL_EXPR, CVC3::READ, CVC3::TERMS_ONLY, UCONST, CVC3::UMINUS, and CVC3::WRITE.

Expr Translator::preprocess	(	const Expr &	e,
		ExprMap< Expr > &	cache
	)		`[private]`

Definition at line 549 of file translator.cpp.

References std::endl(), and CVC3::Expr::toString().

Referenced by finish().

Expr Translator::preprocess2Rec	(	const Expr &	e,
		ExprMap< Expr > &	cache,
		Type	desiredType
	)		`[private]`

Expr Translator::preprocess2	(	const Expr &	e,
		ExprMap< Expr > &	cache
	)		`[private]`

Definition at line 783 of file translator.cpp.

References std::endl(), and CVC3::Expr::toString().

Referenced by finish().

bool Translator::containsArray ( const Expr & e ) [private]

Definition at line 799 of file translator.cpp.

References CVC3::ARRAY, CVC3::Expr::begin(), CVC3::Expr::end(), and CVC3::Expr::getKind().

Referenced by dump().

Expr Translator::processType ( const Expr & e ) [private]

bool Translator::start ( const std::string & dumpFile )

Definition at line 845 of file translator.cpp.

References d_dump, d_dumpFileOpen, d_em, d_osdump, d_osdumpFile, d_tmpFile, d_translate, std::endl(), fileToSMTLIBIdentifier(), CVC3::ExprManager::getOutputLang(), CVC3::SMTLIB_LANG, and CVC3::SPASS_LANG.

void Translator::dump	(	const Expr &	e,
		bool	dumpOnly = `false`
	)

Dump the expression in the current output language

Parameters:

dumpOnly When false, the expression is output both when translating and when producing a trace of commands. When true, the expression is only output when producing a trace of commands (i.e. ignored during translation).

Definition at line 939 of file translator.cpp.

References CVC3::Expr::arity(), CVC3::ARRAY, ARROW, CONST, containsArray(), d_convertArray, d_dump, d_dumpExprs, d_translate, DebugAssert, and CVC3::Expr::getKind().