CVC3
LFSCLraProof.cpp
Go to the documentation of this file.
1 #include "LFSCLraProof.h"
2 
3 //LFSCLraAdd ...
4 
5 void LFSCLraAdd::print_pf( std::ostream& s, int ind )
6 {
7  s<<"(lra_add_";
8  s <<kind_to_str(d_op1);
9  s <<"_";
10  s << kind_to_str(d_op2);
11  s <<" _ _ _ ";
12  d_children[0]->print(s, ind+1);
13  s<<" ";
14  d_children[1]->print(s, ind+1);
15  s<<")";
16 }
17 LFSCProof* LFSCLraAdd::Make(LFSCProof* pf1, LFSCProof* pf2, int op1, int op2)
18 {
19  if( pf1->isTrivial() )
20  return pf2;
21  else if( pf2->isTrivial() )
22  return pf1;
23  else{
24  op1 = pf1->checkOp()!=-1 ? pf1->checkOp() : op1;
25  op2 = pf2->checkOp()!=-1 ? pf2->checkOp() : op2;
26  if( get_knd_order( op1 )>get_knd_order( op2 ) )
27  return Make( pf2, pf1, op2, op1 );
28  else
29  return new LFSCLraAdd( pf1, pf2, op1, op2 );
30  }
31 }
32 
33 // LFSCLraAxiom ...
34 
36 
38  if( !eq.get() ){
39  eq = new LFSCLraAxiom( EQ );
40  }
41  return eq.get();
42 }
43 
44 void LFSCLraAxiom::print_pf( std::ostream& s, int ind )
45 {
46  s<<"(lra_axiom_" << kind_to_str(d_op);
47  if( d_op!= EQ ){
48  s << " ";
49  print_rational( d_r, s );
50  }
51  s<<")";
52 }
53 
54 //LFSCLraMulC ...
55 
56 void LFSCLraMulC::print_pf( std::ostream& s, int ind )
57 {
58  s <<"(lra_mul_c_"<<kind_to_str(d_op)<<" _ _ ";
59  print_rational( d_r, s );
60  s << " ";
61  d_pf->print( s, ind+1 );
62  s << ")";
63 }
64 
66 {
67  if( pf->isTrivial() || r==1 )
68  return pf;
69  else if( pf->AsLFSCLraMulC() ){
70  Rational rt = r*pf->AsLFSCLraMulC()->d_r;
71  if( rt==1 )
72  return pf->AsLFSCLraMulC()->d_pf.get();
73  else
74  return new LFSCLraMulC( pf->AsLFSCLraMulC()->d_pf.get(), rt, op );
75  }else
76  return new LFSCLraMulC( pf, r, op );
77 }
78 
79 //LFSCLraSub ...
80 
81 void LFSCLraSub::print_pf( std::ostream& s, int ind ){
82  s <<"(lra_sub_"<<kind_to_str(d_op1)<<"_"<<kind_to_str(d_op2)<<" _ _ _ ";
83  d_children[0]->print(s, ind+1);
84  s <<" ";
85  d_children[1]->print(s, ind+1);
86  s <<")";
87 }
88 
89 LFSCProof* LFSCLraSub::Make(LFSCProof* pf1, LFSCProof* pf2, int op1, int op2){
90  if( pf2->isTrivial() )
91  return pf1;
92  else if( pf1->isTrivial() ){
93  Rational r = Rational( -1 );
94  return LFSCLraMulC::Make( pf2, r, op2 );
95  }else
96  return new LFSCLraSub( pf1, pf2, op1, op2 );
97 }
98 
99 //LFSCLraPoly ...
100 
101 void LFSCLraPoly::print_pf( std::ostream& s, int ind ){
102  if( d_var<0 ){
103  s << "(lra_not_" << kind_to_str(get_normalized( d_op ));
104  s << "_to_" << kind_to_str(get_normalized( get_not( d_op ) ));
105  s << " _ _";
106  }
107  s << " (poly_form";
108  if( d_var<0 )
109  s << "_not";
110  s << " _ _ @pn" << abs( d_var ) << " ";
111  d_pf->print( s, ind );
112  s << ")";
113  if( d_var<0 )
114  s << ")";
115 }
116 
118 {
119  Expr e1 = queryAtomic( e );
120  Expr eb = queryAtomic( e, true );
121  if( is_eq_kind( e1.getKind() ) )
122  {
123  int m = queryM( e );
124  //get the required term that is needed to normalize
125  Expr et;
126  if( is_opposite( eb.getKind() ) )
127  et = Expr( MINUS, eb[1], eb[0] );
128  else
129  et = Expr( MINUS, eb[0], eb[1] );
130 
131  //et.print();
132 
133  //get the polynomial normalization proof number
134  int valT = queryMt( et );
135  //store it in d_pn_form (this will setup the proper pn*)
136  d_pn_form[eb] = valT;
137 
138  p = LFSCLraPoly::Make( p, m, eb.getKind() );
139  p->setChOp( get_normalized( e1.getKind() ) );
140  return p;
141  //if( m<0 )
142  //{
143  // os << "(lra_not_" << kind_to_str(get_normalized( eb.getKind() ));
144  // os << "_to_" << kind_to_str(get_normalized( get_not( eb.getKind() ) ));
145  // os << " _ _";
146  // os2 << ")";
147  //}
148  //os << " (poly_form";
149  //if( m<0 )
150  // os << "_not";
151  //os << " _ _ @pn" << abs( m ) << " ";
152  //os2 << ")";
153  }
154  else
155  {
156  ostringstream ose;
157  ose << "ERROR:make_polynomial_proof: Trying to make non-atomic " << e1 << " " << e.isNot() << std::endl;
158  ose << e << std::endl;
159  print_error( ose.str().c_str(), cout );
160  return NULL;
161  }
162 }