CVC3
Classes | Public Member Functions | Private Member Functions | Private Attributes

CVC3::Translator Class Reference

#include <translator.h>

Collaboration diagram for CVC3::Translator:
Collaboration graph
[legend]

List of all members.

Classes

Public Member Functions

Private Member Functions

Private Attributes


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

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

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

Definition at line 69 of file translator.h.

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

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

Definition at line 86 of file translator.h.

Referenced by finish(), and start().

Definition at line 88 of file translator.h.

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

Definition at line 88 of file translator.h.

Referenced by printArrayExpr(), and processType().

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

Definition at line 88 of file translator.h.

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

Definition at line 89 of file translator.h.

Referenced by finish(), and processType().

Definition at line 90 of file translator.h.

Referenced by finish(), and processType().

Definition at line 91 of file translator.h.

Referenced by finish().

Definition at line 92 of file translator.h.

Referenced by finish().

Definition at line 93 of file translator.h.

Referenced by finish().

Definition at line 94 of file translator.h.

Referenced by finish().

Definition at line 96 of file translator.h.

Referenced by finish(), and zeroVar().

Definition at line 97 of file translator.h.

Referenced by finish(), and processType().

Definition at line 99 of file translator.h.

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

Definition at line 100 of file translator.h.

Referenced by finish(), and setTheoryUF().

Definition at line 101 of file translator.h.

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

Definition at line 102 of file translator.h.

Referenced by finish(), and setTheoryArray().

Definition at line 103 of file translator.h.

Referenced by finish(), and setTheoryQuant().

Definition at line 104 of file translator.h.

Referenced by finish(), and setTheoryRecords().

Definition at line 105 of file translator.h.

Referenced by finish(), and setTheorySimulate().

Definition at line 106 of file translator.h.

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

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

Definition at line 112 of file translator.h.

Referenced by finish().

Definition at line 113 of file translator.h.

Referenced by finish(), and processType().

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: