CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
search
LFSCProof.h
Go to the documentation of this file.
1
#ifndef LFSC_PROOF_H_
2
#define LFSC_PROOF_H_
3
4
#include "
LFSCObject.h
"
5
6
//////////////////////////////////
7
/// LFSC Proof Class & subclasses
8
//////////////////////////////////
9
10
class
LFSCProofExpr
;
11
class
LFSCLraAdd
;
12
class
LFSCLraSub
;
13
class
LFSCLraMulC
;
14
class
LFSCLraAxiom
;
15
class
LFSCLraContra
;
16
class
LFSCLraPoly
;
17
class
LFSCBoolRes
;
18
class
LFSCLem
;
19
class
LFSCClausify
;
20
class
LFSCAssume
;
21
class
LFSCProofGeneric
;
22
class
LFSCPfVar
;
23
class
LFSCPfLambda
;
24
class
LFSCPfLet
;
25
26
class
LFSCProof
:
public
LFSCObj
{
27
protected
:
28
static
int
pf_counter
;
29
static
std::map< LFSCProof*, int >
lambdaMap
;
30
static
std::map< LFSCProof*, LFSCProof* >
lambdaPrintMap
;
31
int
printCounter
;
32
LFSCProof
*
rplProof
;
33
static
int
lambdaCounter
;
34
long
int
strLen
;
35
int
chOp
;
36
int
assumeVar
;
37
int
assumeVarUsed
;
38
39
std::vector< int >
br
;
40
bool
brComputed
;
41
42
LFSCProof
();
43
virtual
long
int
get_length
() {
return
0; }
44
virtual
~LFSCProof
(){}
45
public
:
46
virtual
LFSCProofExpr
*
AsLFSCProofExpr
(){
return
NULL; }
47
virtual
LFSCLraAdd
*
AsLFSCLraAdd
(){
return
NULL; }
48
virtual
LFSCLraSub
*
AsLFSCLraSub
(){
return
NULL; }
49
virtual
LFSCLraMulC
*
AsLFSCLraMulC
(){
return
NULL; }
50
virtual
LFSCLraAxiom
*
AsLFSCLraAxiom
(){
return
NULL; }
51
virtual
LFSCLraContra
*
AsLFSCLraContra
(){
return
NULL; }
52
virtual
LFSCLraPoly
*
AsLFSCLraPoly
(){
return
NULL; }
53
virtual
LFSCBoolRes
*
AsLFSCBoolRes
(){
return
NULL; }
54
virtual
LFSCLem
*
AsLFSCLem
(){
return
NULL; }
55
virtual
LFSCClausify
*
AsLFSCClausify
(){
return
NULL; }
56
virtual
LFSCAssume
*
AsLFSCAssume
(){
return
NULL; }
57
virtual
LFSCProofGeneric
*
AsLFSCProofGeneric
(){
return
NULL; }
58
virtual
LFSCPfVar
*
AsLFSCPfVar
(){
return
NULL; }
59
virtual
LFSCPfLambda
*
AsLFSCPfLambda
(){
return
NULL; }
60
virtual
LFSCPfLet
*
AsLFSCPfLet
(){
return
NULL; }
61
62
virtual
bool
isLraMulC
() {
return
false
; }
63
static
int
make_lambda
(
LFSCProof
* p ){
64
if
(
lambdaMap
[p]==0 ){
65
lambdaMap
[p] =
lambdaCounter
;
66
lambdaCounter
++;
67
}
68
return
lambdaMap
[p];
69
}
70
void
print
( std::ostream& s,
int
ind = 0 );
71
virtual
void
print_pf
( std::ostream& s,
int
ind = 0 )=0;
72
virtual
bool
isTrivial
() {
return
false
; }
73
long
int
get_string_length
() {
74
if
(
strLen
<0 ){
75
strLen
=
get_length
();
76
//to prevent overflow
77
for
(
int
a=0; a<
getNumChildren
(); a++ ){
78
if
(
strLen
<
getChild
( a )->
get_string_length
() ){
79
strLen
=
getChild
( a )->
get_string_length
();
80
}
81
}
82
}
83
return
strLen
;
84
}
85
void
print_structure
( std::ostream& s,
int
ind = 0 );
86
virtual
void
print_struct
( std::ostream& s,
int
ind = 0 ){
87
static
int
psCounter = 0;
88
s <<
"P"
<< psCounter;
89
psCounter++;
90
}
91
void
setRplProof
(
LFSCProof
* p ) {
rplProof
= p; }
92
virtual
void
fillHoles
();
93
#ifdef OPTIMIZE
94
void
calcL( std::vector< int >& lget, std::vector< int >& lgetu );
95
#endif
96
97
friend
class
LFSCPrinter
;
98
99
virtual
LFSCProof
*
clone
() = 0;
100
virtual
int
getNumChildren
() {
return
0; }
101
virtual
LFSCProof
*
getChild
(
int
n ) {
return
NULL; }
102
virtual
int
checkOp
();
103
int
getChOp
(){
return
chOp
; }
104
void
setChOp
(
int
c ) {
chOp
= c; }
105
virtual
int
checkBoolRes
( std::vector< int >& clause ){
return
0; }
106
107
//proof making methods
108
public
:
109
static
LFSCProof
*
Make_CNF
(
const
Expr
& form,
const
Expr
& reason,
int
pos );
110
static
LFSCProof
*
Make_not_not_elim
(
const
Expr
& pf,
LFSCProof
* p );
111
static
LFSCProof
*
Make_mimic
(
const
Expr
& pf,
LFSCProof
* p,
int
numHoles );
112
static
LFSCProof
*
Make_and_elim
(
const
Expr
& form,
LFSCProof
* p,
int
n,
const
Expr
& expected );
113
114
static
int
get_proof_counter
() {
return
pf_counter
; }
115
};
116
117
118
#endif
Generated on Tue May 14 2013 14:44:52 for CVC3 by
1.8.3.1