CVC3
2.4.1
|
#include <translator.h>
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.
string Translator::fileToSMTLIBIdentifier | ( | const std::string & | filename | ) | [private] |
Definition at line 45 of file translator.cpp.
Referenced by start().
Definition at line 72 of file translator.cpp.
References CVC3::ExprMap::find(), CVC3::ExprMap::end(), CVC3::Expr::isPropAtom(), CVC3::Expr::containsTermITE(), CVC3::Theorem::getRHS(), CVC3::Expr::isClosure(), CVC3::Expr::getBody(), CVC3::Expr::getKind(), CVC3::Expr::getVars(), CVC3::Expr::arity(), CVC3::Expr::getOp(), RATIONAL_EXPR, CVC3::Expr::getRational(), CVC3::Rational::isInteger(), FatalAssert, CVC3::pow(), CVC3::READ, UCONST, CVC3::Expr::getName(), CVC3::WRITE, APPLY, CVC3::Expr::getOpKind(), LAMBDA, CVC3::Expr::getOpExpr(), CVC3::Expr::getKids(), EQ, CVC3::UMINUS, CVC3::BVUMINUS, CVC3::DIVIDE, CVC3::isRational(), CVC3::MINUS, CVC3::BVSUB, CVC3::PLUS, CVC3::BVPLUS, CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::MULT, CVC3::BVMULT, CVC3::POW, CVC3::Rational::getNumerator(), CVC3::LT, CVC3::BVSLT, CVC3::GT, CVC3::LE, CVC3::BVSLE, CVC3::GE, CVC3::INTDIV, CVC3::MOD, ITE, CVC3::Expr::iteExpr(), DebugAssert, CVC3::isInt(), CVC3::Expr::getType(), CVC3::Expr::isVar(), CVC3::NOT_USED, CVC3::TERMS_ONLY, CVC3::IS_INTEGER, CVC3::NONLINEAR, CVC3::LINEAR, CVC3::Expr::isRational(), CVC3::DIFF_ONLY, and NOT.
Definition at line 549 of file translator.cpp.
References CVC3::Expr::toString(), and std::endl().
Referenced by finish().
Expr Translator::preprocess2Rec | ( | const Expr & | e, |
ExprMap< Expr > & | cache, | ||
Type | desiredType | ||
) | [private] |
Definition at line 563 of file translator.cpp.
References TRACE, CVC3::ExprMap::find(), CVC3::ExprMap::end(), CVC3::Type::isNull(), CVC3::Expr::isClosure(), CVC3::Expr::getBody(), CVC3::Expr::getKind(), CVC3::Expr::getVars(), CVC3::Expr::getType(), EQ, CVC3::LT, CVC3::GT, CVC3::LE, CVC3::GE, CVC3::Expr::toString(), ITE, CVC3::UMINUS, CVC3::PLUS, CVC3::MINUS, CVC3::MULT, CVC3::DIVIDE, CVC3::Expr::isApply(), CVC3::Expr::getOpExpr(), CVC3::Type::getExpr(), ANY_TYPE, CVC3::WRITE, CVC3::Expr::arity(), CVC3::Expr::getOp(), RATIONAL_EXPR, CVC3::REAL_CONST, CVC3::NOT_USED, CVC3::LINEAR, CVC3::SMTLIB_V2_LANG, FatalAssert, DebugAssert, CVC3::Expr::isRational(), CVC3::Expr::getRational(), CVC3::READ, CVC3::isInt(), and CVC3::isReal().
Definition at line 783 of file translator.cpp.
References CVC3::Expr::toString(), and std::endl().
Referenced by finish().
bool Translator::containsArray | ( | const Expr & | e | ) | [private] |
Definition at line 799 of file translator.cpp.
References CVC3::Expr::getKind(), CVC3::ARRAY, CVC3::Expr::begin(), and CVC3::Expr::end().
Referenced by dump().
Definition at line 1063 of file translator.cpp.
References CVC3::Expr::getKind(), TYPEDECL, CVC3::INT, d_convertToBV, d_theoryBitvector, CVC3::TheoryBitvector::newBitvectorType(), CVC3::Type::getExpr(), d_theoryCore, CVC3::TheoryCore::getFlags(), d_elementType, d_intUsed, CVC3::REAL, d_real2int, d_theoryArith, CVC3::TheoryArith::intType(), d_realUsed, CVC3::SUBRANGE, d_unknown, CVC3::ARRAY, d_ax, d_arrayType, DebugAssert, CVC3::isInt(), d_intIntArray, CVC3::isReal(), d_intRealArray, CVC3::isArray(), d_intIntRealArray, CVC3::BITVECTOR, CVC3::Theory::theoryOf(), CVC3::Theory::setUsed(), CVC3::Expr::arity(), and CVC3::Expr::getOp().
Referenced by finish().
bool Translator::start | ( | const std::string & | dumpFile | ) |
Definition at line 845 of file translator.cpp.
References d_translate, d_em, CVC3::ExprManager::getOutputLang(), CVC3::SMTLIB_LANG, d_dump, d_osdump, d_osdumpFile, d_dumpFileOpen, d_tmpFile, fileToSMTLIBIdentifier(), std::endl(), and CVC3::SPASS_LANG.
void Translator::dump | ( | const Expr & | e, |
bool | dumpOnly = false |
||
) |
Dump the expression in the current output language
dumpOnly | When 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 DebugAssert, d_dump, d_translate, d_convertArray, CVC3::Expr::getKind(), CONST, CVC3::Expr::arity(), CVC3::ARRAY, containsArray(), ARROW, and d_dumpExprs.
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 QUERY, d_dumpExprs, and d_translate.
void Translator::dumpQueryResult | ( | QueryResult | qres | ) |
Definition at line 986 of file translator.cpp.
References d_translate, d_em, CVC3::ExprManager::getOutputLang(), CVC3::SMTLIB_LANG, d_osdump, CVC3::UNSATISFIABLE, std::endl(), CVC3::SATISFIABLE, CVC3::SMTLIB_V2_LANG, and CVC3::SPASS_LANG.
void Translator::finish | ( | ) |
Definition at line 1145 of file translator.cpp.
References d_translate, d_em, CVC3::ExprManager::getOutputLang(), CVC3::SPASS_LANG, d_osdump, d_expResult, status(), std::endl(), d_dumpExprs, CVC3::Expr::getKind(), TYPE, CONST, CVC3::Expr::arity(), BOOLEAN, ARROW, ANNOTATION, d_theoryCore, CVC3::TheoryCore::getFlags(), STRING_EXPR, CVC3::Expr::getString(), CVC3::isReal(), CVC3::Theory::getBaseType(), CVC3::SMTLIB_LANG, category(), d_indexType, CVC3::Theory::newTypeExpr(), d_elementType, d_arrayType, CVC3::arrayType(), ASSERT, preprocess(), CVC3::Expr::getType(), QUERY, CVC3::Expr::negate(), DebugAssert, processType(), d_convertToBV, ID, CVC3::ExprManager::newStringExpr(), d_zeroVar, CVC3::Type::getExpr(), d_unknown, d_equalities, UCONST, d_arrayConvertMap, CVC3::READ, CVC3::SMTLIB_V2_LANG, d_intUsed, d_realUsed, d_langUsed, CVC3::NOT_USED, CVC3::LINEAR, preprocess2(), d_arithUsed, d_intConstUsed, d_theoryRecords, CVC3::Theory::theoryUsed(), d_theorySimulate, d_theoryDatatype, d_ax, d_theoryBitvector, d_theoryUF, d_intIntArray, d_theoryQuant, d_theoryArray, d_convertArray, CVC3::NONLINEAR, CVC3::DIFF_ONLY, d_UFIDL_ok, source(), quoteAnnotation(), CVC3::PRESENTATION_LANG, d_dump, d_combineAssump, NOT, AND, RAW_LIST, d_replaceSymbols, d_dumpFileOpen, and d_osdumpFile.
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.
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.
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 d_category, and 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 | ) |
Definition at line 1804 of file translator.cpp.
References d_em, CVC3::ExprManager::getOutputLang(), CVC3::SMTLIB_LANG, d_replaceSymbols, Hash::hash_map::find(), and Hash::hash_map::end().
Referenced by CVC3::TheoryCore::printSmtLibShared(), CVC3::TheoryCore::print(), and CVC3::TheoryUF::printSmtLibShared().
const string Translator::escapeSymbol | ( | const std::string & | s | ) |
Definition at line 1816 of file translator.cpp.
References d_em, CVC3::ExprManager::getOutputLang(), and CVC3::SMTLIB_V2_LANG.
Referenced by CVC3::TheoryCore::printSmtLibShared(), and CVC3::TheoryCore::print().
const string Translator::quoteAnnotation | ( | const std::string & | s | ) |
Definition at line 1830 of file translator.cpp.
Referenced by CVC3::TheoryCore::print(), and finish().
bool Translator::printArrayExpr | ( | ExprStream & | os, |
const Expr & | e | ||
) |
Returns true if expression has been printed.
If false is returned, array theory should print expression as usual
Definition at line 1850 of file translator.cpp.
References CVC3::Expr::getKind(), CVC3::ARRAY, d_convertArray, ARROW, d_em, CVC3::ExprManager::getOutputLang(), CVC3::SMTLIB_V2_LANG, DebugAssert, CVC3::Expr::arity(), CVC3::push(), CVC3::space(), CVC3::nodag(), CVC3::pop(), CVC3::SMTLIB_LANG, TYPEDECL, CVC3::isInt(), d_intIntArray, CVC3::isReal(), d_intRealArray, CVC3::isArray(), d_intIntRealArray, CVC3::BITVECTOR, d_theoryBitvector, CVC3::TheoryBitvector::getBitvectorTypeParam(), d_unknown, CVC3::READ, UCONST, CVC3::ExprManager::newSymbolExpr(), CVC3::Expr::getName(), UFUNC, CVC3::WRITE, and CVC3::ARRAY_LITERAL.
Expr Translator::zeroVar | ( | ) |
Definition at line 1943 of file translator.cpp.
References d_zeroVar, d_convertToDiff, d_theoryCore, CVC3::Theory::newVar(), d_theoryArith, CVC3::TheoryArith::intType(), CVC3::Type::getExpr(), and CVC3::TheoryArith::realType().
ExprManager* CVC3::Translator::d_em [private] |
Definition at line 61 of file translator.h.
Referenced by start(), dumpQueryResult(), finish(), fixConstName(), escapeSymbol(), and printArrayExpr().
const bool& CVC3::Translator::d_translate [private] |
Definition at line 62 of file translator.h.
Referenced by start(), dump(), dumpAssertion(), dumpQuery(), dumpQueryResult(), and finish().
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().
bool CVC3::Translator::d_iteLiftArith [private] |
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 setCategory(), and category().
bool CVC3::Translator::d_convertArray [private] |
Definition at line 69 of file translator.h.
Referenced by dump(), finish(), and printArrayExpr().
bool CVC3::Translator::d_combineAssump [private] |
Definition at line 70 of file translator.h.
Referenced by finish().
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 start(), dumpQueryResult(), and finish().
std::ofstream CVC3::Translator::d_osdumpFile [private] |
Definition at line 84 of file translator.h.
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.
bool CVC3::Translator::d_dumpFileOpen [private] |
Definition at line 86 of file translator.h.
bool CVC3::Translator::d_intIntArray [private] |
Definition at line 88 of file translator.h.
Referenced by processType(), finish(), and printArrayExpr().
bool CVC3::Translator::d_intRealArray [private] |
Definition at line 88 of file translator.h.
Referenced by processType(), and printArrayExpr().
bool CVC3::Translator::d_intIntRealArray [private] |
Definition at line 88 of file translator.h.
Referenced by processType(), and printArrayExpr().
bool CVC3::Translator::d_ax [private] |
Definition at line 88 of file translator.h.
Referenced by processType(), and finish().
bool CVC3::Translator::d_unknown [private] |
Definition at line 88 of file translator.h.
Referenced by processType(), finish(), and printArrayExpr().
bool CVC3::Translator::d_realUsed [private] |
Definition at line 89 of file translator.h.
Referenced by processType(), and finish().
bool CVC3::Translator::d_intUsed [private] |
Definition at line 90 of file translator.h.
Referenced by processType(), and finish().
bool CVC3::Translator::d_intConstUsed [private] |
Definition at line 91 of file translator.h.
Referenced by finish().
ArithLang CVC3::Translator::d_langUsed [private] |
Definition at line 92 of file translator.h.
Referenced by finish().
bool CVC3::Translator::d_UFIDL_ok [private] |
Definition at line 93 of file translator.h.
Referenced by finish().
bool CVC3::Translator::d_arithUsed [private] |
Definition at line 94 of file translator.h.
Referenced by finish().
Expr* CVC3::Translator::d_zeroVar [private] |
Definition at line 96 of file translator.h.
int CVC3::Translator::d_convertToBV [private] |
Definition at line 97 of file translator.h.
Referenced by processType(), and finish().
TheoryCore* CVC3::Translator::d_theoryCore [private] |
Definition at line 99 of file translator.h.
Referenced by processType(), finish(), zeroVar(), and setTheoryCore().
TheoryUF* CVC3::Translator::d_theoryUF [private] |
Definition at line 100 of file translator.h.
Referenced by finish(), and setTheoryUF().
TheoryArith* CVC3::Translator::d_theoryArith [private] |
Definition at line 101 of file translator.h.
Referenced by processType(), zeroVar(), and setTheoryArith().
TheoryArray* CVC3::Translator::d_theoryArray [private] |
Definition at line 102 of file translator.h.
Referenced by finish(), and setTheoryArray().
TheoryQuant* CVC3::Translator::d_theoryQuant [private] |
Definition at line 103 of file translator.h.
Referenced by finish(), and setTheoryQuant().
TheoryRecords* CVC3::Translator::d_theoryRecords [private] |
Definition at line 104 of file translator.h.
Referenced by finish(), and setTheoryRecords().
TheorySimulate* CVC3::Translator::d_theorySimulate [private] |
Definition at line 105 of file translator.h.
Referenced by finish(), and setTheorySimulate().
Definition at line 106 of file translator.h.
Referenced by processType(), finish(), printArrayExpr(), and setTheoryBitvector().
TheoryDatatype* CVC3::Translator::d_theoryDatatype [private] |
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 Translator(), ~Translator(), and finish().
Type* CVC3::Translator::d_indexType [private] |
Definition at line 112 of file translator.h.
Referenced by finish().
Type* CVC3::Translator::d_elementType [private] |
Definition at line 113 of file translator.h.
Referenced by processType(), and finish().
Type* CVC3::Translator::d_arrayType [private] |
Definition at line 114 of file translator.h.
Referenced by processType(), and finish().
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 setBenchName(), and benchName().
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().