Go to the documentation of this file.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
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 };
00130
00131 }
00132
00133 #endif