CVC3  2.4.1
LFSCObject.cpp
Go to the documentation of this file.
1 #include "LFSCObject.h"
2 
4 int LFSCObj::formula_i = 1;
5 int LFSCObj::term_i = 1;
6 int LFSCObj::trusted_i = 1;
7 int LFSCObj::tnorm_i = 1;
25 std::map< int, bool > LFSCObj::pntNeeded;
29 //differentiate between variables and rules
31 //boolean resultion rules
102 
103 
104 void LFSCObj::initialize( const Expr& pf_expr, int lfscm )
105 {
106  lfsc_mode = lfscm;
107  cvc3_mimic = lfsc_mode==2 || lfsc_mode==7 || (lfsc_mode>=20 && lfsc_mode <= 29 );
109  debug_conv = lfsc_mode%10 == 0;
110  debug_var = lfsc_mode>10 && ( lfsc_mode%10 == 1 );
111 
112  d_pf_expr = pf_expr;
113  // initialize rules
114  d_bool_res_str = pf_expr.getEM()->newVarExpr("bool_resolution");
115  d_assump_str = pf_expr.getEM()->newVarExpr("assumptions");
116  d_iff_mp_str = pf_expr.getEM()->newVarExpr("iff_mp");
117  d_impl_mp_str = pf_expr.getEM()->newVarExpr("impl_mp");
118  d_iff_trans_str = pf_expr.getEM()->newVarExpr("iff_trans");
119  d_real_shadow_str = pf_expr.getEM()->newVarExpr("real_shadow");
120  d_cycle_conflict_str = pf_expr.getEM()->newVarExpr("cycleConflict");
121  d_real_shadow_eq_str = pf_expr.getEM()->newVarExpr("real_shadow_eq");
122  d_basic_subst_op_str = pf_expr.getEM()->newVarExpr("basic_subst_op");
123  d_mult_ineqn_str = pf_expr.getEM()->newVarExpr("mult_ineqn");
124  d_flip_inequality_str = pf_expr.getEM()->newVarExpr("flip_inequality");
125  d_right_minus_left_str = pf_expr.getEM()->newVarExpr("right_minus_left");
126  d_eq_trans_str = pf_expr.getEM()->newVarExpr("eq_trans");
127  d_eq_symm_str = pf_expr.getEM()->newVarExpr("eq_symm");
128  d_canon_plus_str = pf_expr.getEM()->newVarExpr("canon_plus");
129  d_refl_str = pf_expr.getEM()->newVarExpr("refl");
130  d_cnf_convert_str = pf_expr.getEM()->newVarExpr("cnf_convert");
131  d_learned_clause_str = pf_expr.getEM()->newVarExpr("learned_clause");
132  d_minus_to_plus_str = pf_expr.getEM()->newVarExpr("minus_to_plus");
133  d_plus_predicate_str = pf_expr.getEM()->newVarExpr("plus_predicate");
134  d_flip_inequality_str = pf_expr.getEM()->newVarExpr("flip_inequality");
135  d_negated_inequality_str = pf_expr.getEM()->newVarExpr("negated_inequality");
136 
137  d_iff_true_elim_str = pf_expr.getEM()->newVarExpr("iff_true_elim");
138  d_basic_subst_op1_str= pf_expr.getEM()->newVarExpr("basic_subst_op1");
139  d_basic_subst_op0_str= pf_expr.getEM()->newVarExpr("basic_subst_op0");
140  d_canon_mult_str= pf_expr.getEM()->newVarExpr("canon_mult");
141  d_canon_invert_divide_str= pf_expr.getEM()->newVarExpr("canon_invert_divide");
142  d_iff_true_str= pf_expr.getEM()->newVarExpr("iff_true");
143  d_mult_eqn_str= pf_expr.getEM()->newVarExpr("mult_eqn");
144  d_rewrite_eq_symm_str= pf_expr.getEM()->newVarExpr("rewrite_eq_symm");
145  d_optimized_subst_op_str= pf_expr.getEM()->newVarExpr("optimized_subst_op");
146  d_implyWeakerInequality_str= pf_expr.getEM()->newVarExpr("implyWeakerInequality");
147  d_implyWeakerInequalityDiffLogic_str = pf_expr.getEM()->newVarExpr("implyWeakerInequalityDiffLogic");
148  d_imp_mp_str= pf_expr.getEM()->newVarExpr("impl_mp");
149  d_rewrite_implies_str = pf_expr.getEM()->newVarExpr("rewrite_implies");
150  d_rewrite_or_str = pf_expr.getEM()->newVarExpr("rewrite_or");
151  d_rewrite_and_str = pf_expr.getEM()->newVarExpr("rewrite_and");
152  d_rewrite_iff_symm_str = pf_expr.getEM()->newVarExpr("rewrite_iff_symm");
153  d_iff_not_false_str = pf_expr.getEM()->newVarExpr("iff_not_false");
154  d_iff_false_str = pf_expr.getEM()->newVarExpr("iff_false");
155  d_iff_false_elim_str = pf_expr.getEM()->newVarExpr("iff_false_elim");
156  d_not_to_iff_str = pf_expr.getEM()->newVarExpr("not_to_iff");
157  d_not_not_elim_str = pf_expr.getEM()->newVarExpr("not_not_elim");
158  d_const_predicate_str = pf_expr.getEM()->newVarExpr("const_predicate");
159  d_rewrite_not_not_str = pf_expr.getEM()->newVarExpr("rewrite_not_not");
160  d_rewrite_not_true_str = pf_expr.getEM()->newVarExpr("rewrite_not_true");
161  d_rewrite_not_false_str = pf_expr.getEM()->newVarExpr("rewrite_not_false");
162 
163  d_if_lift_rule_str = pf_expr.getEM()->newVarExpr("if_lift_rule");
164  d_CNFITE_str = pf_expr.getEM()->newVarExpr("CNFITE");
165  d_var_intro_str = pf_expr.getEM()->newVarExpr("var_intro");
166  d_int_const_eq_str = pf_expr.getEM()->newVarExpr("int_const_eq");
167  d_rewrite_eq_refl_str = pf_expr.getEM()->newVarExpr("rewrite_eq_refl");
168  d_iff_symm_str = pf_expr.getEM()->newVarExpr("iff_symm");
169  d_rewrite_iff_str = pf_expr.getEM()->newVarExpr("rewrite_iff");
170  d_implyNegatedInequality_str = pf_expr.getEM()->newVarExpr("implyNegatedInequality");
171  d_uminus_to_mult_str = pf_expr.getEM()->newVarExpr("uminus_to_mult");
172  d_lessThan_To_LE_rhs_rwr_str = pf_expr.getEM()->newVarExpr("lessThan_To_LE_rhs_rwr");
173 
174  d_CNF_str = pf_expr.getEM()->newVarExpr("CNF");
175  d_cnf_add_unit_str = pf_expr.getEM()->newVarExpr("cnf_add_unit");
176  d_minisat_proof_str = pf_expr.getEM()->newVarExpr("minisat_proof");
177  d_rewrite_ite_same_str = pf_expr.getEM()->newVarExpr("rewrite_ite_same");
178  d_andE_str = pf_expr.getEM()->newVarExpr("andE");
179  d_implyEqualities_str = pf_expr.getEM()->newVarExpr("implyEqualities");
180  d_addInequalities_str = pf_expr.getEM()->newVarExpr("addInequalities");
181 
182  //reasons for CNF
183  d_or_final_s = pf_expr.getEM()->newStringExpr("or_final");
184  d_and_final_s = pf_expr.getEM()->newStringExpr("and_final");
185  d_ite_s = pf_expr.getEM()->newStringExpr("ite");
186  d_iff_s = pf_expr.getEM()->newStringExpr("iff");
187  d_imp_s = pf_expr.getEM()->newStringExpr("imp");
188  d_or_mid_s = pf_expr.getEM()->newStringExpr("or_mid");
189  d_and_mid_s = pf_expr.getEM()->newStringExpr("and_mid");
190 
191  // add them to d_rules
192  d_rules[d_iff_mp_str]=true;
193  d_rules[d_impl_mp_str]=true;
194  d_rules[d_iff_trans_str]=true;
202  d_rules[d_eq_trans_str]=true;
203  d_rules[d_eq_symm_str]=true;
205  d_rules[d_refl_str]=true;
208  d_rules[d_bool_res_str] = true;
209  d_rules[d_assump_str] = true;
218  d_rules[d_canon_mult_str] = true;
220  d_rules[d_iff_true_str] = true;
221  d_rules[d_mult_eqn_str] = true;
226  d_rules[d_imp_mp_str] = true;
229  d_rules[d_rewrite_or_str] = true;
230  d_rules[d_rewrite_and_str] = true;
233  d_rules[d_iff_false_str] = true;
235  d_rules[d_not_to_iff_str] = true;
236  d_rules[d_not_not_elim_str] = true;
241 
242  d_rules[d_if_lift_rule_str] = true;
243  d_rules[d_CNFITE_str] = true;
244  d_rules[d_var_intro_str] = true;
245  d_rules[d_int_const_eq_str] = true;
247  d_rules[d_iff_symm_str] = true;
248  d_rules[d_rewrite_iff_str] = true;
252 
253  d_rules[d_CNF_str] = true;
254  d_rules[d_cnf_add_unit_str] = true;
256 
257  d_rules[d_andE_str] = true;
260 }
261 
262 
263 int LFSCObj::getNumNodes( const Expr& pf, bool recount ){
264  if( pf.arity()>0 && d_rules[pf[0]] ){
265  if( nnode_map.find( pf )==nnode_map.end() ){
266  int sum=0;
267  for( int a=1; a<pf.arity(); a++ ){
268  sum += getNumNodes( pf[a], recount );
269  }
270  nnode_map[pf] = sum + 1;
271  return sum + 1;
272  }else if( recount ){
273  return nnode_map[pf];
274  }else{
275  return 1;
276  }
277  }
278  return 0;
279 }
280 
282 {
283  if( cas_map.find( e ) != cas_map.end() ){
284  return cas_map[e];
285  }else{
286  Expr ce;
287  if( e.getKind()==SKOLEM_VAR ){
288  ce = skolem_vars[e];
289  }else if( e.getKind()==ITE ){
290  ce = Expr( ITE, cascade_expr( e[0] ),
291  cascade_expr( e[1] ),
292  cascade_expr( e[2] ) );
293  }else if( e.arity()==1 ){
294  ce = Expr( e.getKind(), cascade_expr( e[0] ) );
295  }else if( e.arity()>0 ){
296  ce = cascade_expr( e[e.arity()-1] );
297  for( int a=e.arity()-2; a>=0; a-- ){
298  ce = Expr( e.getKind(), cascade_expr( e[a] ), ce );
299  }
300  }else{
301  return e;
302  }
303  cas_map[e] = ce;
304  return ce;
305  }
306 }
307 
309 {
310  if( e.arity()>0 && d_rules[ e[0] ] && !temp_visited[e] )
311  {
312  temp_visited[e] = true;
313  if( e[0] == d_assump_str )
314  {
315  if( e[1].isIff() && e[1][1].isEq() && e[1][1][1].getKind()==SKOLEM_VAR ){
316  Expr ce = cascade_expr( e[1][1][0] );
317  skolem_vars[ e[1][1][1] ] = ce;
318  //store it in the tmap
319  queryT( ce );
320  }else{
321  Expr ce = cascade_expr( e[1] );
322  if( !d_assump_map[ ce ] ){
323  ostringstream ose;
324  ose << "Unexpected non-discharged assumption " << ce;
325  print_error( ose.str().c_str(), cout );
326  }
327  }
328  }
329  if( e[0]!=d_learned_clause_str ){
330  for( int a=1; a<e.arity(); a++ ){
331  define_skolem_vars( e[a] );
332  }
333  }
334  }
335 }
336 
337 bool LFSCObj::isVar( const Expr& e )
338 {
339  return (e.getKind()==UCONST && d_rules[e]==false);
340 }
341 
342 void LFSCObj::collect_vars(const Expr& e,bool readPred){
343  if(isVar(e)){
344  if( readPred )
345  input_preds[e] = true;
346  else
347  input_vars[e]=true;
348  }else{
349  readPred = !is_eq_kind( e.getKind() ) && readPred;
350  for(int a=0; a<e.arity(); a++ ){
351  collect_vars( e[a], ( readPred || (e.getKind()==ITE && a==0 ) ) );
352  }
353  }
354 }
355 
357 {
358  Expr e = expr;
359  while( e.isNot() && e[0].isNot() )
360  e = e[0][0];
361  return e;
362 }
363 
364 
365 Expr LFSCObj::queryAtomic(const Expr& expr, bool getBase)
366 {
367  Expr e = cascade_expr( queryElimNotNot( expr ) );
368  if( e.isNot() ){
369  if( getBase ){
370  return e[0];
371  }else{
372  if( e[0].isTrue() ){
373  e = d_pf_expr.getEM()->falseExpr();
374  return e;
375  }else if( e[0].isFalse() ){
376  e = d_pf_expr.getEM()->trueExpr();
377  return e;
378  }else if( is_eq_kind( e[0].getKind() ) ){
379  return Expr( get_not( e[0].getKind() ), e[0][1], e[0][0] );
380  }
381  }
382  }
383  return e;
384 }
385 
386 int LFSCObj::queryM(const Expr& expr, bool add, bool trusted)
387 {
388  //cout << "query : " << expr << endl;
389  bool neg = false;
390  Expr e = cascade_expr( queryElimNotNot( expr ) );
391  if( !trusted ){
392  if( e.isNot() ){
393  neg = true;
394  e = e[0];
395  }
396  int val = d_formulas[e];
397  if( val==0 && add )
398  {
399  if( !e.isInitialized() ){
400  print_error( "WARNING: uninitialized e in query", cout );
401  }
402  d_formulas[e] = formula_i;
403  val = formula_i;
404  formula_i++;
405  }
406  return val*(neg ? -1 : 1 );
407  }else{
408  int val = d_trusted[e];
409  if( val==0 && add ){
410  d_trusted[e] = trusted_i;
411  val = trusted_i;
412  trusted_i++;
413  }
414  return val;
415  }
416 }
417 
418 int LFSCObj::queryMt(const Expr& expr)
419 {
420  Expr ce = cascade_expr( expr );
421  if( !can_pnorm( ce ) ){
422  ostringstream os;
423  os << "ERROR: cannot make polynomial normalization for " << ce << std::endl;
424  print_error( os.str().c_str(), cout );
425  }
426  int val = d_pn[ce];
427  if( val==0 )
428  {
429  d_pn[ce] = tnorm_i;
430  val = tnorm_i;
431  tnorm_i++;
432  }
433  return val;
434 }
435 
436 int LFSCObj::queryT( const Expr& e )
437 {
438  Expr ce = cascade_expr( e );
439  int val = d_terms[ce];
440  if( val==0 ){
441  d_terms[ce] = term_i;
442  val = term_i;
443  term_i++;
444  }
445  return val;
446 }
447 
448 bool LFSCObj::getY( const Expr& e, Expr& pe, bool doIff, bool doLogic )
449 {
450  //cout << "getY = " << e << std::endl;
451  Expr ea = queryAtomic( e );
452  if( is_eq_kind( ea.getKind() ) ){
453  //must be able to pnorm it
454  if( can_pnorm( ea[0] ) && can_pnorm( ea[1] ) ){
455  if( is_opposite( ea.getKind() ) ){
456  pe = Expr( get_normalized( ea.getKind() ), ea[1], ea[0] );
457  }else{
458  pe = ea;
459  }
460  return true;
461  }else{
462  ostringstream ose;
463  ose << "Can't pnorm " << ea[0] << " " << ea[1] << std::endl;
464  print_error( ose.str().c_str(), cout );
465  }
466  }
467  if( doIff ){
468  if( e.arity()==2 )
469  {
470  Expr pe1;
471  Expr pe2;
472  if ( e.isIff() ){
473  if( getY( e[1], pe2, false ) ){
474  if( getY( e[0], pe1, false, pe2.getKind()==TRUE_EXPR || pe2.getKind()==FALSE_EXPR ) ){
475  if( pe2.getKind()==TRUE_EXPR ){
476  pe = pe1;
477  return true;
478  }else if( pe1.getKind()==FALSE_EXPR ){
479  pe = d_pf_expr.getEM()->trueExpr();
480  return true;
481  }
482  if( pe1.getKind()==pe2.getKind() ){
483  pe = Expr( EQ, Expr( MINUS, pe1[0], pe2[0] ), Expr( MINUS, pe1[1], pe2[1] ) );
484  }
485  return true;
486  }
487  }
488  }
489  else if( e.isImpl() ){
490  if( getY( e[1], pe2, false, false ) ){
491  if( getY( e[0], pe1, false, false ) ){
492  if( is_comparison( pe1.getKind() ) && is_comparison( pe2.getKind() ) ){
493  pe = Expr( pe1.getKind()==GT && pe2.getKind()==GT ? GT : GE,
494  Expr( MINUS, pe1[0], pe2[0] ), Expr( MINUS, pe1[1], pe2[1] ) );
495  }
496  return true;
497  }
498  }
499  }
500  }
501  }
502  if( doLogic ){
503  if( ea.isFalse() ){
504  pe = d_pf_expr.getEM()->trueExpr();
505  return true;
506  }else if( ea.isTrue() ){
507  pe = ea;
508  return true;
509  }
510  }
511  return false;
512 }
513 
514 bool LFSCObj::isFormula( const Expr& e )
515 {
516  return ( is_eq_kind( e.getKind() ) || e.isAnd() || e.isOr() || e.isImpl() || e.isIff() || e.isFalse() || e.isTrue() || e.isNot() ||
517  ( e.getKind()==ITE && isFormula( e[1] ) ) || ( input_preds.find( e )!=input_preds.end() ) );
518 }
519 
520 bool LFSCObj::can_pnorm( const Expr& e )
521 {
522  if( is_eq_kind( e.getKind() ) ){
523  return can_pnorm( e[0] ) && can_pnorm( e[1] );
524  }else if( e.getKind()==PLUS || e.getKind()==MINUS || e.getKind()==MULT || e.getKind()==DIVIDE ){
525  return can_pnorm( e[0] ) && can_pnorm( e[1] );
526  }else if( e.getKind()==UMINUS ){
527  return can_pnorm( e[0] );
528  }else if( e.isRational() ){
529  return true;
530  }else if( e.getKind()==ITE ){
531  queryT( e );
532  return true;
533  }else if( e.isVar() && input_preds.find( e )==input_preds.end() ){
534  return true;
535  }
536  return false;
537 }
538 
539 bool LFSCObj::what_is_proven( const Expr& pf, Expr& pe )
540 {
541  if(pf.arity()>0 ){
542  if(d_rules[pf[0]]&&pf[0].getKind()==UCONST){
543  if( pf[0] == d_assump_str || pf[0] == d_cnf_add_unit_str ||
544  pf[0]== d_cnf_convert_str || pf[0] == d_iff_true_elim_str ){
545  pe = pf[1];
546  return true;
547  }
548  else if( pf[0] == d_canon_plus_str || pf[0]==d_canon_mult_str ){
549  pe = Expr( EQ, pf[1], pf[2] );
550  return true;
551  }
552  else if( pf[0] == d_canon_invert_divide_str )
553  {
554  Rational r1 = Rational( 1 );
555  Expr er1 = d_pf_expr.getEM()->newRatExpr( pf[1][0].getRational() );
556  Expr er2 = d_pf_expr.getEM()->newRatExpr( r1/pf[1][1].getRational() );
557  pe = Expr( EQ, pf[1], Expr( MULT, er1, er2 ) );
558  return true;
559  }
560  else if( pf[0] == d_iff_trans_str )
561  {
562  pe = Expr( IFF, pf[1], pf[3] );
563  return true;
564  }
565  else if( pf[0] == d_iff_mp_str || pf[0] == d_impl_mp_str)
566  {
567  pe = pf[2];
568  return true;
569  }
570  else if( pf[0] == d_eq_trans_str )
571  {
572  pe = Expr( EQ, pf[2], pf[4] );
573  return true;
574  }
575  else if( pf[0] == d_eq_symm_str )
576  {
577  pe = Expr( EQ, pf[3], pf[2] );
578  return true;
579  }
580  else if( pf[0] == d_basic_subst_op_str || pf[0] == d_rewrite_and_str ||
581  pf[0] == d_rewrite_or_str || pf[0] == d_lessThan_To_LE_rhs_rwr_str ||
582  pf[0] == d_mult_ineqn_str || pf[0] == d_plus_predicate_str ||
583  pf[0] == d_flip_inequality_str || pf[0] == d_int_const_eq_str ||
584  pf[0] == d_const_predicate_str )
585  {
586  pe = Expr( IFF, pf[1], pf[2] );
587  return true;
588  }
589  else if (pf[0] == d_iff_symm_str){
590  pe = pf[2].iffExpr(pf[1]);
591  return true;
592  }
593  else if( pf[0] == d_basic_subst_op0_str )
594  {
595  if( pf[1].getKind()==UMINUS ){
596  pe = Expr( EQ, pf[1], pf[2] );
597  return true;
598  }else if( pf[1].getKind()==NOT ){
599  pe = Expr( IFF, pf[1], pf[2] );
600  return true;
601  }
602  }
603  else if( pf[0] == d_mult_eqn_str )
604  {
605  pe = Expr( IFF, Expr( EQ, pf[1], pf[2] ),
606  Expr( EQ, Expr( MULT, pf[1], pf[3] ), Expr( MULT, pf[2], pf[3] ) ) );
607  return true;
608  }
609  else if( pf[0] == d_real_shadow_str )
610  {
611  pe = Expr( ( pf[1].getKind()==LE && pf[2].getKind()==LE ) ? LE : LT, pf[1][0], pf[2][1] );
612  return true;
613  }
614  else if(pf[0] == d_real_shadow_eq_str){
615  pe = Expr(EQ, pf[2][0], pf[2][1]);
616  return true;
617  }
618  else if( pf[0] == d_optimized_subst_op_str || pf[0] == d_basic_subst_op1_str )
619  {
620  if( pf[1].getKind()==AND || pf[1].getKind()==OR || pf[1].getKind()==IFF || is_eq_kind( pf[1].getKind() ) ||
621  ( pf[1].getKind()==ITE && isFormula( pf[1] ) ) ){
622  pe = Expr( IFF, pf[1], pf[2] );
623  return true;
624  }else if( pf[1].getKind()==ITE || pf[1].getKind()==PLUS || pf[1].getKind()==MINUS || pf[1].getKind()==MULT ){
625  pe = Expr( EQ, pf[1], pf[2] );
626  return true;
627  }
628  }
629  else if( pf[0] == d_andE_str )
630  {
631  pe = pf[2][ pf[1].getRational().getNumerator().getInt() ];
632  return true;
633  }
634  else if( pf[0] == d_rewrite_implies_str )
635  {
636  Expr e1 = Expr( IMPLIES, pf[1], pf[2] );
637  Expr e2 = Expr( NOT, pf[1] );
638  Expr e3 = Expr( OR, e2, pf[2] );
639  pe = Expr( IFF, e1, e3 );
640  return true;
641  }
642  else if( pf[0] == d_rewrite_eq_symm_str )
643  {
644  Expr e1 = Expr( EQ, pf[2], pf[3] );
645  Expr e2 = Expr( EQ, pf[3], pf[2] );
646  pe = Expr( IFF, e1, e2 );
647  return true;
648  }
649  else if( pf[0] == d_rewrite_iff_symm_str )
650  {
651  Expr e1 = Expr( IFF, pf[1], pf[2] );
652  Expr e2 = Expr( IFF, pf[2], pf[1] );
653  pe = Expr( IFF, e1, e2 );
654  return true;
655  }
656  else if( pf[0] == d_rewrite_ite_same_str )
657  {
658  pe = Expr( EQ, Expr( ITE, pf[2], pf[3], pf[3] ), pf[3] );
659  return true;
660  }
661  else if( pf[0] == d_rewrite_eq_refl_str )
662  {
663  pe = Expr( IFF, Expr( EQ, pf[2], pf[2] ), d_pf_expr.getEM()->trueExpr() );
664  return true;
665  }
666  else if( pf[0] == d_refl_str )
667  {
668  if( isFormula( pf[1] ) )
669  pe = Expr( IFF, pf[1], pf[1] );
670  else
671  pe = Expr( EQ, pf[1], pf[1] );
672  return true;
673  }
674  else if( pf[0] == d_rewrite_not_not_str )
675  {
676  Expr e1 = Expr( NOT, pf[1] );
677  pe = Expr( NOT, e1 );
678  return true;
679  }
680  else if( pf[0] == d_not_to_iff_str )
681  {
682  pe = Expr( IFF, Expr( NOT, pf[1] ), d_pf_expr.getEM()->falseExpr() );
683  return true;
684  }
685  else if( pf[0] == d_minus_to_plus_str )
686  {
687  Expr er1 = d_pf_expr.getEM()->newRatExpr( Rational( -1 ) );
688  pe = Expr( EQ, Expr( MINUS, pf[1], pf[2] ), Expr( PLUS, pf[1], Expr( MULT, er1, pf[2] ) ) );
689  return true;
690  }
691  else if( pf[0] == d_right_minus_left_str )
692  {
693  Expr er1 = d_pf_expr.getEM()->newRatExpr( Rational( 0 ) );
694  Expr e1 = Expr( pf[1].getKind(), er1, Expr( MINUS, pf[1][1], pf[1][0] ) );
695  pe = Expr(IFF, pf[1], e1);
696  return true;
697  }
698  else if( pf[0] == d_negated_inequality_str )
699  {
700  pe = Expr( IFF, pf[1], Expr( get_not( pf[1][0].getKind() ), pf[1][0][0], pf[1][0][1] ) );
701  return true;
702  }
703  else if( pf[0] == d_iff_false_elim_str )
704  {
705  pe = queryElimNotNot( Expr( NOT, pf[1] ) );
706  return true;
707  }
708  else if( pf[0] == d_iff_true_str )
709  {
710  pe = Expr( IFF, pf[1], d_pf_expr.getEM()->trueExpr() );
711  return true;
712  }
713  else if( pf[0] == d_iff_not_false_str )
714  {
715  pe = Expr( IFF, queryElimNotNot( Expr( NOT, pf[1] ) ), d_pf_expr.getEM()->falseExpr() );
716  return true;
717  }
718  else if( pf[0] == d_uminus_to_mult_str )
719  {
720  Expr er1 = d_pf_expr.getEM()->newRatExpr( Rational( -1 ) );
721  pe = Expr( EQ, Expr( UMINUS, pf[1] ), Expr( MULT, er1, pf[1] ) );
722  return true;
723  }
724  else if( pf[0] == d_rewrite_not_true_str )
725  {
726  pe = Expr( IFF, Expr( NOT, d_pf_expr.getEM()->trueExpr() ),
727  d_pf_expr.getEM()->falseExpr() );
728  return true;
729  }
730  else if( pf[0] == d_rewrite_not_false_str )
731  {
732  pe = Expr( IFF, Expr( NOT, d_pf_expr.getEM()->falseExpr() ),
733  d_pf_expr.getEM()->trueExpr() );
734  return true;
735  }
736  else if( pf[0] == d_cycle_conflict_str )
737  {
738  pe = d_pf_expr.getEM()->falseExpr();
739  return true;
740  }
741  else if(pf[0] == d_implyNegatedInequality_str)
742  {
743  pe = pf[1].impExpr(pf[3]);
744  return true;
745  }
746  else if(pf[0] == d_implyWeakerInequality_str){
747  pe = pf[1].impExpr(pf[2]);
748  return true;
749  }
750  else if( pf[0] == d_rewrite_iff_symm_str )
751  {
752  Expr e1 = Expr( IFF, pf[1], pf[2] );
753  Expr e2 = Expr( IFF, pf[2], pf[1] );
754  pe = Expr( IFF, e1, e2 );
755  return true;
756  }
757  else if( pf[0] == d_rewrite_iff_str){
758  Expr e = Expr( IFF, pf[1], pf[2]);
759  Expr e_true = d_pf_expr.getEM()->trueExpr();
760  Expr e_false = d_pf_expr.getEM()->falseExpr();
761 
762  if(pf[1] == pf[2]){
763  pe = e.iffExpr(d_pf_expr.getEM()->trueExpr());
764  return true;
765  }
766 
767  if(pf[1] == e_true){
768  pe = e.iffExpr(e_true);
769  return true;
770  }
771  if(pf[1] == e_false){
772  pe = e.iffExpr(e_false);
773  return true;
774  }
775 
776  if(pf[1].isNot() && pf[1][0] == pf[2]){
777  pe = e.iffExpr(pf[2].negate());
778  return true;
779  }
780 
781  if(pf[2] == e_true){
782  pe = e.iffExpr(e_true);
783  return true;
784  }
785 
786  if(pf[2] == e_false){
787  pe = e.iffExpr(e_false);
788  return true;
789  }
790 
791  if(pf[2].isNot() && pf[2][0] == pf[1]){
792  pe = e.iffExpr(pf[1].negate());
793  return true;
794  }
795 
796  if(pf[1] < pf[2]){
797  Expr e_sym = Expr(IFF, pf[2], pf[1]);
798  pe = e.iffExpr(e_sym);
799  return true;
800  }
801  pe = e.iffExpr(e);
802  return true;
803  }
804  else if(pf[0] == d_implyEqualities_str){
805  pe = Expr(AND, pf[1][0]);
806  return true;
807  }
808  }
809  }
810  ostringstream ose;
811  ose << "What_is_proven, unknown: (" << d_rules[pf[0]] << "): " << pf[0];
812  print_error( ose.str().c_str(), cout );
813  return false;
814 }