CVC3  2.4.1
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
Theorem notNotElim(const Theorem &e)
Theorem iffTrue(const Theorem &e)
Data structure of expressions in CVC3.
Definition: expr.h:133
Theorem rewriteOr(const Expr &e)
==> OR(e1,...,en) IFF [simplified expr]
Theorem rewriteIteSame(const Expr &e)
==> ITE(c, e, e) == e
Theorem rewriteIteTrue(const Expr &e)
==> ITE(TRUE, e1, e2) == e1
void findITE(const Expr &e, Expr &condition, Expr &thenpart, Expr &elsepart)
Helper function for liftOneITE.
std::vector< Theorem > & getSkolemAxioms()
Theorem3 implIntro3(const Theorem3 &phi, const std::vector< Expr > &assump, const std::vector< Theorem > &tccs)
3-valued implication introduction rule:
Theorem rewriteNotExists(const Expr &existsExpr)
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
Theorem rewriteNotTrue(const Expr &e)
==> NOT TRUE IFF FALSE
Theorem reflexivityRule(const Expr &a)
Theorem ackermann(const Expr &e1, const Expr &e2)
Theorem varIntroRule(const Expr &e)
|- EXISTS x. e = x
Theorem rewriteReflexivity(const Expr &t)
==> (a == a) IFF TRUE
Theorem iffNotFalse(const Theorem &e)
Theorem contradictionRule(const Theorem &e, const Theorem &not_e)
Theorem iffTrueElim(const Theorem &e)
std::vector< Theorem > d_skolem_axioms
Theorem3.
Definition: theorem.h:308
Theorem3 queryTCC(const Theorem &phi, const Theorem &D_phi)
Convert 2-valued formula to 3-valued by discharging its TCC ( ): .
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
Theorem varIntroSkolem(const Expr &e)
Retrun a theorem "|- e = v" for a new Skolem constant v.
Theorem andIntro(const Theorem &e1, const Theorem &e2)
e1, e2 ==> AND(e1, e2)
Theorem rewriteNotFalse(const Expr &e)
==> NOT FALSE IFF TRUE
Theorem andElim(const Theorem &e, int i)
Theorem rewriteIteFalse(const Expr &e)
==> ITE(FALSE, e1, e2) == e2
Theorem implMP(const Theorem &e1, const Theorem &e1_impl_e2)
Theorem substitutivityRule(const Expr &e, const Theorem &thm)
Optimized case for expr with one child.
Theorem rewriteNotForall(const Expr &forallExpr)
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
CDMap< Expr, Theorem > d_skolemized_thms
Theorem skolemizeRewriteVar(const Expr &e)
Special version of skolemizeRewrite for "EXISTS x. t = x".
CDMap< Expr, Theorem > d_skolemVars
Mapping of e to "|- e = v" for fresh Skolem vars v.
Theorem iffFalseElim(const Theorem &e)
Theorem symmetryRule(const Theorem &a1_eq_a2)
(same for IFF)
Theorem assumpRule(const Expr &a, int scope=-1)
Theorem rewriteUsingSymmetry(const Expr &a1_eq_a2)
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(same for IFF)
Theorem implIntro(const Theorem &phi, const std::vector< Expr > &assump)
Implication introduction rule: .
Theorem rewriteIff(const Expr &e)
==> (e1 <=> e2) <=> [simplified expr]
Theorem implContrapositive(const Theorem &thm)
e1 => e2 ==> ~e2 => ~e1
Theorem notToIff(const Theorem &not_e)
Theorem rewriteNotNot(const Expr &e)
==> NOT NOT e IFF e, takes !!e
Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)
Theorem iffContrapositive(const Theorem &thm)
e1 <=> e2 ==> ~e1 <=> ~e2