CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theorem
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
40
class
CommonTheoremProducer
:
public
CommonProofRules
,
public
TheoremProducer
{
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 */
50
CDMap<Expr, Theorem>
d_skolemized_thms
;
51
52
//! Mapping of e to "|- e = v" for fresh Skolem vars v
53
CDMap<Expr, Theorem>
d_skolemVars
;
54
55
//! Helper function for liftOneITE
56
void
findITE
(
const
Expr
& e,
Expr
& condition,
Expr
& thenpart,
Expr
& elsepart);
57
58
public
:
59
CommonTheoremProducer
(
TheoremManager
* tm);
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);
68
Theorem
rewriteReflexivity
(
const
Expr
& t);
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);
73
Theorem
substitutivityRule
(
const
Expr
& e,
74
const
Theorem
& thm);
75
Theorem
substitutivityRule
(
const
Expr
& e,
76
const
Theorem
& thm1,
77
const
Theorem
& thm2);
78
Theorem
substitutivityRule
(
const
Op
& op,
79
const
std::vector<Theorem>& thms);
80
Theorem
substitutivityRule
(
const
Expr
& e,
81
const
std::vector<unsigned>& changed,
82
const
std::vector<Theorem>& thms);
83
Theorem
substitutivityRule
(
const
Expr
& e,
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);
120
Theorem
trueTheorem
();
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
Generated on Fri Aug 9 2013 10:34:40 for CVC3 by
1.8.4