CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
search
LFSCConvert.h
Go to the documentation of this file.
1
#ifndef LFSC_CONVERT_H_
2
#define LFSC_CONVERT_H_
3
4
#include "
TReturn.h
"
5
6
class
LFSCConvert
:
public
LFSCObj
7
{
8
private
:
9
//the converted LFSCProof
10
RefPtr< LFSCProof >
pfinal
;
11
// translations of proofs for cvc3_to_lfsc : if a proof has already been done,
12
// return the TReturn store for it
13
ExprMap<bool>
d_th_trans
;
14
ExprMap<TReturn*>
d_th_trans_map
[2];
15
// these are the current TReturns we need to make into lambdas
16
std::map<TReturn*, bool>
d_th_trans_lam
[2];
17
//counts for theory/non-theory
18
int
nodeCount
;
19
int
nodeCountTh
;
20
int
unodeCount
;
21
int
unodeCountTh
;
22
//whether to ignore theory lemmas
23
bool
ignore_theory_lemmas
;
24
25
// other helper methods
26
bool
isTrivialTheoryAxiom
(
const
Expr
& expr,
bool
checkBody =
false
);
27
bool
isTrivialBooleanAxiom
(
const
Expr
& expr);
28
bool
isIgnoredRule
(
const
Expr
& expr);
29
30
// main method to implement T transformation:
31
// cvc3 proof syntax tree to lfsc proof syntax tree
32
// beneath_lc is whether you are beneath a learned clause
33
// rev_pol is whether you should prove ~psi2 V psi1 in the provesY = 2 case (reverse the implication)
34
TReturn
*
cvc3_to_lfsc
(
const
Expr
& pf,
bool
beneath_lc =
false
,
bool
rev_pol=
false
);
35
TReturn
*
cvc3_to_lfsc_h
(
const
Expr
& pf,
bool
beneath_lc =
false
,
bool
rev_pol=
false
);
36
//do basic subst op procedure
37
TReturn
*
do_bso
(
const
Expr
& pf,
bool
beneath_lc,
bool
rev_pol,
TReturn
* t1,
TReturn
* t2, ostringstream& ose );
38
//get proof type
39
int
get_proof_pattern
(
const
Expr
& pf,
Expr
& modE );
40
//make the let proof
41
LFSCProof
*
make_let_proof
(
LFSCProof
* p );
42
//make trusted
43
TReturn
*
make_trusted
(
const
Expr
& pf );
44
45
virtual
~LFSCConvert
(){}
46
public
:
47
LFSCConvert
(
int
lfscm );
48
//main conversion function
49
void
convert
(
const
Expr
& pf );
50
//get the results
51
LFSCProof
*
getLFSCProof
() {
return
pfinal
.
get
(); }
52
};
53
54
#endif
Generated on Sat May 18 2013 12:01:25 for CVC3 by
1.8.3.1