CVC3 2.2
|
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 00031 namespace CVC3 { 00032 00033 class Expr; 00034 class Type; 00035 class ExprManager; 00036 class ExprStream; 00037 class TheoryCore; 00038 class TheoryUF; 00039 class TheoryArith; 00040 class TheoryArray; 00041 class TheoryQuant; 00042 class TheoryRecords; 00043 class TheorySimulate; 00044 class TheoryBitvector; 00045 class TheoryDatatype; 00046 template <class Data> class ExprMap; 00047 00048 //! Used to keep track of which subset of arith is being used 00049 typedef enum { 00050 NOT_USED = 0, 00051 TERMS_ONLY, 00052 DIFF_ONLY, 00053 LINEAR, 00054 NONLINEAR 00055 } ArithLang; 00056 00057 //All the translation code should go here 00058 class Translator { 00059 ExprManager* d_em; 00060 const bool& d_translate; 00061 const bool& d_real2int; 00062 const bool& d_convertArith; 00063 const std::string& d_convertToDiff; 00064 bool d_iteLiftArith; 00065 const std::string& d_expResult; 00066 const std::string& d_category; 00067 bool d_convertArray; 00068 bool d_combineAssump; 00069 00070 //! The log file for top-level API calls in the CVC3 input language 00071 std::ostream* d_osdump; 00072 std::ofstream d_osdumpFile; 00073 std::ifstream d_tmpFile; 00074 bool d_dump, d_dumpFileOpen; 00075 00076 bool d_intIntArray, d_intRealArray, d_intIntRealArray, d_ax, d_unknown; 00077 bool d_realUsed; 00078 bool d_intUsed; 00079 bool d_intConstUsed; 00080 ArithLang d_langUsed; 00081 bool d_UFIDL_ok; 00082 bool d_arithUsed; 00083 00084 Expr* d_zeroVar; 00085 int d_convertToBV; 00086 00087 TheoryCore* d_theoryCore; 00088 TheoryUF* d_theoryUF; 00089 TheoryArith* d_theoryArith; 00090 TheoryArray* d_theoryArray; 00091 TheoryQuant* d_theoryQuant; 00092 TheoryRecords* d_theoryRecords; 00093 TheorySimulate* d_theorySimulate; 00094 TheoryBitvector* d_theoryBitvector; 00095 TheoryDatatype* d_theoryDatatype; 00096 00097 std::vector<Expr> d_dumpExprs; 00098 00099 std::map<std::string, Type>* d_arrayConvertMap; 00100 Type* d_indexType; 00101 Type* d_elementType; 00102 Type* d_arrayType; 00103 std::vector<Expr> d_equalities; 00104 00105 std::string fileToSMTLIBIdentifier(const std::string& filename); 00106 Expr preprocessRec(const Expr& e, ExprMap<Expr>& cache); 00107 Expr preprocess(const Expr& e, ExprMap<Expr>& cache); 00108 Expr preprocess2Rec(const Expr& e, ExprMap<Expr>& cache, Type desiredType); 00109 Expr preprocess2(const Expr& e, ExprMap<Expr>& cache); 00110 bool containsArray(const Expr& e); 00111 Expr processType(const Expr& e); 00112 00113 public: 00114 // Constructors 00115 Translator(ExprManager* em, 00116 const bool& translate, 00117 const bool& real2int, 00118 const bool& convertArith, 00119 const std::string& convertToDiff, 00120 bool iteLiftArith, 00121 const std::string& expResult, 00122 const std::string& category, 00123 bool convertArray, 00124 bool combineAssump, 00125 int convertToBV); 00126 ~Translator(); 00127 00128 bool start(const std::string& dumpFile); 00129 /*! Dump the expression in the current output language 00130 \param dumpOnly When false, the expression is output both when 00131 translating and when producing a trace of commands. When true, the 00132 expression is only output when producing a trace of commands 00133 (i.e. ignored during translation). 00134 */ 00135 void dump(const Expr& e, bool dumpOnly = false); 00136 bool dumpAssertion(const Expr& e); 00137 bool dumpQuery(const Expr& e); 00138 void dumpQueryResult(QueryResult qres); 00139 void finish(); 00140 00141 void setTheoryCore(TheoryCore* theoryCore) { d_theoryCore = theoryCore; } 00142 void setTheoryUF(TheoryUF* theoryUF) { d_theoryUF = theoryUF; } 00143 void setTheoryArith(TheoryArith* theoryArith) { d_theoryArith = theoryArith; } 00144 void setTheoryArray(TheoryArray* theoryArray) { d_theoryArray = theoryArray; } 00145 void setTheoryQuant(TheoryQuant* theoryQuant) { d_theoryQuant = theoryQuant; } 00146 void setTheoryRecords(TheoryRecords* theoryRecords) { d_theoryRecords = theoryRecords; } 00147 void setTheorySimulate(TheorySimulate* theorySimulate) { d_theorySimulate = theorySimulate; } 00148 void setTheoryBitvector(TheoryBitvector* theoryBitvector) { d_theoryBitvector = theoryBitvector; } 00149 void setTheoryDatatype(TheoryDatatype* theoryDatatype) { d_theoryDatatype = theoryDatatype; } 00150 00151 const std::string fixConstName(const std::string& s); 00152 //! Returns true if expression has been printed 00153 /*! If false is returned, array theory should print expression as usual */ 00154 bool printArrayExpr(ExprStream& os, const Expr& e); 00155 00156 Expr zeroVar(); 00157 00158 }; // end of class Translator 00159 00160 } // end of namespace CVC3 00161 00162 #endif