arith_theorem_producer3.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_producer3.h"
00033 #include "theory_core.h"
00034 #include "theory_arith3.h"
00035 
00036 using namespace std;
00037 using namespace CVC3;
00038 
00039 ////////////////////////////////////////////////////////////////////
00040 // TheoryArith: trusted method for creating ArithTheoremProducer3
00041 ////////////////////////////////////////////////////////////////////
00042 
00043 ArithProofRules* TheoryArith3::createProofRules3() {
00044   return new ArithTheoremProducer3(theoryCore()->getTM(), this);
00045 }
00046 
00047 ////////////////////////////////////////////////////////////////////
00048 // Canonization rules
00049 ////////////////////////////////////////////////////////////////////
00050 
00051 
00052 #define CLASS_NAME "ArithTheoremProducer3"
00053 
00054 
00055 // Rule for variables: e == 1 * e
00056 Theorem ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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                "ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::greaterthan(e1,e2);
00423   }
00424 };
00425 
00426 typedef map<Expr,Rational,MonomialLess> MonomMap;
00427 
00428 Expr
00429 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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     "ArithTheoremProducer3::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     "ArithTheoremProducer3::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 ArithTheoremProducer3::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 ArithTheoremProducer3::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 // 0 = (* e1 e2 ...) <=> 0 = e1 OR 0 = e2 OR ...
01142 Theorem ArithTheoremProducer3::multEqZero(const Expr& expr)
01143 {
01144   if (CHECK_PROOFS) {
01145     CHECK_SOUND(expr.isEq() && expr[0].isRational() &&
01146                 expr[0].getRational() == 0 &&
01147                 isMult(expr[1]) && expr[1].arity() > 1,
01148                 "multEqZero invariant violated"+expr.toString());
01149   }
01150   Proof pf;
01151   vector<Expr> kids;
01152   Expr::iterator i = expr[1].begin(), iend = expr[1].end();
01153   for (; i != iend; ++i) {
01154     kids.push_back(rat(0).eqExpr(*i));
01155   }
01156   if (withProof()) {
01157     pf = newPf("multEqZero", expr);
01158   }
01159   return newRWTheorem(expr, Expr(OR, kids), Assumptions::emptyAssump(), pf);
01160 }
01161 
01162 
01163 // 0 = (^ c x) <=> false if c <=0
01164 //             <=> 0 = x if c > 0
01165 Theorem ArithTheoremProducer3::powEqZero(const Expr& expr)
01166 {
01167   if (CHECK_PROOFS) {
01168     CHECK_SOUND(expr.isEq() && expr[0].isRational() &&
01169                 expr[0].getRational() == 0 &&
01170                 isPow(expr[1]) && expr[1].arity() == 2 &&
01171                 expr[1][0].isRational(),
01172                 "powEqZero invariant violated"+expr.toString());
01173   }
01174   Proof pf;
01175   if (withProof()) {
01176     pf = newPf("powEqZero", expr);
01177   }
01178   Rational r = expr[1][0].getRational();
01179   Expr res;
01180   if (r <= 0) {
01181     res = d_em->falseExpr();
01182   }
01183   else {
01184     res = rat(0).eqExpr(expr[1][1]);
01185   }
01186   return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
01187 }
01188 
01189 
01190 // x^n = y^n <=> x = y (if n is odd)
01191 // x^n = y^n <=> x = y OR x = -y (if n is even)
01192 Theorem ArithTheoremProducer3::elimPower(const Expr& expr)
01193 {
01194   if (CHECK_PROOFS) {
01195     CHECK_SOUND(expr.isEq() && isPow(expr[0]) &&
01196                 isPow(expr[1]) &&
01197                 isIntegerConst(expr[0][0]) &&
01198                 expr[0][0].getRational() > 0 &&
01199                 expr[0][0] == expr[1][0],
01200                 "elimPower invariant violated"+expr.toString());
01201   }
01202   Proof pf;
01203   if (withProof()) {
01204     pf = newPf("elimPower", expr);
01205   }
01206   Rational r = expr[0][0].getRational();
01207   Expr res = expr[0][1].eqExpr(expr[1][1]);
01208   if (r % 2 == 0) {
01209     res = res.orExpr(expr[0][1].eqExpr(-expr[1][1]));
01210   }
01211   return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
01212 }
01213 
01214 
01215 // x^n = c <=> x = root (if n is odd and root^n = c)
01216 // x^n = c <=> x = root OR x = -root (if n is even and root^n = c)
01217 Theorem ArithTheoremProducer3::elimPowerConst(const Expr& expr, const Rational& root)
01218 {
01219   if (CHECK_PROOFS) {
01220     CHECK_SOUND(expr.isEq() && isPow(expr[0]) &&
01221                 isIntegerConst(expr[0][0]) &&
01222                 expr[0][0].getRational() > 0 &&
01223                 expr[1].isRational() &&
01224                 pow(expr[0][0].getRational(), root) == expr[1].getRational(),
01225                 "elimPowerConst invariant violated"+expr.toString());
01226   }
01227   Proof pf;
01228   if (withProof()) {
01229     pf = newPf("elimPowerConst", expr, rat(root));
01230   }
01231   Rational r = expr[0][0].getRational();
01232   Expr res = expr[0][1].eqExpr(rat(root));
01233   if (r % 2 == 0) {
01234     res = res.orExpr(expr[0][1].eqExpr(rat(-root)));
01235   }
01236   return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
01237 }
01238 
01239 
01240 // x^n = c <=> false (if n is even and c is negative)
01241 Theorem ArithTheoremProducer3::evenPowerEqNegConst(const Expr& expr)
01242 {
01243   if (CHECK_PROOFS) {
01244     CHECK_SOUND(expr.isEq() && isPow(expr[0]) &&
01245                 expr[1].isRational() &&
01246                 isIntegerConst(expr[0][0]) &&
01247                 expr[0][0].getRational() % 2 == 0 &&
01248                 expr[1].getRational() < 0,
01249                 "evenPowerEqNegConst invariant violated"+expr.toString());
01250   }
01251   Proof pf;
01252   if (withProof()) {
01253     pf = newPf("evenPowerEqNegConst", expr);
01254   }
01255   return newRWTheorem(expr, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
01256 }
01257 
01258 
01259 // x^n = c <=> false (if x is an integer and c is not a perfect n power)
01260 Theorem ArithTheoremProducer3::intEqIrrational(const Expr& expr, const Theorem& isIntx)
01261 {
01262   if (CHECK_PROOFS) {
01263     CHECK_SOUND(expr.isEq() && isPow(expr[0]) &&
01264                 expr[1].isRational() &&
01265                 expr[1].getRational() != 0 &&
01266                 isIntegerConst(expr[0][0]) &&
01267                 expr[0][0].getRational() > 0 &&
01268                 ratRoot(expr[1].getRational(), expr[0][0].getRational().getUnsigned()) == 0,
01269                 "intEqIrrational invariant violated"+expr.toString());
01270     CHECK_SOUND(isIntPred(isIntx.getExpr()) && isIntx.getExpr()[0] == expr[0][1],
01271     "ArithTheoremProducer3::intEqIrrational:\n "
01272     "wrong integrality constraint:\n expr = "
01273     +expr.toString()+"\n isIntx = "
01274     +isIntx.getExpr().toString());
01275   }
01276   const Assumptions& assump(isIntx.getAssumptionsRef());
01277   Proof pf;
01278   if (withProof()) {
01279     pf = newPf("int_eq_irr", expr, isIntx.getProof());
01280   }
01281   return newRWTheorem(expr, d_em->falseExpr(), assump, pf);
01282 }
01283 
01284 
01285 // e[0] kind e[1] <==> true when e[0] kind e[1],
01286 // false when e[0] !kind e[1], for constants only
01287 Theorem ArithTheoremProducer3::constPredicate(const Expr& e) {
01288   if(CHECK_PROOFS) {
01289     CHECK_SOUND(e.arity() == 2 && isRational(e[0]) && isRational(e[1]),
01290                 CLASS_NAME "::constPredicate:\n  "
01291                 "non-const parameters: " + e.toString());
01292   }
01293   Proof pf;
01294   bool result(false);
01295   int kind = e.getKind();
01296   Rational r1 = e[0].getRational(), r2 = e[1].getRational();
01297   switch(kind) {
01298   case EQ:
01299     result = (r1 == r2)?true : false;
01300     break;
01301   case LT:
01302     result = (r1 < r2)?true : false;
01303     break;
01304   case LE:
01305     result = (r1 <= r2)?true : false;
01306     break;
01307   case GT:
01308     result = (r1 > r2)?true : false;
01309     break;
01310   case GE:
01311     result = (r1 >= r2)?true : false;
01312     break;
01313   default:
01314     if(CHECK_PROOFS) {
01315       CHECK_SOUND(false,
01316                   "ArithTheoremProducer3::constPredicate: wrong kind");
01317     }
01318     break;
01319   }
01320   Expr ret = (result) ? d_em->trueExpr() : d_em->falseExpr();
01321   if(withProof()) pf = newPf("const_predicate", e,ret);
01322   return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
01323 }
01324 
01325 // e[0] kind e[1] <==> 0 kind e[1] - e[0]
01326 Theorem ArithTheoremProducer3::rightMinusLeft(const Expr& e)
01327 {
01328   Proof pf;
01329   int kind = e.getKind();
01330   if(CHECK_PROOFS) {
01331     CHECK_SOUND((EQ==kind) ||
01332                 (LT==kind) ||
01333                 (LE==kind) ||
01334                 (GE==kind) ||
01335                 (GT==kind),
01336                 "ArithTheoremProducer3::rightMinusLeft: wrong kind");
01337   }
01338   if(withProof()) pf = newPf("right_minus_left",e);
01339   return newRWTheorem(e, Expr(e.getOp(), rat(0), e[1] - e[0]), Assumptions::emptyAssump(), pf);
01340 }
01341 
01342 
01343 // e[0] kind e[1] <==> 0 kind e[1] - e[0]
01344 Theorem ArithTheoremProducer3::leftMinusRight(const Expr& e)
01345 {
01346   Proof pf;
01347   int kind = e.getKind();
01348   if(CHECK_PROOFS) {
01349     CHECK_SOUND((EQ==kind) ||
01350                 (LT==kind) ||
01351                 (LE==kind) ||
01352                 (GE==kind) ||
01353                 (GT==kind),
01354                 "ArithTheoremProducer3::rightMinusLeft: wrong kind");
01355   }
01356   if(withProof()) pf = newPf("left_minus_right",e);
01357   return newRWTheorem(e, Expr(e.getOp(), e[0] - e[1], rat(0)), Assumptions::emptyAssump(), pf);
01358 }
01359 
01360 
01361 // x kind y <==> x + z kind y + z
01362 Theorem ArithTheoremProducer3::plusPredicate(const Expr& x,
01363                                       const Expr& y,
01364                                       const Expr& z, int kind) {
01365   if(CHECK_PROOFS) {
01366     CHECK_SOUND((EQ==kind) ||
01367                 (LT==kind) ||
01368                 (LE==kind) ||
01369                 (GE==kind) ||
01370                 (GT==kind),
01371                 "ArithTheoremProducer3::plusPredicate: wrong kind");
01372   }
01373   Proof pf;
01374   Expr left = Expr(kind, x, y);
01375   Expr right = Expr(kind, x + z, y + z);
01376   if(withProof()) pf = newPf("plus_predicate",left,right);
01377   return newRWTheorem(left, right, Assumptions::emptyAssump(), pf);
01378 }
01379 
01380 // x = y <==> x * z = y * z
01381 Theorem ArithTheoremProducer3::multEqn(const Expr& x,
01382                                       const Expr& y,
01383                                       const Expr& z) {
01384   Proof pf;
01385   if(CHECK_PROOFS)
01386     CHECK_SOUND(z.isRational() && z.getRational() != 0,
01387     "ArithTheoremProducer3::multEqn(): multiplying equation by 0");
01388   if(withProof()) pf = newPf("mult_eqn", x, y, z);
01389   return newRWTheorem(x.eqExpr(y), (x * z).eqExpr(y * z), Assumptions::emptyAssump(), pf);
01390 }
01391 
01392 
01393 // x = y <==> z=0 OR x * 1/z = y * 1/z
01394 Theorem ArithTheoremProducer3::divideEqnNonConst(const Expr& x,
01395                                                    const Expr& y,
01396                                                    const Expr& z) {
01397   Proof pf;
01398   if(withProof()) pf = newPf("mult_eqn_nonconst", x, y, z);
01399   return newRWTheorem(x.eqExpr(y), (z.eqExpr(rat(0))).orExpr((x / z).eqExpr(y / z)),
01400                       Assumptions::emptyAssump(), pf);
01401 }
01402 
01403 
01404 // if z is +ve, return e[0] LT|LE|GT|GE e[1] <==> e[0]*z LT|LE|GT|GE e[1]*z
01405 // if z is -ve, return e[0] LT|LE|GT|GE e[1] <==> e[1]*z LT|LE|GT|GE e[0]*z
01406 Theorem ArithTheoremProducer3::multIneqn(const Expr& e, const Expr& z)
01407 {
01408   int kind = e.getKind();
01409 
01410   if(CHECK_PROOFS) {
01411     CHECK_SOUND((LT==kind) ||
01412                 (LE==kind) ||
01413                 (GE==kind) ||
01414                 (GT==kind),
01415                 "ArithTheoremProducer3::multIneqn: wrong kind");
01416     CHECK_SOUND(z.isRational() && z.getRational() != 0,
01417                 "ArithTheoremProducer3::multIneqn: "
01418     "z must be non-zero rational: " + z.toString());
01419   }
01420   Op op(e.getOp());
01421   Proof pf;
01422 
01423   Expr ret;
01424   if(0 < z.getRational())
01425     ret = Expr(op, e[0]*z, e[1]*z);
01426   else
01427     ret = Expr(op, e[1]*z, e[0]*z);
01428   if(withProof()) pf = newPf("mult_ineqn", e, ret);
01429   return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
01430 }
01431 
01432 
01433 Theorem ArithTheoremProducer3::eqToIneq(const Expr& e) {
01434 
01435     // Check soundness of the rule if necessary
01436   if (CHECK_PROOFS)
01437     CHECK_SOUND(e.isEq(), "eqToIneq: input must be an equality: " + e.toString());
01438 
01439     // The proof object we will use
01440     Proof pf;
01441 
01442   // The parts of the equality x = y
01443     const Expr& x = e[0];
01444     const Expr& y = e[1];
01445 
01446   // Setup the proof if needed
01447     if (withProof())
01448       pf = newPf("eqToIneq", e);
01449 
01450     // Retrun the theorem explaining the transformation
01451   return newRWTheorem(e, leExpr(x,y).andExpr(geExpr(x,y)), Assumptions::emptyAssump(), pf);
01452 }
01453 
01454 // "op1 GE|GT op2" <==> op2 LE|LT op1
01455 Theorem ArithTheoremProducer3::flipInequality(const Expr& e)
01456 {
01457   Proof pf;
01458   if(CHECK_PROOFS) {
01459     CHECK_SOUND(isGT(e) || isGE(e),
01460                 "ArithTheoremProducer3::flipInequality: wrong kind: " +
01461                 e.toString());
01462   }
01463 
01464   int kind = isGE(e) ? LE : LT;
01465   Expr ret =  Expr(kind, e[1], e[0]);
01466   if(withProof()) pf = newPf("flip_inequality", e,ret);
01467   return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
01468 }
01469 
01470 
01471 // NOT (op1 LT op2)  <==> (op1 GE op2)
01472 // NOT (op1 LE op2)  <==> (op1 GT op2)
01473 // NOT (op1 GT op2)  <==> (op1 LE op2)
01474 // NOT (op1 GE op2)  <==> (op1 LT op2)
01475 Theorem ArithTheoremProducer3::negatedInequality(const Expr& e)
01476 {
01477   const Expr& ineq = e[0];
01478   if(CHECK_PROOFS) {
01479     CHECK_SOUND(e.isNot(),
01480                 "ArithTheoremProducer3::negatedInequality: wrong kind: " +
01481                 e.toString());
01482     CHECK_SOUND(isIneq(ineq),
01483                 "ArithTheoremProducer3::negatedInequality: wrong kind: " +
01484                 (ineq).toString());
01485   }
01486   Proof pf;
01487   if(withProof()) pf = newPf("negated_inequality", e);
01488 
01489   int kind;
01490   // NOT (op1 LT op2)  <==> (op1 GE op2)
01491   // NOT (op1 LE op2)  <==> (op1 GT op2)
01492   // NOT (op1 GT op2)  <==> (op1 LE op2)
01493   // NOT (op1 GE op2)  <==> (op1 LT op2)
01494   kind =
01495     isLT(ineq) ? GE :
01496     isLE(ineq) ? GT :
01497     isGT(ineq) ? LE :
01498     LT;
01499   return newRWTheorem(e, Expr(kind, ineq[0], ineq[1]), Assumptions::emptyAssump(), pf);
01500 }
01501 
01502 //takes two ineqs "|- alpha LT|LE t" and "|- t LT|LE beta"
01503 //and returns "|- alpha LT|LE beta"
01504 Theorem ArithTheoremProducer3::realShadow(const Theorem& alphaLTt,
01505                                          const Theorem& tLTbeta)
01506 {
01507   const Expr& expr1 = alphaLTt.getExpr();
01508   const Expr& expr2 = tLTbeta.getExpr();
01509   if(CHECK_PROOFS) {
01510     CHECK_SOUND((isLE(expr1) || isLT(expr1)) &&
01511                 (isLE(expr2) || isLT(expr2)),
01512                 "ArithTheoremProducer3::realShadow: Wrong Kind: " +
01513                 alphaLTt.toString() +  tLTbeta.toString());
01514 
01515     CHECK_SOUND(expr1[1] == expr2[0],
01516                 "ArithTheoremProducer3::realShadow:"
01517                 " t must be same for both inputs: " +
01518                 expr1[1].toString() + " , " + expr2[0].toString());
01519   }
01520   Assumptions a(alphaLTt, tLTbeta);
01521   int firstKind = expr1.getKind();
01522   int secondKind = expr2.getKind();
01523   int kind = (firstKind == secondKind) ? firstKind : LT;
01524   Proof pf;
01525   if(withProof()) {
01526     vector<Proof> pfs;
01527     pfs.push_back(alphaLTt.getProof());
01528     pfs.push_back(tLTbeta.getProof());
01529     pf = newPf("real_shadow",expr1, expr2, pfs);
01530   }
01531   return newTheorem(Expr(kind, expr1[0], expr2[1]), a, pf);
01532 }
01533 
01534 //! alpha <= t <= alpha ==> t = alpha
01535 
01536 /*! takes two ineqs "|- alpha LE t" and "|- t LE alpha"
01537   and returns "|- t = alpha"
01538 */
01539 Theorem ArithTheoremProducer3::realShadowEq(const Theorem& alphaLEt,
01540                                            const Theorem& tLEalpha)
01541 {
01542   const Expr& expr1 = alphaLEt.getExpr();
01543   const Expr& expr2 = tLEalpha.getExpr();
01544   if(CHECK_PROOFS) {
01545     CHECK_SOUND(isLE(expr1) && isLE(expr2),
01546                 "ArithTheoremProducer3::realShadowLTLE: Wrong Kind: " +
01547                 alphaLEt.toString() +  tLEalpha.toString());
01548 
01549     CHECK_SOUND(expr1[1] == expr2[0],
01550                 "ArithTheoremProducer3::realShadowLTLE:"
01551                 " t must be same for both inputs: " +
01552                 alphaLEt.toString() + " , " + tLEalpha.toString());
01553 
01554     CHECK_SOUND(expr1[0] == expr2[1],
01555                 "ArithTheoremProducer3::realShadowLTLE:"
01556                 " alpha must be same for both inputs: " +
01557                 alphaLEt.toString() + " , " + tLEalpha.toString());
01558   }
01559   Assumptions a(alphaLEt, tLEalpha);
01560   Proof pf;
01561   if(withProof()) {
01562     vector<Proof> pfs;
01563     pfs.push_back(alphaLEt.getProof());
01564     pfs.push_back(tLEalpha.getProof());
01565     pf = newPf("real_shadow_eq", alphaLEt.getExpr(), tLEalpha.getExpr(), pfs);
01566   }
01567   return newRWTheorem(expr1[0], expr1[1], a, pf);
01568 }
01569 
01570 Theorem
01571 ArithTheoremProducer3::finiteInterval(const Theorem& aLEt,
01572              const Theorem& tLEac,
01573              const Theorem& isInta,
01574              const Theorem& isIntt) {
01575   const Expr& e1 = aLEt.getExpr();
01576   const Expr& e2 = tLEac.getExpr();
01577   if(CHECK_PROOFS) {
01578     CHECK_SOUND(isLE(e1) && isLE(e2),
01579     "ArithTheoremProducer3::finiteInterval:\n e1 = "
01580     +e1.toString()+"\n e2 = "+e2.toString());
01581     // term 't' is the same in both inequalities
01582     CHECK_SOUND(e1[1] == e2[0],
01583     "ArithTheoremProducer3::finiteInterval:\n e1 = "
01584     +e1.toString()+"\n e2 = "+e2.toString());
01585     // RHS in e2 is (a+c)
01586     CHECK_SOUND(isPlus(e2[1]) && e2[1].arity() == 2,
01587     "ArithTheoremProducer3::finiteInterval:\n e1 = "
01588     +e1.toString()+"\n e2 = "+e2.toString());
01589     // term 'a' in LHS of e1 and RHS of e2 is the same
01590     CHECK_SOUND(e1[0] == e2[1][0],
01591     "ArithTheoremProducer3::finiteInterval:\n e1 = "
01592     +e1.toString()+"\n e2 = "+e2.toString());
01593     // 'c' in the RHS of e2 is a positive integer constant
01594     CHECK_SOUND(e2[1][1].isRational() && e2[1][1].getRational().isInteger()
01595     && e2[1][1].getRational() >= 1,
01596     "ArithTheoremProducer3::finiteInterval:\n e1 = "
01597     +e1.toString()+"\n e2 = "+e2.toString());
01598     // Integrality constraints
01599     const Expr& isIntaExpr = isInta.getExpr();
01600     const Expr& isInttExpr = isIntt.getExpr();
01601     CHECK_SOUND(isIntPred(isIntaExpr) && isIntaExpr[0] == e1[0],
01602     "Wrong integrality constraint:\n e1 = "
01603     +e1.toString()+"\n isInta = "+isIntaExpr.toString());
01604     CHECK_SOUND(isIntPred(isInttExpr) && isInttExpr[0] == e1[1],
01605     "Wrong integrality constraint:\n e1 = "
01606     +e1.toString()+"\n isIntt = "+isInttExpr.toString());
01607   }
01608   vector<Theorem> thms;
01609   thms.push_back(aLEt);
01610   thms.push_back(tLEac);
01611   thms.push_back(isInta);
01612   thms.push_back(isIntt);
01613   Assumptions a(thms);
01614   Proof pf;
01615   if(withProof()) {
01616     vector<Expr> es;
01617     vector<Proof> pfs;
01618     es.push_back(e1);
01619     es.push_back(e2);
01620     es.push_back(isInta.getExpr());
01621     es.push_back(isIntt.getExpr());
01622     pfs.push_back(aLEt.getProof());
01623     pfs.push_back(tLEac.getProof());
01624     pfs.push_back(isInta.getProof());
01625     pfs.push_back(isIntt.getProof());
01626     pf = newPf("finite_interval", es, pfs);
01627   }
01628   // Construct GRAY_SHADOW(t, a, 0, c)
01629   Expr g(grayShadow(e1[1], e1[0], 0, e2[1][1].getRational()));
01630   return newTheorem(g, a, pf);
01631 }
01632 
01633 
01634 // Dark & Gray shadows when a <= b
01635 Theorem ArithTheoremProducer3::darkGrayShadow2ab(const Theorem& betaLEbx,
01636             const Theorem& axLEalpha,
01637             const Theorem& isIntAlpha,
01638             const Theorem& isIntBeta,
01639             const Theorem& isIntx) {
01640   const Expr& expr1 = betaLEbx.getExpr();
01641   const Expr& expr2 = axLEalpha.getExpr();
01642   const Expr& isIntAlphaExpr = isIntAlpha.getExpr();
01643   const Expr& isIntBetaExpr = isIntBeta.getExpr();
01644   const Expr& isIntxExpr = isIntx.getExpr();
01645 
01646   if(CHECK_PROOFS) {
01647     CHECK_SOUND(isLE(expr1) && isLE(expr2),
01648                 "ArithTheoremProducer3::darkGrayShadow2ab: Wrong Kind: " +
01649                 betaLEbx.toString() +  axLEalpha.toString());
01650   }
01651 
01652   const Expr& beta = expr1[0];
01653   const Expr& bx = expr1[1];
01654   const Expr& ax = expr2[0];
01655   const Expr& alpha = expr2[1];
01656   Rational a = isMult(ax)? ax[0].getRational() : 1;
01657   Rational b = isMult(bx)? bx[0].getRational() : 1;
01658   const Expr& x = isMult(ax)? ax[1] : ax;
01659 
01660   if(CHECK_PROOFS) {
01661     // Integrality constraints
01662     CHECK_SOUND(isIntPred(isIntAlphaExpr) && isIntAlphaExpr[0] == alpha,
01663     "ArithTheoremProducer3::darkGrayShadow2ab:\n "
01664     "wrong integrality constraint:\n alpha = "
01665     +alpha.toString()+"\n isIntAlpha = "
01666     +isIntAlphaExpr.toString());
01667     CHECK_SOUND(isIntPred(isIntBetaExpr) && isIntBetaExpr[0] == beta,
01668     "ArithTheoremProducer3::darkGrayShadow2ab:\n "
01669     "wrong integrality constraint:\n beta = "
01670     +beta.toString()+"\n isIntBeta = "
01671     +isIntBetaExpr.toString());
01672     CHECK_SOUND(isIntPred(isIntxExpr) && isIntxExpr[0] == x,
01673     "ArithTheoremProducer3::darkGrayShadow2ab:\n "
01674     "wrong integrality constraint:\n x = "
01675     +x.toString()+"\n isIntx = "
01676     +isIntxExpr.toString());
01677     // Expressions ax and bx should match on x
01678     CHECK_SOUND(!isMult(ax) || ax.arity() == 2,
01679     "ArithTheoremProducer3::darkGrayShadow2ab:\n ax<=alpha: " +
01680                 axLEalpha.toString());
01681     CHECK_SOUND(!isMult(bx) || (bx.arity() == 2 && bx[1] == x),
01682     "ArithTheoremProducer3::darkGrayShadow2ab:\n beta<=bx: "
01683     +betaLEbx.toString()
01684     +"\n ax<=alpha: "+ axLEalpha.toString());
01685     CHECK_SOUND(1 <= a && a <= b && 2 <= b,
01686     "ArithTheoremProducer3::darkGrayShadow2ab:\n beta<=bx: "
01687     +betaLEbx.toString()
01688     +"\n ax<=alpha: "+ axLEalpha.toString());
01689   }
01690   vector<Theorem> thms;
01691   thms.push_back(betaLEbx);
01692   thms.push_back(axLEalpha);
01693   thms.push_back(isIntAlpha);
01694   thms.push_back(isIntBeta);
01695   thms.push_back(isIntx);
01696   Assumptions A(thms);
01697 
01698   Expr bAlpha = multExpr(rat(b), alpha);
01699   Expr aBeta = multExpr(rat(a), beta);
01700   Expr t = minusExpr(bAlpha, aBeta);
01701   Expr d = darkShadow(rat(a*b-1), t);
01702   Expr g = grayShadow(ax, alpha, -a+1, 0);
01703 
01704   Proof pf;
01705   if(withProof()) {
01706     vector<Expr> exprs;
01707     exprs.push_back(expr1);
01708     exprs.push_back(expr2);
01709     exprs.push_back(d);
01710     exprs.push_back(g);
01711 
01712     vector<Proof> pfs;
01713     pfs.push_back(betaLEbx.getProof());
01714     pfs.push_back(axLEalpha.getProof());
01715     pfs.push_back(isIntAlpha.getProof());
01716     pfs.push_back(isIntBeta.getProof());
01717     pfs.push_back(isIntx.getProof());
01718 
01719     pf = newPf("dark_grayshadow_2ab", exprs, pfs);
01720   }
01721 
01722   return newTheorem((d || g), A, pf);
01723 }
01724 
01725 // Dark & Gray shadows when b <= a
01726 Theorem ArithTheoremProducer3::darkGrayShadow2ba(const Theorem& betaLEbx,
01727             const Theorem& axLEalpha,
01728             const Theorem& isIntAlpha,
01729             const Theorem& isIntBeta,
01730             const Theorem& isIntx) {
01731   const Expr& expr1 = betaLEbx.getExpr();
01732   const Expr& expr2 = axLEalpha.getExpr();
01733   const Expr& isIntAlphaExpr = isIntAlpha.getExpr();
01734   const Expr& isIntBetaExpr = isIntBeta.getExpr();
01735   const Expr& isIntxExpr = isIntx.getExpr();
01736 
01737   if(CHECK_PROOFS) {
01738     CHECK_SOUND(isLE(expr1) && isLE(expr2),
01739                 "ArithTheoremProducer3::darkGrayShadow2ba: Wrong Kind: " +
01740                 betaLEbx.toString() +  axLEalpha.toString());
01741   }
01742 
01743   const Expr& beta = expr1[0];
01744   const Expr& bx = expr1[1];
01745   const Expr& ax = expr2[0];
01746   const Expr& alpha = expr2[1];
01747   Rational a = isMult(ax)? ax[0].getRational() : 1;
01748   Rational b = isMult(bx)? bx[0].getRational() : 1;
01749   const Expr& x = isMult(ax)? ax[1] : ax;
01750 
01751   if(CHECK_PROOFS) {
01752     // Integrality constraints
01753     CHECK_SOUND(isIntPred(isIntAlphaExpr) && isIntAlphaExpr[0] == alpha,
01754     "ArithTheoremProducer3::darkGrayShadow2ab:\n "
01755     "wrong integrality constraint:\n alpha = "
01756     +alpha.toString()+"\n isIntAlpha = "
01757     +isIntAlphaExpr.toString());
01758     CHECK_SOUND(isIntPred(isIntBetaExpr) && isIntBetaExpr[0] == beta,
01759     "ArithTheoremProducer3::darkGrayShadow2ab:\n "
01760     "wrong integrality constraint:\n beta = "
01761     +beta.toString()+"\n isIntBeta = "
01762     +isIntBetaExpr.toString());
01763     CHECK_SOUND(isIntPred(isIntxExpr) && isIntxExpr[0] == x,
01764     "ArithTheoremProducer3::darkGrayShadow2ab:\n "
01765     "wrong integrality constraint:\n x = "
01766     +x.toString()+"\n isIntx = "
01767     +isIntxExpr.toString());
01768     // Expressions ax and bx should match on x
01769     CHECK_SOUND(!isMult(ax) || ax.arity() == 2,
01770     "ArithTheoremProducer3::darkGrayShadow2ba:\n ax<=alpha: " +
01771                 axLEalpha.toString());
01772     CHECK_SOUND(!isMult(bx) || (bx.arity() == 2 && bx[1] == x),
01773     "ArithTheoremProducer3::darkGrayShadow2ba:\n beta<=bx: "
01774     +betaLEbx.toString()
01775     +"\n ax<=alpha: "+ axLEalpha.toString());
01776     CHECK_SOUND(1 <= b && b <= a && 2 <= a,
01777     "ArithTheoremProducer3::darkGrayShadow2ba:\n beta<=bx: "
01778     +betaLEbx.toString()
01779     +"\n ax<=alpha: "+ axLEalpha.toString());
01780   }
01781   vector<Theorem> thms;
01782   thms.push_back(betaLEbx);
01783   thms.push_back(axLEalpha);
01784   thms.push_back(isIntAlpha);
01785   thms.push_back(isIntBeta);
01786   thms.push_back(isIntx);
01787   Assumptions A(thms);
01788   Proof pf;
01789   if(withProof()) {
01790     vector<Proof> pfs;
01791     pfs.push_back(betaLEbx.getProof());
01792     pfs.push_back(axLEalpha.getProof());
01793     pfs.push_back(isIntAlpha.getProof());
01794     pfs.push_back(isIntBeta.getProof());
01795     pfs.push_back(isIntx.getProof());
01796 
01797     pf = newPf("dark_grayshadow_2ba", betaLEbx.getExpr(),
01798          axLEalpha.getExpr(), pfs);
01799   }
01800 
01801   Expr bAlpha = multExpr(rat(b), alpha);
01802   Expr aBeta = multExpr(rat(a), beta);
01803   Expr t = minusExpr(bAlpha, aBeta);
01804   Expr d = darkShadow(rat(a*b-1), t);
01805   Expr g = grayShadow(bx, beta, 0, b-1);
01806   return newTheorem((d || g), A, pf);
01807 }
01808 
01809 /*! takes a dark shadow and expands it into an inequality.
01810 */
01811 Theorem ArithTheoremProducer3::expandDarkShadow(const Theorem& darkShadow) {
01812   const Expr& theShadow = darkShadow.getExpr();
01813   if(CHECK_PROOFS){
01814     CHECK_SOUND(isDarkShadow(theShadow),
01815     "ArithTheoremProducer3::expandDarkShadow: not DARK_SHADOW: " +
01816     theShadow.toString());
01817   }
01818   Proof pf;
01819   if(withProof())
01820     pf = newPf("expand_dark_shadow", theShadow, darkShadow.getProof());
01821   return newTheorem(leExpr(theShadow[0], theShadow[1]), darkShadow.getAssumptionsRef(), pf);
01822 }
01823 
01824 
01825 // takes a grayShadow (c1==c2) and expands it into an equality
01826 Theorem ArithTheoremProducer3::expandGrayShadow0(const Theorem& grayShadow) {
01827   const Expr& theShadow = grayShadow.getExpr();
01828   if(CHECK_PROOFS) {
01829     CHECK_SOUND(isGrayShadow(theShadow),
01830     "ArithTheoremProducer3::expandGrayShadowConst0:"
01831     " not GRAY_SHADOW: " +
01832     theShadow.toString());
01833     CHECK_SOUND(theShadow[2] == theShadow[3],
01834     "ArithTheoremProducer3::expandGrayShadow0: c1!=c2: " +
01835     theShadow.toString());
01836   }
01837   Proof pf;
01838   if(withProof()) pf = newPf("expand_gray_shadowconst0", theShadow,
01839            grayShadow.getProof());
01840   const Expr& v = theShadow[0];
01841   const Expr& e = theShadow[1];
01842   return newRWTheorem(v, e + theShadow[2], grayShadow.getAssumptionsRef(), pf);
01843 }
01844 
01845 
01846 // G ==> (G1 or G2) and (!G1 or !G2),
01847 // where G  = G(x, e, c1, c2),
01848 //       G1 = G(x,e,c1,c)
01849 //       G2 = G(x,e,c+1,c2),
01850 // and    c = floor((c1+c2)/2)
01851 // DEJAN: TRY THE MIDDLE IMMEDIATELY, WE MIGHT GET LUCKY
01852 Theorem ArithTheoremProducer3::splitGrayShadow(const Theorem& gThm) {
01853   const Expr& theShadow = gThm.getExpr();
01854   if(CHECK_PROOFS) {
01855     CHECK_SOUND(isGrayShadow(theShadow),
01856     "ArithTheoremProducer3::expandGrayShadowConst: not a shadow" +
01857     theShadow.toString());
01858   }
01859 
01860   const Rational& c1 = theShadow[2].getRational();
01861   const Rational& c2 = theShadow[3].getRational();
01862 
01863   if(CHECK_PROOFS) {
01864     CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
01865     "ArithTheoremProducer3::expandGrayShadow: " +
01866     theShadow.toString());
01867   }
01868 
01869   const Expr& v = theShadow[0];
01870   const Expr& e = theShadow[1];
01871 
01872   Proof pf;
01873   Rational c(floor((c1+c2) / 2));
01874   Expr g1(grayShadow(v, e, c1, c));
01875   Expr g2(grayShadow(v, e, c+1, c2));
01876 
01877   if(withProof()){
01878     vector<Expr> exprs;
01879     exprs.push_back(theShadow);
01880     exprs.push_back(g1);
01881     exprs.push_back(g2);
01882     pf = newPf("split_gray_shadow", exprs, gThm.getProof());
01883   }
01884 
01885   return newTheorem((g1 || g2) && (!g1 || !g2), gThm.getAssumptionsRef(), pf);
01886 }
01887 
01888 
01889 Theorem ArithTheoremProducer3::expandGrayShadow(const Theorem& gThm) {
01890   const Expr& theShadow = gThm.getExpr();
01891   if(CHECK_PROOFS) {
01892     CHECK_SOUND(isGrayShadow(theShadow),
01893     "ArithTheoremProducer3::expandGrayShadowConst: not a shadow" +
01894     theShadow.toString());
01895   }
01896 
01897   const Rational& c1 = theShadow[2].getRational();
01898   const Rational& c2 = theShadow[3].getRational();
01899 
01900   if(CHECK_PROOFS) {
01901     CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
01902     "ArithTheoremProducer3::expandGrayShadow: " +
01903     theShadow.toString());
01904   }
01905 
01906   const Expr& v = theShadow[0];
01907   const Expr& e = theShadow[1];
01908 
01909   Proof pf;
01910   if(withProof())
01911     pf = newPf("expand_gray_shadow", theShadow, gThm.getProof());
01912   Expr ineq1(leExpr(e+rat(c1), v));
01913   Expr ineq2(leExpr(v, e+rat(c2)));
01914   return newTheorem(ineq1 && ineq2, gThm.getAssumptionsRef(), pf);
01915 }
01916 
01917 
01918 // Expanding GRAY_SHADOW(a*x, c, b), where c is a constant
01919 Theorem
01920 ArithTheoremProducer3::expandGrayShadowConst(const Theorem& gThm) {
01921   const Expr& theShadow = gThm.getExpr();
01922   const Expr& ax = theShadow[0];
01923   const Expr& cExpr = theShadow[1];
01924   const Expr& bExpr = theShadow[2];
01925 
01926   if(CHECK_PROOFS) {
01927     CHECK_SOUND(!isMult(ax) || ax[0].isRational(),
01928     "ArithTheoremProducer3::expandGrayShadowConst: "
01929     "'a' in a*x is not a const: " +theShadow.toString());
01930   }
01931 
01932   Rational a = isMult(ax)? ax[0].getRational() : 1;
01933 
01934   if(CHECK_PROOFS) {
01935     CHECK_SOUND(isGrayShadow(theShadow),
01936     "ArithTheoremProducer3::expandGrayShadowConst: "
01937     "not a GRAY_SHADOW: " +theShadow.toString());
01938     CHECK_SOUND(a.isInteger() && a >= 1,
01939     "ArithTheoremProducer3::expandGrayShadowConst: "
01940     "'a' is not integer: " +theShadow.toString());
01941     CHECK_SOUND(cExpr.isRational(),
01942     "ArithTheoremProducer3::expandGrayShadowConst: "
01943     "'c' is not rational" +theShadow.toString());
01944     CHECK_SOUND(bExpr.isRational() && bExpr.getRational().isInteger(),
01945     "ArithTheoremProducer3::expandGrayShadowConst: b not integer: "
01946     +theShadow.toString());
01947   }
01948 
01949   const Rational& b = bExpr.getRational();
01950   const Rational& c = cExpr.getRational();
01951   Rational j = constRHSGrayShadow(c,b,a);
01952   // Compute sign(b)*j(c,b,a)
01953   Rational signB = (b>0)? 1 : -1;
01954   // |b| (absolute value of b)
01955   Rational bAbs = abs(b);
01956 
01957   const Assumptions& assump(gThm.getAssumptionsRef());
01958   Proof pf;
01959   Theorem conc;  // Conclusion of the rule
01960 
01961   if(bAbs < j) {
01962     if(withProof())
01963       pf = newPf("expand_gray_shadow_const_0", theShadow,
01964      gThm.getProof());
01965     conc = newTheorem(d_em->falseExpr(), assump, pf);
01966   } else if(bAbs < a+j) {
01967     if(withProof())
01968       pf = newPf("expand_gray_shadow_const_1", theShadow,
01969      gThm.getProof());
01970     conc = newRWTheorem(ax, rat(c+b-signB*j), assump, pf);
01971   } else {
01972     if(withProof())
01973       pf = newPf("expand_gray_shadow_const", theShadow,
01974      gThm.getProof());
01975     Expr newGrayShadow(Expr(GRAY_SHADOW, ax, cExpr, rat(b-signB*(a+j))));
01976     conc = newTheorem(ax.eqExpr(rat(c+b-signB*j)).orExpr(newGrayShadow),
01977           assump, pf);
01978   }
01979 
01980   return conc;
01981 }
01982 
01983 
01984 Theorem
01985 ArithTheoremProducer3::grayShadowConst(const Theorem& gThm) {
01986   const Expr& g = gThm.getExpr();
01987   bool checkProofs(CHECK_PROOFS);
01988   if(checkProofs) {
01989     CHECK_SOUND(isGrayShadow(g), "ArithTheoremProducer3::grayShadowConst("
01990     +g.toString()+")");
01991   }
01992 
01993   const Expr& ax = g[0];
01994   const Expr& e = g[1];
01995   const Rational& c1 = g[2].getRational();
01996   const Rational& c2 = g[3].getRational();
01997   Expr aExpr, x;
01998   d_theoryArith->separateMonomial(ax, aExpr, x);
01999 
02000   if(checkProofs) {
02001     CHECK_SOUND(e.isRational() && e.getRational().isInteger(),
02002     "ArithTheoremProducer3::grayShadowConst("+g.toString()+")");
02003     CHECK_SOUND(aExpr.isRational(),
02004     "ArithTheoremProducer3::grayShadowConst("+g.toString()+")");
02005   }
02006 
02007   const Rational& a = aExpr.getRational();
02008   const Rational& c = e.getRational();
02009 
02010   if(checkProofs) {
02011     CHECK_SOUND(a.isInteger() && a >= 2,
02012     "ArithTheoremProducer3::grayShadowConst("+g.toString()+")");
02013   }
02014 
02015   Rational newC1 = ceil((c1+c)/a), newC2 = floor((c2+c)/a);
02016   Expr newG((newC1 > newC2)? d_em->falseExpr()
02017       : grayShadow(x, rat(0), newC1, newC2));
02018   Proof pf;
02019   if(withProof())
02020     pf = newPf("gray_shadow_const", g, newG, gThm.getProof());
02021   return newTheorem(newG, gThm.getAssumptionsRef(), pf);
02022 }
02023 
02024 
02025 Rational ArithTheoremProducer3::constRHSGrayShadow(const Rational& c,
02026               const Rational& b,
02027               const Rational& a) {
02028   DebugAssert(c.isInteger() &&
02029         b.isInteger() &&
02030         a.isInteger() &&
02031         b != 0,
02032         "ArithTheoremProducer3::constRHSGrayShadow: a, b, c must be ints");
02033   if (b > 0)
02034     return mod(c+b, a);
02035   else
02036     return mod(a-(c+b), a);
02037 }
02038 
02039 /*! Takes a Theorem(\\alpha < \\beta) and returns
02040  *  Theorem(\\alpha < \\beta <==> \\alpha <= \\beta -1)
02041  * where \\alpha and \\beta are integer expressions
02042  */
02043 Theorem ArithTheoremProducer3::lessThanToLE(const Theorem& less,
02044              const Theorem& isIntLHS,
02045              const Theorem& isIntRHS,
02046              bool changeRight) {
02047   const Expr& ineq = less.getExpr();
02048   const Expr& isIntLHSexpr = isIntLHS.getExpr();
02049   const Expr& isIntRHSexpr = isIntRHS.getExpr();
02050 
02051   if(CHECK_PROOFS) {
02052     CHECK_SOUND(isLT(ineq),
02053     "ArithTheoremProducer3::LTtoLE: ineq must be <");
02054     // Integrality check
02055     CHECK_SOUND(isIntPred(isIntLHSexpr) && isIntLHSexpr[0] == ineq[0],
02056     "ArithTheoremProducer3::lessThanToLE: bad integrality check:\n"
02057     " ineq = "+ineq.toString()+"\n isIntLHS = "
02058     +isIntLHSexpr.toString());
02059     CHECK_SOUND(isIntPred(isIntRHSexpr) && isIntRHSexpr[0] == ineq[1],
02060     "ArithTheoremProducer3::lessThanToLE: bad integrality check:\n"
02061     " ineq = "+ineq.toString()+"\n isIntRHS = "
02062     +isIntRHSexpr.toString());
02063   }
02064   vector<Theorem> thms;
02065   thms.push_back(less);
02066   thms.push_back(isIntLHS);
02067   thms.push_back(isIntRHS);
02068   Assumptions a(thms);
02069   Proof pf;
02070   Expr le = changeRight?
02071     leExpr(ineq[0], ineq[1] + rat(-1))
02072     : leExpr(ineq[0] + rat(1), ineq[1]);
02073   if(withProof()) {
02074     vector<Proof> pfs;
02075     pfs.push_back(less.getProof());
02076     pfs.push_back(isIntLHS.getProof());
02077     pfs.push_back(isIntRHS.getProof());
02078     pf = newPf(changeRight? "lessThan_To_LE_rhs" : "lessThan_To_LE_lhs",
02079          ineq,le, pfs);
02080   }
02081 
02082   return newRWTheorem(ineq, le, a, pf);
02083 }
02084 
02085 
02086 /*! \param eqn is an equation 0 = a.x or 0 = c + a.x
02087  *  \param isIntx is a proof of IS_INTEGER(x)
02088  *
02089  * \return the theorem 0 = c + a.x <==> x=-c/a if -c/a is int else
02090  *  return the theorem 0 = c + a.x <==> false.
02091  *
02092  * It also handles the special case of 0 = a.x <==> x = 0
02093  */
02094 Theorem
02095 ArithTheoremProducer3::intVarEqnConst(const Expr& eqn,
02096              const Theorem& isIntx) {
02097   const Expr& left(eqn[0]);
02098   const Expr& right(eqn[1]);
02099   const Expr& isIntxexpr(isIntx.getExpr());
02100 
02101   if(CHECK_PROOFS) {
02102     CHECK_SOUND((isMult(right) && right[0].isRational())
02103                 || (right.arity() == 2 && isPlus(right)
02104                     && right[0].isRational()
02105                     && ((!isMult(right[1]) || right[1][0].isRational()))),
02106                 "ArithTheoremProducer3::intVarEqnConst: "
02107     "rhs has a wrong format: " + right.toString());
02108     CHECK_SOUND(left.isRational() && 0 == left.getRational(),
02109                 "ArithTheoremProducer3:intVarEqnConst:left is not a zero: " +
02110                 left.toString());
02111   }
02112   // Integrality constraint
02113   Expr x(right);
02114   Rational a(1), c(0);
02115   if(isMult(right)) {
02116     Expr aExpr;
02117     d_theoryArith->separateMonomial(right, aExpr, x);
02118     a = aExpr.getRational();
02119   } else { // right is a PLUS
02120     c = right[0].getRational();
02121     Expr aExpr;
02122     d_theoryArith->separateMonomial(right[1], aExpr, x);
02123     a = aExpr.getRational();
02124   }
02125   if(CHECK_PROOFS) {
02126     CHECK_SOUND(isIntPred(isIntxexpr) && isIntxexpr[0] == x,
02127                 "ArithTheoremProducer3:intVarEqnConst: "
02128     "bad integrality constraint:\n right = " +
02129                 right.toString()+"\n isIntx = "+isIntxexpr.toString());
02130     CHECK_SOUND(a!=0, "ArithTheoremProducer3:intVarEqnConst: eqn = "
02131     +eqn.toString());
02132   }
02133   const Assumptions& assump(isIntx.getAssumptionsRef());
02134 
02135   /*
02136       Proof pf;
02137   if(withProof())
02138     pf = newPf("int_const_eq", eqn, isIntx.getProof());
02139 
02140   // Solve for x:   x = r = -c/a
02141   Rational r(-c/a);
02142 
02143   if(r.isInteger()){
02144     return newRWTheorem(eqn, x.eqExpr(rat(r)), assump, pf);
02145   else
02146     return newRWTheorem(eqn, d_em->falseExpr(), assump, pf);
02147   */
02148 
02149   Proof pf;
02150   // Solve for x:   x = r = -c/a
02151   Rational r(-c/a);
02152 
02153   if(r.isInteger()){
02154     if(withProof())
02155       pf = newPf("int_const_eq", eqn, x.eqExpr(rat(r)),isIntx.getProof());
02156     return newRWTheorem(eqn, x.eqExpr(rat(r)), assump, pf);
02157   }
02158   else{
02159     if(withProof())
02160       pf = newPf("int_const_eq", eqn, d_em->falseExpr(),isIntx.getProof());
02161     return newRWTheorem(eqn, d_em->falseExpr(), assump, pf);
02162   }
02163 }
02164 
02165 
02166 Expr
02167 ArithTheoremProducer3::create_t(const Expr& eqn) {
02168   const Expr& lhs = eqn[0];
02169   DebugAssert(isMult(lhs),
02170               CLASS_NAME "create_t : lhs must be a MULT"
02171               + lhs.toString());
02172   const Expr& x = lhs[1];
02173   Rational m = lhs[0].getRational()+1;
02174   DebugAssert(m > 0, "ArithTheoremProducer3::create_t: m = "+m.toString());
02175   vector<Expr> kids;
02176   if(isPlus(eqn[1]))
02177     sumModM(kids, eqn[1], m, m);
02178   else
02179     kids.push_back(monomialModM(eqn[1], m, m));
02180 
02181   kids.push_back(multExpr(rat(1/m), x));
02182   return plusExpr(kids);
02183 }
02184 
02185 Expr
02186 ArithTheoremProducer3::create_t2(const Expr& lhs, const Expr& rhs,
02187         const Expr& sigma) {
02188   Rational m = lhs[0].getRational()+1;
02189   DebugAssert(m > 0, "ArithTheoremProducer3::create_t2: m = "+m.toString());
02190   vector<Expr> kids;
02191   if(isPlus(rhs))
02192     sumModM(kids, rhs, m, -1);
02193   else {
02194     kids.push_back(rat(0)); // For canonical form
02195     Expr monom = monomialModM(rhs, m, -1);
02196     if(!monom.isRational())
02197       kids.push_back(monom);
02198     else
02199       DebugAssert(monom.getRational() == 0, "");
02200   }
02201   kids.push_back(rat(m)*sigma);
02202   return plusExpr(kids);
02203 }
02204 
02205 Expr
02206 ArithTheoremProducer3::create_t3(const Expr& lhs, const Expr& rhs,
02207         const Expr& sigma) {
02208   const Rational& a = lhs[0].getRational();
02209   Rational m = a+1;
02210   DebugAssert(m > 0, "ArithTheoremProducer3::create_t3: m = "+m.toString());
02211   vector<Expr> kids;
02212   if(isPlus(rhs))
02213     sumMulF(kids, rhs, m, 1);
02214   else {
02215     kids.push_back(rat(0)); // For canonical form
02216     Expr monom = monomialMulF(rhs, m, 1);
02217     if(!monom.isRational())
02218       kids.push_back(monom);
02219     else
02220       DebugAssert(monom.getRational() == 0, "");
02221   }
02222   kids.push_back(rat(-a)*sigma);
02223   return plusExpr(kids);
02224 }
02225 
02226 Rational
02227 ArithTheoremProducer3::modEq(const Rational& i, const Rational& m) {
02228   DebugAssert(m > 0, "ArithTheoremProducer3::modEq: m = "+m.toString());
02229   Rational half(1,2);
02230   Rational res((i - m*(floor((i/m) + half))));
02231   TRACE("arith eq", "modEq("+i.toString()+", "+m.toString()+") = ", res, "");
02232   return res;
02233 }
02234 
02235 Rational
02236 ArithTheoremProducer3::f(const Rational& i, const Rational& m) {
02237   DebugAssert(m > 0, "ArithTheoremProducer3::f: m = "+m.toString());
02238   Rational half(1,2);
02239   return (floor(i/m + half)+modEq(i,m));
02240 }
02241 
02242 void
02243 ArithTheoremProducer3::sumModM(vector<Expr>& summands, const Expr& sum,
02244                               const Rational& m, const Rational& divisor) {
02245   DebugAssert(divisor != 0, "ArithTheoremProducer3::sumModM: divisor = "
02246         +divisor.toString());
02247   Expr::iterator i = sum.begin();
02248   DebugAssert(i != sum.end(), CLASS_NAME "::sumModM");
02249   Rational C = i->getRational();
02250   C = modEq(C,m)/divisor;
02251   summands.push_back(rat(C));
02252   i++;
02253   for(Expr::iterator iend=sum.end(); i!=iend; ++i) {
02254     Expr monom = monomialModM(*i, m, divisor);
02255     if(!monom.isRational())
02256       summands.push_back(monom);
02257     else
02258       DebugAssert(monom.getRational() == 0, "");
02259   }
02260 }
02261 
02262 Expr
02263 ArithTheoremProducer3::monomialModM(const Expr& i,
02264                                    const Rational& m, const Rational& divisor)
02265 {
02266   DebugAssert(divisor != 0, "ArithTheoremProducer3::monomialModM: divisor = "
02267         +divisor.toString());
02268   Expr res;
02269   if(isMult(i)) {
02270     Rational ai = i[0].getRational();
02271     ai = modEq(ai,m)/divisor;
02272     if(0 == ai) res = rat(0);
02273     else if(1 == ai && i.arity() == 2) res = i[1];
02274     else {
02275       vector<Expr> kids = i.getKids();
02276       kids[0] = rat(ai);
02277       res = multExpr(kids);
02278     }
02279   } else { // It's a single variable
02280     Rational ai = modEq(1,m)/divisor;
02281     if(1 == ai) res = i;
02282     else res = rat(ai)*i;
02283   }
02284   DebugAssert(!res.isNull(), "ArithTheoremProducer3::monomialModM()");
02285   TRACE("arith eq", "monomialModM(i="+i.toString()+", m="+m.toString()
02286   +", div="+divisor.toString()+") = ", res, "");
02287   return res;
02288 }
02289 
02290 void
02291 ArithTheoremProducer3::sumMulF(vector<Expr>& summands, const Expr& sum,
02292                               const Rational& m, const Rational& divisor) {
02293   DebugAssert(divisor != 0, "ArithTheoremProducer3::sumMulF: divisor = "
02294         +divisor.toString());
02295   Expr::iterator i = sum.begin();
02296   DebugAssert(i != sum.end(), CLASS_NAME "::sumModM");
02297   Rational C = i->getRational();
02298   C = f(C,m)/divisor;
02299   summands.push_back(rat(C));
02300   i++;
02301   for(Expr::iterator iend=sum.end(); i!=iend; ++i) {
02302     Expr monom = monomialMulF(*i, m, divisor);
02303     if(!monom.isRational())
02304       summands.push_back(monom);
02305     else
02306       DebugAssert(monom.getRational() == 0, "");
02307   }
02308 }
02309 
02310 Expr
02311 ArithTheoremProducer3::monomialMulF(const Expr& i,
02312                                    const Rational& m, const Rational& divisor)
02313 {
02314   DebugAssert(divisor != 0, "ArithTheoremProducer3::monomialMulF: divisor = "
02315         +divisor.toString());
02316   Rational ai = isMult(i) ? (i)[0].getRational() : 1;
02317   Expr xi = isMult(i) ? (i)[1] : (i);
02318   ai = f(ai,m)/divisor;
02319   if(0 == ai) return rat(0);
02320   if(1 == ai) return xi;
02321   return multExpr(rat(ai), xi);
02322 }
02323 
02324 // This recursive function accepts a term, t, and a 'map' of
02325 // substitutions [x1/t1, x2/t2,...,xn/tn].  it returns a t' which is
02326 // basically t[x1/t1,x2/t2...xn/tn]
02327 Expr
02328 ArithTheoremProducer3::substitute(const Expr& term, ExprMap<Expr>& eMap)
02329 {
02330   ExprMap<Expr>::iterator i, iend = eMap.end();
02331 
02332   i = eMap.find(term);
02333   if(iend != i)
02334     return (*i).second;
02335 
02336   if (isMult(term)) {
02337     //in this case term is of the form c.x
02338     i = eMap.find(term[1]);
02339     if(iend != i)
02340       return term[0]*(*i).second;
02341     else
02342       return term;
02343   }
02344 
02345   if(isPlus(term)) {
02346     vector<Expr> output;
02347     for(Expr::iterator j = term.begin(), jend = term.end(); j != jend; ++j)
02348       output.push_back(substitute(*j, eMap));
02349     return plusExpr(output);
02350   }
02351   return term;
02352 }
02353 
02354 bool ArithTheoremProducer3::greaterthan(const Expr & l, const Expr & r)
02355 {
02356   //    DebugAssert(l != r, "");
02357   if (l==r) return false;
02358 
02359   switch(l.getKind()) {
02360   case RATIONAL_EXPR:
02361     DebugAssert(!r.isRational(), "");
02362     return true;
02363     break;
02364   case POW:
02365     switch (r.getKind()) {
02366     case RATIONAL_EXPR:
02367       // TODO:
02368       // alternately I could return (not greaterthan(r,l))
02369       return false;
02370       break;
02371     case POW:
02372       // x^n > y^n if x > y
02373       // x^n1 > x^n2 if n1 > n2
02374       return
02375         ((r[1] < l[1]) ||
02376          ((r[1]==l[1]) && (r[0].getRational() < l[0].getRational())));
02377       break;
02378 
02379     case MULT:
02380       DebugAssert(r.arity() > 1, "");
02381       DebugAssert((r.arity() > 2) || (r[1] != l), "");
02382       if (r[1] == l) return false;
02383       return greaterthan(l, r[1]);
02384       break;
02385     case PLUS:
02386       DebugAssert(false, "");
02387       return true;
02388       break;
02389     default:
02390       // leaf
02391       return ((r < l[1]) || ((r == l[1]) && l[0].getRational() > 1));
02392       break;
02393     }
02394     break;
02395   case MULT:
02396     DebugAssert(l.arity() > 1, "");
02397     switch (r.getKind()) {
02398     case RATIONAL_EXPR:
02399       return false;
02400       break;
02401     case POW:
02402       DebugAssert(l.arity() > 1, "");
02403       DebugAssert((l.arity() > 2) || (l[1] != r), "");
02404       // TODO:
02405       // alternately return (not greaterthan(r,l)
02406       return ((l[1] == r) || greaterthan(l[1], r));
02407       break;
02408     case MULT:
02409       {
02410 
02411         DebugAssert(r.arity() > 1, "");
02412         Expr::iterator i = l.begin();
02413         Expr::iterator j = r.begin();
02414         ++i;
02415         ++j;
02416         for (; i != l.end() && j != r.end(); ++i, ++j) {
02417           if (*i == *j)
02418             continue;
02419           return greaterthan(*i,*j);
02420         }
02421         DebugAssert(i != l.end() || j != r.end(), "");
02422         if (i == l.end()) {
02423           // r is bigger
02424           return false;
02425         }
02426         else
02427           {
02428             // l is bigger
02429             return true;
02430           }
02431       }
02432       break;
02433     case PLUS:
02434       DebugAssert(false, "");
02435       return true;
02436       break;
02437     default:
02438       // leaf
02439       DebugAssert((l.arity() > 2) || (l[1] != r), "");
02440       return ((l[1] == r) || greaterthan(l[1], r));
02441       break;
02442     }
02443     break;
02444   case PLUS:
02445     DebugAssert(false, "");
02446     return true;
02447     break;
02448   default:
02449     // leaf
02450     switch (r.getKind()) {
02451     case RATIONAL_EXPR:
02452       return false;
02453       break;
02454     case POW:
02455       return ((r[1] < l) || ((r[1] == l) && (r[0].getRational() < 1)));
02456       break;
02457     case MULT:
02458       DebugAssert(r.arity() > 1, "");
02459       DebugAssert((r.arity() > 2) || (r[1] != l), "");
02460       if (l == r[1]) return false;
02461       return greaterthan(l,r[1]);
02462       break;
02463     case PLUS:
02464       DebugAssert(false, "");
02465       return true;
02466       break;
02467     default:
02468       // leaf
02469       return (r < l);
02470       break;
02471     }
02472     break;
02473   }
02474 }
02475 
02476 
02477 /*! IS_INTEGER(x) |= EXISTS (y : INT) y = x
02478  * where x is not already known to be an integer.
02479  */
02480 Theorem ArithTheoremProducer3::IsIntegerElim(const Theorem& isIntx)
02481 {
02482   Expr expr = isIntx.getExpr();
02483   if (CHECK_PROOFS) {
02484     CHECK_SOUND(expr.getKind() == IS_INTEGER,
02485                 "Expected IS_INTEGER predicate");
02486   }
02487   expr = expr[0];
02488   DebugAssert(!d_theoryArith->isInteger(expr), "Expected non-integer");
02489 
02490   Assumptions a(isIntx);
02491   Proof pf;
02492 
02493   if (withProof())
02494   {
02495     pf = newPf("isIntElim", isIntx.getProof());
02496   }
02497 
02498   Expr newVar = d_em->newBoundVarExpr(d_theoryArith->intType());
02499   Expr res = d_em->newClosureExpr(EXISTS, newVar, newVar.eqExpr(expr));
02500 
02501   return newTheorem(res, a, pf);
02502 }
02503 
02504 
02505 Theorem
02506 ArithTheoremProducer3::eqElimIntRule(const Theorem& eqn, const Theorem& isIntx,
02507             const vector<Theorem>& isIntVars) {
02508   TRACE("arith eq", "eqElimIntRule(", eqn.getExpr(), ") {");
02509   Proof pf;
02510 
02511   if(CHECK_PROOFS)
02512     CHECK_SOUND(eqn.isRewrite(),
02513                 "ArithTheoremProducer3::eqElimInt: input must be an equation" +
02514                 eqn.toString());
02515 
02516   const Expr& lhs = eqn.getLHS();
02517   const Expr& rhs = eqn.getRHS();
02518   Expr a, x;
02519   d_theoryArith->separateMonomial(lhs, a, x);
02520 
02521   if(CHECK_PROOFS) {
02522     // Checking LHS
02523     const Expr& isIntxe = isIntx.getExpr();
02524     CHECK_SOUND(isIntPred(isIntxe) && isIntxe[0] == x,
02525     "ArithTheoremProducer3::eqElimInt\n eqn = "
02526     +eqn.getExpr().toString()
02527     +"\n isIntx = "+isIntxe.toString());
02528     CHECK_SOUND(isRational(a) && a.getRational().isInteger()
02529     && a.getRational() >= 2,
02530     "ArithTheoremProducer3::eqElimInt:\n lhs = "+lhs.toString());
02531     // Checking RHS
02532     // It cannot be a division (we don't handle it)
02533     CHECK_SOUND(!isDivide(rhs),
02534     "ArithTheoremProducer3::eqElimInt:\n rhs = "+rhs.toString());
02535     // If it's a single monomial, then it's the only "variable"
02536     if(!isPlus(rhs)) {
02537       Expr c, v;
02538       d_theoryArith->separateMonomial(rhs, c, v);
02539       CHECK_SOUND(isIntVars.size() == 1
02540       && isIntPred(isIntVars[0].getExpr())
02541       && isIntVars[0].getExpr()[0] == v
02542       && isRational(c) && c.getRational().isInteger(),
02543       "ArithTheoremProducer3::eqElimInt:\n rhs = "+rhs.toString()
02544       +"isIntVars.size = "+int2string(isIntVars.size()));
02545     } else { // RHS is a plus
02546       CHECK_SOUND(isIntVars.size() + 1 == (size_t)rhs.arity(),
02547       "ArithTheoremProducer3::eqElimInt: rhs = "+rhs.toString());
02548       // Check the free constant
02549       CHECK_SOUND(isRational(rhs[0]) && rhs[0].getRational().isInteger(),
02550       "ArithTheoremProducer3::eqElimInt: rhs = "+rhs.toString());
02551       // Check the vars
02552       for(size_t i=0, iend=isIntVars.size(); i<iend; ++i) {
02553   Expr c, v;
02554   d_theoryArith->separateMonomial(rhs[i+1], c, v);
02555   const Expr& isInt(isIntVars[i].getExpr());
02556   CHECK_SOUND(isIntPred(isInt) && isInt[0] == v
02557         && isRational(c) && c.getRational().isInteger(),
02558         "ArithTheoremProducer3::eqElimInt:\n rhs["+int2string(i+1)
02559         +"] = "+rhs[i+1].toString()
02560         +"\n isInt = "+isInt.toString());
02561       }
02562     }
02563   }
02564 
02565   // Creating a fresh bound variable
02566   static int varCount(0);
02567   Expr newVar = d_em->newBoundVarExpr("_int_var", int2string(varCount++));
02568   newVar.setType(intType());
02569   Expr t2 = create_t2(lhs, rhs, newVar);
02570   Expr t3 = create_t3(lhs, rhs, newVar);
02571   vector<Expr> vars;
02572   vars.push_back(newVar);
02573   Expr res = d_em->newClosureExpr(EXISTS, vars,
02574                                   x.eqExpr(t2) && rat(0).eqExpr(t3));
02575 
02576   vector<Theorem> thms(isIntVars);
02577   thms.push_back(isIntx);
02578   thms.push_back(eqn);
02579   Assumptions assump(thms);
02580 
02581   if(withProof()) {
02582     vector<Proof> pfs;
02583     pfs.push_back(eqn.getProof());
02584     pfs.push_back(isIntx.getProof());
02585     vector<Theorem>::const_iterator i=isIntVars.begin(), iend=isIntVars.end();
02586     for(; i!=iend; ++i)
02587       pfs.push_back(i->getProof());
02588     pf = newPf("eq_elim_int", eqn.getExpr(), res, pfs);
02589   }
02590 
02591   Theorem thm(newTheorem(res, assump, pf));
02592   TRACE("arith eq", "eqElimIntRule => ", thm.getExpr(), " }");
02593   return thm;
02594 }
02595 
02596 
02597 Theorem
02598 ArithTheoremProducer3::isIntConst(const Expr& e) {
02599   Proof pf;
02600 
02601   if(CHECK_PROOFS) {
02602     CHECK_SOUND(isIntPred(e) && e[0].isRational(),
02603     "ArithTheoremProducer3::isIntConst(e = "
02604     +e.toString()+")");
02605   }
02606   if(withProof())
02607     pf = newPf("is_int_const", e);
02608   bool isInt = e[0].getRational().isInteger();
02609   return newRWTheorem(e, isInt? d_em->trueExpr() : d_em->falseExpr(), Assumptions::emptyAssump(), pf);
02610 }
02611 
02612 
02613 Theorem
02614 ArithTheoremProducer3::equalLeaves1(const Theorem& thm)
02615 {
02616   Proof pf;
02617   const Expr& e = thm.getRHS();
02618 
02619   if (CHECK_PROOFS) {
02620     CHECK_SOUND(e[1].getKind() == RATIONAL_EXPR &&
02621     e[1].getRational() == Rational(0) &&
02622     e[0].getKind() == PLUS &&
02623     e[0].arity() == 3 &&
02624     e[0][0].getKind() == RATIONAL_EXPR &&
02625     e[0][0].getRational() == Rational(0) &&
02626     e[0][1].getKind() == MULT &&
02627     e[0][1].arity() == 2 &&
02628     e[0][1][0].getKind() == RATIONAL_EXPR &&
02629     e[0][1][0].getRational() == Rational(-1),
02630     "equalLeaves1");
02631   }
02632   if (withProof())
02633   {
02634     vector<Proof> pfs;
02635     pfs.push_back(thm.getProof());
02636     pf = newPf("equalLeaves1", e, pfs);
02637   }
02638   return newRWTheorem(e, e[0][1][1].eqExpr(e[0][2]), thm.getAssumptionsRef(), pf);
02639 }
02640 
02641 
02642 Theorem
02643 ArithTheoremProducer3::equalLeaves2(const Theorem& thm)
02644 {
02645   Proof pf;
02646   const Expr& e = thm.getRHS();
02647 
02648   if (CHECK_PROOFS) {
02649     CHECK_SOUND(e[0].getKind() == RATIONAL_EXPR &&
02650     e[0].getRational() == Rational(0) &&
02651     e[1].getKind() == PLUS &&
02652     e[1].arity() == 3 &&
02653     e[1][0].getKind() == RATIONAL_EXPR &&
02654     e[1][0].getRational() == Rational(0) &&
02655     e[1][1].getKind() == MULT &&
02656     e[1][1].arity() == 2 &&
02657     e[1][1][0].getKind() == RATIONAL_EXPR &&
02658     e[1][1][0].getRational() == Rational(-1),
02659     "equalLeaves2");
02660   }
02661   if (withProof())
02662   {
02663     vector<Proof> pfs;
02664     pfs.push_back(thm.getProof());
02665     pf = newPf("equalLeaves2", e, pfs);
02666   }
02667   return newRWTheorem(e, e[1][1][1].eqExpr(e[1][2]), thm.getAssumptionsRef(), pf);
02668 }
02669 
02670 
02671 Theorem
02672 ArithTheoremProducer3::equalLeaves3(const Theorem& thm)
02673 {
02674   Proof pf;
02675   const Expr& e = thm.getRHS();
02676 
02677   if (CHECK_PROOFS) {
02678     CHECK_SOUND(e[1].getKind() == RATIONAL_EXPR &&
02679     e[1].getRational() == Rational(0) &&
02680     e[0].getKind() == PLUS &&
02681     e[0].arity() == 3 &&
02682     e[0][0].getKind() == RATIONAL_EXPR &&
02683     e[0][0].getRational() == Rational(0) &&
02684     e[0][2].getKind() == MULT &&
02685     e[0][2].arity() == 2 &&
02686     e[0][2][0].getKind() == RATIONAL_EXPR &&
02687     e[0][2][0].getRational() == Rational(-1),
02688     "equalLeaves3");
02689   }
02690   if (withProof())
02691   {
02692     vector<Proof> pfs;
02693     pfs.push_back(thm.getProof());
02694     pf = newPf("equalLeaves3", e, pfs);
02695   }
02696   return newRWTheorem(e, e[0][2][1].eqExpr(e[0][1]), thm.getAssumptionsRef(), pf);
02697 }
02698 
02699 
02700 Theorem
02701 ArithTheoremProducer3::equalLeaves4(const Theorem& thm)
02702 {
02703   Proof pf;
02704   const Expr& e = thm.getRHS();
02705 
02706   if (CHECK_PROOFS) {
02707     CHECK_SOUND(e[0].getKind() == RATIONAL_EXPR &&
02708     e[0].getRational() == Rational(0) &&
02709     e[1].getKind() == PLUS &&
02710     e[1].arity() == 3 &&
02711     e[1][0].getKind() == RATIONAL_EXPR &&
02712     e[1][0].getRational() == Rational(0) &&
02713     e[1][2].getKind() == MULT &&
02714     e[1][2].arity() == 2 &&
02715     e[1][2][0].getKind() == RATIONAL_EXPR &&
02716     e[1][2][0].getRational() == Rational(-1),
02717     "equalLeaves4");
02718   }
02719   if (withProof())
02720   {
02721     vector<Proof> pfs;
02722     pfs.push_back(thm.getProof());
02723     pf = newPf("equalLeaves4", e, pfs);
02724   }
02725   return newRWTheorem(e, e[1][2][1].eqExpr(e[1][1]), thm.getAssumptionsRef(), pf);
02726 }
02727 
02728 Theorem
02729 ArithTheoremProducer3::diseqToIneq(const Theorem& diseq) {
02730   Proof pf;
02731 
02732   const Expr& e = diseq.getExpr();
02733 
02734   if(CHECK_PROOFS) {
02735     CHECK_SOUND(e.isNot() && e[0].isEq(),
02736     "ArithTheoremProducer3::diseqToIneq: expected disequality:\n"
02737     " e = "+e.toString());
02738   }
02739 
02740   const Expr& x = e[0][0];
02741   const Expr& y = e[0][1];
02742 
02743   if(withProof())
02744     pf = newPf(e, diseq.getProof());
02745   return newTheorem(ltExpr(x,y).orExpr(gtExpr(x,y)), diseq.getAssumptionsRef(), pf);
02746 }
02747 
02748 Theorem ArithTheoremProducer3::dummyTheorem(const Expr& e) {
02749   Proof pf;
02750   return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
02751 }
02752 
02753 Theorem ArithTheoremProducer3::oneElimination(const Expr& e) {
02754 
02755   // Check soundness
02756   if (CHECK_PROOFS)
02757     CHECK_SOUND(isMult(e) &&
02758           e.arity() == 2 &&
02759                 e[0].isRational() &&
02760                 e[0].getRational() == 1,
02761                 "oneElimination: input must be a multiplication by one" + e.toString());
02762 
02763   // The proof object that we will us
02764   Proof pf;
02765 
02766   // Setup the proof if needed
02767   if (withProof())
02768     pf = newPf("oneElimination", e);
02769 
02770   // Return the rewrite theorem that explains the phenomenon
02771   return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
02772 }
02773 
02774 Theorem ArithTheoremProducer3::clashingBounds(const Theorem& lowerBound, const Theorem& upperBound) {
02775 
02776   // Get the expressions
02777   const Expr& lowerBoundExpr = lowerBound.getExpr();
02778   const Expr& upperBoundExpr = upperBound.getExpr();
02779 
02780   // Check soundness
02781   if (CHECK_PROOFS) {
02782     CHECK_SOUND(isLE(lowerBoundExpr) || isLT(lowerBoundExpr), "clashingBounds: lowerBound should be >= or > " + lowerBoundExpr.toString());
02783     CHECK_SOUND(isGE(upperBoundExpr) || isGT(upperBoundExpr), "clashingBounds: upperBound should be <= or < " + upperBoundExpr.toString());
02784     CHECK_SOUND(lowerBoundExpr[0].isRational(), "clashingBounds: lowerBound left side should be a rational " + lowerBoundExpr.toString());
02785     CHECK_SOUND(upperBoundExpr[0].isRational(), "clashingBounds: upperBound left side should be a rational " + upperBoundExpr.toString());
02786     CHECK_SOUND(lowerBoundExpr[1] == upperBoundExpr[1], "clashingBounds: bounds not on the same term " + lowerBoundExpr.toString() + ", " + upperBoundExpr.toString());
02787 
02788     // Get the bounds
02789     Rational lowerBoundR = lowerBoundExpr[0].getRational();
02790     Rational upperBoundR = upperBoundExpr[0].getRational();
02791 
02792     if (isLE(lowerBoundExpr) && isGE(upperBoundExpr)) {
02793       CHECK_SOUND(upperBoundR < lowerBoundR, "clashingBounds: bounds are satisfiable");
02794     } else {
02795       CHECK_SOUND(upperBoundR <= lowerBoundR, "clashingBounds: bounds are satisfiable");
02796     }
02797   }
02798 
02799   // The proof object that we will use
02800   Proof pf;
02801   // Setup the proof if needed
02802   if (withProof())
02803     pf = newPf("clashingBounds", lowerBoundExpr, upperBoundExpr);
02804 
02805   // Put the bounds expressions in the assumptions
02806   Assumptions assumptions;
02807   assumptions.add(lowerBound);
02808   assumptions.add(upperBound);
02809 
02810   // Return the theorem
02811   return newTheorem(d_em->falseExpr(), assumptions, pf);
02812 }
02813 
02814 Theorem ArithTheoremProducer3::addInequalities(const Theorem& thm1, const Theorem& thm2) {
02815 
02816   // Get the expressions of the theorem
02817   const Expr& expr1 = thm1.getExpr();
02818   const Expr& expr2 = thm2.getExpr();
02819 
02820   // Check soundness
02821   if (CHECK_PROOFS) {
02822 
02823     CHECK_SOUND(isIneq(expr1), "addInequalities: expecting an inequality for thm1, got " + expr1.toString());
02824     CHECK_SOUND(isIneq(expr2), "addInequalities: expecting an inequality for thm2, got " + expr2.toString());
02825 
02826     if (isLE(expr1) || isLT(expr1))
02827       CHECK_SOUND(isLE(expr2) || isLT(expr2), "addInequalities: expr2 should be <(=) also " + expr2.toString());
02828     if (isGE(expr1) || isGT(expr1))
02829       CHECK_SOUND(isGE(expr2) || isGT(expr2), "addInequalities: expr2 should be >(=) also" + expr2.toString());
02830   }
02831 
02832   // Create the assumptions
02833   Assumptions a(thm1, thm2);
02834 
02835     // Get the kinds of the inequalitites
02836     int kind1  = expr1.getKind();
02837     int kind2  = expr2.getKind();
02838 
02839     // Set-up the resulting inequality
02840     int kind = (kind1 == kind2) ? kind1 : ((kind1 == LT) || (kind2 == LT))? LT : GT;
02841 
02842     // Create the proof object
02843     Proof pf;
02844     if(withProof()) {
02845       vector<Proof> pfs;
02846       pfs.push_back(thm1.getProof());
02847       pfs.push_back(thm2.getProof());
02848       pf = newPf("addInequalities", expr1, expr2, pfs);
02849     }
02850 
02851     // Create the new expressions
02852     Expr leftSide  = plusExpr(expr1[0], expr2[0]);
02853     Expr rightSide = plusExpr(expr1[1], expr2[1]);
02854 
02855     // Return the theorem
02856     return newTheorem(Expr(kind, leftSide, rightSide), a, pf);
02857 }
02858 
02859 Theorem ArithTheoremProducer3::implyWeakerInequality(const Expr& expr1, const Expr& expr2) {
02860 
02861   // Check soundness
02862   if (CHECK_PROOFS) {
02863 
02864     // Both must be inequalitites
02865     CHECK_SOUND(isIneq(expr1), "implyWeakerInequality: expr1 should be an inequality" + expr1.toString());
02866     CHECK_SOUND(isIneq(expr2), "implyWeakerInequality: expr1 should be an inequality" + expr2.toString());
02867 
02868     // Should be of the same type
02869     if (isLE(expr1) || isLT(expr1))
02870       CHECK_SOUND(isLE(expr2) || isLT(expr2), "implyWeakerInequality: expr2 should be <(=) also " + expr2.toString());
02871     if (isGE(expr1) || isGT(expr1))
02872       CHECK_SOUND(isGE(expr2) || isGT(expr2), "implyWeakerInequality: expr2 should be >(=) also" + expr2.toString());
02873 
02874     // Left sides must be rational numbers
02875     CHECK_SOUND(expr1[0].isRational(), "implyWeakerInequality: expr1 should have a rational on the left side" + expr1.toString());
02876     CHECK_SOUND(expr2[0].isRational(), "implyWeakerInequality: expr2 should have a rational on the left side" + expr2.toString());
02877 
02878     // Right sides must be identical
02879     CHECK_SOUND(expr1[1] == expr2[1], "implyWeakerInequality: the expression must be the same" + expr1.toString() + " and " + expr2.toString());
02880 
02881     Rational expr1rat = expr1[0].getRational();
02882     Rational expr2rat = expr2[0].getRational();
02883 
02884 
02885     // Check the bounds
02886     if (isLE(expr1) || isLT(expr2)) {
02887       CHECK_SOUND(expr2rat < expr1rat,  "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
02888     } else {
02889       CHECK_SOUND(expr2rat <= expr1rat, "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
02890     }
02891     if (isGE(expr1) || isGT(expr2)) {
02892       CHECK_SOUND(expr2rat > expr1rat,  "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
02893     } else {
02894       CHECK_SOUND(expr2rat >= expr1rat, "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
02895     }
02896   }
02897 
02898     // Create the proof object
02899     Proof pf;
02900     if(withProof()) pf = newPf("implyWeakerInequality", expr1, expr2);
02901 
02902   // Return the theorem
02903   return newTheorem(expr1.impExpr(expr2), Assumptions::emptyAssump(), pf);
02904 }
02905 
02906 Theorem ArithTheoremProducer3::implyNegatedInequality(const Expr& expr1, const Expr& expr2) {
02907 
02908   // Check soundness
02909   if (CHECK_PROOFS) {
02910     CHECK_SOUND(isIneq(expr1), "implyNegatedInequality: lowerBound should be an inequality " + expr1.toString());
02911     CHECK_SOUND(isIneq(expr2), "implyNegatedInequality: upperBound should be be an inequality " + expr2.toString());
02912     CHECK_SOUND(expr1[0].isRational(), "implyNegatedInequality: lowerBound left side should be a rational " + expr1.toString());
02913     CHECK_SOUND(expr2[0].isRational(), "implyNegatedInequality: upperBound left side should be a rational " + expr2.toString());
02914     CHECK_SOUND(expr1[1] == expr2[1], "implyNegatedInequality: bounds not on the same term " + expr1.toString() + ", " + expr2.toString());
02915 
02916     // Get the bounds
02917     Rational lowerBoundR = expr1[0].getRational();
02918     Rational upperBoundR = expr2[0].getRational();
02919 
02920     if (isLE(expr1) && isGE(expr2))
02921       CHECK_SOUND(upperBoundR < lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());
02922     if (isLT(expr1) || isGT(expr2))
02923       CHECK_SOUND(upperBoundR <= lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());
02924     if (isGE(expr1) && isLE(expr2))
02925       CHECK_SOUND(upperBoundR > lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());
02926     if (isGT(expr1) || isLT(expr2))
02927       CHECK_SOUND(upperBoundR >= lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());
02928   }
02929 
02930   // The proof object that we will use
02931   Proof pf;
02932   if (withProof()) pf = newPf("implyNegatedInequality", expr1, expr2);
02933 
02934   // Return the theorem
02935   return newTheorem(expr1.impExpr(expr2.negate()), Assumptions::emptyAssump(), pf);
02936 }
02937 
02938 Theorem ArithTheoremProducer3::trustedRewrite(const Expr& expr1, const Expr& expr2) {
02939 
02940   // The proof object that we will us
02941   Proof pf;
02942 
02943   // Setup the proof if needed
02944   if (withProof()) pf = newPf("trustedRewrite", expr1, expr2);
02945 
02946   // Return the rewrite theorem that explains the phenomenon
02947   return newRWTheorem(expr1, expr2, Assumptions::emptyAssump(), pf);
02948 
02949 }
02950 
02951 Theorem ArithTheoremProducer3::integerSplit(const Expr& intVar, const Rational& intPoint) {
02952 
02953   // Check soundness
02954   if (CHECK_PROOFS) {
02955     CHECK_SOUND(intPoint.isInteger(), "integerSplit: we can only split on integer points, given" + intPoint.toString());
02956   }
02957 
02958   // Create the expression
02959   const Expr& split = Expr(IS_INTEGER, intVar).impExpr(leExpr(intVar, rat(intPoint)).orExpr(geExpr(intVar, rat(intPoint + 1))));
02960 
02961   // The proof object that we will use
02962   Proof pf;
02963   if (withProof()) pf = newPf("integerSplit", intVar, rat(intPoint));
02964 
02965   // Return the theorem
02966   return newTheorem(split, Assumptions::emptyAssump(), pf);
02967 }
02968 
02969 
02970 Theorem ArithTheoremProducer3::rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr) {
02971 
02972 
02973   // Check soundness
02974   if (CHECK_PROOFS) {
02975     // Right side of the constraint should correspond to the proved integer expression
02976     CHECK_SOUND(isIneq(constr), "rafineStrictInteger: expected a constraint got : " + constr.toString());
02977     CHECK_SOUND(isIntConstrThm.getExpr()[0] == constr[1], "rafineStrictInteger: proof of intger doesn't correspond to the constarint right side");
02978     CHECK_SOUND(constr[0].isRational(), "rafineStrictInteger: right side of the constraint muts be a rational");
02979   }
02980 
02981   // Get the contraint bound
02982   Rational bound = constr[0].getRational();
02983 
02984   // Get the kind of the constraint
02985   int kind = constr.getKind();
02986 
02987   // If the bound is strict, make it non-strict
02988   switch (kind) {
02989     case LT:
02990       kind = LE;
02991       if (bound.isInteger()) bound ++;             // 3 < x   --> 4 <= x
02992       else bound = ceil(bound);                    // 3.4 < x --> 4 <= x
02993       break;
02994     case LE:
02995       kind = LE;
02996       if (!bound.isInteger()) bound = ceil(bound); // 3.5 <= x --> 4 <= x
02997       break;
02998     case GT:
02999       kind = GE;
03000       if (bound.isInteger()) bound --;             // 3 > x   --> 2 >= x
03001       else bound = floor(bound);                   // 3.4 > x --> 3 >= x
03002       break;
03003     case GE:
03004       kind = GE;
03005       if (!bound.isInteger()) bound = floor(bound); // 3.4 >= x --> 3 >= x
03006       break;
03007   }
03008 
03009   // The new constraint
03010   Expr newConstr(kind, rat(bound), constr[1]);
03011 
03012   // Pick up the assumptions from the integer proof
03013   const Assumptions& assump(isIntConstrThm.getAssumptionsRef());
03014 
03015     // Construct the proof object if necessary
03016     Proof pf;
03017   if (withProof()) pf = newPf("rafineStrictInteger", constr, isIntConstrThm.getProof());
03018 
03019   // Return the rewrite theorem that explains the phenomenon
03020   return newRWTheorem(constr, newConstr, assump, pf);
03021 }
03022 
03023 
03024 Theorem ArithTheoremProducer3::splitGrayShadowSmall(const Theorem& gThm) {
03025   DebugAssert(false, "Not implemented!!!");
03026   return Theorem();
03027 }
03028 
03029 Theorem ArithTheoremProducer3::implyWeakerInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) {
03030   DebugAssert(false, "Not implemented!!!");
03031   return Theorem();
03032 }
03033 
03034 Theorem ArithTheoremProducer3::implyNegatedInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) {
03035   DebugAssert(false, "Not implemented!!!");
03036   return Theorem();
03037 }
03038 
03039 Theorem ArithTheoremProducer3::expandGrayShadowRewrite(const Expr& theShadow) {
03040   DebugAssert(false, "Not implemented!!!");
03041   return Theorem();
03042 }
03043 
03044 Theorem ArithTheoremProducer3::compactNonLinearTerm(const Expr& nonLinear) {
03045   DebugAssert(false, "Not implemented!!!");
03046   return Theorem();
03047 }
03048 
03049 Theorem ArithTheoremProducer3::nonLinearIneqSignSplit(const Theorem& ineqThm) {
03050   DebugAssert(false, "Not implemented!!!");
03051   return Theorem();
03052 }
03053 
03054 Theorem ArithTheoremProducer3::implyDiffLogicBothBounds(const Expr& x,
03055               std::vector<Theorem>& c1_le_x, Rational c1,
03056                 std::vector<Theorem>& x_le_c2, Rational c2) {
03057   DebugAssert(false, "Not implemented!!!");
03058   return Theorem();
03059 }
03060 
03061 Theorem ArithTheoremProducer3::addInequalities(const vector<Theorem>& thms) {
03062   DebugAssert(false, "Not implemented!!!");
03063   return Theorem();
03064 }
03065 
03066 Theorem ArithTheoremProducer3::powerOfOne(const Expr& e) {
03067   DebugAssert(false, "Not implemented!!!");
03068   return Theorem();
03069 }
03070 
03071 //
03072 // This one is here just to compile... the code is in old arithmetic
03073 Theorem ArithTheoremProducer3::simpleIneqInt(const Expr& ineq, const Theorem& isIntRHS)
03074 {
03075   DebugAssert(false, "Not implemented!!!");
03076   return Theorem();
03077 }
03078 
03079 // Given:
03080 // 0 = c + t
03081 // where t is integer and c is not
03082 // deduce bot
03083 Theorem ArithTheoremProducer3::intEqualityRationalConstant(const Theorem& isIntConstrThm, const Expr& constr) {
03084   DebugAssert(false, "Not implemented!!!");
03085   return Theorem();
03086 }
03087 
03088 Theorem ArithTheoremProducer3::cycleConflict(const vector<Theorem>& inequalitites) {
03089   DebugAssert(false, "Not implemented!!!");
03090   return Theorem();
03091 }
03092 
03093 Theorem ArithTheoremProducer3::implyEqualities(const vector<Theorem>& inequalitites) {
03094   DebugAssert(false, "Not implemented!!!");
03095   return Theorem();
03096 }
03097 
03098 
03099 /*! Takes a Theorem(\\alpha < \\beta) and returns
03100  *  Theorem(\\alpha < \\beta <==> \\alpha <= \\beta -1)
03101  * where \\alpha and \\beta are integer expressions
03102  */
03103 Theorem ArithTheoremProducer3::lessThanToLERewrite(const Expr& ineq,
03104                                                    const Theorem& isIntLHS,
03105                                                    const Theorem& isIntRHS,
03106                                                    bool changeRight) {
03107 
03108   const Expr& isIntLHSexpr = isIntLHS.getExpr();
03109   const Expr& isIntRHSexpr = isIntRHS.getExpr();
03110 
03111   if(CHECK_PROOFS) {
03112     CHECK_SOUND(isLT(ineq), "ArithTheoremProducerOld::LTtoLE: ineq must be <");
03113     // Integrality check
03114     CHECK_SOUND(isIntPred(isIntLHSexpr) && isIntLHSexpr[0] == ineq[0],
03115     "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
03116     " ineq = "+ineq.toString()+"\n isIntLHS = "
03117     +isIntLHSexpr.toString());
03118     CHECK_SOUND(isIntPred(isIntRHSexpr) && isIntRHSexpr[0] == ineq[1],
03119     "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
03120     " ineq = "+ineq.toString()+"\n isIntRHS = "
03121     +isIntRHSexpr.toString());
03122   }
03123 
03124   vector<Theorem> thms;
03125   thms.push_back(isIntLHS);
03126   thms.push_back(isIntRHS);
03127   Assumptions a(thms);
03128   Proof pf;
03129   Expr le = changeRight? leExpr(ineq[0], ineq[1] + rat(-1)) : leExpr(ineq[0] + rat(1), ineq[1]);
03130   if(withProof()) {
03131     vector<Proof> pfs;
03132     pfs.push_back(isIntLHS.getProof());
03133     pfs.push_back(isIntRHS.getProof());
03134     pf = newPf(changeRight? "lessThan_To_LE_rhs" : "lessThan_To_LE_lhs", le, pfs);
03135   }
03136 
03137   return newRWTheorem(ineq, le, a, pf);
03138 }

Generated on Wed Nov 18 16:13:28 2009 for CVC3 by  doxygen 1.5.2