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