00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
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
00044
00045
00046 std::vector<Theorem> d_skolem_axioms;
00047
00048
00049
00050 CDMap<Expr, Theorem> d_skolemized_thms;
00051
00052
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 };
00123
00124 }
00125
00126 #endif