CVC3

translator.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file translator.h
00004  * \brief An exception to be thrown by the smtlib translator.
00005  * 
00006  * Author: Clark Barrett
00007  * 
00008  * Created: Sat Jun 25 18:03:09 2005
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  */
00020 /*****************************************************************************/
00021 
00022 #ifndef _cvc3__translator_h_
00023 #define _cvc3__translator_h_
00024 
00025 #include <string>
00026 #include <fstream>
00027 #include <vector>
00028 #include <map>
00029 #include "queryresult.h"
00030 #include "compat_hash_map.h"
00031 
00032 namespace CVC3 {
00033 
00034 class Expr;
00035 template <class Data> class ExprMap;
00036 class Type;
00037 class ExprManager;
00038 class ExprStream;
00039 class TheoryCore;
00040 class TheoryUF;
00041 class TheoryArith;
00042 class TheoryArray;
00043 class TheoryQuant;
00044 class TheoryRecords;
00045 class TheorySimulate;
00046 class TheoryBitvector;
00047 class TheoryDatatype;
00048 template <class Data> class ExprMap;
00049 
00050 //! Used to keep track of which subset of arith is being used
00051 typedef enum {
00052   NOT_USED = 0,
00053   TERMS_ONLY,
00054   DIFF_ONLY,
00055   LINEAR,
00056   NONLINEAR
00057 } ArithLang;
00058 
00059 //All the translation code should go here
00060 class Translator {
00061   ExprManager* d_em;
00062   const bool& d_translate;
00063   const bool& d_real2int;
00064   const bool& d_convertArith;
00065   const std::string& d_convertToDiff;
00066   bool d_iteLiftArith;
00067   const std::string& d_expResult;
00068   std::string d_category;
00069   bool d_convertArray;
00070   bool d_combineAssump;
00071 
00072   /** Private class for hashing strings; copied from ExprManager */
00073   class HashString {
00074     std::hash<char*> h;
00075   public:
00076     size_t operator()(const std::string& s) const {
00077       return h(const_cast<char*>(s.c_str()));
00078     }
00079   };
00080   std::hash_map<std::string, std::string, HashString> d_replaceSymbols;
00081 
00082   //! The log file for top-level API calls in the CVC3 input language
00083   std::ostream* d_osdump;
00084   std::ofstream d_osdumpFile;
00085   std::ifstream d_tmpFile;
00086   bool d_dump, d_dumpFileOpen;
00087 
00088   bool d_intIntArray, d_intRealArray, d_intIntRealArray, d_ax, d_unknown;
00089   bool d_realUsed;
00090   bool d_intUsed;
00091   bool d_intConstUsed;
00092   ArithLang d_langUsed;
00093   bool d_UFIDL_ok;
00094   bool d_arithUsed;
00095 
00096   Expr* d_zeroVar;
00097   int d_convertToBV;
00098 
00099   TheoryCore* d_theoryCore;
00100   TheoryUF* d_theoryUF;
00101   TheoryArith* d_theoryArith;
00102   TheoryArray* d_theoryArray;
00103   TheoryQuant* d_theoryQuant;
00104   TheoryRecords* d_theoryRecords;
00105   TheorySimulate* d_theorySimulate;
00106   TheoryBitvector* d_theoryBitvector;
00107   TheoryDatatype* d_theoryDatatype;
00108 
00109   std::vector<Expr> d_dumpExprs;
00110 
00111   std::map<std::string, Type>* d_arrayConvertMap;
00112   Type* d_indexType;
00113   Type* d_elementType;
00114   Type* d_arrayType;
00115   std::vector<Expr> d_equalities;
00116 
00117   // Name of benchmark in SMT-LIB
00118   std::string d_benchName;
00119   // Status of benchmark in SMT-LIB
00120   std::string d_status;
00121   // Source of benchmark in SMT-LIB
00122   std::string d_source;
00123 
00124   std::string fileToSMTLIBIdentifier(const std::string& filename);
00125   Expr preprocessRec(const Expr& e, ExprMap<Expr>& cache);
00126   Expr preprocess(const Expr& e, ExprMap<Expr>& cache);
00127   Expr preprocess2Rec(const Expr& e, ExprMap<Expr>& cache, Type desiredType);
00128   Expr preprocess2(const Expr& e, ExprMap<Expr>& cache);
00129   bool containsArray(const Expr& e);
00130   Expr processType(const Expr& e);
00131 
00132   /*
00133   Expr spassPreprocess(const Expr& e, ExprMap<Expr>& mapping,
00134                        std::vector<Expr>& functions,
00135                        std::vector<Expr>& predicates);
00136   */
00137 
00138 public:
00139   // Constructors
00140   Translator(ExprManager* em,
00141              const bool& translate,
00142              const bool& real2int,
00143              const bool& convertArith,
00144              const std::string& convertToDiff,
00145              bool iteLiftArith,
00146              const std::string& expResult,
00147              const std::string& category,
00148              bool convertArray,
00149              bool combineAssump,
00150              int convertToBV);
00151   ~Translator();
00152 
00153   bool start(const std::string& dumpFile);
00154   /*! Dump the expression in the current output language
00155       \param dumpOnly When false, the expression is output both when
00156       translating and when producing a trace of commands.  When true, the
00157       expression is only output when producing a trace of commands
00158       (i.e. ignored during translation).
00159    */
00160   void dump(const Expr& e, bool dumpOnly = false);
00161   bool dumpAssertion(const Expr& e);
00162   bool dumpQuery(const Expr& e);
00163   void dumpQueryResult(QueryResult qres);
00164   void finish();
00165 
00166   void setTheoryCore(TheoryCore* theoryCore) { d_theoryCore = theoryCore; }
00167   void setTheoryUF(TheoryUF* theoryUF) { d_theoryUF = theoryUF; }
00168   void setTheoryArith(TheoryArith* theoryArith) { d_theoryArith = theoryArith; }
00169   void setTheoryArray(TheoryArray* theoryArray) { d_theoryArray = theoryArray; }
00170   void setTheoryQuant(TheoryQuant* theoryQuant) { d_theoryQuant = theoryQuant; }
00171   void setTheoryRecords(TheoryRecords* theoryRecords) { d_theoryRecords = theoryRecords; }
00172   void setTheorySimulate(TheorySimulate* theorySimulate) { d_theorySimulate = theorySimulate; }
00173   void setTheoryBitvector(TheoryBitvector* theoryBitvector) { d_theoryBitvector = theoryBitvector; }
00174   void setTheoryDatatype(TheoryDatatype* theoryDatatype) { d_theoryDatatype = theoryDatatype; }
00175 
00176   void setBenchName(std::string name) { d_benchName = name; }
00177   std::string benchName() { return d_benchName; }
00178   void setStatus(std::string status) { d_status = status; }
00179   std::string status() { return d_status; }
00180   void setSource(std::string source) { d_source = source; }
00181   std::string source() { return d_source; }
00182   void setCategory(std::string category) { d_category = category; }
00183   std::string category() { return d_category; }
00184 
00185   const std::string fixConstName(const std::string& s);
00186   const std::string escapeSymbol(const std::string& s);
00187   const std::string quoteAnnotation(const std::string& s);
00188   //! Returns true if expression has been printed
00189   /*! If false is returned, array theory should print expression as usual */
00190   bool printArrayExpr(ExprStream& os, const Expr& e);
00191 
00192   Expr zeroVar();
00193 
00194 }; // end of class Translator
00195 
00196 } // end of namespace CVC3 
00197 
00198 #endif