containsArray(const Expr &e) | CVC3::Translator | [private] |
d_arithUsed | CVC3::Translator | [private] |
d_arrayConvertMap | CVC3::Translator | [private] |
d_arrayType | CVC3::Translator | [private] |
d_ax | CVC3::Translator | [private] |
d_category | CVC3::Translator | [private] |
d_combineAssump | CVC3::Translator | [private] |
d_convertArith | CVC3::Translator | [private] |
d_convertArray | CVC3::Translator | [private] |
d_convertToBV | CVC3::Translator | [private] |
d_convertToDiff | CVC3::Translator | [private] |
d_dump | CVC3::Translator | [private] |
d_dumpExprs | CVC3::Translator | [private] |
d_dumpFileOpen | CVC3::Translator | [private] |
d_elementType | CVC3::Translator | [private] |
d_em | CVC3::Translator | [private] |
d_equalities | CVC3::Translator | [private] |
d_expResult | CVC3::Translator | [private] |
d_indexType | CVC3::Translator | [private] |
d_intConstUsed | CVC3::Translator | [private] |
d_intIntArray | CVC3::Translator | [private] |
d_intIntRealArray | CVC3::Translator | [private] |
d_intRealArray | CVC3::Translator | [private] |
d_intUsed | CVC3::Translator | [private] |
d_iteLiftArith | CVC3::Translator | [private] |
d_langUsed | CVC3::Translator | [private] |
d_osdump | CVC3::Translator | [private] |
d_osdumpFile | CVC3::Translator | [private] |
d_real2int | CVC3::Translator | [private] |
d_realUsed | CVC3::Translator | [private] |
d_theoryArith | CVC3::Translator | [private] |
d_theoryArray | CVC3::Translator | [private] |
d_theoryBitvector | CVC3::Translator | [private] |
d_theoryCore | CVC3::Translator | [private] |
d_theoryDatatype | CVC3::Translator | [private] |
d_theoryQuant | CVC3::Translator | [private] |
d_theoryRecords | CVC3::Translator | [private] |
d_theorySimulate | CVC3::Translator | [private] |
d_theoryUF | CVC3::Translator | [private] |
d_tmpFile | CVC3::Translator | [private] |
d_translate | CVC3::Translator | [private] |
d_UFIDL_ok | CVC3::Translator | [private] |
d_unknown | CVC3::Translator | [private] |
d_zeroVar | CVC3::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 | |
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] |
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] |
start(const std::string &dumpFile) | CVC3::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) | CVC3::Translator | |
zeroVar() | CVC3::Translator | |
~Translator() | CVC3::Translator | |