00001 /*****************************************************************************/ 00002 /*! 00003 * \file vc.h 00004 * \brief Generic API for a validity checker 00005 * 00006 * Author: Clark Barrett 00007 * 00008 * Created: Tue Nov 26 17:45:10 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__vc_h_ 00023 #define _cvc3__include__vc_h_ 00024 00025 #include "os.h" 00026 #include "queryresult.h" 00027 #include "expr.h" 00028 00029 /*****************************************************************************/ 00030 /*! 00031 *\defgroup Note Note that this list of modules is very incomplete 00032 *\brief Note that this list of modules is very incomplete 00033 */ 00034 /*****************************************************************************/ 00035 00036 /*****************************************************************************/ 00037 /*! 00038 *\defgroup CVC3 CVC3 00039 *\brief The top level group which includes all of CVC3 documentation. 00040 *@{ 00041 */ 00042 /*****************************************************************************/ 00043 00044 /*****************************************************************************/ 00045 /*! 00046 *\defgroup BuildingBlocks Building Blocks 00047 *\brief Code providing basic infrastructure 00048 */ 00049 /*****************************************************************************/ 00050 00051 /*****************************************************************************/ 00052 /*! 00053 *\defgroup VC Validity Checker 00054 *\brief The modules that make up the validity checker 00055 */ 00056 /*****************************************************************************/ 00057 00058 /*@}*/ // end of group CVC3 00059 00060 /*****************************************************************************/ 00061 /*! 00062 *\defgroup VC_API Validity Checker API 00063 * \ingroup VC 00064 *\brief The library interface of the validity checker (class ValidityChecker) 00065 */ 00066 /*****************************************************************************/ 00067 00068 namespace CVC3 { 00069 00070 class Context; 00071 class CLFlags; 00072 class Statistics; 00073 00074 /*****************************************************************************/ 00075 /*! 00076 *\class ValidityChecker 00077 *\brief Generic API for a validity checker 00078 *\ingroup VC_API 00079 *\anchor vc 00080 * 00081 * Author: Clark Barrett 00082 * 00083 * Created: Tue Nov 26 18:24:25 2002 00084 * 00085 * All terms and formulas are represented as expressions using the Expr class. 00086 * The notion of a context is also important. A context is a "background" set 00087 * of formulas which are assumed to be true or false. Formulas can be added to 00088 * the context explicitly, using assertFormula, or they may be added as part of 00089 * processing a query command. At any time, the current set of formulas making 00090 * up the context can be retrieved using getAssumptions. 00091 */ 00092 /*****************************************************************************/ 00093 class CVC_DLL ValidityChecker { 00094 00095 public: 00096 //! Constructor 00097 ValidityChecker() {} 00098 //! Destructor 00099 virtual ~ValidityChecker() {} 00100 00101 //! Return the set of command-line flags 00102 /*! The flags are returned by reference, and if modified, will have an 00103 immediate effect on the subsequent commands. Note that not all flags will 00104 have such an effect; some flags are used only at initialization time (like 00105 "sat"), and therefore, will not take effect if modified after 00106 ValidityChecker is created. 00107 */ 00108 virtual CLFlags& getFlags() const = 0; 00109 //! Force reprocessing of all flags 00110 virtual void reprocessFlags() = 0; 00111 00112 /***************************************************************************/ 00113 /* 00114 * Static methods 00115 */ 00116 /***************************************************************************/ 00117 00118 //! Create the set of command line flags with default values; 00119 /*! 00120 \return the set of flags by value 00121 */ 00122 static CLFlags createFlags(); 00123 //! Create an instance of ValidityChecker 00124 /*! 00125 \param flags is the set of command line flags. 00126 */ 00127 static ValidityChecker* create(const CLFlags& flags); 00128 //! Create an instance of ValidityChecker using default flag values. 00129 static ValidityChecker* create(); 00130 00131 /***************************************************************************/ 00132 /*! 00133 *\name Type-related methods 00134 * Methods for creating and looking up types 00135 *\sa class Type 00136 *@{ 00137 */ 00138 /***************************************************************************/ 00139 00140 // Basic types 00141 virtual Type boolType() = 0; //!< Create type BOOLEAN 00142 00143 virtual Type realType() = 0; //!< Create type REAL 00144 00145 virtual Type intType() = 0; //!< Create type INT 00146 00147 //! Create a subrange type [l..r] 00148 /*! l and r can be Null; l=Null represents minus infinity, r=Null is 00149 * plus infinity. 00150 */ 00151 virtual Type subrangeType(const Expr& l, const Expr& r) = 0; 00152 00153 //! Creates a subtype defined by the given predicate 00154 /*! 00155 * \param pred is a predicate taking one argument of type T and returning 00156 * Boolean. The resulting type is a subtype of T whose elements x are those 00157 * satisfying the predicate pred(x). 00158 * 00159 * \param witness is an expression of type T for which pred holds (if a Null 00160 * expression is passed as a witness, cvc will try to prove \f$\exists x. pred(x))\f$. 00161 * if the witness check fails, a TypecheckException is thrown. 00162 */ 00163 virtual Type subtypeType(const Expr& pred, const Expr& witness) = 0; 00164 00165 // Tuple types 00166 //! 2-element tuple 00167 virtual Type tupleType(const Type& type0, const Type& type1) = 0; 00168 00169 //! 3-element tuple 00170 virtual Type tupleType(const Type& type0, const Type& type1, 00171 const Type& type2) = 0; 00172 //! n-element tuple (from a vector of types) 00173 virtual Type tupleType(const std::vector<Type>& types) = 0; 00174 00175 // Record types 00176 //! 1-element record 00177 virtual Type recordType(const std::string& field, const Type& type) = 0; 00178 00179 //! 2-element record 00180 /*! Fields will be sorted automatically */ 00181 virtual Type recordType(const std::string& field0, const Type& type0, 00182 const std::string& field1, const Type& type1) = 0; 00183 //! 3-element record 00184 /*! Fields will be sorted automatically */ 00185 virtual Type recordType(const std::string& field0, const Type& type0, 00186 const std::string& field1, const Type& type1, 00187 const std::string& field2, const Type& type2) = 0; 00188 //! n-element record (fields and types must be of the same length) 00189 /*! Fields will be sorted automatically */ 00190 virtual Type recordType(const std::vector<std::string>& fields, 00191 const std::vector<Type>& types) = 0; 00192 00193 // Datatypes 00194 00195 //! Single datatype, single constructor 00196 /*! The types are either type exressions (obtained from a type with 00197 * getExpr()) or string expressions containing the name of (one of) the 00198 * dataType(s) being defined. */ 00199 virtual Type dataType(const std::string& name, 00200 const std::string& constructor, 00201 const std::vector<std::string>& selectors, 00202 const std::vector<Expr>& types) = 0; 00203 00204 //! Single datatype, multiple constructors 00205 /*! The types are either type exressions (obtained from a type with 00206 * getExpr()) or string expressions containing the name of (one of) the 00207 * dataType(s) being defined. */ 00208 virtual Type dataType(const std::string& name, 00209 const std::vector<std::string>& constructors, 00210 const std::vector<std::vector<std::string> >& selectors, 00211 const std::vector<std::vector<Expr> >& types) = 0; 00212 00213 //! Multiple datatypes 00214 /*! The types are either type exressions (obtained from a type with 00215 * getExpr()) or string expressions containing the name of (one of) the 00216 * dataType(s) being defined. */ 00217 virtual void dataType(const std::vector<std::string>& names, 00218 const std::vector<std::vector<std::string> >& constructors, 00219 const std::vector<std::vector<std::vector<std::string> > >& selectors, 00220 const std::vector<std::vector<std::vector<Expr> > >& types, 00221 std::vector<Type>& returnTypes) = 0; 00222 00223 //! Create an array type (ARRAY typeIndex OF typeData) 00224 virtual Type arrayType(const Type& typeIndex, const Type& typeData) = 0; 00225 00226 //! Create a bitvector type of length n 00227 virtual Type bitvecType(int n) = 0; 00228 00229 //! Create a function type typeDom -> typeRan 00230 virtual Type funType(const Type& typeDom, const Type& typeRan) = 0; 00231 00232 //! Create a function type (t1,t2,...,tn) -> typeRan 00233 virtual Type funType(const std::vector<Type>& typeDom, const Type& typeRan) = 0; 00234 00235 //! Create named user-defined uninterpreted type 00236 virtual Type createType(const std::string& typeName) = 0; 00237 00238 //! Create named user-defined interpreted type (type abbreviation) 00239 virtual Type createType(const std::string& typeName, const Type& def) = 0; 00240 00241 //! Lookup a user-defined (uninterpreted) type by name 00242 virtual Type lookupType(const std::string& typeName) = 0; 00243 00244 /*@}*/ // End of Type-related methods 00245 00246 /***************************************************************************/ 00247 /*! 00248 *\name General Expr methods 00249 *\sa class Expr 00250 *\sa class ExprManager 00251 *@{ 00252 */ 00253 /***************************************************************************/ 00254 00255 //! Return the ExprManager 00256 virtual ExprManager* getEM() = 0; 00257 00258 //! Create a variable with a given name and type 00259 /*! 00260 \param name is the name of the variable 00261 \param type is its type. The type cannot be a function type. 00262 \return an Expr representation of a new variable 00263 */ 00264 virtual Expr varExpr(const std::string& name, const Type& type) = 0; 00265 00266 //! Create a variable with a given name, type, and value 00267 virtual Expr varExpr(const std::string& name, const Type& type, 00268 const Expr& def) = 0; 00269 00270 //! Create a bound variable with a given name, unique ID (uid) and type 00271 /*! 00272 \param name is the name of the variable 00273 \param uid is the unique ID (a string), which must be unique for 00274 each variable 00275 \param type is its type. The type cannot be a function type. 00276 \return an Expr representation of a new variable 00277 */ 00278 virtual Expr boundVarExpr(const std::string& name, 00279 const std::string& uid, 00280 const Type& type) = 0; 00281 00282 //! Get the variable associated with a name, and its type 00283 /*! 00284 \param name is the variable name 00285 \param type is where the type value is returned 00286 00287 \return a variable by the name. If there is no such Expr, a NULL \ 00288 Expr is returned. 00289 */ 00290 virtual Expr lookupVar(const std::string& name, Type* type) = 0; 00291 00292 //! Get the type of the Expr. 00293 virtual Type getType(const Expr& e) = 0; 00294 00295 //! Get the largest supertype of the Expr. 00296 virtual Type getBaseType(const Expr& e) = 0; 00297 00298 //! Get the largest supertype of the Type. 00299 virtual Type getBaseType(const Type& t) = 0; 00300 00301 //! Get the subtype predicate 00302 virtual Expr getTypePred(const Type&t, const Expr& e) = 0; 00303 00304 //! Create a string Expr 00305 virtual Expr stringExpr(const std::string& str) = 0; 00306 00307 //! Create an ID Expr 00308 virtual Expr idExpr(const std::string& name) = 0; 00309 00310 //! Create a list Expr 00311 /*! Intermediate representation for DP-specific expressions. 00312 * Normally, the first element of the list is a string Expr 00313 * representing an operator, and the rest of the list are the 00314 * arguments. For example, 00315 * 00316 * kids.push_back(vc->stringExpr("PLUS")); 00317 * kids.push_back(x); // x and y are previously created Exprs 00318 * kids.push_back(y); 00319 * Expr lst = vc->listExpr(kids); 00320 * 00321 * Or, alternatively (using its overloaded version): 00322 * 00323 * Expr lst = vc->listExpr("PLUS", x, y); 00324 * 00325 * or 00326 * 00327 * vector<Expr> summands; 00328 * summands.push_back(x); summands.push_back(y); ... 00329 * Expr lst = vc->listExpr("PLUS", summands); 00330 */ 00331 virtual Expr listExpr(const std::vector<Expr>& kids) = 0; 00332 00333 //! Overloaded version of listExpr with one argument 00334 virtual Expr listExpr(const Expr& e1) = 0; 00335 00336 //! Overloaded version of listExpr with two arguments 00337 virtual Expr listExpr(const Expr& e1, const Expr& e2) = 0; 00338 00339 //! Overloaded version of listExpr with three arguments 00340 virtual Expr listExpr(const Expr& e1, const Expr& e2, const Expr& e3) = 0; 00341 00342 //! Overloaded version of listExpr with string operator and many arguments 00343 virtual Expr listExpr(const std::string& op, 00344 const std::vector<Expr>& kids) = 0; 00345 00346 //! Overloaded version of listExpr with string operator and one argument 00347 virtual Expr listExpr(const std::string& op, const Expr& e1) = 0; 00348 00349 //! Overloaded version of listExpr with string operator and two arguments 00350 virtual Expr listExpr(const std::string& op, const Expr& e1, 00351 const Expr& e2) = 0; 00352 00353 //! Overloaded version of listExpr with string operator and three arguments 00354 virtual Expr listExpr(const std::string& op, const Expr& e1, 00355 const Expr& e2, const Expr& e3) = 0; 00356 00357 //! Prints e to the standard output 00358 virtual void printExpr(const Expr& e) = 0; 00359 00360 //! Prints e to the given ostream 00361 virtual void printExpr(const Expr& e, std::ostream& os) = 0; 00362 00363 //! Parse an expression using a Theory-specific parser 00364 virtual Expr parseExpr(const Expr& e) = 0; 00365 00366 //! Parse a type expression using a Theory-specific parser 00367 virtual Type parseType(const Expr& e) = 0; 00368 00369 //! Import the Expr from another instance of ValidityChecker 00370 /*! When expressions need to be passed among several instances of 00371 * ValidityChecker, they need to be explicitly imported into the 00372 * corresponding instance using this method. The return result is 00373 * an identical expression that belongs to the current instance of 00374 * ValidityChecker, and can be safely used as part of more complex 00375 * expressions from the same instance. 00376 */ 00377 virtual Expr importExpr(const Expr& e) = 0; 00378 00379 //! Import the Type from another instance of ValidityChecker 00380 /*! \sa getType() */ 00381 virtual Type importType(const Type& t) = 0; 00382 00383 /*@}*/ // End of General Expr Methods 00384 00385 /***************************************************************************/ 00386 /*! 00387 *\name Core expression methods 00388 * Methods for manipulating core expressions 00389 * 00390 * Except for equality and ite, the children provided as arguments must be of 00391 * type Boolean. 00392 *@{ 00393 */ 00394 /***************************************************************************/ 00395 00396 //! Return TRUE Expr 00397 virtual Expr trueExpr() = 0; 00398 00399 //! Return FALSE Expr 00400 virtual Expr falseExpr() = 0; 00401 00402 //! Create negation 00403 virtual Expr notExpr(const Expr& child) = 0; 00404 00405 //! Create 2-element conjunction 00406 virtual Expr andExpr(const Expr& left, const Expr& right) = 0; 00407 00408 //! Create n-element conjunction 00409 virtual Expr andExpr(const std::vector<Expr>& children) = 0; 00410 00411 //! Create 2-element disjunction 00412 virtual Expr orExpr(const Expr& left, const Expr& right) = 0; 00413 00414 //! Create n-element disjunction 00415 virtual Expr orExpr(const std::vector<Expr>& children) = 0; 00416 00417 //! Create Boolean implication 00418 virtual Expr impliesExpr(const Expr& hyp, const Expr& conc) = 0; 00419 00420 //! Create left IFF right (boolean equivalence) 00421 virtual Expr iffExpr(const Expr& left, const Expr& right) = 0; 00422 00423 //! Create an equality expression. 00424 /*! 00425 The two children must have the same type, and cannot be of type 00426 Boolean. 00427 */ 00428 virtual Expr eqExpr(const Expr& child0, const Expr& child1) = 0; 00429 00430 //! Create IF ifpart THEN thenpart ELSE elsepart ENDIF 00431 /*! 00432 \param ifpart must be of type Boolean. 00433 \param thenpart and \param elsepart must have the same type, which will 00434 also be the type of the ite expression. 00435 */ 00436 virtual Expr iteExpr(const Expr& ifpart, const Expr& thenpart, 00437 const Expr& elsepart) = 0; 00438 00439 /*@}*/ // End of Core expression methods 00440 00441 /***************************************************************************/ 00442 /*! 00443 *\name User-defined (uninterpreted) function methods 00444 * Methods for manipulating uninterpreted function expressions 00445 *@{ 00446 */ 00447 /***************************************************************************/ 00448 00449 //! Create a named uninterpreted function with a given type 00450 /*! 00451 \param name is the new function's name (as ID Expr) 00452 \param type is a function type ( [range -> domain] ) 00453 */ 00454 virtual Op createOp(const std::string& name, const Type& type) = 0; 00455 00456 //! Create a named user-defined function with a given type 00457 virtual Op createOp(const std::string& name, const Type& type, 00458 const Expr& def) = 0; 00459 00460 //! Unary function application (op must be of function type) 00461 virtual Expr funExpr(const Op& op, const Expr& child) = 0; 00462 00463 //! Binary function application (op must be of function type) 00464 virtual Expr funExpr(const Op& op, const Expr& left, const Expr& right) = 0; 00465 00466 //! Ternary function application (op must be of function type) 00467 virtual Expr funExpr(const Op& op, const Expr& child0, 00468 const Expr& child1, const Expr& child2) = 0; 00469 00470 //! n-ary function application (op must be of function type) 00471 virtual Expr funExpr(const Op& op, const std::vector<Expr>& children) = 0; 00472 00473 /*@}*/ // End of User-defined (uninterpreted) function methods 00474 00475 /***************************************************************************/ 00476 /*! 00477 *\name Arithmetic expression methods 00478 * Methods for manipulating arithmetic expressions 00479 * 00480 * These functions create arithmetic expressions. The children provided 00481 * as arguments must be of type Real. 00482 *@{ 00483 */ 00484 /***************************************************************************/ 00485 00486 //! Create a rational number with numerator n and denominator d. 00487 /*! 00488 \param n the numerator 00489 \param d the denominator, cannot be 0. 00490 */ 00491 virtual Expr ratExpr(int n, int d = 1) = 0; 00492 00493 //! Create a rational number with numerator n and denominator d. 00494 /*! 00495 Here n and d are given as strings. They are converted to 00496 arbitrary-precision integers according to the given base. 00497 */ 00498 virtual Expr ratExpr(const std::string& n, const std::string& d, int base) = 0; 00499 00500 //! Create a rational from a single string. 00501 /*! 00502 \param n can be a string containing an integer, a pair of integers 00503 "nnn/ddd", or a number in the fixed or floating point format. 00504 \param base is the base in which to interpret the string. 00505 */ 00506 virtual Expr ratExpr(const std::string& n, int base = 10) = 0; 00507 00508 //! Unary minus. 00509 virtual Expr uminusExpr(const Expr& child) = 0; 00510 00511 //! Create 2-element sum (left + right) 00512 virtual Expr plusExpr(const Expr& left, const Expr& right) = 0; 00513 00514 //! Make a difference (left - right) 00515 virtual Expr minusExpr(const Expr& left, const Expr& right) = 0; 00516 00517 //! Create a product (left * right) 00518 virtual Expr multExpr(const Expr& left, const Expr& right) = 0; 00519 00520 //! Create a power expression (x ^ n); n must be integer 00521 virtual Expr powExpr(const Expr& x, const Expr& n) = 0; 00522 00523 //! Create expression x / y 00524 virtual Expr divideExpr(const Expr& numerator, const Expr& denominator) = 0; 00525 00526 //! Create (left < right) 00527 virtual Expr ltExpr(const Expr& left, const Expr& right) = 0; 00528 00529 //! Create (left <= right) 00530 virtual Expr leExpr(const Expr& left, const Expr& right) = 0; 00531 00532 //! Create (left > right) 00533 virtual Expr gtExpr(const Expr& left, const Expr& right) = 0; 00534 00535 //! Create (left >= right) 00536 virtual Expr geExpr(const Expr& left, const Expr& right) = 0; 00537 00538 /*@}*/ // End of Arithmetic expression methods 00539 00540 /***************************************************************************/ 00541 /*! 00542 *\name Record expression methods 00543 * Methods for manipulating record expressions 00544 *@{ 00545 */ 00546 /***************************************************************************/ 00547 00548 //! Create a 1-element record value (# field := expr #) 00549 /*! Fields will be sorted automatically */ 00550 virtual Expr recordExpr(const std::string& field, const Expr& expr) = 0; 00551 00552 //! Create a 2-element record value (# field0 := expr0, field1 := expr1 #) 00553 /*! Fields will be sorted automatically */ 00554 virtual Expr recordExpr(const std::string& field0, const Expr& expr0, 00555 const std::string& field1, const Expr& expr1) = 0; 00556 00557 //! Create a 3-element record value (# field_i := expr_i #) 00558 /*! Fields will be sorted automatically */ 00559 virtual Expr recordExpr(const std::string& field0, const Expr& expr0, 00560 const std::string& field1, const Expr& expr1, 00561 const std::string& field2, const Expr& expr2) = 0; 00562 00563 //! Create an n-element record value (# field_i := expr_i #) 00564 /*! 00565 * \param fields 00566 * \param exprs must be the same length as fields 00567 * 00568 * Fields will be sorted automatically 00569 */ 00570 virtual Expr recordExpr(const std::vector<std::string>& fields, 00571 const std::vector<Expr>& exprs) = 0; 00572 00573 //! Create record.field (field selection) 00574 /*! Create an expression representing the selection of a field from 00575 a record. */ 00576 virtual Expr recSelectExpr(const Expr& record, const std::string& field) = 0; 00577 00578 //! Record update; equivalent to "record WITH .field := newValue" 00579 /*! Notice the `.' before field in the presentation language (and 00580 the comment above); this is to distinguish it from datatype 00581 update. 00582 */ 00583 virtual Expr recUpdateExpr(const Expr& record, const std::string& field, 00584 const Expr& newValue) = 0; 00585 00586 /*@}*/ // End of Record expression methods 00587 00588 /***************************************************************************/ 00589 /*! 00590 *\name Array expression methods 00591 * Methods for manipulating array expressions 00592 *@{ 00593 */ 00594 /***************************************************************************/ 00595 00596 //! Create an expression array[index] (array access) 00597 /*! Create an expression for the value of array at the given index */ 00598 virtual Expr readExpr(const Expr& array, const Expr& index) = 0; 00599 00600 //! Array update; equivalent to "array WITH index := newValue" 00601 virtual Expr writeExpr(const Expr& array, const Expr& index, 00602 const Expr& newValue) = 0; 00603 00604 /*@}*/ // End of Array expression methods 00605 00606 /***************************************************************************/ 00607 /*! 00608 *\name Bitvector expression methods 00609 * Methods for manipulating bitvector expressions 00610 *@{ 00611 */ 00612 /***************************************************************************/ 00613 00614 // Bitvector constants 00615 // From a string of digits in a given base 00616 virtual Expr newBVConstExpr(const std::string& s, int base = 2) = 0; 00617 // From a vector of bools 00618 virtual Expr newBVConstExpr(const std::vector<bool>& bits) = 0; 00619 // From a rational: bitvector is of length 'len', or the min. needed length when len=0. 00620 virtual Expr newBVConstExpr(const Rational& r, int len = 0) = 0; 00621 00622 // Concat and extract 00623 virtual Expr newConcatExpr(const Expr& t1, const Expr& t2) = 0; 00624 virtual Expr newConcatExpr(const std::vector<Expr>& kids) = 0; 00625 virtual Expr newBVExtractExpr(const Expr& e, int hi, int low) = 0; 00626 00627 // Bitwise Boolean operators: Negation, And, Nand, Or, Nor, Xor, Xnor 00628 virtual Expr newBVNegExpr(const Expr& t1) = 0; 00629 00630 virtual Expr newBVAndExpr(const Expr& t1, const Expr& t2) = 0; 00631 virtual Expr newBVAndExpr(const std::vector<Expr>& kids) = 0; 00632 00633 virtual Expr newBVOrExpr(const Expr& t1, const Expr& t2) = 0; 00634 virtual Expr newBVOrExpr(const std::vector<Expr>& kids) = 0; 00635 00636 virtual Expr newBVXorExpr(const Expr& t1, const Expr& t2) = 0; 00637 virtual Expr newBVXorExpr(const std::vector<Expr>& kids) = 0; 00638 00639 virtual Expr newBVXnorExpr(const Expr& t1, const Expr& t2) = 0; 00640 virtual Expr newBVXnorExpr(const std::vector<Expr>& kids) = 0; 00641 00642 virtual Expr newBVNandExpr(const Expr& t1, const Expr& t2) = 0; 00643 virtual Expr newBVNorExpr(const Expr& t1, const Expr& t2) = 0; 00644 00645 // Unsigned bitvector inequalities 00646 virtual Expr newBVLTExpr(const Expr& t1, const Expr& t2) = 0; 00647 virtual Expr newBVLEExpr(const Expr& t1, const Expr& t2) = 0; 00648 00649 // Signed bitvector inequalities 00650 virtual Expr newBVSLTExpr(const Expr& t1, const Expr& t2) = 0; 00651 virtual Expr newBVSLEExpr(const Expr& t1, const Expr& t2) = 0; 00652 00653 // Sign-extend t1 to a total of len bits 00654 virtual Expr newSXExpr(const Expr& t1, int len) = 0; 00655 00656 // Bitvector arithmetic: unary minus, plus, subtract, multiply 00657 virtual Expr newBVUminusExpr(const Expr& t1) = 0; 00658 virtual Expr newBVSubExpr(const Expr& t1, const Expr& t2) = 0; 00659 //! 'numbits' is the number of bits in the result 00660 virtual Expr newBVPlusExpr(int numbits, const std::vector<Expr>& k) = 0; 00661 virtual Expr newBVMultExpr(int numbits, 00662 const Expr& t1, const Expr& t2) = 0; 00663 00664 // Left shift by r bits: result is old size + r bits 00665 virtual Expr newFixedLeftShiftExpr(const Expr& t1, int r) = 0; 00666 // Left shift by r bits: result is same size as t1 00667 virtual Expr newFixedConstWidthLeftShiftExpr(const Expr& t1, int r) = 0; 00668 // Logical right shift by r bits: result is same size as t1 00669 virtual Expr newFixedRightShiftExpr(const Expr& t1, int r) = 0; 00670 00671 /*@}*/ // End of Bitvector expression methods 00672 00673 /***************************************************************************/ 00674 /*! 00675 *\name Other expression methods 00676 * Methods for manipulating other kinds of expressions 00677 *@{ 00678 */ 00679 /***************************************************************************/ 00680 00681 //! Tuple expression 00682 virtual Expr tupleExpr(const std::vector<Expr>& exprs) = 0; 00683 00684 //! Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5) 00685 virtual Expr tupleSelectExpr(const Expr& tuple, int index) = 0; 00686 00687 //! Tuple update; equivalent to "tuple WITH index := newValue" 00688 virtual Expr tupleUpdateExpr(const Expr& tuple, int index, 00689 const Expr& newValue) = 0; 00690 00691 //! Datatype constructor expression 00692 virtual Expr datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args) = 0; 00693 00694 //! Datatype selector expression 00695 virtual Expr datatypeSelExpr(const std::string& selector, const Expr& arg) = 0; 00696 00697 //! Datatype tester expression 00698 virtual Expr datatypeTestExpr(const std::string& constructor, const Expr& arg) = 0; 00699 00700 //! Universal quantifier 00701 virtual Expr forallExpr(const std::vector<Expr>& vars, const Expr& body) = 0; 00702 00703 //! Existential quantifier 00704 virtual Expr existsExpr(const std::vector<Expr>& vars, const Expr& body) = 0; 00705 00706 //! Lambda-expression 00707 virtual Op lambdaExpr(const std::vector<Expr>& vars, const Expr& body) = 0; 00708 00709 //! Symbolic simulation expression 00710 /*! 00711 * \param f is the next state function (LAMBDA-expression) 00712 * \param s0 is the initial state 00713 * \param inputs is the vector of LAMBDA-expressions representing 00714 * the sequences of inputs to f 00715 * \param n is a constant, the number of cycles to run the simulation. 00716 */ 00717 virtual Expr simulateExpr(const Expr& f, const Expr& s0, 00718 const std::vector<Expr>& inputs, 00719 const Expr& n) = 0; 00720 00721 /*@}*/ // End of Other expression methods 00722 00723 /***************************************************************************/ 00724 /*! 00725 *\name Validity checking methods 00726 * Methods related to validity checking 00727 * 00728 * This group includes methods for asserting formulas, checking 00729 * validity in the given logical context, manipulating the scope 00730 * level of the context, etc. 00731 *@{ 00732 */ 00733 /***************************************************************************/ 00734 00735 //! Set the resource limit (0==unlimited, 1==exhausted). 00736 /*! Currently, the limit is the total number of processed facts. */ 00737 virtual void setResourceLimit(unsigned limit) = 0; 00738 00739 //! Assert a new formula in the current context. 00740 /*! This creates the assumption e |- e. The formula must have Boolean type. 00741 */ 00742 virtual void assertFormula(const Expr& e) = 0; 00743 00744 //! Register an atomic formula of interest. 00745 /*! Registered atoms are tracked by the decision procedures. If one of them 00746 is deduced to be true or false, it is added to a list of implied literals. 00747 Implied literals can be retrieved with the getImpliedLiteral function */ 00748 virtual void registerAtom(const Expr& e) = 0; 00749 00750 //! Return next literal implied by last assertion. Null Expr if none. 00751 /*! Returned literals are either registered atomic formulas or their negation 00752 */ 00753 virtual Expr getImpliedLiteral() = 0; 00754 00755 //! Simplify e with respect to the current context 00756 virtual Expr simplify(const Expr& e) = 0; 00757 00758 //! Check validity of e in the current context. 00759 /*! If it returns VALID, the scope and context are the same 00760 * as when called. If it returns INVALID, the context will be one which 00761 * falsifies the query. If it returns UNKNOWN, the context will falsify the 00762 * query, but the context may be inconsistent. Finally, if it returns 00763 * ABORT, the context will be one which satisfies as much as possible. 00764 * 00765 * \param e is the queried formula 00766 */ 00767 virtual QueryResult query(const Expr& e) = 0; 00768 00769 //! Check satisfiability of the expr in the current context. 00770 /*! Equivalent to query(!e) */ 00771 virtual QueryResult checkUnsat(const Expr& e) = 0; 00772 00773 //! Get the next model 00774 /*! This method should only be called after a query which returns 00775 INVALID. Its return values are as for query(). */ 00776 virtual QueryResult checkContinue() = 0; 00777 00778 //! Restart the most recent query with e as an additional assertion. 00779 /*! This method should only be called after a query which returns 00780 INVALID. Its return values are as for query(). */ 00781 virtual QueryResult restart(const Expr& e) = 0; 00782 00783 //! Returns to context immediately before last invalid query. 00784 /*! This method should only be called after a query which returns false. 00785 */ 00786 virtual void returnFromCheck() = 0; 00787 00788 //! Get assumptions made by the user in this and all previous contexts. 00789 /*! User assumptions are created either by calls to assertFormula or by a 00790 * call to query. In the latter case, the negated query is added as an 00791 * assumption. 00792 * \param assumptions should be empty on entry. 00793 */ 00794 virtual void getUserAssumptions(std::vector<Expr>& assumptions) = 0; 00795 00796 //! Get assumptions made internally in this and all previous contexts. 00797 /*! Internal assumptions are literals assumed by the sat solver. 00798 * \param assumptions should be empty on entry. 00799 */ 00800 virtual void getInternalAssumptions(std::vector<Expr>& assumptions) = 0; 00801 00802 //! Get all assumptions made in this and all previous contexts. 00803 /*! \param assumptions should be empty on entry. 00804 */ 00805 virtual void getAssumptions(std::vector<Expr>& assumptions) = 0; 00806 00807 //! Returns the set of assumptions used in the proof of queried formula. 00808 /*! It returns a subset of getAssumptions(). If the last query was false 00809 * or there has not yet been a query, it does nothing. 00810 * \param assumptions should be empty on entry. 00811 */ 00812 virtual void getAssumptionsUsed(std::vector<Expr>& assumptions) = 0; 00813 00814 //! Return the internal assumptions that make the queried formula false. 00815 /*! This method should only be called after a query which returns 00816 false. It will try to return the simplest possible subset of 00817 the internal assumptions sufficient to make the queried expression 00818 false. 00819 \param assumptions should be empty on entry. 00820 \param inOrder if true, returns the assumptions in the order they 00821 were made. This is slightly more expensive than inOrder = false. 00822 */ 00823 virtual void getCounterExample(std::vector<Expr>& assumptions, 00824 bool inOrder=true) = 0; 00825 00826 //! Will assign concrete values to all user created variables 00827 /*! This function should only be called after a query which return false. 00828 */ 00829 virtual void getConcreteModel(ExprMap<Expr> & m) = 0; 00830 00831 //! Returns true if the current context is inconsistent. 00832 /*! Also returns a minimal set of assertions used to determine the 00833 inconsistency. 00834 \param assumptions should be empty on entry. 00835 */ 00836 virtual bool inconsistent(std::vector<Expr>& assumptions) = 0; 00837 00838 //! Returns true if the invalid result from last query() is imprecise 00839 /*! 00840 * Some decision procedures in CVC are incomplete (quantifier 00841 * elimination, non-linear arithmetic, etc.). If any incomplete 00842 * features were used during the last query(), and the result is 00843 * "invalid" (query() returns false), then this result is 00844 * inconclusive. It means that the system gave up the search for 00845 * contradiction at some point. 00846 */ 00847 virtual bool incomplete() = 0; 00848 00849 //! Returns true if the invalid result from last query() is imprecise 00850 /*! 00851 * \sa incomplete() 00852 * 00853 * The argument is filled with the reasons for incompleteness (they 00854 * are intended to be shown to the end user). 00855 */ 00856 virtual bool incomplete(std::vector<std::string>& reasons) = 0; 00857 00858 //! Returns the proof term for the last proven query 00859 /*! If there has not been a successful query, it should return a NULL proof 00860 */ 00861 virtual Proof getProof() = 0; 00862 00863 //! Returns the TCC of the last assumption or query 00864 /*! Returns Null if no assumptions or queries were performed. */ 00865 virtual Expr getTCC() = 0; 00866 00867 //! Return the set of assumptions used in the proof of the last TCC 00868 virtual void getAssumptionsTCC(std::vector<Expr>& assumptions) = 0; 00869 00870 //! Returns the proof of TCC of the last assumption or query 00871 /*! Returns Null if no assumptions or queries were performed. */ 00872 virtual Proof getProofTCC() = 0; 00873 00874 //! After successful query, return its closure |- Gamma => phi 00875 /*! Turn a valid query Gamma |- phi into an implication 00876 * |- Gamma => phi. 00877 * 00878 * Returns Null if last query was invalid. 00879 */ 00880 virtual Expr getClosure() = 0; 00881 00882 //! Construct a proof of the query closure |- Gamma => phi 00883 /*! Returns Null if last query was Invalid. */ 00884 virtual Proof getProofClosure() = 0; 00885 00886 /*@}*/ // End of Validity checking methods 00887 00888 /***************************************************************************/ 00889 /*! 00890 *\name Context methods 00891 * Methods for manipulating contexts 00892 * 00893 * Contexts support stack-based push and pop. There are two 00894 * separate notions of the current context stack. stackLevel(), push(), 00895 * pop(), and popto() work with the user-level notion of the stack. 00896 * 00897 * scopeLevel(), pushScope(), popScope(), and poptoScope() work with 00898 * the internal stack which is more fine-grained than the user 00899 * stack. 00900 * 00901 * Do not use the scope methods unless you know what you are doing. 00902 * *@{ 00903 */ 00904 /***************************************************************************/ 00905 00906 //! Returns the current stack level. Initial level is 0. 00907 virtual int stackLevel() = 0; 00908 00909 //! Checkpoint the current context and increase the scope level 00910 virtual void push() = 0; 00911 00912 //! Restore the current context to its state at the last checkpoint 00913 virtual void pop() = 0; 00914 00915 //! Restore the current context to the given stackLevel. 00916 /*! 00917 \param stackLevel should be greater than or equal to 0 and less 00918 than or equal to the current scope level. 00919 */ 00920 virtual void popto(int stackLevel) = 0; 00921 00922 //! Returns the current scope level. Initially, the scope level is 1. 00923 virtual int scopeLevel() = 0; 00924 00925 /*! @brief Checkpoint the current context and increase the 00926 * <strong>internal</strong> scope level. Do not use unless you 00927 * know what you're doing! 00928 */ 00929 virtual void pushScope() = 0; 00930 00931 /*! @brief Restore the current context to its state at the last 00932 * <strong>internal</strong> checkpoint. Do not use unless you know 00933 * what you're doing! 00934 */ 00935 virtual void popScope() = 0; 00936 00937 //! Restore the current context to the given scopeLevel. 00938 /*! 00939 \param scopeLevel should be less than or equal to the current scope level. 00940 00941 If scopeLevel is less than 1, then the current context is reset 00942 and the scope level is set to 1. 00943 */ 00944 virtual void poptoScope(int scopeLevel) = 0; 00945 00946 //! Get the current context 00947 virtual Context* getCurrentContext() = 0; 00948 00949 /*@}*/ // End of Context methods 00950 00951 /***************************************************************************/ 00952 /*! 00953 *\name Reading files 00954 * Methods for reading external files 00955 *@{ 00956 */ 00957 /***************************************************************************/ 00958 00959 //! Read and execute the commands from a file given by name ("" means stdin) 00960 virtual void loadFile(const std::string& fileName, 00961 InputLanguage lang = PRESENTATION_LANG, 00962 bool interactive = false) = 0; 00963 00964 //! Read and execute the commands from a stream 00965 virtual void loadFile(std::istream& is, 00966 InputLanguage lang = PRESENTATION_LANG, 00967 bool interactive = false) = 0; 00968 00969 /*@}*/ // End of methods for reading files 00970 00971 /***************************************************************************/ 00972 /*! 00973 *\name Reporting Statistics 00974 * Methods for collecting and reporting run-time statistics 00975 *@{ 00976 */ 00977 /***************************************************************************/ 00978 00979 //! Get statistics object 00980 virtual Statistics& getStatistics() = 0; 00981 00982 //! Print collected statistics to stdout 00983 virtual void printStatistics() = 0; 00984 00985 /*@}*/ // End of Statistics Methods 00986 00987 00988 }; // End of class ValidityChecker 00989 00990 } // End of namespace CVC3 00991 00992 #endif