CVC3
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