| containsArray(const Expr &e) | CVC3::Translator | [private] |
| d_arithUsed | 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_convertToDiff | CVC3::Translator | [private] |
| d_dump | CVC3::Translator | [private] |
| d_dumpExprs | CVC3::Translator | [private] |
| d_dumpFileOpen | CVC3::Translator | [private] |
| d_em | CVC3::Translator | [private] |
| d_expResult | 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) | CVC3::Translator | |
| zeroVar() | CVC3::Translator | |
| ~Translator() | CVC3::Translator | [inline, virtual] |