CVC3: CVC3::Translator Class Reference

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 689 of file translator.cpp.

References d_arrayConvertMap.

Translator::~Translator ( )

Definition at line 720 of file translator.cpp.

References d_arrayConvertMap.

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

Definition at line 43 of file translator.cpp.

Referenced by start().

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

Definition at line 70 of file translator.cpp.

References CVC3::APPLY, CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVMULT, CVC3::BVPLUS, CVC3::BVSLE, CVC3::BVSLT, CVC3::BVSUB, CVC3::BVUMINUS, d_arrayConvertMap, d_convertArith, d_convertToBV, d_convertToDiff, d_elementType, d_em, d_equalities, d_indexType, d_intConstUsed, d_iteLiftArith, d_langUsed, d_realUsed, d_theoryArith, d_theoryBitvector, d_theoryCore, d_UFIDL_ok, d_unknown, DebugAssert, CVC3::DIFF_ONLY, CVC3::DIVIDE, CVC3::Expr::end(), CVC3::ExprMap< Data >::end(), CVC3::EQ, FatalAssert, CVC3::ExprMap< Data >::find(), CVC3::GE, CVC3::Theory::getBaseType(), CVC3::Expr::getBody(), CVC3::TheoryCore::getFlags(), CVC3::Expr::getKids(), CVC3::Expr::getKind(), CVC3::Expr::getName(), CVC3::Expr::getOp(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getRational(), CVC3::Expr::getType(), CVC3::Expr::getVars(), CVC3::GT, CVC3::INTDIV, CVC3::TheoryArith::intType(), CVC3::IS_INTEGER, CVC3::TheoryArith::isAtomicArithFormula(), CVC3::Expr::isClosure(), CVC3::isInt(), CVC3::Rational::isInteger(), CVC3::Theory::isLeaf(), CVC3::isRational(), CVC3::TheoryArith::isSyntacticRational(), CVC3::Expr::isVar(), CVC3::ITE, CVC3::Expr::iteExpr(), CVC3::LAMBDA, CVC3::LE, CVC3::LINEAR, CVC3::LT, CVC3::MINUS, CVC3::MOD, CVC3::MULT, CVC3::TheoryBitvector::newBitvectorType(), CVC3::ExprManager::newClosureExpr(), CVC3::ExprManager::newRatExpr(), CVC3::Theory::newVar(), CVC3::NONLINEAR, CVC3::NOT, CVC3::NOT_USED, CVC3::PLUS, CVC3::POW, CVC3::pow(), CVC3::RATIONAL_EXPR, CVC3::READ, CVC3::TheoryArith::realType(), CVC3::TheoryArith::rewriteToDiff(), CVC3::Theory::setUsed(), CVC3::TheoryBitvector::signed_newBVConstExpr(), CVC3::TERMS_ONLY, CVC3::Theory::theoryOf(), CVC3::UCONST, CVC3::UMINUS, and CVC3::WRITE.

Referenced by preprocess().

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

Definition at line 540 of file translator.cpp.

References std::endl(), preprocessRec(), 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 664 of file translator.cpp.

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

Referenced by finish().

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

Definition at line 680 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 726 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(), and CVC3::SMTLIB_LANG.

Referenced by CVC3::VCL::init().

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 795 of file translator.cpp.

References CVC3::Expr::arity(), CVC3::ARRAY, CVC3::ARROW, CVC3::CONST, containsArray(), d_convertArray, d_dump, d_dumpExprs, d_em, d_osdump, d_translate, DebugAssert, std::endl(), CVC3::Expr::getKind(), CVC3::ExprManager::getOutputLang(), and CVC3::SMTLIB_LANG.