CVC3

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