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     //! Helper function for liftOneITE
00056     void findITE(const Expr& e, Expr& condition, Expr& thenpart, Expr& elsepart);
00057 
00058   public:
00059     CommonTheoremProducer(TheoremManager* tm);
00060     virtual ~CommonTheoremProducer() { }
00061 
00062     Theorem3 queryTCC(const Theorem& phi, const Theorem& D_phi);
00063     Theorem3 implIntro3(const Theorem3& phi,
00064       const std::vector<Expr>& assump,
00065       const std::vector<Theorem>& tccs);
00066     Theorem assumpRule(const Expr& a, int scope = -1);
00067     Theorem reflexivityRule(const Expr& a);
00068     Theorem rewriteReflexivity(const Expr& t);
00069     Theorem symmetryRule(const Theorem& a1_eq_a2);
00070     Theorem rewriteUsingSymmetry(const Expr& a1_eq_a2);
00071     Theorem transitivityRule(const Theorem& a1_eq_a2,
00072                              const Theorem& a2_eq_a3);
00073     Theorem substitutivityRule(const Expr& e,
00074                                const Theorem& thm);
00075     Theorem substitutivityRule(const Expr& e,
00076                                const Theorem& thm1,
00077                                const Theorem& thm2);
00078     Theorem substitutivityRule(const Op& op,
00079                                const std::vector<Theorem>& thms);
00080     Theorem substitutivityRule(const Expr& e,
00081                                const std::vector<unsigned>& changed,
00082                                const std::vector<Theorem>& thms);
00083     Theorem substitutivityRule(const Expr& e,
00084                                const int changed,
00085                                const Theorem& thm);
00086     Theorem contradictionRule(const Theorem& e, const Theorem& not_e);
00087     Theorem excludedMiddle(const Expr& e);
00088     Theorem iffTrue(const Theorem& e);
00089     Theorem iffNotFalse(const Theorem& e);
00090     Theorem iffTrueElim(const Theorem& e);
00091     Theorem iffFalseElim(const Theorem& e);
00092     Theorem iffContrapositive(const Theorem& thm);
00093     Theorem notNotElim(const Theorem& e);
00094     Theorem iffMP(const Theorem& e1, const Theorem& e1_iff_e2);
00095     Theorem implMP(const Theorem& e1, const Theorem& e1_impl_e2);
00096     Theorem andElim(const Theorem& e, int i);
00097     Theorem andIntro(const Theorem& e1, const Theorem& e2);
00098     Theorem andIntro(const std::vector<Theorem>& es);
00099     Theorem implIntro(const Theorem& phi, const std::vector<Expr>& assump);
00100     Theorem implContrapositive(const Theorem& thm);
00101     Theorem rewriteIteTrue(const Expr& e);
00102     Theorem rewriteIteFalse(const Expr& e);
00103     Theorem rewriteIteSame(const Expr& e);
00104     Theorem notToIff(const Theorem& not_e);
00105     Theorem xorToIff(const Expr& e);
00106     Theorem rewriteIff(const Expr& e);
00107     Theorem rewriteAnd(const Expr& e);
00108     Theorem rewriteOr(const Expr& e);
00109     Theorem rewriteNotTrue(const Expr& e);
00110     Theorem rewriteNotFalse(const Expr& e);
00111     Theorem rewriteNotNot(const Expr& e);
00112     Theorem rewriteNotForall(const Expr& forallExpr);
00113     Theorem rewriteNotExists(const Expr& existsExpr);
00114     Expr skolemize(const Expr& e);
00115     Theorem skolemizeRewrite(const Expr& e);
00116     Theorem skolemizeRewriteVar(const Expr& e);
00117     Theorem varIntroRule(const Expr& e);
00118     Theorem skolemize(const Theorem& thm);
00119     Theorem varIntroSkolem(const Expr& e);
00120     Theorem trueTheorem();
00121     Theorem rewriteAnd(const Theorem& e);
00122     Theorem rewriteOr(const Theorem& e);
00123     Theorem ackermann(const Expr& e1, const Expr& e2);
00124     Theorem liftOneITE(const Expr& e);
00125 
00126     std::vector<Theorem>& getSkolemAxioms() { return d_skolem_axioms; }
00127     void clearSkolemAxioms() { d_skolem_axioms.clear(); }
00128 
00129   }; // end of class CommonTheoremProducer
00130 
00131 } // end of namespace CVC3
00132 
00133 #endif

Generated on Wed Nov 18 16:13:29 2009 for CVC3 by  doxygen 1.5.2