CVC3  2.4.1
Classes | Public Member Functions | Private Member Functions | Private Attributes | List of all members
CVC3::Translator Class Reference

#include <translator.h>

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

ExprManagerd_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. More...
 
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
 
Exprd_zeroVar
 
int d_convertToBV
 
TheoryCored_theoryCore
 
TheoryUFd_theoryUF
 
TheoryArithd_theoryArith
 
TheoryArrayd_theoryArray
 
TheoryQuantd_theoryQuant
 
TheoryRecordsd_theoryRecords
 
TheorySimulated_theorySimulate
 
TheoryBitvectord_theoryBitvector
 
TheoryDatatyped_theoryDatatype
 
std::vector< Exprd_dumpExprs
 
std::map< std::string, Type > * d_arrayConvertMap
 
Typed_indexType
 
Typed_elementType
 
Typed_arrayType
 
std::vector< Exprd_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
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)
void Translator::dump ( const Expr e,
bool  dumpOnly = false 
)

Dump the expression in the current output language

Parameters
dumpOnlyWhen 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().

bool Translator::dumpAssertion ( const Expr e)

Definition at line 970 of file translator.cpp.

References ASSERT, d_dumpExprs, and d_translate.

bool Translator::dumpQuery ( const Expr e)

Definition at line 978 of file translator.cpp.

References d_dumpExprs, d_translate, and QUERY.

void Translator::dumpQueryResult ( QueryResult  qres)
void Translator::finish ( )
void CVC3::Translator::setTheoryCore ( TheoryCore theoryCore)
inline

Definition at line 166 of file translator.h.

References d_theoryCore.

void CVC3::Translator::setTheoryUF ( TheoryUF theoryUF)
inline

Definition at line 167 of file translator.h.

References d_theoryUF.

void CVC3::Translator::setTheoryArith ( TheoryArith theoryArith)
inline

Definition at line 168 of file translator.h.

References d_theoryArith.

void CVC3::Translator::setTheoryArray ( TheoryArray theoryArray)
inline

Definition at line 169 of file translator.h.

References d_theoryArray.

void CVC3::Translator::setTheoryQuant ( TheoryQuant theoryQuant)
inline

Definition at line 170 of file translator.h.

References d_theoryQuant.

void CVC3::Translator::setTheoryRecords ( TheoryRecords theoryRecords)
inline

Definition at line 171 of file translator.h.

References d_theoryRecords.

void CVC3::Translator::setTheorySimulate ( TheorySimulate theorySimulate)
inline

Definition at line 172 of file translator.h.

References d_theorySimulate.

void CVC3::Translator::setTheoryBitvector ( TheoryBitvector theoryBitvector)
inline

Definition at line 173 of file translator.h.

References d_theoryBitvector.

void CVC3::Translator::setTheoryDatatype ( TheoryDatatype theoryDatatype)
inline

Definition at line 174 of file translator.h.

References d_theoryDatatype.

void CVC3::Translator::setBenchName ( std::string  name)
inline

Definition at line 176 of file translator.h.

References d_benchName.

std::string CVC3::Translator::benchName ( )
inline

Definition at line 177 of file translator.h.

References d_benchName.

void CVC3::Translator::setStatus ( std::string  status)
inline

Definition at line 178 of file translator.h.

References d_status, and status().

std::string CVC3::Translator::status ( )
inline

Definition at line 179 of file translator.h.

References d_status.

Referenced by finish(), and setStatus().

void CVC3::Translator::setSource ( std::string  source)
inline

Definition at line 180 of file translator.h.

References d_source, and source().

std::string CVC3::Translator::source ( )
inline

Definition at line 181 of file translator.h.

References d_source.

Referenced by finish(), and setSource().

void CVC3::Translator::setCategory ( std::string  category)
inline

Definition at line 182 of file translator.h.

References category(), and d_category.

std::string CVC3::Translator::category ( )
inline

Definition at line 183 of file translator.h.

References d_category.

Referenced by finish(), and setCategory().

const string Translator::fixConstName ( const std::string &  s)
const string Translator::escapeSymbol ( const std::string &  s)
const string Translator::quoteAnnotation ( const std::string &  s)

Definition at line 1830 of file translator.cpp.

Referenced by finish(), and CVC3::TheoryCore::print().

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

Member Data Documentation

ExprManager* CVC3::Translator::d_em
private

Definition at line 61 of file translator.h.

Referenced by dumpQueryResult(), escapeSymbol(), finish(), fixConstName(), printArrayExpr(), and start().

const bool& CVC3::Translator::d_translate
private

Definition at line 62 of file translator.h.

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

const bool& CVC3::Translator::d_real2int
private

Definition at line 63 of file translator.h.

Referenced by processType().

const bool& CVC3::Translator::d_convertArith
private

Definition at line 64 of file translator.h.

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

Definition at line 65 of file translator.h.

Referenced by zeroVar().

bool CVC3::Translator::d_iteLiftArith
private

Definition at line 66 of file translator.h.

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

Definition at line 67 of file translator.h.

Referenced by finish().

std::string CVC3::Translator::d_category
private

Definition at line 68 of file translator.h.

Referenced by category(), and setCategory().

bool CVC3::Translator::d_convertArray
private

Definition at line 69 of file translator.h.

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

bool CVC3::Translator::d_combineAssump
private

Definition at line 70 of file translator.h.

Referenced by finish().

std::hash_map<std::string, std::string, HashString> CVC3::Translator::d_replaceSymbols
private

Definition at line 80 of file translator.h.

Referenced by finish(), and fixConstName().

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

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

Definition at line 83 of file translator.h.

Referenced by dumpQueryResult(), finish(), and start().

std::ofstream CVC3::Translator::d_osdumpFile
private

Definition at line 84 of file translator.h.

Referenced by finish(), and start().

std::ifstream CVC3::Translator::d_tmpFile
private

Definition at line 85 of file translator.h.

Referenced by start().

bool CVC3::Translator::d_dump
private

Definition at line 86 of file translator.h.

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

bool CVC3::Translator::d_dumpFileOpen
private

Definition at line 86 of file translator.h.

Referenced by finish(), and start().

bool CVC3::Translator::d_intIntArray
private

Definition at line 88 of file translator.h.

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

bool CVC3::Translator::d_intRealArray
private

Definition at line 88 of file translator.h.

Referenced by printArrayExpr(), and processType().

bool CVC3::Translator::d_intIntRealArray
private

Definition at line 88 of file translator.h.

Referenced by printArrayExpr(), and processType().

bool CVC3::Translator::d_ax
private

Definition at line 88 of file translator.h.

Referenced by finish(), and processType().

bool CVC3::Translator::d_unknown
private

Definition at line 88 of file translator.h.

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

bool CVC3::Translator::d_realUsed
private

Definition at line 89 of file translator.h.

Referenced by finish(), and processType().

bool CVC3::Translator::d_intUsed
private

Definition at line 90 of file translator.h.

Referenced by finish(), and processType().

bool CVC3::Translator::d_intConstUsed
private

Definition at line 91 of file translator.h.

Referenced by finish().

ArithLang CVC3::Translator::d_langUsed
private

Definition at line 92 of file translator.h.

Referenced by finish().

bool CVC3::Translator::d_UFIDL_ok
private

Definition at line 93 of file translator.h.

Referenced by finish().

bool CVC3::Translator::d_arithUsed
private

Definition at line 94 of file translator.h.

Referenced by finish().

Expr* CVC3::Translator::d_zeroVar
private

Definition at line 96 of file translator.h.

Referenced by finish(), and zeroVar().

int CVC3::Translator::d_convertToBV
private

Definition at line 97 of file translator.h.

Referenced by finish(), and processType().

TheoryCore* CVC3::Translator::d_theoryCore
private

Definition at line 99 of file translator.h.

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

TheoryUF* CVC3::Translator::d_theoryUF
private

Definition at line 100 of file translator.h.

Referenced by finish(), and setTheoryUF().

TheoryArith* CVC3::Translator::d_theoryArith
private

Definition at line 101 of file translator.h.

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

TheoryArray* CVC3::Translator::d_theoryArray
private

Definition at line 102 of file translator.h.

Referenced by finish(), and setTheoryArray().

TheoryQuant* CVC3::Translator::d_theoryQuant
private

Definition at line 103 of file translator.h.

Referenced by finish(), and setTheoryQuant().

TheoryRecords* CVC3::Translator::d_theoryRecords
private

Definition at line 104 of file translator.h.

Referenced by finish(), and setTheoryRecords().

TheorySimulate* CVC3::Translator::d_theorySimulate
private

Definition at line 105 of file translator.h.

Referenced by finish(), and setTheorySimulate().

TheoryBitvector* CVC3::Translator::d_theoryBitvector
private

Definition at line 106 of file translator.h.

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

TheoryDatatype* CVC3::Translator::d_theoryDatatype
private

Definition at line 107 of file translator.h.

Referenced by finish(), and setTheoryDatatype().

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

Definition at line 109 of file translator.h.

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

std::map<std::string, Type>* CVC3::Translator::d_arrayConvertMap
private

Definition at line 111 of file translator.h.

Referenced by finish(), Translator(), and ~Translator().

Type* CVC3::Translator::d_indexType
private

Definition at line 112 of file translator.h.

Referenced by finish().

Type* CVC3::Translator::d_elementType
private

Definition at line 113 of file translator.h.

Referenced by finish(), and processType().

Type* CVC3::Translator::d_arrayType
private

Definition at line 114 of file translator.h.

Referenced by finish(), and processType().

std::vector<Expr> CVC3::Translator::d_equalities
private

Definition at line 115 of file translator.h.

Referenced by finish().

std::string CVC3::Translator::d_benchName
private

Definition at line 118 of file translator.h.

Referenced by benchName(), and setBenchName().

std::string CVC3::Translator::d_status
private

Definition at line 120 of file translator.h.

Referenced by setStatus(), and status().

std::string CVC3::Translator::d_source
private

Definition at line 122 of file translator.h.

Referenced by setSource(), and source().


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