CVC3
common_theorem_producer.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file common_theorem_producer.h
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Feb 05 03:40:36 GMT 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 // CLASS: CommonTheoremProducer
21 //
22 // AUTHOR: Sergey Berezin, 12/09/2002
23 //
24 // Description: Implementation of the proof rules for ground
25 // equational logic (reflexivity, symmetry, transitivity, and
26 // substitutivity).
27 //
28 ///////////////////////////////////////////////////////////////////////////////
29 
30 #ifndef _cvc3__common_theorem_producer_h_
31 #define _cvc3__common_theorem_producer_h_
32 
33 #include "common_proof_rules.h"
34 #include "theorem_producer.h"
35 #include "theorem.h"
36 #include "cdmap.h"
37 
38 namespace CVC3 {
39 
41  private:
42 
43  // TODO: do we need to record skolem axioms? do we need context-dependence?
44 
45  // skolem axioms
46  std::vector<Theorem> d_skolem_axioms;
47 
48  /* @brief Keep skolemization axioms so that they can be reused
49  without being recreated each time */
51 
52  //! Mapping of e to "|- e = v" for fresh Skolem vars v
54 
55  //! Helper function for liftOneITE
56  void findITE(const Expr& e, Expr& condition, Expr& thenpart, Expr& elsepart);
57 
58  public:
60  virtual ~CommonTheoremProducer() { }
61 
62  Theorem3 queryTCC(const Theorem& phi, const Theorem& D_phi);
63  Theorem3 implIntro3(const Theorem3& phi,
64  const std::vector<Expr>& assump,
65  const std::vector<Theorem>& tccs);
66  Theorem assumpRule(const Expr& a, int scope = -1);
67  Theorem reflexivityRule(const Expr& a);
69  Theorem symmetryRule(const Theorem& a1_eq_a2);
70  Theorem rewriteUsingSymmetry(const Expr& a1_eq_a2);
71  Theorem transitivityRule(const Theorem& a1_eq_a2,
72  const Theorem& a2_eq_a3);
74  const Theorem& thm);
76  const Theorem& thm1,
77  const Theorem& thm2);
78  Theorem substitutivityRule(const Op& op,
79  const std::vector<Theorem>& thms);
81  const std::vector<unsigned>& changed,
82  const std::vector<Theorem>& thms);
84  const int changed,
85  const Theorem& thm);
86  Theorem contradictionRule(const Theorem& e, const Theorem& not_e);
87  Theorem excludedMiddle(const Expr& e);
88  Theorem iffTrue(const Theorem& e);
89  Theorem iffNotFalse(const Theorem& e);
90  Theorem iffTrueElim(const Theorem& e);
91  Theorem iffFalseElim(const Theorem& e);
92  Theorem iffContrapositive(const Theorem& thm);
93  Theorem notNotElim(const Theorem& e);
94  Theorem iffMP(const Theorem& e1, const Theorem& e1_iff_e2);
95  Theorem implMP(const Theorem& e1, const Theorem& e1_impl_e2);
96  Theorem andElim(const Theorem& e, int i);
97  Theorem andIntro(const Theorem& e1, const Theorem& e2);
98  Theorem andIntro(const std::vector<Theorem>& es);
99  Theorem implIntro(const Theorem& phi, const std::vector<Expr>& assump);
100  Theorem implContrapositive(const Theorem& thm);
101  Theorem rewriteIteTrue(const Expr& e);
102  Theorem rewriteIteFalse(const Expr& e);
103  Theorem rewriteIteSame(const Expr& e);
104  Theorem notToIff(const Theorem& not_e);
105  Theorem xorToIff(const Expr& e);
106  Theorem rewriteIff(const Expr& e);
107  Theorem rewriteAnd(const Expr& e);
108  Theorem rewriteOr(const Expr& e);
109  Theorem rewriteNotTrue(const Expr& e);
110  Theorem rewriteNotFalse(const Expr& e);
111  Theorem rewriteNotNot(const Expr& e);
112  Theorem rewriteNotForall(const Expr& forallExpr);
113  Theorem rewriteNotExists(const Expr& existsExpr);
114  Expr skolemize(const Expr& e);
115  Theorem skolemizeRewrite(const Expr& e);
116  Theorem skolemizeRewriteVar(const Expr& e);
117  Theorem varIntroRule(const Expr& e);
118  Theorem skolemize(const Theorem& thm);
119  Theorem varIntroSkolem(const Expr& e);
121  Theorem rewriteAnd(const Theorem& e);
122  Theorem rewriteOr(const Theorem& e);
123  Theorem ackermann(const Expr& e1, const Expr& e2);
124  Theorem liftOneITE(const Expr& e);
125 
126  std::vector<Theorem>& getSkolemAxioms() { return d_skolem_axioms; }
127  void clearSkolemAxioms() { d_skolem_axioms.clear(); }
128 
129  }; // end of class CommonTheoremProducer
130 
131 } // end of namespace CVC3
132 
133 #endif