CVC3  2.4.1
LFSCLraProof.h
Go to the documentation of this file.
1 #ifndef LFSC_LRA_PROOF_H_
2 #define LFSC_LRA_PROOF_H_
3 
4 #include "LFSCProof.h"
5 
6 // lra_add_~_~
7 class LFSCLraAdd: public LFSCProof{
8 private:
10  int d_op1, d_op2;
11 
12  LFSCLraAdd(LFSCProof* pf1, LFSCProof* pf2, int op1, int op2): LFSCProof(),
13  d_op1(op1),
14  d_op2(op2){
15  d_children[0] = pf1;
16  d_children[1] = pf2;
17  }
18  virtual ~LFSCLraAdd(){}
19  long int get_length(){
20  return 20 + d_children[0]->get_string_length() + d_children[1]->get_string_length();
21  }
22 public:
23  virtual LFSCLraAdd* AsLFSCLraAdd(){ return this; }
24  void print_pf( std::ostream& s, int ind = 0 );
25  static LFSCProof* Make(LFSCProof* pf1, LFSCProof* pf2, int op1, int op2);
26  LFSCProof* clone() { return new LFSCLraAdd( d_children[0].get(), d_children[1].get(), d_op1, d_op2 ); }
27  int getNumChildren() { return 2; }
28  LFSCProof* getChild( int n ) { return d_children[n].get(); }
29  int checkOp() { return get_knd_result( d_op1, d_op2 ); }
30 };
31 
32 
33 // lra_~_axiom
34 
35 class LFSCLraAxiom: public LFSCProof{
36 private:
38  int d_op;
40  LFSCLraAxiom(int op ) : LFSCProof(), d_op(op){}
42  d_op(op),
43  d_r(r){}
44  virtual ~LFSCLraAxiom(){}
45  long int get_length(){ return 15; }
46 public:
47  virtual LFSCLraAxiom* AsLFSCLraAxiom(){ return this; }
48  void print_pf( std::ostream& s, int ind = 0 );
49  bool isTrivial() { return d_op==EQ; }
50  static LFSCProof* MakeEq();
51  static LFSCProof* Make( Rational r, int op ){ return new LFSCLraAxiom( op,r ); }
52  LFSCProof* clone() { return new LFSCLraAxiom( d_op, d_r ); }
53  int checkOp() { return d_op; }
54 };
55 
56 
57 // lra_mult_c
58 class LFSCLraMulC: public LFSCProof{
59 private:
62  int d_op; // = | > | >= | distinct
64  d_pf(pf),
65  d_r(r),
66  d_op(op){
67  d_op = pf->checkOp() != -1 ? pf->checkOp() : d_op;
68  }
69  virtual ~LFSCLraMulC(){}
70  long int get_length(){ return 20 + d_pf->get_string_length(); }
71 public:
72  virtual LFSCLraMulC* AsLFSCLraMulC(){ return this; }
73  bool isLraMulC() { return true; }
74  void print_pf( std::ostream& s, int ind = 0 );
75  static LFSCProof* Make(LFSCProof* pf, Rational r, int op);
76  LFSCProof* clone() { return new LFSCLraMulC( d_pf.get(), d_r, d_op ); }
77  int getNumChildren() { return 1; }
78  LFSCProof* getChild( int n ) { return d_pf.get(); }
79  int checkOp() { return d_op; }
80 };
81 
82 
83 // lra_sub_~_~
84 class LFSCLraSub: public LFSCProof{
85 private:
87  int d_op1, d_op2;
88  LFSCLraSub(LFSCProof* pf1, LFSCProof* pf2, int op1, int op2): LFSCProof(),
89  d_op1(op1),
90  d_op2(op2){
91  d_children[0] = pf1;
92  d_children[1] = pf2;
93  d_op1 = pf1->checkOp()!=-1 ? pf1->checkOp() : d_op1;
94  d_op2 = pf2->checkOp()!=-1 ? pf2->checkOp() : d_op2;
95  }
96  virtual ~LFSCLraSub(){}
97  long int get_length(){
98  return 20 + d_children[0]->get_string_length() + d_children[1]->get_string_length();
99  }
100 public:
101  virtual LFSCLraSub* AsLFSCLraSub(){ return this; }
102  void print_pf( std::ostream& s, int ind = 0 );
103  static LFSCProof* Make(LFSCProof* pf1, LFSCProof* pf2, int op1, int op2);
104  LFSCProof* clone() { return new LFSCLraSub( d_children[0].get(), d_children[1].get(), d_op1, d_op2 ); }
105  int getNumChildren() { return 2; }
106  LFSCProof* getChild( int n ) { return d_children[n].get(); }
107  int checkOp() { return get_knd_result( d_op1, d_op2 ); }
108 };
109 
110 class LFSCLraPoly : public LFSCProof
111 {
112 private:
114  int d_var;
115  int d_op;
116  LFSCLraPoly( LFSCProof* pf, int var, int op ) : LFSCProof(),
117  d_pf( pf ),
118  d_var( var ),
119  d_op( op ){
120  d_op = pf->checkOp() != -1 ? pf->checkOp() : d_op;
121  }
122  virtual ~LFSCLraPoly(){}
123  long int get_length(){ return 15 + d_pf->get_string_length(); }
124 public:
125  virtual LFSCLraPoly* AsLFSCLraPoly(){ return this; }
126  void print_pf( std::ostream& s, int ind = 0 );
127  static LFSCProof* Make( LFSCProof* pf, int var, int op ){
128  return new LFSCLraPoly( pf, var, op );
129  }
130  static LFSCProof* Make( const Expr& e, LFSCProof* p );
131  LFSCProof* clone() { return new LFSCLraPoly( d_pf.get(), d_var, d_op ); }
132  int getNumChildren() { return 1; }
133  LFSCProof* getChild( int n ) { return d_pf.get(); }
134  int checkOp() {
135  return get_normalized( d_op, d_var<0 );
136  }
137 
138 };
139 
140 class LFSCLraContra : public LFSCProof
141 {
142 private:
144  int d_op;
145  LFSCLraContra( LFSCProof* pf, int op ) : LFSCProof(),
146  d_pf( pf ),
147  d_op( op ){
148  d_op = pf->checkOp() != -1 ? pf->checkOp() : d_op;
149  }
150  virtual ~LFSCLraContra(){}
151  long int get_length(){ return 15 + d_pf->get_string_length(); }
152 public:
153  virtual LFSCLraContra* AsLFSCLraContra(){ return this; }
154  void print_pf( std::ostream& s, int ind = 0 ){
155  s <<"(lra_contra_" << kind_to_str(d_op) << " _ ";
156  d_pf->print( s, ind+1 );
157  s << ")";
158  }
159  static LFSCProof* Make( LFSCProof* pf, int op ){
160  return new LFSCLraContra( pf, op );
161  }
162  LFSCProof* clone() { return new LFSCLraContra( d_pf.get(), d_op ); }
163  int getNumChildren() { return 1; }
164  LFSCProof* getChild( int n ) { return d_pf.get(); }
165  int checkOp() { return d_op; }
166 };
167 
168 
169 #endif
RefPtr< LFSCProof > d_pf
Definition: LFSCLraProof.h:113
long int get_length()
Definition: LFSCLraProof.h:45
LFSCLraAxiom(int op)
Definition: LFSCLraProof.h:40
LFSCProof * clone()
Definition: LFSCLraProof.h:26
static LFSCProof * MakeEq()
Data structure of expressions in CVC3.
Definition: expr.h:133
LFSCProof * getChild(int n)
Definition: LFSCLraProof.h:164
LFSCLraContra(LFSCProof *pf, int op)
Definition: LFSCLraProof.h:145
long int get_length()
Definition: LFSCLraProof.h:19
static LFSCProof * Make(LFSCProof *pf1, LFSCProof *pf2, int op1, int op2)
virtual ~LFSCLraAxiom()
Definition: LFSCLraProof.h:44
virtual LFSCLraAdd * AsLFSCLraAdd()
Definition: LFSCLraProof.h:23
int checkOp()
Definition: LFSCLraProof.h:107
void print_pf(std::ostream &s, int ind=0)
static LFSCProof * Make(LFSCProof *pf, int op)
Definition: LFSCLraProof.h:159
int getNumChildren()
Definition: LFSCLraProof.h:77
LFSCProof * clone()
Definition: LFSCLraProof.h:104
void print_pf(std::ostream &s, int ind=0)
Definition: LFSCLraProof.h:154
long int get_string_length()
Definition: LFSCProof.h:73
LFSCProof * getChild(int n)
Definition: LFSCLraProof.h:133
LFSCLraAdd(LFSCProof *pf1, LFSCProof *pf2, int op1, int op2)
Definition: LFSCLraProof.h:12
LFSCLraAxiom(int op, Rational r)
Definition: LFSCLraProof.h:41
LFSCLraSub(LFSCProof *pf1, LFSCProof *pf2, int op1, int op2)
Definition: LFSCLraProof.h:88
int getNumChildren()
Definition: LFSCLraProof.h:132
virtual LFSCLraSub * AsLFSCLraSub()
Definition: LFSCLraProof.h:101
long int get_length()
Definition: LFSCLraProof.h:123
bool isTrivial()
Definition: LFSCLraProof.h:49
LFSCProof * clone()
Definition: LFSCLraProof.h:52
int getNumChildren()
Definition: LFSCLraProof.h:163
LFSCProof * clone()
Definition: LFSCLraProof.h:162
int get_normalized(int knd, bool isnot)
Definition: Util.cpp:100
LFSCProof * getChild(int n)
Definition: LFSCLraProof.h:106
T * get()
Definition: Object.h:56
long int get_length()
Definition: LFSCLraProof.h:97
virtual ~LFSCLraContra()
Definition: LFSCLraProof.h:150
LFSCProof * clone()
Definition: LFSCLraProof.h:131
void print_pf(std::ostream &s, int ind=0)
Rational d_r
Definition: LFSCLraProof.h:61
int checkOp()
Definition: LFSCLraProof.h:29
int checkOp()
Definition: LFSCLraProof.h:79
LFSCLraPoly(LFSCProof *pf, int var, int op)
Definition: LFSCLraProof.h:116
Rational d_r
Definition: LFSCLraProof.h:39
static LFSCProof * Make(Rational r, int op)
Definition: LFSCLraProof.h:51
virtual ~LFSCLraAdd()
Definition: LFSCLraProof.h:18
virtual LFSCLraAxiom * AsLFSCLraAxiom()
Definition: LFSCLraProof.h:47
RefPtr< LFSCProof > d_pf
Definition: LFSCLraProof.h:60
void print_pf(std::ostream &s, int ind=0)
void print_pf(std::ostream &s, int ind=0)
static LFSCProof * Make(LFSCProof *pf, Rational r, int op)
virtual LFSCLraContra * AsLFSCLraContra()
Definition: LFSCLraProof.h:153
LFSCLraMulC(LFSCProof *pf, Rational r, int op)
Definition: LFSCLraProof.h:63
string kind_to_str(int knd)
Definition: Util.cpp:17
LFSCProof * getChild(int n)
Definition: LFSCLraProof.h:28
static RefPtr< LFSCProof > eq
Definition: LFSCLraProof.h:37
void print(std::ostream &s, int ind=0)
Definition: LFSCProof.cpp:23
bool isLraMulC()
Definition: LFSCLraProof.h:73
virtual ~LFSCLraSub()
Definition: LFSCLraProof.h:96
int getNumChildren()
Definition: LFSCLraProof.h:27
static LFSCProof * Make(LFSCProof *pf, int var, int op)
Definition: LFSCLraProof.h:127
void print_pf(std::ostream &s, int ind=0)
Definition: LFSCLraProof.cpp:5
static LFSCProof * Make(LFSCProof *pf1, LFSCProof *pf2, int op1, int op2)
RefPtr< LFSCProof > d_children[2]
Definition: LFSCLraProof.h:86
long int get_length()
Definition: LFSCLraProof.h:70
long int get_length()
Definition: LFSCLraProof.h:151
RefPtr< LFSCProof > d_children[2]
Definition: LFSCLraProof.h:9
virtual int checkOp()
Definition: LFSCProof.cpp:83
int get_knd_result(int knd1, int knd2)
Definition: Util.cpp:111
Definition: kinds.h:61
RefPtr< LFSCProof > d_pf
Definition: LFSCLraProof.h:143
LFSCProof * clone()
Definition: LFSCLraProof.h:76
virtual LFSCLraMulC * AsLFSCLraMulC()
Definition: LFSCLraProof.h:72
LFSCProof * getChild(int n)
Definition: LFSCLraProof.h:78
virtual ~LFSCLraPoly()
Definition: LFSCLraProof.h:122
virtual ~LFSCLraMulC()
Definition: LFSCLraProof.h:69
int getNumChildren()
Definition: LFSCLraProof.h:105
virtual LFSCLraPoly * AsLFSCLraPoly()
Definition: LFSCLraProof.h:125