CVC3::Translator Class Reference

#include <translator.h>

Collaboration diagram for CVC3::Translator:

[legend]

List of all members.

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)
const std::string fixConstName (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
const std::string & d_category
bool d_convertArray
bool d_combineAssump
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

Detailed Description

Definition at line 58 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 689 of file translator.cpp.

References d_arrayConvertMap.

Translator::~Translator ( )

Definition at line 720 of file translator.cpp.

References d_arrayConvertMap.

Member Function Documentation

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::Rational::getNumerator(), 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::Expr::isRational(), 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.