CVC3

theory.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theory.h
00004  * \brief Generic API for Theories plus methods commonly used by theories
00005  * 
00006  * Author: Clark Barrett
00007  * 
00008  * Created: Sat Nov 30 23:30:15 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__theory_h_
00023 #define _cvc3__include__theory_h_
00024 
00025 #include "expr_stream.h"
00026 #include "common_proof_rules.h"
00027 #include "cdlist.h"
00028 
00029 namespace CVC3 {
00030 
00031 class TheoryCore;
00032 class Theorem;
00033 class Type;
00034 
00035 /************************************************************************/
00036 /*!
00037  *\defgroup Theories Theories
00038  *\ingroup VC
00039  *\brief Theories
00040  *@{
00041  */
00042 /***********************************************************************/
00043 
00044 /*****************************************************************************/
00045 /*!
00046  *\anchor Theory
00047  *\class Theory
00048  *\brief Base class for theories
00049  *
00050  * Author: Clark Barrett
00051  *
00052  * Created: Thu Jan 30 16:37:56 2003
00053  *
00054  * This is an abstract class which all theories should inherit from.  In
00055  * addition to providing an abstract theory interface, it provides access
00056  * functions to core functionality.  However, in order to avoid duplicating the
00057  * data structures which implement this functionality, all the functionality is
00058  * stored in a separate class (which actually derives from this one) called
00059  * TheoryCore.  These two classes work closely together to provide the core
00060  * functionality.
00061  */
00062 /*****************************************************************************/
00063 
00064 class Theory {
00065   friend class TheoryCore;
00066 private:
00067   ExprManager* d_em;
00068   TheoryCore* d_theoryCore; //!< Provides the core functionality
00069   CommonProofRules* d_commonRules; //!< Commonly used proof rules
00070   std::string d_name; //!< Name of the theory (for debugging)
00071 
00072   //! Private default constructor.
00073   /*! Everyone besides TheoryCore has to use the public constructor
00074     which sets up all the provided functionality automatically.
00075   */
00076   Theory(void);
00077 
00078 protected:
00079   bool d_theoryUsed; //! Whether theory has been used (for smtlib translator)
00080 
00081 public:
00082   //! Exposed constructor.
00083   /*! Note that each instance of Theory must have a name (mostly for
00084     debugging purposes). */
00085   Theory(TheoryCore* theoryCore, const std::string& name);
00086   //! Destructor
00087   virtual ~Theory(void);
00088 
00089   //! Access to ExprManager
00090   ExprManager* getEM() { return d_em; }
00091 
00092   //! Get a pointer to theoryCore
00093   TheoryCore* theoryCore() { return d_theoryCore; }
00094 
00095   //! Get a pointer to common proof rules
00096   CommonProofRules* getCommonRules() { return d_commonRules; }
00097 
00098   //! Get the name of the theory (for debugging purposes)
00099   const std::string& getName() const { return d_name; }
00100 
00101   //! Set the "used" flag on this theory (for smtlib translator)
00102   virtual void setUsed() { d_theoryUsed = true; }
00103   //! Get whether theory has been used (for smtlib translator)
00104   virtual bool theoryUsed() { return d_theoryUsed; }
00105 
00106   /***************************************************************************/
00107   /*!
00108    *\defgroup Theory_API Abstract Theory Interface
00109    *\anchor theory_api
00110    *\ingroup Theories
00111    *\brief Abstract Theory Interface
00112    *
00113    * These are the theory-specific methods which provide the decision procedure
00114    * functionality for a new theory.  At the very least, a theory must
00115    * implement the checkSat method.  The other methods can be used to make the
00116    * implementation more convenient.  For more information on this API, see
00117    * Clark Barrett's PhD dissertation and \ref theory_api_howto.
00118    *@{
00119    */
00120   /***************************************************************************/
00121 
00122   //! Notify theory of a new shared term
00123   /*! When a term e associated with theory i occurs as a child of an expression
00124     associated with theory j, the framework calls i->addSharedTerm(e) and
00125     j->addSharedTerm(e)
00126   */
00127   virtual void addSharedTerm(const Expr& e) {}
00128 
00129   //! Assert a new fact to the decision procedure
00130   /*! Each fact that makes it into the core framework is assigned to exactly
00131     one theory: the theory associated with that fact.  assertFact is called to
00132     inform the theory that a new fact has been assigned to the theory.
00133   */
00134   virtual void assertFact(const Theorem& e) = 0;
00135 
00136   //! Check for satisfiability in the theory
00137   /*! \param fullEffort when it is false, checkSat can do as much or
00138    as little work as it likes, though simple inferences and checks for
00139    consistency should be done to increase efficiency.  If fullEffort is true,
00140    checkSat must check whether the set of facts given by assertFact together
00141    with the arrangement of shared terms (provided by addSharedTerm) induced by
00142    the global find database equivalence relation are satisfiable.  If
00143    satisfiable, checkSat does nothing.
00144 
00145    If satisfiability can be acheived by merging some of the shared terms, a new
00146    fact must be enqueued using enqueueFact (this fact need not be a literal).
00147    If there is no way to make things satisfiable, setInconsistent must be called.
00148   */
00149   virtual void checkSat(bool fullEffort) = 0;
00150 
00151   //! Theory-specific rewrite rules.  
00152   /*! By default, rewrite just returns a reflexive theorem stating that the
00153     input expression is equivalent to itself.  However, rewrite is allowed to
00154     return any theorem which describes how the input expression is equivalent
00155     to some new expression.  rewrite should be used to perform simplifications,
00156     normalization, and any other preprocessing on theory-specific expressions
00157     that needs to be done.
00158   */
00159   virtual Theorem rewrite(const Expr& e) { return reflexivityRule(e); }
00160 
00161   //! Theory-specific preprocessing
00162   /*! This gets called each time a new assumption or query is preprocessed.
00163     By default it does nothing. */
00164   virtual Theorem theoryPreprocess(const Expr& e) { return reflexivityRule(e); }
00165 
00166   //! Set up the term e for call-backs when e or its children change.
00167   /*! setup is called once for each expression associated with the theory.  It
00168     is typically used to setup theory-specific data for an expression and to
00169     add call-back information for use with update.
00170     \sa update
00171   */
00172   virtual void setup(const Expr& e) {}
00173 
00174   //! Notify a theory of a new equality
00175   /*! update is a call-back used by the notify mechanism of the core theory.
00176     It works as follows.  When an equation t1 = t2 makes it into the core
00177     framework, the two find equivalence classes for t1 and t2 are merged.  The
00178     result is that t2 is the new equivalence class representative and t1 is no
00179     longer an equivalence class representative.  When this happens, the notify
00180     list of t1 is traversed.  Notify list entries consist of a theory and an
00181     expression d.  For each entry (i,d), i->update(e, d) is called, where e is
00182     the theorem corresponding to the equality t1=t2.
00183 
00184     To add the entry (i,d) to a term t1's notify list, a call must be made to
00185     t1.addNotify(i,d).  This is typically done in setup.
00186 
00187     \sa setup
00188   */
00189   virtual void update(const Theorem& e, const Expr& d) {}
00190 
00191   //! An optional solver.
00192   /*! The solve method can be used to implement a Shostak-style solver.  Since
00193     solvers do not in general combine, the following technique is used.  One
00194     theory is designated as the primary solver (in our case, it is the theory
00195     of arithmetic).  For each equation that enters the core framework, the
00196     primary solver is called to ensure that the equation is in solved form with
00197     respect to the primary theory.
00198 
00199     After the primary solver, the solver for the theory associated with the
00200     equation is called.  This solver can do whatever it likes, as long as the
00201     result is still in solved form with respect to the primary solver.  This is
00202     a slight generalization of what is described in my (Clark)'s PhD thesis.
00203   */
00204   virtual Theorem solve(const Theorem& e) { return e; }
00205   //! A debug check used by the primary solver
00206   virtual void checkAssertEqInvariant(const Theorem& e) { }
00207 
00208   /////////////////////////////////
00209   // Extensions to original API: //
00210   /////////////////////////////////
00211 
00212   //! Recursive simplification step
00213   /*!
00214    * INVARIANT: the result is a Theorem(e=e'), where e' is a fully
00215    * simplified version of e.  To simplify subexpressions recursively,
00216    * call simplify() function.
00217    *
00218    * This theory-specific method is called when the simplifier
00219    * descends top-down into the expression.  Normally, every kid is
00220    * simplified recursively, and the results are combined into the new
00221    * parent with the same operator (Op).  This functionality is
00222    * provided with the default implementation.
00223    *
00224    * However, in some expressions some kids may not matter in the
00225    * result, and can be skipped.  For instance, if the first kid in a
00226    * long AND simplifies to FALSE, then the entire expression
00227    * simplifies to FALSE, and the remaining kids do not need to be
00228    * simplified.
00229    *
00230    * This call is a chance for a DP to provide these types of
00231    * optimizations during the top-down phase of simplification.
00232    */
00233   virtual Theorem simplifyOp(const Expr& e);
00234 
00235   //! Check that e is a valid Type expr
00236   virtual void checkType(const Expr& e)
00237     { throw Exception("Cannot construct type from expr: "+e.toString()); }
00238 
00239   //! Compute information related to finiteness of types
00240   /*! Used by the TypeComputer defined in TheoryCore (theories should not call this
00241    *  funtion directly -- they should use the methods in Type instead).  Each theory
00242    *  should implement this if it contains any types that could be non-infinite.
00243    *
00244    * 1. Returns Cardinality of the type (finite, infinite, or unknown)
00245    * 2. If cardinality = finite and enumerate is true,
00246    *    sets e to the nth element of the type if it can
00247    *    sets e to NULL if n is out of bounds or if unable to compute nth element
00248    * 3. If cardinality = finite and computeSize is true,
00249    *    sets n to the size of the type if it can
00250    *    sets n to 0 otherwise
00251    */
00252   virtual Cardinality finiteTypeInfo(Expr& e, Unsigned& n,
00253                                      bool enumerate, bool computeSize)
00254   { return CARD_INFINITE; }
00255 
00256   //! Compute and store the type of e
00257   /*!
00258    * \param e is the expression whose type is computed.  
00259    *
00260    * This function computes the type of the top-level operator of e,
00261    * and recurses into children using getType(), if necessary.
00262    */
00263   virtual void computeType(const Expr& e) {}
00264   //! Compute the base type of the top-level operator of an arbitrary type
00265   virtual Type computeBaseType(const Type& tp) { return tp; }
00266   /*! @brief  Theory specific computation of the subtyping predicate for 
00267    *  type t applied to the expression e.
00268    */ 
00269   /*! By default returns true. Each theory needs to compute subtype predicates
00270    *  for the types associated with it. So, for example, the theory of records
00271    *  will take a record type [# f1: T1, f2: T2 #] and an expression e
00272    *  and will return the subtyping predicate for e, namely:
00273    *  computeTypePred(T1, e.f1) AND computeTypePred(T2, e.f2)
00274    */ 
00275   virtual Expr computeTypePred(const Type& t, const Expr& e) 
00276     { return e.getEM()->trueExpr(); }
00277   //! Compute and cache the TCC of e.
00278   /*! 
00279    * \param e is an expression (term or formula).  This function
00280    * computes the TCC of e which is true iff the expression is defined.
00281    *
00282    * This function computes the TCC or predicate of the top-level
00283    * operator of e, and recurses into children using getTCC(), if
00284    * necessary.
00285    *
00286    * The default implementation is to compute TCCs recursively for all
00287    * children, and return their conjunction.
00288    */
00289   virtual Expr computeTCC(const Expr& e);
00290 
00291   //! Theory-specific parsing implemented by the DP
00292   virtual Expr parseExprOp(const Expr& e) { return e; }
00293 
00294   //! Theory-specific pretty-printing.
00295   /*! By default, print the top node in AST, and resume
00296     pretty-printing the children.  The same call e.print(os) can be
00297     used in DP-specific printers to use AST printing for the given
00298     node.  In fact, it is strongly recommended to add e.print(os) as
00299     the default for all the cases/kinds that are not handled by the
00300     particular pretty-printer.
00301   */
00302   virtual ExprStream& print(ExprStream& os, const Expr& e) {
00303     return e.printAST(os);
00304   }
00305 
00306   //! Add variables from 'e' to 'v' for constructing a concrete model
00307   /*! If e is already of primitive type, do NOT add it to v. */
00308   virtual void computeModelTerm(const Expr& e, std::vector<Expr>& v);
00309   //! Process disequalities from the arrangement for model generation
00310   virtual void refineCounterExample() {}
00311   //! Assign concrete values to basic-type variables in v
00312   virtual void computeModelBasic(const std::vector<Expr>& v) {}
00313   //! Compute the value of a compound variable from the more primitive ones
00314   /*! The more primitive variables for e are already assigned concrete
00315    * values, and are available through getModelValue().
00316    *
00317    * The new value for e must be assigned using assignValue() method.
00318    *
00319    * \param e is the compound type expression to assign a value;
00320    *
00321    * \param vars are the variables actually assigned.  Normally, 'e'
00322    * is the only element of vars.  However, e.g. in the case of
00323    * uninterpreted functions, assigning 'f' means assigning all
00324    * relevant applications of 'f' to constant values (f(0), f(5),
00325    * etc.).  Such applications might not be known before the model is
00326    * constructed (they may be of the form f(x), f(y+z), etc., where
00327    * x,y,z are still unassigned).
00328    *
00329    * Populating 'vars' is an opportunity for a DP to change the set of
00330    * top-level "variables" to assign, if needed.  In particular, it
00331    * may drop 'e' from the model entirely, if it is already a concrete
00332    * value by itself.
00333    */
00334   virtual void computeModel(const Expr& e, std::vector<Expr>& vars) {
00335     assignValue(find(e));
00336     vars.push_back(e);
00337   }
00338 
00339   //! Receives all the type predicates for the types of the given theory
00340   /*! Type predicates may be expensive to enqueue eagerly, and DPs may
00341     choose to postpone them, or transform them to something more
00342     efficient.  By default, the asserted type predicate is
00343     immediately enqueued as a new fact.
00344 
00345     Note: Used only by bitvector theory.
00346 
00347     \param e is the expression for which the type predicate is computed
00348     \param pred is the predicate theorem P(e)
00349   */
00350   virtual void assertTypePred(const Expr& e, const Theorem& pred)
00351     { enqueueFact(pred); }
00352 
00353   //! Theory-specific rewrites for atomic formulas
00354   /*! The intended use is to convert complex atomic formulas into an
00355    * equivalent Boolean combination of simpler formulas.  Such
00356    * conversion may be harmful for algebraic rewrites, and is not
00357    * always desirable to have in rewrite() method.
00358    *
00359    * Note: Used only by bitvector theory and rewriteLiteral in core.
00360    *
00361    * However, if rewrite() alone cannot solve the problem, and the SAT
00362    * solver needs to be envoked, these additional rewrites may ease
00363    * the job for the SAT solver.
00364    */
00365   virtual Theorem rewriteAtomic(const Expr& e) { return reflexivityRule(e); }
00366 
00367   //! Notification of conflict
00368   /*!
00369    * Decision procedures implement this method when they want to be
00370    * notified about a conflict.
00371    *
00372    * Note: Used only by quantifier theory
00373    *
00374    * \param thm is the theorem of FALSE given to setInconsistent()
00375    */
00376   virtual void notifyInconsistent(const Theorem& thm) { }
00377 
00378   virtual void registerAtom(const Expr& e, const Theorem& thm);
00379 
00380   //! Theory-specific registration of atoms
00381   /*!
00382    * If a theory wants to implement its own theory propagation, it
00383    * should implement this method and use it to collect all atoms
00384    * that the core is interested in.  If the theory can deduce the atom
00385    * or its negation, it should do so (using enqueueFact).
00386    */
00387   virtual void registerAtom(const Expr& e) { }
00388 
00389 
00390 #ifdef _CVC3_DEBUG_MODE
00391   //! Theory-specific debug function
00392   virtual void debug(int i) { }
00393   //! help function, as debug(int i). yeting
00394   virtual int help(int i) { return 9999 ;} ;
00395 #endif
00396 
00397   /*@}*/ // End of Theory_API group
00398 
00399   /***************************************************************************/
00400   /*!
00401    *\name Core Framework Functionality
00402    * These methods provide convenient access to core functionality for the
00403    * benefit of decision procedures.
00404    *@{
00405    */
00406   /***************************************************************************/
00407 
00408   //! Check if the current context is inconsistent
00409   virtual bool inconsistent();
00410   //! Make the context inconsistent; The formula proved by e must FALSE.
00411   virtual void setInconsistent(const Theorem& e);
00412 
00413   //! Mark the current decision branch as possibly incomplete
00414   /*!
00415    * This should be set when a decision procedure uses an incomplete
00416    * algorithm, and cannot guarantee satisfiability after the final
00417    * checkSat() call with full effort.  An example would be
00418    * instantiation of universal quantifiers.
00419    *
00420    * A decision procedure can provide a reason for incompleteness,
00421    * which will be reported back to the user.
00422    */
00423   virtual void setIncomplete(const std::string& reason);
00424 
00425   //! Simplify a term e and return a Theorem(e==e')
00426   /*! \sa simplifyExpr() */
00427   virtual Theorem simplify(const Expr& e);
00428   //! Simplify a term e w.r.t. the current context
00429   /*! \sa simplify */
00430   Expr simplifyExpr(const Expr& e)
00431     { return simplify(e).getRHS(); }
00432 
00433   //! Submit a derived fact to the core from a decision procedure
00434   /*! \param e is the Theorem for the new fact 
00435    */
00436   virtual void enqueueFact(const Theorem& e);
00437   virtual void enqueueSE(const Theorem& e);
00438 
00439   //! Handle new equalities (usually asserted through addFact)
00440   /*!
00441    * INVARIANT: the Theorem 'e' is an equality e1==e2, where e2 is
00442    * i-leaf simplified in the current context, or a conjunction of
00443    * such equalities.
00444    *
00445    */
00446   virtual void assertEqualities(const Theorem& e);
00447 
00448   //! Parse the generic expression.
00449   /*! This method should be used in parseExprOp() for recursive calls
00450    *  to subexpressions, and is the method called by the command
00451    *  processor.
00452    */
00453   virtual Expr parseExpr(const Expr& e);
00454 
00455   //! Assigns t a concrete value val.  Used in model generation.
00456   virtual void assignValue(const Expr& t, const Expr& val);
00457   //! Record a derived assignment to a variable (LHS).
00458   virtual void assignValue(const Theorem& thm);
00459 
00460   /*@}*/ // End of Core Framework Functionality
00461 
00462   /***************************************************************************/
00463   /*!
00464    *\name Theory Helper Methods
00465    * These methods provide basic functionality needed by all theories.
00466    *@{
00467    */
00468   /***************************************************************************/
00469 
00470   //! Register new kinds with the given theory
00471   void registerKinds(Theory* theory, std::vector<int>& kinds);
00472   //! Unregister kinds for a theory
00473   void unregisterKinds(Theory* theory, std::vector<int>& kinds);
00474   //! Register a new theory
00475   void registerTheory(Theory* theory, std::vector<int>& kinds,
00476           bool hasSolver=false);
00477   //! Unregister a theory
00478   void unregisterTheory(Theory* theory, std::vector<int>& kinds,
00479                         bool hasSolver);
00480 
00481   //! Return the number of registered theories
00482   int getNumTheories();
00483 
00484   //! Test whether a kind maps to any theory
00485   bool hasTheory(int kind);
00486   //! Return the theory associated with a kind
00487   Theory* theoryOf(int kind);
00488   //! Return the theory associated with a type
00489   Theory* theoryOf(const Type& e);
00490   //! Return the theory associated with an Expr
00491   Theory* theoryOf(const Expr& e);
00492 
00493   //! Return the theorem that e is equal to its find
00494   Theorem find(const Expr& e);
00495   //! Return the find as a reference: expr must have a find
00496   const Theorem& findRef(const Expr& e);
00497 
00498   //! Return find-reduced version of e
00499   Theorem findReduce(const Expr& e);
00500   //! Return true iff e is find-reduced
00501   bool findReduced(const Expr& e);
00502   //! Return the find of e, or e if it has no find
00503   inline Expr findExpr(const Expr& e)
00504     { return e.hasFind() ? find(e).getRHS() : e; }
00505 
00506   //! Compute the TCC of e, or the subtyping predicate, if e is a type
00507   Expr getTCC(const Expr& e);
00508   //! Compute (or look up in cache) the base type of e and return the result
00509   Type getBaseType(const Expr& e);
00510   //! Compute the base type from an arbitrary type
00511   Type getBaseType(const Type& tp);
00512   //! Calls the correct theory to compute a type predicate
00513   Expr getTypePred(const Type& t, const Expr& e);
00514 
00515   //! Update the children of the term e
00516   /*! When a decision procedure receives a call to update() because a
00517     child of a term 'e' has changed, this method can be called to
00518     compute the new value of 'e'.
00519     \sa update
00520   */
00521   Theorem updateHelper(const Expr& e);
00522   //! Setup a term for congruence closure (must have sig and rep attributes)
00523   void setupCC(const Expr& e);
00524   //! Update a term w.r.t. congruence closure (must be setup with setupCC())
00525   void updateCC(const Theorem& e, const Expr& d);
00526   //! Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
00527   Theorem rewriteCC(const Expr& e);
00528 
00529   /*! @brief Calls the correct theory to get all of the terms that
00530     need to be assigned values in the concrete model */
00531   void getModelTerm(const Expr& e, std::vector<Expr>& v);
00532   //! Fetch the concrete assignment to the variable during model generation
00533   Theorem getModelValue(const Expr& e);
00534 
00535   //! Suggest a splitter to the SearchEngine
00536   void addSplitter(const Expr& e, int priority = 0);
00537 
00538   //! Add a global lemma
00539   void addGlobalLemma(const Theorem& thm, int priority = 0);
00540 
00541   /*@}*/ // End of Theory Helper Methods
00542 
00543   /***************************************************************************/
00544   /*!
00545    *\name Core Testers
00546    *@{
00547    */
00548   /***************************************************************************/
00549 
00550   //! Test if e is an i-leaf term for the current theory
00551   /*! A term 'e' is an i-leaf for a theory 'i', if it is a variable,
00552     or 'e' belongs to a different theory.  This definition makes sense
00553     for a larger term which by itself belongs to the current theory
00554     'i', but (some of) its children are variables or belong to
00555     different theories. */
00556   bool isLeaf(const Expr& e) { return e.isVar() || theoryOf(e) != this; }
00557 
00558   //! Test if e1 is an i-leaf in e2
00559   /*! \sa isLeaf */
00560   bool isLeafIn(const Expr& e1, const Expr& e2);
00561 
00562   //! Test if all i-leaves of e are simplified
00563   /*! \sa isLeaf */
00564   bool leavesAreSimp(const Expr& e);
00565 
00566   /*@}*/ // End of Core Testers
00567 
00568   /***************************************************************************/
00569   /*!
00570    *\name Common Type and Expr Methods
00571    *@{
00572    */
00573   /***************************************************************************/
00574 
00575   //! Return BOOLEAN type
00576   Type boolType() { return Type::typeBool(d_em); }
00577 
00578   //! Return FALSE Expr
00579   const Expr& falseExpr() { return d_em->falseExpr(); }
00580 
00581   //! Return TRUE Expr
00582   const Expr& trueExpr() { return d_em->trueExpr(); }
00583 
00584   //! Create a new variable given its name and type
00585   /*! Add the variable to the database for resolving IDs in parseExpr
00586    */
00587   Expr newVar(const std::string& name, const Type& type);
00588   //! Create a new named expression given its name, type, and definition
00589   /*! Add the definition to the database for resolving IDs in parseExpr
00590    */
00591   Expr newVar(const std::string& name, const Type& type, const Expr& def);
00592 
00593   //! Create a new uninterpreted function
00594   /*! Add the definition to the database for resolving IDs in parseExpr
00595    */
00596   Op newFunction(const std::string& name, const Type& type,
00597                  bool computeTransClosure);
00598 
00599   //! Look up a function by name.
00600   /*! Returns the function and sets type to the type of the function if it
00601    * exists.  If not, returns a NULL Op object.
00602    */
00603   Op lookupFunction(const std::string& name, Type* type);
00604 
00605   //! Create a new defined function
00606   /*! Add the definition to the database for resolving IDs in parseExpr
00607    */
00608   Op newFunction(const std::string& name, const Type& type, const Expr& def);
00609 
00610   //! Create and add a new bound variable to the stack, for parseExprOp().
00611   /*!
00612    * The stack is popped automatically upon return from the
00613    * parseExprOp() which used this method.
00614    *
00615    * Bound variable names may repeat, in which case the latest
00616    * declaration takes precedence.
00617    */
00618   Expr addBoundVar(const std::string& name, const Type& type);
00619   //! Create and add a new bound named def to the stack, for parseExprOp().
00620   /*!
00621    * The stack is popped automatically upon return from the
00622    * parseExprOp() which used this method.
00623    *
00624    * Bound variable names may repeat, in which case the latest
00625    * declaration takes precedence.
00626    *
00627    * The type may be Null, but 'def' must always be a valid Expr
00628    */
00629   Expr addBoundVar(const std::string& name, const Type& type, const Expr& def);
00630 
00631   /*! @brief Lookup variable and return it and its type.  Return NULL Expr if
00632     it doesn't exist yet. */
00633   Expr lookupVar(const std::string& name, Type* type);
00634 
00635   //! Create a new uninterpreted type with the given name
00636   /*! Add the name to the global variable database d_globals
00637    */
00638   Type newTypeExpr(const std::string& name);
00639   //! Lookup type by name.  Return Null if no such type exists.
00640   Type lookupTypeExpr(const std::string& name);
00641   //! Create a new type abbreviation with the given name 
00642   Type newTypeExpr(const std::string& name, const Type& def);
00643 
00644   //! Create a new subtype expression
00645   Type newSubtypeExpr(const Expr& pred, const Expr& witness);
00646 
00647   //! Resolve an identifier, for use in parseExprOp()
00648   /*!
00649    * First, search the bound variable stack, and if the name is not
00650    * found, search the global constant and type declarations.  
00651    *
00652    * \return an expression to use in place of the identifier, or Null
00653    * if cannot resolve the name.
00654    */
00655   Expr resolveID(const std::string& name);
00656 
00657   //! Install name as a new identifier associated with Expr e
00658   void installID(const std::string& name, const Expr& e);
00659 
00660   Theorem typePred(const Expr& e);
00661 
00662   /*@}*/ // End of Common Type and Expr Methods
00663 
00664   /***************************************************************************/
00665   /*!
00666    *\name Commonly Used Proof Rules
00667    *\anchor theory_api_core_proof_rules
00668    *@{
00669    */
00670   /***************************************************************************/
00671 
00672   //!  ==> a == a
00673   Theorem reflexivityRule(const Expr& a)
00674     { return d_commonRules->reflexivityRule(a); }
00675 
00676   //!  a1 == a2 ==> a2 == a1
00677   Theorem symmetryRule(const Theorem& a1_eq_a2)
00678     { return d_commonRules->symmetryRule(a1_eq_a2); }
00679 
00680   //! (a1 == a2) & (a2 == a3) ==> (a1 == a3)
00681   Theorem transitivityRule(const Theorem& a1_eq_a2,
00682          const Theorem& a2_eq_a3)
00683     { return d_commonRules->transitivityRule(a1_eq_a2, a2_eq_a3); }
00684 
00685   //! (c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
00686   Theorem substitutivityRule(const Op& op,
00687            const std::vector<Theorem>& thms)
00688     { return d_commonRules->substitutivityRule(op, thms); }
00689 
00690   //! Special case for unary operators
00691   Theorem substitutivityRule(const Expr& e,
00692                              const Theorem& t)
00693     { return d_commonRules->substitutivityRule(e, t); }
00694 
00695   //! Special case for binary operators
00696   Theorem substitutivityRule(const Expr& e,
00697                              const Theorem& t1,
00698                              const Theorem& t2)
00699     { return d_commonRules->substitutivityRule(e, t1, t2); }
00700 
00701   //! Optimized: only positions which changed are included
00702   Theorem substitutivityRule(const Expr& e,
00703            const std::vector<unsigned>& changed,
00704            const std::vector<Theorem>& thms)
00705     { return d_commonRules->substitutivityRule(e, changed, thms); }
00706 
00707   //! Optimized: only a single position changed
00708   Theorem substitutivityRule(const Expr& e,
00709                              int changed,
00710                              const Theorem& thm)
00711     { return d_commonRules->substitutivityRule(e, changed, thm); }
00712 
00713   //! e1 AND (e1 IFF e2) ==> e2
00714   Theorem iffMP(const Theorem& e1, const Theorem& e1_iff_e2) {
00715     return d_commonRules->iffMP(e1, e1_iff_e2);
00716   }
00717 
00718   //! ==> AND(e1,e2) IFF [simplified expr]
00719   Theorem rewriteAnd(const Expr& e) {
00720     return d_commonRules->rewriteAnd(e);
00721   }
00722 
00723   //! ==> OR(e1,...,en) IFF [simplified expr]
00724   Theorem rewriteOr(const Expr& e) {
00725     return d_commonRules->rewriteOr(e);
00726   }
00727   
00728   //! Derived rule for rewriting ITE
00729   Theorem rewriteIte(const Expr& e);
00730 
00731   //! Derived rule to create a new name for an expression
00732   Theorem renameExpr(const Expr& e);
00733   
00734   /*@}*/ // End of Commonly Used Proof Rules
00735 
00736 
00737 };
00738 
00739 /*@}*/ // End of group Theories
00740 
00741 }
00742 
00743 #endif