CVC3  2.4.1
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:
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
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 
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
bool lcalced
Definition: TReturn.h:29
Data structure of expressions in CVC3.
Definition: expr.h:133
Rational d_c
Definition: TReturn.h:20
Rational mult_rational(TReturn *lhs)
Definition: TReturn.cpp:24
T * get()
Definition: Object.h:56
int getProvesY()
Definition: TReturn.h:38
Rational getRational()
Definition: TReturn.h:36
bool d_hasRt
Definition: TReturn.h:21
static int normalize_tr(const Expr &pf1, TReturn *&t1, int y, bool rev_pol=false, bool printErr=true)
Definition: TReturn.cpp:125
void getL(std::vector< int > &lget, std::vector< int > &lgetu)
Definition: TReturn.cpp:37
LFSCProof * getLFSCProof()
Definition: TReturn.h:37
bool hasFv()
Definition: TReturn.h:39
TReturn(LFSCProof *lfsc_pf, std::vector< int > &L, std::vector< int > &Lused, Rational r, bool hasR, int pvY)
Definition: TReturn.cpp:8
std::vector< int > d_L
Definition: TReturn.h:16
std::vector< int > d_L_used
Definition: TReturn.h:18
static int normalize_tret(const Expr &pf1, TReturn *&t1, const Expr &pf2, TReturn *&t2, bool rev_pol=false)
Definition: TReturn.cpp:84
bool hasRational()
Definition: TReturn.h:35
RefPtr< LFSCProof > d_lfsc_pf
Definition: TReturn.h:14
int d_provesY
Definition: TReturn.h:28
static void normalize_to_tf(const Expr &pf, TReturn *&t1, int y)
Definition: TReturn.cpp:423