CVC3
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file vcl.h 00004 * \brief Main implementation of ValidityChecker for CVC3. 00005 * 00006 * Author: Clark Barrett 00007 * 00008 * Created: Wed Dec 11 14:40:39 2002 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__include__vcl_h_ 00023 #define _cvc3__include__vcl_h_ 00024 00025 #include <queue> 00026 00027 #include "vc.h" 00028 #include "command_line_flags.h" 00029 #include "statistics.h" 00030 #include "cdmap.h" 00031 #include "cdlist.h" 00032 00033 namespace CVC3 { 00034 00035 class SearchEngine; 00036 class Theory; 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 class Translator; 00047 00048 class CVC_DLL VCL : public ValidityChecker { 00049 00050 //! Pointers to main system components 00051 ExprManager* d_em; 00052 ContextManager* d_cm; 00053 TheoremManager* d_tm; 00054 SearchEngine* d_se; 00055 00056 //! Pointers to theories 00057 TheoryCore* d_theoryCore; 00058 TheoryUF* d_theoryUF; 00059 TheoryArith* d_theoryArith; 00060 TheoryArray* d_theoryArray; 00061 TheoryQuant* d_theoryQuant; 00062 TheoryRecords* d_theoryRecords; 00063 TheorySimulate* d_theorySimulate; 00064 TheoryBitvector* d_theoryBitvector; 00065 TheoryDatatype* d_theoryDatatype; 00066 Translator* d_translator; 00067 00068 //! All theories are stored in this common vector 00069 /*! This includes TheoryCore and TheoryArith. */ 00070 std::vector<Theory*> d_theories; 00071 00072 //! Command line flags 00073 CLFlags *d_flags; 00074 00075 //! User-level view of the scope stack 00076 CDO<int> *d_stackLevel; 00077 00078 //! Run-time statistics 00079 Statistics* d_statistics; 00080 00081 //! Next index for user assertion 00082 size_t d_nextIdx; 00083 00084 //! Structure to hold user assertions indexed by declaration order 00085 class UserAssertion { 00086 size_t d_idx; 00087 Theorem d_thm; //! The theorem of the assertion (a |- a) 00088 Theorem d_tcc; //! The proof of its TCC 00089 public: 00090 //! Default constructor 00091 UserAssertion() { } 00092 //! Constructor 00093 UserAssertion(const Theorem& thm, const Theorem& tcc, size_t idx) 00094 : d_idx(idx), d_thm(thm), d_tcc(tcc) { } 00095 //! Fetching a Theorem 00096 const Theorem& thm() const { return d_thm; } 00097 //! Fetching a TCC 00098 const Theorem& tcc() const { return d_tcc; } 00099 //! Auto-conversion to Theorem 00100 operator Theorem() { return d_thm; } 00101 //! Comparison for use in std::map, to sort in declaration order 00102 friend bool operator<(const UserAssertion& a1, const UserAssertion& a2) { 00103 return (a1.d_idx < a2.d_idx); 00104 } 00105 }; 00106 00107 //! Backtracking map of user assertions 00108 CDMap<Expr,UserAssertion>* d_userAssertions; 00109 00110 //! Backtracking map of assertions when assertion batching is on 00111 CDList<Expr>* d_batchedAssertions; 00112 00113 //! Index into batched Assertions 00114 CDO<unsigned>* d_batchedAssertionsIdx; 00115 00116 //! Result of the last query() 00117 /*! Saved for printing assumptions and proofs. Normally it is 00118 * Theorem3, but query() on a TCC returns a 2-valued Theorem. */ 00119 Theorem3 d_lastQuery; 00120 00121 //! Result of the last query(e, true) (for a TCC). 00122 Theorem d_lastQueryTCC; 00123 00124 //! Closure of the last query(e): |- Gamma => e 00125 Theorem3 d_lastClosure; 00126 00127 //! Whether to dump a trace (or a translated version) 00128 bool d_dump; 00129 00130 // Private methods 00131 00132 //! Construct the closure "|-_3 Gamma => phi" of thm = "Gamma |-_3 phi" 00133 Theorem3 deriveClosure(const Theorem3& thm); 00134 00135 //! Recursive assumption graph traversal to find user assumptions 00136 /*! 00137 * If an assumption has a TCC, traverse the proof of TCC and add its 00138 * assumptions to the set recursively. 00139 */ 00140 void getAssumptionsRec(const Theorem& thm, 00141 std::set<UserAssertion>& assumptions, 00142 bool addTCCs); 00143 00144 //! Get set of user assertions from the set of assumptions 00145 void getAssumptions(const Assumptions& a, std::vector<Expr>& assumptions); 00146 00147 //! Check the tcc 00148 Theorem checkTCC(const Expr& tcc); 00149 00150 #ifdef _CVC3_DEBUG_MODE 00151 //! Print an entry to the dump file: change of scope 00152 void dumpTrace(int scope); 00153 #endif 00154 00155 //! Initialize everything except flags 00156 void init(void); 00157 //! Destroy everything except flags 00158 void destroy(void); 00159 00160 public: 00161 // Takes the vector of command line flags. 00162 VCL(const CLFlags& flags); 00163 ~VCL(); 00164 00165 // Implementation of vc.h virtual functions 00166 00167 CLFlags& getFlags() const { return *d_flags; } 00168 void reprocessFlags(); 00169 00170 TheoryCore* core(); 00171 00172 Type boolType(); 00173 Type realType(); 00174 Type intType(); 00175 Type subrangeType(const Expr& l, const Expr& r); 00176 Type subtypeType(const Expr& pred, const Expr& witness); 00177 Type tupleType(const Type& type0, const Type& type1); 00178 Type tupleType(const Type& type0, const Type& type1, const Type& type2); 00179 Type tupleType(const std::vector<Type>& types); 00180 Type recordType(const std::string& field, const Type& type); 00181 Type recordType(const std::string& field0, const Type& type0, 00182 const std::string& field1, const Type& type1); 00183 Type recordType(const std::string& field0, const Type& type0, 00184 const std::string& field1, const Type& type1, 00185 const std::string& field2, const Type& type2); 00186 Type recordType(const std::vector<std::string>& fields, 00187 const std::vector<Type>& types); 00188 Type dataType(const std::string& name, 00189 const std::string& constructor, 00190 const std::vector<std::string>& selectors, 00191 const std::vector<Expr>& types); 00192 Type dataType(const std::string& name, 00193 const std::vector<std::string>& constructors, 00194 const std::vector<std::vector<std::string> >& selectors, 00195 const std::vector<std::vector<Expr> >& types); 00196 void dataType(const std::vector<std::string>& names, 00197 const std::vector<std::vector<std::string> >& constructors, 00198 const std::vector<std::vector<std::vector<std::string> > >& selectors, 00199 const std::vector<std::vector<std::vector<Expr> > >& types, 00200 std::vector<Type>& returnTypes); 00201 Type arrayType(const Type& typeIndex, const Type& typeData); 00202 Type bitvecType(int n); 00203 Type funType(const Type& typeDom, const Type& typeRan); 00204 Type funType(const std::vector<Type>& typeDom, const Type& typeRan); 00205 Type createType(const std::string& typeName); 00206 Type createType(const std::string& typeName, const Type& def); 00207 Type lookupType(const std::string& typeName); 00208 00209 ExprManager* getEM() { return d_em; } 00210 Expr varExpr(const std::string& name, const Type& type); 00211 Expr varExpr(const std::string& name, const Type& type, const Expr& def); 00212 Expr lookupVar(const std::string& name, Type* type); 00213 Type getType(const Expr& e); 00214 Type getBaseType(const Expr& e); 00215 Type getBaseType(const Type& e); 00216 Expr getTypePred(const Type&t, const Expr& e); 00217 Expr stringExpr(const std::string& str); 00218 Expr idExpr(const std::string& name); 00219 Expr listExpr(const std::vector<Expr>& kids); 00220 Expr listExpr(const Expr& e1); 00221 Expr listExpr(const Expr& e1, const Expr& e2); 00222 Expr listExpr(const Expr& e1, const Expr& e2, const Expr& e3); 00223 Expr listExpr(const std::string& op, const std::vector<Expr>& kids); 00224 Expr listExpr(const std::string& op, const Expr& e1); 00225 Expr listExpr(const std::string& op, const Expr& e1, 00226 const Expr& e2); 00227 Expr listExpr(const std::string& op, const Expr& e1, 00228 const Expr& e2, const Expr& e3); 00229 void printExpr(const Expr& e); 00230 void printExpr(const Expr& e, std::ostream& os); 00231 Expr parseExpr(const Expr& e); 00232 Type parseType(const Expr& e); 00233 Expr importExpr(const Expr& e); 00234 Type importType(const Type& t); 00235 void cmdsFromString(const std::string& s, InputLanguage lang); 00236 Expr exprFromString(const std::string& s); 00237 00238 Expr trueExpr(); 00239 Expr falseExpr(); 00240 Expr notExpr(const Expr& child); 00241 Expr andExpr(const Expr& left, const Expr& right); 00242 Expr andExpr(const std::vector<Expr>& children); 00243 Expr orExpr(const Expr& left, const Expr& right); 00244 Expr orExpr(const std::vector<Expr>& children); 00245 Expr impliesExpr(const Expr& hyp, const Expr& conc); 00246 Expr iffExpr(const Expr& left, const Expr& right); 00247 Expr eqExpr(const Expr& child0, const Expr& child1); 00248 Expr distinctExpr(const std::vector<Expr>& children); 00249 Expr iteExpr(const Expr& ifpart, const Expr& thenpart, const Expr& elsepart); 00250 00251 Op createOp(const std::string& name, const Type& type); 00252 Op createOp(const std::string& name, const Type& type, const Expr& def); 00253 Op lookupOp(const std::string& name, Type* type); 00254 Expr funExpr(const Op& op, const Expr& child); 00255 Expr funExpr(const Op& op, const Expr& left, const Expr& right); 00256 Expr funExpr(const Op& op, const Expr& child0, const Expr& child1, const Expr& child2); 00257 Expr funExpr(const Op& op, const std::vector<Expr>& children); 00258 00259 bool addPairToArithOrder(const Expr& smaller, const Expr& bigger); 00260 Expr ratExpr(int n, int d); 00261 Expr ratExpr(const std::string& n, const std::string& d, int base); 00262 Expr ratExpr(const std::string& n, int base); 00263 Expr uminusExpr(const Expr& child); 00264 Expr plusExpr(const Expr& left, const Expr& right); 00265 Expr plusExpr(const std::vector<Expr>& children); 00266 Expr minusExpr(const Expr& left, const Expr& right); 00267 Expr multExpr(const Expr& left, const Expr& right); 00268 Expr powExpr(const Expr& x, const Expr& n); 00269 Expr divideExpr(const Expr& left, const Expr& right); 00270 Expr ltExpr(const Expr& left, const Expr& right); 00271 Expr leExpr(const Expr& left, const Expr& right); 00272 Expr gtExpr(const Expr& left, const Expr& right); 00273 Expr geExpr(const Expr& left, const Expr& right); 00274 00275 Expr recordExpr(const std::string& field, const Expr& expr); 00276 Expr recordExpr(const std::string& field0, const Expr& expr0, 00277 const std::string& field1, const Expr& expr1); 00278 Expr recordExpr(const std::string& field0, const Expr& expr0, 00279 const std::string& field1, const Expr& expr1, 00280 const std::string& field2, const Expr& expr2); 00281 Expr recordExpr(const std::vector<std::string>& fields, 00282 const std::vector<Expr>& exprs); 00283 Expr recSelectExpr(const Expr& record, const std::string& field); 00284 Expr recUpdateExpr(const Expr& record, const std::string& field, 00285 const Expr& newValue); 00286 00287 Expr readExpr(const Expr& array, const Expr& index); 00288 Expr writeExpr(const Expr& array, const Expr& index, const Expr& newValue); 00289 00290 Expr newBVConstExpr(const std::string& s, int base); 00291 Expr newBVConstExpr(const std::vector<bool>& bits); 00292 Expr newBVConstExpr(const Rational& r, int len); 00293 Expr newConcatExpr(const Expr& t1, const Expr& t2); 00294 Expr newConcatExpr(const std::vector<Expr>& kids); 00295 Expr newBVExtractExpr(const Expr& e, int hi, int low); 00296 Expr newBVNegExpr(const Expr& t1); 00297 Expr newBVAndExpr(const Expr& t1, const Expr& t2); 00298 Expr newBVAndExpr(const std::vector<Expr>& kids); 00299 Expr newBVOrExpr(const Expr& t1, const Expr& t2); 00300 Expr newBVOrExpr(const std::vector<Expr>& kids); 00301 Expr newBVXorExpr(const Expr& t1, const Expr& t2); 00302 Expr newBVXorExpr(const std::vector<Expr>& kids); 00303 Expr newBVXnorExpr(const Expr& t1, const Expr& t2); 00304 Expr newBVXnorExpr(const std::vector<Expr>& kids); 00305 Expr newBVNandExpr(const Expr& t1, const Expr& t2); 00306 Expr newBVNorExpr(const Expr& t1, const Expr& t2); 00307 Expr newBVCompExpr(const Expr& t1, const Expr& t2); 00308 Expr newBVLTExpr(const Expr& t1, const Expr& t2); 00309 Expr newBVLEExpr(const Expr& t1, const Expr& t2); 00310 Expr newBVSLTExpr(const Expr& t1, const Expr& t2); 00311 Expr newBVSLEExpr(const Expr& t1, const Expr& t2); 00312 Expr newSXExpr(const Expr& t1, int len); 00313 Expr newBVUminusExpr(const Expr& t1); 00314 Expr newBVSubExpr(const Expr& t1, const Expr& t2); 00315 Expr newBVPlusExpr(int numbits, const std::vector<Expr>& k); 00316 Expr newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2); 00317 Expr newBVMultExpr(int numbits, const Expr& t1, const Expr& t2); 00318 Expr newBVUDivExpr(const Expr& t1, const Expr& t2); 00319 Expr newBVURemExpr(const Expr& t1, const Expr& t2); 00320 Expr newBVSDivExpr(const Expr& t1, const Expr& t2); 00321 Expr newBVSRemExpr(const Expr& t1, const Expr& t2); 00322 Expr newBVSModExpr(const Expr& t1, const Expr& t2); 00323 Expr newFixedLeftShiftExpr(const Expr& t1, int r); 00324 Expr newFixedConstWidthLeftShiftExpr(const Expr& t1, int r); 00325 Expr newFixedRightShiftExpr(const Expr& t1, int r); 00326 Expr newBVSHL(const Expr& t1, const Expr& t2); 00327 Expr newBVLSHR(const Expr& t1, const Expr& t2); 00328 Expr newBVASHR(const Expr& t1, const Expr& t2); 00329 Rational computeBVConst(const Expr& e); 00330 00331 Expr tupleExpr(const std::vector<Expr>& exprs); 00332 Expr tupleSelectExpr(const Expr& tuple, int index); 00333 Expr tupleUpdateExpr(const Expr& tuple, int index, const Expr& newValue); 00334 Expr datatypeConsExpr(const std::string& constructor, 00335 const std::vector<Expr>& args); 00336 Expr datatypeSelExpr(const std::string& selector, const Expr& arg); 00337 Expr datatypeTestExpr(const std::string& constructor, const Expr& arg); 00338 Expr boundVarExpr(const std::string& name, const std::string& uid, 00339 const Type& type); 00340 Expr forallExpr(const std::vector<Expr>& vars, const Expr& body); 00341 Expr forallExpr(const std::vector<Expr>& vars, const Expr& body, const Expr& trigger); 00342 Expr forallExpr(const std::vector<Expr>& vars, const Expr& body, 00343 const std::vector<Expr>& triggers); 00344 Expr forallExpr(const std::vector<Expr>& vars, const Expr& body, 00345 const std::vector<std::vector<Expr> >& triggers); 00346 00347 void setTriggers(const Expr& e, const std::vector<std::vector<Expr> >& triggers); 00348 void setTriggers(const Expr& e, const std::vector<Expr>& triggers); 00349 void setTrigger(const Expr& e, const Expr& trigger); 00350 void setMultiTrigger(const Expr& e, const std::vector<Expr>& multiTrigger); 00351 00352 Expr existsExpr(const std::vector<Expr>& vars, const Expr& body); 00353 Op lambdaExpr(const std::vector<Expr>& vars, const Expr& body); 00354 Op transClosure(const Op& op); 00355 Expr simulateExpr(const Expr& f, const Expr& s0, 00356 const std::vector<Expr>& inputs, const Expr& n); 00357 00358 void setResourceLimit(unsigned limit); 00359 void setTimeLimit(unsigned limit); 00360 void assertFormula(const Expr& e); 00361 void registerAtom(const Expr& e); 00362 Expr getImpliedLiteral(); 00363 Expr simplify(const Expr& e); 00364 Theorem simplifyThm(const Expr& e); 00365 QueryResult query(const Expr& e); 00366 QueryResult checkUnsat(const Expr& e); 00367 QueryResult checkContinue(); 00368 QueryResult restart(const Expr& e); 00369 void returnFromCheck(); 00370 void getUserAssumptions(std::vector<Expr>& assumptions); 00371 void getInternalAssumptions(std::vector<Expr>& assumptions); 00372 void getAssumptions(std::vector<Expr>& assumptions); 00373 void getAssumptionsUsed(std::vector<Expr>& assumptions); 00374 Expr getProofQuery(); 00375 void getCounterExample(std::vector<Expr>& assumptions, bool inOrder); 00376 void getConcreteModel(ExprMap<Expr> & m); 00377 QueryResult tryModelGeneration(); 00378 FormulaValue value(const Expr& e); 00379 bool inconsistent(std::vector<Expr>& assumptions); 00380 bool inconsistent(); 00381 bool incomplete(); 00382 bool incomplete(std::vector<std::string>& reasons); 00383 Proof getProof(); 00384 Expr getTCC(); 00385 void getAssumptionsTCC(std::vector<Expr>& assumptions); 00386 Proof getProofTCC(); 00387 Expr getClosure(); 00388 Proof getProofClosure(); 00389 00390 int stackLevel(); 00391 void push(); 00392 void pop(); 00393 void popto(int stackLevel); 00394 int scopeLevel(); 00395 void pushScope(); 00396 void popScope(); 00397 void poptoScope(int scopeLevel); 00398 Context* getCurrentContext(); 00399 void reset(); 00400 void logAnnotation(const Expr& annot); 00401 00402 void loadFile(const std::string& fileName, 00403 InputLanguage lang = PRESENTATION_LANG, 00404 bool interactive = false, 00405 bool calledFromParser = false); 00406 void loadFile(std::istream& is, 00407 InputLanguage lang = PRESENTATION_LANG, 00408 bool interactive = false); 00409 00410 Statistics& getStatistics() { return *d_statistics; } 00411 void printStatistics() { std::cout << *d_statistics << std::endl; } 00412 unsigned long getMemory(int verbosity = 0); 00413 00414 }; 00415 00416 } 00417 00418 #endif