CVC3
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