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)
• 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 ()
• virtual ~Translator ()

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
• 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

---

Detailed Description

Definition at line 57 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
	)

Definition at line 500 of file translator.cpp.

virtual CVC3::Translator::~Translator

(

)

[inline, virtual]

Definition at line 143 of file translator.h.

---

Member Function Documentation

string Translator::fileToSMTLIBIdentifier

(

const std::string &

filename

)

[private]

Definition at line 42 of file translator.cpp.

Referenced by start().

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

Definition at line 69 of file translator.cpp.

References CVC3::APPLY, CVC3::Expr::arity(), CVC3::Expr::begin(), d_convertArith, d_convertToDiff, d_em, d_intConstUsed, d_iteLiftArith, d_langUsed, d_realUsed, d_theoryArith, 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::Expr::getKids(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getRational(), CVC3::Expr::getVars(), CVC3::GT, CVC3::INTDIV, CVC3::IS_INTEGER, CVC3::TheoryArith::isAtomicArithFormula(), CVC3::Expr::isClosure(), CVC3::Theory::isLeaf(), CVC3::isRational(), CVC3::TheoryArith::isSyntacticRational(), CVC3::ITE, CVC3::Expr::iteExpr(), CVC3::LAMBDA, CVC3::LE, CVC3::LINEAR, CVC3::LT, CVC3::MINUS, CVC3::MOD, CVC3::MULT, CVC3::ExprManager::newClosureExpr(), CVC3::ExprManager::newRatExpr(), CVC3::NONLINEAR, CVC3::NOT_USED, CVC3::PLUS, CVC3::POW, CVC3::RATIONAL_EXPR, CVC3::TheoryArith::realType(), CVC3::TheoryArith::rewriteToDiff(), CVC3::Theory::setUsed(), CVC3::TERMS_ONLY, CVC3::Theory::theoryOf(), and CVC3::UMINUS.

Referenced by preprocess().

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

Definition at line 351 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]

Definition at line 365 of file translator.cpp.

References CVC3::ANY_TYPE, CVC3::Expr::arity(), d_em, d_theoryArith, d_unknown, CVC3::DIVIDE, CVC3::ExprMap< Data >::end(), CVC3::EQ, CVC3::ExprMap< Data >::find(), CVC3::GE, CVC3::Expr::getBody(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::Expr::getOpExpr(), CVC3::Expr::getType(), CVC3::Expr::getVars(), CVC3::GT, CVC3::TheoryArith::intType(), CVC3::Expr::isApply(), CVC3::Expr::isClosure(), CVC3::Type::isNull(), CVC3::ITE, CVC3::LE, CVC3::LT, CVC3::MINUS, CVC3::MULT, CVC3::ExprManager::newClosureExpr(), CVC3::PLUS, CVC3::RATIONAL_EXPR, CVC3::REAL_CONST, CVC3::TheoryArith::realType(), CVC3::Expr::toString(), and CVC3::UMINUS.

Referenced by preprocess2().

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

Definition at line 475 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 491 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]

Definition at line 680 of file translator.cpp.

References CVC3::Expr::arity(), d_intUsed, d_real2int, d_realUsed, d_theoryArith, d_theoryCore, d_unknown, CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::INT, CVC3::TheoryArith::intType(), CVC3::REAL, CVC3::Theory::setUsed(), CVC3::SUBRANGE, and CVC3::Theory::theoryOf().

Referenced by finish().

bool Translator::start

(

const std::string &

dumpFile

)

Definition at line 528 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.

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

Definition at line 597 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.

Referenced by CVC3::VCL::checkContinue(), CVC3::VCL::createOp(), CVC3::VCL::createType(), CVC3::VCL::getAssumptions(), CVC3::VCL::getAssumptionsTCC(), CVC3::VCL::getAssumptionsUsed(), CVC3::VCL::getClosure(), CVC3::VCL::getConcreteModel(), CVC3::VCL::getCounterExample(), CVC3::VCL::getProof(), CVC3::VCL::getProofClosure(), CVC3::VCL::getProofTCC(), CVC3::VCL::getTCC(), CVC3::VCL::pop(), CVC3::VCL::popScope(), CVC3::VCL::popto(), CVC3::VCL::poptoScope(), CVC3::VCL::push(), CVC3::VCL::pushScope(), CVC3::VCL::restart(), and CVC3::VCL::varExpr().

bool Translator::dumpAssertion

(

const Expr &

e

)

Definition at line 635 of file translator.cpp.

References CVC3::ASSERT, d_dumpExprs, d_em, d_osdump, d_translate, std::endl(), CVC3::ExprManager::getOutputLang(), and CVC3::SMTLIB_LANG.

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

bool Translator::dumpQuery

(

const Expr &

e

)

Definition at line 648 of file translator.cpp.

References d_dumpExprs, d_em, d_osdump, d_translate, std::endl(), CVC3::ExprManager::getOutputLang(), CVC3::QUERY, and CVC3::SMTLIB_LANG.

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

void Translator::dumpQueryResult

(

QueryResult

qres

)

Definition at line 661 of file translator.cpp.

References d_em, d_osdump, d_translate, std::endl(), CVC3::ExprManager::getOutputLang(), CVC3::SATISFIABLE, CVC3::SMTLIB_LANG, and CVC3::UNSATISFIABLE.

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

void Translator::finish

(

)

Definition at line 715 of file translator.cpp.

References CVC3::AND, CVC3::ASSERT, CVC3::CONST, d_arithUsed, d_ax, d_category, d_combineAssump, d_convertArray, d_dumpExprs, d_dumpFileOpen, d_em, d_expResult, d_intConstUsed, d_intIntArray, d_intUsed, d_langUsed, d_osdump, d_osdumpFile, d_realUsed, d_theoryArray, d_theoryBitvector, d_theoryDatatype, d_theoryQuant, d_theoryRecords, d_theorySimulate, d_theoryUF, d_translate, d_UFIDL_ok, d_unknown, d_zeroVar, DebugAssert, CVC3::DIFF_ONLY, std::endl(), CVC3::Type::getExpr(), CVC3::ExprManager::getOutputLang(), CVC3::Expr::getType(), CVC3::ID, CVC3::LINEAR, CVC3::Expr::negate(), CVC3::ExprManager::newStringExpr(), CVC3::NONLINEAR, CVC3::NOT_USED, preprocess(), preprocess2(), processType(), CVC3::QUERY, CVC3::RAW_LIST, CVC3::SMTLIB_LANG, CVC3::STRING_EXPR, CVC3::Theory::theoryUsed(), and CVC3::TYPE.

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

void CVC3::Translator::setTheoryCore

(

TheoryCore *

theoryCore

)

[inline]

Definition at line 125 of file translator.h.

References d_theoryCore.

void CVC3::Translator::setTheoryUF

(

TheoryUF *

theoryUF

)

[inline]

Definition at line 126 of file translator.h.

References d_theoryUF.

void CVC3::Translator::setTheoryArith

(

TheoryArith *

theoryArith

)

[inline]

Definition at line 127 of file translator.h.

References d_theoryArith.

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

void CVC3::Translator::setTheoryArray

(

TheoryArray *

theoryArray

)

[inline]

Definition at line 128 of file translator.h.

References d_theoryArray.

void CVC3::Translator::setTheoryQuant

(

TheoryQuant *

theoryQuant

)

[inline]

Definition at line 129 of file translator.h.

References d_theoryQuant.

void CVC3::Translator::setTheoryRecords

(

TheoryRecords *

theoryRecords

)

[inline]

Definition at line 130 of file translator.h.

References d_theoryRecords.

void CVC3::Translator::setTheorySimulate

(

TheorySimulate *

theorySimulate

)

[inline]

Definition at line 131 of file translator.h.

References d_theorySimulate.

void CVC3::Translator::setTheoryBitvector

(

TheoryBitvector *

theoryBitvector

)

[inline]

Definition at line 132 of file translator.h.

References d_theoryBitvector.

void CVC3::Translator::setTheoryDatatype

(

TheoryDatatype *

theoryDatatype

)

[inline]

Definition at line 133 of file translator.h.

References d_theoryDatatype.

const string Translator::fixConstName

(

const std::string &

s

)

Definition at line 1025 of file translator.cpp.

References d_em, CVC3::ExprManager::getOutputLang(), and CVC3::SMTLIB_LANG.

Referenced by CVC3::TheoryCore::print().

bool Translator::printArrayExpr	(	ExprStream &	os,
		const Expr &	e
	)

Returns true if expression has been printed.

If false is returned, array theory should print expression as usual

Definition at line 1036 of file translator.cpp.

References CVC3::ARRAY, CVC3::ARRAY_LITERAL, CVC3::ARROW, CVC3::BITVECTOR, d_ax, d_convertArray, d_em, d_intIntArray, d_intIntRealArray, d_intRealArray, d_theoryBitvector, d_unknown, DebugAssert, CVC3::TheoryBitvector::getBitvectorTypeParam(), CVC3::Expr::getKind(), CVC3::ExprManager::getOutputLang(), CVC3::isArray(), CVC3::isInt(), CVC3::isReal(), CVC3::ExprManager::newSymbolExpr(), CVC3::READ, CVC3::SMTLIB_LANG, CVC3::TYPEDECL, CVC3::UCONST, CVC3::UFUNC, and CVC3::WRITE.

Expr Translator::zeroVar

(

)

Definition at line 1125 of file translator.cpp.

References d_convertToDiff, d_theoryArith, d_theoryCore, d_zeroVar, CVC3::Type::getExpr(), CVC3::TheoryArith::intType(), CVC3::Theory::newVar(), and CVC3::TheoryArith::realType().

Referenced by CVC3::TheoryArith::rewriteToDiff().

---

Member Data Documentation

ExprManager* CVC3::Translator::d_em [private]

Definition at line 58 of file translator.h.

Referenced by dump(), dumpAssertion(), dumpQuery(), dumpQueryResult(), finish(), fixConstName(), preprocess2Rec(), preprocessRec(), printArrayExpr(), and start().

const bool& CVC3::Translator::d_translate [private]

Definition at line 59 of file translator.h.

Referenced by dump(), dumpAssertion(), dumpQuery(), dumpQueryResult(), finish(), and start().

const bool& CVC3::Translator::d_real2int [private]

Definition at line 60 of file translator.h.

Referenced by processType().

const bool& CVC3::Translator::d_convertArith [private]

Definition at line 61 of file translator.h.

Referenced by preprocessRec().

const std::string& CVC3::Translator::d_convertToDiff [private]

Definition at line 62 of file translator.h.

Referenced by preprocessRec(), and zeroVar().

bool CVC3::Translator::d_iteLiftArith [private]

Definition at line 63 of file translator.h.

Referenced by preprocessRec().

const std::string& CVC3::Translator::d_expResult [private]

Definition at line 64 of file translator.h.

Referenced by finish().

const std::string& CVC3::Translator::d_category [private]

Definition at line 65 of file translator.h.

Referenced by finish().

bool CVC3::Translator::d_convertArray [private]

Definition at line 66 of file translator.h.

Referenced by dump(), finish(), and printArrayExpr().

bool CVC3::Translator::d_combineAssump [private]

Definition at line 67 of file translator.h.

Referenced by finish().

std::ostream* CVC3::Translator::d_osdump [private]

The log file for top-level API calls in the CVC3 input language.

Definition at line 70 of file translator.h.

Referenced by dump(), dumpAssertion(), dumpQuery(), dumpQueryResult(), finish(), and start().

std::ofstream CVC3::Translator::d_osdumpFile [private]

Definition at line 71 of file translator.h.

Referenced by finish(), and start().

std::ifstream CVC3::Translator::d_tmpFile [private]

Definition at line 72 of file translator.h.

Referenced by start().

bool CVC3::Translator::d_dump [private]

Definition at line 73 of file translator.h.

Referenced by dump(), and start().

bool CVC3::Translator::d_dumpFileOpen [private]

Definition at line 73 of file translator.h.

Referenced by finish(), and start().

bool CVC3::Translator::d_intIntArray [private]

Definition at line 75 of file translator.h.

Referenced by finish(), and printArrayExpr().

bool CVC3::Translator::d_intRealArray [private]

Definition at line 75 of file translator.h.

Referenced by printArrayExpr().

bool CVC3::Translator::d_intIntRealArray [private]

Definition at line 75 of file translator.h.

Referenced by printArrayExpr().

bool CVC3::Translator::d_ax [private]

Definition at line 75 of file translator.h.

Referenced by finish(), and printArrayExpr().

bool CVC3::Translator::d_unknown [private]

Definition at line 75 of file translator.h.

Referenced by finish(), preprocess2Rec(), preprocessRec(), printArrayExpr(), and processType().

bool CVC3::Translator::d_realUsed [private]

Definition at line 76 of file translator.h.

Referenced by finish(), preprocessRec(), and processType().

bool CVC3::Translator::d_intUsed [private]

Definition at line 77 of file translator.h.

Referenced by finish(), and processType().

bool CVC3::Translator::d_intConstUsed [private]

Definition at line 78 of file translator.h.

Referenced by finish(), and preprocessRec().

ArithLang CVC3::Translator::d_langUsed [private]

Definition at line 79 of file translator.h.

Referenced by finish(), and preprocessRec().

bool CVC3::Translator::d_UFIDL_ok [private]

Definition at line 80 of file translator.h.

Referenced by finish(), and preprocessRec().

bool CVC3::Translator::d_arithUsed [private]

Definition at line 81 of file translator.h.

Referenced by finish().

Expr* CVC3::Translator::d_zeroVar [private]

Definition at line 83 of file translator.h.

Referenced by finish(), and zeroVar().

TheoryCore* CVC3::Translator::d_theoryCore [private]

Definition at line 85 of file translator.h.

Referenced by preprocessRec(), processType(), setTheoryCore(), and zeroVar().

TheoryUF* CVC3::Translator::d_theoryUF [private]

Definition at line 86 of file translator.h.

Referenced by finish(), and setTheoryUF().

TheoryArith* CVC3::Translator::d_theoryArith [private]

Definition at line 87 of file translator.h.

Referenced by preprocess2Rec(), preprocessRec(), processType(), setTheoryArith(), and zeroVar().

TheoryArray* CVC3::Translator::d_theoryArray [private]

Definition at line 88 of file translator.h.

Referenced by finish(), and setTheoryArray().

TheoryQuant* CVC3::Translator::d_theoryQuant [private]

Definition at line 89 of file translator.h.

Referenced by finish(), and setTheoryQuant().

TheoryRecords* CVC3::Translator::d_theoryRecords [private]

Definition at line 90 of file translator.h.

Referenced by finish(), and setTheoryRecords().

TheorySimulate* CVC3::Translator::d_theorySimulate [private]

Definition at line 91 of file translator.h.

Referenced by finish(), and setTheorySimulate().

TheoryBitvector* CVC3::Translator::d_theoryBitvector [private]

Definition at line 92 of file translator.h.

Referenced by finish(), printArrayExpr(), and setTheoryBitvector().

TheoryDatatype* CVC3::Translator::d_theoryDatatype [private]

Definition at line 93 of file translator.h.

Referenced by finish(), and setTheoryDatatype().

std::vector<Expr> CVC3::Translator::d_dumpExprs [private]

Definition at line 95 of file translator.h.

Referenced by dump(), dumpAssertion(), dumpQuery(), and finish().

---

The documentation for this class was generated from the following files:

• translator.h
• translator.cpp

---