CVC3  2.4.1
CVC3::Translator Member List

This is the complete list of members for CVC3::Translator, including all inherited members.

benchName()CVC3::Translatorinline
category()CVC3::Translatorinline
containsArray(const Expr &e)CVC3::Translatorprivate
d_arithUsedCVC3::Translatorprivate
d_arrayConvertMapCVC3::Translatorprivate
d_arrayTypeCVC3::Translatorprivate
d_axCVC3::Translatorprivate
d_benchNameCVC3::Translatorprivate
d_categoryCVC3::Translatorprivate
d_combineAssumpCVC3::Translatorprivate
d_convertArithCVC3::Translatorprivate
d_convertArrayCVC3::Translatorprivate
d_convertToBVCVC3::Translatorprivate
d_convertToDiffCVC3::Translatorprivate
d_dumpCVC3::Translatorprivate
d_dumpExprsCVC3::Translatorprivate
d_dumpFileOpenCVC3::Translatorprivate
d_elementTypeCVC3::Translatorprivate
d_emCVC3::Translatorprivate
d_equalitiesCVC3::Translatorprivate
d_expResultCVC3::Translatorprivate
d_indexTypeCVC3::Translatorprivate
d_intConstUsedCVC3::Translatorprivate
d_intIntArrayCVC3::Translatorprivate
d_intIntRealArrayCVC3::Translatorprivate
d_intRealArrayCVC3::Translatorprivate
d_intUsedCVC3::Translatorprivate
d_iteLiftArithCVC3::Translatorprivate
d_langUsedCVC3::Translatorprivate
d_osdumpCVC3::Translatorprivate
d_osdumpFileCVC3::Translatorprivate
d_real2intCVC3::Translatorprivate
d_realUsedCVC3::Translatorprivate
d_replaceSymbolsCVC3::Translatorprivate
d_sourceCVC3::Translatorprivate
d_statusCVC3::Translatorprivate
d_theoryArithCVC3::Translatorprivate
d_theoryArrayCVC3::Translatorprivate
d_theoryBitvectorCVC3::Translatorprivate
d_theoryCoreCVC3::Translatorprivate
d_theoryDatatypeCVC3::Translatorprivate
d_theoryQuantCVC3::Translatorprivate
d_theoryRecordsCVC3::Translatorprivate
d_theorySimulateCVC3::Translatorprivate
d_theoryUFCVC3::Translatorprivate
d_tmpFileCVC3::Translatorprivate
d_translateCVC3::Translatorprivate
d_UFIDL_okCVC3::Translatorprivate
d_unknownCVC3::Translatorprivate
d_zeroVarCVC3::Translatorprivate
dump(const Expr &e, bool dumpOnly=false)CVC3::Translator
dumpAssertion(const Expr &e)CVC3::Translator
dumpQuery(const Expr &e)CVC3::Translator
dumpQueryResult(QueryResult qres)CVC3::Translator
escapeSymbol(const std::string &s)CVC3::Translator
fileToSMTLIBIdentifier(const std::string &filename)CVC3::Translatorprivate
finish()CVC3::Translator
fixConstName(const std::string &s)CVC3::Translator
preprocess(const Expr &e, ExprMap< Expr > &cache)CVC3::Translatorprivate
preprocess2(const Expr &e, ExprMap< Expr > &cache)CVC3::Translatorprivate
preprocess2Rec(const Expr &e, ExprMap< Expr > &cache, Type desiredType)CVC3::Translatorprivate
preprocessRec(const Expr &e, ExprMap< Expr > &cache)CVC3::Translatorprivate
printArrayExpr(ExprStream &os, const Expr &e)CVC3::Translator
processType(const Expr &e)CVC3::Translatorprivate
quoteAnnotation(const std::string &s)CVC3::Translator
setBenchName(std::string name)CVC3::Translatorinline
setCategory(std::string category)CVC3::Translatorinline
setSource(std::string source)CVC3::Translatorinline
setStatus(std::string status)CVC3::Translatorinline
setTheoryArith(TheoryArith *theoryArith)CVC3::Translatorinline
setTheoryArray(TheoryArray *theoryArray)CVC3::Translatorinline
setTheoryBitvector(TheoryBitvector *theoryBitvector)CVC3::Translatorinline
setTheoryCore(TheoryCore *theoryCore)CVC3::Translatorinline
setTheoryDatatype(TheoryDatatype *theoryDatatype)CVC3::Translatorinline
setTheoryQuant(TheoryQuant *theoryQuant)CVC3::Translatorinline
setTheoryRecords(TheoryRecords *theoryRecords)CVC3::Translatorinline
setTheorySimulate(TheorySimulate *theorySimulate)CVC3::Translatorinline
setTheoryUF(TheoryUF *theoryUF)CVC3::Translatorinline
source()CVC3::Translatorinline
start(const std::string &dumpFile)CVC3::Translator
status()CVC3::Translatorinline
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)CVC3::Translator
zeroVar()CVC3::Translator
~Translator()CVC3::Translator