core_proof_rules.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file core_proof_rules.h
00004  *\brief Proof rules used by theory_core
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Wed Jan 11 15:48:35 2006
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__core_proof_rules_h_
00023 #define _cvc3__core_proof_rules_h_
00024 
00025 #include <vector>
00026 
00027 namespace CVC3 {
00028 
00029   class Theorem;
00030   class Theorem3;
00031   class Expr;
00032   class Op;
00033 
00034   class CoreProofRules {
00035   public:
00036     //! Destructor
00037     virtual ~CoreProofRules() { }
00038 
00039     //! e: T ==> |- typePred_T(e)  [deriving the type predicate of e]
00040     virtual Theorem typePred(const Expr& e) = 0;
00041 
00042     ////////////////////////////////////////////////////////////////////////
00043     // Core rewrite rules
00044     ////////////////////////////////////////////////////////////////////////
00045 
00046     //! Replace LETDECL with its definition
00047     /*! Used only in TheoryCore */ 
00048     virtual Theorem rewriteLetDecl(const Expr& e) = 0;
00049     //! ==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...)
00050     virtual Theorem rewriteNotAnd(const Expr& e) = 0;
00051     //! ==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...)
00052     virtual Theorem rewriteNotOr(const Expr& e) = 0;
00053     //! ==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2)
00054     virtual Theorem rewriteNotIff(const Expr& e) = 0;
00055     //! ==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c)
00056     virtual Theorem rewriteNotIte(const Expr& e) = 0;
00057     //! ==> ITE(TRUE, e1, e2) == e1
00058     virtual Theorem rewriteIteTrue(const Expr& e) = 0;
00059     //! ==> ITE(FALSE, e1, e2) == e2
00060     virtual Theorem rewriteIteFalse(const Expr& e) = 0;
00061     //! ==> ITE(c, e, e) == e
00062     virtual Theorem rewriteIteSame(const Expr& e) = 0;
00063     //! a |- b == d ==> ITE(a, b, c) == ITE(a, d, c)
00064     virtual Theorem rewriteIteThen(const Expr& e, const Theorem& thenThm) = 0;
00065     //! !a |- c == d ==> ITE(a, b, c) == ITE(a, b, d)
00066     virtual Theorem rewriteIteElse(const Expr& e, const Theorem& elseThm) = 0;
00067     //! ==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2)
00068     virtual Theorem rewriteIteBool(const Expr& c,
00069            const Expr& e1, const Expr& e2) = 0;
00070 
00071     //! |= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn)
00072     virtual Theorem orDistributivityRule(const Expr& e) = 0;
00073     //! |= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn)
00074     virtual Theorem andDistributivityRule(const Expr& e) = 0;
00075 
00076 
00077     //! ==> IMPLIES(e1,e2) IFF OR(!e1, e2)
00078     virtual Theorem rewriteImplies(const Expr& e) = 0;
00079 
00080     //! ==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j])
00081     virtual Theorem rewriteDistinct(const Expr& e) = 0;
00082 
00083     //! ==> NOT(e) == ITE(e, FALSE, TRUE)
00084     virtual Theorem NotToIte(const Expr& not_e) = 0;
00085     //! ==> Or(e) == ITE(e[1], TRUE, e[0])
00086     virtual Theorem OrToIte(const Expr& e) = 0;
00087     //! ==> And(e) == ITE(e[1], e[0], FALSE)
00088     virtual Theorem AndToIte(const Expr& e) = 0;
00089     //! ==> IFF(a,b) == ITE(a, b, !b)
00090     virtual Theorem IffToIte(const Expr& e) = 0;
00091     //! ==> IMPLIES(a,b) == ITE(a, b, TRUE)
00092     virtual Theorem ImpToIte(const Expr& e) = 0;
00093 
00094     //! ==> ITE(e, FALSE, TRUE) IFF NOT(e)
00095     virtual Theorem rewriteIteToNot(const Expr& e) = 0;
00096     //! ==> ITE(a, TRUE, b) IFF OR(a, b)
00097     virtual Theorem rewriteIteToOr(const Expr& e) = 0;
00098     //! ==> ITE(a, b, FALSE) IFF AND(a, b)
00099     virtual Theorem rewriteIteToAnd(const Expr& e) = 0;
00100     //! ==> ITE(a, b, !b) IFF IFF(a, b)
00101     virtual Theorem rewriteIteToIff(const Expr& e) = 0;
00102     //! ==> ITE(a, b, TRUE) IFF IMPLIES(a, b)
00103     virtual Theorem rewriteIteToImp(const Expr& e) = 0;
00104     //! ==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))
00105     virtual Theorem rewriteIteCond(const Expr& e) = 0;
00106 
00107     //! |- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b))
00108     virtual Theorem ifLiftUnaryRule(const Expr& e) = 0;
00109     //! ((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff'
00110     virtual Theorem iffOrDistrib(const Expr& iff) = 0;
00111     //! ((a&b)<=>(a&c))<=>(!a|(b<=>c)); takes ((a&b)<=>(a&c)) as 'iff'
00112     virtual Theorem iffAndDistrib(const Expr& iff) = 0;
00113 
00114     // Advanced Boolean transformations
00115 
00116     //! (a & b) <=> a & b[a/true]; takes the index of a
00117     /*! and rewrites all the other conjuncts. */
00118     virtual Theorem rewriteAndSubterms(const Expr& e, int idx) = 0;
00119     //! (a | b) <=> a | b[a/false]; takes the index of a
00120     /*! and rewrites all the other disjuncts. */
00121     virtual Theorem rewriteOrSubterms(const Expr& e, int idx) = 0;
00122 
00123   }; // end of class CoreProofRules
00124 
00125 } // end of namespace CVC3
00126 
00127 #endif

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