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   //! Set up the term e for call-backs when e or its children change.
00162   /*! setup is called once for each expression associated with the theory.  It
00163     is typically used to setup theory-specific data for an expression and to
00164     add call-back information for use with update.
00165     \sa update
00166   */
00167   virtual void setup(const Expr& e) {}
00168 
00169   //! Notify a theory of a new equality
00170   /*! update is a call-back used by the notify mechanism of the core theory.
00171     It works as follows.  When an equation t1 = t2 makes it into the core
00172     framework, the two find equivalence classes for t1 and t2 are merged.  The
00173     result is that t2 is the new equivalence class representative and t1 is no
00174     longer an equivalence class representative.  When this happens, the notify
00175     list of t1 is traversed.  Notify list entries consist of a theory and an
00176     expression d.  For each entry (i,d), i->update(e, d) is called, where e is
00177     the theorem corresponding to the equality t1=t2.
00178 
00179     To add the entry (i,d) to a term t1's notify list, a call must be made to
00180     t1.addNotify(i,d).  This is typically done in setup.
00181 
00182     \sa setup
00183   */
00184   virtual void update(const Theorem& e, const Expr& d) {}
00185 
00186   //! An optional solver.
00187   /*! The solve method can be used to implement a Shostak-style solver.  Since
00188     solvers do not in general combine, the following technique is used.  One
00189     theory is designated as the primary solver (in our case, it is the theory
00190     of arithmetic).  For each equation that enters the core framework, the
00191     primary solver is called to ensure that the equation is in solved form with
00192     respect to the primary theory.
00193 
00194     After the primary solver, the solver for the theory associated with the
00195     equation is called.  This solver can do whatever it likes, as long as the
00196     result is still in solved form with respect to the primary solver.  This is
00197     a slight generalization of what is described in my (Clark)'s PhD thesis.
00198   */
00199   virtual Theorem solve(const Theorem& e) { return e; }
00200   //! A debug check used by the primary solver
00201   virtual void checkAssertEqInvariant(const Theorem& e) { }
00202 
00203   /////////////////////////////////
00204   // Extensions to original API: //
00205   /////////////////////////////////
00206 
00207   //! Recursive simplification step
00208   /*!
00209    * INVARIANT: the result is a Theorem(e=e'), where e' is a fully
00210    * simplified version of e.  To simplify subexpressions recursively,
00211    * call simplify() function.
00212    *
00213    * This theory-specific method is called when the simplifier
00214    * descends top-down into the expression.  Normally, every kid is
00215    * simplified recursively, and the results are combined into the new
00216    * parent with the same operator (Op).  This functionality is
00217    * provided with the default implementation.
00218    *
00219    * However, in some expressions some kids may not matter in the
00220    * result, and can be skipped.  For instance, if the first kid in a
00221    * long AND simplifies to FALSE, then the entire expression
00222    * simplifies to FALSE, and the remaining kids do not need to be
00223    * simplified.
00224    *
00225    * This call is a chance for a DP to provide these types of
00226    * optimizations during the top-down phase of simplification.
00227    */
00228   virtual Theorem simplifyOp(const Expr& e);
00229 
00230   //! Check that e is a valid Type expr
00231   virtual void checkType(const Expr& e)
00232     { throw Exception("Cannot construct type from expr: "+e.toString()); }
00233 
00234   //! Compute and store the type of e
00235   /*!
00236    * \param e is the expression whose type is computed.  
00237    *
00238    * This function computes the type of the top-level operator of e,
00239    * and recurses into children using getType(), if necessary.
00240    */
00241   virtual void computeType(const Expr& e) {}
00242   //! Compute the base type of the top-level operator of an arbitrary type
00243   virtual Type computeBaseType(const Type& tp) { return tp; }
00244   /*! @brief  Theory specific computation of the subtyping predicate for 
00245    *  type t applied to the expression e.
00246    */ 
00247   /*! By default returns true. Each theory needs to compute subtype predicates
00248    *  for the types associated with it. So, for example, the theory of records
00249    *  will take a record type [# f1: T1, f2: T2 #] and an expression e
00250    *  and will return the subtyping predicate for e, namely:
00251    *  computeTypePred(T1, e.f1) AND computeTypePred(T2, e.f2)
00252    */ 
00253   virtual Expr computeTypePred(const Type& t, const Expr& e) 
00254     { return e.getEM()->trueExpr(); }
00255   //! Compute and cache the TCC of e.
00256   /*! 
00257    * \param e is an expression (term or formula).  This function
00258    * computes the TCC of e which is true iff the expression is defined.
00259    *
00260    * This function computes the TCC or predicate of the top-level
00261    * operator of e, and recurses into children using getTCC(), if
00262    * necessary.
00263    *
00264    * The default implementation is to compute TCCs recursively for all
00265    * children, and return their conjunction.
00266    */
00267   virtual Expr computeTCC(const Expr& e);
00268 
00269   //! Theory-specific parsing implemented by the DP
00270   virtual Expr parseExprOp(const Expr& e) { return e; }
00271 
00272   //! Theory-specific pretty-printing.
00273   /*! By default, print the top node in AST, and resume
00274     pretty-printing the children.  The same call e.print(os) can be
00275     used in DP-specific printers to use AST printing for the given
00276     node.  In fact, it is strongly recommended to add e.print(os) as
00277     the default for all the cases/kinds that are not handled by the
00278     particular pretty-printer.
00279   */
00280   virtual ExprStream& print(ExprStream& os, const Expr& e) {
00281     return e.printAST(os);
00282   }
00283 
00284   //! Add variables from 'e' to 'v' for constructing a concrete model
00285   /*! If e is already of primitive type, do NOT add it to v. */
00286   virtual void computeModelTerm(const Expr& e, std::vector<Expr>& v);
00287   //! Process disequalities from the arrangement for model generation
00288   virtual void refineCounterExample() {}
00289   //! Assign concrete values to basic-type variables in v
00290   virtual void computeModelBasic(const std::vector<Expr>& v) {}
00291   //! Compute the value of a compound variable from the more primitive ones
00292   /*! The more primitive variables for e are already assigned concrete
00293    * values, and are available through getModelValue().
00294    *
00295    * The new value for e must be assigned using assignValue() method.
00296    *
00297    * \param e is the compound type expression to assign a value;
00298    *
00299    * \param vars are the variables actually assigned.  Normally, 'e'
00300    * is the only element of vars.  However, e.g. in the case of
00301    * uninterpreted functions, assigning 'f' means assigning all
00302    * relevant applications of 'f' to constant values (f(0), f(5),
00303    * etc.).  Such applications might not be known before the model is
00304    * constructed (they may be of the form f(x), f(y+z), etc., where
00305    * x,y,z are still unassigned).
00306    *
00307    * Populating 'vars' is an opportunity for a DP to change the set of
00308    * top-level "variables" to assign, if needed.  In particular, it
00309    * may drop 'e' from the model entirely, if it is already a concrete
00310    * value by itself.
00311    */
00312   virtual void computeModel(const Expr& e, std::vector<Expr>& vars) {
00313     assignValue(find(e));
00314     vars.push_back(e);
00315   }
00316 
00317   //! Receives all the type predicates for the types of the given theory
00318   /*! Type predicates may be expensive to enqueue eagerly, and DPs may
00319     choose to postpone them, or transform them to something more
00320     efficient.  By default, the asserted type predicate is
00321     immediately enqueued as a new fact.
00322 
00323     Note: Used only by bitvector theory.
00324 
00325     \param e is the expression for which the type predicate is computed
00326     \param pred is the predicate theorem P(e)
00327   */
00328   virtual void assertTypePred(const Expr& e, const Theorem& pred)
00329     { enqueueFact(pred); }
00330 
00331   //! Theory-specific rewrites for atomic formulas
00332   /*! The intended use is to convert complex atomic formulas into an
00333    * equivalent Boolean combination of simpler formulas.  Such
00334    * conversion may be harmful for algebraic rewrites, and is not
00335    * always desirable to have in rewrite() method.
00336    *
00337    * Note: Used only by bitvector theory and rewriteLiteral in core.
00338    *
00339    * However, if rewrite() alone cannot solve the problem, and the SAT
00340    * solver needs to be envoked, these additional rewrites may ease
00341    * the job for the SAT solver.
00342    */
00343   virtual Theorem rewriteAtomic(const Expr& e) { return reflexivityRule(e); }
00344 
00345   //! Notification of conflict
00346   /*!
00347    * Decision procedures implement this method when they want to be
00348    * notified about a conflict.
00349    *
00350    * Note: Used only by quantifier theory
00351    *
00352    * \param thm is the theorem of FALSE given to setInconsistent()
00353    */
00354   virtual void notifyInconsistent(const Theorem& thm) { }
00355 
00356   //! Theory-specific registration of atoms
00357   /*!
00358    * If a theory wants to implement its own theory propagation, it
00359    * should implement this method and use it to collect all atoms
00360    * that the core is interested in.  If the theory can deduce the atom
00361    * or its negation, it should do so (using enqueueFact).
00362    */
00363   virtual void registerAtom(const Expr& e) { }
00364 
00365   /*@}*/ // End of Theory_API group
00366 
00367   /***************************************************************************/
00368   /*!
00369    *\name Core Framework Functionality
00370    * These methods provide convenient access to core functionality for the
00371    * benefit of decision procedures.
00372    *@{
00373    */
00374   /***************************************************************************/
00375 
00376   //! Check if the current context is inconsistent
00377   virtual bool inconsistent();
00378   //! Make the context inconsistent; The formula proved by e must FALSE.
00379   virtual void setInconsistent(const Theorem& e);
00380 
00381   //! Mark the current decision branch as possibly incomplete
00382   /*!
00383    * This should be set when a decision procedure uses an incomplete
00384    * algorithm, and cannot guarantee satisfiability after the final
00385    * checkSat() call with full effort.  An example would be
00386    * instantiation of universal quantifiers.
00387    *
00388    * A decision procedure can provide a reason for incompleteness,
00389    * which will be reported back to the user.
00390    */
00391   virtual void setIncomplete(const std::string& reason);
00392 
00393   //! Simplify a term e and return a Theorem(e==e')
00394   /*! \sa simplifyExpr() */
00395   virtual Theorem simplify(const Expr& e);
00396   //! Simplify a term e w.r.t. the current context
00397   /*! \sa simplify */
00398   Expr simplifyExpr(const Expr& e)
00399     { return simplify(e).getRHS(); }
00400 
00401   //! Submit a derived fact to the core from a decision procedure
00402   /*! \param e is the Theorem for the new fact 
00403    */
00404   virtual void enqueueFact(const Theorem& e);
00405 
00406   //! Handle new equalities (usually asserted through addFact)
00407   /*!
00408    * INVARIANT: the Theorem 'e' is an equality e1==e2, where e2 is
00409    * i-leaf simplified in the current context, or a conjunction of
00410    * such equalities.
00411    *
00412    */
00413   virtual void assertEqualities(const Theorem& e);
00414 
00415   //! Parse the generic expression.
00416   /*! This method should be used in parseExprOp() for recursive calls
00417    *  to subexpressions, and is the method called by the command
00418    *  processor.
00419    */
00420   virtual Expr parseExpr(const Expr& e);
00421 
00422   //! Assigns t a concrete value val.  Used in model generation.
00423   virtual void assignValue(const Expr& t, const Expr& val);
00424   //! Record a derived assignment to a variable (LHS).
00425   virtual void assignValue(const Theorem& thm);
00426 
00427   /*@}*/ // End of Core Framework Functionality
00428 
00429   /***************************************************************************/
00430   /*!
00431    *\name Theory Helper Methods
00432    * These methods provide basic functionality needed by all theories.
00433    *@{
00434    */
00435   /***************************************************************************/
00436 
00437   //! Register new kinds with the given theory
00438   void registerKinds(Theory* theory, std::vector<int>& kinds);
00439   //! Register a new theory
00440   void registerTheory(Theory* theory, std::vector<int>& kinds,
00441           bool hasSolver=false);
00442 
00443   //! Return the number of registered theories
00444   int getNumTheories();
00445 
00446   //! Test whether a kind maps to any theory
00447   bool hasTheory(int kind);
00448   //! Return the theory associated with a kind
00449   Theory* theoryOf(int kind);
00450   //! Return the theory associated with an Expr
00451   Theory* theoryOf(const Expr& e);
00452 
00453   //! Return the theorem that e is equal to its find
00454   Theorem find(const Expr& e);
00455   //! Return the find as a reference: expr must have a find
00456   const Theorem& findRef(const Expr& e);
00457 
00458   //! Return true iff e is find-reduced
00459   bool findReduced(const Expr& e);
00460   //! Return the find of e, or e if it has no find
00461   inline Expr findExpr(const Expr& e)
00462     { return e.hasFind() ? find(e).getRHS() : e; }
00463 
00464   //! Compute the TCC of e, or the subtyping predicate, if e is a type
00465   Expr getTCC(const Expr& e);
00466   //! Compute (or look up in cache) the base type of e and return the result
00467   Type getBaseType(const Expr& e);
00468   //! Compute the base type from an arbitrary type
00469   Type getBaseType(const Type& tp);
00470   //! Calls the correct theory to compute a type predicate
00471   Expr getTypePred(const Type& t, const Expr& e);
00472 
00473   //! Update the children of the term e
00474   /*! When a decision procedure receives a call to update() because a
00475     child of a term 'e' has changed, this method can be called to
00476     compute the new value of 'e'.
00477     \sa update
00478   */
00479   Theorem updateHelper(const Expr& e);
00480   //! Setup a term for congruence closure (must have sig and rep attributes)
00481   void setupCC(const Expr& e);
00482   //! Update a term w.r.t. congruence closure (must be setup with setupCC())
00483   void updateCC(const Theorem& e, const Expr& d);
00484   //! Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
00485   Theorem rewriteCC(const Expr& e);
00486 
00487   /*! @brief Calls the correct theory to get all of the terms that
00488     need to be assigned values in the concrete model */
00489   void getModelTerm(const Expr& e, std::vector<Expr>& v);
00490   //! Fetch the concrete assignment to the variable during model generation
00491   Theorem getModelValue(const Expr& e);
00492 
00493   //! Suggest a splitter to the SearchEngine
00494   void addSplitter(const Expr& e, int priority = 0);
00495 
00496   /*@}*/ // End of Theory Helper Methods
00497 
00498   /***************************************************************************/
00499   /*!
00500    *\name Core Testers
00501    *@{
00502    */
00503   /***************************************************************************/
00504 
00505   //! Test if e is an i-leaf term for the current theory
00506   /*! A term 'e' is an i-leaf for a theory 'i', if it is a variable,
00507     or 'e' belongs to a different theory.  This definition makes sense
00508     for a larger term which by itself belongs to the current theory
00509     'i', but (some of) its children are variables or belong to
00510     different theories. */
00511   bool isLeaf(const Expr& e) { return e.isVar() || theoryOf(e) != this; }
00512 
00513   //! Test if e1 is an i-leaf in e2
00514   /*! \sa isLeaf */
00515   bool isLeafIn(const Expr& e1, const Expr& e2);
00516 
00517   //! Test if all i-leaves of e are simplified
00518   /*! \sa isLeaf */
00519   bool leavesAreSimp(const Expr& e);
00520 
00521   /*@}*/ // End of Core Testers
00522 
00523   /***************************************************************************/
00524   /*!
00525    *\name Common Type and Expr Methods
00526    *@{
00527    */
00528   /***************************************************************************/
00529 
00530   //! Return BOOLEAN type
00531   Type boolType() { return Type::typeBool(d_em); }
00532 
00533   //! Return FALSE Expr
00534   const Expr& falseExpr() { return d_em->falseExpr(); }
00535 
00536   //! Return TRUE Expr
00537   const Expr& trueExpr() { return d_em->trueExpr(); }
00538 
00539   //! Create a new variable given its name and type
00540   /*! Add the variable to the database for resolving IDs in parseExpr
00541    */
00542   Expr newVar(const std::string& name, const Type& type);
00543   //! Create a new named expression given its name, type, and definition
00544   /*! Add the definition to the database for resolving IDs in parseExpr
00545    */
00546   Expr newVar(const std::string& name, const Type& type, const Expr& def);
00547 
00548   //! Create a new uninterpreted function
00549   /*! Add the definition to the database for resolving IDs in parseExpr
00550    */
00551   Op newFunction(const std::string& name, const Type& type,
00552                  bool computeTransClosure);
00553   //! Create a new defined function
00554   /*! Add the definition to the database for resolving IDs in parseExpr
00555    */
00556   Op newFunction(const std::string& name, const Type& type, const Expr& def);
00557 
00558   //! Create and add a new bound variable to the stack, for parseExprOp().
00559   /*!
00560    * The stack is popped automatically upon return from the
00561    * parseExprOp() which used this method.
00562    *
00563    * Bound variable names may repeat, in which case the latest
00564    * declaration takes precedence.
00565    */
00566   Expr addBoundVar(const std::string& name, const Type& type);
00567   //! Create and add a new bound named def to the stack, for parseExprOp().
00568   /*!
00569    * The stack is popped automatically upon return from the
00570    * parseExprOp() which used this method.
00571    *
00572    * Bound variable names may repeat, in which case the latest
00573    * declaration takes precedence.
00574    *
00575    * The type may be Null, but 'def' must always be a valid Expr
00576    */
00577   Expr addBoundVar(const std::string& name, const Type& type, const Expr& def);
00578 
00579   /*! @brief Lookup variable and return it and its type.  Return NULL Expr if
00580     it doesn't exist yet. */
00581   Expr lookupVar(const std::string& name, Type* type);
00582 
00583   //! Create a new uninterpreted type with the given name
00584   /*! Add the name to the global variable database d_globals
00585    */
00586   Type newTypeExpr(const std::string& name);
00587   //! Create a new type abbreviation with the given name 
00588   Type newTypeExpr(const std::string& name, const Type& def);
00589 
00590   //! Create a new subtype expression
00591   Type newSubtypeExpr(const Expr& pred, const Expr& witness);
00592 
00593   //! Resolve an identifier, for use in parseExprOp()
00594   /*!
00595    * First, search the bound variable stack, and if the name is not
00596    * found, search the global constant and type declarations.  
00597    *
00598    * \return an expression to use in place of the identifier, or Null
00599    * if cannot resolve the name.
00600    */
00601   Expr resolveID(const std::string& name);
00602 
00603   //! Install name as a new identifier associated with Expr e
00604   void installID(const std::string& name, const Expr& e);
00605 
00606   Theorem typePred(const Expr& e);
00607 
00608   /*@}*/ // End of Common Type and Expr Methods
00609 
00610   /***************************************************************************/
00611   /*!
00612    *\name Commonly Used Proof Rules
00613    *\anchor theory_api_core_proof_rules
00614    *@{
00615    */
00616   /***************************************************************************/
00617 
00618   //!  ==> a == a
00619   Theorem reflexivityRule(const Expr& a)
00620     { return d_commonRules->reflexivityRule(a); }
00621 
00622   //!  a1 == a2 ==> a2 == a1
00623   Theorem symmetryRule(const Theorem& a1_eq_a2)
00624     { return d_commonRules->symmetryRule(a1_eq_a2); }
00625 
00626   //! (a1 == a2) & (a2 == a3) ==> (a1 == a3)
00627   Theorem transitivityRule(const Theorem& a1_eq_a2,
00628          const Theorem& a2_eq_a3)
00629     { return d_commonRules->transitivityRule(a1_eq_a2, a2_eq_a3); }
00630 
00631   //! (c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
00632   Theorem substitutivityRule(const Op& op,
00633            const std::vector<Theorem>& thms)
00634     { return d_commonRules->substitutivityRule(op, thms); }
00635 
00636   //! Special case for binary operators
00637   Theorem substitutivityRule(const Expr& e,
00638                              const Theorem& t1,
00639                              const Theorem& t2)
00640     { return d_commonRules->substitutivityRule(e, t1, t2); }
00641 
00642   //! Optimized: only positions which changed are included
00643   Theorem substitutivityRule(const Expr& e,
00644            const std::vector<unsigned>& changed,
00645            const std::vector<Theorem>& thms)
00646     { return d_commonRules->substitutivityRule(e, changed, thms); }
00647 
00648   //! Optimized: only a single position changed
00649   Theorem substitutivityRule(const Expr& e,
00650                              int changed,
00651                              const Theorem& thm)
00652     { return d_commonRules->substitutivityRule(e, changed, thm); }
00653 
00654   //! e1 AND (e1 IFF e2) ==> e2
00655   Theorem iffMP(const Theorem& e1, const Theorem& e1_iff_e2) {
00656     return d_commonRules->iffMP(e1, e1_iff_e2);
00657   }
00658 
00659   //! ==> AND(e1,e2) IFF [simplified expr]
00660   Theorem rewriteAnd(const Expr& e) {
00661     return d_commonRules->rewriteAnd(e);
00662   }
00663 
00664   //! ==> OR(e1,...,en) IFF [simplified expr]
00665   Theorem rewriteOr(const Expr& e) {
00666     return d_commonRules->rewriteOr(e);
00667   }
00668   
00669   /*@}*/ // End of Commonly Used Proof Rules
00670 
00671 
00672 };
00673 
00674 /*@}*/ // End of group Theories
00675 
00676 }
00677 
00678 #endif

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