common_theorem_producer.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file common_theorem_producer.h
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Feb 05 03:40:36 GMT 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 // CLASS: CommonTheoremProducer
00021 //
00022 // AUTHOR: Sergey Berezin, 12/09/2002
00023 //
00024 // Description: Implementation of the proof rules for ground
00025 // equational logic (reflexivity, symmetry, transitivity, and
00026 // substitutivity).
00027 //
00028 ///////////////////////////////////////////////////////////////////////////////
00029 
00030 #ifndef _cvc3__common_theorem_producer_h_
00031 #define _cvc3__common_theorem_producer_h_
00032 
00033 #include "common_proof_rules.h"
00034 #include "theorem_producer.h"
00035 #include "theorem.h"
00036 #include "cdmap.h"
00037 
00038 namespace CVC3 {
00039 
00040   class CommonTheoremProducer: public CommonProofRules, public TheoremProducer {
00041   private:
00042 
00043     // TODO: do we need to record skolem axioms?  do we need context-dependence?
00044 
00045     // skolem axioms
00046     std::vector<Theorem> d_skolem_axioms;
00047 
00048     /* @brief Keep skolemization axioms so that they can be reused 
00049        without being recreated each time */
00050     CDMap<Expr, Theorem> d_skolemized_thms;
00051 
00052     //! Mapping of e to "|- e = v" for fresh Skolem vars v
00053     CDMap<Expr, Theorem> d_skolemVars;
00054 
00055   public:
00056     CommonTheoremProducer(TheoremManager* tm);
00057     virtual ~CommonTheoremProducer() { }
00058 
00059     Theorem3 queryTCC(const Theorem& phi, const Theorem& D_phi);
00060     Theorem3 implIntro3(const Theorem3& phi,
00061       const std::vector<Expr>& assump,
00062       const std::vector<Theorem>& tccs);
00063     Theorem assumpRule(const Expr& a, int scope = -1);
00064     Theorem reflexivityRule(const Expr& a);
00065     Theorem rewriteReflexivity(const Expr& t);
00066     Theorem symmetryRule(const Theorem& a1_eq_a2);
00067     Theorem rewriteUsingSymmetry(const Expr& a1_eq_a2);
00068     Theorem transitivityRule(const Theorem& a1_eq_a2,
00069                              const Theorem& a2_eq_a3);
00070     Theorem substitutivityRule(const Expr& e,
00071                                const Theorem& thm);
00072     Theorem substitutivityRule(const Expr& e,
00073                                const Theorem& thm1,
00074                                const Theorem& thm2);
00075     Theorem substitutivityRule(const Op& op,
00076                                const std::vector<Theorem>& thms);
00077     Theorem substitutivityRule(const Expr& e,
00078                                const std::vector<unsigned>& changed,
00079                                const std::vector<Theorem>& thms);
00080     Theorem substitutivityRule(const Expr& e,
00081                                const int changed,
00082                                const Theorem& thm);
00083     Theorem contradictionRule(const Theorem& e, const Theorem& not_e);
00084     Theorem excludedMiddle(const Expr& e);
00085     Theorem iffTrue(const Theorem& e);
00086     Theorem iffNotFalse(const Theorem& e);
00087     Theorem iffTrueElim(const Theorem& e);
00088     Theorem iffFalseElim(const Theorem& e);
00089     Theorem iffContrapositive(const Theorem& thm);
00090     Theorem notNotElim(const Theorem& e);
00091     Theorem iffMP(const Theorem& e1, const Theorem& e1_iff_e2);
00092     Theorem implMP(const Theorem& e1, const Theorem& e1_impl_e2);
00093     Theorem andElim(const Theorem& e, int i);
00094     Theorem andIntro(const Theorem& e1, const Theorem& e2);
00095     Theorem andIntro(const std::vector<Theorem>& es);
00096     Theorem implIntro(const Theorem& phi, const std::vector<Expr>& assump);
00097     Theorem implContrapositive(const Theorem& thm);
00098     Theorem notToIff(const Theorem& not_e);
00099     Theorem xorToIff(const Expr& e);
00100     Theorem rewriteIff(const Expr& e);
00101     Theorem rewriteAnd(const Expr& e);
00102     Theorem rewriteOr(const Expr& e);
00103     Theorem rewriteNotTrue(const Expr& e);
00104     Theorem rewriteNotFalse(const Expr& e);
00105     Theorem rewriteNotNot(const Expr& e);
00106     Theorem rewriteNotForall(const Expr& forallExpr);
00107     Theorem rewriteNotExists(const Expr& existsExpr);
00108     Expr skolemize(const Expr& e);
00109     Theorem skolemizeRewrite(const Expr& e);
00110     Theorem skolemizeRewriteVar(const Expr& e);
00111     Theorem varIntroRule(const Expr& e);
00112     Theorem skolemize(const Theorem& thm);
00113     Theorem varIntroSkolem(const Expr& e);
00114     Theorem trueTheorem();
00115     Theorem rewriteAnd(const Theorem& e);
00116     Theorem rewriteOr(const Theorem& e);
00117     Theorem ackermann(const Expr& e1, const Expr& e2);
00118 
00119     std::vector<Theorem>& getSkolemAxioms() { return d_skolem_axioms; }
00120     void clearSkolemAxioms() { d_skolem_axioms.clear(); }
00121 
00122   }; // end of class CommonTheoremProducer
00123 
00124 } // end of namespace CVC3
00125 
00126 #endif

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