CVC3  2.4.1
translator.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file translator.h
4  * \brief An exception to be thrown by the smtlib translator.
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Sat Jun 25 18:03:09 2005
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #ifndef _cvc3__translator_h_
23 #define _cvc3__translator_h_
24 
25 #include <string>
26 #include <fstream>
27 #include <vector>
28 #include <map>
29 #include "queryresult.h"
30 #include "compat_hash_map.h"
31 
32 namespace CVC3 {
33 
34 class Expr;
35 template <class Data> class ExprMap;
36 class Type;
37 class ExprManager;
38 class ExprStream;
39 class TheoryCore;
40 class TheoryUF;
41 class TheoryArith;
42 class TheoryArray;
43 class TheoryQuant;
44 class TheoryRecords;
45 class TheorySimulate;
46 class TheoryBitvector;
47 class TheoryDatatype;
48 template <class Data> class ExprMap;
49 
50 //! Used to keep track of which subset of arith is being used
51 typedef enum {
52  NOT_USED = 0,
57 } ArithLang;
58 
59 //All the translation code should go here
60 class Translator {
62  const bool& d_translate;
63  const bool& d_real2int;
64  const bool& d_convertArith;
65  const std::string& d_convertToDiff;
67  const std::string& d_expResult;
68  std::string d_category;
71 
72  /** Private class for hashing strings; copied from ExprManager */
73  class HashString {
75  public:
76  size_t operator()(const std::string& s) const {
77  return h(const_cast<char*>(s.c_str()));
78  }
79  };
81 
82  //! The log file for top-level API calls in the CVC3 input language
83  std::ostream* d_osdump;
84  std::ofstream d_osdumpFile;
85  std::ifstream d_tmpFile;
87 
89  bool d_realUsed;
90  bool d_intUsed;
93  bool d_UFIDL_ok;
95 
98 
108 
109  std::vector<Expr> d_dumpExprs;
110 
111  std::map<std::string, Type>* d_arrayConvertMap;
115  std::vector<Expr> d_equalities;
116 
117  // Name of benchmark in SMT-LIB
118  std::string d_benchName;
119  // Status of benchmark in SMT-LIB
120  std::string d_status;
121  // Source of benchmark in SMT-LIB
122  std::string d_source;
123 
124  std::string fileToSMTLIBIdentifier(const std::string& filename);
125  Expr preprocessRec(const Expr& e, ExprMap<Expr>& cache);
126  Expr preprocess(const Expr& e, ExprMap<Expr>& cache);
127  Expr preprocess2Rec(const Expr& e, ExprMap<Expr>& cache, Type desiredType);
128  Expr preprocess2(const Expr& e, ExprMap<Expr>& cache);
129  bool containsArray(const Expr& e);
130  Expr processType(const Expr& e);
131 
132  /*
133  Expr spassPreprocess(const Expr& e, ExprMap<Expr>& mapping,
134  std::vector<Expr>& functions,
135  std::vector<Expr>& predicates);
136  */
137 
138 public:
139  // Constructors
141  const bool& translate,
142  const bool& real2int,
143  const bool& convertArith,
144  const std::string& convertToDiff,
145  bool iteLiftArith,
146  const std::string& expResult,
147  const std::string& category,
148  bool convertArray,
149  bool combineAssump,
150  int convertToBV);
151  ~Translator();
152 
153  bool start(const std::string& dumpFile);
154  /*! Dump the expression in the current output language
155  \param dumpOnly When false, the expression is output both when
156  translating and when producing a trace of commands. When true, the
157  expression is only output when producing a trace of commands
158  (i.e. ignored during translation).
159  */
160  void dump(const Expr& e, bool dumpOnly = false);
161  bool dumpAssertion(const Expr& e);
162  bool dumpQuery(const Expr& e);
163  void dumpQueryResult(QueryResult qres);
164  void finish();
165 
166  void setTheoryCore(TheoryCore* theoryCore) { d_theoryCore = theoryCore; }
167  void setTheoryUF(TheoryUF* theoryUF) { d_theoryUF = theoryUF; }
168  void setTheoryArith(TheoryArith* theoryArith) { d_theoryArith = theoryArith; }
169  void setTheoryArray(TheoryArray* theoryArray) { d_theoryArray = theoryArray; }
170  void setTheoryQuant(TheoryQuant* theoryQuant) { d_theoryQuant = theoryQuant; }
171  void setTheoryRecords(TheoryRecords* theoryRecords) { d_theoryRecords = theoryRecords; }
172  void setTheorySimulate(TheorySimulate* theorySimulate) { d_theorySimulate = theorySimulate; }
173  void setTheoryBitvector(TheoryBitvector* theoryBitvector) { d_theoryBitvector = theoryBitvector; }
174  void setTheoryDatatype(TheoryDatatype* theoryDatatype) { d_theoryDatatype = theoryDatatype; }
175 
176  void setBenchName(std::string name) { d_benchName = name; }
177  std::string benchName() { return d_benchName; }
178  void setStatus(std::string status) { d_status = status; }
179  std::string status() { return d_status; }
180  void setSource(std::string source) { d_source = source; }
181  std::string source() { return d_source; }
182  void setCategory(std::string category) { d_category = category; }
183  std::string category() { return d_category; }
184 
185  const std::string fixConstName(const std::string& s);
186  const std::string escapeSymbol(const std::string& s);
187  const std::string quoteAnnotation(const std::string& s);
188  //! Returns true if expression has been printed
189  /*! If false is returned, array theory should print expression as usual */
190  bool printArrayExpr(ExprStream& os, const Expr& e);
191 
192  Expr zeroVar();
193 
194 }; // end of class Translator
195 
196 } // end of namespace CVC3
197 
198 #endif
const std::string & d_expResult
Definition: translator.h:67
void setTheoryQuant(TheoryQuant *theoryQuant)
Definition: translator.h:170
const std::string fixConstName(const std::string &s)
void setTheoryRecords(TheoryRecords *theoryRecords)
Definition: translator.h:171
Data structure of expressions in CVC3.
Definition: expr.h:133
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 ...
Definition: theory_core.h:53
std::vector< Expr > d_equalities
Definition: translator.h:115
void dump(const Expr &e, bool dumpOnly=false)
Definition: translator.cpp:939
TheoryUF * d_theoryUF
Definition: translator.h:100
Expr processType(const Expr &e)
Type * d_arrayType
Definition: translator.h:114
std::string benchName()
Definition: translator.h:177
QueryResult
Definition: queryresult.h:32
void dumpQueryResult(QueryResult qres)
Definition: translator.cpp:986
std::ofstream d_osdumpFile
Definition: translator.h:84
bool containsArray(const Expr &e)
Definition: translator.cpp:799
size_t operator()(const std::string &s) const
Definition: translator.h:76
void setTheorySimulate(TheorySimulate *theorySimulate)
Definition: translator.h:172
This theory handles basic linear arithmetic.
Definition: theory_arith.h:70
bool start(const std::string &dumpFile)
Definition: translator.cpp:845
TheoryDatatype * d_theoryDatatype
Definition: translator.h:107
MS C++ specific settings.
Definition: type.h:42
"Theory" of symbolic simulation.
This theory handles uninterpreted functions.
Definition: theory_uf.h:48
Expr preprocess2Rec(const Expr &e, ExprMap< Expr > &cache, Type desiredType)
Definition: translator.cpp:563
std::string d_category
Definition: translator.h:68
const bool & d_translate
Definition: translator.h:62
void setTheoryDatatype(TheoryDatatype *theoryDatatype)
Definition: translator.h:174
TheoryArray * d_theoryArray
Definition: translator.h:102
void setTheoryArith(TheoryArith *theoryArith)
Definition: translator.h:168
enumerated type for result of queries
ArithLang
Used to keep track of which subset of arith is being used.
Definition: translator.h:51
void setTheoryBitvector(TheoryBitvector *theoryBitvector)
Definition: translator.h:173
std::string d_source
Definition: translator.h:122
Expr preprocessRec(const Expr &e, ExprMap< Expr > &cache)
Definition: translator.cpp:72
Expr * d_zeroVar
Definition: translator.h:96
bool d_combineAssump
Definition: translator.h:70
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: translator.cpp:808
std::string fileToSMTLIBIdentifier(const std::string &filename)
Definition: translator.cpp:45
void setBenchName(std::string name)
Definition: translator.h:176
This theory handles datatypes.
std::string d_status
Definition: translator.h:120
std::map< std::string, Type > * d_arrayConvertMap
Definition: translator.h:111
bool dumpAssertion(const Expr &e)
Definition: translator.cpp:970
void setSource(std::string source)
Definition: translator.h:180
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
TheoryArith * d_theoryArith
Definition: translator.h:101
Expression Manager.
Definition: expr_manager.h:58
void setTheoryArray(TheoryArray *theoryArray)
Definition: translator.h:169
This theory handles records.
void setStatus(std::string status)
Definition: translator.h:178
const std::string quoteAnnotation(const std::string &s)
TheoryRecords * d_theoryRecords
Definition: translator.h:104
This theory handles arrays.
Definition: theory_array.h:50
std::vector< Expr > d_dumpExprs
Definition: translator.h:109
std::string d_benchName
Definition: translator.h:118
std::string status()
Definition: translator.h:179
TheoryQuant * d_theoryQuant
Definition: translator.h:103
Expr preprocess(const Expr &e, ExprMap< Expr > &cache)
Definition: translator.cpp:549
Expr preprocess2(const Expr &e, ExprMap< Expr > &cache)
Definition: translator.cpp:783
ExprManager * d_em
Definition: translator.h:61
const std::string escapeSymbol(const std::string &s)
void setTheoryCore(TheoryCore *theoryCore)
Definition: translator.h:166
std::hash< char * > h
Definition: translator.h:74
void setTheoryUF(TheoryUF *theoryUF)
Definition: translator.h:167
std::ifstream d_tmpFile
Definition: translator.h:85
TheorySimulate * d_theorySimulate
Definition: translator.h:105
std::string category()
Definition: translator.h:183
Type * d_elementType
Definition: translator.h:113
const std::string & d_convertToDiff
Definition: translator.h:65
std::string source()
Definition: translator.h:181
Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)
bool dumpQuery(const Expr &e)
Definition: translator.cpp:978
Definition: expr.cpp:35
ArithLang d_langUsed
Definition: translator.h:92
bool d_intIntRealArray
Definition: translator.h:88
TheoryCore * d_theoryCore
Definition: translator.h:99
Type * d_indexType
Definition: translator.h:112
std::hash_map< std::string, std::string, HashString > d_replaceSymbols
Definition: translator.h:80
std::ostream * d_osdump
The log file for top-level API calls in the CVC3 input language.
Definition: translator.h:83
This theory handles quantifiers.
Definition: theory_quant.h:186
const bool & d_real2int
Definition: translator.h:63
void setCategory(std::string category)
Definition: translator.h:182
const bool & d_convertArith
Definition: translator.h:64
TheoryBitvector * d_theoryBitvector
Definition: translator.h:106