CVC Lite: refined_arith_theorem_producer.cpp Source File

00001 
00002 // This code is trusted
00003 #define _CVCL_TRUSTED_
00004 
00005 #include <iostream> 
00006 #include "refined_arith_theorem_producer.h"
00007 #include "arith_theorem_producer.h"
00008 #include "theory_arith.h"
00009 #include "vcl.h"
00010 #include "common_proof_rules.h"
00011 #include "theory_core.h"
00012 
00013 using namespace std; 
00014 using namespace CVCL;
00015 
00016 
00017 // ----------------------------------------------------------------------// 
00018 //  Constants                                                            // 
00019 // ----------------------------------------------------------------------// 
00020 
00021 
00022 Theorem RefinedArithTheoremProducer::canonPlus(const Expr& e){
00023   cout << "In Sean's canonPlus!!!" << endl;
00024   return ArithTheoremProducer::canonPlus(e);
00025 }
00026 
00027 // ----------------------------------------------------------------------// 
00028 //  Core Util                                                            // 
00029 // ----------------------------------------------------------------------// 
00030 
00031 // void printExpr(Expr& x){
00032 //   cout << x.toString() << endl;
00033 // }
00034 
00035 Expr RefinedArithTheoremProducer::neg(const Expr& x){
00036   return Expr(d_em,UMINUS,x);
00037 }
00038 
00039 Expr RefinedArithTheoremProducer::inv(const Expr& x){
00040   return Expr(d_em,DIVIDE,one,x);
00041 }
00042 
00043 Expr RefinedArithTheoremProducer::plus(const Expr& x,const Expr& y){
00044   return Expr(d_em,PLUS,x,y);
00045 }
00046 
00047 Expr RefinedArithTheoremProducer::frac(const Expr& x,const Expr& y){
00048   return Expr(d_em,DIVIDE,x,y);
00049 }
00050 
00051 
00052 Theorem RefinedArithTheoremProducer::trans(const Theorem& t1,const Theorem& t2){
00053   return core->transitivityRule(t1,t2);
00054 }
00055 
00056 Theorem RefinedArithTheoremProducer::trans(const Expr& e){
00057   return core->reflexivityRule(e);
00058 }
00059 
00060 Theorem RefinedArithTheoremProducer::symm(const Theorem& t){
00061   return core->symmetryRule(t);
00062 }
00063 
00064 Theorem RefinedArithTheoremProducer::subst(Op op,const Expr& x,const Theorem& t){
00065   vector<Theorem> thms;
00066   thms.push_back(core->reflexivityRule(x));
00067   thms.push_back(t);
00068   return core->substitutivityRule(op,thms);
00069 }
00070 
00071 Theorem RefinedArithTheoremProducer::subst(Op op,const Theorem& t,const Expr& x){
00072   vector<Theorem> thms;
00073   thms.push_back(t);
00074   thms.push_back(core->reflexivityRule(x));
00075   return core->substitutivityRule(op,thms);
00076 }
00077 
00078 Theorem RefinedArithTheoremProducer::subst(Op op,const Theorem& t1,const Theorem& t2){
00079   vector<Theorem> thms;
00080   thms.push_back(t1);
00081   thms.push_back(t2);
00082   return core->substitutivityRule(op,thms);
00083 }
00084 
00085 
00086 // ======================================================================// 
00087 //  Axioms of the Reals                                                  // 
00088 // ======================================================================// 
00089 
00090 
00091 // -----------------------------------------------------------------------// 
00092 // addAssoc                                                               // 
00093 //                                                                        // 
00094 // args    :                                                              // 
00095 //         : x                                                            // 
00096 //         : y                                                            // 
00097 //         : z                                                            // 
00098 //                                                                        // 
00099 // returns : |- (x + y) + z = x + (y + z)                                 // 
00100 // -----------------------------------------------------------------------// 
00101 
00102 Theorem RefinedArithTheoremProducer::addAssoc(const Expr& x,const Expr& y,const Expr& z){
00103   Assumptions assum;
00104   Proof pf;
00105   Expr xPy = Expr(d_tm->getEM(),PLUS,x,y);
00106   Expr lhs = Expr(d_tm->getEM(),PLUS,xPy,z);
00107   Expr yPz = Expr(d_tm->getEM(),PLUS,y,z);
00108   Expr rhs = Expr(d_tm->getEM(),PLUS,x,yPz);
00109   if(withProof()) pf = newPf("add_assoc",x,y,z);
00110   return newRWTheorem(lhs,rhs,assum,pf);
00111 }
00112 
00113 // -----------------------------------------------------------------------// 
00114 // multAssoc                                                              // 
00115 //                                                                        // 
00116 // args    :                                                              // 
00117 //         : x                                                            // 
00118 //         : y                                                            // 
00119 //         : z                                                            // 
00120 //                                                                        // 
00121 // returns : |- (xy)z = x(yz)                                             // 
00122 // -----------------------------------------------------------------------// 
00123 
00124 Theorem RefinedArithTheoremProducer::multAssoc(const Expr& x,const Expr& y,const Expr& z){
00125   Assumptions assum;
00126   Proof pf;
00127   Expr xy = Expr(d_tm->getEM(),MULT,x,y);
00128   Expr lhs = Expr(d_tm->getEM(),MULT,xy,z);
00129   Expr yz = Expr(d_tm->getEM(),MULT,y,z);
00130   Expr rhs = Expr(d_tm->getEM(),MULT,x,yz);
00131   if(withProof()) pf = newPf("mult_assoc",x,y,z);
00132   return newRWTheorem(lhs,rhs,assum,pf);
00133 }
00134 
00135 // -----------------------------------------------------------------------// 
00136 // addRefl                                                                // 
00137 //                                                                        // 
00138 // args    :                                                              // 
00139 //         : x                                                            // 
00140 //         : y                                                            // 
00141 //                                                                        // 
00142 // returns : |- x + y = y + x                                             // 
00143 // -----------------------------------------------------------------------// 
00144 
00145 Theorem RefinedArithTheoremProducer::addSymm(const Expr& x,const Expr& y){
00146   Assumptions assum;
00147   Proof pf;
00148   Expr lhs = Expr(d_tm->getEM(),PLUS,x,y);
00149   Expr rhs = Expr(d_tm->getEM(),PLUS,y,x);
00150   if(withProof()) pf = newPf("add_symm",x,y);
00151   return newRWTheorem(lhs,rhs,assum,pf);
00152 }
00153 
00154 // -----------------------------------------------------------------------// 
00155 // multSymm                                                               // 
00156 //                                                                        // 
00157 // args    :                                                              // 
00158 //         : x                                                            // 
00159 //         : y                                                            // 
00160 //                                                                        // 
00161 // returns : |- xy = yx                                                   // 
00162 // -----------------------------------------------------------------------// 
00163 
00164 Theorem RefinedArithTheoremProducer::multSymm(const Expr& x,const Expr& y){
00165   Assumptions assum;
00166   Proof pf;
00167   Expr lhs = Expr(d_tm->getEM(),MULT,x,y);
00168   Expr rhs = Expr(d_tm->getEM(),MULT,y,x);
00169   if(withProof()) pf = newPf("mult_symm",x,y);
00170   return newRWTheorem(lhs,rhs,assum,pf);
00171 }
00172 
00173 // -----------------------------------------------------------------------// 
00174 // distribL                                                               // 
00175 //                                                                        // 
00176 // args    :                                                              // 
00177 //         : x                                                            // 
00178 //         : y                                                            // 
00179 //         : z                                                            // 
00180 //                                                                        // 
00181 // returns : |- x(y + z) = xy + xz                                        // 
00182 // -----------------------------------------------------------------------// 
00183 
00184 Theorem RefinedArithTheoremProducer::distribL(const Expr& x,const Expr& y,const Expr& z){
00185   Assumptions assum;
00186   Proof pf;
00187   Expr yPz = Expr(d_tm->getEM(),PLUS,y,z);
00188   Expr lhs = Expr(d_tm->getEM(),MULT,x,yPz);
00189   Expr xy = Expr(d_tm->getEM(),MULT,x,y); 
00190   Expr xz = Expr(d_tm->getEM(),MULT,x,z); 
00191   Expr rhs = Expr(d_tm->getEM(),PLUS,xy,xz);
00192   if(withProof()) pf = newPf("distrib_l",x,y,z);
00193   return newRWTheorem(lhs,rhs,assum,pf);
00194 }
00195 
00196 // -----------------------------------------------------------------------// 
00197 // addLID                                                                 // 
00198 //                                                                        // 
00199 // args    :                                                              // 
00200 //         : x                                                            // 
00201 //                                                                        // 
00202 // returns : |- 0 + x = x                                                 // 
00203 // -----------------------------------------------------------------------// 
00204 
00205 Theorem RefinedArithTheoremProducer::addLID(const Expr& x){
00206   Assumptions assum;
00207   Proof pf;
00208   Expr lhs = Expr(d_tm->getEM(),PLUS,zero,x);
00209   Expr rhs = x;
00210   if(withProof()) pf = newPf("add_lid",x);
00211   return newRWTheorem(lhs,rhs,assum,pf);
00212 }
00213 
00214 // ----------------------------------------------------------------------// 
00215 // multLID                                                               // 
00216 //                                                                       // 
00217 // args    :                                                             // 
00218 //         : x                                                           // 
00219 //                                                                       // 
00220 // returns : |- 1 * x = x                                                // 
00221 // ----------------------------------------------------------------------// 
00222 
00223 Theorem RefinedArithTheoremProducer::multLID(const Expr& x){
00224   Assumptions assum;
00225   Proof pf;
00226   Expr lhs = Expr(d_tm->getEM(),MULT,one,x);
00227   Expr rhs = x;
00228   if(withProof()) pf = newPf("mult_lid",x);
00229   return newRWTheorem(lhs,rhs,assum,pf);
00230 }
00231 
00232 // ----------------------------------------------------------------------// 
00233 // addInvR                                                               // 
00234 //                                                                       // 
00235 // args    :                                                             // 
00236 //         : x                                                           // 
00237 //                                                                       // 
00238 // returns : |- x + -x = 0                                               // 
00239 // ----------------------------------------------------------------------// 
00240 
00241 Theorem RefinedArithTheoremProducer::addInvR(const Expr& x){
00242   Assumptions assum;
00243   Proof pf;
00244   Expr ix = Expr(d_tm->getEM(),UMINUS,x);
00245   Expr lhs = Expr(d_tm->getEM(),PLUS,x,ix); 
00246   Expr rhs = zero;
00247   if(withProof()) pf = newPf("add_inv_r",x);
00248   return newRWTheorem(lhs,rhs,assum,pf);
00249 }
00250 
00251 // ----------------------------------------------------------------------// 
00252 // multInvR                                                              // 
00253 //                                                                       // 
00254 // args    :                                                             // 
00255 //         : x                                                           // 
00256 //                                                                       // 
00257 // returns : |- x * 1/x = 1                                              // 
00258 // ----------------------------------------------------------------------// 
00259 
00260 Theorem RefinedArithTheoremProducer::multInvR(const Expr& x){
00261   Assumptions assum;
00262   Proof pf;
00263   Expr ix = Expr(d_tm->getEM(),DIVIDE,one,x);
00264   Expr lhs = Expr(d_tm->getEM(),MULT,x,ix); 
00265   Expr rhs = one;
00266   if(withProof()) pf = newPf("mult_inv_r",x);
00267   return newRWTheorem(lhs,rhs,assum,pf);
00268 }
00269 
00270 // ----------------------------------------------------------------------// 
00271 // ltAddR                                                                // 
00272 //                                                                       // 
00273 // args    :                                                             // 
00274 //         : x                                                           // 
00275 //         : y                                                           // 
00276 //         : z                                                           // 
00277 //                                                                       // 
00278 // returns : |- x < y -> x + z < y + z                                   // 
00279 // ----------------------------------------------------------------------// 
00280 
00281 Theorem RefinedArithTheoremProducer::ltAddR(const Expr& x,const Expr& y,const Expr& z){
00282   Assumptions assum;
00283   Proof pf;
00284   Expr ant = Expr(d_tm->getEM(),LT,x,y);
00285   Expr lhs = Expr(d_tm->getEM(),PLUS,x,z); 
00286   Expr rhs = Expr(d_tm->getEM(),PLUS,y,z); 
00287   Expr cons = Expr(d_tm->getEM(),LT,lhs,rhs);
00288   Expr ret = Expr(d_tm->getEM(),IMPLIES,ant,cons);
00289   if(withProof()) pf = newPf("lt_add_r",x,y,z);
00290   return newTheorem(ret,assum,pf);
00291 }
00292 
00293 // ----------------------------------------------------------------------// 
00294 // ltTrans                                                               // 
00295 //                                                                       // 
00296 // args    :                                                             // 
00297 //         : x                                                           // 
00298 //         : y                                                           // 
00299 //         : z                                                           // 
00300 //                                                                       // 
00301 // returns : |- x < y -> y < z -> x < z                                  // 
00302 // ----------------------------------------------------------------------// 
00303 
00304 Theorem RefinedArithTheoremProducer::ltTrans(const Expr& x,const Expr& y,const Expr& z){
00305   Assumptions assum;
00306   Proof pf;
00307   Expr ant1 = Expr(d_tm->getEM(),LT,x,y);
00308   Expr ant2 = Expr(d_tm->getEM(),LT,y,z); 
00309   Expr cons = Expr(d_tm->getEM(),LT,x,z);
00310   Expr rhs = Expr(d_tm->getEM(),IMPLIES,ant2,cons);
00311   Expr ret = Expr(d_tm->getEM(),IMPLIES,ant1,rhs);
00312   if(withProof()) pf = newPf("lt_trans",x,y,z);
00313   return newTheorem(ret,assum,pf);
00314 }
00315 
00316 // ----------------------------------------------------------------------// 
00317 // ltScale                                                               // 
00318 //                                                                       // 
00319 // args    :                                                             // 
00320 //         : x                                                           // 
00321 //         : y                                                           // 
00322 //         : z                                                           // 
00323 //                                                                       // 
00324 // returns : |- x < y -> 0 < z -> xz < yz                                // 
00325 // ----------------------------------------------------------------------// 
00326 
00327 Theorem RefinedArithTheoremProducer::ltScale(const Expr& x,const Expr& y,const Expr& z){
00328   Assumptions assum;
00329   Proof pf;
00330   Expr ant1 = Expr(d_tm->getEM(),LT,x,y);
00331   Expr ant2 = Expr(d_tm->getEM(),LT,zero,z); 
00332   Expr xz = Expr(d_tm->getEM(),MULT,x,z);
00333   Expr yz = Expr(d_tm->getEM(),MULT,y,z);
00334   Expr cons = Expr(d_tm->getEM(),LT,xz,yz);
00335   Expr rhs = Expr(d_tm->getEM(),IMPLIES,ant2,cons);
00336   Expr ret = Expr(d_tm->getEM(),IMPLIES,ant1,rhs);
00337   if(withProof()) pf = newPf("lt_trans",x,y,z);
00338   return newTheorem(ret,assum,pf);
00339 }
00340 
00341 // ----------------------------------------------------------------------// 
00342 // arithmetic                                                            // 
00343 // lhs and rhs are op expressions whose leaves are real constants        //
00344 //                                                                       // 
00345 // args    :                                                             // 
00346 //         : lhs                                                         // 
00347 //         : rhs                                                         // 
00348 //                                                                       // 
00349 // returns : |- lhs = rhs                                                // 
00350 // ----------------------------------------------------------------------// 
00351 
00352 Theorem RefinedArithTheoremProducer::arithmetic(const Expr& lhs,const Expr& rhs){
00353   Assumptions assum;
00354   Proof pf;
00355   Rational l = eval(lhs);
00356   Rational r = eval(rhs);
00357   if(l == r){
00358     if(withProof()) pf = newPf("arithmetic",lhs,rhs);
00359     return newRWTheorem(lhs,rhs,assum,pf);
00360   } else {
00361     CHECK_SOUND(false,"lhs and rhs not equal:\n lhs: " + lhs.toString() 
00362                              + "\n rhs: " + rhs.toString());
00363   }
00364 }
00365 
00366 Rational RefinedArithTheoremProducer::eval(const Expr& e){
00367   vector<Rational> children;
00368   Rational val = 0;
00369   for (int i = 0; i < e.arity(); i++){
00370     Rational child = eval(e[i]);
00371     children.push_back(child);
00372   }
00373   switch (e.getKind()){
00374   case RATIONAL_EXPR:
00375     return e.getRational();
00376     break;
00377   case MULT: 
00378     for(unsigned i = 0; i< children.size();i++)
00379       val *= children[i];
00380     return val;
00381     break;
00382   case UMINUS: 
00383     return -(e[0].getRational());
00384     break;
00385   case PLUS:
00386     for(unsigned i = 0; i< children.size();i++)
00387       val += children[i];
00388     return val;
00389     break;
00390   case DIVIDE:
00391     return children[0]/childrent[1];
00392     break;
00393   default:
00394     CHECK_SOUND(false,"Can't evaluate rational expression: " + e.toString());
00395   }
00396 }
00397 
00398 // ======================================================================// 
00399 //  Definitions                                                          // 
00400 // ======================================================================// 
00401 
00402  
00403 // ----------------------------------------------------------------------// 
00404 // minusDef                                                              // 
00405 //                                                                       // 
00406 // args    :                                                             // 
00407 //         : x                                                           // 
00408 //         : y                                                           // 
00409 //                                                                       // 
00410 // returns : |- x - y = x + (-y)                                         // 
00411 // ----------------------------------------------------------------------// 
00412 Theorem RefinedArithTheoremProducer::minusDef(const Expr& x,const Expr& y){
00413   Assumptions assum;
00414   Proof pf;
00415   Expr xMy = Expr(d_tm->getEM(),MINUS,x,y);
00416   Expr xPMy = plus(x,neg(y));
00417   if(withProof()) pf = newPf("minus_def",x,y);
00418   return newRWTheorem(xMy,xPMy,assum,pf);
00419 }
00420 
00421 // ----------------------------------------------------------------------// 
00422 // divideDef                                                             // 
00423 //                                                                       // 
00424 // args    :                                                             // 
00425 //         : a                                                           // 
00426 //         : b                                                           // 
00427 //                                                                       // 
00428 // returns : |- a/b = 1/b * a                                            // 
00429 // ----------------------------------------------------------------------// 
00430 Theorem RefinedArithTheoremProducer::divideDef(const Expr& a,const Expr& b){
00431   Assumptions assum;
00432   Proof pf;
00433   Expr aDb = Expr(d_tm->getEM(),DIVIDE,a,b);
00434   Expr xPMy = plus(x,neg(y));
00435   if(withProof()) pf = newPf("minus_def",x,y);
00436   return newRWTheorem(xMy,xPMy,assum,pf);
00437 }
00438 
00439 // ----------------------------------------------------------------------// 
00440 // exOp                                                                  // 
00441 //                                                                       // 
00442 // args    :                                                             // 
00443 //         : e                                                           // 
00444 //                                                                       // 
00445 // returns : |- (op e_1 e_2 ... e_n) = ((((op e_1 e_2) e_3) e_4)... e_n) // 
00446 // ----------------------------------------------------------------------// 
00447 Theorem RefinedArithTheoremProducer::exOp(const Expr& e){
00448   Assumptions assum;
00449   Proof pf;
00450   int arity = p.arity();
00451   CHECK_SOUND(arity>=2,"op expressions have at least 2 children");
00452   int kind = e.getKind();
00453   Expr ex = Expr(d_tm->getEM(),kind,e[0],e[1]);
00454   for(int i=2;i<arity;i++){
00455     ex = Expr(d_tm->getEM(),kind,ex,e[i]);
00456   }
00457   if(withProof()) pf = newPf("exOp",e,ex);
00458   return newRWTheorem(e,ex,assum,pf);
00459 }
00460 
00461 
00462 // ======================================================================// 
00463 //  Derived Rules (No use of new[RW]Theorem from now on)                 // 
00464 // ======================================================================// 
00465 
00466 // ----------------------------------------------------------------------// 
00467 // distribR                                                              // 
00468 //                                                                       // 
00469 // args    :                                                             // 
00470 //         : x                                                           // 
00471 //         : y                                                           // 
00472 //         : z                                                           // 
00473 //                                                                       // 
00474 // returns : |- (x + y) * z = xz + yz                                    // 
00475 // ----------------------------------------------------------------------// 
00476 
00477 ////////////////////////////
00478 // Proof:
00479 //         1)  (x+y)z = z(x+y)    : multSymm
00480 //         2)  z(x+y) = zx+zy     : distribL
00481 //         3)  zx = xz            : multSymm
00482 //         4)  zy = yz            : multSymm
00483 //         5)  (x+y)z = zx+zy     : transitivityRule 1,2
00484 //         6)  zx+zy = xz+yz      : substitutivityRule 3,4
00485 //         7)  (x+y)z = xz+yz     : transitivityRule 5,6
00486 //
00487 ////////////////////////////
00488 Theorem RefinedArithTheoremProducer::distribR(const Expr& x,const Expr& y,const Expr& z){
00489   Expr xPy = Expr(d_em,PLUS,x,y);
00490   Theorem t1 = multSymm(xPy,z);
00491   Theorem t2 = distribL(z,x,y);
00492   Theorem t3 = multSymm(z,x);
00493   Theorem t4 = multSymm(z,y);
00494   Theorem t5 = trans(t1,t2);
00495   Theorem t6 = subst(Op(PLUS),t3,t4);
00496   Theorem t7 = trans(t5,t6);
00497   return t7;
00498 }
00499 
00500 // ----------------------------------------------------------------------// 
00501 // addR                                                                  // 
00502 //                                                                       // 
00503 // args    :                                                             // 
00504 //         : |- x = y                                                    // 
00505 //         : z                                                           // 
00506 //                                                                       // 
00507 // returns : |- x + z = y + z                                            // 
00508 // ----------------------------------------------------------------------// 
00509 Theorem RefinedArithTheoremProducer::addR(const Theorem& xEy,const Expr& z){
00510   Theorem ret = subst(Op(PLUS),xEy,z);
00511   return ret;
00512 }
00513 
00514 // ----------------------------------------------------------------------// 
00515 // addRID                                                                // 
00516 //                                                                       // 
00517 // args    :                                                             // 
00518 //         : x                                                           // 
00519 //                                                                       // 
00520 // returns : |- x + 0 = x                                                // 
00521 // ----------------------------------------------------------------------// 
00522 
00523 ////////////////////////////
00524 // Proof:
00525 //         1)  x + 0 = 0 + x      : addSymm
00526 //         2)  0 + x = x          : addLID
00527 //         3)  x + 0 = x          : transitivityRule 1 2
00528 //
00529 ////////////////////////////
00530 Theorem RefinedArithTheoremProducer::addRID(const Expr& x){
00531   Theorem t1 = addSymm(x,zero);
00532   Theorem t2 = addLID(x);
00533   Theorem ret = trans(t1,t2);
00534   return ret;
00535 }
00536 
00537 // ----------------------------------------------------------------------// 
00538 // cancelR                                                               // 
00539 //                                                                       // 
00540 // args    :                                                             // 
00541 //         : x                                                           // 
00542 //         : y                                                           // 
00543 //                                                                       // 
00544 // returns : |- (x+y)+-y = x                                             // 
00545 // ----------------------------------------------------------------------// 
00546 
00547 ////////////////////////////
00548 // Proof:
00549 //         1)  (x+y)+-y = x+(y+-y)              : addAssoc
00550 //         2)  y+-y = 0                         : addInvR
00551 //         3)  x+(y+-y) = x+0                   : substitutivityRule
00552 //         4)  x+0 = x                          : substitutivityRule
00553 //         5)  (x+y)+-y = x+0                   : transitivityRule 2 4
00554 //         6)  (x+y)+-y = x                     : transitivityRule 6 5
00555 //
00556 ////////////////////////////
00557 Theorem RefinedArithTheoremProducer::cancelR(const Expr& x,const Expr& y){ 
00558   Expr yi = neg(y); 
00559   Theorem t1 = addAssoc(x,y,yi);
00560   Theorem t2 = addInvR(y);
00561   Theorem t3 = subst(Op(PLUS),x,t2);
00562   Theorem t4 = addRID(x);
00563   Theorem t5 = trans(t1,t3);
00564   Theorem t6 = trans(t5,t4);
00565   return t6;
00566 }
00567                                         
00568 
00569 // ----------------------------------------------------------------------// 
00570 // addRCancel                                                            // 
00571 //                                                                       // 
00572 // args    :                                                             // 
00573 //         : |- x + z = y + z                                            // 
00574 //                                                                       // 
00575 // returns : |- x = y                                                    // 
00576 // ----------------------------------------------------------------------// 
00577 
00578 ////////////////////////////
00579 // Proof:
00580 //         1)  (x+z)+-z = (y+z)+-z              : addR
00581 //         2)  (x+z)+-z = x                     : cancelR
00582 //         3)  (y+z)+-z = y                     : cancelR
00583 //         4)  x=(x+z)+-z                       : symmetryRule
00584 //         5)  x=(y+z)+-z                       : transitivityRule 4 1
00585 //         6)  x=y                              : transitivityRule 5 3
00586 //
00587 ////////////////////////////
00588 Theorem RefinedArithTheoremProducer::addRCancel(const Theorem& t){
00589   Expr x = t.getLHS()[0];
00590   Expr y = t.getRHS()[0];
00591   Expr z = t.getLHS()[1];
00592   Theorem t1 = addR(t,neg(z));
00593   Theorem t2 = cancelR(x,z);
00594   Theorem t3 = cancelR(y,z);
00595   Theorem t4 = symm(t2);
00596   Theorem t5 = trans(t4,t1);
00597   Theorem t6 = trans(t5,t3);
00598   return t6;
00599 }
00600 
00601 
00602 // ----------------------------------------------------------------------// 
00603 // multZeroL                                                             // 
00604 //                                                                       // 
00605 // args    :                                                             // 
00606 //         : e                                                           // 
00607 //                                                                       // 
00608 // returns : |- 0 * e = 0                                                // 
00609 // ----------------------------------------------------------------------// 
00610 
00611 ////////////////////////////
00612 // Proof:
00613 //         1)  0 = 0 + 0                            : arithmetic
00614 //         2)  0*e = (0+0)*e                        : substitutivityRule 2
00615 //        2a)  (0+0)*e = 0*e+0*e                    : distribR
00616 //         3)  0*e = 0*e+0*e                        : transitivityRule 2 2a
00617 //         4)  0*e + -0*e = (0*e + 0*e) + -0*e      : addR 4
00618 //         5)  (0*e + 0*e) + -0*e = 0*e + (0*e + -0*e) : addAssoc 
00619 //         6)  0*e + -0*e = 0*e + (0*e + -0*e)      : transitivityRule 4 5
00620 //         7)  0*e + -0*e = 0                       : addInvR
00621 //         8)  0 = 0*e + -0*e                       : symm
00622 //         9)  0 = 0*e + (0*e + -0*e)               : transitivityRule 8 6
00623 //        10)  0*e + (0*e + -0*e) = 0*e + 0         : substitutivityRule 8
00624 //        11)  0 = 0*e + 0                          : transitivityRule 9 10
00625 //        12)  0*e + 0 = 0*e                        : addRID
00626 //        13)  0 = 0*e                              : transitivityRule 11 12
00627 //        14)  0*e = 0                              : symmetryRule 14
00628 ////////////////////////////
00629 Theorem RefinedArithTheoremProducer::multZeroL(const Expr& e){
00630   Expr zz = Expr(d_tm->getEM(),PLUS,zero,zero);
00631   Theorem t1 = arithmetic(zero,zz);
00632   Theorem t2 = subst(Op(MULT),t1,e);
00633   Theorem t2a = distribR(zero,zero,e);
00634   Theorem t3 = trans(t2,t2a);
00635   Expr ze = t2.getLHS();
00636   Expr mze = neg(ze);
00637   Theorem t4 = addR(t3,mze);
00638   Theorem t5 = addAssoc(ze,ze,mze);
00639   Theorem t6 = trans(t4,t5);
00640   Theorem t7 = addInvR(ze);
00641   Theorem t8 = symm(t7);
00642   Theorem t9 = trans(t8,t6);
00643   Theorem t10 = subst(Op(PLUS),ze,t7);
00644   Theorem t11 = trans(t9,t10);
00645   Theorem t12 = addRID(ze);
00646   Theorem t13 = trans(t11,t12);
00647   Theorem ret = symm(t13);
00648   return ret;
00649 }
00650 
00651 // ======================================================================// 
00652 //  Rules for Linear Arithmetic Decision Procedure                       // 
00653 // ======================================================================// 
00654 
00655 // ----------------------------------------------------------------------// 
00656 // uMinusToMult                                                          // 
00657 //                                                                       // 
00658 // args    :                                                             // 
00659 //         : y                                                           // 
00660 //                                                                       // 
00661 // returns : |- -y = -1*y                                                // 
00662 // ----------------------------------------------------------------------// 
00663 
00664 //////////////////////////////
00665 // Proof:
00666 //         1)  0*y = 0                              :  multZeroL
00667 //         2)  0 = 0*y                              :  symm
00668 //         3)  0 = -1+1                             :  arithmetic
00669 //         4)  0y=(-1+1)y                           :  subst
00670 //         5)  0=(-1+1)y                            :  trans
00671 //         6)  (-1+1)y=-1y+1y                       :  distribR
00672 //         7)  0=-1y+1y                             :  trans
00673 //         8)  1y=y                                :  multLID
00674 //         9)  -1y+1y=-1y+y                        :  subst
00675 //         10)  0=-1y+y                             :  trans
00676 //         11)  0+-y=(-1y+y)+-y                     :  addR
00677 //         12)  0+-y=-y                             :  addLID
00678 //         13)  -y=0+-y                             :  symm
00679 //         14)  -y=(-1y+y)+-y                       :  trans
00680 //         15)  (-1y+y)+-y=-1y+(y+-y)               :  addAssoc
00681 //         16)  -y = -1y+(y+-y)                     :  trans
00682 //         17)  y+-y=0                              :  addInv
00683 //         18)  -1y+(y+-y)=-1y+0                    :  subst
00684 //         19)  -y = -1y+0                          :  trans
00685 //         20)  -1y+0=-1y                           :  addRID
00686 //         21)  -y=-1y                              :  trans
00687 //////////////////////////////
00688 Theorem RefinedArithTheoremProducer::uMinusToMult(const Expr& y){
00689   Theorem t1 = multZeroL(y);
00690   Theorem t2 = symm(t1);
00691   Theorem t3 = arithmetic(zero,plus(neg(one),one));
00692   Theorem t4 = subst(Op(MULT),t3,y);
00693   Theorem t5 = trans(t2,t4);
00694   Theorem t6 = distribR(neg(one),one,y);
00695   Theorem t7 = trans(t5,t6);
00696   Theorem t8 = multLID(y);
00697   Expr m1y = t7.getRHS()[0];
00698   Theorem t9 = subst(Op(PLUS),m1y,t8);
00699   Theorem t10 = trans(t7,t9);
00700   Theorem t11 = addR(t10,neg(y));
00701   Theorem t12 = addLID(neg(y));
00702   Theorem t13 = symm(t12);
00703   Theorem t14 = trans(t13,t11);
00704   Theorem t15 = addAssoc(m1y,y,neg(y));
00705   Theorem t16 = trans(t14,t15);
00706   Theorem t17 = addInvR(y);
00707   Theorem t18 = subst(Op(PLUS),m1y,t17);
00708   Theorem t19 = trans(t16,t18);
00709   Theorem t20 = addRID(m1y);
00710   Theorem t21 = trans(t19,t20);
00711   return t21;
00712 }
00713 
00714 
00715 // ----------------------------------------------------------------------// 
00716 // minusToPlus                                                           // 
00717 //                                                                       // 
00718 // args    :                                                             // 
00719 //         : x                                                           // 
00720 //         : y                                                           // 
00721 //                                                                       // 
00722 // returns : |- x - y = x + (-1) * y                                     // 
00723 // ----------------------------------------------------------------------// 
00724 //////////////////////////////
00725 // Proof:
00726 //         1)  x-y=x+-y                             :  minusDef
00727 //         2)  -y = -1*y                            :  uMinusToMult
00728 //         3)  x+-y=x+(-1*y)                        :  subst
00729 //         4)  x-y = x+(-1*y)                       :  trans
00730 //////////////////////////////
00731 Theorem RefinedArithTheoremProducer::minusToPlus(const Expr& x,const Expr& y){
00732   Theorem t1 = minusDef(x,y);
00733   Theorem t2 = uMinusToMult(y);
00734   Theorem t3 = subst(Op(PLUS),x,t2);
00735   Theorem t4 = trans(t1,t3);
00736   return t4;
00737 }
00738