CVC3  2.4.1
TReturn.cpp
Go to the documentation of this file.
1 #include "TReturn.h"
2 
3 #include "LFSCUtilProof.h"
4 #include "LFSCLraProof.h"
5 #include "LFSCBoolProof.h"
6 #include "LFSCPrinter.h"
7 
8 TReturn::TReturn(LFSCProof* lfsc_pf, std::vector<int>& L, std::vector<int>& Lused, Rational r, bool hasR, int pvY):
9  d_lfsc_pf(lfsc_pf), d_c( r ), d_provesY(pvY){
10  d_hasRt = hasR;
11  for( int a=0; a<(int)L.size(); a++ )
12  d_L.push_back( L[a] );
13  for( int a=0; a<(int)Lused.size(); a++ )
14  d_L_used.push_back( Lused[a] );
15 
16 #ifdef DEBUG_MEM_STATS
17  static int counter = 0;
18  counter++;
19  cout << "make a tret " << counter << std::endl;
20 #endif
21  lcalced = false;
22 }
23 
25 {
26  if( !hasRational() && lhs->hasRational() )
27  return lhs->mult_rational( this );
28  else if( hasRational() ){
29  if( lhs->hasRational() )
30  return d_c*lhs->d_c;
31  else
32  return d_c;
33  }else
34  return lhs->d_c;
35 }
36 
37 void TReturn::getL( std::vector< int >& lget, std::vector< int >& lgetu ){
38 #ifndef OPTIMIZE
39  std::vector< int >::iterator i;
40  for( int a=0; a<(int)d_L.size(); a++ ){
41  i = std::find( lget.begin(), lget.end(), d_L[a] );
42  if( i==lget.end() ){
43  lget.push_back( d_L[a] );
44  }
45  }
46  for( int a=0; a<(int)d_L_used.size(); a++ ){
47  i = std::find( lgetu.begin(), lgetu.end(), d_L_used[a] );
48  if( i==lgetu.end() ){
49  lgetu.push_back( d_L_used[a] );
50  }
51  }
52 #endif
53 }
54 
55 #ifdef OPTIMIZE
56 void TReturn::calcL( std::vector< int >& lget, std::vector< int >& lgetu ){
57  if( !lcalced ){
58  d_L.clear();
59  d_L_used.clear();
60  d_lfsc_pf->calcL( d_L, d_L_used );
61  lcalced = true;
62  }
63  std::vector< int >::iterator i;
64  for( int a=0; a<(int)d_L.size(); a++ ){
65  i = std::find( lget.begin(), lget.end(), d_L[a] );
66  if( i==lget.end() ){
67  lget.push_back( d_L[a] );
68  }
69  }
70  for( int a=0; a<(int)d_L_used.size(); a++ ){
71  i = std::find( lgetu.begin(), lgetu.end(), d_L_used[a] );
72  if( i==lgetu.end() ){
73  lgetu.push_back( d_L_used[a] );
74  }
75  }
76 }
77 #endif
78 
79 
80 // make it so that the two TReturns agree on what they are proving
81 // t1 proves pf1, Y( pf1 ), or Y2( pf1 )
82 // t2 proves pf2, Y( pf2 ), or Y2( pf2 )
83 // on return, t1->d_proveY should equal t2->d_proveY
84 int TReturn::normalize_tret( const Expr& pf1, TReturn*& t1, const Expr& pf2, TReturn*& t2, bool rev_pol )
85 {
86  if( t1->getProvesY()!=t2->getProvesY() )
87  {
88  if( t1->getProvesY()>t2->getProvesY() )
89  return normalize_tret( pf2, t2, pf1, t1, rev_pol );
90  else
91  {
92  if( debug_conv )
93  cout << "normalizing proofs " << t1->getProvesY() << " " << t2->getProvesY() << " " << rev_pol << std::endl;
94 
95  if( t1->getProvesY()==0 && t2->getProvesY()==2 )
96  normalize_tr( pf1, t1, 2, rev_pol );
97  if( t1->getProvesY()==1 && t2->getProvesY()==2 )
98  normalize_tr( pf1, t1, 2, rev_pol );
99  if( t1->getProvesY()==0 && t2->getProvesY()==1 ){
100  if( normalize_tr( pf1, t1, 1, rev_pol, false )==-1 ){ //try to go 0 to 1 (optional)
101  if( normalize_tr( pf2, t2, 0, rev_pol, false )==-1 ){ //try to go 1 to 0 immediately (optional)
102  normalize_tr( pf1, t1, 2, rev_pol );
103  normalize_tr( pf2, t2, 2, rev_pol );
104  }
105  }
106  }
107  if( t2->getProvesY()==3 ){
108  normalize_tr( pf1, t1, 3, rev_pol );
109  }
110 
111  if( t1->getProvesY()!=t2->getProvesY() ){
112  ostringstream os;
113  os << "ERROR:normalize_tret: Could not normalize proofs " << t1->getProvesY() << " " << t2->getProvesY() << std::endl;
114  os << pf1[0] << " " << pf2[0] << std::endl;
115  print_error( os.str().c_str(), cout );
116  return -1;
117  }else{
118  return t1->getProvesY();
119  }
120  }
121  }
122  return t1->getProvesY();
123 }
124 
125 int TReturn::normalize_tr( const Expr& pf1, TReturn*& t1, int y, bool rev_pol, bool printErr )
126 {
127  TReturn* torig = t1;
128 
129  int chOp = t1->getLFSCProof()->getChOp();
130  std::vector< int > emptyL;
131  std::vector< int > emptyLUsed;
132  t1->getL( emptyL, emptyLUsed );
133 
134  if( t1->getProvesY()!=y )
135  {
136  if( debug_conv ){
137  cout << "normalizing tr " << t1->getProvesY() << " to " << y << " rev_pol = " << rev_pol << std::endl;
138  }
139  Expr e;
140  if( what_is_proven( pf1, e ) )
141  {
142  e = queryElimNotNot( e );
143  if( rev_pol ){
144  if( e.isIff() ){
145  //cout << "Warning: rev_pol called on IFF, 0 normalize to " << y << std::endl;
146  e = Expr( IFF, e[1], e[0] );
147  }else if( e.isImpl() ){
148  e = Expr( IMPLIES, e[1], e[0] );
149  }
150  }
151  Expr eb = queryAtomic( e, true );
152  if( y==3 )
153  {
154  if( t1->getProvesY()!=2 ){
155  if( normalize_tr( pf1, t1, 2, rev_pol )==-1 ){
156  return -1;
157  }
158  }
159  if( e.isIff() ){
160  e = Expr( IMPLIES, e[0], e[1] );
161  }
162  //clausify what t1 is proving
163  t1 = new TReturn( LFSCClausify::Make( e, t1->getLFSCProof() ), emptyL, emptyLUsed, nullRat, false, 3 );
164  }
165  else if( y==1 )
166  {
167  if( t1->getProvesY()==0 || t1->getProvesY()==2 ){
168  if( can_pnorm( eb ) )
169  {
170  t1 = new TReturn( LFSCLraPoly::Make( e, t1->getLFSCProof() ), emptyL, emptyLUsed,
171  t1->getRational(), t1->hasRational(), 1 );
172  }else{
173  //cout << "nrt kind = " << kind_to_str( eb.getKind() ) << std::endl;
174  }
175  }
176  }
177  else if( y==0 )
178  {
179  if( is_eq_kind( eb.getKind() ) ){
180  normalize_to_tf( e, t1, 0 );
181  }else if( e[0]==e[1] ){
182  ostringstream os1, os2;
183  os1 << "(iff_refl ";
185  os2 << ")";
186  t1 = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ),
187  emptyL, emptyLUsed, nullRat, false, 0 );
188  }else{
189  if( t1->getProvesY()==1 ){
190 #ifdef PRINT_MAJOR_METHODS
191  cout << ";[M]: Normalize 1 to 0, iff" << std::endl;
192 #endif
193  if( e[1].isFalse() )
194  {
195  Expr ea = Expr( NOT, e[0] );
196  normalize_to_tf( ea, t1, 0 );
197  ostringstream os1, os2;
198  os1 << "(" << ( e[0].getKind()==NOT ? "not_to_iff" : "iff_not_false" );
199  os1 << " _ ";
200  os2 << ")";
201  t1 = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), os2.str() ),
202  emptyL, emptyLUsed, nullRat, false, 0 );
203  }
204  else if( e[1].isTrue() )
205  {
206  normalize_to_tf( e[0], t1, 0 );
207  ostringstream os1, os2;
208  os1 << "(iff_true _ ";
209  os2 << ")";
210  t1 = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), os2.str() ),
211  emptyL, emptyLUsed, nullRat, false, 0 );
212  }
213  else if( printErr )
214  {
215  TReturn* torg = new TReturn( LFSCPfVar::Make( "@V", 0 ), emptyL, emptyLUsed,
216  t1->getRational(), t1->hasRational(), t1->getProvesY() );
217  TReturn *ti1, *ti2;
218  TReturn* to = torg;
219  if( normalize_tr( pf1, to, 2, rev_pol ) )
220  {
221  ti1 = to;
222  to = torg;
223  if( normalize_tr( pf1, to, 2, !rev_pol ) )
224  {
225  ti2 = to;
226  ostringstream os1, os2, os3, os4;
227  os1 << "(impl_elim _ _ ";
228  os2 << "(impl_intro _ _ (\\ @V0 (iff_intro _ _ ";
229  os3 << " ";
230  os4 << "))))";
231  std::vector< RefPtr< LFSCProof > > pfs;
232  pfs.push_back( t1->getLFSCProof() );
233  pfs.push_back( ti1->getLFSCProof() );
234  pfs.push_back( ti2->getLFSCProof() );
235  std::vector< string > strs;
236  strs.push_back( os1.str() );
237  strs.push_back( os2.str() );
238  strs.push_back( os3.str() );
239  strs.push_back( os4.str() );
240  t1 = new TReturn( LFSCProofGeneric::Make( pfs, strs ), emptyL, emptyLUsed, nullRat, false, 0 );
241  }
242  }
243  }
244  }
245  }
246  }
247  else if( y==2 )
248  {
249  if( t1->getProvesY()==0 )
250  {
252  if( e.isIff() ){
253  ostringstream os1, os2;
254  os1 << "(iff_elim_1 _ _ ";
255  os2 << ")";
256  p = LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), os2.str() );
257  }else{
258  //cout << "actually I can just drop it " << e << std::endl;
259  p = t1->getLFSCProof();
260  }
261  t1 = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 2 );
262  }
263  else if( t1->getProvesY()==1 )
264  {
265  if( is_eq_kind( eb.getKind() ) ){
266  normalize_to_tf( e, t1, 2 );
267  }else if( e.isIff() || e.isImpl() ){
268  Expr eatom1 = queryAtomic( e[0] );
269  Expr eatom2 = queryAtomic( e[1] );
270  //Expr ebase1 = queryAtomic( eatom1, true );
271  //Expr ebase2 = queryAtomic( eatom2, true );
272  int val1 = queryM( e[0] );
273  int val2 = queryM( e[1] );
274  int k1 = eatom1.getKind();
275  int k2 = eatom2.getKind();
276 
277  if( e[0]==e[1] ){
278  ostringstream os;
279  os << "(impl_refl_atom" << (val1<0 ? "_not" : "" );
280  os << " _ _ @a" << abs( val1 ) << ")";
281  //d_formulas_printed[queryAtomic( e[0], true )] = true;
282  t1 = new TReturn( LFSCProofGeneric::MakeStr( os.str().c_str()),
283  emptyL, emptyLUsed, nullRat, false, 2 );
284  }else if( eatom2.isFalse() || eatom2.isTrue() ){
285  if( eatom1.getKind()==eatom2.getKind() )
286  {
287 #ifdef PRINT_MAJOR_METHODS
288  cout << ";[M]: Normalize 1 to 2, iff/impl double logical iff" << std::endl;
289 #endif
290  if( e[0]!=e[1] ){
291  ostringstream ose;
292  ose << "Warning: normalize logical atoms, not equal ";
293  ose << e[0] << " " << e[1] << std::endl;
294  print_error( ose.str().c_str(), cout );
295  }
296  ostringstream os;
297  os << "impl_refl_" << ( eatom2.isFalse() ? "false" : "true" );
298  t1 = new TReturn( LFSCProofGeneric::MakeStr(os.str().c_str()),
299  emptyL, emptyLUsed, nullRat, false, 2 );
300  }
301  else if( eatom2.isTrue() )
302  {
303  normalize_to_tf( e[0], t1, 2 );
304  ostringstream oss1, oss2;
305  oss1 << "(iff_true_impl _ ";
306  oss2 << ")";
307  t1 = new TReturn( LFSCProofGeneric::Make( oss1.str(), t1->getLFSCProof(), oss2.str() ),
308  emptyL, emptyLUsed, nullRat, false, 2 );
309  }
310  else if( eatom2.isFalse() )
311  {
312 #ifdef PRINT_MAJOR_METHODS
313  // cout << ";[M]: Normalize 1 to 2, iff/impl logical iff" << std::endl;
314 #endif
315  //make proof for assumption
316  RefPtr< LFSCProof > p = LFSCPfVar::Make( "@v", abs( val1 ) );
317  p = LFSCLraPoly::Make( e[0], p.get() );
318 
319  p = LFSCLraAdd::Make( p.get(), t1->getLFSCProof(),
320  get_normalized( k1 ),
321  get_normalized( k1, true ) );
322  p = LFSCLraContra::Make( p.get(), is_comparison( k1 ) ? (int)GT : (int)DISTINCT );
323 
324  ostringstream oss1, oss2;
325  //oss1 << std::endl << "this is a normalization proof of " << e[0] << "->" << e[1] << std::endl;
326  //oss1 << "or a proof of " << eatom1 << " -> " << eatom2 << std::endl;
327  oss1 << "(impl_intro"; // << ( eatom2.isTrue() ? "_not" : "" );
328  oss1 << " _ _ (\\ @v" << abs( val1 ) << " ";
329  oss1 << "(bottom_elim ";
330  printer->print_formula( e[1], oss1 );
331  oss1 << " ";
332 
333  oss2 << ")))";
334  p = LFSCProofGeneric::Make( oss1.str(), p.get(), oss2.str() );
335  //p = LFSCAssume::Make( val1, p.get(), false, 1 );
336 
337  t1 = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 2 );
338  }
339  }
340  else if( is_eq_kind( k1 ) && is_eq_kind( k2 ) )
341  {
342 #ifdef PRINT_MAJOR_METHODS
343  //cout << ";[M]: Normalize 1 to 2, iff/impl" << std::endl;
344 #endif
346  //assume1
347  ostringstream os1, os2;
348  //os1 << "this is a normalization proof of " << e[0] << "->" << e[1] << std::endl;
349  //os1 << "or a proof of " << eatom1 << " -> " << eatom2 << std::endl;
350  os1 << "(impl_intro";
351  os1 << " _ _ (\\ ";
352  os1 << "@v" << abs( val1 ) << " ";
353  os2 << "))";
354 
355  //make proof for assumption
356  RefPtr< LFSCProof > p1 = LFSCPfVar::Make( "@v", abs( val1 ) );
357  RefPtr< LFSCProof > p2 = LFSCPfVar::Make( "@v", abs( val2 ) );
358 
359  //convert to polynomial proofs
360  p1 = LFSCLraPoly::Make( e[0], p1.get() );
361  Expr ea2 = Expr( NOT, e[1] );
362  p2 = LFSCLraPoly::Make( ea2, p2.get() );
363 
364  if( t1->hasRational() ){
365  if( rev_pol )
366  p2 = LFSCLraMulC::Make( p2.get(), t1->getRational(), get_normalized( k2, true ) );
367  else
368  p1 = LFSCLraMulC::Make( p1.get(), t1->getRational(), get_normalized( k1 ) );
369  }
370 
371  p = LFSCLraAdd::Make( p1.get(), p2.get(),
372  get_normalized( k1 ),
373  get_normalized( k2, true ) );
374 
375  p = LFSCLraSub::Make( p.get(), t1->getLFSCProof(),
376  is_comparison( k1 ) ? (int)GT : (int)DISTINCT, EQ );
377  p = LFSCLraContra::Make( p.get(),
378  is_comparison( k1 ) ? (int)GT : (int)DISTINCT );
379 
380  p = LFSCAssume::Make( val2, p.get(), false, 1 );
381 
382  p = LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() );
383 
384  t1 = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 2 );
385  }
386  else
387  {
388  ostringstream ose;
389  ose << "NTret 12 could not handle " << eatom1 << " " << eatom2;
390  print_error( ose.str().c_str(), cout );
391  }
392  }
393  }
394  }
395  }
396  }
397  t1->getLFSCProof()->setChOp( chOp );
398  if( t1->getProvesY()!=y )
399  {
400  if( printErr || debug_conv ){
401  ostringstream ose;
402  ose << "Failed normalize_tr " << t1->getProvesY() << " " << y << std::endl;
403  Expr e;
404  if( what_is_proven( pf1, e ) )
405  ose << "proven_expr = " << e << std::endl;
406  print_error( ose.str().c_str(), cout );
407  }
408  return -1;
409  }
410  else
411  {
412 #ifdef IGNORE_NORMALIZE
413  t1 = new TReturn( torig->getLFSCProof(), emptyL, emptyLUsed,
414  torig->getRational(), torig->hasRational(), y );
415  t1->getLFSCProof()->setChOp( chOp );
416  return t1->getProvesY();
417 #else
418  return t1->getProvesY();
419 #endif
420  }
421 }
422 
423 void TReturn::normalize_to_tf( const Expr& e, TReturn*& t1, int y )
424 {
425  int chOp = t1->getLFSCProof()->getChOp();
426  if( t1->getProvesY()!=1 ){
427  ostringstream ose;
428  ose << "Bad mode for norm to tf " << t1->getProvesY() << std::endl;
429  print_error( ose.str().c_str(), cout );
430  }
431  std::vector< int > emptyL;
432  std::vector< int > emptyLUsed;
433  t1->getL( emptyL, emptyLUsed );
434 
435  if( t1->getLFSCProof()->AsLFSCLraPoly() && false )
436  {
437 #ifdef PRINT_MAJOR_METHODS
438  cout << ";[M]: Normalize 1 to " << y << ", simplify case" << std::endl;
439 #endif
440  t1 = new TReturn( t1->getLFSCProof()->getChild( 0 ), emptyL, emptyLUsed, nullRat, false, y );
441  }
442  else
443  {
444 
445 #ifdef PRINT_MAJOR_METHODS
446  cout << ";[M]: Normalize 1 to " << y << ", iff/impl, atom" << std::endl;
447 #endif
448 
449  Expr eatom = queryAtomic( e );
450  int val = queryM( e );
451  int knd = eatom.getKind();
452 
453  //make proof for assumption
454  RefPtr< LFSCProof > p = LFSCPfVar::Make( "@v", abs( val ) );
455  //convert to polynomial proof
456  Expr ea = Expr( NOT, e );
457  p = LFSCLraPoly::Make( ea, p.get() );
458 
460  LFSCLraAdd::Make( p.get(), t1->getLFSCProof(),
461  get_normalized( knd, (val<0) ),
462  get_normalized( knd, !(val<0) ) ),
463  is_comparison( knd ) ? (int)GT : (int)DISTINCT );
464 
465  p = LFSCAssume::Make( val, p.get(), false, 1 );
466 
467  //ostringstream os1, os2;
468  //os1 << "This is the atomization of " << e << ":";
469  //os2 << " ";
470  //p = LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() );
471 
472  //we have concluded e
473  t1 = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, y );
474  }
475  t1->getLFSCProof()->setChOp( chOp );
476 }
bool isIff() const
Definition: expr.h:424
bool lcalced
Definition: TReturn.h:29
void print_formula(const Expr &clause, std::ostream &s)
Definition: LFSCPrinter.h:42
Data structure of expressions in CVC3.
Definition: expr.h:133
static LFSCProof * Make(LFSCProof *pf1, LFSCProof *pf2, int op1, int op2)
bool isTrue() const
Definition: expr.h:356
bool isImpl() const
Definition: expr.h:425
static int queryM(const Expr &expr, bool add=true, bool trusted=false)
Definition: LFSCObject.cpp:386
static LFSCProof * Make(LFSCProof *pf, int op)
Definition: LFSCLraProof.h:159
bool isFalse() const
Definition: expr.h:355
static LFSCProof * Make(const Expr &e, bool isH=false)
Definition: LFSCUtilProof.h:17
Definition: kinds.h:66
virtual LFSCLraPoly * AsLFSCLraPoly()
Definition: LFSCProof.h:52
static LFSCProof * Make(const char *c, int v)
Rational d_c
Definition: TReturn.h:20
Rational mult_rational(TReturn *lhs)
Definition: TReturn.cpp:24
static LFSCPrinter * printer
Definition: LFSCObject.h:16
bool is_eq_kind(int knd)
Definition: Util.cpp:47
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
int get_normalized(int knd, bool isnot)
Definition: Util.cpp:100
static void print_error(const char *c, std::ostream &s)
Definition: Object.h:95
static Expr queryAtomic(const Expr &expr, bool getBase=false)
Definition: LFSCObject.cpp:365
T * get()
Definition: Object.h:56
int getProvesY()
Definition: TReturn.h:38
Rational getRational()
Definition: TReturn.h:36
static LFSCProof * Make(vector< RefPtr< LFSCProof > > &d_pfs, std::vector< string > &d_strs, bool db_str=false)
Definition: LFSCUtilProof.h:80
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
static bool what_is_proven(const Expr &pf, Expr &pe)
Definition: LFSCObject.cpp:539
LFSCProof * getLFSCProof()
Definition: TReturn.h:37
int getKind() const
Definition: expr.h:1168
T abs(T t)
Definition: cvc_util.h:53
static bool can_pnorm(const Expr &e)
Definition: LFSCObject.cpp:520
static LFSCProof * Make(int v, LFSCProof *pf)
Definition: LFSCBoolProof.h:76
static LFSCProof * MakeStr(const char *c, bool db_str=false)
static LFSCProof * Make(LFSCProof *pf, Rational r, int op)
Definition: kinds.h:71
static bool debug_conv
Definition: LFSCObject.h:24
TReturn(LFSCProof *lfsc_pf, std::vector< int > &L, std::vector< int > &Lused, Rational r, bool hasR, int pvY)
Definition: TReturn.cpp:8
virtual LFSCProof * getChild(int n)
Definition: LFSCProof.h:101
std::vector< int > d_L
Definition: TReturn.h:16
static LFSCProof * Make(LFSCProof *pf, int var, int op)
Definition: LFSCLraProof.h:127
bool is_comparison(int knd)
Definition: Util.cpp:70
static Expr queryElimNotNot(const Expr &expr)
Definition: LFSCObject.cpp:356
static LFSCProof * Make(LFSCProof *pf1, LFSCProof *pf2, int op1, int op2)
std::vector< int > d_L_used
Definition: TReturn.h:18
Definition: kinds.h:63
Definition: kinds.h:61
void setChOp(int c)
Definition: LFSCProof.h:104
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
static LFSCProof * Make(int v, LFSCProof *pf, bool assm=true, int type=3)
static Rational nullRat
Definition: LFSCObject.h:29
static void normalize_to_tf(const Expr &pf, TReturn *&t1, int y)
Definition: TReturn.cpp:423
Definition: kinds.h:70
int getChOp()
Definition: LFSCProof.h:103