22 #ifndef _cvc3__translator_h_
23 #define _cvc3__translator_h_
35 template <
class Data>
class ExprMap;
46 class TheoryBitvector;
48 template <
class Data>
class ExprMap;
77 return h(const_cast<char*>(s.c_str()));
141 const bool& translate,
142 const bool& real2int,
143 const bool& convertArith,
144 const std::string& convertToDiff,
146 const std::string& expResult,
153 bool start(
const std::string& dumpFile);
160 void dump(
const Expr& e,
bool dumpOnly =
false);
const std::string & d_expResult
void setTheoryQuant(TheoryQuant *theoryQuant)
const std::string fixConstName(const std::string &s)
void setTheoryRecords(TheoryRecords *theoryRecords)
Data structure of expressions in CVC3.
bool printArrayExpr(ExprStream &os, const Expr &e)
Returns true if expression has been printed.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
std::vector< Expr > d_equalities
void dump(const Expr &e, bool dumpOnly=false)
Expr processType(const Expr &e)
void dumpQueryResult(QueryResult qres)
std::ofstream d_osdumpFile
bool containsArray(const Expr &e)
size_t operator()(const std::string &s) const
void setTheorySimulate(TheorySimulate *theorySimulate)
This theory handles basic linear arithmetic.
bool start(const std::string &dumpFile)
TheoryDatatype * d_theoryDatatype
MS C++ specific settings.
"Theory" of symbolic simulation.
This theory handles uninterpreted functions.
Expr preprocess2Rec(const Expr &e, ExprMap< Expr > &cache, Type desiredType)
void setTheoryDatatype(TheoryDatatype *theoryDatatype)
TheoryArray * d_theoryArray
void setTheoryArith(TheoryArith *theoryArith)
enumerated type for result of queries
ArithLang
Used to keep track of which subset of arith is being used.
void setTheoryBitvector(TheoryBitvector *theoryBitvector)
Expr preprocessRec(const Expr &e, ExprMap< Expr > &cache)
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)
std::string fileToSMTLIBIdentifier(const std::string &filename)
void setBenchName(std::string name)
This theory handles datatypes.
std::map< std::string, Type > * d_arrayConvertMap
bool dumpAssertion(const Expr &e)
void setSource(std::string source)
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
TheoryArith * d_theoryArith
void setTheoryArray(TheoryArray *theoryArray)
This theory handles records.
void setStatus(std::string status)
const std::string quoteAnnotation(const std::string &s)
TheoryRecords * d_theoryRecords
This theory handles arrays.
std::vector< Expr > d_dumpExprs
TheoryQuant * d_theoryQuant
Expr preprocess(const Expr &e, ExprMap< Expr > &cache)
Expr preprocess2(const Expr &e, ExprMap< Expr > &cache)
const std::string escapeSymbol(const std::string &s)
void setTheoryCore(TheoryCore *theoryCore)
void setTheoryUF(TheoryUF *theoryUF)
TheorySimulate * d_theorySimulate
const std::string & d_convertToDiff
Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)
bool dumpQuery(const Expr &e)
TheoryCore * d_theoryCore
std::hash_map< std::string, std::string, HashString > d_replaceSymbols
std::ostream * d_osdump
The log file for top-level API calls in the CVC3 input language.
This theory handles quantifiers.
void setCategory(std::string category)
const bool & d_convertArith
TheoryBitvector * d_theoryBitvector