CVC3
2.4.1
|
#include <translator.h>
Classes | |
class | HashString |
Public Member Functions | |
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) | |
~Translator () | |
bool | start (const std::string &dumpFile) |
void | dump (const Expr &e, bool dumpOnly=false) |
bool | dumpAssertion (const Expr &e) |
bool | dumpQuery (const Expr &e) |
void | dumpQueryResult (QueryResult qres) |
void | finish () |
void | setTheoryCore (TheoryCore *theoryCore) |
void | setTheoryUF (TheoryUF *theoryUF) |
void | setTheoryArith (TheoryArith *theoryArith) |
void | setTheoryArray (TheoryArray *theoryArray) |
void | setTheoryQuant (TheoryQuant *theoryQuant) |
void | setTheoryRecords (TheoryRecords *theoryRecords) |
void | setTheorySimulate (TheorySimulate *theorySimulate) |
void | setTheoryBitvector (TheoryBitvector *theoryBitvector) |
void | setTheoryDatatype (TheoryDatatype *theoryDatatype) |
void | setBenchName (std::string name) |
std::string | benchName () |
void | setStatus (std::string status) |
std::string | status () |
void | setSource (std::string source) |
std::string | source () |
void | setCategory (std::string category) |
std::string | category () |
const std::string | fixConstName (const std::string &s) |
const std::string | escapeSymbol (const std::string &s) |
const std::string | quoteAnnotation (const std::string &s) |
bool | printArrayExpr (ExprStream &os, const Expr &e) |
Returns true if expression has been printed. More... | |
Expr | zeroVar () |
Private Member Functions | |
std::string | fileToSMTLIBIdentifier (const std::string &filename) |
Expr | preprocessRec (const Expr &e, ExprMap< Expr > &cache) |
Expr | preprocess (const Expr &e, ExprMap< Expr > &cache) |
Expr | preprocess2Rec (const Expr &e, ExprMap< Expr > &cache, Type desiredType) |
Expr | preprocess2 (const Expr &e, ExprMap< Expr > &cache) |
bool | containsArray (const Expr &e) |
Expr | processType (const Expr &e) |
Definition at line 60 of file 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.
|
private |
Definition at line 45 of file translator.cpp.
Referenced by start().
Definition at line 72 of file translator.cpp.
References APPLY, CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BVMULT, CVC3::BVPLUS, CVC3::BVSLE, CVC3::BVSLT, CVC3::BVSUB, CVC3::BVUMINUS, CVC3::Expr::containsTermITE(), DebugAssert, CVC3::DIFF_ONLY, CVC3::DIVIDE, CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), EQ, FatalAssert, CVC3::ExprMap< Data >::find(), CVC3::GE, CVC3::Expr::getBody(), CVC3::Expr::getKids(), CVC3::Expr::getKind(), CVC3::Expr::getName(), CVC3::Rational::getNumerator(), CVC3::Expr::getOp(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getRational(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Expr::getVars(), CVC3::GT, CVC3::INTDIV, CVC3::IS_INTEGER, CVC3::Expr::isClosure(), CVC3::isInt(), CVC3::Rational::isInteger(), CVC3::Expr::isPropAtom(), CVC3::isRational(), CVC3::Expr::isRational(), CVC3::Expr::isVar(), ITE, CVC3::Expr::iteExpr(), LAMBDA, CVC3::LE, CVC3::LINEAR, CVC3::LT, CVC3::MINUS, CVC3::MOD, CVC3::MULT, CVC3::NONLINEAR, NOT, CVC3::NOT_USED, CVC3::PLUS, CVC3::POW, CVC3::pow(), RATIONAL_EXPR, CVC3::READ, CVC3::TERMS_ONLY, UCONST, CVC3::UMINUS, and CVC3::WRITE.
Definition at line 549 of file translator.cpp.
References std::endl(), and CVC3::Expr::toString().
Referenced by finish().
|
private |
Definition at line 563 of file translator.cpp.
References ANY_TYPE, CVC3::Expr::arity(), DebugAssert, CVC3::DIVIDE, CVC3::ExprMap< Data >::end(), EQ, FatalAssert, CVC3::ExprMap< Data >::find(), CVC3::GE, CVC3::Expr::getBody(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::Expr::getOpExpr(), CVC3::Expr::getRational(), CVC3::Expr::getType(), CVC3::Expr::getVars(), CVC3::GT, CVC3::Expr::isApply(), CVC3::Expr::isClosure(), CVC3::isInt(), CVC3::Type::isNull(), CVC3::Expr::isRational(), CVC3::isReal(), ITE, CVC3::LE, CVC3::LINEAR, CVC3::LT, CVC3::MINUS, CVC3::MULT, CVC3::NOT_USED, CVC3::PLUS, RATIONAL_EXPR, CVC3::READ, CVC3::REAL_CONST, CVC3::SMTLIB_V2_LANG, CVC3::Expr::toString(), TRACE, CVC3::UMINUS, and CVC3::WRITE.
Definition at line 783 of file translator.cpp.
References std::endl(), and CVC3::Expr::toString().
Referenced by finish().
|
private |
Definition at line 799 of file translator.cpp.
References CVC3::ARRAY, CVC3::Expr::begin(), CVC3::Expr::end(), and CVC3::Expr::getKind().
Referenced by dump().
Definition at line 1063 of file translator.cpp.
References CVC3::Expr::arity(), CVC3::ARRAY, CVC3::BITVECTOR, d_arrayType, d_ax, d_convertToBV, d_elementType, d_intIntArray, d_intIntRealArray, d_intRealArray, d_intUsed, d_real2int, d_realUsed, d_theoryArith, d_theoryBitvector, d_theoryCore, d_unknown, DebugAssert, CVC3::Type::getExpr(), CVC3::TheoryCore::getFlags(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::INT, CVC3::TheoryArith::intType(), CVC3::isArray(), CVC3::isInt(), CVC3::isReal(), CVC3::TheoryBitvector::newBitvectorType(), CVC3::REAL, CVC3::Theory::setUsed(), CVC3::SUBRANGE, CVC3::Theory::theoryOf(), and TYPEDECL.
Referenced by finish().
bool Translator::start | ( | const std::string & | dumpFile) |
Definition at line 845 of file translator.cpp.
References d_dump, d_dumpFileOpen, d_em, d_osdump, d_osdumpFile, d_tmpFile, d_translate, std::endl(), fileToSMTLIBIdentifier(), CVC3::ExprManager::getOutputLang(), CVC3::SMTLIB_LANG, 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 CVC3::Expr::arity(), CVC3::ARRAY, ARROW, CONST, containsArray(), d_convertArray, d_dump, d_dumpExprs, d_translate, DebugAssert, and CVC3::Expr::getKind().
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 d_dumpExprs, d_translate, and QUERY.
void Translator::dumpQueryResult | ( | QueryResult | qres) |
Definition at line 986 of file translator.cpp.
References d_em, d_osdump, d_translate, std::endl(), CVC3::ExprManager::getOutputLang(), CVC3::SATISFIABLE, CVC3::SMTLIB_LANG, CVC3::SMTLIB_V2_LANG, CVC3::SPASS_LANG, and CVC3::UNSATISFIABLE.
void Translator::finish | ( | ) |
Definition at line 1145 of file translator.cpp.
References AND, ANNOTATION, CVC3::Expr::arity(), CVC3::arrayType(), ARROW, ASSERT, BOOLEAN, category(), CONST, d_arithUsed, d_arrayConvertMap, d_arrayType, d_ax, d_combineAssump, d_convertArray, d_convertToBV, d_dump, d_dumpExprs, d_dumpFileOpen, d_elementType, d_em, d_equalities, d_expResult, d_indexType, d_intConstUsed, d_intIntArray, d_intUsed, d_langUsed, d_osdump, d_osdumpFile, d_realUsed, d_replaceSymbols, d_theoryArray, d_theoryBitvector, d_theoryCore, d_theoryDatatype, d_theoryQuant, d_theoryRecords, d_theorySimulate, d_theoryUF, d_translate, d_UFIDL_ok, d_unknown, d_zeroVar, DebugAssert, CVC3::DIFF_ONLY, std::endl(), CVC3::Theory::getBaseType(), CVC3::Type::getExpr(), CVC3::TheoryCore::getFlags(), CVC3::Expr::getKind(), CVC3::ExprManager::getOutputLang(), CVC3::Expr::getString(), CVC3::Expr::getType(), ID, CVC3::isReal(), CVC3::LINEAR, CVC3::Expr::negate(), CVC3::ExprManager::newStringExpr(), CVC3::Theory::newTypeExpr(), CVC3::NONLINEAR, NOT, CVC3::NOT_USED, preprocess(), preprocess2(), CVC3::PRESENTATION_LANG, processType(), QUERY, quoteAnnotation(), RAW_LIST, CVC3::READ, CVC3::SMTLIB_LANG, CVC3::SMTLIB_V2_LANG, source(), CVC3::SPASS_LANG, status(), STRING_EXPR, CVC3::Theory::theoryUsed(), TYPE, and UCONST.
|
inline |
Definition at line 166 of file translator.h.
References d_theoryCore.
|
inline |
Definition at line 167 of file translator.h.
References d_theoryUF.
|
inline |
Definition at line 168 of file translator.h.
References d_theoryArith.
|
inline |
Definition at line 169 of file translator.h.
References d_theoryArray.
|
inline |
Definition at line 170 of file translator.h.
References d_theoryQuant.
|
inline |
Definition at line 171 of file translator.h.
References d_theoryRecords.
|
inline |
Definition at line 172 of file translator.h.
References d_theorySimulate.
|
inline |
Definition at line 173 of file translator.h.
References d_theoryBitvector.
|
inline |
Definition at line 174 of file translator.h.
References d_theoryDatatype.
|
inline |
Definition at line 176 of file translator.h.
References d_benchName.
|
inline |
Definition at line 177 of file translator.h.
References d_benchName.
|
inline |
Definition at line 178 of file translator.h.
|
inline |
Definition at line 179 of file translator.h.
References d_status.
Referenced by finish(), and setStatus().
|
inline |
Definition at line 180 of file translator.h.
|
inline |
Definition at line 181 of file translator.h.
References d_source.
Referenced by finish(), and setSource().
|
inline |
Definition at line 182 of file translator.h.
References category(), and d_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, d_replaceSymbols, CVC3::ExprManager::getOutputLang(), and CVC3::SMTLIB_LANG.
Referenced by CVC3::TheoryCore::print(), CVC3::TheoryUF::printSmtLibShared(), and CVC3::TheoryCore::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::print(), and CVC3::TheoryCore::printSmtLibShared().
const string Translator::quoteAnnotation | ( | const std::string & | s) |
Definition at line 1830 of file translator.cpp.
Referenced by finish(), and CVC3::TheoryCore::print().
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::arity(), CVC3::ARRAY, CVC3::ARRAY_LITERAL, ARROW, CVC3::BITVECTOR, d_convertArray, d_em, d_intIntArray, d_intIntRealArray, d_intRealArray, d_theoryBitvector, d_unknown, DebugAssert, CVC3::TheoryBitvector::getBitvectorTypeParam(), CVC3::Expr::getKind(), CVC3::Expr::getName(), CVC3::ExprManager::getOutputLang(), CVC3::isArray(), CVC3::isInt(), CVC3::isReal(), CVC3::ExprManager::newSymbolExpr(), CVC3::nodag(), CVC3::pop(), CVC3::push(), CVC3::READ, CVC3::SMTLIB_LANG, CVC3::SMTLIB_V2_LANG, CVC3::space(), TYPEDECL, UCONST, UFUNC, and CVC3::WRITE.
Expr Translator::zeroVar | ( | ) |
Definition at line 1943 of file translator.cpp.
References d_convertToDiff, d_theoryArith, d_theoryCore, d_zeroVar, CVC3::Type::getExpr(), CVC3::TheoryArith::intType(), CVC3::Theory::newVar(), and CVC3::TheoryArith::realType().
|
private |
Definition at line 61 of file translator.h.
Referenced by dumpQueryResult(), escapeSymbol(), finish(), fixConstName(), printArrayExpr(), and start().
|
private |
Definition at line 62 of file translator.h.
Referenced by dump(), dumpAssertion(), dumpQuery(), dumpQueryResult(), finish(), and start().
|
private |
Definition at line 63 of file translator.h.
Referenced by processType().
|
private |
Definition at line 64 of file translator.h.
|
private |
Definition at line 65 of file translator.h.
Referenced by zeroVar().
|
private |
Definition at line 66 of file translator.h.
|
private |
Definition at line 67 of file translator.h.
Referenced by finish().
|
private |
Definition at line 68 of file translator.h.
Referenced by category(), and setCategory().
|
private |
Definition at line 69 of file translator.h.
Referenced by dump(), finish(), and printArrayExpr().
|
private |
Definition at line 70 of file translator.h.
Referenced by finish().
|
private |
Definition at line 80 of file translator.h.
Referenced by finish(), and fixConstName().
|
private |
The log file for top-level API calls in the CVC3 input language.
Definition at line 83 of file translator.h.
Referenced by dumpQueryResult(), finish(), and start().
|
private |
Definition at line 84 of file translator.h.
|
private |
Definition at line 85 of file translator.h.
Referenced by start().
|
private |
Definition at line 86 of file translator.h.
|
private |
Definition at line 86 of file translator.h.
|
private |
Definition at line 88 of file translator.h.
Referenced by finish(), printArrayExpr(), and processType().
|
private |
Definition at line 88 of file translator.h.
Referenced by printArrayExpr(), and processType().
|
private |
Definition at line 88 of file translator.h.
Referenced by printArrayExpr(), and processType().
|
private |
Definition at line 88 of file translator.h.
Referenced by finish(), and processType().
|
private |
Definition at line 88 of file translator.h.
Referenced by finish(), printArrayExpr(), and processType().
|
private |
Definition at line 89 of file translator.h.
Referenced by finish(), and processType().
|
private |
Definition at line 90 of file translator.h.
Referenced by finish(), and processType().
|
private |
Definition at line 91 of file translator.h.
Referenced by finish().
|
private |
Definition at line 92 of file translator.h.
Referenced by finish().
|
private |
Definition at line 93 of file translator.h.
Referenced by finish().
|
private |
Definition at line 94 of file translator.h.
Referenced by finish().
|
private |
Definition at line 96 of file translator.h.
|
private |
Definition at line 97 of file translator.h.
Referenced by finish(), and processType().
|
private |
Definition at line 99 of file translator.h.
Referenced by finish(), processType(), setTheoryCore(), and zeroVar().
|
private |
Definition at line 100 of file translator.h.
Referenced by finish(), and setTheoryUF().
|
private |
Definition at line 101 of file translator.h.
Referenced by processType(), setTheoryArith(), and zeroVar().
|
private |
Definition at line 102 of file translator.h.
Referenced by finish(), and setTheoryArray().
|
private |
Definition at line 103 of file translator.h.
Referenced by finish(), and setTheoryQuant().
|
private |
Definition at line 104 of file translator.h.
Referenced by finish(), and setTheoryRecords().
|
private |
Definition at line 105 of file translator.h.
Referenced by finish(), and setTheorySimulate().
|
private |
Definition at line 106 of file translator.h.
Referenced by finish(), printArrayExpr(), processType(), and setTheoryBitvector().
|
private |
Definition at line 107 of file translator.h.
Referenced by finish(), and setTheoryDatatype().
|
private |
Definition at line 109 of file translator.h.
Referenced by dump(), dumpAssertion(), dumpQuery(), and finish().
|
private |
Definition at line 111 of file translator.h.
Referenced by finish(), Translator(), and ~Translator().
|
private |
Definition at line 112 of file translator.h.
Referenced by finish().
|
private |
Definition at line 113 of file translator.h.
Referenced by finish(), and processType().
|
private |
Definition at line 114 of file translator.h.
Referenced by finish(), and processType().
|
private |
Definition at line 115 of file translator.h.
Referenced by finish().
|
private |
Definition at line 118 of file translator.h.
Referenced by benchName(), and setBenchName().
|
private |
Definition at line 120 of file translator.h.
Referenced by setStatus(), and status().
|
private |
Definition at line 122 of file translator.h.
Referenced by setSource(), and source().