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