vc.h

Go to the documentation of this file.
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

Generated on Tue Jul 3 14:33:42 2007 for CVC3 by  doxygen 1.5.1