CVC3  2.4.1
LFSCConvert.cpp
Go to the documentation of this file.
1 #include "LFSCConvert.h"
2 
3 #include "LFSCUtilProof.h"
4 #include "LFSCBoolProof.h"
5 #include "LFSCLraProof.h"
6 
7 std::map< Expr, int > vMap;
8 
10 {
11  nodeCount = 0;
12  nodeCountTh = 0;
13  unodeCount = 0;
14  unodeCountTh = 0;
16 }
17 
18 void LFSCConvert::convert( const Expr& pf )
19 {
20  TReturn* tfinal = cvc3_to_lfsc( pf, false, false );
21  pfinal = tfinal->getLFSCProof();
22 
23  //print out sat_lem if we are in clausal form
24  if( tfinal->getProvesY()==3 ){
25  ostringstream os1, os2;
26  os1 << "(satlem _ _ _ ";
27  os2 << "(\\ @done @done))" << endl;
28  pfinal = LFSCProofGeneric::Make( os1.str(), pfinal.get(), os2.str() );
29  }
30 
31  //print out all necessary proof let's
33 
34  //double ratio = (double)( nodeCountTh )/double( nodeCount + nodeCountTh );
35  //cout << "Theory Node ratio : " << ratio << endl;
36  //cout << "Node Count : " << nodeCount << endl;
37  //cout << "Th Node Count : " << nodeCountTh << endl;
38  //cout << "Total Count : " << ( nodeCount + nodeCountTh ) << endl;
39  //cout << (double)( nodeCountTh )/double( nodeCount + nodeCountTh ) << endl;
40  //cout << "uNode Count : " << unodeCount << endl;
41  //cout << "Th uNode Count : " << unodeCountTh << endl;
42  //cout << "LFSC proof count: " << LFSCProof::get_proof_counter() << endl;
43  //cout << "getNumNodes : " << getNumNodes( pf, false ) << endl;
44  //nnode_map.clear();
45  //cout << "getNumNodes(rc) : " << getNumNodes( pf, true ) << endl;
46  //cout << "map size 1 : " << (int)d_th_trans_map[1].size() << endl;
47  //cout << "map size 2 : " << (int)d_th_trans_map[0].size() << endl;
48  //std::map< Expr, int >::iterator vmIt = vMap.begin();
49  //while( vmIt != vMap.end() ){
50  // cout << (*vmIt).first << ": " << (*vmIt).second << endl;
51  // ++vmIt;
52  //}
53  //exit( 0 );
54 }
55 
56 // helper method to identify axioms of the form |- 0 = 0
57 bool LFSCConvert::isTrivialTheoryAxiom(const Expr& expr, bool checkBody){
58  if( expr[0]==d_plus_predicate_str || expr[0]==d_right_minus_left_str ||
59  expr[0]==d_minus_to_plus_str || expr[0]==d_mult_ineqn_str ||
60  expr[0]==d_canon_mult_str || expr[0]==d_canon_plus_str ||
61  expr[0]==d_flip_inequality_str || expr[0]==d_negated_inequality_str ||
62  expr[0]==d_rewrite_eq_symm_str || expr[0]==d_refl_str ||
63  expr[0]==d_mult_eqn_str || expr[0]==d_canon_invert_divide_str ||
64  expr[0]==d_rewrite_eq_refl_str || expr[0]==d_uminus_to_mult_str ||
65  expr[0]==d_rewrite_not_true_str || expr[0]==d_rewrite_not_false_str ||
66  expr[0]==d_int_const_eq_str ){
67  Expr pe;
68  Expr yexpr;
69  if( !checkBody || ( what_is_proven( expr, pe ) && getY( pe, yexpr ) ) ){
70  return true;
71  }else{
72  //cout << "Trivial theory axiom with bad arguments : " << expr[0] << std::endl;
73  }
74  }
75  return false;
76  //FIXME: should rewrite_not_true be used in theory lemma? expr==d_rewrite_not_true_str
77 }
78 
80 {
81  return ( expr==d_rewrite_not_not_str );
82 }
83 
84 
85 // *****NOTE that these rules must have a subproof expr[2]
87 {
88  return ( expr==d_iff_not_false_str || expr==d_iff_true_str ||
90  expr==d_not_not_elim_str || expr==d_not_to_iff_str );
91 }
92 
93 TReturn* LFSCConvert::cvc3_to_lfsc(const Expr& pf, bool beneath_lc, bool rev_pol){
94  if( beneath_lc )
95  nodeCountTh++;
96  else
97  nodeCount++;
98  if( lfsc_mode==5){
99  cvc3_mimic = cvc3_mimic_input || !beneath_lc;
100  }
101  int cvcm = cvc3_mimic ? 1 : 0;
102  TReturn* tRetVal = NULL;
103  //if( !tRetVal && cvcm==0 ){
104  // tRetVal = d_th_trans_map[1][pf];
105  //}
106  if( d_th_trans_map[cvcm].find( pf )!=d_th_trans_map[cvcm].end() ){
107  tRetVal = d_th_trans_map[cvcm][pf];
108  if( d_th_trans_lam[cvcm].find( tRetVal )==d_th_trans_lam[cvcm].end() ){
109  if( debug_conv )
110  cout << "set th_trans" << std::endl;
111  //set this TReturn to be lambda'ed into a let proof
112  d_th_trans_lam[cvcm][tRetVal] = true;
113  }
114  return tRetVal;
115  }
116 
117  if( beneath_lc )
118  unodeCountTh++;
119  else
120  unodeCount++;
121 
122  //if( (unodeCountTh + unodeCount)%10000==0 )
123  // cout << unodeCount << " " << unodeCountTh << endl;
124  //if( pf.isSelected() )
125  // std::cout << "already did this one?" << std::endl;
126 
127  if( vMap.find( pf[0] )==vMap.end() ){
128  vMap[ pf[0] ] = 0;
129  }
130  vMap[ pf[0] ]++;
131 
132 
133  std::vector< int > emptyL;
134  std::vector< int > emptyLUsed;
135  int yMode = -2;
136  ostringstream ose;
137  if( debug_conv ){
138  cout << "handle ";
139  pf[0].print();
140  }
141  Expr pfMod;
142  int pfPat = get_proof_pattern( pf, pfMod );
143  if( pfPat==0 )
144  {
145  if (pf[0] == d_CNF_str ){
146  RefPtr< LFSCProof > p = LFSCProof::Make_CNF( pf[2], pf[1], pf[4].getRational().getNumerator().getInt() );
147  if( p.get() )
148  {
149  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
150  }
151  }
152  else if( pf[0] == d_CNFITE_str ){
153  if( pf[5].isRational() ){
154  RefPtr< LFSCProof > p = LFSCProof::Make_CNF( pf[1], d_ite_s, pf[5].getRational().getNumerator().getInt() );
155  if( p.get() ){
156  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
157  }
158  }
159  }else if( pf[0] == d_cnf_add_unit_str ){
160  TReturn* t = cvc3_to_lfsc( pf[2] );
161  yMode = TReturn::normalize_tr( pf[2], t, 3 );
162  if( yMode==3 ){
163  tRetVal = t;
164  }
165  }
166  else if( pf[0] == d_cnf_convert_str ){
167  if( pf.arity()>3 ){
168  if( ignore_theory_lemmas && pf[3][0]==d_learned_clause_str ){
169  TReturn* t = make_trusted( pf );
170  tRetVal = new TReturn( LFSCClausify::Make( pf[1], t->getLFSCProof(), true ), emptyL, emptyLUsed, nullRat, false, 3 );
171  }else{
172  TReturn* t = cvc3_to_lfsc( pf[3],beneath_lc, rev_pol);
173  if( TReturn::normalize_tr( pf[3], t, 3, rev_pol )==3 ){
175  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
176  }
177  }
178  }
179  }
180  else if( pf[0] == d_bool_res_str ){
181  //ajr_debug_print( pf );
182  TReturn* t1 = cvc3_to_lfsc( pf[2],beneath_lc, rev_pol);
183  TReturn* t2 = cvc3_to_lfsc( pf[3],beneath_lc, rev_pol);
184  //t1->getL( emptyL, emptyLUsed );
185  //t2->getL( emptyL, emptyLUsed );
186  TReturn::normalize_tr( pf[2], t1, 3, rev_pol );
187  TReturn::normalize_tr( pf[3], t2, 3, rev_pol );
188  if( t1->getProvesY()==3 && t2->getProvesY()==3 ){
189  tRetVal = new TReturn( LFSCBoolRes::Make( t1->getLFSCProof(), t2->getLFSCProof(), pf[1], pf ),
190  emptyL, emptyLUsed, nullRat, false, 3 );
191  }
192  }
193  else if( pf[0] == d_minisat_proof_str ){
194  tRetVal = cvc3_to_lfsc( pf[2] );
195  }
196  else if(pf[0]==d_assump_str){ //assumptions rule
197  Expr ce = cascade_expr( pf[1] );
198  int val = queryM( ce );
200  yMode = 0;
201  if( d_assump_map.find( ce ) != d_assump_map.end() ){
202  //cout << "This is an assumption: " << pf[1] << std::endl;
203  p = LFSCPfVar::Make( "@F", abs( val ) );
204  if( !cvc3_mimic ){
205 #ifndef LRA2_PRIME
206  p = LFSCProof::Make_not_not_elim( pf[1], p.get() );
207 #endif
208  }
209  }else if( beneath_lc ){
210  p = LFSCPfVar::MakeV( abs( val ) );
211  if( cvc3_mimic ){
212  //ostringstream os1, os2;
213  //os1 << "(spec ";
214  //RefPtr< LFSCProof > ps = LFSCProofExpr::Make( pf[1] );
215  //os2 << ")";
216  //p = LFSCProofGeneric::Make( os1.str(), p.get(), ps.get(), os2.str() );
217  d_formulas_printed[queryAtomic( ce, true )] = true;
218  }
219 #ifdef OPTIMIZE
220  p->assumeVarUsed = val;
221 #else
222  emptyLUsed.push_back( val );
223 #endif
224  }else{
225  ostringstream os;
226  os << "WARNING: Assuming a trusted formula: " << ce << std::endl;
227  print_error( os.str().c_str(), cout );
228  int valT = queryM( ce, true, true );
229  p = LFSCPfVar::Make( "@T", abs( valT ) );
230  }
231  if( beneath_lc ){
232 #ifdef OPTIMIZE
233  p->assumeVar = val;
234 #else
235  emptyL.push_back( val );
236 #endif
237  if( !cvc3_mimic ){
238  Expr ey;
239  if( getY( ce, ey ) ){
240  p = LFSCLraPoly::Make( ce, p.get() );
241  yMode = 1;
242  }else{
243  ostringstream os;
244  os << "WARNING: Beneath a learned clause and Y is not defined for assumption " << pf[1] << std::endl;
245  print_error( os.str().c_str(), cout );
246  }
247  }
248  }
249  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, yMode );
250  }
251  else if( pf[0] == d_iff_trans_str ){
252  TReturn* t1 = cvc3_to_lfsc(pf[4],beneath_lc, rev_pol);
253 #ifdef LRA2_PRIME
254  if( ( isTrivialBooleanAxiom( pf[5][0] ) || pf[5][0]==d_rewrite_not_true_str ) && !cvc3_mimic && t1->getProvesY()==1 ){
255 #else
256  if( ( isTrivialBooleanAxiom( pf[5][0] ) || pf[5][0]==d_rewrite_not_true_str ) && !cvc3_mimic ){
257 #endif
258  tRetVal = t1;
259  }else{
260  TReturn* t2 = cvc3_to_lfsc(pf[5],beneath_lc, rev_pol);
261  t1->getL( emptyL, emptyLUsed );
262  t2->getL( emptyL, emptyLUsed );
263  yMode = TReturn::normalize_tret( pf[4], t1, pf[5], t2, rev_pol );
264  //case for arithmetic simplification
265  if( yMode==1 )
266  {
267  int knd2 = queryAtomic( pf[2] ).getKind();
268  int knd3 = queryAtomic( pf[3] ).getKind();
269  //if we have an equation on the RHS
270  if( is_eq_kind( knd3 ) )
271  {
272  RefPtr< LFSCProof > lfsc_pf = t1->getLFSCProof();
273  if( t2->hasRational() )
274  lfsc_pf = LFSCLraMulC::Make(t1->getLFSCProof(), t2->getRational(), EQ);
275  LFSCLraAdd::Make( lfsc_pf.get(), t2->getLFSCProof(), EQ, EQ);
276 
277  Rational newR = t1->mult_rational( t2 );
278  tRetVal = new TReturn(lfsc_pf.get(), emptyL, emptyLUsed, t1->mult_rational( t2 ), t1->hasRational() || t2->hasRational(),1);
279  }
280  else if( knd3==FALSE_EXPR || knd3==TRUE_EXPR )
281  {
282 #ifdef PRINT_MAJOR_METHODS
283  cout << ";[M]: iff_trans, logical " << (knd3==TRUE_EXPR) << std::endl;
284 #endif
286  if ( knd3==TRUE_EXPR ){
287  p = LFSCLraAdd::Make( t1->getLFSCProof(), t2->getLFSCProof(), EQ, is_eq_kind( knd2 ) ? get_normalized( knd2, true ) : EQ );
288  }else{
289  p = LFSCLraSub::Make( t2->getLFSCProof(), t1->getLFSCProof(), is_eq_kind( knd2 ) ? get_normalized( knd2, true ) : EQ, EQ );
290  }
291  if( t1->hasRational() ){
292  Rational r = 1/t1->getRational();
293  p = LFSCLraMulC::Make( p.get(), r, is_eq_kind( knd2 ) ? get_normalized( knd2, true ) : EQ );
294  }
295  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
296  }
297  }else if( yMode == 3 ){
298 //#ifdef PRINT_MAJOR_METHODS
299 // cout << ";[M]: iff_trans, boolean " << std::endl;
300 //#endif
301 // //resolving on the middle formula
302 // RefPtr< LFSCProof > p;
303 // if( rev_pol ){
304 // p = LFSCBoolRes::Make( t2->getLFSCProof(), t1->getLFSCProof(), pf[2], pf );
305 // }else{
306 // p = LFSCBoolRes::Make( t1->getLFSCProof(), t2->getLFSCProof(), pf[2], pf );
307 // }
308  //tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, 1, 1, 3 );
309  }else if( yMode == 0 || yMode==2 ){
310  ostringstream os1;
311  os1 << "(" << (yMode==0 ? "iff" : "impl" ) << "_trans _ _ _ ";
312  //if( yMode==2 && t1->getLFSCProof()->get_string_length()<100 ){
313  // os1 << "[";
314  // t1->getLFSCProof()->print( os1, 0 );
315  // os1 << "]";
316  //}
317  ostringstream os2;
318  os2 << ")";
319 
320  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ),
321  emptyL, emptyLUsed, nullRat, false, yMode );
322  }
323  }
324  }
325  else if (pf[0] == d_iff_mp_str ){ //iff_mp rule
326  TReturn* t1 = cvc3_to_lfsc(pf[3],beneath_lc);
327 #ifdef LRA2_PRIME
328  if( isTrivialBooleanAxiom( pf[4][0] ) && !cvc3_mimic && t1->getProvesY()==1 ){
329 #else
330  if( isTrivialBooleanAxiom( pf[4][0] ) && !cvc3_mimic ){
331 #endif
332  tRetVal = t1;
333  }else{
334  TReturn* t2 = cvc3_to_lfsc(pf[4],beneath_lc);
335  t1->getL( emptyL, emptyLUsed );
336  t2->getL( emptyL, emptyLUsed );
337  if( t1->getProvesY()==1 && t2->getProvesY()==1 )
338  {
339  yMode = 1;
340  int knd = queryAtomic( pf[1] ).getKind();
341  int knd2 = queryAtomic( pf[2] ).getKind();
342  if( is_eq_kind( knd2 ) )
343  {
345  if( t2->hasRational() )
346  p = LFSCLraMulC::Make(p.get(), t2->getRational(), get_normalized( knd ));
347  p = LFSCLraSub::Make( p.get(), t2->getLFSCProof(), get_normalized( knd ), EQ);
348  tRetVal = new TReturn(p.get(), emptyL, emptyLUsed, t2->getRational(), t2->hasRational() , 1);
349  }else if( knd2==FALSE_EXPR ){ //false case
350 #ifdef PRINT_MAJOR_METHODS
351  //cout << ";[M]: iff_mp, false" << std::endl;
352 #endif
353  //becomes a contradiction
355  p = LFSCLraAdd::Make( p.get(), t2->getLFSCProof(),
356  get_normalized( knd ),
357  get_normalized( knd, true ) );
358  p = LFSCLraContra::Make( p.get(), is_comparison( knd ) ? (int)GT : (int)DISTINCT );
359  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
360  }
361  }else if( t2->getProvesY()==3 || t1->getProvesY()==3 ){
362 // yMode = TReturn::normalize_tret( pf[3], t1, pf[4], t2, rev_pol );
363 // if( yMode==3 ){
364 //#ifdef PRINT_MAJOR_METHODS
365 // cout << ";[M]: iff_mp, boolean" << std::endl;
366 //#endif
367 // //do boolean resolution
368 // tRetVal = new TReturn( LFSCBoolRes::Make( t1->getLFSCProof(), t2->getLFSCProof(), pf[1], pf ),
369 // emptyL, emptyLUsed, nullRat, false, 3 );
370 // }
371  }else{
372  if( t2->getProvesY()!=1 || TReturn::normalize_tr( pf[4], t2, 2, rev_pol )!=-1 ){
373  if( t1->getProvesY()!=1 || TReturn::normalize_tr( pf[3], t1, 2, rev_pol )!=-1 ){
374  ostringstream os1;
375  os1 << "(" << (t2->getProvesY()==0 ? "iff" : "impl" ) << "_mp _ _ ";
376  ostringstream os2;
377  os2 << ")";
378  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
379  }
380  }
381  }
382  }
383  }
384  else if(pf[0]==d_iff_symm_str )
385  {
386  TReturn* t = cvc3_to_lfsc( pf[3], beneath_lc, !rev_pol );
387  yMode = t->getProvesY();
388  t->getL( emptyL, emptyLUsed );
389  if( yMode==1 )
390  {
391 #ifdef PRINT_MAJOR_METHODS
392  cout << ";[M]: iff_symm" << std::endl;
393 #endif
394  if( t->hasRational() ){
395  Rational r = 1/t->getRational();
396  //adding this
397  Rational rNeg = -1/t->getRational();
399  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, r, true, 1 );
400  }else{
401  Rational r = Rational( -1 );
403  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
404  }
405  }
406  else if( yMode==0 )
407  {
408  tRetVal = new TReturn( LFSCProof::Make_mimic( pf, t->getLFSCProof(), 2 ), emptyL, emptyLUsed, t->getRational(), t->hasRational(), 0 );
409  }
410  }
411  else if(pf[0]==d_impl_mp_str){ // impl_mp rule
412  // get subproofs
413  TReturn* t1 = cvc3_to_lfsc(pf[3],beneath_lc);
414  TReturn* t2 = cvc3_to_lfsc(pf[4],beneath_lc);
415  t1->getL( emptyL, emptyLUsed );
416  t2->getL( emptyL, emptyLUsed );
417  yMode = TReturn::normalize_tret( pf[3], t1, pf[4], t2);
418  if( yMode==1 ){
419  int knd1 = get_normalized( queryAtomic( pf[1] ).getKind() );
420  int knd2 = get_normalized( queryAtomic( pf[2] ).getKind() );
421  if( is_eq_kind( knd2 ) )
422  {
423 #ifdef PRINT_MAJOR_METHODS
424  cout << ";[M]: impl_mp" << std::endl;
425 #endif
426  RefPtr< LFSCProof > p1 = LFSCLraAdd::Make( t1->getLFSCProof(), t2->getLFSCProof(), knd1, knd2 );
427  // if non-homogenous case
428  if( knd1 == GT && knd2 == GE ){
429  ostringstream os1;
430  os1 <<"(>0_to_>=0_Real _";
431  ostringstream os2;
432  os2 <<")";
433  p1 = LFSCProofGeneric::Make(os1.str(), p1.get(), os2.str());
434  p1->setChOp( GE );
435  }
436  tRetVal = new TReturn(p1.get(), emptyL, emptyLUsed, nullRat, false, 1);
437  }else{
438  cout << "Kind = " << kind_to_str( knd2 ) << std::endl;
439  }
440  }
441  else
442  {
443  ostringstream os1, os2;
444  os1 << "(impl_mp _ _ ";
445  os2 << ")";
446  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0);
447  }
448  }
449  else if( pf[0]==d_basic_subst_op_str || pf[0]==d_basic_subst_op1_str )
450  {
451  if( pf.arity()==5 ){
452  // get subproofs
453  bool prevCvc3Mimic = cvc3_mimic;
454 #ifdef LRA2_PRIME
455  if( pf[1].getKind()==IFF || pf[1].getKind()==AND || pf[1].getKind()==OR && getNumNodes( pf )<=3 ){
456 #else
457  if( pf[1].getKind()==IFF ){
458 #endif
459  cvc3_mimic = true;
460  }
461 #ifdef PRINT_MAJOR_METHODS
462  cout << ";[M]: basic_subst_op1 " << kind_to_str( pf[1].getKind() ) << std::endl;
463 #endif
464  //cvc3_mimic = (( pe1.getKind()==AND || pe1.getKind()==OR ) && getNumNodes( pf1 )<5 ) ? true : prevCvc3Mimic;
465  TReturn* t1 = cvc3_to_lfsc(pf[3],beneath_lc, rev_pol);
466  //cvc3_mimic = (( pe1.getKind()==AND || pe1.getKind()==OR ) && getNumNodes( pf2 )<5 ) ? true : prevCvc3Mimic;
467  TReturn* t2 = cvc3_to_lfsc(pf[4],beneath_lc, rev_pol);
468  cvc3_mimic = prevCvc3Mimic;
469 
470  tRetVal = do_bso( pf, beneath_lc, rev_pol, t1, t2, ose );
471  }
472  }
473  else if( pf[0]==d_basic_subst_op0_str ){
474  if( pf.arity()==4 ){
475  TReturn* t = cvc3_to_lfsc(pf[3],beneath_lc, !rev_pol);
476  yMode = t->getProvesY();
477  t->getL( emptyL, emptyLUsed );
478  if( yMode==1 ){
479  if( pf[1].isNot() || pf[1].getKind()==UMINUS ){
480  if( !pf[2][0].isFalse() && !pf[2][0].isTrue() ){
482  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, t->getRational(), t->hasRational(), 1 );
483  }else{
484  tRetVal = t;
485  }
486  }
487  }else if( yMode==3 ){
488  }else if( yMode==2 ){
489  if( pf[1].isNot() ) //rev_pol should have switched things already
490  tRetVal = t;
491  }else if( yMode==0 ){
492  ostringstream os1;
493  os1 << "(basic_subst_op0_" << kind_to_str( pf[1].getKind() ) << " _ _ ";
494  ostringstream os2;
495  os2 << ")";
496  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
497  }
498  }
499  if( !tRetVal ){
500  ose << "subst0 kind = " << kind_to_str( pf[1].getKind() ) << std::endl;
501  ose << "subst0 arity = " << pf.arity() << std::endl;
502  }
503  }
504  else if( pf[0]==d_optimized_subst_op_str )
505  {
506  if( pf[1].getKind()==ITE ){
507 #ifdef PRINT_MAJOR_METHODS
508  cout << ";[M]: optimized_subst_op, ite " << std::endl;
509 #endif
510  //make reflexive proof of proven statement
512 
513  ostringstream os1, os2;
514  if( isFormula( pf[1] ) ){
515  os1 << "(iff_refl ";
516  }else{
517  os1 << "(refl Real ";
518  }
519  os2 << ")";
520  p = LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() );
521 
522  bool success = true;
523  for( int a=3; a<pf.arity(); a++ ){
524  if( success ){
525  success = false;
526  Expr pe;
527  if( what_is_proven( pf[a], pe ) )
528  {
529  int type = -1;
530  for( int b=0; b<3; b++ ){
531  if( pe[0]==pf[1][b] )
532  type = b;
533  }
534  //set cvc3 mimic to true if we are proving an equivalence of the conditional formula
535  bool prev_cvc3_mimic = cvc3_mimic;
536  if( type==0 || isFormula( pf[1] ) )
537  cvc3_mimic = true;
538 
539  TReturn* t = cvc3_to_lfsc(pf[a],beneath_lc);
540 
541  cvc3_mimic = prev_cvc3_mimic;
542 
543  t->getL( emptyL, emptyLUsed );
544  if( TReturn::normalize_tr( pf[a], t, 0 )==0 ){
545  if( type!=-1 ){
546  ostringstream os1, os2;
547  os1 << "(optimized_subst_op_";
548  if( isFormula( pf[1] ) )
549  os1 << "ifte";
550  else
551  os1 << "ite";
552  if( type==1 )
553  os1 << "_t1";
554  else if( type==2 )
555  os1 << "_t2";
556  os1 << " _ _ _ _ _ _ _ ";
557  os2 << ")";
558  p = LFSCProofGeneric::Make( os1.str(), p.get(), t->getLFSCProof(), os2.str() );
559  success = true;
560  }
561  }
562  }
563  }
564  }
565  if( success ){
566  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 0 );
567  }
568  }else if( pf[1].getKind()==PLUS ){
569  //cout << ";[M]: optimized_subst_op, plus " << std::endl;
570  TReturn* t = cvc3_to_lfsc(pf[3],beneath_lc);
571  yMode = t->getProvesY();
572  t->getL( emptyL, emptyLUsed );
573  if( t->getProvesY()==1 ){
574  tRetVal = t;
575  }else{
576  //tRetVal = make_trusted( pf );
577  Expr pe;
578  if( what_is_proven( pf[3], pe ) )
579  {
580  if( pe.getKind()==EQ )
581  {
582  ostringstream os1, os2;
583  os1 << "(canonize_conv _ _ _ _ _ _ ";
584  int pnt1 = queryMt( Expr( MINUS, pe[0], pe[1] ) );
585  int pnt2 = queryMt( Expr( MINUS, pf[1], pf[2] ) );
586  os1 << "@pnt" << pnt1 << " @pnt" << pnt2 << " ";
587  os2 << ")";
588  pntNeeded[ pnt1 ] = true;
589  pntNeeded[ pnt2 ] = true;
590  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t->getLFSCProof(), os2.str() ),
591  emptyL, emptyLUsed, t->getRational(), t->hasRational(), 0 );
592  }else{
593  cout << "proving kind " << kind_to_str( pe.getKind() ) << std::endl;
594  cout << pf[3][0] << " " << pe << std::endl;
595  }
596  }
597  }
598  }else{
599  //tRetVal = make_trusted( pf );
600  if( pf[1].arity()==pf.arity()-3 ){
601 #ifdef PRINT_MAJOR_METHODS
602  cout << ";[M]: optimized_subst_op, cascade " << kind_to_str( pf[1].getKind() ) << std::endl;
603 #endif
604  Expr pfn = pf[pf.arity()-1];
605  Expr cf1 = pf[1][pf.arity()-4];
606  Expr cf2 = pf[2][pf.arity()-4];
607  tRetVal = cvc3_to_lfsc( pf[pf.arity()-1], beneath_lc, rev_pol );
608  for( int a=(int)pf.arity()-2; a>=3; a-- ){
609  cf1 = Expr( pf[1].getKind(), pf[1][a-3], cf1 );
610  cf2 = Expr( pf[2].getKind(), pf[2][a-3], cf2 );
611  std::vector < Expr > exprs;
612  exprs.push_back( d_basic_subst_op1_str );
613  exprs.push_back( cf1 );
614  exprs.push_back( cf2 );
615  exprs.push_back( pf[a] );
616  exprs.push_back( pfn );
617  //cascade it, turn it into a different proof
618  pfn = Expr(PF_APPLY, exprs );
619  TReturn* tc = cvc3_to_lfsc( pf[a], beneath_lc, rev_pol );
620  tRetVal = do_bso( pfn, beneath_lc, rev_pol, tc, tRetVal, ose );
621  }
622  }else{
623  ose << "opt_subst_op arity pv1 = " << pf[1].arity() << " " << pf.arity()-3 << std::endl;
624  ose << "opt_subst_op arity pv2 = " << pf[2].arity() << " " << pf.arity()-3 << std::endl;
625  }
626  }
627  if( !tRetVal ){
628  for( int a=0; a<pf.arity(); a++ ){
629  if( a>=3 && pf[a].arity()>0 ){
630  ose << a << ": ";
631  ose << pf[a][0] << std::endl;
632  Expr pre;
633  what_is_proven( pf[a], pre );
634  ose << "wip: " << pre << std::endl;
635  }else{
636  ose << a << ": " << pf[a] << std::endl;
637  }
638  }
639  //RefPtr< LFSCProof > p;
640  //TReturn* curr = NULL;
641  //for( int a=(int)(pf.arity()-1); a>=4; a-- ){
642  // TReturn* t = cvc3_to_lfsc(pf[a],beneath_lc);
643  // if( curr ){
644  // int cyMode = TReturn::normalize_tret(
645  // if( pf[1].getKind()==AND || pf[1].getKind()==OR ){
646  // ostringstream os1, os2;
647  // os1 << "(optimized_subst_op_";
648  // if( yMode==2 )
649  // os1 << "impl_";
650  // os1 << kind_to_str( pf[1].getKind() );
651  // os1 << " _ _ _ _ ";
652  // os2 << ")";
653  // p = LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() );
654  // }else{
655  // curr = t;
656  // }
657  // tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, t->getProvesY() );
658  //}
659  ose << "opt_subst_op kind = " << kind_to_str( pf[1].getKind() ) << std::endl;
660  ose << "opt_subst_op arity = " << pf.arity() << std::endl;
661  }
662  }
663  else if( pf[0]==d_eq_trans_str ){
664  // get subproofs
665  TReturn* t1 = cvc3_to_lfsc(pf[5],beneath_lc);
666  TReturn* t2 = cvc3_to_lfsc(pf[6],beneath_lc);
667  t1->getL( emptyL, emptyLUsed );
668  t2->getL( emptyL, emptyLUsed );
669  yMode = TReturn::normalize_tret( pf[5], t1, pf[6], t2 );
670  if( yMode==1 ){
671  // merge literals
672  tRetVal = new TReturn( LFSCLraAdd::Make( t1->getLFSCProof(), t2->getLFSCProof(),
673  EQ, EQ ), emptyL, emptyLUsed, nullRat, false, 1 );
674  }else if( yMode==0 ){
675  std::vector< RefPtr< LFSCProof > > pfs;
676  std::vector< string > strs;
677  ostringstream os1, os2, os3;
678  os1 << "(trans Real ";
679  os2 << " ";
680  os3 << ")";
681  pfs.push_back( LFSCProofExpr::Make( pf[2] ) );
682  pfs.push_back( LFSCProofExpr::Make( pf[3] ) );
683  pfs.push_back( LFSCProofExpr::Make( pf[4] ) );
684  pfs.push_back( t1->getLFSCProof() );
685  pfs.push_back( t2->getLFSCProof() );
686  strs.push_back( os1.str() );
687  strs.push_back( os2.str() );
688  strs.push_back( os2.str() );
689  strs.push_back( os2.str() );
690  strs.push_back( os2.str() );
691  strs.push_back( os3.str() );
692  tRetVal = new TReturn( LFSCProofGeneric::Make( pfs, strs ), emptyL, emptyLUsed, nullRat, false, 0 );
693  }
694  }
695  else if(pf[0] == d_eq_symm_str){ // eq_symm rule
696  TReturn* t = cvc3_to_lfsc(pf[4],beneath_lc);
697  t->getL( emptyL, emptyLUsed );
698  if( t->getProvesY()==1 )
699  {
700  tRetVal = new TReturn(LFSCLraMulC::Make(t->getLFSCProof(), Rational( -1 ), EQ), emptyL, emptyLUsed, nullRat, false, 1);
701  }
702  else if( t->getProvesY()==0 )
703  {
704  ostringstream os1, os2;
705  os1 << "(symm Real _ _ ";
706  os2 << ")";
707  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0);
708  }
709  }
710  else if( pf[0]==d_real_shadow_str )
711  {
712  // get subproofs
713  TReturn* t1 = cvc3_to_lfsc(pf[3],beneath_lc);
714  TReturn* t2 = cvc3_to_lfsc(pf[4],beneath_lc);
715  t1->getL( emptyL, emptyLUsed );
716  t2->getL( emptyL, emptyLUsed );
717  yMode = TReturn::normalize_tret( pf[3], t1, pf[4], t2 );
718  if( yMode==1 )
719  {
720  int op1 = get_normalized( queryAtomic( pf[1] ).getKind() );
721  int op2 = get_normalized( queryAtomic( pf[2] ).getKind() );
722  tRetVal = new TReturn( LFSCLraAdd::Make( t1->getLFSCProof(), t2->getLFSCProof(), op1, op2 ), emptyL, emptyLUsed, nullRat, false, 1 );
723  }
724  else if( yMode==0 )
725  {
726  ostringstream os1, os2;
727  os1 << "(real_shadow_" << kind_to_str( pf[1].getKind() );
728  os1 << "_" << kind_to_str( pf[2].getKind() );
729  os1 << " _ _ _ ";
730  os2 << ")";
731  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ),
732  emptyL, emptyLUsed, nullRat, false, 0 );
733  }
734  }
735  else if( pf[0]==d_addInequalities_str )
736  {
737  // get subproofs
738  TReturn* t1 = cvc3_to_lfsc(pf[3],beneath_lc);
739  TReturn* t2 = cvc3_to_lfsc(pf[4],beneath_lc);
740  t1->getL( emptyL, emptyLUsed );
741  t2->getL( emptyL, emptyLUsed );
742  yMode = TReturn::normalize_tret( pf[3], t1, pf[4], t2 );
743  if( yMode==1 )
744  {
745  tRetVal = new TReturn( LFSCLraAdd::Make( t1->getLFSCProof(), t2->getLFSCProof(),
746  pf[1].getKind(), pf[2].getKind() ), emptyL, emptyLUsed, nullRat, false, 1 );
747  }
748  else if( yMode==0 )
749  {
750  ostringstream os1, os2;
751  os1 << "(add_inequalities_" << kind_to_str( pf[1].getKind() );
752  os1 << "_" << kind_to_str( pf[2].getKind() );
753  os1 << " _ _ _ _ ";
754  os2 << ")";
755  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ),
756  emptyL, emptyLUsed, nullRat, false, 0 );
757  }
758  }
759  else if( pf[0] == d_real_shadow_eq_str){
760  TReturn* t1 = cvc3_to_lfsc(pf[3], beneath_lc);
761  TReturn* t2 = cvc3_to_lfsc(pf[4], beneath_lc);
762  t1->getL( emptyL, emptyLUsed );
763  t2->getL( emptyL, emptyLUsed );
764  yMode = TReturn::normalize_tret( pf[3], t1, pf[4], t2 );
765  if( yMode==1 ){
766  ostringstream os1, os2;
767  os1 << "(lra_>=_>=_to_= _ _ ";
768  os2 << ")";
769  RefPtr< LFSCProof > p = LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() );
770  p->setChOp( EQ );
771  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
772  }else if( yMode==0 || yMode==2 ){
773  ostringstream os1, os2;
774  os1 << "(real_shadow_eq _ _";
775  os2 << ")";
776  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ),
777  emptyL, emptyLUsed, nullRat, false, 0 );
778  }
779  }
780  else if( pf[0]==d_cycle_conflict_str )
781  {
782  // get subproofs
783  bool isErr = false;
784  int n = ( pf.arity() - 1 )/2 + 1;
785  std::vector < TReturn* > trets;
786  for( int a=n; a<pf.arity(); a++ ){
787  if( !isErr ){
788  TReturn* t = cvc3_to_lfsc(pf[a],beneath_lc);
789  if( TReturn::normalize_tr( pf[a], t, 1 )!=1 ){
790  isErr = true;
791  }else{
792  trets.push_back( t );
793  t->getL( emptyL, emptyLUsed );
794  }
795  }
796  }
797  //add them together
798  if( !isErr ){
799  int currOp = get_normalized( pf[1].getKind() );
800  RefPtr< LFSCProof > p1 = trets[0]->getLFSCProof();
801  for( int a=1; a<(int)trets.size(); a++ ){
802  int op = get_normalized( pf[a+1].getKind() );
803  p1 = LFSCLraAdd::Make( trets[a]->getLFSCProof(), p1.get(), op, currOp );
804  if( op==GT ){
805  currOp = GT;
806  }else if( op==GE ){
807  currOp = currOp==GT ? GT : GE;
808  }
809  }
810  tRetVal = new TReturn( LFSCLraContra::Make( p1.get(), GT ), emptyL, emptyLUsed, nullRat, false, 0 );
811  }
812  }
813  else if( pf[0]==d_learned_clause_str )
814  {
815  if( pf.arity()==2 )
816  {
817  TReturn* t = cvc3_to_lfsc(pf[1],true);
818  t->getL( emptyL, emptyLUsed );
820 
821  Expr pe;
822  what_is_proven( pf[1], pe );
823  bool success = true;
824  if( !pe.isFalse() ){
825  success = false;
826  if( TReturn::normalize_tr( pf[1], t, 3, false )==3 )
827  {
828  p = t->getLFSCProof();
829  success = true;
830  }
831 #ifdef PRINT_MAJOR_METHODS
832  cout << ";[M]: learned clause, not proven false" << std::endl;
833 #endif
834  }
835  else if( cvc3_mimic && pf[1][0]!=d_cycle_conflict_str )
836  {
837  ostringstream os1, os2;
838  os1 << "(clausify_false ";
839  os2 << ")";
840  p = LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() );
841  }
842  if( success ){
843  //ostringstream os1, os2;
844  //if( debug_var )
845  // os1 << "LC:";
846  //we must close all proof-lets that contain free variables
847  //p = make_let_proof( p.get(), emptyL, false );
848 #ifdef OPTIMIZE
849  std::vector< int > assumes, assumesUsed;
850  t->calcL( assumes, assumesUsed );
851  for( int a=0; a<(int)assumes.size(); a++ ){
852  p = LFSCAssume::Make( assumes[a], p.get(), true );
853  }
854 #else
855  for( int a=0; a<(int)emptyL.size(); a++ ){
856  p = LFSCAssume::Make( emptyL[a], p.get(), true );
857  }
858 #endif
859  emptyL.clear();
860  emptyLUsed.clear();
861  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
862  }
863  }
864  }
865  else if( pf[0]==d_andE_str )
866  {
867  TReturn* t = cvc3_to_lfsc(pf[3],beneath_lc);
868  t->getL( emptyL, emptyLUsed );
869  if( t->getProvesY()==0 )
870  {
871  int pos = pf[1].getRational().getNumerator().getInt();
872  RefPtr< LFSCProof > p = LFSCProof::Make_and_elim( pf[2], t->getLFSCProof(), pos, pf[2][pos] );
873  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, t->getRational(), t->hasRational(), 0 );
874  }
875  else if( t->getProvesY()==3 )
876  {
877  //need to use and CNF rules
879  pf[1].getRational().getNumerator().getInt() );
880  p = LFSCBoolRes::Make( t->getLFSCProof(), p.get(), pf[2], pf );
881  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
882  }
883  }
884  else if( pf[0]==d_rewrite_implies_str )
885  {
886  if( !cvc3_mimic )
887  {
888  Expr ei = Expr( IMPLIES, pf[1], pf[2] );
890  if( p.get() )
891  {
892  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
893  }
894  }
895  else
896  {
897  //tRetVal = new TReturn( LFSCProofGeneric::MakeStr( "(rewrite_implies _ _)" ), emptyL, emptyLUsed, nullRat, false, 0 );
898  }
899  }
900  else if( pf[0]==d_rewrite_ite_same_str )
901  {
902  ostringstream os1, os2;
903  os1 << "(rewrite_ite_same ";
906  os2 << ")";
907  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ),
908  emptyL, emptyLUsed, nullRat, false, 0 );
909  }
910  else if( pf[0]==d_rewrite_and_str || pf[0]==d_rewrite_or_str )
911  {
912  //Expr e = Expr( IFF, pf[1], pf[2] );
913  bool isAnd = pf[0]==d_rewrite_and_str;
914  if( pf[1].arity()==2 && pf[1][0]==pf[1][1] ){ //try to apply binary redundant rule
915  ostringstream os1, os2 ;
916  os1 << "(" << ( isAnd ? "and" : "or" ) << "_redundant ";
918  os2 << ")";
919  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
920  }else if( isFlat( pf[2] ) ){ //try to do the normalize
921  Expr e1 = cascade_expr( pf[1] );
922  Expr e2 = cascade_expr( pf[2] );
923  Expr pe;
924  make_flatten_expr( e1, pe, pf[1].getKind() );
925  //cout << "we have an and normalize " << e1 << std::endl;
926  //cout << "making and normalize for " << pe << std::endl;
927  //cout << "this should be equal to " << e2 << std::endl;
928  //cout << (pe==e2) << std::endl;
929  if( pe==e2 ){ //standard and normalize
930  ostringstream os1, os2;
931  os1 << "(" << ( isAnd ? "and" : "or" ) << "_normalize _ ";
932  os2 << ")";
934  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
935  }
936  //else if( pf[1].arity()==2 ){ //try to normalize the symm version
937  // Expr e1s = cascade_expr( Expr( pf[1].getKind(), pf[1][1], pf[1][0] ) );
938  // make_flatten_expr( e1s, pe, pf[1].getKind() );
939  // if( pe==e2 ){
940  // ostringstream oss1, oss2, oss3, oss4;
941  // oss1 << "(iff_trans _ _ (" << ( isAnd ? "and" : "or" );
942  // oss1 << "_symm ";
943  // RefPtr< LFSCProof > pex1 = LFSCProofExpr::Make( pf[1][0] );
944  // oss2 << " ";
945  // RefPtr< LFSCProof > pex2 = LFSCProofExpr::Make( pf[1][1] );
946  // oss3 << ") " << "(" << ( isAnd ? "and" : "or" ) << "_normalize _ ";
947  // RefPtr< LFSCProof > ps = LFSCProofExpr::Make( e1s );
948  // oss4 << "))";
949  // std::vector< RefPtr< LFSCProof > > pfs;
950  // pfs.push_back( pex1.get() );
951  // pfs.push_back( pex2.get() );
952  // pfs.push_back( ps.get() );
953  // std::vector< string > strs;
954  // strs.push_back( oss1.str() );
955  // strs.push_back( oss2.str() );
956  // strs.push_back( oss3.str() );
957  // strs.push_back( oss4.str() );
958  // tRetVal = new TReturn( LFSCProofGeneric::Make( pfs, strs ), emptyL, emptyLUsed, nullRat, false, 0 );
959  // }
960  //}
961  }
962  if( !tRetVal ){
963  //going to have to trust it
964  TReturn* t = make_trusted( pf );
965  //this code runs the normalize side condition, but ignores it (for consistency with proof checking times)
966  ostringstream os1, os2;
967  os1 << "(" << (isAnd ? "and" : "or" ) << "_nd _ _ _ ";
968  os2 << ")";
969  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
970  }
971  }
972  else if( pf[0]==d_rewrite_iff_symm_str )
973  {
974  ostringstream os1, os2;
975  os1 << "(rewrite_iff_symm ";
978  os2 << ")";
979  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
980  }
981  else if( pf[0]== d_implyEqualities_str){
982 
983  if( pf.arity()==5 ){
984  TReturn* t1 = cvc3_to_lfsc(pf[3],beneath_lc);
985  TReturn* t2 = cvc3_to_lfsc(pf[4],beneath_lc);
986  t1->getL( emptyL, emptyLUsed );
987  t2->getL( emptyL, emptyLUsed );
988  if( TReturn::normalize_tr( pf[3], t1, 0 )==0 && TReturn::normalize_tr( pf[4], t2, 0 )==0 )
989  {
990  Expr e1, e2;
991  if( what_is_proven( pf[3], e1 ) && what_is_proven( pf[4], e2 ) )
992  {
993  int m1 = queryMt( Expr( MINUS, e1[1], e1[0] ) );
994  int m2 = queryMt( Expr( MINUS, e2[1], e2[0] ) );
995 
996  ostringstream os1, os2;
997  os1<<"(imply_equalities _ _ _ _ _ _ ";
998  os1 << "@pnt" << abs( m1 ) << " @pnt" << abs( m2 ) << " ";
999  os2 << ")";
1000  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1001  }
1002  }
1003  }
1004  }
1005  else if( pf[0]==d_implyWeakerInequality_str )
1006  {
1007 #ifdef PRINT_MAJOR_METHODS
1008  //cout << ";[M]: imply weaker equality " << pf[1] << std::endl;
1009 #endif
1010  if( !cvc3_mimic ){
1011  if( pf[1].arity()==2 && pf[2].arity()==2 && pf[1][1][0].isRational() && pf[2][1][0].isRational() )
1012  {
1013  //Rational r = pf[1][1][0].getRational() - pf[2][1][0].getRational();
1014  //tRetVal = new TReturn( LFSCLraAxiom::Make( r, GT ), emptyL, emptyLUsed, nullRat, false, 1 );
1015  tRetVal = new TReturn( LFSCLraAxiom::MakeEq(), emptyL, emptyLUsed, nullRat, false, 1 );
1016  }
1017  }else{
1018  Rational r1, r2;
1019  ostringstream os1, os2;
1020  getRat(pf[1][1][0], r1);
1021  getRat(pf[2][1][0], r2);
1023 
1024  os1 <<"(imply_weaker_inequality_" << kind_to_str( pf[1].getKind() ) << "_" << kind_to_str( pf[2].getKind() );
1025  if(pf[1][1].arity() > 2)
1026  {
1027  vector<Expr> t1_children;
1028  int start_i = 1;
1029  int end_i = pf[1][1].arity();
1030  for(int i = start_i; i < end_i; i ++) {
1031  const Expr& term = pf[1][1][i];
1032  t1_children.push_back(term);
1033  }
1034  p = LFSCProofExpr::Make(Expr(pf[1][1].getKind(), t1_children));
1035  }
1036  else
1037  {
1038  p = LFSCProofExpr::Make(pf[1][1][1]);
1039  }
1040  os2<<" ";
1041  print_rational(r1, os2);
1042  os2 << " ";
1043  print_rational(r2, os2);
1044  os2<<")";
1045  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ),
1046  emptyL, emptyLUsed, nullRat, false, 0 );
1047  }
1048  }
1049  else if( pf[0]==d_implyNegatedInequality_str )
1050  {
1051 #ifdef PRINT_MAJOR_METHODS
1052  //cout << ";[M]: imply negated equality " << pf[1] << std::endl;
1053 #endif
1054  if( !cvc3_mimic ){
1055  if( pf[1].arity()==2 && pf[2].arity()==2 && pf[1][1][0].isRational() && pf[2][1][0].isRational() )
1056  {
1057  //Rational r = -( pf[1][1][0].getRational() + pf[2][1][0].getRational() );
1058  //tRetVal = new TReturn( LFSCLraAxiom::Make( r, GT ), emptyL, emptyLUsed, nullRat, false, 1 );
1059  tRetVal = new TReturn( LFSCLraAxiom::MakeEq(), emptyL, emptyLUsed, nullRat, false, 1 );
1060  }
1061  }else{
1062  Rational r1, r2;
1063  if( getRat( pf[1][1][0], r1 ) && getRat(pf[2][1][0], r2) ){
1064  Expr ep = pf[1][1][1];
1065  Rational negOne = Rational( -1 );
1066  bool isNeg = false;
1067  if ( pf[1][1][1].getKind()==MULT && pf[1][1][1][0].isRational() && pf[1][1][1][0].getRational()==negOne ){
1068  isNeg = true;
1069  if(pf[1][1].arity() > 2)
1070  {
1071  vector<Expr> t1_children;
1072  int start_i = 1;
1073  int end_i = pf[1][1].arity();
1074  for(int i = start_i; i < end_i; i ++) {
1075  const Expr& term = pf[1][1][i];
1076  t1_children.push_back(term);
1077  }
1078  ep = Expr(pf[1][1].getKind(), t1_children);
1079  }
1080  else
1081  {
1082  ep = pf[1][1][1][1];
1083  }
1084 
1085  }
1086  if(r1 == r2) {
1087  ostringstream os1, os2;
1088  os1 << "(imply_negated_inequality_<" << (isNeg ? "n" : "" );
1089  os1 << " ";
1091  os2 << " ";
1092  print_rational( r1, os2 );
1093  os2 << ")";
1094  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ),
1095  emptyL, emptyLUsed, nullRat, false, 0 );
1096  }else{
1097  ostringstream os1, os2;
1098  os1 << "(imply_negated_inequality_";
1099  os1 << kind_to_str(pf[1].getKind()) << "_"<<kind_to_str(pf[2].getKind()) << (isNeg ? "n" : "" );
1100  os1 << " ";
1102  os2 << " ";
1103  print_rational( r1, os2 );
1104  os2 << " ";
1105  print_rational( r2, os2 );
1106  os2 << ")";
1107  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ),
1108  emptyL, emptyLUsed, nullRat, false, 0 );
1109  }
1110  }
1111  }
1112  }
1113  else if( pf[0]==d_rewrite_iff_str){
1114  ostringstream os1, os2;
1115 
1116  // then it's just the iff_refl rule
1117  if(pf[1] == pf[2]){
1118  os1 << "(iff_refl ";
1119  os2 << ")";
1121  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed,
1122  nullRat, false, 0 );
1123  }
1124  if(pf[1] == d_pf_expr.getEM()->trueExpr()){
1125  os1 << "(rewrite_iff_true_l ";
1127  os2 << ")";
1128  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1129  }
1130  if(pf[1] == d_pf_expr.getEM()->falseExpr()){
1131  os1 << "(rewrite_iff_false_l ";
1133  os2 << ")";
1134  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1135  }
1136  if(pf[2] == d_pf_expr.getEM()->trueExpr()){
1137  os1 << "(rewrite_iff_true_r ";
1139  os2 << ")";
1140  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1141  }
1142  if(pf[2] == d_pf_expr.getEM()->falseExpr()){
1143  os1 << "(rewrite_iff_false_r ";
1145  os2 << ")";
1146  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1147  }
1148  if(pf[1].isNot() && pf[1][0] == pf[2]){
1149  os1 << "(rewrite_iff_not_l ";
1150  RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1][0] );
1151 
1152  os2 << ")";
1153  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1154  }
1155  if(pf[2].isNot() && pf[2][0] == pf[1]){
1156  os1 << "(rewrite_iff_not_r ";
1157  RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[2][0] );
1158  os2 << ")";
1159  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1160  }
1161  // just flips them
1162  if(pf[1] < pf[2]){
1163  os1 << "(rewrite_iff_symm ";
1166  os2 << ")";
1167  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1168  }
1169  if( !tRetVal ){
1170  os1 << "(iff_refl ";
1171  os2 << ")";
1172  RefPtr< LFSCProof > p = LFSCProofExpr::Make( pf[1].iffExpr(pf[2]) );
1173  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed,
1174  nullRat, false, 0 );
1175  }
1176  }
1177  else if( isIgnoredRule( pf[0] ) )
1178  {
1179  TReturn* t = cvc3_to_lfsc(pf[2],beneath_lc);
1180  yMode = t->getProvesY();
1181  t->getL( emptyL, emptyLUsed );
1182  if( !cvc3_mimic )
1183  {
1184  if( yMode==1 ){
1185  tRetVal = t;
1186  }
1187  }
1188  else
1189  {
1190  if( yMode==0 || yMode==2 )
1191  {
1192  ostringstream os1, os2;
1193  os1 << "(" << pf[0] << (yMode==2 ? "_impl" : "" ) << " _ ";
1194  os2 << ")";
1195  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t->getLFSCProof(), os2.str() ), emptyL, emptyLUsed,
1196  t->getRational(), t->hasRational(), 0 );
1197  }
1198  }
1199  }
1200  else if( isTrivialTheoryAxiom( pf ) )
1201  {
1202  //find the rational multiplier for the axiom
1203  Rational r;
1204  bool hasRat = false;
1205  if( pf[0]==d_mult_ineqn_str || pf[0]==d_mult_eqn_str || pf[0]==d_rewrite_eq_symm_str || pf[0]==d_int_const_eq_str ){
1206  if( pf[0]==d_mult_ineqn_str && pf[2].arity()==2 && pf[2][1].arity()==2 ){
1207  if( pf[2][1][1].isRational() ){
1208  r = pf[2][1][1].getRational();
1209  hasRat = true;
1210  }else if( pf[2][1][0].isRational() ){
1211  r = pf[2][1][0].getRational();
1212  hasRat = true;
1213  }
1214  }else if( pf[0]==d_mult_eqn_str && pf[3].isRational() ){
1215  r = pf[3].getRational();
1216  hasRat = true;
1217  }else if( pf[0]==d_rewrite_eq_symm_str ){
1218  r = -1;
1219  hasRat = true;
1220  }else if( pf[0]==d_int_const_eq_str ){
1221  if( pf[1].getKind()==EQ && !pf[2].isFalse() ){
1222  if( pf[1][1].getKind()==MULT && getRat( pf[1][1][0], r ) ){
1223  r = -r;
1224  }else if( pf[1][1].getKind()==PLUS && pf[1][1][1].getKind()==MULT && getRat( pf[1][1][1][0], r ) ){
1225  r = -r;
1226  }else{
1227  r = -1;
1228  }
1229  hasRat = true;
1230  }
1231  }
1232  if( !hasRat )
1233  {
1234  ose << pf[0] << ", Warning: Can't find rational multiplier " << std::endl;
1235  ose << pf[2] << std::endl;
1236  }
1237  }
1238  //handle the axiom - only do it if the term is polynomial normalizable
1239  if( !cvc3_mimic && isTrivialTheoryAxiom( pf, true ) )
1240  {
1241  //ignore it if cvc3_mimic is false
1242  if( hasRat && r<0 && pf[0]==d_mult_ineqn_str ){
1243  r = -r;
1244  }
1245  //if( debug_conv && !beneath_lc ){
1246  // cout << "WARNING: Trivial theory axiom used, not underneath learned clause: " << pf[0] << std::endl;
1247  //}
1248  tRetVal = new TReturn( LFSCLraAxiom::MakeEq(), emptyL, emptyLUsed, r, hasRat, 1 );
1249  }else{
1250  //int val = queryM( pf[1] );
1251  if( pf[0] == d_refl_str )
1252  {
1253  if( isFormula( pf[1] ) ){
1254  ostringstream os1, os2;
1255  os1 << "(iff_refl ";
1256  os2 << ")";
1258  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed,
1259  nullRat, false, 0 );
1260  }else{
1261  ostringstream os1, os2;
1262  os1 << "(refl Real ";
1263  os2 << ")";
1265  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed,
1266  nullRat, false, 0 );
1267  }
1268  }
1269  else if( pf[0] == d_flip_inequality_str )
1270  {
1271  ostringstream os1, os2;
1272  os1 << "(flip_inequality_" << kind_to_str( pf[1].getKind() );
1273  os1 << "_" << kind_to_str( pf[2].getKind() ) << " ";
1274  os2 << ")";
1275  RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1][0] );
1276  RefPtr< LFSCProof > p2 = LFSCProofExpr::Make( pf[1][1] );
1277  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1278  nullRat, false, 0 );
1279  }
1280  else if( pf[0] == d_right_minus_left_str )
1281  {
1282  ostringstream os1, os2;
1283  os1 << "(right_minus_left_" << kind_to_str( pf[1].getKind() ) << " ";
1284  os2 << ")";
1285  RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1][0] );
1286  RefPtr< LFSCProof > p2 = LFSCProofExpr::Make( pf[1][1] );
1287  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1288  nullRat, false, 0 );
1289  }
1290  else if( pf[0] == d_minus_to_plus_str )
1291  {
1292  ostringstream os1, os2;
1293  os1 << "(minus_to_plus ";
1294  os2 << ")";
1297  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1298  nullRat, false, 0 );
1299  }
1300  else if( pf[0] == d_plus_predicate_str )
1301  {
1302  ostringstream os1, os2;
1303  os1 << "(plus_predicate_" << kind_to_str( pf[1].getKind() ) << " ";
1304  std::vector< string > strs;
1305  std::vector< RefPtr< LFSCProof > > pfs;
1306  pfs.push_back( LFSCProofExpr::Make( pf[1][0] ) );
1307  pfs.push_back( LFSCProofExpr::Make( pf[1][1] ) );
1308  pfs.push_back( LFSCProofExpr::Make( pf[2][0][1] ) );
1309  os2 << ")";
1310  std::string spc( " " );
1311  strs.push_back( os1.str() );
1312  strs.push_back( spc );
1313  strs.push_back( spc );
1314  strs.push_back( os2.str() );
1315  tRetVal = new TReturn( LFSCProofGeneric::Make( pfs, strs ), emptyL, emptyLUsed,
1316  nullRat, false, 0 );
1317  }
1318  else if( pf[0] == d_canon_plus_str || pf[0]==d_canon_mult_str )
1319  {
1320  int m = queryMt( Expr( MINUS, pf[1], pf[2] ) );
1321  ostringstream os;
1322  os << "(canonize_= _ _ _ ";
1323  os << "@pnt" << m << ")";
1324  pntNeeded[ m ] = true;
1325  tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os.str().c_str() ), emptyL, emptyLUsed,
1326  nullRat, false, 0 );
1327  }
1328  else if( pf[0] == d_canon_invert_divide_str )
1329  {
1330  Rational r1 = Rational( 1 );
1331  Expr er1 = d_pf_expr.getEM()->newRatExpr( pf[1][0].getRational() );
1332  Expr er2 = d_pf_expr.getEM()->newRatExpr( r1/pf[1][1].getRational() );
1333  //cout << "we have made " << er1 << " " << er2 << std::endl;
1334  int m = queryMt( Expr( MINUS, pf[1], Expr( MULT, er1, er2 )) );
1335  ostringstream os;
1336  os << "(canonize_= _ _ _ ";
1337  os << "@pnt" << m << ")";
1338  pntNeeded[ m ] = true;
1339  tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os.str().c_str() ), emptyL, emptyLUsed,
1340  nullRat, false, 0 );
1341  }
1342  else if( pf[0] == d_mult_ineqn_str && hasRat )
1343  {
1344  ostringstream os1, os2;
1345  os1 << "(mult_ineqn_" << (r<0 ? "neg_" : "");
1346  os1 << kind_to_str( pf[1].getKind() ) << " ";
1347  RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1][0] );
1348  RefPtr< LFSCProof > p2 = LFSCProofExpr::Make( pf[1][1] );
1349  os2 << " ";
1350  print_rational( r, os2 );
1351  os2 << ")";
1352  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1353  nullRat, false, 0 );
1354  }
1355  else if( pf[0] == d_mult_eqn_str && hasRat )
1356  {
1357  ostringstream os1, os2;
1358  os1 << "(mult_eqn ";
1361  os2 << " ";
1362  print_rational( r, os2 );
1363  os2 << ")";
1364  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1365  nullRat, false, 0 );
1366  }
1367  else if( pf[0] == d_negated_inequality_str )
1368  {
1369  Expr e1 = queryAtomic( pf[1], true );
1370 
1371  ostringstream os1, os2;
1372  os1 << "(negated_inequality_" << kind_to_str( e1.getKind() );
1373  os1 << "_" << kind_to_str( get_not( e1.getKind() ) ) << " ";
1374  RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1][0][0] );
1375  RefPtr< LFSCProof > p2 = LFSCProofExpr::Make( pf[1][0][1] );
1376  os2 << ")";
1377  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1378  nullRat, false, 0 );
1379  }
1380  else if( pf[0] == d_rewrite_eq_symm_str )
1381  {
1382  ostringstream os1, os2;
1383  os1 << "(rewrite_eq_symm ";
1386  os2 << ")";
1387  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1388  nullRat, false, 0 );
1389  }
1390  else if( pf[0] == d_rewrite_eq_refl_str )
1391  {
1392  ostringstream os1, os2;
1393  os1 << "(rewrite_eq_refl ";
1394  os2 << ")";
1395  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), LFSCProofExpr::Make( pf[2] ), os2.str() ),
1396  emptyL, emptyLUsed, nullRat, false, 0 );
1397  }
1398  else if( pf[0] == d_uminus_to_mult_str )
1399  {
1400  if( pf[1].isRational() )
1401  {
1402  ostringstream os;
1403  os << "(uminus_to_mult ";
1404  print_rational( pf[1].getRational(), os );
1405  os << ")";
1406  tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os.str().c_str() ), emptyL, emptyLUsed,
1407  nullRat, false, 0 );
1408  }
1409  }
1410  else if( pf[0] == d_rewrite_not_true_str )
1411  {
1412  tRetVal = new TReturn( LFSCProofGeneric::MakeStr( "rewrite_not_true" ), emptyL, emptyLUsed, nullRat, false, 0 );
1413  }
1414  else if( pf[0] == d_rewrite_not_false_str )
1415  {
1416  tRetVal = new TReturn( LFSCProofGeneric::MakeStr( "rewrite_not_false" ), emptyL, emptyLUsed, nullRat, false, 0 );
1417  }
1418  else if( pf[0] == d_int_const_eq_str )
1419  {
1420  int m1 = queryMt( Expr( MINUS, pf[1][0], pf[1][1] ) );
1421  int m2 = queryMt( Expr( MINUS, pf[2][0], pf[2][1] ) );
1422  ostringstream os;
1423  os << "(canonize_iff _ _ _ _ _ _ @pnt" << m1 << " @pnt" << m2 << ")";
1424  pntNeeded[ m1 ] = true;
1425  pntNeeded[ m2 ] = true;
1426  tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os.str().c_str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1427  }
1428  }
1429  }
1430  else if( pf[0]==d_lessThan_To_LE_rhs_rwr_str )
1431  {
1432  //FIXME: this introduces weirdness into the logic of completeness of the proof conversion
1433  //why is integer reasoning used in CVC3 QF_LRA proofs?
1434  if( !cvc3_mimic )
1435  tRetVal = new TReturn( LFSCLraAxiom::MakeEq(), emptyL, emptyLUsed, nullRat, false, 1 );
1436  else{
1437  tRetVal = make_trusted( pf );
1438  }
1439  }
1440  else if( pf[0]==d_rewrite_not_not_str )
1441  {
1442  //note that "not not" is already taken care of FIXME
1443 #ifdef LRA2_PRIME
1444  tRetVal = new TReturn( LFSCProofGeneric::MakeStr("(rewrite_not_not _)"), emptyL, emptyLUsed, nullRat, false, 0 );
1445 #else
1446  if( !cvc3_mimic ){
1447  tRetVal = new TReturn( LFSCProofGeneric::MakeStr("(iff_refl _)"), emptyL, emptyLUsed, nullRat, false, 0 );
1448  }else{
1449  tRetVal = new TReturn( LFSCProofGeneric::MakeStr("(rewrite_not_not _)"), emptyL, emptyLUsed, nullRat, false, 0 );
1450  }
1451 #endif
1452  }
1453  else if( isTrivialBooleanAxiom( pf[0] ) )
1454  {
1455  if( !cvc3_mimic ){
1456  tRetVal = new TReturn( LFSCLem::Make( queryM( pf[1] ) ), emptyL, emptyLUsed, nullRat, false, 3 );
1457  }else{
1458 
1459  }
1460  }
1461  else if( pf[0]==d_const_predicate_str )
1462  {
1463  if( is_eq_kind( pf[1].getKind() ) )
1464  {
1465  Rational r1, r2;
1466  //int knd = pf[2].isFalse() ? get_not( pf[1].getKind() ) : pf[1].getKind();
1468  if( getRat( pf[1][0], r1 ) && getRat( pf[1][1], r2 ) ){
1469 #ifdef PRINT_MAJOR_METHODS
1470  cout << ";[M]: const_pred " << kind_to_str( pf[1].getKind() );
1471  cout << " " << pf[2].isFalse();
1472  cout << ", rp=" << rev_pol << ", cvc=" << cvc3_mimic << std::endl;
1473 #endif
1474  if( !cvc3_mimic ){
1475  //if( rev_pol ){
1476  // ostringstream ose1;
1477  // ose1 << "Warning: Const predicate, rev pol true" << std::endl;
1478  // print_warning( ose1.str().c_str() );
1479  // knd = get_not( knd );
1480  //}
1481  if( pf[1].getKind()==EQ ){
1482  p = LFSCLraAxiom::MakeEq();
1483  }else{
1484  //Rational r = is_opposite( knd ) ? r2 - r1 : r1 - r2;
1485  //if( knd==GT )
1486  // r = Rational( 1, 1000000 );
1487  //if( knd==GE
1488  // r = Rational( 0 );
1489  //p = LFSCLraAxiom::Make( r, get_normalized( knd ) );
1490  p = LFSCLraAxiom::MakeEq();
1491  }
1492  if( p.get() ){
1493  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
1494  }
1495  }
1496  else
1497  {
1498  ostringstream os;
1499  os << "(const_predicate_" << kind_to_str( pf[1].getKind() );
1500  if( pf[2].getKind()==TRUE_EXPR )
1501  os << "_t";
1502  os << " ";
1503  print_rational( r1, os );
1504  os << " ";
1505  print_rational( r2, os );
1506  os << ")";
1507  tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os.str().c_str() ),
1508  emptyL, emptyLUsed, nullRat, false, 0 );
1509  }
1510  }else{
1511  ose << "ERROR: Could not find rational for const predicate" << std::endl;
1512  }
1513  }
1514  if( !tRetVal )
1515  ose << "kind = " << kind_to_str( pf[1].getKind() );
1516  }
1517  }
1518  else
1519  {
1520  //use Expr pfMod
1521  //switch( pfPat )
1522  //{
1523  //}
1524  if( pfPat==1 )
1525  {
1526  ostringstream os1, os2, os3;
1527  os1 << "(ite_axiom ";
1528  os2 << " ";
1529  os3 << ")";
1530  std::vector< string > strs;
1531  std::vector< RefPtr< LFSCProof > > pfs;
1532 
1533  strs.push_back( os1.str() );
1534  pfs.push_back( LFSCProofExpr::Make( pf[1][0] ) );
1535  strs.push_back( os2.str() );
1536  pfs.push_back( LFSCProofExpr::Make( pf[1][1][1] ) );
1537  strs.push_back( os2.str() );
1538  pfs.push_back( LFSCProofExpr::Make( pf[1][2][1] ) );
1539  strs.push_back( os3.str() );
1541 
1542  tRetVal = new TReturn( LFSCClausify::Make( pf[1], p.get() ), emptyL, emptyLUsed,
1543  nullRat, false, 3 );
1544  }else{
1545  ostringstream ose;
1546  ose << "WARNING: Unknown proof pattern [" << pfPat << "]";
1547  print_error( ose.str().c_str(), cout );
1548  //ostringstream os1;
1549  //os1 << "PROOF_PAT_" << pfPat;
1550  //tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os1.str().c_str() ), emptyL, emptyLUsed, nullRat, false, 3 );
1551  }
1552  }
1553  if( !tRetVal ){
1554  static bool firstTime = true;
1555  if(pf.arity()>0 && (yMode!=-1 || firstTime ) ){
1556  firstTime = false;
1557  ose << "Unknown proof rule (" << d_rules[pf[0]] << ") " << pf[0] << endl;
1558  ose << "YMode : ";
1559  if( yMode==-2 )
1560  ose << "unknown";
1561  else if( yMode==-1 )
1562  ose << "fail";
1563  else
1564  ose << yMode;
1565  ose << std::endl;
1566  if( rev_pol )
1567  ose << "rev_pol = true" << std::endl;
1568  if( pfPat!=0 )
1569  {
1570  ose << "proof pattern = " << pfPat << std::endl;
1571  }
1572  print_error( ose.str().c_str(), cout );
1573  }
1574  tRetVal = new TReturn( LFSCProofGeneric::MakeUnk(), emptyL, emptyLUsed, nullRat, false, -1 );
1575  }
1576 
1577 
1578  if( debug_conv ){
1579  //cout << "print length = " << tRetVal->getLFSCProof()->get_string_length() << std::endl;
1580  cout << "...done " << pf[0] << " " << tRetVal->getProvesY() << std::endl;
1581  }
1582  if( debug_var ){
1583  ostringstream os1, os2;
1584  os1 << "[" << pf[0];
1586  os1 << "_" << kind_to_str( pf[1].getKind() );
1587  if( pf[0]==d_const_predicate_str )
1588  os1 << "_" << pf[2];
1589  os1 << " ";
1590  os2 << "]";
1591  std::vector< int > lv, lvUsed;
1592  tRetVal->getL( lv, lvUsed );
1593  tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), tRetVal->getLFSCProof(), os2.str(), true ),
1594  lv, lvUsed, tRetVal->getRational(), tRetVal->hasRational(), tRetVal->getProvesY() );
1595  }
1596  //dont bother making small proofs into lambdas (length less than 30), or they are trivial
1597  if( !tRetVal->getLFSCProof()->isTrivial() && tRetVal->getLFSCProof()->get_string_length()>30 )
1598  {
1599  d_th_trans[pf] = true;
1600  //if( !d_th_trans_map[cvcm][pf] && pf.isSelected() ){
1601  // std::cout << "already selected" << std::endl;
1602  //}
1603  d_th_trans_map[cvcm][pf] = tRetVal;
1604  //pf.setSelected();
1605  }
1606  //else if( tRetVal->getLFSCProof()->get_string_length()<=30 && getNumNodes( pf )>10 ){
1607  // std::cout << "strange proof " << pf[0] << " " << getNumNodes( pf ) << std::endl;
1608  // tRetVal->getLFSCProof()->print( cout );
1609  // cout << endl;
1610  //}
1611  //if( cvc3_mimic && ( tRetVal->getProvesY()==1 || tRetVal->getProvesY()==2 ) ){
1612  // ostringstream ose;
1613  // ose << "Warning: After " << pf[0] << ", cvc_mimic, Ymode = " << tRetVal->getProvesY() << std::endl;
1614  // print_warning( ose.str().c_str() );
1615  //}
1616  //if( tRetVal->getProvesY()==1 ){
1617  // if( tRetVal->getLFSCProof()->checkOp()==-1 ){
1618  // ostringstream ose;
1619  // ose << "Error: After " << pf[0] << ", check op failed. " << tRetVal->getLFSCProof()->getNumChildren() << std::endl;
1620  // ose << pf << std::endl;
1621  // tRetVal->getLFSCProof()->print_pf( ose );
1622  // print_warning( ose.str().c_str() );
1623  // }
1624  //}
1625  //if( tRetVal->getProvesY()==1 ){
1626  // Expr pe;
1627  // Expr yexpr;
1628  // if( !what_is_proven( pf, pe ) || !getY( pe, yexpr ) ){
1629  // ostringstream ose;
1630  // ose << "Warning: Bad yMode 1 formula after " << pf[0] << std::endl;
1631  // if( pe.isInitialized() )
1632  // ose << pe << std::endl;
1633  // ose << pf << std::endl;
1634  // print_error( ose.str().c_str(), cout );
1635  // }
1636  //}
1637  return tRetVal;
1638 }
1639 
1640 //look at the pattern of the proof, return relevant information in modE
1642 {
1643  if( pf[0]==d_cnf_add_unit_str )
1644  {
1645  if( pf[2][0]==d_iff_mp_str )
1646  {
1647  if( pf[2][3][0]==d_eq_symm_str && pf[2][4][0]==d_if_lift_rule_str )
1648  {
1649  if( pf[2][3][4][0]==d_iff_mp_str )
1650  {
1651  if( pf[2][3][4][3][0]==d_var_intro_str &&
1652  pf[2][3][4][4][0]==d_assump_str )
1653  {
1654  return 1;
1655  }
1656  }
1657  }
1658  }
1659  }
1660  return 0;
1661 }
1662 
1664 {
1665  if( debug_conv )
1666  cout << "make let proof..." << std::endl;
1667  //std::map< TReturn*, bool >::iterator t_lbend = d_th_trans_lam.begin(), t_lb = d_th_trans_lam.end();
1668  //--t_lb;
1669  if( !d_th_trans.empty() ){
1670  //ExprMap< TReturn* >::iterator t_lb = d_th_trans.begin(), t_lbend = d_th_trans.end();
1672  --t_lb;
1673  while(t_lb != t_lbend){
1674  for( int cvcm=0; cvcm<2; cvcm++ ){
1675  if( d_th_trans_map[cvcm].find( (*t_lb).first )!= d_th_trans_map[cvcm].end() )
1676  {
1677  TReturn* t = d_th_trans_map[cvcm][(*t_lb).first];
1678  if( t ){
1679  std::vector< int > lv;
1680  std::vector< int > lvUsed;
1681 #ifdef OPTIMIZE
1682  t->calcL( lv, lvUsed );
1683 #else
1684  t->getL( lv, lvUsed );
1685 #endif
1686  if( d_th_trans_lam[cvcm][t] ){
1687  d_th_trans_lam[cvcm][t] = false;
1688  int lmt1 = LFSCProof::make_lambda( t->getLFSCProof() );
1689  RefPtr< LFSCProof > pfV = LFSCPfVar::Make( "@l", lmt1 );
1690  p = LFSCPfLet::Make( t->getLFSCProof(), (LFSCPfVar*)pfV.get(), p,
1691  t->getProvesY()!=3, lvUsed );
1692  }
1693  }
1694  }
1695  }
1696  --t_lb;
1697  //t_lb++;
1698  }
1699  }
1700  if( debug_conv )
1701  cout << "...done " << std::endl;
1702  return p;
1703 }
1704 
1706 {
1707  Expr e;
1708  std::vector< int > emptyL;
1709  std::vector< int > emptyLUsed;
1710  if( what_is_proven( pf, e ) ){
1711  int valT = queryM( e, true, true );
1712  return new TReturn( LFSCPfVar::Make( "@T", valT ), emptyL, emptyLUsed, nullRat, false, 0 );
1713  }else{
1714  return new TReturn( LFSCProofGeneric::MakeStr( "@T-unk" ), emptyL, emptyLUsed, nullRat, false, 0 );
1715  }
1716 }
1717 
1718 TReturn* LFSCConvert::do_bso( const Expr& pf, bool beneath_lc, bool rev_pol,
1719  TReturn* t1, TReturn* t2, ostringstream& ose )
1720 {
1721  std::vector< int > emptyL;
1722  std::vector< int > emptyLUsed;
1723  int yMode = -2;
1724  TReturn* tRetVal = NULL;
1725  // merge literals
1726  t1->getL( emptyL, emptyLUsed );
1727  t2->getL( emptyL, emptyLUsed );
1728  bool isErr = false;
1729  if( pf[1].getKind()==PLUS || pf[1].getKind()==MINUS ||
1730  pf[1].getKind()==MULT || is_eq_kind( pf[1].getKind() ) )
1731  {
1732  yMode = TReturn::normalize_tret( pf[3], t1, pf[4], t2, rev_pol );
1733  if( yMode==1 )
1734  {
1735  if( pf[1].getKind()==PLUS )
1736  tRetVal = new TReturn( LFSCLraAdd::Make( t1->getLFSCProof(), t2->getLFSCProof(), EQ, EQ ),
1737  emptyL, emptyLUsed, nullRat, false, 1 );
1738  else if( pf[1].getKind()==MINUS )
1739  tRetVal = new TReturn( LFSCLraSub::Make( t1->getLFSCProof(), t2->getLFSCProof(), EQ, EQ ),
1740  emptyL, emptyLUsed, nullRat, false, 1 );
1741  else if( pf[1].getKind()==MULT ){
1742 #ifdef PRINT_MAJOR_METHODS
1743  cout << ";[M]: basic_subst_op1_* " << std::endl;
1744 #endif
1745  Rational r;
1746  if( getRat( pf[1][0], r ) ){
1747  tRetVal = new TReturn( LFSCLraMulC::Make( t2->getLFSCProof(), r, EQ ),
1748  emptyL, emptyLUsed, nullRat, false, 1 );
1749  }else if( getRat( pf[1][1], r ) ){
1750  tRetVal = new TReturn( LFSCLraMulC::Make( t1->getLFSCProof(), r, EQ ),
1751  emptyL, emptyLUsed, nullRat, false, 1 );
1752  }else{
1753  print_error( "Could not find rational mult in basic_subst_op1", cout );
1754  isErr = true;
1755  }
1756  }else if( is_eq_kind( pf[1].getKind() ) ){
1758  if( is_opposite( pf[1].getKind() ) ){
1759  p = LFSCLraSub::Make( t2->getLFSCProof(), t1->getLFSCProof(), EQ, EQ );
1760  }else{
1761  p = LFSCLraSub::Make( t1->getLFSCProof(), t2->getLFSCProof(), EQ, EQ );
1762  }
1763  tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
1764  }
1765  if( !tRetVal && debug_conv ){
1766  cout << "basic_subst_op1: abort, have to normalize to 2, for " << kind_to_str( pf[1].getKind() ) << std::endl;
1767  }
1768  }
1769  }
1770  if( !tRetVal ){
1771  if( !isErr ){
1772  if( t1->getProvesY()==1 ){
1773  TReturn::normalize_tr( pf[3], t1, 2, rev_pol );
1774  }
1775  if( t2->getProvesY()==1 ){
1776  TReturn::normalize_tr( pf[4], t2, 2, rev_pol );
1777  }
1778  }
1779  yMode = TReturn::normalize_tret( pf[3], t1, pf[4], t2, rev_pol );
1780  if( yMode==0 || yMode==2 )
1781  {
1782  if( pf[1].getKind()==OR || pf[1].getKind()==AND ||
1783  pf[1].getKind()==IFF || pf[1].getKind()==PLUS ||
1784  is_eq_kind( pf[1].getKind() ) || pf[1].getKind()==MULT || pf[1].getKind()==MINUS ){
1785 
1786  ostringstream os1, os2, os3;
1787  os1 << "(basic_subst_op1_";
1788  if( yMode==2 )
1789  os1 << "impl_";
1790  os1 << kind_to_str( pf[1].getKind() ) << " ";
1791  os3 << " ";
1792  os2 << ")";
1793  std::vector< string > strs;
1794  std::vector< RefPtr< LFSCProof > > pfs;
1795  strs.push_back( os1.str() );
1796  pfs.push_back( LFSCProofExpr::Make( cascade_expr( pf[1][0] ), true ) );
1797  strs.push_back( os3.str() );
1798  pfs.push_back( LFSCProofExpr::Make( cascade_expr( pf[2][0] ), true ) );
1799  strs.push_back( os3.str() );
1800  pfs.push_back( LFSCProofExpr::Make( cascade_expr( pf[1][1] ), true ) );
1801  strs.push_back( os3.str() );
1802  pfs.push_back( LFSCProofExpr::Make( cascade_expr( pf[2][1] ), true ) );
1803  strs.push_back( os3.str() );
1804  pfs.push_back( t1->getLFSCProof() );
1805  strs.push_back( os3.str() );
1806  pfs.push_back( t2->getLFSCProof() );
1807  strs.push_back( os2.str() );
1808  tRetVal = new TReturn( LFSCProofGeneric::Make( pfs, strs ), emptyL, emptyLUsed, nullRat, false, yMode );
1809  }
1810  }
1811  }
1812  if( !tRetVal ){
1813  ose << pf[0] << endl;
1814  for( int a=0; a<pf.arity(); a++ ){
1815  if( a>=3 ){
1816  ose << a << ": " << pf[a][0] << std::endl;
1817  Expr pre;
1818  what_is_proven( pf[a], pre );
1819  ose << "wip: " << pre << std::endl;
1820  }else{
1821  ose << a << ": " << pf[a] << std::endl;
1822  }
1823  }
1824  ose << "subst kind = " << kind_to_str( pf[1].getKind() ) << std::endl;
1825  ose << "subst arity = " << pf.arity() << std::endl;
1826  }
1827  return tRetVal;
1828 }