arith_theorem_producer_old.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file arith_theorem_producer.cpp
00004  * 
00005  * Author: Vijay Ganesh, Sergey Berezin
00006  * 
00007  * Created: Dec 13 02:09:04 GMT 2002
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 // CLASS: ArithProofRules
00021 //
00022 // AUTHOR: Sergey Berezin, 12/11/2002
00023 // AUTHOR: Vijay Ganesh,   05/30/2003
00024 //
00025 // Description: TRUSTED implementation of arithmetic proof rules.
00026 //
00027 ///////////////////////////////////////////////////////////////////////////////
00028 
00029 // This code is trusted
00030 #define _CVC3_TRUSTED_
00031 
00032 #include "arith_theorem_producer_old.h"
00033 #include "theory_core.h"
00034 #include "theory_arith_old.h"
00035 
00036 using namespace std;
00037 using namespace CVC3;
00038 
00039 ////////////////////////////////////////////////////////////////////
00040 // TheoryArith: trusted method for creating ArithTheoremProducerOld
00041 ////////////////////////////////////////////////////////////////////
00042 
00043 ArithProofRules* TheoryArithOld::createProofRulesOld() {
00044   return new ArithTheoremProducerOld(theoryCore()->getTM(), this);
00045 }
00046   
00047 ////////////////////////////////////////////////////////////////////
00048 // Canonization rules
00049 ////////////////////////////////////////////////////////////////////
00050 
00051 
00052 #define CLASS_NAME "ArithTheoremProducerOld"
00053 
00054 
00055 // Rule for variables: e == 1 * e
00056 Theorem ArithTheoremProducerOld::varToMult(const Expr& e) {
00057   Proof pf;
00058   if(withProof()) pf = newPf("var_to_mult", e);
00059   return newRWTheorem(e, (rat(1) * e), Assumptions::emptyAssump(), pf);
00060 }
00061 
00062 
00063 // Rule for unary minus: -e == (-1) * e
00064 Theorem ArithTheoremProducerOld::uMinusToMult(const Expr& e) {
00065   Proof pf;
00066   if(withProof()) pf = newPf("uminus_to_mult", e);
00067   return newRWTheorem((-e), (rat(-1) * e), Assumptions::emptyAssump(), pf);
00068 }
00069 
00070 
00071 // ==> x - y = x + (-1) * y
00072 Theorem ArithTheoremProducerOld::minusToPlus(const Expr& x, const Expr& y)
00073 {
00074   Proof pf;
00075   if(withProof()) pf = newPf("minus_to_plus", x, y);
00076   return newRWTheorem((x-y), (x + (rat(-1) * y)), Assumptions::emptyAssump(), pf);  
00077 }
00078 
00079 
00080 // Rule for unary minus: -e == e/(-1)
00081 // This is to reduce the number of almost identical rules for uminus and div
00082 Theorem ArithTheoremProducerOld::canonUMinusToDivide(const Expr& e) {
00083   Proof pf;
00084   if(withProof()) pf = newPf("canon_uminus", e);
00085   return newRWTheorem((-e), (e / rat(-1)), Assumptions::emptyAssump(), pf);
00086 }
00087 
00088 // Rules for division by constant
00089 
00090 // (c)/(d) ==> (c/d).  When d==0, c/0 = 0 (our total extension).
00091 Theorem ArithTheoremProducerOld::canonDivideConst(const Expr& c,
00092                                                const Expr& d) {
00093   // Make sure c and d are a const
00094   if(CHECK_PROOFS) {
00095     CHECK_SOUND(isRational(c),
00096                 CLASS_NAME "::canonDivideConst:\n c not a constant: "
00097                 + c.toString());
00098     CHECK_SOUND(isRational(d),
00099                 CLASS_NAME "::canonDivideConst:\n d not a constant: "
00100                 + d.toString());
00101   }
00102   Proof pf;
00103   if(withProof())
00104     pf = newPf("canon_divide_const", c, d, d_hole);
00105   const Rational& dr = d.getRational();
00106   return newRWTheorem((c/d), (rat(dr==0? 0 : (c.getRational()/dr))), Assumptions::emptyAssump(), pf);
00107 }
00108 
00109 // (c * x)/d ==> (c/d) * x, takes (c*x) and d
00110 Theorem ArithTheoremProducerOld::canonDivideMult(const Expr& cx,
00111                                               const Expr& d) {
00112   // Check the format of c*x
00113   if(CHECK_PROOFS) {
00114     CHECK_SOUND(isMult(cx) && isRational(cx[0]),
00115                 CLASS_NAME "::canonDivideMult:\n  "
00116                 "Not a (c * x) expression: "
00117                 + cx.toString());
00118     CHECK_SOUND(isRational(d),
00119                 CLASS_NAME "::canonDivideMult:\n  "
00120                 "d is not a constant: " + d.toString());
00121   }
00122   const Rational& dr = d.getRational();
00123   Rational cdr(dr==0? 0 : (cx[0].getRational()/dr));
00124   Expr cd(rat(cdr));
00125   Proof pf;
00126   if(withProof())
00127     pf = newPf("canon_divide_mult", cx[0], cx[1], d);
00128   // (c/d) may be == 1, so we also need to canonize 1*x to x
00129   if(cdr == 1)
00130     return newRWTheorem((cx/d), (cx[1]), Assumptions::emptyAssump(), pf);
00131   else if(cdr == 0) // c/0 == 0 case
00132     return newRWTheorem((cx/d), cd, Assumptions::emptyAssump(), pf);
00133   else
00134     return newRWTheorem((cx/d), (cd*cx[1]), Assumptions::emptyAssump(), pf);
00135 }
00136 
00137 // (+ t1 ... tn)/d ==> (+ (t1/d) ... (tn/d))
00138 Theorem ArithTheoremProducerOld::canonDividePlus(const Expr& sum, const Expr& d) {
00139   if(CHECK_PROOFS) {
00140     CHECK_SOUND(isPlus(sum) && sum.arity() >= 2 && isRational(sum[0]),
00141                 CLASS_NAME "::canonUMinusPlus:\n  "
00142                 "Expr is not a canonical sum: "
00143                 + sum.toString());
00144     CHECK_SOUND(isRational(d),
00145                 CLASS_NAME "::canonUMinusPlus:\n  "
00146                 "d is not a const: " + d.toString());
00147   }
00148   // First, propagate '/d' down to the args
00149   Proof pf;
00150   if(withProof())
00151     pf = newPf("canon_divide_plus", rat(sum.arity()),
00152                sum.begin(), sum.end());
00153   vector<Expr> newKids;
00154   for(Expr::iterator i=sum.begin(), iend=sum.end(); i!=iend; ++i)
00155     newKids.push_back((*i)/d);
00156   // (+ t1 ... tn)/d == (+ (t1/d) ... (tn/d))
00157   return newRWTheorem((sum/d), (plusExpr(newKids)), Assumptions::emptyAssump(), pf);
00158 }
00159 
00160 // x/(d) ==> (1/d) * x, unless d == 1
00161 Theorem ArithTheoremProducerOld::canonDivideVar(const Expr& e, const Expr& d) {
00162   if(CHECK_PROOFS) {
00163     CHECK_SOUND(isRational(d),
00164                 CLASS_NAME "::canonDivideVar:\n  "
00165                 "d is not a const: " + d.toString());
00166   }
00167   Proof pf;
00168 
00169   if(withProof())
00170     pf = newPf("canon_divide_var", e);
00171 
00172   const Rational& dr = d.getRational();
00173   if(dr == 1) 
00174     return newRWTheorem(e/d, e, Assumptions::emptyAssump(), pf);
00175   if(dr == 0) // e/0 == 0 (total extension of division)
00176     return newRWTheorem(e/d, d, Assumptions::emptyAssump(), pf);
00177   else
00178     return newRWTheorem(e/d, rat(1/dr) * e, Assumptions::emptyAssump(), pf);
00179 }
00180 
00181 
00182 // Multiplication
00183 // (MULT expr1 expr2 expr3 ...)
00184 // Each expr is in canonical form, i.e. it can be a
00185 // 1) Rational constant
00186 // 2) Arithmetic Leaf (var or term from another theory)
00187 // 3) (POW rational leaf)
00188 // where rational cannot be 0 or 1
00189 // 4) (MULT rational mterm'_1 ...) where each mterm' is of type (2) or (3)
00190 // If rational == 1 then there should be at least two mterms
00191 // 5) (PLUS rational sterm_1 ...) where each sterm is of 
00192 //     type (2) or (3) or (4) 
00193 //    if rational == 0 then there should be at least two sterms
00194 
00195 
00196 Expr ArithTheoremProducerOld::simplifiedMultExpr(std::vector<Expr> & mulKids)
00197 {
00198   DebugAssert(mulKids.size() >= 1 && mulKids[0].isRational(), "");
00199   if (mulKids.size() == 1) {
00200     return mulKids[0];
00201   }
00202   if ((mulKids[0] == rat(1)) && mulKids.size() == 2) {
00203     return mulKids[1];
00204   }
00205   else
00206     return multExpr(mulKids);
00207 }
00208 
00209 Expr ArithTheoremProducerOld::canonMultConstMult(const Expr & c,
00210                                               const Expr & e)
00211 {
00212   // c is a rational
00213   // e is (MULT rat mterm'_1 ....)
00214   // assume that e2 is already in canonic form
00215   DebugAssert(c.isRational() && e.getKind() == MULT, "");
00216   std::vector<Expr> mulKids;
00217   DebugAssert ((e.arity() > 1) && (e[0].isRational()),
00218                "ArithTheoremProducerOld::canonMultConstMult: "
00219                "a canonized MULT expression must have arity "
00220                "greater than 1: and first child must be "
00221                "rational " + e.toString());
00222   Expr::iterator i = e.begin();
00223   mulKids.push_back(rat(c.getRational() * (*i).getRational()));
00224   ++i;
00225   for(; i != e.end(); ++i) {
00226     mulKids.push_back(*i);
00227   }
00228   return simplifiedMultExpr(mulKids);
00229 }
00230 
00231 Expr ArithTheoremProducerOld::canonMultConstPlus(const Expr & e1,
00232                                               const Expr & e2)
00233 {
00234   DebugAssert(e1.isRational() && e2.getKind() == PLUS &&
00235               e2.arity() > 0, "");
00236   // e1 is a rational
00237   // e2 is of the form (PLUS rational sterm1 sterm2 ...)
00238   // assume that e2 is already in canonic form
00239   std::vector<Theorem> thmPlusVector;
00240   Expr::iterator i = e2.begin();
00241   for(; i!= e2.end(); ++i) {
00242     thmPlusVector.push_back(canonMultMtermMterm(e1*(*i)));
00243   }
00244     
00245   Theorem thmPlus1 = 
00246     d_theoryArith->substitutivityRule(e2.getOp(), thmPlusVector);
00247   return thmPlus1.getRHS();
00248 }
00249 
00250 Expr ArithTheoremProducerOld::canonMultPowPow(const Expr & e1,
00251                                            const Expr & e2)
00252 {
00253   DebugAssert(e1.getKind() == POW && e2.getKind() == POW, "");
00254   // (POW r1 leaf1) * (POW r2 leaf2)
00255   Expr leaf1 = e1[1];
00256   Expr leaf2 = e2[1];
00257   Expr can_expr;
00258   if (leaf1 == leaf2) {
00259     Rational rsum = e1[0].getRational() + e2[0].getRational();
00260     if (rsum == 0) {
00261       return rat(1);
00262     }
00263     else if (rsum == 1) {
00264       return leaf1;
00265     }
00266     else
00267       {
00268         return powExpr(rat(rsum), leaf1);
00269       }
00270   }
00271   else
00272     {
00273       std::vector<Expr> mulKids;
00274       mulKids.push_back(rat(1));
00275       // the leafs should be put in decreasing order
00276       if (leaf1 < leaf2) {
00277         mulKids.push_back(e2);
00278         mulKids.push_back(e1);
00279       }
00280       else 
00281         {
00282           mulKids.push_back(e1);
00283           mulKids.push_back(e2);
00284         }
00285       // FIXME: don't really need to simplify, just wrap up a MULT?
00286       return simplifiedMultExpr(mulKids);
00287     }
00288 }
00289 
00290 Expr ArithTheoremProducerOld::canonMultPowLeaf(const Expr & e1,
00291                                             const Expr & e2)
00292 {
00293   DebugAssert(e1.getKind() == POW, "");
00294   // (POW r1 leaf1) * leaf2
00295   Expr leaf1 = e1[1];
00296   Expr leaf2 = e2;
00297   Expr can_expr;
00298   if (leaf1 == leaf2) {
00299     Rational rsum = e1[0].getRational() + 1;
00300     if (rsum == 0) {
00301       return rat(1);
00302     }
00303     else if (rsum == 1) {
00304       return leaf1;
00305     }
00306     else
00307       {
00308         return powExpr(rat(rsum), leaf1);
00309       }
00310   }
00311   else
00312     {
00313       std::vector<Expr> mulKids;
00314       mulKids.push_back(rat(1));
00315       // the leafs should be put in decreasing order
00316       if (leaf1 < leaf2) {
00317         mulKids.push_back(e2);
00318         mulKids.push_back(e1);
00319       }
00320       else 
00321         {
00322           mulKids.push_back(e1);
00323           mulKids.push_back(e2);
00324         }
00325       return simplifiedMultExpr(mulKids);
00326     }
00327 }
00328 
00329 Expr ArithTheoremProducerOld::canonMultLeafLeaf(const Expr & e1,
00330                                              const Expr & e2)
00331 {
00332   // leaf1 * leaf2
00333   Expr leaf1 = e1;
00334   Expr leaf2 = e2;
00335   Expr can_expr;
00336   if (leaf1 == leaf2) {
00337     return powExpr(rat(2), leaf1);
00338   }
00339   else
00340     {
00341       std::vector<Expr> mulKids;
00342       mulKids.push_back(rat(1));
00343       // the leafs should be put in decreasing order
00344       if (leaf1 < leaf2) {
00345         mulKids.push_back(e2);
00346         mulKids.push_back(e1);
00347       }
00348       else 
00349         {
00350           mulKids.push_back(e1);
00351           mulKids.push_back(e2);
00352         }
00353       return simplifiedMultExpr(mulKids);
00354     }
00355 }
00356 
00357 Expr ArithTheoremProducerOld::canonMultLeafOrPowMult(const Expr & e1,
00358                                                   const Expr & e2)
00359 {
00360   DebugAssert(e2.getKind() == MULT, "");
00361   // Leaf * (MULT rat1 mterm1 ...)
00362   // (POW r1 leaf1) * (MULT rat1 mterm1 ...) where
00363   // each mterm is a leaf or (POW r leaf).  Furthermore the leafs
00364   // in the mterms are in descending order
00365   Expr leaf1 = e1.getKind() == POW ? e1[1] : e1;
00366   std::vector<Expr> mulKids;
00367   DebugAssert(e2.arity() > 1, "MULT expr must have arity 2 or more");
00368   Expr::iterator i = e2.begin();
00369   // push the rational
00370   mulKids.push_back(*i);
00371   ++i;
00372   // Now i points to the first mterm
00373   for(; i != e2.end(); ++i) {
00374     Expr leaf2 = ((*i).getKind() == POW) ? (*i)[1] : (*i);
00375     if (leaf1 == leaf2) {
00376       Rational r1 = e1.getKind() == POW ? e1[0].getRational() : 1;
00377       Rational r2 = 
00378         ((*i).getKind() == POW ? (*i)[0].getRational() : 1);
00379       // if r1 + r2 == 0 then it is the case of x^n * x^{-n}
00380       // So, nothing needs to be added
00381       if (r1 + r2 != 0) {
00382         if (r1 + r2 == 1) {
00383           mulKids.push_back(leaf1);
00384         }
00385         else
00386           {
00387             mulKids.push_back(powExpr(rat(r1 + r2), leaf1));
00388           }
00389       }
00390       break;
00391     }
00392     // This ensures that the leaves in the mterms are also arranged
00393     // in decreasing order
00394     // Note that this will need to be changed if we want the order to
00395     // be increasing order.
00396     else if (leaf2 < leaf1) {
00397       mulKids.push_back(e1);
00398       mulKids.push_back(*i);
00399       break;
00400     }
00401     else // leaf1 < leaf2
00402       mulKids.push_back(*i);
00403   }
00404   if (i == e2.end()) {
00405     mulKids.push_back(e1);
00406   }
00407   else
00408     {
00409       // e1 and *i have already been added
00410       for (++i; i != e2.end(); ++i) {
00411         mulKids.push_back(*i);
00412       }
00413     }
00414   return simplifiedMultExpr(mulKids);
00415 }
00416 
00417 // Local class for ordering monomials; note, that it flips the
00418 // ordering given by greaterthan(), to sort in ascending order.
00419 class MonomialLess {
00420 public:
00421   bool operator()(const Expr& e1, const Expr& e2) const {
00422     return ArithTheoremProducerOld::greaterthan(e1,e2);
00423   }
00424 };
00425 
00426 typedef map<Expr,Rational,MonomialLess> MonomMap;
00427 
00428 Expr 
00429 ArithTheoremProducerOld::canonCombineLikeTerms(const std::vector<Expr> & sumExprs)
00430 {
00431   Rational constant = 0;
00432   MonomMap sumHashMap;
00433   vector<Expr> sumKids;
00434  
00435   // Add each distinct mterm (not including the rational) into 
00436   // an appropriate hash map entry 
00437   std::vector<Expr>::const_iterator i = sumExprs.begin();
00438   for (; i != sumExprs.end(); ++i) {
00439     Expr mul = *i;
00440     if (mul.isRational()) {
00441       constant = constant + mul.getRational();
00442     }
00443     else {
00444       switch (mul.getKind()) {
00445       case MULT: {
00446         std::vector<Expr> mulKids;
00447         DebugAssert(mul.arity() > 1 && mul[0].isRational(),"");
00448         mulKids.push_back(rat(1));
00449         Expr::iterator j = mul.begin();
00450         ++j;
00451         for (; j!= mul.end(); ++j) {
00452           mulKids.push_back(*j);
00453         }
00454                 
00455         // make sure that tempExpr is also in canonic form
00456         Expr tempExpr = mulKids.size() > 2 ? multExpr(mulKids): mulKids[1];
00457   MonomMap::iterator i=sumHashMap.find(tempExpr);
00458         if (i == sumHashMap.end()) {
00459           sumHashMap[tempExpr] = mul[0].getRational();
00460         }
00461         else {
00462           (*i).second += mul[0].getRational();
00463         }
00464       }
00465         break;
00466       default: {
00467   MonomMap::iterator i=sumHashMap.find(mul);
00468         // covers the case of POW, leaf
00469         if (i == sumHashMap.end()) {
00470           sumHashMap[mul] = 1;
00471         }
00472         else {
00473           (*i).second += 1;
00474         }
00475         break;
00476       }
00477       }
00478     }
00479   }
00480   // Now transfer to sumKids
00481   sumKids.push_back(rat(constant));
00482   MonomMap::iterator j = sumHashMap.begin(), jend=sumHashMap.end();
00483   for(; j != jend; ++j) {
00484     if ((*j).second != 0)
00485       sumKids.push_back
00486   (canonMultMtermMterm(rat((*j).second) * (*j).first).getRHS());
00487   }
00488     
00489   /*
00490     for (unsigned k = 0; k < sumKids.size(); ++k)
00491     {
00492     cout << "sumKids[" << k << "] = " << sumKids[k].toString() << endl;
00493     }
00494   */    
00495 
00496   // The ordering in map guarantees the correct order; no need to sort
00497 
00498   // std::sort(sumKids.begin(), sumKids.end(), greaterthan);
00499     
00500   if ((constant == 0) && (sumKids.size() == 2)) {
00501     return sumKids[1];
00502   }
00503   else if (sumKids.size() == 1) {
00504     return sumKids[0];
00505   }
00506   else
00507     return plusExpr(sumKids);
00508 }
00509 
00510 Expr ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus(const Expr & e1,
00511                                                         const Expr & e2)
00512 {
00513   DebugAssert(e2.getKind() == PLUS, "");
00514   // Leaf *  (PLUS rational sterm1 ...) 
00515   // or 
00516   // (POW n1 x1) * (PLUS rational sterm1 ...)
00517   // or
00518   // (MULT r1 m1 m2 ...) * (PLUS rational sterm1 ...)
00519   // assume that e1 and e2 are themselves canonized
00520   std::vector<Expr> sumExprs;
00521   // Multiply each term in turn. 
00522   Expr::iterator i = e2.begin();
00523   for (; i != e2.end(); ++i) {
00524     sumExprs.push_back(canonMultMtermMterm(e1 * (*i)).getRHS());
00525   }
00526   return canonCombineLikeTerms(sumExprs);
00527 }
00528 
00529 Expr ArithTheoremProducerOld::canonMultPlusPlus(const Expr & e1,
00530                                              const Expr & e2)
00531 {
00532   DebugAssert(e1.getKind() == PLUS && e2.getKind() == PLUS, "");
00533   // (PLUS r1 .... ) * (PLUS r1' ...)
00534   // assume that e1 and e2 are themselves canonized
00535 
00536   std::vector<Expr> sumExprs;
00537   // Multiply each term in turn. 
00538   Expr::iterator i = e1.begin();
00539   for (;  i != e1.end(); ++i) {
00540     Expr::iterator j = e2.begin();
00541     for (;  j != e2.end(); ++j) {
00542       sumExprs.push_back(canonMultMtermMterm((*i) * (*j)).getRHS());
00543     }
00544   }
00545   return canonCombineLikeTerms(sumExprs);
00546 }
00547 
00548 
00549 
00550 // The following produces a Theorem which is the result of multiplication
00551 // of two canonized mterms.  e = e1*e2
00552 Theorem
00553 ArithTheoremProducerOld::canonMultMtermMterm(const Expr& e)
00554 {
00555   if(CHECK_PROOFS) {
00556     CHECK_SOUND(isMult(e) && e.arity() == 2, 
00557     "canonMultMtermMterm: e = "+e.toString());
00558   }
00559   Proof pf;
00560   Expr rhs;
00561   const Expr& e1 = e[0];
00562   const Expr& e2 = e[1];
00563   string cmmm = "canon_mult_mterm_mterm";
00564 
00565   if (e1.isRational()) {
00566     // e1 is a Rational
00567     const Rational& c = e1.getRational();
00568     if (c == 0)
00569       return canonMultZero(e2);
00570     else if (c == 1)
00571       return canonMultOne(e2);
00572     else {
00573       switch (e2.getKind()) {
00574       case RATIONAL_EXPR :
00575         // rat * rat
00576         return canonMultConstConst(e1,e2);
00577         break;
00578         // TODO case of leaf
00579       case POW:
00580         // rat * (POW rat leaf)
00581         // nothing to simplify
00582         return d_theoryArith->reflexivityRule (e);
00583                 
00584         break;
00585       case MULT:
00586         rhs = canonMultConstMult(e1,e2);
00587         if(withProof()) pf = newPf(cmmm,e,rhs);
00588         return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00589         break;
00590       case PLUS:
00591         rhs = canonMultConstPlus(e1,e2);
00592         if(withProof()) pf = newPf(cmmm,e,rhs);
00593         return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00594         break;
00595       default:
00596         // TODO: I am going to assume that this is just a leaf
00597         // i.e., a variable or term from another theory
00598         return d_theoryArith->reflexivityRule(e);
00599         break;
00600       }
00601     }
00602   }
00603   else if (e1.getKind() == POW) {
00604     switch (e2.getKind()) {
00605     case RATIONAL_EXPR:
00606       // switch the order of the two arguments
00607       return canonMultMtermMterm(e2 * e1);
00608       break;
00609     case POW:
00610       rhs = canonMultPowPow(e1,e2);
00611       if(withProof()) pf = newPf(cmmm,e,rhs);
00612       return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
00613       break;
00614     case MULT:
00615       rhs = canonMultLeafOrPowMult(e1,e2);
00616       if(withProof()) pf = newPf(cmmm,e,rhs);
00617       return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00618       break;
00619     case PLUS:
00620       rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
00621       if(withProof()) pf = newPf(cmmm,e,rhs);
00622       return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);                          
00623       break;
00624     default:
00625       rhs = canonMultPowLeaf(e1,e2);
00626       if(withProof()) pf = newPf(cmmm,e,rhs);
00627       return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
00628       break;
00629     }
00630   }
00631   else if (e1.getKind() == MULT) {
00632     switch (e2.getKind()) {
00633     case RATIONAL_EXPR:
00634     case POW:
00635       // switch the order of the two arguments
00636       return canonMultMtermMterm(e2 * e1);
00637       break;
00638     case MULT:
00639       {
00640         // (Mult r m1 m2 ...) (Mult r' m1' m2' ...)
00641         Expr result = e2;
00642         Expr::iterator i = e1.begin();
00643         for (; i != e1.end(); ++i) {
00644           result = canonMultMtermMterm((*i) * result).getRHS();
00645         }
00646         if(withProof()) pf = newPf(cmmm,e,result);
00647         return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
00648       }
00649       break;
00650     case PLUS:
00651       rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
00652       if(withProof()) pf = newPf(cmmm,e,rhs);
00653       return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
00654       break;
00655     default:
00656       // leaf
00657       // switch the order of the two arguments
00658       return canonMultMtermMterm(e2 * e1);
00659       break;
00660     }
00661   }
00662   else if (e1.getKind() == PLUS) {
00663     switch (e2.getKind()) {
00664     case RATIONAL_EXPR:
00665     case POW:
00666     case MULT:
00667       // switch the order of the two arguments
00668       return canonMultMtermMterm(e2 * e1);
00669       break;
00670     case PLUS:
00671       rhs = canonMultPlusPlus(e1,e2);
00672       if(withProof()) pf = newPf(cmmm,e,rhs);
00673       return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00674       break;
00675     default:
00676       // leaf
00677       // switch the order of the two arguments
00678       return canonMultMtermMterm(e2 * e1);
00679       break;
00680     }
00681   }
00682   else {
00683     // leaf
00684     switch (e2.getKind()) {
00685     case RATIONAL_EXPR:
00686       // switch the order of the two arguments
00687       return canonMultMtermMterm(e2 * e1);
00688       break;
00689     case POW:
00690       rhs = canonMultPowLeaf(e2,e1);
00691       if(withProof()) pf = newPf(cmmm,e,rhs);
00692       return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00693       break;
00694     case MULT:
00695       rhs = canonMultLeafOrPowMult(e1,e2);;
00696       if(withProof()) pf = newPf(cmmm,e,rhs);
00697       return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00698       break;
00699     case PLUS:
00700       rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
00701       if(withProof()) pf = newPf(cmmm,e,rhs);
00702       return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00703       break;
00704     default:
00705       // leaf * leaf
00706       rhs = canonMultLeafLeaf(e1,e2);
00707       if(withProof()) pf = newPf(cmmm,e,rhs);
00708       return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00709       break;
00710     }
00711   }
00712   FatalAssert(false, "Unreachable");
00713   return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00714 }
00715 
00716 // (PLUS expr1 expr2 ...) where each expr is itself in canonic form
00717 Theorem
00718 ArithTheoremProducerOld::canonPlus(const Expr& e) 
00719 {
00720   Proof pf;
00721     
00722   if (withProof()) {
00723     pf = newPf("canon_plus", e);
00724   }
00725   DebugAssert(e.getKind() == PLUS, "");
00726 
00727   // First flatten the PLUS
00728 
00729   std::vector<Expr> sumKids;
00730   Expr::iterator i = e.begin();
00731   for(; i != e.end(); ++i) {
00732     if ((*i).getKind() != PLUS) {
00733       sumKids.push_back(*i);
00734     }
00735     else
00736       {
00737         Expr::iterator j = (*i).begin();
00738         for(; j != (*i).end(); ++j)
00739           sumKids.push_back(*j);
00740       }
00741   }
00742   Expr val = canonCombineLikeTerms(sumKids);
00743   if (withProof()) {
00744     pf = newPf("canon_plus", e, val);
00745   }    
00746   return newRWTheorem(e, val, Assumptions::emptyAssump(), pf);
00747 }
00748 
00749 // (MULT expr1 expr2 ...) where each expr is itself in canonic form
00750 Theorem
00751 ArithTheoremProducerOld::canonMult(const Expr& e) 
00752 {
00753   Proof pf;
00754   DebugAssert(e.getKind() == MULT && e.arity() > 1, "");
00755   Expr::iterator i = e.begin();
00756   Expr result = *i;
00757   ++i;
00758   for (; i != e.end(); ++i) {
00759     result = canonMultMtermMterm(result * (*i)).getRHS();
00760   }
00761   if (withProof()) {
00762     pf = newPf("canon_mult", e,result);
00763   }
00764   return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
00765 }
00766 
00767 
00768 Theorem
00769 ArithTheoremProducerOld::canonInvertConst(const Expr& e) 
00770 {
00771   if(CHECK_PROOFS)
00772     CHECK_SOUND(isRational(e), "expecting a rational: e = "+e.toString());
00773     
00774   Proof pf;
00775     
00776   if (withProof()) {
00777     pf = newPf("canon_invert_const", e);
00778   }
00779   const Rational& er = e.getRational();
00780   return newRWTheorem((rat(1)/e), rat(er==0? 0 : (1/er)), Assumptions::emptyAssump(), pf);
00781 }
00782 
00783 
00784 Theorem
00785 ArithTheoremProducerOld::canonInvertLeaf(const Expr& e) 
00786 {
00787   Proof pf;
00788     
00789   if (withProof()) {
00790     pf = newPf("canon_invert_leaf", e);
00791   }
00792   return newRWTheorem((rat(1)/e), powExpr(rat(-1), e), Assumptions::emptyAssump(), pf);
00793 }
00794 
00795 
00796 Theorem
00797 ArithTheoremProducerOld::canonInvertPow(const Expr& e) 
00798 {
00799   DebugAssert(e.getKind() == POW, "expecting a rational"+e[0].toString());
00800     
00801   Proof pf;
00802     
00803   if (withProof()) {
00804     pf = newPf("canon_invert_pow", e);
00805   }
00806   if (e[0].getRational() == -1)
00807     return newRWTheorem((rat(1)/e), e[1], Assumptions::emptyAssump(), pf);
00808   else
00809     return newRWTheorem((rat(1)/e), 
00810                         powExpr(rat(-e[0].getRational()), e), 
00811                         Assumptions::emptyAssump(), 
00812                         pf);
00813 }
00814 
00815 Theorem
00816 ArithTheoremProducerOld::canonInvertMult(const Expr& e) 
00817 {
00818   DebugAssert(e.getKind() == MULT, "expecting a rational"+e[0].toString());
00819 
00820   Proof pf;
00821     
00822   if (withProof()) {
00823     pf = newPf("canon_invert_mult", e);
00824   }
00825 
00826   DebugAssert(e.arity() > 1, "MULT should have arity > 1"+e.toString());
00827   Expr result = canonInvert(e[0]).getRHS();
00828   for (int i = 1; i < e.arity(); ++i) {
00829     result = 
00830       canonMultMtermMterm(result * canonInvert(e[i]).getRHS()).getRHS();
00831   }
00832   return newRWTheorem((rat(1)/e), result, Assumptions::emptyAssump(), pf);
00833 }
00834 
00835 
00836 // Given an expression e in Canonic form generate 1/e in canonic form
00837 // This function assumes that e is not a PLUS expression
00838 Theorem
00839 ArithTheoremProducerOld::canonInvert(const Expr& e) 
00840 {
00841   DebugAssert(e.getKind() != PLUS, 
00842               "Cannot do inverse on a PLUS"+e.toString());
00843   switch (e.getKind()) {
00844   case RATIONAL_EXPR:
00845     return canonInvertConst(e);
00846     break;
00847   case POW:
00848     return canonInvertPow(e);
00849     break;
00850   case MULT:
00851     return canonInvertMult(e);
00852     break;
00853   default:
00854     // leaf
00855     return canonInvertLeaf(e);
00856     break;
00857   }
00858 }
00859 
00860 
00861 Theorem ArithTheoremProducerOld::moveSumConstantRight(const Expr& e) {
00862     
00863   // Check soundness of the rule if necessary
00864   if (CHECK_PROOFS) {
00865     CHECK_SOUND(isIneq(e) || e.isEq(), "moveSumConstantRight: input must be Eq or Ineq: " + e.toString());
00866     CHECK_SOUND(isRational(e[0]) || isPlus(e[0]), "moveSumConstantRight: left side must be a canonised sum: " + e.toString());
00867     CHECK_SOUND(isRational(e[1]) && e[1].getRational() == 0, "moveSumConstantRight: right side must be 0: " + e.toString());
00868   }
00869   
00870   // The rational constant of the sum
00871   Rational r = 0;
00872   
00873   // The right hand side of the expression
00874   Expr right = e[0];
00875   
00876   // The vector of sum terms
00877   vector<Expr> sumTerms;
00878 
00879   // Get all the non rational children and 
00880   if (!right.isRational()) 
00881     for(Expr::iterator it = right.begin(); it != right.end(); it ++) {
00882       // If the term is rational then add the rational number to r 
00883       if ((*it).isRational()) r = r + (*it).getRational();
00884       // Otherwise just add the sumTerm to the sumTerms
00885       else sumTerms.push_back((*it));
00886     }   
00887     
00888   // Setup the new expression
00889   Expr transformed;
00890   if (sumTerms.size() > 1) 
00891     // If the number of summands is > 1 return the sum of them
00892     transformed = Expr(e.getKind(), plusExpr(sumTerms), rat(-r));
00893   else 
00894     // Otherwise return the one summand as itself
00895     transformed = Expr(e.getKind(), sumTerms[0], rat(-r));
00896     
00897 
00898   // If proof is needed set it up
00899   Proof pf;
00900   if (withProof()) pf = newPf("arithm_sum_constant_right", e); 
00901 
00902   // Retrun the theorem explaining the transformation
00903   return newRWTheorem(e, transformed, Assumptions::emptyAssump(), pf);  
00904 }
00905 
00906 Theorem
00907 ArithTheoremProducerOld::canonDivide(const Expr& e) 
00908 {
00909   DebugAssert(e.getKind() == DIVIDE, "Expecting Divide"+e.toString());
00910   Proof pf;
00911     
00912   if (withProof()) {
00913     pf = newPf("canon_invert_divide", e);
00914   }
00915 
00916   Theorem thm = newRWTheorem(e, e[0]*(canonInvert(e[1]).getRHS()), Assumptions::emptyAssump(), pf);
00917     
00918   return d_theoryArith->transitivityRule(thm, canonMult(thm.getRHS()));
00919 }
00920 
00921 
00922 // Rules for multiplication
00923 // t*c ==> c*t, takes constant c and term t
00924 Theorem 
00925 ArithTheoremProducerOld::canonMultTermConst(const Expr& c, const Expr& t) {
00926   Proof pf;
00927   if(CHECK_PROOFS) {
00928     CHECK_SOUND(isRational(c),
00929                 CLASS_NAME "::canonMultTermConst:\n  "
00930                 "c is not a constant: " + c.toString());
00931   }
00932   if(withProof()) pf = newPf("canon_mult_term_const", c, t);
00933   return newRWTheorem((t*c), (c*t), Assumptions::emptyAssump(), pf);
00934 }
00935 
00936 // Rules for multiplication
00937 // t1*t2 ==> Error, takes t1 and t2 where both are non-constants
00938 Theorem 
00939 ArithTheoremProducerOld::canonMultTerm1Term2(const Expr& t1, const Expr& t2) {
00940   // Proof pf;
00941   // if(withProof()) pf = newPf("canon_mult_term1_term2", t1, t2);
00942   if(CHECK_PROOFS) {
00943     CHECK_SOUND(false, "Fatal Error: We don't support multiplication"
00944                 "of two non constant terms at this time " 
00945                 + t1.toString() + " and " + t2.toString());
00946   }
00947   return Theorem();
00948 }
00949 
00950 // Rules for multiplication
00951 // 0*x = 0, takes x
00952 Theorem ArithTheoremProducerOld::canonMultZero(const Expr& e) {
00953   Proof pf;
00954   if(withProof()) pf = newPf("canon_mult_zero", e);
00955   return newRWTheorem((rat(0)*e), rat(0), Assumptions::emptyAssump(), pf);
00956 }
00957 
00958 // Rules for multiplication
00959 // 1*x ==> x, takes x
00960 Theorem ArithTheoremProducerOld::canonMultOne(const Expr& e) {
00961   Proof pf;
00962   if(withProof()) pf = newPf("canon_mult_one", e);
00963   return newRWTheorem((rat(1)*e), e, Assumptions::emptyAssump(), pf);
00964 }
00965 
00966 // Rules for multiplication
00967 // c1*c2 ==> c', takes constant c1*c2 
00968 Theorem 
00969 ArithTheoremProducerOld::canonMultConstConst(const Expr& c1, const Expr& c2) {
00970   Proof pf;
00971   if(CHECK_PROOFS) {
00972     CHECK_SOUND(isRational(c1),
00973                 CLASS_NAME "::canonMultConstConst:\n  "
00974                 "c1 is not a constant: " + c1.toString());
00975     CHECK_SOUND(isRational(c2),
00976                 CLASS_NAME "::canonMultConstConst:\n  "
00977                 "c2 is not a constant: " + c2.toString());
00978   }
00979   if(withProof()) pf = newPf("canon_mult_const_const", c1, c2);
00980   return 
00981     newRWTheorem((c1*c2), rat(c1.getRational()*c2.getRational()), Assumptions::emptyAssump(), pf);
00982 }
00983 
00984 // Rules for multiplication
00985 // c1*(c2*t) ==> c'*t, takes c1 and c2 and t
00986 Theorem 
00987 ArithTheoremProducerOld::canonMultConstTerm(const Expr& c1,
00988                                          const Expr& c2,const Expr& t) {
00989   Proof pf;
00990   if(CHECK_PROOFS) {
00991     CHECK_SOUND(isRational(c1),
00992                 CLASS_NAME "::canonMultConstTerm:\n  "
00993                 "c1 is not a constant: " + c1.toString());
00994     CHECK_SOUND(isRational(c2),
00995                 CLASS_NAME "::canonMultConstTerm:\n  "
00996                 "c2 is not a constant: " + c2.toString());
00997   }
00998   
00999   if(withProof()) pf = newPf("canon_mult_const_term", c1, c2, t);
01000   return 
01001     newRWTheorem(c1*(c2*t), rat(c1.getRational()*c2.getRational())*t, Assumptions::emptyAssump(), pf);
01002 }
01003 
01004 // Rules for multiplication
01005 // c1*(+ c2 v1 ...) ==> (+ c1c2 c1v1 ...), takes c1 and the sum
01006 Theorem 
01007 ArithTheoremProducerOld::canonMultConstSum(const Expr& c1, const Expr& sum) {
01008   Proof pf;
01009   std::vector<Expr> sumKids;
01010   
01011   if(CHECK_PROOFS) {
01012     CHECK_SOUND(isRational(c1),
01013                 CLASS_NAME "::canonMultConstTerm:\n  "
01014                 "c1 is not a constant: " + c1.toString());
01015     CHECK_SOUND(PLUS == sum.getKind(),
01016                 CLASS_NAME "::canonMultConstTerm:\n  "
01017                 "the kind must be a PLUS: " + sum.toString());
01018   }
01019   Expr::iterator i = sum.begin();
01020   for(; i != sum.end(); ++i)
01021     sumKids.push_back(c1*(*i));
01022   Expr ret = plusExpr(sumKids);
01023   if(withProof()) pf = newPf("canon_mult_const_sum", c1, sum, ret);
01024   return newRWTheorem((c1*sum),ret , Assumptions::emptyAssump(), pf);
01025 }
01026 
01027 
01028 // c^n = c' (compute the constant power expression)
01029 Theorem
01030 ArithTheoremProducerOld::canonPowConst(const Expr& e) {
01031   if(CHECK_PROOFS) {
01032     CHECK_SOUND(e.getKind() == POW && e.arity() == 2
01033     && e[0].isRational() && e[1].isRational(),
01034     "ArithTheoremProducerOld::canonPowConst("+e.toString()+")");
01035   }
01036   const Rational& p = e[0].getRational();
01037   const Rational& base = e[1].getRational();
01038   if(CHECK_PROOFS) {
01039     CHECK_SOUND(p.isInteger(),
01040     "ArithTheoremProducerOld::canonPowConst("+e.toString()+")");
01041   }
01042   Expr res;
01043   if (base == 0 && p < 0) {
01044     res = rat(0);
01045   }
01046   else res = rat(pow(p, base));
01047   Proof pf;
01048   if(withProof())
01049     pf = newPf("canon_pow_const", e);
01050   return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
01051 }
01052 
01053 
01054 // Rules for addition
01055 // flattens the input. accepts a PLUS expr
01056 Theorem 
01057 ArithTheoremProducerOld::canonFlattenSum(const Expr& e) {
01058   Proof pf;
01059   std::vector<Expr> sumKids;
01060   if(CHECK_PROOFS) {
01061     CHECK_SOUND(PLUS == e.getKind(),
01062                 CLASS_NAME "::canonFlattenSum:\n"
01063                 "input must be a PLUS:" + e.toString());
01064   }
01065 
01066   Expr::iterator i = e.begin();
01067   for(; i != e.end(); ++i){
01068     if (PLUS != (*i).getKind())
01069       sumKids.push_back(*i);
01070     else {
01071       Expr::iterator j = (*i).begin();
01072       for(; j != (*i).end(); ++j)
01073         sumKids.push_back(*j);
01074     }
01075   }
01076   Expr ret =  plusExpr(sumKids);
01077   if(withProof()) pf = newPf("canon_flatten_sum", e,ret);
01078   return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
01079 }
01080 
01081 // Rules for addition
01082 // combine like terms. accepts a flattened PLUS expr
01083 Theorem 
01084 ArithTheoremProducerOld::canonComboLikeTerms(const Expr& e) {
01085   Proof pf;
01086   std::vector<Expr> sumKids;
01087   ExprMap<Rational> sumHashMap;
01088   Rational constant = 0;
01089 
01090   if(CHECK_PROOFS) {
01091     Expr::iterator k = e.begin();
01092     for(; k != e.end(); ++k)
01093       CHECK_SOUND(!isPlus(*k),
01094                   CLASS_NAME "::canonComboLikeTerms:\n"
01095                   "input must be a flattened PLUS:" + k->toString());
01096   }
01097   Expr::iterator i = e.begin();
01098   for(; i != e.end(); ++i){
01099     if(i->isRational())
01100       constant = constant + i->getRational();
01101     else {
01102       if (!isMult(*i)) {
01103         if(0 == sumHashMap.count((*i)))
01104           sumHashMap[*i] = 1;
01105         else
01106           sumHashMap[*i] += 1;
01107       }
01108       else {
01109         if(0 == sumHashMap.count((*i)[1]))
01110           sumHashMap[(*i)[1]] = (*i)[0].getRational();
01111         else
01112           sumHashMap[(*i)[1]] = sumHashMap[(*i)[1]] + (*i)[0].getRational();
01113       }
01114     }
01115   }
01116 
01117   sumKids.push_back(rat(constant));
01118   ExprMap<Rational>::iterator j = sumHashMap.begin();
01119   for(; j != sumHashMap.end(); ++j) {
01120     if(0 == (*j).second)
01121       ;//do nothing
01122     else if (1 == (*j).second)
01123       sumKids.push_back((*j).first);
01124     else
01125       sumKids.push_back(rat((*j).second) * (*j).first);
01126   }
01127   
01128   //constant is same as sumKids[0].
01129   //corner cases: "0 + monomial" and "constant"(no monomials)
01130 
01131   Expr ret;
01132   if(2 == sumKids.size() && 0 == constant) ret = sumKids[1];
01133   else if (1 == sumKids.size()) ret = sumKids[0];
01134   else ret = plusExpr(sumKids);
01135 
01136   if(withProof()) pf = newPf("canon_combo_like_terms",e,ret);  
01137   return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
01138 }
01139 
01140 
01141 
01142 
01143 
01144 // e[0] kind e[1] <==> true when e[0] kind e[1],
01145 // false when e[0] !kind e[1], for constants only
01146 Theorem ArithTheoremProducerOld::constPredicate(const Expr& e) {
01147   if(CHECK_PROOFS) {
01148     CHECK_SOUND(e.arity() == 2 && isRational(e[0]) && isRational(e[1]),
01149                 CLASS_NAME "::constPredicate:\n  "
01150                 "non-const parameters: " + e.toString());
01151   }
01152   Proof pf;
01153   bool result(false);
01154   int kind = e.getKind();
01155   Rational r1 = e[0].getRational(), r2 = e[1].getRational();
01156   switch(kind) {
01157   case EQ:
01158     result = (r1 == r2)?true : false; 
01159     break;
01160   case LT:
01161     result = (r1 < r2)?true : false; 
01162     break;
01163   case LE:
01164     result = (r1 <= r2)?true : false; 
01165     break;
01166   case GT:
01167     result = (r1 > r2)?true : false; 
01168     break;
01169   case GE:
01170     result = (r1 >= r2)?true : false; 
01171     break;
01172   default:
01173     if(CHECK_PROOFS) {
01174       CHECK_SOUND(false,
01175                   "ArithTheoremProducerOld::constPredicate: wrong kind");
01176     }
01177     break;
01178   }
01179   Expr ret = (result) ? d_em->trueExpr() : d_em->falseExpr();
01180   if(withProof()) pf = newPf("const_predicate", e,ret);
01181   return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
01182 }
01183 
01184 // e[0] kind e[1] <==> 0 kind e[1] - e[0]
01185 Theorem ArithTheoremProducerOld::rightMinusLeft(const Expr& e)
01186 {
01187   Proof pf;
01188   int kind = e.getKind();
01189   if(CHECK_PROOFS) {
01190     CHECK_SOUND((EQ==kind) || 
01191                 (LT==kind) || 
01192                 (LE==kind) || 
01193                 (GE==kind) || 
01194                 (GT==kind),
01195                 "ArithTheoremProducerOld::rightMinusLeft: wrong kind");
01196   }
01197   if(withProof()) pf = newPf("right_minus_left",e);
01198   return newRWTheorem(e, Expr(e.getOp(), rat(0), e[1] - e[0]), Assumptions::emptyAssump(), pf);
01199 }
01200 
01201 
01202 // e[0] kind e[1] <==> 0 kind e[1] - e[0]
01203 Theorem ArithTheoremProducerOld::leftMinusRight(const Expr& e)
01204 {
01205   Proof pf;
01206   int kind = e.getKind();
01207   if(CHECK_PROOFS) {
01208     CHECK_SOUND((EQ==kind) || 
01209                 (LT==kind) || 
01210                 (LE==kind) || 
01211                 (GE==kind) || 
01212                 (GT==kind),
01213                 "ArithTheoremProducerOld::rightMinusLeft: wrong kind");
01214   }
01215   if(withProof()) pf = newPf("left_minus_right",e);
01216   return newRWTheorem(e, Expr(e.getOp(), e[0] - e[1], rat(0)), Assumptions::emptyAssump(), pf);
01217 }
01218 
01219 
01220 // x kind y <==> x + z kind y + z
01221 Theorem ArithTheoremProducerOld::plusPredicate(const Expr& x, 
01222                                       const Expr& y,
01223                                       const Expr& z, int kind) {
01224   if(CHECK_PROOFS) {
01225     CHECK_SOUND((EQ==kind) || 
01226                 (LT==kind) || 
01227                 (LE==kind) || 
01228                 (GE==kind) || 
01229                 (GT==kind),
01230                 "ArithTheoremProducerOld::plusPredicate: wrong kind");
01231   }
01232   Proof pf;
01233   Expr left = Expr(kind, x, y);
01234   Expr right = Expr(kind, x + z, y + z);
01235   if(withProof()) pf = newPf("plus_predicate",left,right);
01236   return newRWTheorem(left, right, Assumptions::emptyAssump(), pf);
01237 }
01238 
01239 // x = y <==> x * z = y * z
01240 Theorem ArithTheoremProducerOld::multEqn(const Expr& x, 
01241                                       const Expr& y,
01242                                       const Expr& z) {
01243   Proof pf;
01244   if(CHECK_PROOFS)
01245     CHECK_SOUND(z.isRational() && z.getRational() != 0,
01246     "ArithTheoremProducerOld::multEqn(): multiplying equation by 0");
01247   if(withProof()) pf = newPf("mult_eqn", x, y, z);
01248   return newRWTheorem(x.eqExpr(y), (x * z).eqExpr(y * z), Assumptions::emptyAssump(), pf);
01249 }
01250 
01251 
01252 // if z is +ve, return e[0] LT|LE|GT|GE e[1] <==> e[0]*z LT|LE|GT|GE e[1]*z
01253 // if z is -ve, return e[0] LT|LE|GT|GE e[1] <==> e[1]*z LT|LE|GT|GE e[0]*z
01254 Theorem ArithTheoremProducerOld::multIneqn(const Expr& e, const Expr& z)
01255 {
01256   int kind = e.getKind();
01257 
01258   if(CHECK_PROOFS) {
01259     CHECK_SOUND((LT==kind) || 
01260                 (LE==kind) || 
01261                 (GE==kind) || 
01262                 (GT==kind),
01263                 "ArithTheoremProducerOld::multIneqn: wrong kind");    
01264     CHECK_SOUND(z.isRational() && z.getRational() != 0,
01265                 "ArithTheoremProducerOld::multIneqn: "
01266     "z must be non-zero rational: " + z.toString());
01267   }
01268   Op op(e.getOp());
01269   Proof pf;
01270 
01271   Expr ret;
01272   if(0 < z.getRational())
01273     ret = Expr(op, e[0]*z, e[1]*z);
01274   else
01275     ret = Expr(op, e[1]*z, e[0]*z);
01276   if(withProof()) pf = newPf("mult_ineqn", e, ret);  
01277   return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
01278 }
01279 
01280 
01281 Theorem ArithTheoremProducerOld::eqToIneq(const Expr& e) {
01282   
01283     // Check soundness of the rule if necessary
01284   if (CHECK_PROOFS)
01285     CHECK_SOUND(e.isEq(), "eqToIneq: input must be an equality: " + e.toString());
01286     
01287     // The proof object we will use 
01288     Proof pf;
01289 
01290   // The parts of the equality x = y
01291     const Expr& x = e[0];
01292     const Expr& y = e[1];
01293 
01294   // Setup the proof if needed
01295     if (withProof())
01296       pf = newPf("eqToIneq", e);
01297       
01298     // Retrun the theorem explaining the transformation
01299   return newRWTheorem(e, leExpr(x,y).andExpr(geExpr(x,y)), Assumptions::emptyAssump(), pf);
01300 }
01301 
01302 // "op1 GE|GT op2" <==> op2 LE|LT op1
01303 Theorem ArithTheoremProducerOld::flipInequality(const Expr& e)
01304 {
01305   Proof pf;
01306   if(CHECK_PROOFS) {
01307     CHECK_SOUND(isGT(e) || isGE(e),
01308                 "ArithTheoremProducerOld::flipInequality: wrong kind: " + 
01309                 e.toString());
01310   }
01311   
01312   int kind = isGE(e) ? LE : LT; 
01313   Expr ret =  Expr(kind, e[1], e[0]);
01314   if(withProof()) pf = newPf("flip_inequality", e,ret);
01315   return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
01316 }
01317 
01318 
01319 // NOT (op1 LT op2)  <==> (op1 GE op2)
01320 // NOT (op1 LE op2)  <==> (op1 GT op2)
01321 // NOT (op1 GT op2)  <==> (op1 LE op2)
01322 // NOT (op1 GE op2)  <==> (op1 LT op2)
01323 Theorem ArithTheoremProducerOld::negatedInequality(const Expr& e)
01324 {
01325   const Expr& ineq = e[0];
01326   if(CHECK_PROOFS) {
01327     CHECK_SOUND(e.isNot(),
01328                 "ArithTheoremProducerOld::negatedInequality: wrong kind: " +
01329                 e.toString());
01330     CHECK_SOUND(isIneq(ineq),
01331                 "ArithTheoremProducerOld::negatedInequality: wrong kind: " +
01332                 (ineq).toString());
01333   }
01334   Proof pf;
01335   if(withProof()) pf = newPf("negated_inequality", e);
01336 
01337   int kind;
01338   // NOT (op1 LT op2)  <==> (op1 GE op2)
01339   // NOT (op1 LE op2)  <==> (op1 GT op2)
01340   // NOT (op1 GT op2)  <==> (op1 LE op2)
01341   // NOT (op1 GE op2)  <==> (op1 LT op2)
01342   kind = 
01343     isLT(ineq) ? GE : 
01344     isLE(ineq) ? GT : 
01345     isGT(ineq) ? LE : 
01346     LT;
01347   return newRWTheorem(e, Expr(kind, ineq[0], ineq[1]), Assumptions::emptyAssump(), pf);
01348 }
01349 
01350 //takes two ineqs "|- alpha LT|LE t" and "|- t LT|LE beta"
01351 //and returns "|- alpha LT|LE beta"
01352 Theorem ArithTheoremProducerOld::realShadow(const Theorem& alphaLTt, 
01353                                          const Theorem& tLTbeta)
01354 {
01355   const Expr& expr1 = alphaLTt.getExpr();
01356   const Expr& expr2 = tLTbeta.getExpr();
01357   if(CHECK_PROOFS) {
01358     CHECK_SOUND((isLE(expr1) || isLT(expr1)) &&
01359                 (isLE(expr2) || isLT(expr2)),
01360                 "ArithTheoremProducerOld::realShadow: Wrong Kind: " + 
01361                 alphaLTt.toString() +  tLTbeta.toString());
01362     
01363     CHECK_SOUND(expr1[1] == expr2[0], 
01364                 "ArithTheoremProducerOld::realShadow:" 
01365                 " t must be same for both inputs: " +
01366                 expr1[1].toString() + " , " + expr2[0].toString());
01367   }
01368   Assumptions a(alphaLTt, tLTbeta);
01369   int firstKind = expr1.getKind();
01370   int secondKind = expr2.getKind();
01371   int kind = (firstKind == secondKind) ? firstKind : LT;
01372   Proof pf; 
01373   if(withProof()) {
01374     vector<Proof> pfs;
01375     pfs.push_back(alphaLTt.getProof());
01376     pfs.push_back(tLTbeta.getProof());
01377     pf = newPf("real_shadow",expr1, expr2, pfs);
01378   }
01379   return newTheorem(Expr(kind, expr1[0], expr2[1]), a, pf); 
01380 }
01381 
01382 //! alpha <= t <= alpha ==> t = alpha
01383 
01384 /*! takes two ineqs "|- alpha LE t" and "|- t LE alpha"
01385   and returns "|- t = alpha"
01386 */
01387 Theorem ArithTheoremProducerOld::realShadowEq(const Theorem& alphaLEt, 
01388                                            const Theorem& tLEalpha)
01389 {
01390   const Expr& expr1 = alphaLEt.getExpr();
01391   const Expr& expr2 = tLEalpha.getExpr();
01392   if(CHECK_PROOFS) {
01393     CHECK_SOUND(isLE(expr1) && isLE(expr2),
01394                 "ArithTheoremProducerOld::realShadowLTLE: Wrong Kind: " + 
01395                 alphaLEt.toString() +  tLEalpha.toString());
01396     
01397     CHECK_SOUND(expr1[1] == expr2[0], 
01398                 "ArithTheoremProducerOld::realShadowLTLE:" 
01399                 " t must be same for both inputs: " +
01400                 alphaLEt.toString() + " , " + tLEalpha.toString());
01401 
01402     CHECK_SOUND(expr1[0] == expr2[1], 
01403                 "ArithTheoremProducerOld::realShadowLTLE:" 
01404                 " alpha must be same for both inputs: " +
01405                 alphaLEt.toString() + " , " + tLEalpha.toString());
01406   }
01407   Assumptions a(alphaLEt, tLEalpha);
01408   Proof pf;
01409   if(withProof()) {
01410     vector<Proof> pfs;
01411     pfs.push_back(alphaLEt.getProof());
01412     pfs.push_back(tLEalpha.getProof());
01413     pf = newPf("real_shadow_eq", alphaLEt.getExpr(), tLEalpha.getExpr(), pfs);
01414   }
01415   return newRWTheorem(expr1[0], expr1[1], a, pf);
01416 }
01417 
01418 Theorem 
01419 ArithTheoremProducerOld::finiteInterval(const Theorem& aLEt,
01420              const Theorem& tLEac,
01421              const Theorem& isInta,
01422              const Theorem& isIntt) {
01423   const Expr& e1 = aLEt.getExpr();
01424   const Expr& e2 = tLEac.getExpr();
01425   if(CHECK_PROOFS) {
01426     CHECK_SOUND(isLE(e1) && isLE(e2),
01427     "ArithTheoremProducerOld::finiteInterval:\n e1 = "
01428     +e1.toString()+"\n e2 = "+e2.toString());
01429     // term 't' is the same in both inequalities
01430     CHECK_SOUND(e1[1] == e2[0],
01431     "ArithTheoremProducerOld::finiteInterval:\n e1 = "
01432     +e1.toString()+"\n e2 = "+e2.toString());
01433     // RHS in e2 is (a+c)
01434     CHECK_SOUND(isPlus(e2[1]) && e2[1].arity() == 2,
01435     "ArithTheoremProducerOld::finiteInterval:\n e1 = "
01436     +e1.toString()+"\n e2 = "+e2.toString());
01437     // term 'a' in LHS of e1 and RHS of e2 is the same
01438     CHECK_SOUND(e1[0] == e2[1][0],
01439     "ArithTheoremProducerOld::finiteInterval:\n e1 = "
01440     +e1.toString()+"\n e2 = "+e2.toString());
01441     // 'c' in the RHS of e2 is a positive integer constant
01442     CHECK_SOUND(e2[1][1].isRational() && e2[1][1].getRational().isInteger()
01443     && e2[1][1].getRational() >= 1,
01444     "ArithTheoremProducerOld::finiteInterval:\n e1 = "
01445     +e1.toString()+"\n e2 = "+e2.toString());
01446     // Integrality constraints
01447     const Expr& isIntaExpr = isInta.getExpr();
01448     const Expr& isInttExpr = isIntt.getExpr();
01449     CHECK_SOUND(isIntPred(isIntaExpr) && isIntaExpr[0] == e1[0],
01450     "Wrong integrality constraint:\n e1 = "
01451     +e1.toString()+"\n isInta = "+isIntaExpr.toString());
01452     CHECK_SOUND(isIntPred(isInttExpr) && isInttExpr[0] == e1[1],
01453     "Wrong integrality constraint:\n e1 = "
01454     +e1.toString()+"\n isIntt = "+isInttExpr.toString());
01455   }
01456   vector<Theorem> thms;
01457   thms.push_back(aLEt);
01458   thms.push_back(tLEac);
01459   thms.push_back(isInta);
01460   thms.push_back(isIntt);
01461   Assumptions a(thms);
01462   Proof pf;
01463   if(withProof()) {
01464     vector<Expr> es;
01465     vector<Proof> pfs;
01466     es.push_back(e1);
01467     es.push_back(e2);
01468     es.push_back(isInta.getExpr());
01469     es.push_back(isIntt.getExpr());
01470     pfs.push_back(aLEt.getProof());
01471     pfs.push_back(tLEac.getProof());
01472     pfs.push_back(isInta.getProof());
01473     pfs.push_back(isIntt.getProof());
01474     pf = newPf("finite_interval", es, pfs);
01475   }
01476   // Construct GRAY_SHADOW(t, a, 0, c)
01477   Expr g(grayShadow(e1[1], e1[0], 0, e2[1][1].getRational()));
01478   return newTheorem(g, a, pf);
01479 }
01480 
01481 
01482 // Dark & Gray shadows when a <= b
01483 Theorem ArithTheoremProducerOld::darkGrayShadow2ab(const Theorem& betaLEbx, 
01484             const Theorem& axLEalpha,
01485             const Theorem& isIntAlpha,
01486             const Theorem& isIntBeta,
01487             const Theorem& isIntx) {
01488   const Expr& expr1 = betaLEbx.getExpr();
01489   const Expr& expr2 = axLEalpha.getExpr();
01490   const Expr& isIntAlphaExpr = isIntAlpha.getExpr();
01491   const Expr& isIntBetaExpr = isIntBeta.getExpr();
01492   const Expr& isIntxExpr = isIntx.getExpr();
01493 
01494   if(CHECK_PROOFS) {
01495     CHECK_SOUND(isLE(expr1) && isLE(expr2),
01496                 "ArithTheoremProducerOld::darkGrayShadow2ab: Wrong Kind: " + 
01497                 betaLEbx.toString() +  axLEalpha.toString());
01498   }
01499 
01500   const Expr& beta = expr1[0];
01501   const Expr& bx = expr1[1];
01502   const Expr& ax = expr2[0];
01503   const Expr& alpha = expr2[1];
01504   Rational a = isMult(ax)? ax[0].getRational() : 1;
01505   Rational b = isMult(bx)? bx[0].getRational() : 1;
01506   const Expr& x = isMult(ax)? ax[1] : ax;
01507 
01508   if(CHECK_PROOFS) {
01509     // Integrality constraints
01510     CHECK_SOUND(isIntPred(isIntAlphaExpr) && isIntAlphaExpr[0] == alpha,
01511     "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01512     "wrong integrality constraint:\n alpha = "
01513     +alpha.toString()+"\n isIntAlpha = "
01514     +isIntAlphaExpr.toString());
01515     CHECK_SOUND(isIntPred(isIntBetaExpr) && isIntBetaExpr[0] == beta,
01516     "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01517     "wrong integrality constraint:\n beta = "
01518     +beta.toString()+"\n isIntBeta = "
01519     +isIntBetaExpr.toString());
01520     CHECK_SOUND(isIntPred(isIntxExpr) && isIntxExpr[0] == x,
01521     "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01522     "wrong integrality constraint:\n x = "
01523     +x.toString()+"\n isIntx = "
01524     +isIntxExpr.toString());
01525     // Expressions ax and bx should match on x
01526     CHECK_SOUND(!isMult(ax) || ax.arity() == 2,
01527     "ArithTheoremProducerOld::darkGrayShadow2ab:\n ax<=alpha: " +
01528                 axLEalpha.toString());
01529     CHECK_SOUND(!isMult(bx) || (bx.arity() == 2 && bx[1] == x),
01530     "ArithTheoremProducerOld::darkGrayShadow2ab:\n beta<=bx: "
01531     +betaLEbx.toString()
01532     +"\n ax<=alpha: "+ axLEalpha.toString());
01533     CHECK_SOUND(1 <= a && a <= b && 2 <= b,
01534     "ArithTheoremProducerOld::darkGrayShadow2ab:\n beta<=bx: "
01535     +betaLEbx.toString()
01536     +"\n ax<=alpha: "+ axLEalpha.toString());
01537   }
01538   vector<Theorem> thms;
01539   thms.push_back(betaLEbx);
01540   thms.push_back(axLEalpha);
01541   thms.push_back(isIntAlpha);
01542   thms.push_back(isIntBeta);
01543   thms.push_back(isIntx);
01544   Assumptions A(thms);
01545   Proof pf;
01546   if(withProof()) {
01547     vector<Proof> pfs;
01548     pfs.push_back(betaLEbx.getProof());
01549     pfs.push_back(axLEalpha.getProof());
01550     pfs.push_back(isIntAlpha.getProof());
01551     pfs.push_back(isIntBeta.getProof());
01552     pfs.push_back(isIntx.getProof());
01553     
01554     pf = newPf("dark_grayshadow_2ab", expr1, expr2, pfs);
01555   }
01556   
01557   Expr bAlpha = multExpr(rat(b), alpha);
01558   Expr aBeta = multExpr(rat(a), beta);
01559   Expr t = minusExpr(bAlpha, aBeta);
01560   Expr d = darkShadow(rat(a*b-1), t);
01561   Expr g = grayShadow(ax, alpha, -a+1, 0);
01562   return newTheorem((d || g) && (!d || !g), A, pf);
01563 }
01564 
01565 // Dark & Gray shadows when b <= a
01566 Theorem ArithTheoremProducerOld::darkGrayShadow2ba(const Theorem& betaLEbx, 
01567             const Theorem& axLEalpha,
01568             const Theorem& isIntAlpha,
01569             const Theorem& isIntBeta,
01570             const Theorem& isIntx) {
01571   const Expr& expr1 = betaLEbx.getExpr();
01572   const Expr& expr2 = axLEalpha.getExpr();
01573   const Expr& isIntAlphaExpr = isIntAlpha.getExpr();
01574   const Expr& isIntBetaExpr = isIntBeta.getExpr();
01575   const Expr& isIntxExpr = isIntx.getExpr();
01576 
01577   if(CHECK_PROOFS) {
01578     CHECK_SOUND(isLE(expr1) && isLE(expr2),
01579                 "ArithTheoremProducerOld::darkGrayShadow2ba: Wrong Kind: " + 
01580                 betaLEbx.toString() +  axLEalpha.toString());
01581   }
01582 
01583   const Expr& beta = expr1[0];
01584   const Expr& bx = expr1[1];
01585   const Expr& ax = expr2[0];
01586   const Expr& alpha = expr2[1];
01587   Rational a = isMult(ax)? ax[0].getRational() : 1;
01588   Rational b = isMult(bx)? bx[0].getRational() : 1;
01589   const Expr& x = isMult(ax)? ax[1] : ax;
01590 
01591   if(CHECK_PROOFS) {
01592     // Integrality constraints
01593     CHECK_SOUND(isIntPred(isIntAlphaExpr) && isIntAlphaExpr[0] == alpha,
01594     "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01595     "wrong integrality constraint:\n alpha = "
01596     +alpha.toString()+"\n isIntAlpha = "
01597     +isIntAlphaExpr.toString());
01598     CHECK_SOUND(isIntPred(isIntBetaExpr) && isIntBetaExpr[0] == beta,
01599     "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01600     "wrong integrality constraint:\n beta = "
01601     +beta.toString()+"\n isIntBeta = "
01602     +isIntBetaExpr.toString());
01603     CHECK_SOUND(isIntPred(isIntxExpr) && isIntxExpr[0] == x,
01604     "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01605     "wrong integrality constraint:\n x = "
01606     +x.toString()+"\n isIntx = "
01607     +isIntxExpr.toString());
01608     // Expressions ax and bx should match on x
01609     CHECK_SOUND(!isMult(ax) || ax.arity() == 2,
01610     "ArithTheoremProducerOld::darkGrayShadow2ba:\n ax<=alpha: " +
01611                 axLEalpha.toString());
01612     CHECK_SOUND(!isMult(bx) || (bx.arity() == 2 && bx[1] == x),
01613     "ArithTheoremProducerOld::darkGrayShadow2ba:\n beta<=bx: "
01614     +betaLEbx.toString()
01615     +"\n ax<=alpha: "+ axLEalpha.toString());
01616     CHECK_SOUND(1 <= b && b <= a && 2 <= a,
01617     "ArithTheoremProducerOld::darkGrayShadow2ba:\n beta<=bx: "
01618     +betaLEbx.toString()
01619     +"\n ax<=alpha: "+ axLEalpha.toString());
01620   }
01621   vector<Theorem> thms;
01622   thms.push_back(betaLEbx);
01623   thms.push_back(axLEalpha);
01624   thms.push_back(isIntAlpha);
01625   thms.push_back(isIntBeta);
01626   thms.push_back(isIntx);
01627   Assumptions A(thms);
01628   Proof pf;
01629   if(withProof()) {
01630     vector<Proof> pfs;
01631     pfs.push_back(betaLEbx.getProof());
01632     pfs.push_back(axLEalpha.getProof());
01633     pfs.push_back(isIntAlpha.getProof());
01634     pfs.push_back(isIntBeta.getProof());
01635     pfs.push_back(isIntx.getProof());
01636     
01637     pf = newPf("dark_grayshadow_2ba", betaLEbx.getExpr(),
01638          axLEalpha.getExpr(), pfs);
01639   }
01640   
01641   Expr bAlpha = multExpr(rat(b), alpha);
01642   Expr aBeta = multExpr(rat(a), beta);
01643   Expr t = minusExpr(bAlpha, aBeta);
01644   Expr d = darkShadow(rat(a*b-1), t);
01645   Expr g = grayShadow(bx, beta, 0, b-1);
01646   return newTheorem((d || g) && (!d || !g), A, pf);
01647 }
01648 
01649 /*! takes a dark shadow and expands it into an inequality.
01650 */
01651 Theorem ArithTheoremProducerOld::expandDarkShadow(const Theorem& darkShadow) {
01652   const Expr& theShadow = darkShadow.getExpr();
01653   if(CHECK_PROOFS){
01654     CHECK_SOUND(isDarkShadow(theShadow),
01655     "ArithTheoremProducerOld::expandDarkShadow: not DARK_SHADOW: " +
01656     theShadow.toString());
01657   }
01658   Proof pf;
01659   if(withProof())
01660     pf = newPf("expand_dark_shadow", theShadow, darkShadow.getProof());
01661   return newTheorem(leExpr(theShadow[0], theShadow[1]), darkShadow.getAssumptionsRef(), pf);
01662 }
01663 
01664 
01665 // takes a grayShadow (c1==c2) and expands it into an equality
01666 Theorem ArithTheoremProducerOld::expandGrayShadow0(const Theorem& grayShadow) {
01667   const Expr& theShadow = grayShadow.getExpr();
01668   if(CHECK_PROOFS) {
01669     CHECK_SOUND(isGrayShadow(theShadow),
01670     "ArithTheoremProducerOld::expandGrayShadowConst0:"
01671     " not GRAY_SHADOW: " +
01672     theShadow.toString());
01673     CHECK_SOUND(theShadow[2] == theShadow[3],
01674     "ArithTheoremProducerOld::expandGrayShadow0: c1!=c2: " +
01675     theShadow.toString());
01676   }
01677   Proof pf;
01678   if(withProof()) pf = newPf("expand_gray_shadowconst0", theShadow,
01679            grayShadow.getProof());
01680   const Expr& v = theShadow[0];
01681   const Expr& e = theShadow[1];
01682   return newRWTheorem(v, e + theShadow[2], grayShadow.getAssumptionsRef(), pf);
01683 }
01684 
01685 
01686 // G ==> (G1 or G2) and (!G1 or !G2),
01687 // where G  = G(x, e, c1, c2),
01688 //       G1 = G(x,e,c1,c)
01689 //       G2 = G(x,e,c+1,c2),
01690 // and    c = floor((c1+c2)/2)
01691 Theorem ArithTheoremProducerOld::splitGrayShadow(const Theorem& gThm) {
01692   const Expr& theShadow = gThm.getExpr();
01693   if(CHECK_PROOFS) {
01694     CHECK_SOUND(isGrayShadow(theShadow),
01695     "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
01696     theShadow.toString());
01697   }
01698 
01699   const Rational& c1 = theShadow[2].getRational();
01700   const Rational& c2 = theShadow[3].getRational();
01701 
01702   if(CHECK_PROOFS) {
01703     CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
01704     "ArithTheoremProducerOld::expandGrayShadow: " +
01705     theShadow.toString());
01706   }
01707 
01708   const Expr& v = theShadow[0];
01709   const Expr& e = theShadow[1];
01710 
01711   Proof pf;
01712   if(withProof())
01713     pf = newPf("expand_gray_shadow", theShadow, gThm.getProof());
01714   Rational c(floor((c1+c2) / 2));
01715   Expr g1(grayShadow(v, e, c1, c));
01716   Expr g2(grayShadow(v, e, c+1, c2));
01717   return newTheorem((g1 || g2) && (!g1 || !g2), gThm.getAssumptionsRef(), pf);
01718 }
01719 
01720 
01721 Theorem ArithTheoremProducerOld::expandGrayShadow(const Theorem& gThm) {
01722   const Expr& theShadow = gThm.getExpr();
01723   if(CHECK_PROOFS) {
01724     CHECK_SOUND(isGrayShadow(theShadow),
01725     "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
01726     theShadow.toString());
01727   }
01728 
01729   const Rational& c1 = theShadow[2].getRational();
01730   const Rational& c2 = theShadow[3].getRational();
01731 
01732   if(CHECK_PROOFS) {
01733     CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
01734     "ArithTheoremProducerOld::expandGrayShadow: " +
01735     theShadow.toString());
01736   }
01737 
01738   const Expr& v = theShadow[0];
01739   const Expr& e = theShadow[1];
01740 
01741   Proof pf;
01742   if(withProof())
01743     pf = newPf("expand_gray_shadow", theShadow, gThm.getProof());
01744   Expr ineq1(leExpr(e+rat(c1), v));
01745   Expr ineq2(leExpr(v, e+rat(c2)));
01746   return newTheorem(ineq1 && ineq2, gThm.getAssumptionsRef(), pf);
01747 }
01748 
01749 
01750 // Expanding GRAY_SHADOW(a*x, c, b), where c is a constant
01751 Theorem
01752 ArithTheoremProducerOld::expandGrayShadowConst(const Theorem& gThm) {
01753   const Expr& theShadow = gThm.getExpr();
01754   const Expr& ax = theShadow[0];
01755   const Expr& cExpr = theShadow[1];
01756   const Expr& bExpr = theShadow[2];
01757 
01758   if(CHECK_PROOFS) {
01759     CHECK_SOUND(!isMult(ax) || ax[0].isRational(),
01760     "ArithTheoremProducerOld::expandGrayShadowConst: "
01761     "'a' in a*x is not a const: " +theShadow.toString());
01762   }
01763 
01764   Rational a = isMult(ax)? ax[0].getRational() : 1;
01765 
01766   if(CHECK_PROOFS) {
01767     CHECK_SOUND(isGrayShadow(theShadow),
01768     "ArithTheoremProducerOld::expandGrayShadowConst: "
01769     "not a GRAY_SHADOW: " +theShadow.toString());
01770     CHECK_SOUND(a.isInteger() && a >= 1,
01771     "ArithTheoremProducerOld::expandGrayShadowConst: "
01772     "'a' is not integer: " +theShadow.toString());
01773     CHECK_SOUND(cExpr.isRational(),
01774     "ArithTheoremProducerOld::expandGrayShadowConst: "
01775     "'c' is not rational" +theShadow.toString());
01776     CHECK_SOUND(bExpr.isRational() && bExpr.getRational().isInteger(),
01777     "ArithTheoremProducerOld::expandGrayShadowConst: b not integer: "
01778     +theShadow.toString());
01779   }
01780 
01781   const Rational& b = bExpr.getRational();
01782   const Rational& c = cExpr.getRational();
01783   Rational j = constRHSGrayShadow(c,b,a);
01784   // Compute sign(b)*j(c,b,a)
01785   Rational signB = (b>0)? 1 : -1;
01786   // |b| (absolute value of b)
01787   Rational bAbs = abs(b);
01788 
01789   const Assumptions& assump(gThm.getAssumptionsRef());
01790   Proof pf;
01791   Theorem conc;  // Conclusion of the rule
01792 
01793   if(bAbs < j) {
01794     if(withProof())
01795       pf = newPf("expand_gray_shadow_const_0", theShadow,
01796      gThm.getProof());
01797     conc = newTheorem(d_em->falseExpr(), assump, pf);
01798   } else if(bAbs < a+j) {
01799     if(withProof())
01800       pf = newPf("expand_gray_shadow_const_1", theShadow,
01801      gThm.getProof());
01802     conc = newRWTheorem(ax, rat(c+b-signB*j), assump, pf);
01803   } else {
01804     if(withProof())
01805       pf = newPf("expand_gray_shadow_const", theShadow,
01806      gThm.getProof());
01807     Expr newGrayShadow(Expr(GRAY_SHADOW, ax, cExpr, rat(b-signB*(a+j))));
01808     conc = newTheorem(ax.eqExpr(rat(c+b-signB*j)).orExpr(newGrayShadow),
01809           assump, pf);
01810   }
01811 
01812   return conc;
01813 }
01814 
01815 
01816 Theorem
01817 ArithTheoremProducerOld::grayShadowConst(const Theorem& gThm) {
01818   const Expr& g = gThm.getExpr();
01819   bool checkProofs(CHECK_PROOFS);
01820   if(checkProofs) {
01821     CHECK_SOUND(isGrayShadow(g), "ArithTheoremProducerOld::grayShadowConst("
01822     +g.toString()+")");
01823   }
01824 
01825   const Expr& ax = g[0];
01826   const Expr& e = g[1];
01827   const Rational& c1 = g[2].getRational();
01828   const Rational& c2 = g[3].getRational();
01829   Expr aExpr, x;
01830   d_theoryArith->separateMonomial(ax, aExpr, x);
01831 
01832   if(checkProofs) {
01833     CHECK_SOUND(e.isRational() && e.getRational().isInteger(),
01834     "ArithTheoremProducerOld::grayShadowConst("+g.toString()+")");
01835     CHECK_SOUND(aExpr.isRational(),
01836     "ArithTheoremProducerOld::grayShadowConst("+g.toString()+")");
01837   }
01838 
01839   const Rational& a = aExpr.getRational();
01840   const Rational& c = e.getRational();
01841 
01842   if(checkProofs) {
01843     CHECK_SOUND(a.isInteger() && a >= 2,
01844     "ArithTheoremProducerOld::grayShadowConst("+g.toString()+")");
01845   }
01846 
01847   Rational newC1 = ceil((c1+c)/a), newC2 = floor((c2+c)/a);
01848   Expr newG((newC1 > newC2)? d_em->falseExpr()
01849       : grayShadow(x, rat(0), newC1, newC2));
01850   Proof pf;
01851   if(withProof())
01852     pf = newPf("gray_shadow_const", g, gThm.getProof());
01853   return newTheorem(newG, gThm.getAssumptionsRef(), pf);
01854 }
01855 
01856 
01857 Rational ArithTheoremProducerOld::constRHSGrayShadow(const Rational& c,
01858               const Rational& b,
01859               const Rational& a) {
01860   DebugAssert(c.isInteger() &&
01861         b.isInteger() &&
01862         a.isInteger() &&
01863         b != 0,
01864         "ArithTheoremProducerOld::constRHSGrayShadow: a, b, c must be ints");
01865   if (b > 0)
01866     return mod(c+b, a);
01867   else
01868     return mod(a-(c+b), a);
01869 }
01870 
01871 /*! Takes a Theorem(\\alpha < \\beta) and returns 
01872  *  Theorem(\\alpha < \\beta <==> \\alpha <= \\beta -1)
01873  * where \\alpha and \\beta are integer expressions
01874  */
01875 Theorem ArithTheoremProducerOld::lessThanToLE(const Theorem& less,
01876              const Theorem& isIntLHS,
01877              const Theorem& isIntRHS,
01878              bool changeRight) {
01879   const Expr& ineq = less.getExpr();
01880   const Expr& isIntLHSexpr = isIntLHS.getExpr();
01881   const Expr& isIntRHSexpr = isIntRHS.getExpr();
01882   
01883   if(CHECK_PROOFS) {
01884     CHECK_SOUND(isLT(ineq),
01885     "ArithTheoremProducerOld::LTtoLE: ineq must be <");
01886     // Integrality check
01887     CHECK_SOUND(isIntPred(isIntLHSexpr) && isIntLHSexpr[0] == ineq[0],
01888     "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
01889     " ineq = "+ineq.toString()+"\n isIntLHS = "
01890     +isIntLHSexpr.toString());
01891     CHECK_SOUND(isIntPred(isIntRHSexpr) && isIntRHSexpr[0] == ineq[1],
01892     "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
01893     " ineq = "+ineq.toString()+"\n isIntRHS = "
01894     +isIntRHSexpr.toString());
01895   }
01896   vector<Theorem> thms;
01897   thms.push_back(less);
01898   thms.push_back(isIntLHS);
01899   thms.push_back(isIntRHS);
01900   Assumptions a(thms);
01901   Proof pf;
01902   if(withProof()) {
01903     vector<Proof> pfs;
01904     pfs.push_back(less.getProof());
01905     pfs.push_back(isIntLHS.getProof());
01906     pfs.push_back(isIntRHS.getProof());
01907     pf = newPf(changeRight? "lessThan_To_LE_rhs" : "lessThan_To_LE_lhs",
01908          ineq, pfs);
01909   }
01910   Expr le = changeRight?
01911     leExpr(ineq[0], ineq[1] + rat(-1))
01912     : leExpr(ineq[0] + rat(1), ineq[1]);
01913   return newRWTheorem(ineq, le, a, pf);
01914 }
01915 
01916 
01917 /*! \param eqn is an equation 0 = a.x or 0 = c + a.x
01918  *  \param isIntx is a proof of IS_INTEGER(x)
01919  *
01920  * \return the theorem 0 = c + a.x <==> x=-c/a if -c/a is int else
01921  *  return the theorem 0 = c + a.x <==> false.
01922  *
01923  * It also handles the special case of 0 = a.x <==> x = 0
01924  */
01925 Theorem 
01926 ArithTheoremProducerOld::intVarEqnConst(const Expr& eqn,
01927              const Theorem& isIntx) {
01928   const Expr& left(eqn[0]);
01929   const Expr& right(eqn[1]);
01930   const Expr& isIntxexpr(isIntx.getExpr());
01931 
01932   if(CHECK_PROOFS) {
01933     CHECK_SOUND((isMult(right) && right[0].isRational())
01934                 || (right.arity() == 2 && isPlus(right)
01935                     && right[0].isRational()
01936                     && ((!isMult(right[1]) || right[1][0].isRational()))),
01937                 "ArithTheoremProducerOld::intVarEqnConst: "
01938     "rhs has a wrong format: " + right.toString());
01939     CHECK_SOUND(left.isRational() && 0 == left.getRational(),
01940                 "ArithTheoremProducerOld:intVarEqnConst:left is not a zero: " +
01941                 left.toString());
01942   }
01943   // Integrality constraint
01944   Expr x(right);
01945   Rational a(1), c(0);
01946   if(isMult(right)) {
01947     Expr aExpr;
01948     d_theoryArith->separateMonomial(right, aExpr, x);
01949     a = aExpr.getRational();
01950   } else { // right is a PLUS
01951     c = right[0].getRational();
01952     Expr aExpr;
01953     d_theoryArith->separateMonomial(right[1], aExpr, x);
01954     a = aExpr.getRational();
01955   }
01956   if(CHECK_PROOFS) {
01957     CHECK_SOUND(isIntPred(isIntxexpr) && isIntxexpr[0] == x,
01958                 "ArithTheoremProducerOld:intVarEqnConst: "
01959     "bad integrality constraint:\n right = " +
01960                 right.toString()+"\n isIntx = "+isIntxexpr.toString());
01961     CHECK_SOUND(a!=0, "ArithTheoremProducerOld:intVarEqnConst: eqn = "
01962     +eqn.toString());
01963   }
01964   const Assumptions& assump(isIntx.getAssumptionsRef());
01965   Proof pf;
01966   if(withProof())
01967     pf = newPf("int_const_eq", eqn, isIntx.getProof());
01968 
01969   // Solve for x:   x = r = -c/a
01970   Rational r(-c/a);
01971 
01972   if(r.isInteger())
01973     return newRWTheorem(eqn, x.eqExpr(rat(r)), assump, pf);
01974   else
01975     return newRWTheorem(eqn, d_em->falseExpr(), assump, pf);
01976 }
01977 
01978 
01979 Expr
01980 ArithTheoremProducerOld::create_t(const Expr& eqn) {
01981   const Expr& lhs = eqn[0];
01982   DebugAssert(isMult(lhs),
01983               CLASS_NAME "create_t : lhs must be a MULT"
01984               + lhs.toString());
01985   const Expr& x = lhs[1];
01986   Rational m = lhs[0].getRational()+1;
01987   DebugAssert(m > 0, "ArithTheoremProducerOld::create_t: m = "+m.toString());
01988   vector<Expr> kids;
01989   if(isPlus(eqn[1]))
01990     sumModM(kids, eqn[1], m, m);
01991   else
01992     kids.push_back(monomialModM(eqn[1], m, m));
01993   
01994   kids.push_back(multExpr(rat(1/m), x));
01995   return plusExpr(kids);
01996 }
01997 
01998 Expr
01999 ArithTheoremProducerOld::create_t2(const Expr& lhs, const Expr& rhs,
02000         const Expr& sigma) {
02001   Rational m = lhs[0].getRational()+1;
02002   DebugAssert(m > 0, "ArithTheoremProducerOld::create_t2: m = "+m.toString());
02003   vector<Expr> kids;
02004   if(isPlus(rhs))
02005     sumModM(kids, rhs, m, -1);
02006   else {
02007     kids.push_back(rat(0)); // For canonical form
02008     Expr monom = monomialModM(rhs, m, -1);
02009     if(!monom.isRational())
02010       kids.push_back(monom);
02011     else 
02012       DebugAssert(monom.getRational() == 0, "");
02013   }
02014   kids.push_back(rat(m)*sigma);
02015   return plusExpr(kids);
02016 }
02017 
02018 Expr
02019 ArithTheoremProducerOld::create_t3(const Expr& lhs, const Expr& rhs,
02020         const Expr& sigma) {
02021   const Rational& a = lhs[0].getRational();
02022   Rational m = a+1;
02023   DebugAssert(m > 0, "ArithTheoremProducerOld::create_t3: m = "+m.toString());
02024   vector<Expr> kids;
02025   if(isPlus(rhs))
02026     sumMulF(kids, rhs, m, 1);
02027   else {
02028     kids.push_back(rat(0)); // For canonical form
02029     Expr monom = monomialMulF(rhs, m, 1);
02030     if(!monom.isRational())
02031       kids.push_back(monom);
02032     else
02033       DebugAssert(monom.getRational() == 0, "");
02034   }
02035   kids.push_back(rat(-a)*sigma);
02036   return plusExpr(kids);
02037 }
02038 
02039 Rational
02040 ArithTheoremProducerOld::modEq(const Rational& i, const Rational& m) {
02041   DebugAssert(m > 0, "ArithTheoremProducerOld::modEq: m = "+m.toString());
02042   Rational half(1,2);
02043   Rational res((i - m*(floor((i/m) + half))));
02044   TRACE("arith eq", "modEq("+i.toString()+", "+m.toString()+") = ", res, "");
02045   return res;
02046 }
02047 
02048 Rational
02049 ArithTheoremProducerOld::f(const Rational& i, const Rational& m) {
02050   DebugAssert(m > 0, "ArithTheoremProducerOld::f: m = "+m.toString());
02051   Rational half(1,2);
02052   return (floor(i/m + half)+modEq(i,m));
02053 }
02054 
02055 void
02056 ArithTheoremProducerOld::sumModM(vector<Expr>& summands, const Expr& sum,
02057                               const Rational& m, const Rational& divisor) {
02058   DebugAssert(divisor != 0, "ArithTheoremProducerOld::sumModM: divisor = "
02059         +divisor.toString());
02060   Expr::iterator i = sum.begin();
02061   DebugAssert(i != sum.end(), CLASS_NAME "::sumModM");
02062   Rational C = i->getRational();
02063   C = modEq(C,m)/divisor;
02064   summands.push_back(rat(C));
02065   i++;
02066   for(Expr::iterator iend=sum.end(); i!=iend; ++i) {
02067     Expr monom = monomialModM(*i, m, divisor);
02068     if(!monom.isRational())
02069       summands.push_back(monom);
02070     else
02071       DebugAssert(monom.getRational() == 0, "");
02072   }
02073 }
02074 
02075 Expr
02076 ArithTheoremProducerOld::monomialModM(const Expr& i,
02077                                    const Rational& m, const Rational& divisor)
02078 {
02079   DebugAssert(divisor != 0, "ArithTheoremProducerOld::monomialModM: divisor = "
02080         +divisor.toString());
02081   Expr res;
02082   if(isMult(i)) {
02083     Rational ai = i[0].getRational();
02084     ai = modEq(ai,m)/divisor;
02085     if(0 == ai) res = rat(0);
02086     else if(1 == ai && i.arity() == 2) res = i[1];
02087     else {
02088       vector<Expr> kids = i.getKids();
02089       kids[0] = rat(ai);
02090       res = multExpr(kids);
02091     }
02092   } else { // It's a single variable
02093     Rational ai = modEq(1,m)/divisor;
02094     if(1 == ai) res = i;
02095     else res = rat(ai)*i;
02096   }
02097   DebugAssert(!res.isNull(), "ArithTheoremProducerOld::monomialModM()");
02098   TRACE("arith eq", "monomialModM(i="+i.toString()+", m="+m.toString()
02099   +", div="+divisor.toString()+") = ", res, "");
02100   return res;
02101 }
02102 
02103 void
02104 ArithTheoremProducerOld::sumMulF(vector<Expr>& summands, const Expr& sum,
02105                               const Rational& m, const Rational& divisor) {
02106   DebugAssert(divisor != 0, "ArithTheoremProducerOld::sumMulF: divisor = "
02107         +divisor.toString());
02108   Expr::iterator i = sum.begin();
02109   DebugAssert(i != sum.end(), CLASS_NAME "::sumModM");
02110   Rational C = i->getRational();
02111   C = f(C,m)/divisor;
02112   summands.push_back(rat(C));
02113   i++;
02114   for(Expr::iterator iend=sum.end(); i!=iend; ++i) {
02115     Expr monom = monomialMulF(*i, m, divisor);
02116     if(!monom.isRational())
02117       summands.push_back(monom);
02118     else
02119       DebugAssert(monom.getRational() == 0, "");
02120   }
02121 }
02122 
02123 Expr
02124 ArithTheoremProducerOld::monomialMulF(const Expr& i,
02125                                    const Rational& m, const Rational& divisor)
02126 {
02127   DebugAssert(divisor != 0, "ArithTheoremProducerOld::monomialMulF: divisor = "
02128         +divisor.toString());
02129   Rational ai = isMult(i) ? (i)[0].getRational() : 1;
02130   Expr xi = isMult(i) ? (i)[1] : (i);
02131   ai = f(ai,m)/divisor;
02132   if(0 == ai) return rat(0);
02133   if(1 == ai) return xi;
02134   return multExpr(rat(ai), xi);
02135 }
02136 
02137 // This recursive function accepts a term, t, and a 'map' of
02138 // substitutions [x1/t1, x2/t2,...,xn/tn].  it returns a t' which is
02139 // basically t[x1/t1,x2/t2...xn/tn]
02140 Expr
02141 ArithTheoremProducerOld::substitute(const Expr& term, ExprMap<Expr>& eMap)
02142 {
02143   ExprMap<Expr>::iterator i, iend = eMap.end();
02144 
02145   i = eMap.find(term);
02146   if(iend != i)
02147     return (*i).second;
02148 
02149   if (isMult(term)) {
02150     //in this case term is of the form c.x
02151     i = eMap.find(term[1]);
02152     if(iend != i)
02153       return term[0]*(*i).second;
02154     else
02155       return term;
02156   }
02157 
02158   if(isPlus(term)) {
02159     vector<Expr> output;
02160     for(Expr::iterator j = term.begin(), jend = term.end(); j != jend; ++j)
02161       output.push_back(substitute(*j, eMap));
02162     return plusExpr(output);
02163   }
02164   return term;    
02165 }
02166 
02167 bool ArithTheoremProducerOld::greaterthan(const Expr & l, const Expr & r)
02168 {
02169   //    DebugAssert(l != r, "");
02170   if (l==r) return false;
02171     
02172   switch(l.getKind()) {
02173   case RATIONAL_EXPR:
02174     DebugAssert(!r.isRational(), "");
02175     return true;
02176     break;
02177   case POW:
02178     switch (r.getKind()) {
02179     case RATIONAL_EXPR:
02180       // TODO:
02181       // alternately I could return (not greaterthan(r,l))
02182       return false;
02183       break;
02184     case POW:
02185       // x^n > y^n if x > y
02186       // x^n1 > x^n2 if n1 > n2
02187       return 
02188         ((r[1] < l[1]) || 
02189          ((r[1]==l[1]) && (r[0].getRational() < l[0].getRational())));
02190       break;
02191             
02192     case MULT:
02193       DebugAssert(r.arity() > 1, "");
02194       DebugAssert((r.arity() > 2) || (r[1] != l), "");
02195       if (r[1] == l) return false;
02196       return greaterthan(l, r[1]);
02197       break;
02198     case PLUS:
02199       DebugAssert(false, "");
02200       return true;
02201       break;
02202     default:
02203       // leaf
02204       return ((r < l[1]) || ((r == l[1]) && l[0].getRational() > 1));
02205       break;
02206     }
02207     break;
02208   case MULT:
02209     DebugAssert(l.arity() > 1, "");
02210     switch (r.getKind()) {
02211     case RATIONAL_EXPR:
02212       return false;
02213       break;
02214     case POW:
02215       DebugAssert(l.arity() > 1, "");
02216       DebugAssert((l.arity() > 2) || (l[1] != r), "");
02217       // TODO:
02218       // alternately return (not greaterthan(r,l)
02219       return ((l[1] == r) || greaterthan(l[1], r));
02220       break;
02221     case MULT:
02222       {
02223             
02224         DebugAssert(r.arity() > 1, "");
02225         Expr::iterator i = l.begin();
02226         Expr::iterator j = r.begin();
02227         ++i;
02228         ++j;
02229         for (; i != l.end() && j != r.end(); ++i, ++j) {
02230           if (*i == *j)
02231             continue;
02232           return greaterthan(*i,*j);
02233         }
02234         DebugAssert(i != l.end() || j != r.end(), "");
02235         if (i == l.end()) {
02236           // r is bigger
02237           return false;
02238         }
02239         else
02240           {
02241             // l is bigger
02242             return true;
02243           }
02244       }
02245       break;
02246     case PLUS:
02247       DebugAssert(false, "");
02248       return true;
02249       break;
02250     default:
02251       // leaf
02252       DebugAssert((l.arity() > 2) || (l[1] != r), "");
02253       return ((l[1] == r) || greaterthan(l[1], r));
02254       break;
02255     }
02256     break;
02257   case PLUS:
02258     DebugAssert(false, "");
02259     return true;
02260     break;
02261   default:
02262     // leaf
02263     switch (r.getKind()) {
02264     case RATIONAL_EXPR:
02265       return false;
02266       break;
02267     case POW:
02268       return ((r[1] < l) || ((r[1] == l) && (r[0].getRational() < 1)));
02269       break;
02270     case MULT:
02271       DebugAssert(r.arity() > 1, "");
02272       DebugAssert((r.arity() > 2) || (r[1] != l), "");
02273       if (l == r[1]) return false;
02274       return greaterthan(l,r[1]);
02275       break;
02276     case PLUS:
02277       DebugAssert(false, "");
02278       return true;
02279       break;
02280     default:
02281       // leaf
02282       return (r < l);
02283       break;
02284     }
02285     break;
02286   }
02287 }
02288 
02289 
02290 Theorem
02291 ArithTheoremProducerOld::eqElimIntRule(const Theorem& eqn, const Theorem& isIntx,
02292             const vector<Theorem>& isIntVars) {
02293   TRACE("arith eq", "eqElimIntRule(", eqn.getExpr(), ") {");
02294   Proof pf;
02295 
02296   if(CHECK_PROOFS)
02297     CHECK_SOUND(eqn.isRewrite(),
02298                 "ArithTheoremProducerOld::eqElimInt: input must be an equation" +
02299                 eqn.toString());
02300 
02301   const Expr& lhs = eqn.getLHS();
02302   const Expr& rhs = eqn.getRHS();
02303   Expr a, x;
02304   d_theoryArith->separateMonomial(lhs, a, x);
02305 
02306   if(CHECK_PROOFS) {
02307     // Checking LHS
02308     const Expr& isIntxe = isIntx.getExpr();
02309     CHECK_SOUND(isIntPred(isIntxe) && isIntxe[0] == x,
02310     "ArithTheoremProducerOld::eqElimInt\n eqn = "
02311     +eqn.getExpr().toString()
02312     +"\n isIntx = "+isIntxe.toString());
02313     CHECK_SOUND(isRational(a) && a.getRational().isInteger()
02314     && a.getRational() >= 2,
02315     "ArithTheoremProducerOld::eqElimInt:\n lhs = "+lhs.toString());
02316     // Checking RHS
02317     // It cannot be a division (we don't handle it)
02318     CHECK_SOUND(!isDivide(rhs),
02319     "ArithTheoremProducerOld::eqElimInt:\n rhs = "+rhs.toString());
02320     // If it's a single monomial, then it's the only "variable"
02321     if(!isPlus(rhs)) {
02322       Expr c, v;
02323       d_theoryArith->separateMonomial(rhs, c, v);
02324       CHECK_SOUND(isIntVars.size() == 1
02325       && isIntPred(isIntVars[0].getExpr())
02326       && isIntVars[0].getExpr()[0] == v
02327       && isRational(c) && c.getRational().isInteger(),
02328       "ArithTheoremProducerOld::eqElimInt:\n rhs = "+rhs.toString()
02329       +"isIntVars.size = "+int2string(isIntVars.size()));
02330     } else { // RHS is a plus
02331       CHECK_SOUND(isIntVars.size() + 1 == (size_t)rhs.arity(),
02332       "ArithTheoremProducerOld::eqElimInt: rhs = "+rhs.toString());
02333       // Check the free constant
02334       CHECK_SOUND(isRational(rhs[0]) && rhs[0].getRational().isInteger(),
02335       "ArithTheoremProducerOld::eqElimInt: rhs = "+rhs.toString());
02336       // Check the vars
02337       for(size_t i=0, iend=isIntVars.size(); i<iend; ++i) {
02338   Expr c, v;
02339   d_theoryArith->separateMonomial(rhs[i+1], c, v);
02340   const Expr& isInt(isIntVars[i].getExpr());
02341   CHECK_SOUND(isIntPred(isInt) && isInt[0] == v
02342         && isRational(c) && c.getRational().isInteger(),
02343         "ArithTheoremProducerOld::eqElimInt:\n rhs["+int2string(i+1)
02344         +"] = "+rhs[i+1].toString()
02345         +"\n isInt = "+isInt.toString());
02346       }
02347     }
02348   }
02349 
02350   // Creating a fresh bound variable
02351   static int varCount(0);
02352   Expr newVar = d_em->newBoundVarExpr("_int_var", int2string(varCount++));
02353   newVar.setType(intType());
02354   Expr t2 = create_t2(lhs, rhs, newVar);
02355   Expr t3 = create_t3(lhs, rhs, newVar);
02356   vector<Expr> vars;
02357   vars.push_back(newVar);
02358   Expr res = d_em->newClosureExpr(EXISTS, vars,
02359                                   x.eqExpr(t2) && rat(0).eqExpr(t3));
02360   
02361   vector<Theorem> thms(isIntVars);
02362   thms.push_back(isIntx);
02363   thms.push_back(eqn);
02364   Assumptions assump(thms);
02365 
02366   if(withProof()) {
02367     vector<Proof> pfs;
02368     pfs.push_back(eqn.getProof());
02369     pfs.push_back(isIntx.getProof());
02370     vector<Theorem>::const_iterator i=isIntVars.begin(), iend=isIntVars.end();
02371     for(; i!=iend; ++i) 
02372       pfs.push_back(i->getProof());
02373     pf = newPf("eq_elim_int", eqn.getExpr(), pfs);
02374   }
02375 
02376   Theorem thm(newTheorem(res, assump, pf));
02377   TRACE("arith eq", "eqElimIntRule => ", thm.getExpr(), " }");
02378   return thm;
02379 }
02380 
02381 
02382 Theorem
02383 ArithTheoremProducerOld::isIntConst(const Expr& e) {
02384   Proof pf;
02385 
02386   if(CHECK_PROOFS) {
02387     CHECK_SOUND(isIntPred(e) && e[0].isRational(),
02388     "ArithTheoremProducerOld::isIntConst(e = "
02389     +e.toString()+")");
02390   }
02391   if(withProof())
02392     pf = newPf("is_int_const", e);
02393   bool isInt = e[0].getRational().isInteger();
02394   return newRWTheorem(e, isInt? d_em->trueExpr() : d_em->falseExpr(), Assumptions::emptyAssump(), pf);
02395 }
02396 
02397 
02398 Theorem
02399 ArithTheoremProducerOld::equalLeaves1(const Theorem& thm)
02400 {
02401   Proof pf;
02402   const Expr& e = thm.getRHS();
02403 
02404   if (CHECK_PROOFS) {
02405     CHECK_SOUND(e[1].getKind() == RATIONAL_EXPR &&
02406     e[1].getRational() == Rational(0) &&
02407     e[0].getKind() == PLUS &&
02408     e[0].arity() == 3 &&
02409     e[0][0].getKind() == RATIONAL_EXPR &&
02410     e[0][0].getRational() == Rational(0) &&
02411     e[0][1].getKind() == MULT &&
02412     e[0][1].arity() == 2 &&
02413     e[0][1][0].getKind() == RATIONAL_EXPR &&
02414     e[0][1][0].getRational() == Rational(-1),
02415     "equalLeaves1");
02416   }
02417   if (withProof())
02418   {
02419     vector<Proof> pfs;
02420     pfs.push_back(thm.getProof());
02421     pf = newPf("equalLeaves1", e, pfs);
02422   }
02423   return newRWTheorem(e, e[0][1][1].eqExpr(e[0][2]), thm.getAssumptionsRef(), pf);
02424 }
02425 
02426 
02427 Theorem
02428 ArithTheoremProducerOld::equalLeaves2(const Theorem& thm)
02429 {
02430   Proof pf;
02431   const Expr& e = thm.getRHS();
02432 
02433   if (CHECK_PROOFS) {
02434     CHECK_SOUND(e[0].getKind() == RATIONAL_EXPR &&
02435     e[0].getRational() == Rational(0) &&
02436     e[1].getKind() == PLUS &&
02437     e[1].arity() == 3 &&
02438     e[1][0].getKind() == RATIONAL_EXPR &&
02439     e[1][0].getRational() == Rational(0) &&
02440     e[1][1].getKind() == MULT &&
02441     e[1][1].arity() == 2 &&
02442     e[1][1][0].getKind() == RATIONAL_EXPR &&
02443     e[1][1][0].getRational() == Rational(-1),
02444     "equalLeaves2");
02445   }
02446   if (withProof())
02447   {
02448     vector<Proof> pfs;
02449     pfs.push_back(thm.getProof());
02450     pf = newPf("equalLeaves2", e, pfs);
02451   }
02452   return newRWTheorem(e, e[1][1][1].eqExpr(e[1][2]), thm.getAssumptionsRef(), pf);
02453 }
02454 
02455 
02456 Theorem
02457 ArithTheoremProducerOld::equalLeaves3(const Theorem& thm)
02458 {
02459   Proof pf;
02460   const Expr& e = thm.getRHS();
02461 
02462   if (CHECK_PROOFS) {
02463     CHECK_SOUND(e[1].getKind() == RATIONAL_EXPR &&
02464     e[1].getRational() == Rational(0) &&
02465     e[0].getKind() == PLUS &&
02466     e[0].arity() == 3 &&
02467     e[0][0].getKind() == RATIONAL_EXPR &&
02468     e[0][0].getRational() == Rational(0) &&
02469     e[0][2].getKind() == MULT &&
02470     e[0][2].arity() == 2 &&
02471     e[0][2][0].getKind() == RATIONAL_EXPR &&
02472     e[0][2][0].getRational() == Rational(-1),
02473     "equalLeaves3");
02474   }
02475   if (withProof())
02476   {
02477     vector<Proof> pfs;
02478     pfs.push_back(thm.getProof());
02479     pf = newPf("equalLeaves3", e, pfs);
02480   }
02481   return newRWTheorem(e, e[0][2][1].eqExpr(e[0][1]), thm.getAssumptionsRef(), pf);
02482 }
02483 
02484 
02485 Theorem
02486 ArithTheoremProducerOld::equalLeaves4(const Theorem& thm)
02487 {
02488   Proof pf;
02489   const Expr& e = thm.getRHS();
02490 
02491   if (CHECK_PROOFS) {
02492     CHECK_SOUND(e[0].getKind() == RATIONAL_EXPR &&
02493     e[0].getRational() == Rational(0) &&
02494     e[1].getKind() == PLUS &&
02495     e[1].arity() == 3 &&
02496     e[1][0].getKind() == RATIONAL_EXPR &&
02497     e[1][0].getRational() == Rational(0) &&
02498     e[1][2].getKind() == MULT &&
02499     e[1][2].arity() == 2 &&
02500     e[1][2][0].getKind() == RATIONAL_EXPR &&
02501     e[1][2][0].getRational() == Rational(-1),
02502     "equalLeaves4");
02503   }
02504   if (withProof())
02505   {
02506     vector<Proof> pfs;
02507     pfs.push_back(thm.getProof());
02508     pf = newPf("equalLeaves4", e, pfs);
02509   }
02510   return newRWTheorem(e, e[1][2][1].eqExpr(e[1][1]), thm.getAssumptionsRef(), pf);
02511 }
02512 
02513 Theorem
02514 ArithTheoremProducerOld::diseqToIneq(const Theorem& diseq) {
02515   Proof pf;
02516 
02517   const Expr& e = diseq.getExpr();
02518 
02519   if(CHECK_PROOFS) {
02520     CHECK_SOUND(e.isNot() && e[0].isEq(),
02521     "ArithTheoremProducerOld::diseqToIneq: expected disequality:\n"
02522     " e = "+e.toString());
02523   }
02524 
02525   const Expr& x = e[0][0];
02526   const Expr& y = e[0][1];
02527 
02528   if(withProof())
02529     pf = newPf(e, diseq.getProof());
02530   return newTheorem(ltExpr(x,y).orExpr(gtExpr(x,y)), diseq.getAssumptionsRef(), pf);
02531 }
02532 
02533 Theorem ArithTheoremProducerOld::dummyTheorem(const Expr& e) {
02534   Proof pf; 
02535   return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
02536 }
02537 
02538 Theorem ArithTheoremProducerOld::oneElimination(const Expr& e) {
02539   
02540   // Check soundness
02541   if (CHECK_PROOFS)
02542     CHECK_SOUND(isMult(e) &&
02543           e.arity() == 2 && 
02544                 e[0].isRational() &&
02545                 e[0].getRational() == 1, 
02546                 "oneElimination: input must be a multiplication by one" + e.toString());
02547 
02548   // The proof object that we will us
02549   Proof pf;
02550   
02551   // Setup the proof if needed
02552   if (withProof()) 
02553     pf = newPf("oneElimination", e);
02554   
02555   // Return the rewrite theorem that explains the phenomenon
02556   return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf); 
02557 }
02558 
02559 Theorem ArithTheoremProducerOld::clashingBounds(const Theorem& lowerBound, const Theorem& upperBound) {
02560   
02561   // Get the expressions
02562   const Expr& lowerBoundExpr = lowerBound.getExpr();
02563   const Expr& upperBoundExpr = upperBound.getExpr();
02564    
02565   // Check soundness
02566   if (CHECK_PROOFS) {
02567     CHECK_SOUND(isLE(lowerBoundExpr) || isLT(lowerBoundExpr), "clashingBounds: lowerBound should be >= or > " + lowerBoundExpr.toString());
02568     CHECK_SOUND(isGE(upperBoundExpr) || isGT(upperBoundExpr), "clashingBounds: upperBound should be <= or < " + upperBoundExpr.toString());
02569     CHECK_SOUND(lowerBoundExpr[0].isRational(), "clashingBounds: lowerBound left side should be a rational " + lowerBoundExpr.toString());
02570     CHECK_SOUND(upperBoundExpr[0].isRational(), "clashingBounds: upperBound left side should be a rational " + upperBoundExpr.toString());
02571     CHECK_SOUND(lowerBoundExpr[1] == upperBoundExpr[1], "clashingBounds: bounds not on the same term " + lowerBoundExpr.toString() + ", " + upperBoundExpr.toString());
02572     
02573     // Get the bounds
02574     Rational lowerBoundR = lowerBoundExpr[0].getRational();
02575     Rational upperBoundR = upperBoundExpr[0].getRational();
02576     
02577     if (isLE(lowerBoundExpr) && isGE(upperBoundExpr))
02578       CHECK_SOUND(upperBoundR < lowerBoundR, "clashingBounds: bounds are satisfiable");
02579     else 
02580       CHECK_SOUND(upperBoundR <= lowerBoundR, "clashingBounds: bounds are satisfiable");
02581   }
02582   
02583   // The proof object that we will use
02584   Proof pf;
02585   // Setup the proof if needed
02586   if (withProof()) 
02587     pf = newPf("clashingBounds", lowerBoundExpr, upperBoundExpr);
02588   
02589   // Put the bounds expressions in the assumptions
02590   Assumptions assumptions;
02591   assumptions.add(lowerBound);
02592   assumptions.add(upperBound);  
02593   
02594   // Return the theorem
02595   return newTheorem(d_em->falseExpr(), assumptions, pf);
02596 }
02597 
02598 Theorem ArithTheoremProducerOld::addInequalities(const Theorem& thm1, const Theorem& thm2) {
02599   
02600   // Get the expressions of the theorem
02601   const Expr& expr1 = thm1.getExpr();
02602   const Expr& expr2 = thm2.getExpr();
02603 
02604   // Check soundness
02605   if (CHECK_PROOFS) {
02606 
02607     CHECK_SOUND(isIneq(expr1), "addInequalities: expecting an inequality for thm1, got " + expr1.toString());
02608     CHECK_SOUND(isIneq(expr2), "addInequalities: expecting an inequality for thm2, got " + expr2.toString());
02609 
02610     if (isLE(expr1) || isLT(expr1))
02611       CHECK_SOUND(isLE(expr2) || isLT(expr2), "addInequalities: expr2 should be <(=) also " + expr2.toString());
02612     if (isGE(expr1) || isGT(expr1)) 
02613       CHECK_SOUND(isGE(expr2) || isGT(expr2), "addInequalities: expr2 should be >(=) also" + expr2.toString());
02614   }
02615   
02616   // Create the assumptions
02617   Assumptions a(thm1, thm2);
02618   
02619     // Get the kinds of the inequalitites
02620     int kind1  = expr1.getKind();
02621     int kind2  = expr2.getKind();
02622   
02623     // Set-up the resulting inequality
02624     int kind = (kind1 == kind2) ? kind1 : ((kind1 == LT) || (kind2 == LT))? LT : GT;
02625   
02626     // Create the proof object
02627     Proof pf;     
02628     if(withProof()) {
02629       vector<Proof> pfs;
02630       pfs.push_back(thm1.getProof());
02631       pfs.push_back(thm2.getProof());
02632       pf = newPf("addInequalities", expr1, expr2, pfs);
02633     }
02634     
02635     // Create the new expressions
02636     Expr leftSide  = plusExpr(expr1[0], expr2[0]);
02637     Expr rightSide = plusExpr(expr1[1], expr2[1]); 
02638     
02639     // Return the theorem 
02640     return newTheorem(Expr(kind, leftSide, rightSide), a, pf); 
02641 }
02642 
02643 Theorem ArithTheoremProducerOld::implyWeakerInequality(const Expr& expr1, const Expr& expr2) {
02644   
02645   // Check soundness
02646   if (CHECK_PROOFS) {
02647     
02648     // Both must be inequalitites
02649     CHECK_SOUND(isIneq(expr1), "implyWeakerInequality: expr1 should be an inequality" + expr1.toString());
02650     CHECK_SOUND(isIneq(expr2), "implyWeakerInequality: expr1 should be an inequality" + expr2.toString());
02651     
02652     // Should be of the same type
02653     if (isLE(expr1) || isLT(expr1))
02654       CHECK_SOUND(isLE(expr2) || isLT(expr2), "implyWeakerInequality: expr2 should be <(=) also " + expr2.toString());
02655     if (isGE(expr1) || isGT(expr1)) 
02656       CHECK_SOUND(isGE(expr2) || isGT(expr2), "implyWeakerInequality: expr2 should be >(=) also" + expr2.toString());
02657       
02658     // Left sides must be rational numbers
02659     CHECK_SOUND(expr1[0].isRational(), "implyWeakerInequality: expr1 should have a rational on the left side" + expr1.toString());
02660     CHECK_SOUND(expr2[0].isRational(), "implyWeakerInequality: expr2 should have a rational on the left side" + expr2.toString());
02661 
02662     // Right sides must be identical
02663     CHECK_SOUND(expr1[1] == expr2[1], "implyWeakerInequality: the expression must be the same" + expr1.toString() + " and " + expr2.toString());          
02664   
02665     Rational expr1rat = expr1[0].getRational();
02666     Rational expr2rat = expr2[0].getRational();
02667     
02668   
02669     // Check the bounds
02670     if (isLE(expr1) || isLT(expr2))
02671         CHECK_SOUND(expr2rat < expr1rat,  "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
02672     else
02673         CHECK_SOUND(expr2rat <= expr1rat, "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
02674     if (isGE(expr1) || isGT(expr2))
02675         CHECK_SOUND(expr2rat > expr1rat,  "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
02676     else
02677         CHECK_SOUND(expr2rat >= expr1rat, "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
02678     
02679   }
02680 
02681     // Create the proof object
02682     Proof pf;     
02683     if(withProof()) pf = newPf("implyWeakerInequality", expr1, expr2);
02684 
02685   // Return the theorem 
02686   return newTheorem(expr1.impExpr(expr2), Assumptions::emptyAssump(), pf);
02687 }
02688 
02689 Theorem ArithTheoremProducerOld::implyNegatedInequality(const Expr& expr1, const Expr& expr2) {
02690 
02691   // Check soundness
02692   if (CHECK_PROOFS) {
02693     CHECK_SOUND(isIneq(expr1), "implyNegatedInequality: lowerBound should be an inequality " + expr1.toString());
02694     CHECK_SOUND(isIneq(expr2), "implyNegatedInequality: upperBound should be be an inequality " + expr2.toString());
02695     CHECK_SOUND(expr1[0].isRational(), "implyNegatedInequality: lowerBound left side should be a rational " + expr1.toString());
02696     CHECK_SOUND(expr2[0].isRational(), "implyNegatedInequality: upperBound left side should be a rational " + expr2.toString());
02697     CHECK_SOUND(expr1[1] == expr2[1], "implyNegatedInequality: bounds not on the same term " + expr1.toString() + ", " + expr2.toString());
02698     
02699     // Get the bounds
02700     Rational lowerBoundR = expr1[0].getRational();
02701     Rational upperBoundR = expr2[0].getRational();
02702     
02703     if (isLE(expr1) && isGE(expr2))
02704       CHECK_SOUND(upperBoundR < lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());
02705     if (isLT(expr1) || isGT(expr2))
02706       CHECK_SOUND(upperBoundR <= lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());    
02707     if (isGE(expr1) && isLE(expr2))
02708       CHECK_SOUND(upperBoundR > lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());
02709     if (isGT(expr1) || isLT(expr2))
02710       CHECK_SOUND(upperBoundR >= lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());
02711   }
02712   
02713   // The proof object that we will use
02714   Proof pf;
02715   if (withProof()) pf = newPf("implyNegatedInequality", expr1, expr2);
02716   
02717   // Return the theorem
02718   return newTheorem(expr1.impExpr(expr2.negate()), Assumptions::emptyAssump(), pf); 
02719 }
02720 
02721 Theorem ArithTheoremProducerOld::trustedRewrite(const Expr& expr1, const Expr& expr2) {
02722 
02723   // The proof object that we will us
02724   Proof pf;
02725 
02726   // Setup the proof if needed
02727   if (withProof()) pf = newPf("trustedRewrite", expr1, expr2);
02728   
02729   // Return the rewrite theorem that explains the phenomenon
02730   return newRWTheorem(expr1, expr2, Assumptions::emptyAssump(), pf); 
02731 
02732 }
02733 
02734 Theorem ArithTheoremProducerOld::integerSplit(const Expr& intVar, const Rational& intPoint) {
02735 
02736   // Check soundness
02737   if (CHECK_PROOFS) {
02738     CHECK_SOUND(intPoint.isInteger(), "integerSplit: we can only split on integer points, given" + intPoint.toString());
02739   }
02740 
02741   // Create the expression
02742   const Expr& split = Expr(IS_INTEGER, intVar).impExpr(leExpr(intVar, rat(intPoint)).orExpr(geExpr(intVar, rat(intPoint + 1))));
02743   
02744   // The proof object that we will use
02745   Proof pf;
02746   if (withProof()) pf = newPf("integerSplit", intVar, rat(intPoint));
02747   
02748   // Return the theorem
02749   return newTheorem(split, Assumptions::emptyAssump(), pf); 
02750 }
02751 
02752 
02753 Theorem ArithTheoremProducerOld::rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr) {
02754   
02755   
02756   // Check soundness
02757   if (CHECK_PROOFS) {
02758     // Right side of the constraint should correspond to the proved integer expression
02759     CHECK_SOUND(isIneq(constr), "rafineStrictInteger: expected a constraint got : " + constr.toString());
02760     CHECK_SOUND(isIntConstrThm.getExpr()[0] == constr[1], "rafineStrictInteger: proof of intger doesn't correspond to the constarint right side");
02761     CHECK_SOUND(constr[0].isRational(), "rafineStrictInteger: right side of the constraint muts be a rational");
02762   }
02763 
02764   // Get the contraint bound
02765   Rational bound = constr[0].getRational();
02766   
02767   // Get the kind of the constraint
02768   int kind = constr.getKind();
02769   
02770   // If the bound is strict, make it non-strict
02771   switch (kind) {
02772     case LT:
02773       kind = LE;                
02774       if (bound.isInteger()) bound ++;             // 3 < x   --> 4 <= x
02775       else bound = ceil(bound);                    // 3.4 < x --> 4 <= x
02776       break;
02777     case LE:
02778       kind = LE;
02779       if (!bound.isInteger()) bound = ceil(bound); // 3.5 <= x --> 4 <= x  
02780       break;
02781     case GT:
02782       kind = GE;                
02783       if (bound.isInteger()) bound --;             // 3 > x   --> 2 >= x
02784       else bound = floor(bound);                   // 3.4 > x --> 3 >= x
02785       break;  
02786     case GE:
02787       kind = GE;
02788       if (!bound.isInteger()) bound = floor(bound); // 3.4 >= x --> 3 >= x 
02789       break;
02790   } 
02791   
02792   // The new constraint 
02793   Expr newConstr(kind, rat(bound), constr[1]);
02794   
02795   // Pick up the assumptions from the integer proof
02796   const Assumptions& assump(isIntConstrThm.getAssumptionsRef());
02797     
02798     // Construct the proof object if necessary
02799     Proof pf;
02800   if (withProof()) pf = newPf("rafineStrictInteger", constr, isIntConstrThm.getProof());
02801     
02802   // Return the rewrite theorem that explains the phenomenon
02803   return newRWTheorem(constr, newConstr, assump, pf); 
02804 }

Generated on Tue Jul 3 14:33:34 2007 for CVC3 by  doxygen 1.5.1