CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
search
TReturn.h
Go to the documentation of this file.
1
#ifndef TRETURN_H_
2
#define TRETURN_H_
3
4
#include "
LFSCProof.h
"
5
6
//////////////////////////////////////////
7
// TReturn = (p_lfsc, L, c)
8
// implements transformation
9
/////////////////////////////////////////
10
11
class
TReturn
:
public
LFSCObj
12
{
13
private
:
14
RefPtr< LFSCProof >
d_lfsc_pf
;
15
// literals (we only store the indices) i corresponds to v_i and -i to not v_i
16
std::vector <int>
d_L
;
17
// literals we use
18
std::vector <int>
d_L_used
;
19
// constant
20
Rational
d_c
;
21
bool
d_hasRt
;
22
// constructor
23
//flag for whether d_lfsc_pf is proving
24
//0: psi,
25
//1: Y(psi) (arithmetic collapse)
26
//2: Y2( psi ) (double implications are single implications)
27
//3: clause( Y2( psi ) )
28
int
d_provesY
;
29
bool
lcalced
;
30
public
:
31
TReturn
(
LFSCProof
* lfsc_pf, std::vector<int>& L, std::vector<int>& Lused,
Rational
r,
bool
hasR,
int
pvY);
32
33
Rational
mult_rational
(
TReturn
* lhs );
34
void
getL
( std::vector< int >& lget, std::vector< int >& lgetu );
35
bool
hasRational
() {
return
d_hasRt
; }
36
Rational
getRational
() {
return
d_c
; }
37
LFSCProof
*
getLFSCProof
(){
return
d_lfsc_pf
.
get
(); }
38
int
getProvesY
() {
return
d_provesY
; }
39
bool
hasFv
() {
return
!
d_L_used
.empty(); }
40
#ifdef OPTIMIZE
41
void
calcL( std::vector< int >& lget, std::vector< int >& lgetu );
42
#endif
43
44
// make it so that the two TReturns agree on what they are proving
45
// t1 corresponds to the conversion of pf1, proving psi, Y( ps1 ), or Y2( ps1 )
46
// t2 corresponds to the conversion of pf2, proving psi, Y( ps1 ), or Y2( ps1 )
47
// on return, t1->d_proveY should equal t2->d_proveY
48
// this will return the mode they normalized on, -1 means fail
49
static
int
normalize_tret
(
const
Expr
& pf1,
TReturn
*& t1,
const
Expr
& pf2,
TReturn
*& t2,
bool
rev_pol =
false
);
50
//normalize TReturn to prove a certain type
51
// this will return the mode it normalized on, -1 means fail
52
static
int
normalize_tr
(
const
Expr
& pf1,
TReturn
*& t1,
int
y,
bool
rev_pol =
false
,
bool
printErr =
true
);
53
//normalize from polynomial formula to term formula atom
54
static
void
normalize_to_tf
(
const
Expr
& pf,
TReturn
*& t1,
int
y );
55
};
56
57
#endif
Generated on Tue May 14 2013 14:44:54 for CVC3 by
1.8.3.1