CVC3

CVC3::Translator Member List

This is the complete list of members for CVC3::Translator, including all inherited members.
benchName()CVC3::Translator [inline]
category()CVC3::Translator [inline]
containsArray(const Expr &e)CVC3::Translator [private]
d_arithUsedCVC3::Translator [private]
d_arrayConvertMapCVC3::Translator [private]
d_arrayTypeCVC3::Translator [private]
d_axCVC3::Translator [private]
d_benchNameCVC3::Translator [private]
d_categoryCVC3::Translator [private]
d_combineAssumpCVC3::Translator [private]
d_convertArithCVC3::Translator [private]
d_convertArrayCVC3::Translator [private]
d_convertToBVCVC3::Translator [private]
d_convertToDiffCVC3::Translator [private]
d_dumpCVC3::Translator [private]
d_dumpExprsCVC3::Translator [private]
d_dumpFileOpenCVC3::Translator [private]
d_elementTypeCVC3::Translator [private]
d_emCVC3::Translator [private]
d_equalitiesCVC3::Translator [private]
d_expResultCVC3::Translator [private]
d_indexTypeCVC3::Translator [private]
d_intConstUsedCVC3::Translator [private]
d_intIntArrayCVC3::Translator [private]
d_intIntRealArrayCVC3::Translator [private]
d_intRealArrayCVC3::Translator [private]
d_intUsedCVC3::Translator [private]
d_iteLiftArithCVC3::Translator [private]
d_langUsedCVC3::Translator [private]
d_osdumpCVC3::Translator [private]
d_osdumpFileCVC3::Translator [private]
d_real2intCVC3::Translator [private]
d_realUsedCVC3::Translator [private]
d_replaceSymbolsCVC3::Translator [private]
d_sourceCVC3::Translator [private]
d_statusCVC3::Translator [private]
d_theoryArithCVC3::Translator [private]
d_theoryArrayCVC3::Translator [private]
d_theoryBitvectorCVC3::Translator [private]
d_theoryCoreCVC3::Translator [private]
d_theoryDatatypeCVC3::Translator [private]
d_theoryQuantCVC3::Translator [private]
d_theoryRecordsCVC3::Translator [private]
d_theorySimulateCVC3::Translator [private]
d_theoryUFCVC3::Translator [private]
d_tmpFileCVC3::Translator [private]
d_translateCVC3::Translator [private]
d_UFIDL_okCVC3::Translator [private]
d_unknownCVC3::Translator [private]
d_zeroVarCVC3::Translator [private]
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::Translator [private]
finish()CVC3::Translator
fixConstName(const std::string &s)CVC3::Translator
preprocess(const Expr &e, ExprMap< Expr > &cache)CVC3::Translator [private]
preprocess2(const Expr &e, ExprMap< Expr > &cache)CVC3::Translator [private]
preprocess2Rec(const Expr &e, ExprMap< Expr > &cache, Type desiredType)CVC3::Translator [private]
preprocessRec(const Expr &e, ExprMap< Expr > &cache)CVC3::Translator [private]
printArrayExpr(ExprStream &os, const Expr &e)CVC3::Translator
processType(const Expr &e)CVC3::Translator [private]
quoteAnnotation(const std::string &s)CVC3::Translator
setBenchName(std::string name)CVC3::Translator [inline]
setCategory(std::string category)CVC3::Translator [inline]
setSource(std::string source)CVC3::Translator [inline]
setStatus(std::string status)CVC3::Translator [inline]
setTheoryArith(TheoryArith *theoryArith)CVC3::Translator [inline]
setTheoryArray(TheoryArray *theoryArray)CVC3::Translator [inline]
setTheoryBitvector(TheoryBitvector *theoryBitvector)CVC3::Translator [inline]
setTheoryCore(TheoryCore *theoryCore)CVC3::Translator [inline]
setTheoryDatatype(TheoryDatatype *theoryDatatype)CVC3::Translator [inline]
setTheoryQuant(TheoryQuant *theoryQuant)CVC3::Translator [inline]
setTheoryRecords(TheoryRecords *theoryRecords)CVC3::Translator [inline]
setTheorySimulate(TheorySimulate *theorySimulate)CVC3::Translator [inline]
setTheoryUF(TheoryUF *theoryUF)CVC3::Translator [inline]
source()CVC3::Translator [inline]
start(const std::string &dumpFile)CVC3::Translator
status()CVC3::Translator [inline]
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