CVC3

arith_theorem_producer_old.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file arith_theorem_producer.cpp
00004  *
00005  * Author: Vijay Ganesh, Sergey Berezin
00006  *
00007  * Created: Dec 13 02:09:04 GMT 2002
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  *
00016  * <hr>
00017  *
00018  */
00019 /*****************************************************************************/
00020 // CLASS: ArithProofRules
00021 //
00022 // AUTHOR: Sergey Berezin, 12/11/2002
00023 // AUTHOR: Vijay Ganesh,   05/30/2003
00024 //
00025 // Description: TRUSTED implementation of arithmetic proof rules.
00026 //
00027 ///////////////////////////////////////////////////////////////////////////////
00028 
00029 // This code is trusted
00030 #define _CVC3_TRUSTED_
00031 
00032 #include "arith_theorem_producer_old.h"
00033 #include "theory_core.h"
00034 #include "theory_arith_old.h"
00035 #include <algorithm>
00036 
00037 using namespace std;
00038 using namespace CVC3;
00039 
00040 ////////////////////////////////////////////////////////////////////
00041 // TheoryArith: trusted method for creating ArithTheoremProducerOld
00042 ////////////////////////////////////////////////////////////////////
00043 
00044 ArithProofRules* TheoryArithOld::createProofRulesOld() {
00045   return new ArithTheoremProducerOld(theoryCore()->getTM(), this);
00046 }
00047 
00048 ////////////////////////////////////////////////////////////////////
00049 // Canonization rules
00050 ////////////////////////////////////////////////////////////////////
00051 
00052 
00053 #define CLASS_NAME "ArithTheoremProducerOld"
00054 
00055 
00056 // Rule for variables: e == 1 * e
00057 Theorem ArithTheoremProducerOld::varToMult(const Expr& e) {
00058   Proof pf;
00059   if(withProof()) pf = newPf("var_to_mult", e);
00060   return newRWTheorem(e, (rat(1) * e), Assumptions::emptyAssump(), pf);
00061 }
00062 
00063 
00064 // Rule for unary minus: -e == (-1) * e
00065 Theorem ArithTheoremProducerOld::uMinusToMult(const Expr& e) {
00066   Proof pf;
00067   if(withProof()) pf = newPf("uminus_to_mult", e);
00068   return newRWTheorem((-e), (rat(-1) * e), Assumptions::emptyAssump(), pf);
00069 }
00070 
00071 
00072 // ==> x - y = x + (-1) * y
00073 Theorem ArithTheoremProducerOld::minusToPlus(const Expr& x, const Expr& y)
00074 {
00075   Proof pf;
00076   if(withProof()) pf = newPf("minus_to_plus", x, y);
00077   return newRWTheorem((x-y), (x + (rat(-1) * y)), Assumptions::emptyAssump(), pf);
00078 }
00079 
00080 
00081 // Rule for unary minus: -e == e/(-1)
00082 // This is to reduce the number of almost identical rules for uminus and div
00083 Theorem ArithTheoremProducerOld::canonUMinusToDivide(const Expr& e) {
00084   Proof pf;
00085   if(withProof()) pf = newPf("canon_uminus", e);
00086   return newRWTheorem((-e), (e / rat(-1)), Assumptions::emptyAssump(), pf);
00087 }
00088 
00089 // Rules for division by constant
00090 
00091 // (c)/(d) ==> (c/d).  When d==0, c/0 = 0 (our total extension).
00092 Theorem ArithTheoremProducerOld::canonDivideConst(const Expr& c,
00093                                                const Expr& d) {
00094   // Make sure c and d are a const
00095   if(CHECK_PROOFS) {
00096     CHECK_SOUND(isRational(c),
00097                 CLASS_NAME "::canonDivideConst:\n c not a constant: "
00098                 + c.toString());
00099     CHECK_SOUND(isRational(d),
00100                 CLASS_NAME "::canonDivideConst:\n d not a constant: "
00101                 + d.toString());
00102   }
00103   Proof pf;
00104   if(withProof())
00105     pf = newPf("canon_divide_const", c, d, d_hole);
00106   const Rational& dr = d.getRational();
00107   return newRWTheorem((c/d), (rat(dr==0? 0 : (c.getRational()/dr))), Assumptions::emptyAssump(), pf);
00108 }
00109 
00110 // (c * x)/d ==> (c/d) * x, takes (c*x) and d
00111 Theorem ArithTheoremProducerOld::canonDivideMult(const Expr& cx,
00112                                               const Expr& d) {
00113   // Check the format of c*x
00114   if(CHECK_PROOFS) {
00115     CHECK_SOUND(isMult(cx) && isRational(cx[0]),
00116                 CLASS_NAME "::canonDivideMult:\n  "
00117                 "Not a (c * x) expression: "
00118                 + cx.toString());
00119     CHECK_SOUND(isRational(d),
00120                 CLASS_NAME "::canonDivideMult:\n  "
00121                 "d is not a constant: " + d.toString());
00122   }
00123   const Rational& dr = d.getRational();
00124   Rational cdr(dr==0? 0 : (cx[0].getRational()/dr));
00125   Expr cd(rat(cdr));
00126   Proof pf;
00127   if(withProof())
00128     pf = newPf("canon_divide_mult", cx[0], cx[1], d);
00129   // (c/d) may be == 1, so we also need to canonize 1*x to x
00130   if(cdr == 1)
00131     return newRWTheorem((cx/d), (cx[1]), Assumptions::emptyAssump(), pf);
00132   else if(cdr == 0) // c/0 == 0 case
00133     return newRWTheorem((cx/d), cd, Assumptions::emptyAssump(), pf);
00134   else
00135     return newRWTheorem((cx/d), (cd*cx[1]), Assumptions::emptyAssump(), pf);
00136 }
00137 
00138 // (+ t1 ... tn)/d ==> (+ (t1/d) ... (tn/d))
00139 Theorem ArithTheoremProducerOld::canonDividePlus(const Expr& sum, const Expr& d) {
00140   if(CHECK_PROOFS) {
00141     CHECK_SOUND(isPlus(sum) && sum.arity() >= 2 && isRational(sum[0]),
00142                 CLASS_NAME "::canonUMinusPlus:\n  "
00143                 "Expr is not a canonical sum: "
00144                 + sum.toString());
00145     CHECK_SOUND(isRational(d),
00146                 CLASS_NAME "::canonUMinusPlus:\n  "
00147                 "d is not a const: " + d.toString());
00148   }
00149   // First, propagate '/d' down to the args
00150   Proof pf;
00151   if(withProof())
00152     pf = newPf("canon_divide_plus", rat(sum.arity()),
00153                sum.begin(), sum.end());
00154   vector<Expr> newKids;
00155   for(Expr::iterator i=sum.begin(), iend=sum.end(); i!=iend; ++i)
00156     newKids.push_back((*i)/d);
00157   // (+ t1 ... tn)/d == (+ (t1/d) ... (tn/d))
00158   return newRWTheorem((sum/d), (plusExpr(newKids)), Assumptions::emptyAssump(), pf);
00159 }
00160 
00161 // x/(d) ==> (1/d) * x, unless d == 1
00162 Theorem ArithTheoremProducerOld::canonDivideVar(const Expr& e, const Expr& d) {
00163   if(CHECK_PROOFS) {
00164     CHECK_SOUND(isRational(d),
00165                 CLASS_NAME "::canonDivideVar:\n  "
00166                 "d is not a const: " + d.toString());
00167   }
00168   Proof pf;
00169 
00170   if(withProof())
00171     pf = newPf("canon_divide_var", e);
00172 
00173   const Rational& dr = d.getRational();
00174   if(dr == 1)
00175     return newRWTheorem(e/d, e, Assumptions::emptyAssump(), pf);
00176   if(dr == 0) // e/0 == 0 (total extension of division)
00177     return newRWTheorem(e/d, d, Assumptions::emptyAssump(), pf);
00178   else
00179     return newRWTheorem(e/d, rat(1/dr) * e, Assumptions::emptyAssump(), pf);
00180 }
00181 
00182 
00183 // Multiplication
00184 // (MULT expr1 expr2 expr3 ...)
00185 // Each expr is in canonical form, i.e. it can be a
00186 // 1) Rational constant
00187 // 2) Arithmetic Leaf (var or term from another theory)
00188 // 3) (POW rational leaf)
00189 // where rational cannot be 0 or 1
00190 // 4) (MULT rational mterm'_1 ...) where each mterm' is of type (2) or (3)
00191 // If rational == 1 then there should be at least two mterms
00192 // 5) (PLUS rational sterm_1 ...) where each sterm is of
00193 //     type (2) or (3) or (4)
00194 //    if rational == 0 then there should be at least two sterms
00195 
00196 
00197 Expr ArithTheoremProducerOld::simplifiedMultExpr(std::vector<Expr> & mulKids)
00198 {
00199   DebugAssert(mulKids.size() >= 1 && mulKids[0].isRational(), "");
00200   if (mulKids.size() == 1) {
00201     return mulKids[0];
00202   }
00203   if ((mulKids[0] == rat(1)) && mulKids.size() == 2) {
00204     return mulKids[1];
00205   }
00206   else
00207     return multExpr(mulKids);
00208 }
00209 
00210 Expr ArithTheoremProducerOld::canonMultConstMult(const Expr & c,
00211                                               const Expr & e)
00212 {
00213   // c is a rational
00214   // e is (MULT rat mterm'_1 ....)
00215   // assume that e2 is already in canonic form
00216   DebugAssert(c.isRational() && e.getKind() == MULT, "");
00217   std::vector<Expr> mulKids;
00218   DebugAssert ((e.arity() > 1) && (e[0].isRational()),
00219                "ArithTheoremProducerOld::canonMultConstMult: "
00220                "a canonized MULT expression must have arity "
00221                "greater than 1: and first child must be "
00222                "rational " + e.toString());
00223   Expr::iterator i = e.begin();
00224   mulKids.push_back(rat(c.getRational() * (*i).getRational()));
00225   ++i;
00226   for(; i != e.end(); ++i) {
00227     mulKids.push_back(*i);
00228   }
00229   return simplifiedMultExpr(mulKids);
00230 }
00231 
00232 Expr ArithTheoremProducerOld::canonMultConstPlus(const Expr & e1,
00233                                               const Expr & e2)
00234 {
00235   DebugAssert(e1.isRational() && e2.getKind() == PLUS &&
00236               e2.arity() > 0, "");
00237   // e1 is a rational
00238   // e2 is of the form (PLUS rational sterm1 sterm2 ...)
00239   // assume that e2 is already in canonic form
00240   std::vector<Theorem> thmPlusVector;
00241   Expr::iterator i = e2.begin();
00242   for(; i!= e2.end(); ++i) {
00243     thmPlusVector.push_back(canonMultMtermMterm(e1*(*i)));
00244   }
00245 
00246   Theorem thmPlus1 =
00247     d_theoryArith->substitutivityRule(e2.getOp(), thmPlusVector);
00248   return thmPlus1.getRHS();
00249 }
00250 
00251 Expr ArithTheoremProducerOld::canonMultPowPow(const Expr & e1,
00252                                            const Expr & e2)
00253 {
00254   DebugAssert(e1.getKind() == POW && e2.getKind() == POW, "");
00255   // (POW r1 leaf1) * (POW r2 leaf2)
00256   Expr leaf1 = e1[1];
00257   Expr leaf2 = e2[1];
00258   Expr can_expr;
00259   if (leaf1 == leaf2) {
00260     Rational rsum = e1[0].getRational() + e2[0].getRational();
00261     if (rsum == 0) {
00262       return rat(1);
00263     }
00264     else if (rsum == 1) {
00265       return leaf1;
00266     }
00267     else
00268       {
00269         return powExpr(rat(rsum), leaf1);
00270       }
00271   }
00272   else
00273     {
00274       std::vector<Expr> mulKids;
00275       mulKids.push_back(rat(1));
00276       // the leafs should be put in decreasing order
00277       if (leaf1 < leaf2) {
00278         mulKids.push_back(e2);
00279         mulKids.push_back(e1);
00280       }
00281       else
00282         {
00283           mulKids.push_back(e1);
00284           mulKids.push_back(e2);
00285         }
00286       // FIXME: don't really need to simplify, just wrap up a MULT?
00287       return simplifiedMultExpr(mulKids);
00288     }
00289 }
00290 
00291 Expr ArithTheoremProducerOld::canonMultPowLeaf(const Expr & e1,
00292                                             const Expr & e2)
00293 {
00294   DebugAssert(e1.getKind() == POW, "");
00295   // (POW r1 leaf1) * leaf2
00296   Expr leaf1 = e1[1];
00297   Expr leaf2 = e2;
00298   Expr can_expr;
00299   if (leaf1 == leaf2) {
00300     Rational rsum = e1[0].getRational() + 1;
00301     if (rsum == 0) {
00302       return rat(1);
00303     }
00304     else if (rsum == 1) {
00305       return leaf1;
00306     }
00307     else
00308       {
00309         return powExpr(rat(rsum), leaf1);
00310       }
00311   }
00312   else
00313     {
00314       std::vector<Expr> mulKids;
00315       mulKids.push_back(rat(1));
00316       // the leafs should be put in decreasing order
00317       if (leaf1 < leaf2) {
00318         mulKids.push_back(e2);
00319         mulKids.push_back(e1);
00320       }
00321       else
00322         {
00323           mulKids.push_back(e1);
00324           mulKids.push_back(e2);
00325         }
00326       return simplifiedMultExpr(mulKids);
00327     }
00328 }
00329 
00330 Expr ArithTheoremProducerOld::canonMultLeafLeaf(const Expr & e1,
00331                                              const Expr & e2)
00332 {
00333   // leaf1 * leaf2
00334   Expr leaf1 = e1;
00335   Expr leaf2 = e2;
00336   Expr can_expr;
00337   if (leaf1 == leaf2) {
00338     return powExpr(rat(2), leaf1);
00339   }
00340   else
00341     {
00342       std::vector<Expr> mulKids;
00343       mulKids.push_back(rat(1));
00344       // the leafs should be put in decreasing order
00345       if (leaf1 < leaf2) {
00346         mulKids.push_back(e2);
00347         mulKids.push_back(e1);
00348       }
00349       else
00350         {
00351           mulKids.push_back(e1);
00352           mulKids.push_back(e2);
00353         }
00354       return simplifiedMultExpr(mulKids);
00355     }
00356 }
00357 
00358 Expr ArithTheoremProducerOld::canonMultLeafOrPowMult(const Expr & e1,
00359                                                   const Expr & e2)
00360 {
00361   DebugAssert(e2.getKind() == MULT, "");
00362   // Leaf * (MULT rat1 mterm1 ...)
00363   // (POW r1 leaf1) * (MULT rat1 mterm1 ...) where
00364   // each mterm is a leaf or (POW r leaf).  Furthermore the leafs
00365   // in the mterms are in descending order
00366   Expr leaf1 = e1.getKind() == POW ? e1[1] : e1;
00367   std::vector<Expr> mulKids;
00368   DebugAssert(e2.arity() > 1, "MULT expr must have arity 2 or more");
00369   Expr::iterator i = e2.begin();
00370   // push the rational
00371   mulKids.push_back(*i);
00372   ++i;
00373   // Now i points to the first mterm
00374   for(; i != e2.end(); ++i) {
00375     Expr leaf2 = ((*i).getKind() == POW) ? (*i)[1] : (*i);
00376     if (leaf1 == leaf2) {
00377       Rational r1 = e1.getKind() == POW ? e1[0].getRational() : 1;
00378       Rational r2 =
00379         ((*i).getKind() == POW ? (*i)[0].getRational() : 1);
00380       // if r1 + r2 == 0 then it is the case of x^n * x^{-n}
00381       // So, nothing needs to be added
00382       if (r1 + r2 != 0) {
00383         if (r1 + r2 == 1) {
00384           mulKids.push_back(leaf1);
00385         }
00386         else
00387           {
00388             mulKids.push_back(powExpr(rat(r1 + r2), leaf1));
00389           }
00390       }
00391       break;
00392     }
00393     // This ensures that the leaves in the mterms are also arranged
00394     // in decreasing order
00395     // Note that this will need to be changed if we want the order to
00396     // be increasing order.
00397     else if (leaf2 < leaf1) {
00398       mulKids.push_back(e1);
00399       mulKids.push_back(*i);
00400       break;
00401     }
00402     else // leaf1 < leaf2
00403       mulKids.push_back(*i);
00404   }
00405   if (i == e2.end()) {
00406     mulKids.push_back(e1);
00407   }
00408   else
00409     {
00410       // e1 and *i have already been added
00411       for (++i; i != e2.end(); ++i) {
00412         mulKids.push_back(*i);
00413       }
00414     }
00415   return simplifiedMultExpr(mulKids);
00416 }
00417 
00418 // Local class for ordering monomials; note, that it flips the
00419 // ordering given by greaterthan(), to sort in ascending order.
00420 class MonomialLess {
00421 public:
00422   bool operator()(const Expr& e1, const Expr& e2) const {
00423     return ArithTheoremProducerOld::greaterthan(e1,e2);
00424   }
00425 };
00426 
00427 typedef map<Expr,Rational,MonomialLess> MonomMap;
00428 
00429 Expr
00430 ArithTheoremProducerOld::canonCombineLikeTerms(const std::vector<Expr> & sumExprs)
00431 {
00432   Rational constant = 0;
00433   MonomMap sumHashMap;
00434   vector<Expr> sumKids;
00435 
00436   // Add each distinct mterm (not including the rational) into
00437   // an appropriate hash map entry
00438   std::vector<Expr>::const_iterator i = sumExprs.begin();
00439   for (; i != sumExprs.end(); ++i) {
00440     Expr mul = *i;
00441     if (mul.isRational()) {
00442       constant = constant + mul.getRational();
00443     }
00444     else {
00445       switch (mul.getKind()) {
00446       case MULT: {
00447         std::vector<Expr> mulKids;
00448         DebugAssert(mul.arity() > 1 && mul[0].isRational(),"");
00449         mulKids.push_back(rat(1));
00450         Expr::iterator j = mul.begin();
00451         ++j;
00452         for (; j!= mul.end(); ++j) {
00453           mulKids.push_back(*j);
00454         }
00455 
00456         // make sure that tempExpr is also in canonic form
00457         Expr tempExpr = mulKids.size() > 2 ? multExpr(mulKids): mulKids[1];
00458   MonomMap::iterator i=sumHashMap.find(tempExpr);
00459         if (i == sumHashMap.end()) {
00460           sumHashMap[tempExpr] = mul[0].getRational();
00461         }
00462         else {
00463           (*i).second += mul[0].getRational();
00464         }
00465       }
00466         break;
00467       default: {
00468   MonomMap::iterator i=sumHashMap.find(mul);
00469         // covers the case of POW, leaf
00470         if (i == sumHashMap.end()) {
00471           sumHashMap[mul] = 1;
00472         }
00473         else {
00474           (*i).second += 1;
00475         }
00476         break;
00477       }
00478       }
00479     }
00480   }
00481   // Now transfer to sumKids
00482   sumKids.push_back(rat(constant));
00483   MonomMap::iterator j = sumHashMap.begin(), jend=sumHashMap.end();
00484   for(; j != jend; ++j) {
00485     if ((*j).second != 0)
00486       sumKids.push_back
00487   (canonMultMtermMterm(rat((*j).second) * (*j).first).getRHS());
00488   }
00489 
00490   /*
00491     for (unsigned k = 0; k < sumKids.size(); ++k)
00492     {
00493     cout << "sumKids[" << k << "] = " << sumKids[k].toString() << endl;
00494     }
00495   */
00496 
00497   // The ordering in map guarantees the correct order; no need to sort
00498 
00499   // std::sort(sumKids.begin(), sumKids.end(), greaterthan);
00500 
00501   if ((constant == 0) && (sumKids.size() == 2)) {
00502     return sumKids[1];
00503   }
00504   else if (sumKids.size() == 1) {
00505     return sumKids[0];
00506   }
00507   else
00508     return plusExpr(sumKids);
00509 }
00510 
00511 Expr ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus(const Expr & e1,
00512                                                         const Expr & e2)
00513 {
00514   DebugAssert(e2.getKind() == PLUS, "");
00515   // Leaf *  (PLUS rational sterm1 ...)
00516   // or
00517   // (POW n1 x1) * (PLUS rational sterm1 ...)
00518   // or
00519   // (MULT r1 m1 m2 ...) * (PLUS rational sterm1 ...)
00520   // assume that e1 and e2 are themselves canonized
00521   std::vector<Expr> sumExprs;
00522   // Multiply each term in turn.
00523   Expr::iterator i = e2.begin();
00524   for (; i != e2.end(); ++i) {
00525     sumExprs.push_back(canonMultMtermMterm(e1 * (*i)).getRHS());
00526   }
00527   return canonCombineLikeTerms(sumExprs);
00528 }
00529 
00530 Expr ArithTheoremProducerOld::canonMultPlusPlus(const Expr & e1,
00531                                              const Expr & e2)
00532 {
00533   DebugAssert(e1.getKind() == PLUS && e2.getKind() == PLUS, "");
00534   // (PLUS r1 .... ) * (PLUS r1' ...)
00535   // assume that e1 and e2 are themselves canonized
00536 
00537   std::vector<Expr> sumExprs;
00538   // Multiply each term in turn.
00539   Expr::iterator i = e1.begin();
00540   for (;  i != e1.end(); ++i) {
00541     Expr::iterator j = e2.begin();
00542     for (;  j != e2.end(); ++j) {
00543       sumExprs.push_back(canonMultMtermMterm((*i) * (*j)).getRHS());
00544     }
00545   }
00546   return canonCombineLikeTerms(sumExprs);
00547 }
00548 
00549 
00550 
00551 // The following produces a Theorem which is the result of multiplication
00552 // of two canonized mterms.  e = e1*e2
00553 Theorem
00554 ArithTheoremProducerOld::canonMultMtermMterm(const Expr& e)
00555 {
00556   if(CHECK_PROOFS) {
00557     CHECK_SOUND(isMult(e) && e.arity() == 2,
00558     "canonMultMtermMterm: e = "+e.toString());
00559   }
00560   Proof pf;
00561   Expr rhs;
00562   const Expr& e1 = e[0];
00563   const Expr& e2 = e[1];
00564   string cmmm = "canon_mult_mterm_mterm";
00565 
00566   if (e1.isRational()) {
00567     // e1 is a Rational
00568     const Rational& c = e1.getRational();
00569     if (c == 0)
00570       return canonMultZero(e2);
00571     else if (c == 1)
00572       return canonMultOne(e2);
00573     else {
00574       switch (e2.getKind()) {
00575       case RATIONAL_EXPR :
00576         // rat * rat
00577         return canonMultConstConst(e1,e2);
00578         break;
00579         // TODO case of leaf
00580       case POW:
00581         // rat * (POW rat leaf)
00582         // nothing to simplify
00583         return d_theoryArith->reflexivityRule (e);
00584 
00585         break;
00586       case MULT:
00587         rhs = canonMultConstMult(e1,e2);
00588         if(withProof()) pf = newPf(cmmm,e,rhs);
00589         return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00590         break;
00591       case PLUS:
00592         rhs = canonMultConstPlus(e1,e2);
00593         if(withProof()) pf = newPf(cmmm,e,rhs);
00594         return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00595         break;
00596       default:
00597         // TODO: I am going to assume that this is just a leaf
00598         // i.e., a variable or term from another theory
00599         return d_theoryArith->reflexivityRule(e);
00600         break;
00601       }
00602     }
00603   }
00604   else if (e1.getKind() == POW) {
00605     switch (e2.getKind()) {
00606     case RATIONAL_EXPR:
00607       // switch the order of the two arguments
00608       return canonMultMtermMterm(e2 * e1);
00609       break;
00610     case POW:
00611       rhs = canonMultPowPow(e1,e2);
00612       if(withProof()) pf = newPf(cmmm,e,rhs);
00613       return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
00614       break;
00615     case MULT:
00616       rhs = canonMultLeafOrPowMult(e1,e2);
00617       if(withProof()) pf = newPf(cmmm,e,rhs);
00618       return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00619       break;
00620     case PLUS:
00621       rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
00622       if(withProof()) pf = newPf(cmmm,e,rhs);
00623       return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00624       break;
00625     default:
00626       rhs = canonMultPowLeaf(e1,e2);
00627       if(withProof()) pf = newPf(cmmm,e,rhs);
00628       return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
00629       break;
00630     }
00631   }
00632   else if (e1.getKind() == MULT) {
00633     switch (e2.getKind()) {
00634     case RATIONAL_EXPR:
00635     case POW:
00636       // switch the order of the two arguments
00637       return canonMultMtermMterm(e2 * e1);
00638       break;
00639     case MULT:
00640       {
00641         // (Mult r m1 m2 ...) (Mult r' m1' m2' ...)
00642         Expr result = e2;
00643         Expr::iterator i = e1.begin();
00644         for (; i != e1.end(); ++i) {
00645           result = canonMultMtermMterm((*i) * result).getRHS();
00646         }
00647         if(withProof()) pf = newPf(cmmm,e,result);
00648         return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
00649       }
00650       break;
00651     case PLUS:
00652       rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
00653       if(withProof()) pf = newPf(cmmm,e,rhs);
00654       return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
00655       break;
00656     default:
00657       // leaf
00658       // switch the order of the two arguments
00659       return canonMultMtermMterm(e2 * e1);
00660       break;
00661     }
00662   }
00663   else if (e1.getKind() == PLUS) {
00664     switch (e2.getKind()) {
00665     case RATIONAL_EXPR:
00666     case POW:
00667     case MULT:
00668       // switch the order of the two arguments
00669       return canonMultMtermMterm(e2 * e1);
00670       break;
00671     case PLUS:
00672       rhs = canonMultPlusPlus(e1,e2);
00673       if(withProof()) pf = newPf(cmmm,e,rhs);
00674       return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00675       break;
00676     default:
00677       // leaf
00678       // switch the order of the two arguments
00679       return canonMultMtermMterm(e2 * e1);
00680       break;
00681     }
00682   }
00683   else {
00684     // leaf
00685     switch (e2.getKind()) {
00686     case RATIONAL_EXPR:
00687       // switch the order of the two arguments
00688       return canonMultMtermMterm(e2 * e1);
00689       break;
00690     case POW:
00691       rhs = canonMultPowLeaf(e2,e1);
00692       if(withProof()) pf = newPf(cmmm,e,rhs);
00693       return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00694       break;
00695     case MULT:
00696       rhs = canonMultLeafOrPowMult(e1,e2);;
00697       if(withProof()) pf = newPf(cmmm,e,rhs);
00698       return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00699       break;
00700     case PLUS:
00701       rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
00702       if(withProof()) pf = newPf(cmmm,e,rhs);
00703       return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00704       break;
00705     default:
00706       // leaf * leaf
00707       rhs = canonMultLeafLeaf(e1,e2);
00708       if(withProof()) pf = newPf(cmmm,e,rhs);
00709       return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00710       break;
00711     }
00712   }
00713   FatalAssert(false, "Unreachable");
00714   return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
00715 }
00716 
00717 // (PLUS expr1 expr2 ...) where each expr is itself in canonic form
00718 Theorem
00719 ArithTheoremProducerOld::canonPlus(const Expr& e)
00720 {
00721   Proof pf;
00722 
00723   if (withProof()) {
00724     pf = newPf("canon_plus", e);
00725   }
00726   DebugAssert(e.getKind() == PLUS, "");
00727 
00728   // First flatten the PLUS
00729 
00730   std::vector<Expr> sumKids;
00731   Expr::iterator i = e.begin();
00732   for(; i != e.end(); ++i) {
00733     if ((*i).getKind() != PLUS) {
00734       sumKids.push_back(*i);
00735     }
00736     else
00737       {
00738         Expr::iterator j = (*i).begin();
00739         for(; j != (*i).end(); ++j)
00740           sumKids.push_back(*j);
00741       }
00742   }
00743   Expr val = canonCombineLikeTerms(sumKids);
00744   if (withProof()) {
00745     pf = newPf("canon_plus", e, val);
00746   }
00747   return newRWTheorem(e, val, Assumptions::emptyAssump(), pf);
00748 }
00749 
00750 // (MULT expr1 expr2 ...) where each expr is itself in canonic form
00751 Theorem
00752 ArithTheoremProducerOld::canonMult(const Expr& e)
00753 {
00754   Proof pf;
00755   TRACE("arith canon", "canonMult(", e.toString(), ")");
00756   DebugAssert(e.getKind() == MULT && e.arity() > 1, "");
00757   Expr::iterator i = e.begin();
00758   Expr result = *i;
00759   ++i;
00760   for (; i != e.end(); ++i) {
00761     result = canonMultMtermMterm(result * (*i)).getRHS();
00762   }
00763   if (withProof()) {
00764     pf = newPf("canon_mult", e,result);
00765   }
00766 
00767   // If multiplicative sign split is on do it
00768   if (d_theoryArith->nonlinearSignSplit()) {
00769 
00770     // Add the sign splits
00771     Expr positive = d_em->trueExpr();
00772     Expr negative = d_em->falseExpr();
00773     vector<Expr> zero;
00774 
00775     // we do the case split if it's not trivial
00776     int count_non_trivial = 0;
00777     int count_constants = 0;
00778 
00779     // a1*a2*...*an is positive if there is an even number of negative ones
00780     // a1*a2*...*an is negative if there is an odd number of negative ones
00781     for (i = e.begin(); i != e.end(); ++i) {
00782       Expr current = (*i);
00783 
00784       if (isPlus(current)) count_non_trivial ++;
00785       if (current.isRational()) count_constants ++;
00786       if (isPow(current) && current[0].getRational() < 0) {
00787         // Bail on negative powers, it's normalization
00788         count_non_trivial = 0;
00789         break;
00790       }
00791 
00792       zero.push_back(current.eqExpr(rat(0)));
00793       positive = Expr(XOR, positive, ltExpr(current, rat(0)));
00794       negative = Expr(XOR, negative, ltExpr(current, rat(0)));
00795     }
00796 
00797     if (count_non_trivial > 0 && !count_constants == (e.arity() - 1)) {
00798       // Any of the factors is zero
00799       Expr zero_lemma = orExpr(zero).iffExpr(result.eqExpr(rat(0)));
00800       Expr positive_lemma = positive.impExpr(geExpr(result, rat(0)));
00801       Expr negative_lemma = negative.impExpr(leExpr(result, rat(0)));
00802       Expr lemma = positive_lemma.andExpr(negative_lemma.andExpr(zero_lemma));
00803 
00804       Proof split_pf;
00805       if (withProof()) split_pf = newPf("multiplicative_sign_split", e, lemma);
00806       Theorem case_split_thm = newTheorem(lemma, Assumptions::emptyAssump(), split_pf);
00807 
00808       TRACE("arith nonlinear", "adding sign split: ", lemma, "");
00809 
00810       d_theoryArith->addMultiplicativeSignSplit(case_split_thm);
00811     }
00812   }
00813 
00814   return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
00815 }
00816 
00817 
00818 Theorem
00819 ArithTheoremProducerOld::canonInvertConst(const Expr& e)
00820 {
00821   if(CHECK_PROOFS)
00822     CHECK_SOUND(isRational(e), "expecting a rational: e = "+e.toString());
00823 
00824   Proof pf;
00825 
00826   if (withProof()) {
00827     pf = newPf("canon_invert_const", e);
00828   }
00829   const Rational& er = e.getRational();
00830   return newRWTheorem((rat(1)/e), rat(er==0? 0 : (1/er)), Assumptions::emptyAssump(), pf);
00831 }
00832 
00833 
00834 Theorem
00835 ArithTheoremProducerOld::canonInvertLeaf(const Expr& e)
00836 {
00837   Proof pf;
00838 
00839   if (withProof()) {
00840     pf = newPf("canon_invert_leaf", e);
00841   }
00842   return newRWTheorem((rat(1)/e), powExpr(rat(-1), e), Assumptions::emptyAssump(), pf);
00843 }
00844 
00845 
00846 Theorem
00847 ArithTheoremProducerOld::canonInvertPow(const Expr& e)
00848 {
00849   DebugAssert(e.getKind() == POW, "expecting a rational"+e[0].toString());
00850 
00851   Proof pf;
00852 
00853   if (withProof()) {
00854     pf = newPf("canon_invert_pow", e);
00855   }
00856   if (e[0].getRational() == -1)
00857     return newRWTheorem((rat(1)/e), e[1], Assumptions::emptyAssump(), pf);
00858   else
00859     return newRWTheorem((rat(1)/e),
00860                         powExpr(rat(-e[0].getRational()), e[1]),
00861                         Assumptions::emptyAssump(),
00862                         pf);
00863 }
00864 
00865 Theorem
00866 ArithTheoremProducerOld::canonInvertMult(const Expr& e)
00867 {
00868   DebugAssert(e.getKind() == MULT, "expecting a rational"+e[0].toString());
00869 
00870   Proof pf;
00871 
00872   if (withProof()) {
00873     pf = newPf("canon_invert_mult", e);
00874   }
00875 
00876   DebugAssert(e.arity() > 1, "MULT should have arity > 1"+e.toString());
00877   Expr result = canonInvert(e[0]).getRHS();
00878   for (int i = 1; i < e.arity(); ++i) {
00879     result =
00880       canonMultMtermMterm(result * canonInvert(e[i]).getRHS()).getRHS();
00881   }
00882   return newRWTheorem((rat(1)/e), result, Assumptions::emptyAssump(), pf);
00883 }
00884 
00885 
00886 // Given an expression e in Canonic form generate 1/e in canonic form
00887 // This function assumes that e is not a PLUS expression
00888 Theorem
00889 ArithTheoremProducerOld::canonInvert(const Expr& e)
00890 {
00891   DebugAssert(e.getKind() != PLUS,
00892               "Cannot do inverse on a PLUS"+e.toString());
00893   switch (e.getKind()) {
00894   case RATIONAL_EXPR:
00895     return canonInvertConst(e);
00896     break;
00897   case POW:
00898     return canonInvertPow(e);
00899     break;
00900   case MULT:
00901     return canonInvertMult(e);
00902     break;
00903   default:
00904     // leaf
00905     return canonInvertLeaf(e);
00906     break;
00907   }
00908 }
00909 
00910 
00911 Theorem ArithTheoremProducerOld::moveSumConstantRight(const Expr& e) {
00912 
00913   // Check soundness of the rule if necessary
00914   if (CHECK_PROOFS) {
00915     CHECK_SOUND(isIneq(e) || e.isEq(), "moveSumConstantRight: input must be Eq or Ineq: " + e.toString());
00916     CHECK_SOUND(isRational(e[0]) || isPlus(e[0]), "moveSumConstantRight: left side must be a canonised sum: " + e.toString());
00917     CHECK_SOUND(isRational(e[1]) && e[1].getRational() == 0, "moveSumConstantRight: right side must be 0: " + e.toString());
00918   }
00919 
00920   // The rational constant of the sum
00921   Rational r = 0;
00922 
00923   // The right hand side of the expression
00924   Expr right = e[0];
00925 
00926   // The vector of sum terms
00927   vector<Expr> sumTerms;
00928 
00929   // Get all the non rational children and
00930   if (!right.isRational())
00931     for(Expr::iterator it = right.begin(); it != right.end(); it ++) {
00932       // If the term is rational then add the rational number to r
00933       if ((*it).isRational()) r = r + (*it).getRational();
00934       // Otherwise just add the sumTerm to the sumTerms
00935       else sumTerms.push_back((*it));
00936     }
00937 
00938   // Setup the new expression
00939   Expr transformed;
00940   if (sumTerms.size() > 1)
00941     // If the number of summands is > 1 return the sum of them
00942     transformed = Expr(e.getKind(), plusExpr(sumTerms), rat(-r));
00943   else
00944     // Otherwise return the one summand as itself
00945     transformed = Expr(e.getKind(), sumTerms[0], rat(-r));
00946 
00947 
00948   // If proof is needed set it up
00949   Proof pf;
00950   if (withProof()) pf = newPf("arithm_sum_constant_right", e);
00951 
00952   // Retrun the theorem explaining the transformation
00953   return newRWTheorem(e, transformed, Assumptions::emptyAssump(), pf);
00954 }
00955 
00956 Theorem
00957 ArithTheoremProducerOld::canonDivide(const Expr& e)
00958 {
00959   DebugAssert(e.getKind() == DIVIDE, "Expecting Divide"+e.toString());
00960   Proof pf;
00961 
00962   if (withProof()) {
00963     pf = newPf("canon_invert_divide", e);
00964   }
00965 
00966   Theorem thm = newRWTheorem(e, e[0]*(canonInvert(e[1]).getRHS()), Assumptions::emptyAssump(), pf);
00967 
00968   return d_theoryArith->transitivityRule(thm, canonMult(thm.getRHS()));
00969 }
00970 
00971 
00972 // Rules for multiplication
00973 // t*c ==> c*t, takes constant c and term t
00974 Theorem
00975 ArithTheoremProducerOld::canonMultTermConst(const Expr& c, const Expr& t) {
00976   Proof pf;
00977   if(CHECK_PROOFS) {
00978     CHECK_SOUND(isRational(c),
00979                 CLASS_NAME "::canonMultTermConst:\n  "
00980                 "c is not a constant: " + c.toString());
00981   }
00982   if(withProof()) pf = newPf("canon_mult_term_const", c, t);
00983   return newRWTheorem((t*c), (c*t), Assumptions::emptyAssump(), pf);
00984 }
00985 
00986 // Rules for multiplication
00987 // t1*t2 ==> Error, takes t1 and t2 where both are non-constants
00988 Theorem
00989 ArithTheoremProducerOld::canonMultTerm1Term2(const Expr& t1, const Expr& t2) {
00990   // Proof pf;
00991   // if(withProof()) pf = newPf("canon_mult_term1_term2", t1, t2);
00992   if(CHECK_PROOFS) {
00993     CHECK_SOUND(false, "Fatal Error: We don't support multiplication"
00994                 "of two non constant terms at this time "
00995                 + t1.toString() + " and " + t2.toString());
00996   }
00997   return Theorem();
00998 }
00999 
01000 // Rules for multiplication
01001 // 0*x = 0, takes x
01002 Theorem ArithTheoremProducerOld::canonMultZero(const Expr& e) {
01003   Proof pf;
01004   if(withProof()) pf = newPf("canon_mult_zero", e);
01005   return newRWTheorem((rat(0)*e), rat(0), Assumptions::emptyAssump(), pf);
01006 }
01007 
01008 // Rules for multiplication
01009 // 1*x ==> x, takes x
01010 Theorem ArithTheoremProducerOld::canonMultOne(const Expr& e) {
01011   Proof pf;
01012   if(withProof()) pf = newPf("canon_mult_one", e);
01013   return newRWTheorem((rat(1)*e), e, Assumptions::emptyAssump(), pf);
01014 }
01015 
01016 // Rules for multiplication
01017 // c1*c2 ==> c', takes constant c1*c2
01018 Theorem
01019 ArithTheoremProducerOld::canonMultConstConst(const Expr& c1, const Expr& c2) {
01020   Proof pf;
01021   if(CHECK_PROOFS) {
01022     CHECK_SOUND(isRational(c1),
01023                 CLASS_NAME "::canonMultConstConst:\n  "
01024                 "c1 is not a constant: " + c1.toString());
01025     CHECK_SOUND(isRational(c2),
01026                 CLASS_NAME "::canonMultConstConst:\n  "
01027                 "c2 is not a constant: " + c2.toString());
01028   }
01029   if(withProof()) pf = newPf("canon_mult_const_const", c1, c2);
01030   return
01031     newRWTheorem((c1*c2), rat(c1.getRational()*c2.getRational()), Assumptions::emptyAssump(), pf);
01032 }
01033 
01034 // Rules for multiplication
01035 // c1*(c2*t) ==> c'*t, takes c1 and c2 and t
01036 Theorem
01037 ArithTheoremProducerOld::canonMultConstTerm(const Expr& c1,
01038                                          const Expr& c2,const Expr& t) {
01039   Proof pf;
01040   if(CHECK_PROOFS) {
01041     CHECK_SOUND(isRational(c1),
01042                 CLASS_NAME "::canonMultConstTerm:\n  "
01043                 "c1 is not a constant: " + c1.toString());
01044     CHECK_SOUND(isRational(c2),
01045                 CLASS_NAME "::canonMultConstTerm:\n  "
01046                 "c2 is not a constant: " + c2.toString());
01047   }
01048 
01049   if(withProof()) pf = newPf("canon_mult_const_term", c1, c2, t);
01050   return
01051     newRWTheorem(c1*(c2*t), rat(c1.getRational()*c2.getRational())*t, Assumptions::emptyAssump(), pf);
01052 }
01053 
01054 // Rules for multiplication
01055 // c1*(+ c2 v1 ...) ==> (+ c1c2 c1v1 ...), takes c1 and the sum
01056 Theorem
01057 ArithTheoremProducerOld::canonMultConstSum(const Expr& c1, const Expr& sum) {
01058   Proof pf;
01059   std::vector<Expr> sumKids;
01060 
01061   if(CHECK_PROOFS) {
01062     CHECK_SOUND(isRational(c1),
01063                 CLASS_NAME "::canonMultConstTerm:\n  "
01064                 "c1 is not a constant: " + c1.toString());
01065     CHECK_SOUND(PLUS == sum.getKind(),
01066                 CLASS_NAME "::canonMultConstTerm:\n  "
01067                 "the kind must be a PLUS: " + sum.toString());
01068   }
01069   Expr::iterator i = sum.begin();
01070   for(; i != sum.end(); ++i)
01071     sumKids.push_back(c1*(*i));
01072   Expr ret = plusExpr(sumKids);
01073   if(withProof()) pf = newPf("canon_mult_const_sum", c1, sum, ret);
01074   return newRWTheorem((c1*sum),ret , Assumptions::emptyAssump(), pf);
01075 }
01076 
01077 
01078 // c^n = c' (compute the constant power expression)
01079 Theorem
01080 ArithTheoremProducerOld::canonPowConst(const Expr& e) {
01081   if(CHECK_PROOFS) {
01082     CHECK_SOUND(e.getKind() == POW && e.arity() == 2
01083     && e[0].isRational() && e[1].isRational(),
01084     "ArithTheoremProducerOld::canonPowConst("+e.toString()+")");
01085   }
01086   const Rational& p = e[0].getRational();
01087   const Rational& base = e[1].getRational();
01088   if(CHECK_PROOFS) {
01089     CHECK_SOUND(p.isInteger(),
01090     "ArithTheoremProducerOld::canonPowConst("+e.toString()+")");
01091   }
01092   Expr res;
01093   if (base == 0 && p < 0) {
01094     res = rat(0);
01095   }
01096   else res = rat(pow(p, base));
01097   Proof pf;
01098   if(withProof())
01099     pf = newPf("canon_pow_const", e, res);
01100   return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
01101 }
01102 
01103 
01104 // Rules for addition
01105 // flattens the input. accepts a PLUS expr
01106 Theorem
01107 ArithTheoremProducerOld::canonFlattenSum(const Expr& e) {
01108   Proof pf;
01109   std::vector<Expr> sumKids;
01110   if(CHECK_PROOFS) {
01111     CHECK_SOUND(PLUS == e.getKind(),
01112                 CLASS_NAME "::canonFlattenSum:\n"
01113                 "input must be a PLUS:" + e.toString());
01114   }
01115 
01116   Expr::iterator i = e.begin();
01117   for(; i != e.end(); ++i){
01118     if (PLUS != (*i).getKind())
01119       sumKids.push_back(*i);
01120     else {
01121       Expr::iterator j = (*i).begin();
01122       for(; j != (*i).end(); ++j)
01123         sumKids.push_back(*j);
01124     }
01125   }
01126   Expr ret =  plusExpr(sumKids);
01127   if(withProof()) pf = newPf("canon_flatten_sum", e,ret);
01128   return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
01129 }
01130 
01131 // Rules for addition
01132 // combine like terms. accepts a flattened PLUS expr
01133 Theorem
01134 ArithTheoremProducerOld::canonComboLikeTerms(const Expr& e) {
01135   Proof pf;
01136   std::vector<Expr> sumKids;
01137   ExprMap<Rational> sumHashMap;
01138   Rational constant = 0;
01139 
01140   if(CHECK_PROOFS) {
01141     Expr::iterator k = e.begin();
01142     for(; k != e.end(); ++k)
01143       CHECK_SOUND(!isPlus(*k),
01144                   CLASS_NAME "::canonComboLikeTerms:\n"
01145                   "input must be a flattened PLUS:" + k->toString());
01146   }
01147   Expr::iterator i = e.begin();
01148   for(; i != e.end(); ++i){
01149     if(i->isRational())
01150       constant = constant + i->getRational();
01151     else {
01152       if (!isMult(*i)) {
01153         if(0 == sumHashMap.count((*i)))
01154           sumHashMap[*i] = 1;
01155         else
01156           sumHashMap[*i] += 1;
01157       }
01158       else {
01159         if(0 == sumHashMap.count((*i)[1]))
01160           sumHashMap[(*i)[1]] = (*i)[0].getRational();
01161         else
01162           sumHashMap[(*i)[1]] = sumHashMap[(*i)[1]] + (*i)[0].getRational();
01163       }
01164     }
01165   }
01166 
01167   sumKids.push_back(rat(constant));
01168   ExprMap<Rational>::iterator j = sumHashMap.begin();
01169   for(; j != sumHashMap.end(); ++j) {
01170     if(0 == (*j).second)
01171       ;//do nothing
01172     else if (1 == (*j).second)
01173       sumKids.push_back((*j).first);
01174     else
01175       sumKids.push_back(rat((*j).second) * (*j).first);
01176   }
01177 
01178   //constant is same as sumKids[0].
01179   //corner cases: "0 + monomial" and "constant"(no monomials)
01180 
01181   Expr ret;
01182   if(2 == sumKids.size() && 0 == constant) ret = sumKids[1];
01183   else if (1 == sumKids.size()) ret = sumKids[0];
01184   else ret = plusExpr(sumKids);
01185 
01186   if(withProof()) pf = newPf("canon_combo_like_terms",e,ret);
01187   return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
01188 }
01189 
01190 
01191 // 0 = (* e1 e2 ...) <=> 0 = e1 OR 0 = e2 OR ...
01192 Theorem ArithTheoremProducerOld::multEqZero(const Expr& expr)
01193 {
01194   Proof pf;
01195   vector<Expr> kids;
01196 
01197   int side = expr[0].isRational() ? 1 : 0;
01198 
01199   vector<Expr> non_zero;
01200 
01201   Expr::iterator i = expr[side].begin(), iend = expr[side].end();
01202   for (; i != iend; ++i) {
01203     Expr x = *i;
01204     // If a rational it can't be 0, so it is false, i.e. just skip it
01205     if (x.isRational()) {
01206       CHECK_SOUND(x.getRational() != 0, "multEqZero: once of the constants is 0");
01207     } else {
01208       Expr leaf = x;
01209       if (isPow(x)) {
01210                     // We assume that 1 / 0 = 0 for simplicity and totality.
01211                     // Divisions by zero that affect the result can be identified by enabling TCCs.
01212                     //        if (x[0].getRational() < 0) {
01213                     //          non_zero.push_back(x[1].eqExpr(rat(0)).notExpr());
01214                     //          continue;
01215                     //        }
01216                     //        else
01217                     leaf = x[1];
01218       }
01219       if (leaf >= rat(0))
01220         kids.push_back(leaf.eqExpr(rat(0)));
01221       else
01222         kids.push_back(rat(0).eqExpr(leaf));
01223     }
01224   }
01225   Expr newExpr;
01226   if (kids.size() == 1) newExpr = kids[0];
01227   else newExpr = Expr(OR, kids);
01228   if (withProof()) {
01229     pf = newPf("multEqZero", expr);
01230   }
01231   //  if (non_zero.size() == 0)
01232   return newRWTheorem(expr, newExpr, Assumptions::emptyAssump(), pf);
01233   //  else return newRWTheorem(expr, Expr(OR, kids).andExpr(Expr(AND, non_zero)), Assumptions::emptyAssump(), pf);
01234 }
01235 
01236 
01237 // 0 = (^ c x) <=> false if c <=0
01238 //             <=> 0 = x if c > 0
01239 Theorem ArithTheoremProducerOld::powEqZero(const Expr& expr)
01240 {
01241   if (CHECK_PROOFS) {
01242     CHECK_SOUND(expr.isEq() && expr[0].isRational() &&
01243                 expr[0].getRational() == 0 &&
01244                 isPow(expr[1]) && expr[1].arity() == 2 &&
01245                 expr[1][0].isRational(),
01246                 "powEqZero invariant violated"+expr.toString());
01247   }
01248   Proof pf;
01249   if (withProof()) {
01250     pf = newPf("powEqZero", expr);
01251   }
01252   Rational r = expr[1][0].getRational();
01253   Expr res;
01254   if (r <= 0) {
01255     res = d_em->falseExpr();
01256   }
01257   else {
01258     res = rat(0).eqExpr(expr[1][1]);
01259   }
01260   return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
01261 }
01262 
01263 
01264 // x^n - y^n = 0 <=> x = y (if n is odd)
01265 // x^n - y^n = 0 <=> x = y OR x = -y (if n is even)
01266 Theorem ArithTheoremProducerOld::elimPower(const Expr& expr)
01267 {
01268   Expr power1, power2;
01269   bool ok = d_theoryArith->isPowersEquality(expr, power1, power2);
01270   if (CHECK_PROOFS)
01271     CHECK_SOUND(ok, "elimPower invariant violated"+expr.toString());
01272   Proof pf;
01273   if (withProof())
01274     pf = newPf("elimPower", expr);
01275   Rational r = power1[0].getRational();
01276   Expr res = power1[1].eqExpr(power2[1]);
01277   if (r % 2 == 0)
01278     res = res.orExpr(power1[1].eqExpr(-power2[1]));
01279   return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
01280 }
01281 
01282 
01283 // x^n = c <=> x = root (if n is odd and root^n = c)
01284 // x^n = c <=> x = root OR x = -root (if n is even and root^n = c)
01285 Theorem ArithTheoremProducerOld::elimPowerConst(const Expr& expr, const Rational& root)
01286 {
01287   if (CHECK_PROOFS)
01288       CHECK_SOUND(expr.isEq(), "elimPowerConst invariant violated" + expr.toString());
01289   Rational constant;
01290   Expr power;
01291   bool ok = d_theoryArith->isPowerEquality(expr, constant, power);
01292   if (CHECK_PROOFS) {
01293     CHECK_SOUND(ok, "elimPowerConst invariant violated" + expr.toString());
01294     CHECK_SOUND(pow(power[0].getRational(), root) == constant, "elimPowerConst invariant violated" + expr.toString());
01295   }
01296 
01297   Proof pf;
01298   if (withProof())
01299     pf = newPf("elimPowerConst", expr, rat(root));
01300   Rational r = power[0].getRational();
01301   Expr res = power[1].eqExpr(rat(root));
01302   if (r % 2 == 0)
01303     res = res.orExpr(power[1].eqExpr(rat(-root)));
01304 
01305   return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
01306 }
01307 
01308 
01309 // x^n = c <=> false (if n is even and c is negative)
01310 Theorem ArithTheoremProducerOld::evenPowerEqNegConst(const Expr& expr)
01311 {
01312   if (CHECK_PROOFS)
01313     CHECK_SOUND(expr.isEq(), "evenPowerEqNegConst, expecting equality, got " + expr.toString());
01314   Rational constant;
01315   Expr power;
01316   bool ok = d_theoryArith->isPowerEquality(expr, constant, power);
01317   if (CHECK_PROOFS) {
01318     CHECK_SOUND(ok, "evenPowerEqNegConst invariant violated" + expr.toString());
01319     CHECK_SOUND(constant < 0, "evenPowerEqNegConst invariant violated" + expr.toString());
01320     CHECK_SOUND(power[0].getRational().isInteger() && power[0].getRational() % 2 == 0, "evenPowerEqNegConst invariant violated" + expr.toString());
01321   }
01322   Proof pf;
01323   if (withProof())
01324     pf = newPf("evenPowerEqNegConst", expr);
01325   return newRWTheorem(expr, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
01326 }
01327 
01328 
01329 // x^n = c <=> ` (if x is an integer and c is not a perfect n power)
01330 Theorem ArithTheoremProducerOld::intEqIrrational(const Expr& expr, const Theorem& isIntx)
01331 {
01332   if (CHECK_PROOFS)
01333       CHECK_SOUND(expr.isEq(), "intEqIrrational invariant violated" + expr.toString());
01334   Rational constant;
01335   Expr power;
01336   bool ok = d_theoryArith->isPowerEquality(expr, constant, power);
01337   if (CHECK_PROOFS) {
01338     CHECK_SOUND(ok, "intEqIrrational invariant violated" + expr.toString());
01339     CHECK_SOUND(constant != 0, "intEqIrrational invariant violated" + expr.toString());
01340     CHECK_SOUND(power[0].getRational() > 0, "intEqIrrational invariant violated" + expr.toString());
01341     CHECK_SOUND(ratRoot(constant, power[0].getRational().getUnsigned()) == 0, "intEqIrrational invariant violated" + expr.toString());
01342     CHECK_SOUND(isIntPred(isIntx.getExpr()) && isIntx.getExpr()[0] == expr[0], "intEqIrrational invariant violated" + isIntx.getExpr()[0].toString());
01343   }
01344 
01345   const Assumptions& assump(isIntx.getAssumptionsRef());
01346   Proof pf;
01347   if (withProof())
01348     pf = newPf("int_eq_irr", expr, isIntx.getProof());
01349   return newRWTheorem(expr, d_em->falseExpr(), assump, pf);
01350 }
01351 
01352 
01353 // e[0] kind e[1] <==> true when e[0] kind e[1],
01354 // false when e[0] !kind e[1], for constants only
01355 Theorem ArithTheoremProducerOld::constPredicate(const Expr& e) {
01356   if(CHECK_PROOFS) {
01357     CHECK_SOUND(e.arity() == 2 && isRational(e[0]) && isRational(e[1]),
01358                 CLASS_NAME "::constPredicate:\n  "
01359                 "non-const parameters: " + e.toString());
01360   }
01361   Proof pf;
01362   bool result(false);
01363   int kind = e.getKind();
01364   Rational r1 = e[0].getRational(), r2 = e[1].getRational();
01365   switch(kind) {
01366   case EQ:
01367     result = (r1 == r2)?true : false;
01368     break;
01369   case LT:
01370     result = (r1 < r2)?true : false;
01371     break;
01372   case LE:
01373     result = (r1 <= r2)?true : false;
01374     break;
01375   case GT:
01376     result = (r1 > r2)?true : false;
01377     break;
01378   case GE:
01379     result = (r1 >= r2)?true : false;
01380     break;
01381   default:
01382     if(CHECK_PROOFS) {
01383       CHECK_SOUND(false,
01384                   "ArithTheoremProducerOld::constPredicate: wrong kind");
01385     }
01386     break;
01387   }
01388   Expr ret = (result) ? d_em->trueExpr() : d_em->falseExpr();
01389   if(withProof()) pf = newPf("const_predicate", e,ret);
01390   return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
01391 }
01392 
01393 // e[0] kind e[1] <==> 0 kind e[1] - e[0]
01394 Theorem ArithTheoremProducerOld::rightMinusLeft(const Expr& e)
01395 {
01396   Proof pf;
01397   int kind = e.getKind();
01398   if(CHECK_PROOFS) {
01399     CHECK_SOUND((EQ==kind) ||
01400                 (LT==kind) ||
01401                 (LE==kind) ||
01402                 (GE==kind) ||
01403                 (GT==kind),
01404                 "ArithTheoremProducerOld::rightMinusLeft: wrong kind");
01405   }
01406   if(withProof()) pf = newPf("right_minus_left",e);
01407   return newRWTheorem(e, Expr(e.getOp(), rat(0), e[1] - e[0]), Assumptions::emptyAssump(), pf);
01408 }
01409 
01410 
01411 // e[0] kind e[1] <==> 0 kind e[1] - e[0]
01412 Theorem ArithTheoremProducerOld::leftMinusRight(const Expr& e)
01413 {
01414   Proof pf;
01415   int kind = e.getKind();
01416   if(CHECK_PROOFS) {
01417     CHECK_SOUND((EQ==kind) ||
01418                 (LT==kind) ||
01419                 (LE==kind) ||
01420                 (GE==kind) ||
01421                 (GT==kind),
01422                 "ArithTheoremProducerOld::rightMinusLeft: wrong kind");
01423   }
01424   if(withProof()) pf = newPf("left_minus_right",e);
01425   return newRWTheorem(e, Expr(e.getOp(), e[0] - e[1], rat(0)), Assumptions::emptyAssump(), pf);
01426 }
01427 
01428 
01429 // x kind y <==> x + z kind y + z
01430 Theorem ArithTheoremProducerOld::plusPredicate(const Expr& x,
01431                                       const Expr& y,
01432                                       const Expr& z, int kind) {
01433   if(CHECK_PROOFS) {
01434     CHECK_SOUND((EQ==kind) ||
01435                 (LT==kind) ||
01436                 (LE==kind) ||
01437                 (GE==kind) ||
01438                 (GT==kind),
01439                 "ArithTheoremProducerOld::plusPredicate: wrong kind");
01440   }
01441   Proof pf;
01442   Expr left = Expr(kind, x, y);
01443   Expr right = Expr(kind, x + z, y + z);
01444   if(withProof()) pf = newPf("plus_predicate",left,right);
01445   return newRWTheorem(left, right, Assumptions::emptyAssump(), pf);
01446 }
01447 
01448 // x = y <==> x * z = y * z
01449 Theorem ArithTheoremProducerOld::multEqn(const Expr& x,
01450                                       const Expr& y,
01451                                       const Expr& z) {
01452   Proof pf;
01453   if(CHECK_PROOFS)
01454     CHECK_SOUND(z.isRational() && z.getRational() != 0,
01455     "ArithTheoremProducerOld::multEqn(): multiplying equation by 0");
01456   if(withProof()) pf = newPf("mult_eqn", x, y, z);
01457   return newRWTheorem(x.eqExpr(y), (x * z).eqExpr(y * z), Assumptions::emptyAssump(), pf);
01458 }
01459 
01460 
01461 // x = y <==> z=0 OR x * 1/z = y * 1/z
01462 Theorem ArithTheoremProducerOld::divideEqnNonConst(const Expr& x,
01463                                                    const Expr& y,
01464                                                    const Expr& z) {
01465   Proof pf;
01466   if(withProof()) pf = newPf("mult_eqn_nonconst", x, y, z);
01467   return newRWTheorem(x.eqExpr(y), (z.eqExpr(rat(0))).orExpr((x / z).eqExpr(y / z)),
01468                       Assumptions::emptyAssump(), pf);
01469 }
01470 
01471 
01472 // if z is +ve, return e[0] LT|LE|GT|GE e[1] <==> e[0]*z LT|LE|GT|GE e[1]*z
01473 // if z is -ve, return e[0] LT|LE|GT|GE e[1] <==> e[1]*z LT|LE|GT|GE e[0]*z
01474 Theorem ArithTheoremProducerOld::multIneqn(const Expr& e, const Expr& z)
01475 {
01476   int kind = e.getKind();
01477 
01478   if(CHECK_PROOFS) {
01479     CHECK_SOUND((LT==kind) ||
01480                 (LE==kind) ||
01481                 (GE==kind) ||
01482                 (GT==kind),
01483                 "ArithTheoremProducerOld::multIneqn: wrong kind");
01484     CHECK_SOUND(z.isRational() && z.getRational() != 0,
01485                 "ArithTheoremProducerOld::multIneqn: "
01486     "z must be non-zero rational: " + z.toString());
01487   }
01488   Op op(e.getOp());
01489   Proof pf;
01490 
01491   Expr ret;
01492   if(0 < z.getRational())
01493     ret = Expr(op, e[0]*z, e[1]*z);
01494   else
01495     ret = Expr(op, e[1]*z, e[0]*z);
01496   if(withProof()) pf = newPf("mult_ineqn", e, ret);
01497   return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
01498 }
01499 
01500 
01501 //
01502 // If expr:
01503 // If b > 0 then (0 <= a + bx) <==> (0 <= floor(a/b) + x)
01504 //    b < 0 then (0 <= a + bx) <==> (0 >= ceil(a/b) + x)
01505 //    b > 0 then (0 >= a + bx) <==> (0 >= ceil(a/b) + x)
01506 //    b < 0 then (0 >= a + bx) <==> (0 <= floor(a/b) + x)
01507 //
01508 Theorem ArithTheoremProducerOld::simpleIneqInt(const Expr& ineq, const Theorem& isIntRHS)
01509 {
01510   // Get the inequality parts
01511   Expr lhs = ineq[0];
01512   Expr rhs = ineq[1];
01513 
01514   // Get the kind of the inequality
01515   int kind = ineq.getKind();
01516 
01517 
01518   if(CHECK_PROOFS) {
01519     // isIntRHS should be an int proof of rhs
01520     const Expr& isIntRHSExpr = isIntRHS.getExpr();
01521     CHECK_SOUND(isIntPred(isIntRHSExpr) && isIntRHSExpr[0] == rhs, "ArithTheoremProducerOld::multSimpleIneqnInt: not an integer proof of rhs");
01522 
01523     // It's an inequality
01524     CHECK_SOUND((LT == kind) || (LE==kind) || (GE==kind) || (GT==kind), "ArithTheoremProducerOld::multSimpleIneqnInt: wrong kind");
01525 
01526     // Left-hand side is 0
01527     CHECK_SOUND(lhs.isRational() && lhs.getRational() == 0, "ArithTheoremProducerOld::multSimpleIneqnInt: left-hand side must be 0");
01528 
01529     // Tight hand side is a sum (a + b*x) where a and b are integers, x is a var
01530     CHECK_SOUND(isPlus(rhs), "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side must be a plus");
01531     CHECK_SOUND(rhs.arity() == 2, "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus");
01532 
01533     Expr a  = rhs[0]; // Should be an integer
01534     Expr bx = rhs[1]; // Should be an integer multiplied by a variable
01535 
01536     // a is an integer
01537     CHECK_SOUND(a.isRational() && a.getRational().isInteger(), "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of a constant");
01538 
01539     // bx should be a multiplication of an intgere and a variable
01540     CHECK_SOUND(isMult(bx) && bx.arity() == 2, "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of and a multiplication");
01541     Expr b = bx[0];
01542     Expr x = bx[1];
01543 
01544     // b should be an integer
01545     CHECK_SOUND(b.isRational() && b.getRational().isInteger(), "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of and a multiplication of a constant");
01546     // x should be a variable
01547     CHECK_SOUND(x.isVar(), "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of and a multiplication of a constant and a leaf");
01548 
01549     // GCD(a, b) should be 1
01550     //CHECK_SOUND(gcd(a.getRational(), b.getRational()) == 1, "ArithTheoremProducerOld::multSimpleIneqnInt: inequation not normalized!!!");
01551   }
01552 
01553   Proof pf;
01554   if(withProof()) {
01555     vector<Proof> pfs;
01556     pfs.push_back(isIntRHS.getProof());
01557     pf = newPf("simpleineqint", ineq, pf);
01558   }
01559 
01560   Rational a = rhs[0].getRational();
01561   Rational b = rhs[1][0].getRational();
01562   Expr x = rhs[1][1];
01563 
01564   Rational new_const;
01565   Expr ret;
01566   switch (kind) {
01567     case LT:
01568       if (b > 0) {
01569         new_const = floor(a/b);
01570         if (new_const != 0)
01571           ret = Expr(kind, rat(0), rat(new_const) + x);
01572         else
01573           ret = Expr(kind, rat(0), x);
01574       }
01575       else {
01576         new_const = ceil(a/b);
01577         //ret = geExpr(rat(0), rat(new_const) + x);
01578         if (new_const != 0)
01579           ret = Expr(kind, rat(0), rat(-new_const) + rat(-1)*x);
01580         else
01581           ret = Expr(kind, rat(0), rat(-1)*x);
01582       }
01583       break;
01584       break;
01585     case LE:
01586       if (b > 0) {
01587         new_const = floor(a/b);
01588         if (new_const != 0)
01589           ret = Expr(kind, rat(0), rat(new_const) + x);
01590         else
01591           ret = Expr(kind, rat(0), x);
01592       }
01593       else {
01594         new_const = ceil(a/b);
01595         //ret = geExpr(rat(0), rat(new_const) + x);
01596         if (new_const != 0)
01597           ret = Expr(kind, rat(0), rat(-new_const) + rat(-1)*x);
01598         else
01599           ret = Expr(kind, rat(0), rat(-1)*x);
01600       }
01601       break;
01602     case GE:
01603     case GT:
01604       // Setup the result kind
01605       if (kind == GT) kind = LT;
01606       else kind = LE;
01607 
01608       if (b > 0) {
01609         new_const = ceil(a/b);
01610         //ret = geExpr(rat(0), rat(new_const) + x);
01611         if (new_const != 0)
01612           ret = Expr(kind, rat(0), rat(-new_const) + rat(-1)*x);
01613         else
01614           ret = Expr(kind, rat(0), rat(-1)*x);
01615       }
01616       else {
01617         new_const = floor(a/b);
01618         if (new_const != 0)
01619           ret = Expr(kind, rat(0), rat(new_const) + x);
01620         else
01621           ret = Expr(kind, rat(0), x);
01622       }
01623       break;
01624   }
01625 
01626   // Return the new theorem
01627   return newRWTheorem(ineq, ret, Assumptions::emptyAssump(), pf);
01628 }
01629 
01630 
01631 Theorem ArithTheoremProducerOld::eqToIneq(const Expr& e) {
01632 
01633     // Check soundness of the rule if necessary
01634   if (CHECK_PROOFS)
01635     CHECK_SOUND(e.isEq(), "eqToIneq: input must be an equality: " + e.toString());
01636 
01637     // The proof object we will use
01638     Proof pf;
01639 
01640   // The parts of the equality x = y
01641     const Expr& x = e[0];
01642     const Expr& y = e[1];
01643 
01644   // Setup the proof if needed
01645     if (withProof())
01646       pf = newPf("eqToIneq", e);
01647 
01648     // Retrun the theorem explaining the transformation
01649   return newRWTheorem(e, leExpr(x,y).andExpr(geExpr(x,y)), Assumptions::emptyAssump(), pf);
01650 }
01651 
01652 // "op1 GE|GT op2" <==> op2 LE|LT op1
01653 Theorem ArithTheoremProducerOld::flipInequality(const Expr& e)
01654 {
01655   Proof pf;
01656   if(CHECK_PROOFS) {
01657     CHECK_SOUND(isGT(e) || isGE(e),
01658                 "ArithTheoremProducerOld::flipInequality: wrong kind: " +
01659                 e.toString());
01660   }
01661 
01662   int kind = isGE(e) ? LE : LT;
01663   Expr ret =  Expr(kind, e[1], e[0]);
01664   if(withProof()) pf = newPf("flip_inequality", e,ret);
01665   return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
01666 }
01667 
01668 
01669 // NOT (op1 LT op2)  <==> (op1 GE op2)
01670 // NOT (op1 LE op2)  <==> (op1 GT op2)
01671 // NOT (op1 GT op2)  <==> (op1 LE op2)
01672 // NOT (op1 GE op2)  <==> (op1 LT op2)
01673 Theorem ArithTheoremProducerOld::negatedInequality(const Expr& e)
01674 {
01675   const Expr& ineq = e[0];
01676   if(CHECK_PROOFS) {
01677     CHECK_SOUND(e.isNot(),
01678                 "ArithTheoremProducerOld::negatedInequality: wrong kind: " +
01679                 e.toString());
01680     CHECK_SOUND(isIneq(ineq),
01681                 "ArithTheoremProducerOld::negatedInequality: wrong kind: " +
01682                 (ineq).toString());
01683   }
01684   Proof pf;
01685   if(withProof()) pf = newPf("negated_inequality", e);
01686 
01687   int kind;
01688   // NOT (op1 LT op2)  <==> (op1 GE op2)
01689   // NOT (op1 LE op2)  <==> (op1 GT op2)
01690   // NOT (op1 GT op2)  <==> (op1 LE op2)
01691   // NOT (op1 GE op2)  <==> (op1 LT op2)
01692   kind =
01693     isLT(ineq) ? GE :
01694     isLE(ineq) ? GT :
01695     isGT(ineq) ? LE :
01696     LT;
01697   return newRWTheorem(e, Expr(kind, ineq[0], ineq[1]), Assumptions::emptyAssump(), pf);
01698 }
01699 
01700 //takes two ineqs "|- alpha LT|LE t" and "|- t LT|LE beta"
01701 //and returns "|- alpha LT|LE beta"
01702 Theorem ArithTheoremProducerOld::realShadow(const Theorem& alphaLTt,
01703                                          const Theorem& tLTbeta)
01704 {
01705   const Expr& expr1 = alphaLTt.getExpr();
01706   const Expr& expr2 = tLTbeta.getExpr();
01707   if(CHECK_PROOFS) {
01708     CHECK_SOUND((isLE(expr1) || isLT(expr1)) &&
01709                 (isLE(expr2) || isLT(expr2)),
01710                 "ArithTheoremProducerOld::realShadow: Wrong Kind: " +
01711                 alphaLTt.toString() +  tLTbeta.toString());
01712 
01713     CHECK_SOUND(expr1[1] == expr2[0],
01714                 "ArithTheoremProducerOld::realShadow:"
01715                 " t must be same for both inputs: " +
01716                 expr1[1].toString() + " , " + expr2[0].toString());
01717   }
01718   Assumptions a(alphaLTt, tLTbeta);
01719   int firstKind = expr1.getKind();
01720   int secondKind = expr2.getKind();
01721   int kind = (firstKind == secondKind) ? firstKind : LT;
01722   Proof pf;
01723   if(withProof()) {
01724     vector<Proof> pfs;
01725     pfs.push_back(alphaLTt.getProof());
01726     pfs.push_back(tLTbeta.getProof());
01727     pf = newPf("real_shadow",expr1, expr2, pfs);
01728   }
01729   return newTheorem(Expr(kind, expr1[0], expr2[1]), a, pf);
01730 }
01731 
01732 //! alpha <= t <= alpha ==> t = alpha
01733 
01734 /*! takes two ineqs "|- alpha LE t" and "|- t LE alpha"
01735   and returns "|- t = alpha"
01736 */
01737 Theorem ArithTheoremProducerOld::realShadowEq(const Theorem& alphaLEt,
01738                                            const Theorem& tLEalpha)
01739 {
01740   const Expr& expr1 = alphaLEt.getExpr();
01741   const Expr& expr2 = tLEalpha.getExpr();
01742   if(CHECK_PROOFS) {
01743     CHECK_SOUND(isLE(expr1) && isLE(expr2),
01744                 "ArithTheoremProducerOld::realShadowLTLE: Wrong Kind: " +
01745                 alphaLEt.toString() +  tLEalpha.toString());
01746 
01747     CHECK_SOUND(expr1[1] == expr2[0],
01748                 "ArithTheoremProducerOld::realShadowLTLE:"
01749                 " t must be same for both inputs: " +
01750                 alphaLEt.toString() + " , " + tLEalpha.toString());
01751 
01752     CHECK_SOUND(expr1[0] == expr2[1],
01753                 "ArithTheoremProducerOld::realShadowLTLE:"
01754                 " alpha must be same for both inputs: " +
01755                 alphaLEt.toString() + " , " + tLEalpha.toString());
01756   }
01757   Assumptions a(alphaLEt, tLEalpha);
01758   Proof pf;
01759   if(withProof()) {
01760     vector<Proof> pfs;
01761     pfs.push_back(alphaLEt.getProof());
01762     pfs.push_back(tLEalpha.getProof());
01763     pf = newPf("real_shadow_eq", alphaLEt.getExpr(), tLEalpha.getExpr(), pfs);
01764   }
01765   return newRWTheorem(expr1[0], expr1[1], a, pf);
01766 }
01767 
01768 Theorem
01769 ArithTheoremProducerOld::finiteInterval(const Theorem& aLEt,
01770              const Theorem& tLEac,
01771              const Theorem& isInta,
01772              const Theorem& isIntt) {
01773   const Expr& e1 = aLEt.getExpr();
01774   const Expr& e2 = tLEac.getExpr();
01775   if(CHECK_PROOFS) {
01776     CHECK_SOUND(isLE(e1) && isLE(e2),
01777     "ArithTheoremProducerOld::finiteInterval:\n e1 = "
01778     +e1.toString()+"\n e2 = "+e2.toString());
01779     // term 't' is the same in both inequalities
01780     CHECK_SOUND(e1[1] == e2[0],
01781     "ArithTheoremProducerOld::finiteInterval:\n e1 = "
01782     +e1.toString()+"\n e2 = "+e2.toString());
01783     // RHS in e2 is (a+c)
01784     CHECK_SOUND(isPlus(e2[1]) && e2[1].arity() == 2,
01785     "ArithTheoremProducerOld::finiteInterval:\n e1 = "
01786     +e1.toString()+"\n e2 = "+e2.toString());
01787     // term 'a' in LHS of e1 and RHS of e2 is the same
01788     CHECK_SOUND(e1[0] == e2[1][0],
01789     "ArithTheoremProducerOld::finiteInterval:\n e1 = "
01790     +e1.toString()+"\n e2 = "+e2.toString());
01791     // 'c' in the RHS of e2 is a positive integer constant
01792     CHECK_SOUND(e2[1][1].isRational() && e2[1][1].getRational().isInteger()
01793     && e2[1][1].getRational() >= 1,
01794     "ArithTheoremProducerOld::finiteInterval:\n e1 = "
01795     +e1.toString()+"\n e2 = "+e2.toString());
01796     // Integrality constraints
01797     const Expr& isIntaExpr = isInta.getExpr();
01798     const Expr& isInttExpr = isIntt.getExpr();
01799     CHECK_SOUND(isIntPred(isIntaExpr) && isIntaExpr[0] == e1[0],
01800     "Wrong integrality constraint:\n e1 = "
01801     +e1.toString()+"\n isInta = "+isIntaExpr.toString());
01802     CHECK_SOUND(isIntPred(isInttExpr) && isInttExpr[0] == e1[1],
01803     "Wrong integrality constraint:\n e1 = "
01804     +e1.toString()+"\n isIntt = "+isInttExpr.toString());
01805   }
01806   vector<Theorem> thms;
01807   thms.push_back(aLEt);
01808   thms.push_back(tLEac);
01809   thms.push_back(isInta);
01810   thms.push_back(isIntt);
01811   Assumptions a(thms);
01812   Proof pf;
01813   if(withProof()) {
01814     vector<Expr> es;
01815     vector<Proof> pfs;
01816     es.push_back(e1);
01817     es.push_back(e2);
01818     es.push_back(isInta.getExpr());
01819     es.push_back(isIntt.getExpr());
01820     pfs.push_back(aLEt.getProof());
01821     pfs.push_back(tLEac.getProof());
01822     pfs.push_back(isInta.getProof());
01823     pfs.push_back(isIntt.getProof());
01824     pf = newPf("finite_interval", es, pfs);
01825   }
01826   // Construct GRAY_SHADOW(t, a, 0, c)
01827   Expr g(grayShadow(e1[1], e1[0], 0, e2[1][1].getRational()));
01828   return newTheorem(g, a, pf);
01829 }
01830 
01831 
01832 // Dark & Gray shadows when a <= b
01833 Theorem ArithTheoremProducerOld::darkGrayShadow2ab(const Theorem& betaLEbx,
01834             const Theorem& axLEalpha,
01835             const Theorem& isIntAlpha,
01836             const Theorem& isIntBeta,
01837             const Theorem& isIntx) {
01838   const Expr& expr1 = betaLEbx.getExpr();
01839   const Expr& expr2 = axLEalpha.getExpr();
01840   const Expr& isIntAlphaExpr = isIntAlpha.getExpr();
01841   const Expr& isIntBetaExpr = isIntBeta.getExpr();
01842   const Expr& isIntxExpr = isIntx.getExpr();
01843 
01844   if(CHECK_PROOFS) {
01845     CHECK_SOUND(isLE(expr1) && isLE(expr2),
01846                 "ArithTheoremProducerOld::darkGrayShadow2ab: Wrong Kind: " +
01847                 betaLEbx.toString() +  axLEalpha.toString());
01848   }
01849 
01850   const Expr& beta = expr1[0];
01851   const Expr& bx = expr1[1];
01852   const Expr& ax = expr2[0];
01853   const Expr& alpha = expr2[1];
01854   Expr a_expr, b_expr, x;
01855   d_theoryArith->separateMonomial(ax, a_expr, x);
01856   d_theoryArith->separateMonomial(bx, b_expr, x);
01857   Rational a = a_expr.getRational();
01858   Rational b = b_expr.getRational();
01859 
01860   if(CHECK_PROOFS) {
01861     // Integrality constraints
01862     CHECK_SOUND(isIntPred(isIntAlphaExpr) && isIntAlphaExpr[0] == alpha,
01863     "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01864     "wrong integrality constraint:\n alpha = "
01865     +alpha.toString()+"\n isIntAlpha = "
01866     +isIntAlphaExpr.toString());
01867     CHECK_SOUND(isIntPred(isIntBetaExpr) && isIntBetaExpr[0] == beta,
01868     "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01869     "wrong integrality constraint:\n beta = "
01870     +beta.toString()+"\n isIntBeta = "
01871     +isIntBetaExpr.toString());
01872     CHECK_SOUND(isIntPred(isIntxExpr) && isIntxExpr[0] == x,
01873     "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01874     "wrong integrality constraint:\n x = "
01875     +x.toString()+"\n isIntx = "
01876     +isIntxExpr.toString());
01877     // NOT FOR NONLINEAR: Expressions ax and bx should match on x
01878 //    CHECK_SOUND(!isMult(ax) || ax.arity() == 2,
01879 //    "ArithTheoremProducerOld::darkGrayShadow2ab:\n ax<=alpha: " +
01880 //                axLEalpha.toString());
01881 //    CHECK_SOUND(!isMult(bx) || (bx.arity() == 2 && bx[1] == x),
01882 //    "ArithTheoremProducerOld::darkGrayShadow2ab:\n beta<=bx: "
01883 //    +betaLEbx.toString()
01884 //    +"\n ax<=alpha: "+ axLEalpha.toString());
01885     CHECK_SOUND(1 <= a && a <= b && 2 <= b,
01886     "ArithTheoremProducerOld::darkGrayShadow2ab:\n beta<=bx: "
01887     +betaLEbx.toString()
01888     +"\n ax<=alpha: "+ axLEalpha.toString());
01889   }
01890   vector<Theorem> thms;
01891   thms.push_back(betaLEbx);
01892   thms.push_back(axLEalpha);
01893   thms.push_back(isIntAlpha);
01894   thms.push_back(isIntBeta);
01895   thms.push_back(isIntx);
01896   Assumptions A(thms);
01897 
01898   Expr bAlpha = multExpr(rat(b), alpha);
01899   Expr aBeta = multExpr(rat(a), beta);
01900   Expr t = minusExpr(bAlpha, aBeta);
01901   Expr d = geExpr(t, rat(a*b-1));
01902   Expr g = grayShadow(ax, alpha, -a+1, 0);
01903 
01904   Proof pf;
01905   if(withProof()) {
01906     vector<Expr> exprs;
01907     exprs.push_back(expr1);
01908     exprs.push_back(expr2);
01909     exprs.push_back(d);
01910     exprs.push_back(g);
01911 
01912     vector<Proof> pfs;
01913     pfs.push_back(betaLEbx.getProof());
01914     pfs.push_back(axLEalpha.getProof());
01915     pfs.push_back(isIntAlpha.getProof());
01916     pfs.push_back(isIntBeta.getProof());
01917     pfs.push_back(isIntx.getProof());
01918 
01919     pf = newPf("dark_grayshadow_2ab", exprs, pfs);
01920   }
01921 
01922   return newTheorem((d || g), A, pf);
01923 }
01924 
01925 // Dark & Gray shadows when b <= a
01926 Theorem ArithTheoremProducerOld::darkGrayShadow2ba(const Theorem& betaLEbx,
01927             const Theorem& axLEalpha,
01928             const Theorem& isIntAlpha,
01929             const Theorem& isIntBeta,
01930             const Theorem& isIntx) {
01931   const Expr& expr1 = betaLEbx.getExpr();
01932   const Expr& expr2 = axLEalpha.getExpr();
01933   const Expr& isIntAlphaExpr = isIntAlpha.getExpr();
01934   const Expr& isIntBetaExpr = isIntBeta.getExpr();
01935   const Expr& isIntxExpr = isIntx.getExpr();
01936 
01937   if(CHECK_PROOFS) {
01938     CHECK_SOUND(isLE(expr1) && isLE(expr2),
01939                 "ArithTheoremProducerOld::darkGrayShadow2ba: Wrong Kind: " +
01940                 betaLEbx.toString() +  axLEalpha.toString());
01941   }
01942 
01943   const Expr& beta = expr1[0];
01944   const Expr& bx = expr1[1];
01945   const Expr& ax = expr2[0];
01946   const Expr& alpha = expr2[1];
01947 
01948   Expr a_expr, b_expr, x;
01949   d_theoryArith->separateMonomial(ax, a_expr, x);
01950   d_theoryArith->separateMonomial(bx, b_expr, x);
01951   Rational a = a_expr.getRational();
01952   Rational b = b_expr.getRational();
01953 
01954   if(CHECK_PROOFS) {
01955   // Integrality constraints
01956     CHECK_SOUND(isIntPred(isIntAlphaExpr) && isIntAlphaExpr[0] == alpha,
01957     "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01958     "wrong integrality constraint:\n alpha = "
01959     +alpha.toString()+"\n isIntAlpha = "
01960     +isIntAlphaExpr.toString());
01961     CHECK_SOUND(isIntPred(isIntBetaExpr) && isIntBetaExpr[0] == beta,
01962     "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01963     "wrong integrality constraint:\n beta = "
01964     +beta.toString()+"\n isIntBeta = "
01965     +isIntBetaExpr.toString());
01966     CHECK_SOUND(isIntPred(isIntxExpr) && isIntxExpr[0] == x,
01967     "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
01968     "wrong integrality constraint:\n x = "
01969     +x.toString()+"\n isIntx = "
01970     +isIntxExpr.toString());
01971     // NOT FOR NONLINEAR: Expressions ax and bx should match on x
01972 //    CHECK_SOUND(!isMult(ax) || ax.arity() == 2,
01973 //    "ArithTheoremProducerOld::darkGrayShadow2ba:\n ax<=alpha: " +
01974 //                axLEalpha.toString());
01975 //    CHECK_SOUND(!isMult(bx) || (bx.arity() == 2 && bx[1] == x),
01976 //    "ArithTheoremProducerOld::darkGrayShadow2ba:\n beta<=bx: "
01977 //    +betaLEbx.toString()
01978 //    +"\n ax<=alpha: "+ axLEalpha.toString());
01979     CHECK_SOUND(1 <= b && b <= a && 2 <= a,
01980     "ArithTheoremProducerOld::darkGrayShadow2ba:\n beta<=bx: "
01981     +betaLEbx.toString()
01982     +"\n ax<=alpha: "+ axLEalpha.toString());
01983   }
01984   vector<Theorem> thms;
01985   thms.push_back(betaLEbx);
01986   thms.push_back(axLEalpha);
01987   thms.push_back(isIntAlpha);
01988   thms.push_back(isIntBeta);
01989   thms.push_back(isIntx);
01990   Assumptions A(thms);
01991   Proof pf;
01992   if(withProof()) {
01993     vector<Proof> pfs;
01994     pfs.push_back(betaLEbx.getProof());
01995     pfs.push_back(axLEalpha.getProof());
01996     pfs.push_back(isIntAlpha.getProof());
01997     pfs.push_back(isIntBeta.getProof());
01998     pfs.push_back(isIntx.getProof());
01999 
02000     pf = newPf("dark_grayshadow_2ba", betaLEbx.getExpr(),
02001          axLEalpha.getExpr(), pfs);
02002   }
02003 
02004   Expr bAlpha = multExpr(rat(b), alpha);
02005   Expr aBeta = multExpr(rat(a), beta);
02006   Expr t = minusExpr(bAlpha, aBeta);
02007   Expr d = geExpr(t, rat(a*b-1));
02008   Expr g = grayShadow(bx, beta, 0, b-1);
02009   return newTheorem((d || g), A, pf);
02010 }
02011 
02012 /*! takes a dark shadow and expands it into an inequality.
02013 */
02014 Theorem ArithTheoremProducerOld::expandDarkShadow(const Theorem& darkShadow) {
02015   const Expr& theShadow = darkShadow.getExpr();
02016   if(CHECK_PROOFS){
02017     CHECK_SOUND(isDarkShadow(theShadow),
02018     "ArithTheoremProducerOld::expandDarkShadow: not DARK_SHADOW: " +
02019     theShadow.toString());
02020   }
02021   Proof pf;
02022   if(withProof())
02023     pf = newPf("expand_dark_shadow", theShadow, darkShadow.getProof());
02024   return newTheorem(leExpr(theShadow[0], theShadow[1]), darkShadow.getAssumptionsRef(), pf);
02025 }
02026 
02027 
02028 // takes a grayShadow (c1==c2) and expands it into an equality
02029 Theorem ArithTheoremProducerOld::expandGrayShadow0(const Theorem& grayShadow) {
02030   const Expr& theShadow = grayShadow.getExpr();
02031   if(CHECK_PROOFS) {
02032     CHECK_SOUND(isGrayShadow(theShadow),
02033     "ArithTheoremProducerOld::expandGrayShadowConst0:"
02034     " not GRAY_SHADOW: " +
02035     theShadow.toString());
02036     CHECK_SOUND(theShadow[2] == theShadow[3],
02037     "ArithTheoremProducerOld::expandGrayShadow0: c1!=c2: " +
02038     theShadow.toString());
02039   }
02040   Proof pf;
02041   if(withProof()) pf = newPf("expand_gray_shadowconst0", theShadow,
02042            grayShadow.getProof());
02043   const Expr& v = theShadow[0];
02044   const Expr& e = theShadow[1];
02045   return newRWTheorem(v, e + theShadow[2], grayShadow.getAssumptionsRef(), pf);
02046 }
02047 
02048 
02049 // G ==> (G1 or G2) and (!G1 or !G2),
02050 // where G  = G(x, e, c1, c2),
02051 //       G1 = G(x,e,c1,c)
02052 //       G2 = G(x,e,c+1,c2),
02053 // and    c = floor((c1+c2)/2)
02054 Theorem ArithTheoremProducerOld::splitGrayShadow(const Theorem& gThm) {
02055   const Expr& theShadow = gThm.getExpr();
02056   if(CHECK_PROOFS) {
02057     CHECK_SOUND(isGrayShadow(theShadow),
02058     "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
02059     theShadow.toString());
02060   }
02061 
02062   const Rational& c1 = theShadow[2].getRational();
02063   const Rational& c2 = theShadow[3].getRational();
02064 
02065   if(CHECK_PROOFS) {
02066     CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
02067     "ArithTheoremProducerOld::expandGrayShadow: " +
02068     theShadow.toString());
02069   }
02070 
02071   const Expr& v = theShadow[0];
02072   const Expr& e = theShadow[1];
02073 
02074   Proof pf;
02075   Rational c(floor((c1+c2) / 2));
02076   Expr g1(grayShadow(v, e, c1, c));
02077   Expr g2(grayShadow(v, e, c+1, c2));
02078 
02079   if(withProof()){
02080     vector<Expr> exprs;
02081     exprs.push_back(theShadow);
02082     exprs.push_back(g1);
02083     exprs.push_back(g2);
02084     pf = newPf("split_gray_shadow", exprs, gThm.getProof());
02085   }
02086 
02087   return newTheorem((g1 || g2) && (!g1 || !g2), gThm.getAssumptionsRef(), pf);
02088 }
02089 
02090 
02091 Theorem ArithTheoremProducerOld::expandGrayShadow(const Theorem& gThm) {
02092   const Expr& theShadow = gThm.getExpr();
02093   if(CHECK_PROOFS) {
02094     CHECK_SOUND(isGrayShadow(theShadow),
02095     "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
02096     theShadow.toString());
02097   }
02098 
02099   const Rational& c1 = theShadow[2].getRational();
02100   const Rational& c2 = theShadow[3].getRational();
02101 
02102   if(CHECK_PROOFS) {
02103     CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
02104     "ArithTheoremProducerOld::expandGrayShadow: " +
02105     theShadow.toString());
02106   }
02107 
02108   const Expr& v = theShadow[0];
02109   const Expr& e = theShadow[1];
02110 
02111   Proof pf;
02112   if(withProof())
02113     pf = newPf("expand_gray_shadow", theShadow, gThm.getProof());
02114   Expr ineq1(leExpr(e+rat(c1), v));
02115   Expr ineq2(leExpr(v, e+rat(c2)));
02116   return newTheorem(ineq1 && ineq2, gThm.getAssumptionsRef(), pf);
02117 }
02118 
02119 
02120 // Expanding GRAY_SHADOW(a*x, c, b), where c is a constant
02121 Theorem
02122 ArithTheoremProducerOld::expandGrayShadowConst(const Theorem& gThm) {
02123   const Expr& theShadow = gThm.getExpr();
02124   const Expr& ax = theShadow[0];
02125   const Expr& cExpr = theShadow[1];
02126   const Expr& bExpr = theShadow[2];
02127 
02128   if(CHECK_PROOFS) {
02129     CHECK_SOUND(!isMult(ax) || ax[0].isRational(),
02130     "ArithTheoremProducerOld::expandGrayShadowConst: "
02131     "'a' in a*x is not a const: " +theShadow.toString());
02132   }
02133 
02134   Rational a = isMult(ax)? ax[0].getRational() : 1;
02135 
02136   if(CHECK_PROOFS) {
02137     CHECK_SOUND(isGrayShadow(theShadow),
02138     "ArithTheoremProducerOld::expandGrayShadowConst: "
02139     "not a GRAY_SHADOW: " +theShadow.toString());
02140     CHECK_SOUND(a.isInteger() && a >= 1,
02141     "ArithTheoremProducerOld::expandGrayShadowConst: "
02142     "'a' is not integer: " +theShadow.toString());
02143     CHECK_SOUND(cExpr.isRational(),
02144     "ArithTheoremProducerOld::expandGrayShadowConst: "
02145     "'c' is not rational" +theShadow.toString());
02146     CHECK_SOUND(bExpr.isRational() && bExpr.getRational().isInteger(),
02147     "ArithTheoremProducerOld::expandGrayShadowConst: b not integer: "
02148     +theShadow.toString());
02149   }
02150 
02151   const Rational& b = bExpr.getRational();
02152   const Rational& c = cExpr.getRational();
02153   Rational j = constRHSGrayShadow(c,b,a);
02154   // Compute sign(b)*j(c,b,a)
02155   Rational signB = (b>0)? 1 : -1;
02156   // |b| (absolute value of b)
02157   Rational bAbs = abs(b);
02158 
02159   const Assumptions& assump(gThm.getAssumptionsRef());
02160   Proof pf;
02161   Theorem conc;  // Conclusion of the rule
02162 
02163   if(bAbs < j) {
02164     if(withProof())
02165       pf = newPf("expand_gray_shadow_const_0", theShadow,
02166      gThm.getProof());
02167     conc = newTheorem(d_em->falseExpr(), assump, pf);
02168   } else if(bAbs < a+j) {
02169     if(withProof())
02170       pf = newPf("expand_gray_shadow_const_1", theShadow,
02171      gThm.getProof());
02172     conc = newRWTheorem(ax, rat(c+b-signB*j), assump, pf);
02173   } else {
02174     if(withProof())
02175       pf = newPf("expand_gray_shadow_const", theShadow,
02176      gThm.getProof());
02177     Expr newGrayShadow(Expr(GRAY_SHADOW, ax, cExpr, rat(b-signB*(a+j))));
02178     conc = newTheorem(ax.eqExpr(rat(c+b-signB*j)).orExpr(newGrayShadow),
02179           assump, pf);
02180   }
02181 
02182   return conc;
02183 }
02184 
02185 
02186 Theorem
02187 ArithTheoremProducerOld::grayShadowConst(const Theorem& gThm) {
02188   const Expr& g = gThm.getExpr();
02189   bool checkProofs(CHECK_PROOFS);
02190   if(checkProofs) {
02191     CHECK_SOUND(isGrayShadow(g), "ArithTheoremProducerOld::grayShadowConst("
02192     +g.toString()+")");
02193   }
02194 
02195   const Expr& ax = g[0];
02196   const Expr& e = g[1];
02197   const Rational& c1 = g[2].getRational();
02198   const Rational& c2 = g[3].getRational();
02199   Expr aExpr, x;
02200   d_theoryArith->separateMonomial(ax, aExpr, x);
02201 
02202   if(checkProofs) {
02203     CHECK_SOUND(e.isRational() && e.getRational().isInteger(),
02204     "ArithTheoremProducerOld::grayShadowConst("+g.toString()+")");
02205     CHECK_SOUND(aExpr.isRational(),
02206     "ArithTheoremProducerOld::grayShadowConst("+g.toString()+")");
02207   }
02208 
02209   const Rational& a = aExpr.getRational();
02210   const Rational& c = e.getRational();
02211 
02212   if(checkProofs) {
02213     CHECK_SOUND(a.isInteger() && a >= 2,
02214     "ArithTheoremProducerOld::grayShadowConst("+g.toString()+")");
02215   }
02216 
02217   Rational newC1 = ceil((c1+c)/a), newC2 = floor((c2+c)/a);
02218   Expr newG((newC1 > newC2)? d_em->falseExpr()
02219       : grayShadow(x, rat(0), newC1, newC2));
02220   Proof pf;
02221   if(withProof())
02222     pf = newPf("gray_shadow_const", g, newG, gThm.getProof());
02223   return newTheorem(newG, gThm.getAssumptionsRef(), pf);
02224 }
02225 
02226 
02227 Rational ArithTheoremProducerOld::constRHSGrayShadow(const Rational& c,
02228               const Rational& b,
02229               const Rational& a) {
02230   DebugAssert(c.isInteger() &&
02231         b.isInteger() &&
02232         a.isInteger() &&
02233         b != 0,
02234         "ArithTheoremProducerOld::constRHSGrayShadow: a, b, c must be ints");
02235   if (b > 0)
02236     return mod(c+b, a);
02237   else
02238     return mod(a-(c+b), a);
02239 }
02240 
02241 /*! Takes a Theorem(\\alpha < \\beta) and returns
02242  *  Theorem(\\alpha < \\beta <==> \\alpha <= \\beta -1)
02243  * where \\alpha and \\beta are integer expressions
02244  */
02245 Theorem ArithTheoremProducerOld::lessThanToLE(const Theorem& less,
02246              const Theorem& isIntLHS,
02247              const Theorem& isIntRHS,
02248              bool changeRight) {
02249   const Expr& ineq = less.getExpr();
02250   const Expr& isIntLHSexpr = isIntLHS.getExpr();
02251   const Expr& isIntRHSexpr = isIntRHS.getExpr();
02252 
02253   if(CHECK_PROOFS) {
02254     CHECK_SOUND(isLT(ineq),
02255     "ArithTheoremProducerOld::LTtoLE: ineq must be <");
02256     // Integrality check
02257     CHECK_SOUND(isIntPred(isIntLHSexpr) && isIntLHSexpr[0] == ineq[0],
02258     "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
02259     " ineq = "+ineq.toString()+"\n isIntLHS = "
02260     +isIntLHSexpr.toString());
02261     CHECK_SOUND(isIntPred(isIntRHSexpr) && isIntRHSexpr[0] == ineq[1],
02262     "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
02263     " ineq = "+ineq.toString()+"\n isIntRHS = "
02264     +isIntRHSexpr.toString());
02265   }
02266   vector<Theorem> thms;
02267   thms.push_back(less);
02268   thms.push_back(isIntLHS);
02269   thms.push_back(isIntRHS);
02270   Assumptions a(thms);
02271   Proof pf;
02272   Expr le = changeRight?
02273     leExpr(ineq[0], ineq[1] + rat(-1))
02274     : leExpr(ineq[0] + rat(1), ineq[1]);
02275   if(withProof()) {
02276     vector<Proof> pfs;
02277     pfs.push_back(less.getProof());
02278     pfs.push_back(isIntLHS.getProof());
02279     pfs.push_back(isIntRHS.getProof());
02280     pf = newPf(changeRight? "lessThan_To_LE_rhs" : "lessThan_To_LE_lhs",
02281          ineq,le, pfs);
02282   }
02283 
02284   return newRWTheorem(ineq, le, a, pf);
02285 }
02286 
02287 
02288 /*! \param eqn is an equation 0 = a.x or 0 = c + a.x
02289  *  \param isIntx is a proof of IS_INTEGER(x)
02290  *
02291  * \return the theorem 0 = c + a.x <==> x=-c/a if -c/a is int else
02292  *  return the theorem 0 = c + a.x <==> false.
02293  *
02294  * It also handles the special case of 0 = a.x <==> x = 0
02295  */
02296 Theorem
02297 ArithTheoremProducerOld::intVarEqnConst(const Expr& eqn,
02298              const Theorem& isIntx) {
02299   const Expr& left(eqn[0]);
02300   const Expr& right(eqn[1]);
02301   const Expr& isIntxexpr(isIntx.getExpr());
02302 
02303   if(CHECK_PROOFS) {
02304     CHECK_SOUND((isMult(right) && right[0].isRational())
02305                 || (right.arity() == 2 && isPlus(right)
02306                     && right[0].isRational()
02307                     && ((!isMult(right[1]) || right[1][0].isRational()))),
02308                 "ArithTheoremProducerOld::intVarEqnConst: "
02309     "rhs has a wrong format: " + right.toString());
02310     CHECK_SOUND(left.isRational() && 0 == left.getRational(),
02311                 "ArithTheoremProducerOld:intVarEqnConst:left is not a zero: " +
02312                 left.toString());
02313   }
02314   // Integrality constraint
02315   Expr x(right);
02316   Rational a(1), c(0);
02317   if(isMult(right)) {
02318     Expr aExpr;
02319     d_theoryArith->separateMonomial(right, aExpr, x);
02320     a = aExpr.getRational();
02321   } else { // right is a PLUS
02322     c = right[0].getRational();
02323     Expr aExpr;
02324     d_theoryArith->separateMonomial(right[1], aExpr, x);
02325     a = aExpr.getRational();
02326   }
02327   if(CHECK_PROOFS) {
02328     CHECK_SOUND(isIntPred(isIntxexpr) && isIntxexpr[0] == x,
02329                 "ArithTheoremProducerOld:intVarEqnConst: "
02330     "bad integrality constraint:\n right = " +
02331                 right.toString()+"\n isIntx = "+isIntxexpr.toString());
02332     CHECK_SOUND(a!=0, "ArithTheoremProducerOld:intVarEqnConst: eqn = "
02333     +eqn.toString());
02334   }
02335   const Assumptions& assump(isIntx.getAssumptionsRef());
02336 
02337   /*
02338       Proof pf;
02339   if(withProof())
02340     pf = newPf("int_const_eq", eqn, isIntx.getProof());
02341 
02342   // Solve for x:   x = r = -c/a
02343   Rational r(-c/a);
02344 
02345   if(r.isInteger()){
02346     return newRWTheorem(eqn, x.eqExpr(rat(r)), assump, pf);
02347   else
02348     return newRWTheorem(eqn, d_em->falseExpr(), assump, pf);
02349   */
02350 
02351   Proof pf;
02352   // Solve for x:   x = r = -c/a
02353   Rational r(-c/a);
02354 
02355   if(r.isInteger()){
02356     if(withProof())
02357       pf = newPf("int_const_eq", eqn, x.eqExpr(rat(r)),isIntx.getProof());
02358     return newRWTheorem(eqn, x.eqExpr(rat(r)), assump, pf);
02359   }
02360   else{
02361     if(withProof())
02362       pf = newPf("int_const_eq", eqn, d_em->falseExpr(),isIntx.getProof());
02363     return newRWTheorem(eqn, d_em->falseExpr(), assump, pf);
02364   }
02365 }
02366 
02367 
02368 Expr
02369 ArithTheoremProducerOld::create_t(const Expr& eqn) {
02370   const Expr& lhs = eqn[0];
02371   DebugAssert(isMult(lhs),
02372               CLASS_NAME "create_t : lhs must be a MULT"
02373               + lhs.toString());
02374   const Expr& x = lhs[1];
02375   Rational m = lhs[0].getRational()+1;
02376   DebugAssert(m > 0, "ArithTheoremProducerOld::create_t: m = "+m.toString());
02377   vector<Expr> kids;
02378   if(isPlus(eqn[1]))
02379     sumModM(kids, eqn[1], m, m);
02380   else
02381     kids.push_back(monomialModM(eqn[1], m, m));
02382 
02383   kids.push_back(multExpr(rat(1/m), x));
02384   return plusExpr(kids);
02385 }
02386 
02387 Expr
02388 ArithTheoremProducerOld::create_t2(const Expr& lhs, const Expr& rhs,
02389         const Expr& sigma) {
02390   Rational m = lhs[0].getRational()+1;
02391   DebugAssert(m > 0, "ArithTheoremProducerOld::create_t2: m = "+m.toString());
02392   vector<Expr> kids;
02393   if(isPlus(rhs))
02394     sumModM(kids, rhs, m, -1);
02395   else {
02396     kids.push_back(rat(0)); // For canonical form
02397     Expr monom = monomialModM(rhs, m, -1);
02398     if(!monom.isRational())
02399       kids.push_back(monom);
02400     else
02401       DebugAssert(monom.getRational() == 0, "");
02402   }
02403   kids.push_back(rat(m)*sigma);
02404   return plusExpr(kids);
02405 }
02406 
02407 Expr
02408 ArithTheoremProducerOld::create_t3(const Expr& lhs, const Expr& rhs,
02409         const Expr& sigma) {
02410   const Rational& a = lhs[0].getRational();
02411   Rational m = a+1;
02412   DebugAssert(m > 0, "ArithTheoremProducerOld::create_t3: m = "+m.toString());
02413   vector<Expr> kids;
02414   if(isPlus(rhs))
02415     sumMulF(kids, rhs, m, 1);
02416   else {
02417     kids.push_back(rat(0)); // For canonical form
02418     Expr monom = monomialMulF(rhs, m, 1);
02419     if(!monom.isRational())
02420       kids.push_back(monom);
02421     else
02422       DebugAssert(monom.getRational() == 0, "");
02423   }
02424   kids.push_back(rat(-a)*sigma);
02425   return plusExpr(kids);
02426 }
02427 
02428 Rational
02429 ArithTheoremProducerOld::modEq(const Rational& i, const Rational& m) {
02430   DebugAssert(m > 0, "ArithTheoremProducerOld::modEq: m = "+m.toString());
02431   Rational half(1,2);
02432   Rational res((i - m*(floor((i/m) + half))));
02433   TRACE("arith eq", "modEq("+i.toString()+", "+m.toString()+") = ", res, "");
02434   return res;
02435 }
02436 
02437 Rational
02438 ArithTheoremProducerOld::f(const Rational& i, const Rational& m) {
02439   DebugAssert(m > 0, "ArithTheoremProducerOld::f: m = "+m.toString());
02440   Rational half(1,2);
02441   return (floor(i/m + half)+modEq(i,m));
02442 }
02443 
02444 void
02445 ArithTheoremProducerOld::sumModM(vector<Expr>& summands, const Expr& sum,
02446                               const Rational& m, const Rational& divisor) {
02447   DebugAssert(divisor != 0, "ArithTheoremProducerOld::sumModM: divisor = "
02448         +divisor.toString());
02449   Expr::iterator i = sum.begin();
02450   DebugAssert(i != sum.end(), CLASS_NAME "::sumModM");
02451   Rational C = i->getRational();
02452   C = modEq(C,m)/divisor;
02453   summands.push_back(rat(C));
02454   i++;
02455   for(Expr::iterator iend=sum.end(); i!=iend; ++i) {
02456     Expr monom = monomialModM(*i, m, divisor);
02457     if(!monom.isRational())
02458       summands.push_back(monom);
02459     else
02460       DebugAssert(monom.getRational() == 0, "");
02461   }
02462 }
02463 
02464 Expr
02465 ArithTheoremProducerOld::monomialModM(const Expr& i,
02466                                    const Rational& m, const Rational& divisor)
02467 {
02468   DebugAssert(divisor != 0, "ArithTheoremProducerOld::monomialModM: divisor = "
02469         +divisor.toString());
02470   Expr res;
02471   if(isMult(i)) {
02472     Rational ai = i[0].getRational();
02473     ai = modEq(ai,m)/divisor;
02474     if(0 == ai) res = rat(0);
02475     else if(1 == ai && i.arity() == 2) res = i[1];
02476     else {
02477       vector<Expr> kids = i.getKids();
02478       kids[0] = rat(ai);
02479       res = multExpr(kids);
02480     }
02481   } else { // It's a single variable
02482     Rational ai = modEq(1,m)/divisor;
02483     if(1 == ai) res = i;
02484     else res = rat(ai)*i;
02485   }
02486   DebugAssert(!res.isNull(), "ArithTheoremProducerOld::monomialModM()");
02487   TRACE("arith eq", "monomialModM(i="+i.toString()+", m="+m.toString()
02488   +", div="+divisor.toString()+") = ", res, "");
02489   return res;
02490 }
02491 
02492 void
02493 ArithTheoremProducerOld::sumMulF(vector<Expr>& summands, const Expr& sum,
02494                               const Rational& m, const Rational& divisor) {
02495   DebugAssert(divisor != 0, "ArithTheoremProducerOld::sumMulF: divisor = "
02496         +divisor.toString());
02497   Expr::iterator i = sum.begin();
02498   DebugAssert(i != sum.end(), CLASS_NAME "::sumModM");
02499   Rational C = i->getRational();
02500   C = f(C,m)/divisor;
02501   summands.push_back(rat(C));
02502   i++;
02503   for(Expr::iterator iend=sum.end(); i!=iend; ++i) {
02504     Expr monom = monomialMulF(*i, m, divisor);
02505     if(!monom.isRational())
02506       summands.push_back(monom);
02507     else
02508       DebugAssert(monom.getRational() == 0, "");
02509   }
02510 }
02511 
02512 Expr
02513 ArithTheoremProducerOld::monomialMulF(const Expr& i,
02514                                    const Rational& m, const Rational& divisor)
02515 {
02516   DebugAssert(divisor != 0, "ArithTheoremProducerOld::monomialMulF: divisor = "
02517         +divisor.toString());
02518   Rational ai = isMult(i) ? (i)[0].getRational() : 1;
02519   Expr xi = isMult(i) ? (i)[1] : (i);
02520   ai = f(ai,m)/divisor;
02521   if(0 == ai) return rat(0);
02522   if(1 == ai) return xi;
02523   return multExpr(rat(ai), xi);
02524 }
02525 
02526 // This recursive function accepts a term, t, and a 'map' of
02527 // substitutions [x1/t1, x2/t2,...,xn/tn].  it returns a t' which is
02528 // basically t[x1/t1,x2/t2...xn/tn]
02529 Expr
02530 ArithTheoremProducerOld::substitute(const Expr& term, ExprMap<Expr>& eMap)
02531 {
02532   ExprMap<Expr>::iterator i, iend = eMap.end();
02533 
02534   i = eMap.find(term);
02535   if(iend != i)
02536     return (*i).second;
02537 
02538   if (isMult(term)) {
02539     //in this case term is of the form c.x
02540     i = eMap.find(term[1]);
02541     if(iend != i)
02542       return term[0]*(*i).second;
02543     else
02544       return term;
02545   }
02546 
02547   if(isPlus(term)) {
02548     vector<Expr> output;
02549     for(Expr::iterator j = term.begin(), jend = term.end(); j != jend; ++j)
02550       output.push_back(substitute(*j, eMap));
02551     return plusExpr(output);
02552   }
02553   return term;
02554 }
02555 
02556 bool ArithTheoremProducerOld::greaterthan(const Expr & l, const Expr & r)
02557 {
02558   //    DebugAssert(l != r, "");
02559   if (l==r) return false;
02560 
02561   switch(l.getKind()) {
02562   case RATIONAL_EXPR:
02563     DebugAssert(!r.isRational(), "");
02564     return true;
02565     break;
02566   case POW:
02567     switch (r.getKind()) {
02568     case RATIONAL_EXPR:
02569       // TODO:
02570       // alternately I could return (not greaterthan(r,l))
02571       return false;
02572       break;
02573     case POW:
02574       // x^n > y^n if x > y
02575       // x^n1 > x^n2 if n1 > n2
02576       return
02577         ((r[1] < l[1]) ||
02578          ((r[1]==l[1]) && (r[0].getRational() < l[0].getRational())));
02579       break;
02580 
02581     case MULT:
02582       DebugAssert(r.arity() > 1, "");
02583       DebugAssert((r.arity() > 2) || (r[1] != l), "");
02584       if (r[1] == l) return false;
02585       return greaterthan(l, r[1]);
02586       break;
02587     case PLUS:
02588       DebugAssert(false, "");
02589       return true;
02590       break;
02591     default:
02592       // leaf
02593       return ((r < l[1]) || ((r == l[1]) && l[0].getRational() > 1));
02594       break;
02595     }
02596     break;
02597   case MULT:
02598     DebugAssert(l.arity() > 1, "");
02599     switch (r.getKind()) {
02600     case RATIONAL_EXPR:
02601       return false;
02602       break;
02603     case POW:
02604       DebugAssert(l.arity() > 1, "");
02605       DebugAssert((l.arity() > 2) || (l[1] != r), "");
02606       // TODO:
02607       // alternately return (not greaterthan(r,l)
02608       return ((l[1] == r) || greaterthan(l[1], r));
02609       break;
02610     case MULT:
02611       {
02612 
02613         DebugAssert(r.arity() > 1, "");
02614         Expr::iterator i = l.begin();
02615         Expr::iterator j = r.begin();
02616         ++i;
02617         ++j;
02618         for (; i != l.end() && j != r.end(); ++i, ++j) {
02619           if (*i == *j)
02620             continue;
02621           return greaterthan(*i,*j);
02622         }
02623         DebugAssert(i != l.end() || j != r.end(), "");
02624         if (i == l.end()) {
02625           // r is bigger
02626           return false;
02627         }
02628         else
02629           {
02630             // l is bigger
02631             return true;
02632           }
02633       }
02634       break;
02635     case PLUS:
02636       DebugAssert(false, "");
02637       return true;
02638       break;
02639     default:
02640       // leaf
02641       DebugAssert((l.arity() > 2) || (l[1] != r), "");
02642       return ((l[1] == r) || greaterthan(l[1], r));
02643       break;
02644     }
02645     break;
02646   case PLUS:
02647     DebugAssert(false, "");
02648     return true;
02649     break;
02650   default:
02651     // leaf
02652     switch (r.getKind()) {
02653     case RATIONAL_EXPR:
02654       return false;
02655       break;
02656     case POW:
02657       return ((r[1] < l) || ((r[1] == l) && (r[0].getRational() < 1)));
02658       break;
02659     case MULT:
02660       DebugAssert(r.arity() > 1, "");
02661       DebugAssert((r.arity() > 2) || (r[1] != l), "");
02662       if (l == r[1]) return false;
02663       return greaterthan(l,r[1]);
02664       break;
02665     case PLUS:
02666       DebugAssert(false, "");
02667       return true;
02668       break;
02669     default:
02670       // leaf
02671       return (r < l);
02672       break;
02673     }
02674     break;
02675   }
02676 }
02677 
02678 
02679 /*! IS_INTEGER(x) |= EXISTS (y : INT) y = x
02680  * where x is not already known to be an integer.
02681  */
02682 Theorem ArithTheoremProducerOld::IsIntegerElim(const Theorem& isIntx)
02683 {
02684   Expr expr = isIntx.getExpr();
02685   if (CHECK_PROOFS) {
02686     CHECK_SOUND(expr.getKind() == IS_INTEGER,
02687                 "Expected IS_INTEGER predicate");
02688   }
02689   expr = expr[0];
02690   DebugAssert(!d_theoryArith->isInteger(expr), "Expected non-integer");
02691 
02692   Assumptions a(isIntx);
02693   Proof pf;
02694 
02695   if (withProof())
02696   {
02697     pf = newPf("isIntElim", isIntx.getProof());
02698   }
02699 
02700   Expr newVar = d_em->newBoundVarExpr(d_theoryArith->intType());
02701   Expr res = d_em->newClosureExpr(EXISTS, newVar, newVar.eqExpr(expr));
02702 
02703   return newTheorem(res, a, pf);
02704 }
02705 
02706 
02707 Theorem
02708 ArithTheoremProducerOld::eqElimIntRule(const Theorem& eqn, const Theorem& isIntx,
02709             const vector<Theorem>& isIntVars) {
02710   TRACE("arith eq", "eqElimIntRule(", eqn.getExpr(), ") {");
02711   Proof pf;
02712 
02713   if(CHECK_PROOFS)
02714     CHECK_SOUND(eqn.isRewrite(),
02715                 "ArithTheoremProducerOld::eqElimInt: input must be an equation" +
02716                 eqn.toString());
02717 
02718   const Expr& lhs = eqn.getLHS();
02719   const Expr& rhs = eqn.getRHS();
02720   Expr a, x;
02721   d_theoryArith->separateMonomial(lhs, a, x);
02722 
02723   if(CHECK_PROOFS) {
02724     // Checking LHS
02725     const Expr& isIntxe = isIntx.getExpr();
02726     CHECK_SOUND(isIntPred(isIntxe) && isIntxe[0] == x,
02727     "ArithTheoremProducerOld::eqElimInt\n eqn = "
02728     +eqn.getExpr().toString()
02729     +"\n isIntx = "+isIntxe.toString());
02730     CHECK_SOUND(isRational(a) && a.getRational().isInteger()
02731     && a.getRational() >= 2,
02732     "ArithTheoremProducerOld::eqElimInt:\n lhs = "+lhs.toString());
02733     // Checking RHS
02734     // It cannot be a division (we don't handle it)
02735     CHECK_SOUND(!isDivide(rhs),
02736     "ArithTheoremProducerOld::eqElimInt:\n rhs = "+rhs.toString());
02737     // If it's a single monomial, then it's the only "variable"
02738     if(!isPlus(rhs)) {
02739       Expr c, v;
02740       d_theoryArith->separateMonomial(rhs, c, v);
02741       CHECK_SOUND(isIntVars.size() == 1
02742       && isIntPred(isIntVars[0].getExpr())
02743       && isIntVars[0].getExpr()[0] == v
02744       && isRational(c) && c.getRational().isInteger(),
02745       "ArithTheoremProducerOld::eqElimInt:\n rhs = "+rhs.toString()
02746       +"isIntVars.size = "+int2string(isIntVars.size()));
02747     } else { // RHS is a plus
02748       CHECK_SOUND(isIntVars.size() + 1 == (size_t)rhs.arity(),
02749       "ArithTheoremProducerOld::eqElimInt: rhs = "+rhs.toString());
02750       // Check the free constant
02751       CHECK_SOUND(isRational(rhs[0]) && rhs[0].getRational().isInteger(),
02752       "ArithTheoremProducerOld::eqElimInt: rhs = "+rhs.toString());
02753       // Check the vars
02754       for(size_t i=0, iend=isIntVars.size(); i<iend; ++i) {
02755   Expr c, v;
02756   d_theoryArith->separateMonomial(rhs[i+1], c, v);
02757   const Expr& isInt(isIntVars[i].getExpr());
02758   CHECK_SOUND(isIntPred(isInt) && isInt[0] == v
02759         && isRational(c) && c.getRational().isInteger(),
02760         "ArithTheoremProducerOld::eqElimInt:\n rhs["+int2string(i+1)
02761         +"] = "+rhs[i+1].toString()
02762         +"\n isInt = "+isInt.toString());
02763       }
02764     }
02765   }
02766 
02767   // Creating a fresh bound variable
02768   static int varCount(0);
02769   Expr newVar = d_em->newBoundVarExpr("_int_var", int2string(varCount++));
02770   newVar.setType(intType());
02771   Expr t2 = create_t2(lhs, rhs, newVar);
02772   Expr t3 = create_t3(lhs, rhs, newVar);
02773   vector<Expr> vars;
02774   vars.push_back(newVar);
02775   Expr res = d_em->newClosureExpr(EXISTS, vars,
02776                                   x.eqExpr(t2) && rat(0).eqExpr(t3));
02777 
02778   vector<Theorem> thms(isIntVars);
02779   thms.push_back(isIntx);
02780   thms.push_back(eqn);
02781   Assumptions assump(thms);
02782 
02783   if(withProof()) {
02784     vector<Proof> pfs;
02785     pfs.push_back(eqn.getProof());
02786     pfs.push_back(isIntx.getProof());
02787     vector<Theorem>::const_iterator i=isIntVars.begin(), iend=isIntVars.end();
02788     for(; i!=iend; ++i)
02789       pfs.push_back(i->getProof());
02790     pf = newPf("eq_elim_int", eqn.getExpr(), res, pfs);
02791   }
02792 
02793   Theorem thm(newTheorem(res, assump, pf));
02794   TRACE("arith eq", "eqElimIntRule => ", thm.getExpr(), " }");
02795   return thm;
02796 }
02797 
02798 
02799 Theorem
02800 ArithTheoremProducerOld::isIntConst(const Expr& e) {
02801   Proof pf;
02802 
02803   if(CHECK_PROOFS) {
02804     CHECK_SOUND(isIntPred(e) && e[0].isRational(),
02805     "ArithTheoremProducerOld::isIntConst(e = "
02806     +e.toString()+")");
02807   }
02808   if(withProof())
02809     pf = newPf("is_int_const", e);
02810   bool isInt = e[0].getRational().isInteger();
02811   return newRWTheorem(e, isInt? d_em->trueExpr() : d_em->falseExpr(), Assumptions::emptyAssump(), pf);
02812 }
02813 
02814 
02815 Theorem
02816 ArithTheoremProducerOld::equalLeaves1(const Theorem& thm)
02817 {
02818   Proof pf;
02819   const Expr& e = thm.getRHS();
02820 
02821   if (CHECK_PROOFS) {
02822     CHECK_SOUND(e[1].getKind() == RATIONAL_EXPR &&
02823     e[1].getRational() == Rational(0) &&
02824     e[0].getKind() == PLUS &&
02825     e[0].arity() == 3 &&
02826     e[0][0].getKind() == RATIONAL_EXPR &&
02827     e[0][0].getRational() == Rational(0) &&
02828     e[0][1].getKind() == MULT &&
02829     e[0][1].arity() == 2 &&
02830     e[0][1][0].getKind() == RATIONAL_EXPR &&
02831     e[0][1][0].getRational() == Rational(-1),
02832     "equalLeaves1");
02833   }
02834   if (withProof())
02835   {
02836     vector<Proof> pfs;
02837     pfs.push_back(thm.getProof());
02838     pf = newPf("equalLeaves1", e, pfs);
02839   }
02840   return newRWTheorem(e, e[0][1][1].eqExpr(e[0][2]), thm.getAssumptionsRef(), pf);
02841 }
02842 
02843 
02844 Theorem
02845 ArithTheoremProducerOld::equalLeaves2(const Theorem& thm)
02846 {
02847   Proof pf;
02848   const Expr& e = thm.getRHS();
02849 
02850   if (CHECK_PROOFS) {
02851     CHECK_SOUND(e[0].getKind() == RATIONAL_EXPR &&
02852     e[0].getRational() == Rational(0) &&
02853     e[1].getKind() == PLUS &&
02854     e[1].arity() == 3 &&
02855     e[1][0].getKind() == RATIONAL_EXPR &&
02856     e[1][0].getRational() == Rational(0) &&
02857     e[1][1].getKind() == MULT &&
02858     e[1][1].arity() == 2 &&
02859     e[1][1][0].getKind() == RATIONAL_EXPR &&
02860     e[1][1][0].getRational() == Rational(-1),
02861     "equalLeaves2");
02862   }
02863   if (withProof())
02864   {
02865     vector<Proof> pfs;
02866     pfs.push_back(thm.getProof());
02867     pf = newPf("equalLeaves2", e, pfs);
02868   }
02869   return newRWTheorem(e, e[1][1][1].eqExpr(e[1][2]), thm.getAssumptionsRef(), pf);
02870 }
02871 
02872 
02873 Theorem
02874 ArithTheoremProducerOld::equalLeaves3(const Theorem& thm)
02875 {
02876   Proof pf;
02877   const Expr& e = thm.getRHS();
02878 
02879   if (CHECK_PROOFS) {
02880     CHECK_SOUND(e[1].getKind() == RATIONAL_EXPR &&
02881     e[1].getRational() == Rational(0) &&
02882     e[0].getKind() == PLUS &&
02883     e[0].arity() == 3 &&
02884     e[0][0].getKind() == RATIONAL_EXPR &&
02885     e[0][0].getRational() == Rational(0) &&
02886     e[0][2].getKind() == MULT &&
02887     e[0][2].arity() == 2 &&
02888     e[0][2][0].getKind() == RATIONAL_EXPR &&
02889     e[0][2][0].getRational() == Rational(-1),
02890     "equalLeaves3");
02891   }
02892   if (withProof())
02893   {
02894     vector<Proof> pfs;
02895     pfs.push_back(thm.getProof());
02896     pf = newPf("equalLeaves3", e, pfs);
02897   }
02898   return newRWTheorem(e, e[0][2][1].eqExpr(e[0][1]), thm.getAssumptionsRef(), pf);
02899 }
02900 
02901 
02902 Theorem
02903 ArithTheoremProducerOld::equalLeaves4(const Theorem& thm)
02904 {
02905   Proof pf;
02906   const Expr& e = thm.getRHS();
02907 
02908   if (CHECK_PROOFS) {
02909     CHECK_SOUND(e[0].getKind() == RATIONAL_EXPR &&
02910     e[0].getRational() == Rational(0) &&
02911     e[1].getKind() == PLUS &&
02912     e[1].arity() == 3 &&
02913     e[1][0].getKind() == RATIONAL_EXPR &&
02914     e[1][0].getRational() == Rational(0) &&
02915     e[1][2].getKind() == MULT &&
02916     e[1][2].arity() == 2 &&
02917     e[1][2][0].getKind() == RATIONAL_EXPR &&
02918     e[1][2][0].getRational() == Rational(-1),
02919     "equalLeaves4");
02920   }
02921   if (withProof())
02922   {
02923     vector<Proof> pfs;
02924     pfs.push_back(thm.getProof());
02925     pf = newPf("equalLeaves4", e, pfs);
02926   }
02927   return newRWTheorem(e, e[1][2][1].eqExpr(e[1][1]), thm.getAssumptionsRef(), pf);
02928 }
02929 
02930 Theorem
02931 ArithTheoremProducerOld::diseqToIneq(const Theorem& diseq) {
02932   Proof pf;
02933 
02934   const Expr& e = diseq.getExpr();
02935 
02936   if(CHECK_PROOFS) {
02937     CHECK_SOUND(e.isNot() && e[0].isEq(),
02938     "ArithTheoremProducerOld::diseqToIneq: expected disequality:\n"
02939     " e = "+e.toString());
02940   }
02941 
02942   const Expr& x = e[0][0];
02943   const Expr& y = e[0][1];
02944 
02945   if(withProof())
02946     pf = newPf(e, diseq.getProof());
02947   return newTheorem(ltExpr(x,y).orExpr(gtExpr(x,y)), diseq.getAssumptionsRef(), pf);
02948 }
02949 
02950 Theorem ArithTheoremProducerOld::dummyTheorem(const Expr& e) {
02951   Proof pf;
02952   return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
02953 }
02954 
02955 Theorem ArithTheoremProducerOld::oneElimination(const Expr& e) {
02956 
02957   // Check soundness
02958   if (CHECK_PROOFS)
02959     CHECK_SOUND(isMult(e) &&
02960           e.arity() == 2 &&
02961                 e[0].isRational() &&
02962                 e[0].getRational() == 1,
02963                 "oneElimination: input must be a multiplication by one" + e.toString());
02964 
02965   // The proof object that we will us
02966   Proof pf;
02967 
02968   // Setup the proof if needed
02969   if (withProof())
02970     pf = newPf("oneElimination", e);
02971 
02972   // Return the rewrite theorem that explains the phenomenon
02973   return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
02974 }
02975 
02976 Theorem ArithTheoremProducerOld::clashingBounds(const Theorem& lowerBound, const Theorem& upperBound) {
02977 
02978   // Get the expressions
02979   const Expr& lowerBoundExpr = lowerBound.getExpr();
02980   const Expr& upperBoundExpr = upperBound.getExpr();
02981 
02982   // Check soundness
02983   if (CHECK_PROOFS) {
02984     CHECK_SOUND(isLE(lowerBoundExpr) || isLT(lowerBoundExpr), "clashingBounds: lowerBound should be >= or > " + lowerBoundExpr.toString());
02985     CHECK_SOUND(isGE(upperBoundExpr) || isGT(upperBoundExpr), "clashingBounds: upperBound should be <= or < " + upperBoundExpr.toString());
02986     CHECK_SOUND(lowerBoundExpr[0].isRational(), "clashingBounds: lowerBound left side should be a rational " + lowerBoundExpr.toString());
02987     CHECK_SOUND(upperBoundExpr[0].isRational(), "clashingBounds: upperBound left side should be a rational " + upperBoundExpr.toString());
02988     CHECK_SOUND(lowerBoundExpr[1] == upperBoundExpr[1], "clashingBounds: bounds not on the same term " + lowerBoundExpr.toString() + ", " + upperBoundExpr.toString());
02989 
02990     // Get the bounds
02991     Rational lowerBoundR = lowerBoundExpr[0].getRational();
02992     Rational upperBoundR = upperBoundExpr[0].getRational();
02993 
02994     if (isLE(lowerBoundExpr) && isGE(upperBoundExpr)) {
02995       CHECK_SOUND(upperBoundR < lowerBoundR, "clashingBounds: bounds are satisfiable");
02996     } else {
02997       CHECK_SOUND(upperBoundR <= lowerBoundR, "clashingBounds: bounds are satisfiable");
02998     }
02999   }
03000 
03001   // The proof object that we will use
03002   Proof pf;
03003   // Setup the proof if needed
03004   if (withProof())
03005     pf = newPf("clashingBounds", lowerBoundExpr, upperBoundExpr);
03006 
03007   // Put the bounds expressions in the assumptions
03008   Assumptions assumptions;
03009   assumptions.add(lowerBound);
03010   assumptions.add(upperBound);
03011 
03012   // Return the theorem
03013   return newTheorem(d_em->falseExpr(), assumptions, pf);
03014 }
03015 
03016 Theorem ArithTheoremProducerOld::addInequalities(const Theorem& thm1, const Theorem& thm2) {
03017 
03018   // Get the expressions of the theorem
03019   const Expr& expr1 = thm1.getExpr();
03020   const Expr& expr2 = thm2.getExpr();
03021 
03022   // Check soundness
03023   if (CHECK_PROOFS) {
03024 
03025     CHECK_SOUND(isIneq(expr1), "addInequalities: expecting an inequality for thm1, got " + expr1.toString());
03026     CHECK_SOUND(isIneq(expr2), "addInequalities: expecting an inequality for thm2, got " + expr2.toString());
03027 
03028     if (isLE(expr1) || isLT(expr1))
03029       CHECK_SOUND(isLE(expr2) || isLT(expr2), "addInequalities: expr2 should be <(=) also " + expr2.toString());
03030     if (isGE(expr1) || isGT(expr1))
03031       CHECK_SOUND(isGE(expr2) || isGT(expr2), "addInequalities: expr2 should be >(=) also" + expr2.toString());
03032   }
03033 
03034   // Create the assumptions
03035   Assumptions a(thm1, thm2);
03036 
03037     // Get the kinds of the inequalitites
03038     int kind1  = expr1.getKind();
03039     int kind2  = expr2.getKind();
03040 
03041     // Set-up the resulting inequality
03042     int kind = (kind1 == kind2) ? kind1 : ((kind1 == LT) || (kind2 == LT))? LT : GT;
03043 
03044     // Create the proof object
03045     Proof pf;
03046     if(withProof()) {
03047       vector<Proof> pfs;
03048       pfs.push_back(thm1.getProof());
03049       pfs.push_back(thm2.getProof());
03050       pf = newPf("addInequalities", expr1, expr2, pfs);
03051     }
03052 
03053     // Create the new expressions
03054     Expr leftSide  = plusExpr(expr1[0], expr2[0]);
03055     Expr rightSide = plusExpr(expr1[1], expr2[1]);
03056 
03057     // Return the theorem
03058     return newTheorem(Expr(kind, leftSide, rightSide), a, pf);
03059 }
03060 
03061 //
03062 // 0 <= c1 + t
03063 // ==> 0 <= c2 + t
03064 // if c2 > c1
03065 Theorem ArithTheoremProducerOld::implyWeakerInequality(const Expr& expr1, const Expr& expr2) {
03066 
03067   // Check soundness
03068   if (CHECK_PROOFS) {
03069 
03070     // Both must be inequalitites
03071     CHECK_SOUND(isIneq(expr1), "implyWeakerInequality: expr1 should be an inequality" + expr1.toString());
03072     CHECK_SOUND(isIneq(expr2), "implyWeakerInequality: expr1 should be an inequality" + expr2.toString());
03073 
03074     // Left sides must be zero
03075     CHECK_SOUND(expr1[0].isRational() && expr1[0].getRational() == 0, "implyWeakerInequality: expr1 should have a rational on the left side" + expr1.toString());
03076     CHECK_SOUND(expr2[0].isRational() && expr2[0].getRational() == 0, "implyWeakerInequality: expr2 should have a rational on the left side" + expr2.toString());
03077 
03078     // Get the expr1 monomials and constant 0 <= c1 + t1
03079     Rational c1 = 0;
03080     vector<Expr> t1_children;
03081     if (isPlus(expr1[1])) {
03082       int start_i = 0;
03083       if (expr1[1][0].isRational()) {
03084         start_i = 1;
03085         c1 = expr1[1][0].getRational();
03086       }
03087       int end_i = expr1[1].arity();
03088         for(int i = start_i; i < end_i; i ++) {
03089           const Expr& term = expr1[1][i];
03090         t1_children.push_back(term);
03091       }
03092     } else
03093       t1_children.push_back(expr1[1]);
03094     Expr t1 = (t1_children.size() > 1 ? plusExpr(t1_children) : t1_children[0]);
03095 
03096     // Get the expr1 monomials and constant 0 <= c1 + t1
03097     Rational c2 = 0;
03098     vector<Expr> t2_children;
03099     if (isPlus(expr2[1])) {
03100       int start_i = 0;
03101       if (expr2[1][0].isRational()) {
03102         start_i = 1;
03103         c2 = expr2[1][0].getRational();
03104       }
03105       int end_i = expr2[1].arity();
03106         for(int i = start_i; i < end_i; i ++) {
03107           const Expr& term = expr2[1][i];
03108         t2_children.push_back(term);
03109       }
03110     } else
03111       t2_children.push_back(expr2[1]);
03112     Expr t2 = (t2_children.size() > 1 ? plusExpr(t2_children) : t2_children[0]);
03113 
03114     CHECK_SOUND(t2 == t1, "implyWeakerInequality: terms different " + t1.toString() + " vs " + t2.toString());
03115     CHECK_SOUND(c2 > c1 || (c2 == c1 && !(expr1.getKind() == LE && expr2.getKind() == LT)), "implyWeakerInequality: c2 is not bigger than c1" + expr1.toString() + " --> " + expr2.toString());
03116   }
03117     // Create the proof object
03118     Proof pf;
03119     if(withProof()) pf = newPf("implyWeakerInequality", expr1, expr2);
03120 
03121   // Return the theorem
03122   return newTheorem(expr1.impExpr(expr2), Assumptions::emptyAssump(), pf);
03123 }
03124 
03125 // Takes
03126 // Expr1: 0 <= c1 + t1
03127 // Expr2: 0 <= c2 + t2    (t2 is -t1)
03128 // if c1 + c2 < 0 then Expr1 => !Expr2
03129 //
03130 
03131 Theorem ArithTheoremProducerOld::implyNegatedInequality(const Expr& expr1, const Expr& expr2) {
03132 
03133   // Check soundness
03134   // Check soundness
03135   if (CHECK_PROOFS) {
03136 
03137     // Both must be inequalitites
03138     CHECK_SOUND(isIneq(expr1), "implyNegatedInequality: expr1 should be an inequality" + expr1.toString());
03139     CHECK_SOUND(isIneq(expr2), "implyNegatedInequality: expr1 should be an inequality" + expr2.toString());
03140 
03141     // Left sides must be zero
03142     CHECK_SOUND(expr1[0].isRational() && expr1[0].getRational() == 0, "implyNegatedInequality: expr1 should have a rational on the left side" + expr1.toString());
03143     CHECK_SOUND(expr2[0].isRational() && expr2[0].getRational() == 0, "implyNegatedInequality: expr2 should have a rational on the left side" + expr2.toString());
03144 
03145     // Get the expr1 monomials and constant 0 <= c1 + t1
03146     Rational c1 = 0;
03147     vector<Expr> t1_children;
03148     if (isPlus(expr1[1])) {
03149       int start_i = 0;
03150       if (expr1[1][0].isRational()) {
03151         start_i = 1;
03152         c1 = expr1[1][0].getRational();
03153       }
03154       int end_i = expr1[1].arity();
03155         for(int i = start_i; i < end_i; i ++) {
03156           const Expr& term = expr1[1][i];
03157         t1_children.push_back(term);
03158       }
03159     } else
03160       t1_children.push_back(expr1[1]);
03161     Expr t1 = (t1_children.size() > 1 ? plusExpr(t1_children) : t1_children[0]);
03162 
03163     // Get the expr1 monomials and constant 0 <= c1 + t1
03164     Rational c2 = 0;
03165     vector<Expr> t2_children;
03166     if (isPlus(expr2[1])) {
03167       int start_i = 0;
03168       if (expr2[1][0].isRational()) {
03169         start_i = 1;
03170         c2 = expr2[1][0].getRational();
03171       }
03172       int end_i = expr2[1].arity();
03173         for(int i = start_i; i < end_i; i ++) {
03174           const Expr& term = expr2[1][i];
03175         t2_children.push_back(term);
03176       }
03177     } else
03178       t2_children.push_back(expr2[1]);
03179     Expr t2 = (t2_children.size() > 1 ? plusExpr(t2_children) : t2_children[0]);
03180 
03181     // t1 shoud be -t2
03182     if (isPlus(t1) && isPlus(t2)) {
03183       CHECK_SOUND(t1.arity() == t2.arity(), "implyNegatedInequality: t1 should be -t2 : " + t1.toString() + " vs " + t2.toString());
03184       for (int i = 0; i < t1.arity(); i++) {
03185         Expr term_t1 = t1[i];
03186         Expr term_t2 = t2[i];
03187         Rational t1_c = (isMult(term_t1) ? term_t1[0].getRational() : 1);
03188         term_t1 = (isMult(term_t1) ? term_t1[1] : term_t1);
03189         Rational t2_c = (isMult(term_t2) ? term_t2[0].getRational() : 1);
03190         term_t2 = (isMult(term_t2) ? term_t2[1] : term_t2);
03191         CHECK_SOUND(t1_c == - t2_c, "implyNegatedInequality: t1 should be -t2 : " + t1.toString() + " vs " + t2.toString());
03192         CHECK_SOUND(term_t1 == term_t2, "implyNegatedInequality: t1 should be -t2 : " + t1.toString() + " vs " + t2.toString());
03193       }
03194     } else {
03195       Rational t1_c = (isMult(t1) ? t1[0].getRational() : 1);
03196       Expr term_t1  = (isMult(t1) ? t1[1] : t1);
03197       Rational t2_c = (isMult(t2) ? t2[0].getRational() : 1);
03198       Expr term_t2  = (isMult(t2) ? t2[1] : t2);
03199       CHECK_SOUND(t1_c == - t2_c, "implyNegatedInequality: t1 should be -t2 : " + t1.toString() + " vs " + t2.toString());
03200       CHECK_SOUND(term_t1 == term_t2, "implyNegatedInequality: t1 should be -t2 : " + t1.toString() + " vs " + t2.toString());
03201     }
03202 
03203     int kind1 = expr1.getKind();
03204     int kind2 = expr2.getKind();
03205     bool bothStrict = kind1 == LT && kind2 == LT;
03206     CHECK_SOUND(c1 + c2 < 0 || (c1 + c2 == 0 && bothStrict), "implyNegatedInequality: sum of constants not negative!");
03207   }
03208 
03209   // The proof object that we will use
03210   Proof pf;
03211   if (withProof()) pf = newPf("implyNegatedInequality", expr1, expr2, expr2.negate());
03212 
03213   // Return the theorem
03214   return newTheorem(expr1.impExpr(expr2.negate()), Assumptions::emptyAssump(), pf);
03215 }
03216 
03217 Theorem ArithTheoremProducerOld::trustedRewrite(const Expr& expr1, const Expr& expr2) {
03218 
03219   // The proof object that we will us
03220   Proof pf;
03221 
03222   // Setup the proof if needed
03223   if (withProof()) pf = newPf("trustedRewrite", expr1, expr2);
03224 
03225   // Return the rewrite theorem that explains the phenomenon
03226   return newRWTheorem(expr1, expr2, Assumptions::emptyAssump(), pf);
03227 
03228 }
03229 
03230 Theorem ArithTheoremProducerOld::integerSplit(const Expr& intVar, const Rational& intPoint) {
03231 
03232   // Check soundness
03233   if (CHECK_PROOFS) {
03234     CHECK_SOUND(intPoint.isInteger(), "integerSplit: we can only split on integer points, given" + intPoint.toString());
03235   }
03236 
03237   // Create the expression
03238   const Expr& split = Expr(IS_INTEGER, intVar).impExpr(leExpr(intVar, rat(intPoint)).orExpr(geExpr(intVar, rat(intPoint + 1))));
03239 
03240   // The proof object that we will use
03241   Proof pf;
03242   if (withProof()) pf = newPf("integerSplit", intVar, rat(intPoint));
03243 
03244   // Return the theorem
03245   return newTheorem(split, Assumptions::emptyAssump(), pf);
03246 }
03247 
03248 //
03249 // Changed from the new arithmetic, takes
03250 // 0 op c + t, where t is an integer expression but c is a rational
03251 // or 0 op x, where x is a leaf
03252 //
03253 Theorem ArithTheoremProducerOld::rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr) {
03254 
03255   // Check soundness
03256   if (CHECK_PROOFS) {
03257     // Right side of the constraint should correspond to the proved integer expression
03258     CHECK_SOUND(isIneq(constr), "rafineStrictInteger: expected a constraint got : " + constr.toString());
03259     CHECK_SOUND(constr[0].isRational() && constr[0].getRational() == 0, "rafineStrictInteger: left hand side must be 0");
03260     CHECK_SOUND(d_theoryArith->isLeaf(constr[1]) || constr[1][0].isRational(), "rafineStrictInteger: right side of the constraint must be a leaf or a sum, with the first one a rational");
03261 
03262     // We have to check that the non-constant children of inequality correspond to the integrality theorem's children
03263     Expr intSum = isIntConstrThm.getExpr()[0];
03264     Expr ineqSum = constr[1];
03265     if (isPlus(intSum)) {
03266       int i, j;
03267       for (i = 0, j = 1; i < intSum.arity() && j < ineqSum.arity(); i ++, j ++)
03268         if (!(intSum[i] == ineqSum[j])) break;
03269       CHECK_SOUND(i == intSum.arity() && j == ineqSum.arity(), "rafineStrictInteger: proof of intger doesn't correspond to the constarint right side");
03270     } else
03271       CHECK_SOUND(intSum == ineqSum || intSum == ineqSum[1], "rafineStrictInteger: proof of intger doesn't correspond to the constarint right side:" + intSum.getString() + " vs " + ineqSum[1].getString());
03272   }
03273 
03274   // Get the contraint bound
03275   Rational c = (isPlus(constr[1]) ? constr[1][0].getRational() : 0);
03276 
03277   // Get the kind of the constraint
03278   int kind = constr.getKind();
03279 
03280   // If the bound is strict, make it non-strict
03281   switch (kind) {
03282     case LT:
03283       kind = LE;
03284       if (c.isInteger()) c --;            // 0 < 3 + x   --> 0 <= 2 + x
03285       else c = floor(c);                  // 0 < 3.4 + x --> 0 <= 3 + x
03286       break;
03287     case LE:
03288       kind = LE;
03289       if (!c.isInteger()) c = floor(c);   // 0 <= 3.5 + x --> 0 <= 3 + x
03290       break;
03291     case GT:
03292       kind = GE;
03293       if (c.isInteger()) c ++;            // 0 > 3 + x   -->  0 >= 4 + x
03294       else c = ceil(c);                   // 0 > 3.4 + x -->  0 >= 4 + x
03295       break;
03296     case GE:
03297       kind = GE;
03298       if (!c.isInteger()) c = ceil(c);   // 0 >= 3.4 + x --> 4 >= x
03299       break;
03300   }
03301 
03302   // The new constraint
03303   vector<Expr> newChildren;
03304   if (isPlus(constr[1])) {
03305     for (int i = 0; i < constr[1].arity(); i ++)
03306       if (constr[1][i].isRational()) newChildren.push_back(rat(c));
03307       else newChildren.push_back(constr[1][i]);
03308   } else {
03309     if (c != 0) newChildren.push_back(rat(c));
03310     newChildren.push_back(constr[1]);
03311   }
03312   Expr newSum = newChildren.size() > 1 ? plusExpr(newChildren) : newChildren[0];
03313   Expr newConstr(kind, rat(0), newSum);
03314 
03315   // Pick up the assumptions from the integer proof
03316   const Assumptions& assump(isIntConstrThm.getAssumptionsRef());
03317 
03318     // Construct the proof object if necessary
03319     Proof pf;
03320   if (withProof())
03321     pf = newPf("rafineStrictInteger", constr,newConstr, isIntConstrThm.getProof());
03322 
03323   // Return the rewrite theorem that explains the phenomenon
03324   return newRWTheorem(constr, newConstr, assump, pf);
03325 }
03326 
03327 
03328 // Given:
03329 // 0 = c + t
03330 // where t is integer and c is not
03331 // deduce bot
03332 Theorem ArithTheoremProducerOld::intEqualityRationalConstant(const Theorem& isIntConstrThm, const Expr& constr) {
03333 
03334   // Check soundness
03335   if (CHECK_PROOFS) {
03336     // Right side of the constraint should correspond to the proved integer expression
03337     CHECK_SOUND(constr.getKind() == EQ, "intEqualityRationalConstant: expected a constraint got : " + constr.toString());
03338     bool sum_on_rhs = (constr[0].isRational() && constr[0].getRational() == 0);
03339     bool sum_on_lhs = (constr[1].isRational() && constr[1].getRational() == 0);
03340     CHECK_SOUND((sum_on_rhs && !sum_on_lhs) ||(!sum_on_rhs && sum_on_lhs),
03341             "intEqualityRationalConstant: left or right hand side must be 0");
03342     CHECK_SOUND((sum_on_rhs && constr[1][0].isRational() && !constr[1][0].getRational().isInteger()) ||
03343             (sum_on_lhs && constr[0][0].isRational() && !constr[0][0].getRational().isInteger()),
03344                 "intEqualityRationalConstant: left or right side of the constraint must be a sum, with the first one a rational (non integer)");
03345 
03346     // We have to check that the non-constant children of inequality correspond to the integrality theorem's children
03347     Expr intSum = isIntConstrThm.getExpr()[0];
03348     Expr eqSum = (sum_on_lhs ? constr[0] : constr[1]);
03349     if (isPlus(intSum)) {
03350       int i, j;
03351       for (i = 0, j = 1; i < intSum.arity() && j < eqSum.arity(); i ++, j ++)
03352         if (!(intSum[i] == eqSum[j])) break;
03353       CHECK_SOUND(i == intSum.arity() && j == eqSum.arity(), "intEqualityRationalConstant: proof of intger doesn't correspond to the constarint right side");
03354     } else
03355       CHECK_SOUND(intSum == eqSum[1], "intEqualityRationalConstant: proof of intger doesn't correspond to the constarint right side:" + intSum.getString() + " vs " + eqSum[1].getString());
03356   }
03357 
03358   const Assumptions& assump(isIntConstrThm.getAssumptionsRef());
03359 
03360     // Construct the proof object if necessary
03361     Proof pf;
03362   if (withProof())
03363     pf = newPf("intEqualityRationalConstant", constr, isIntConstrThm.getProof());
03364 
03365   // Return the rewrite theorem that explains the phenomenon
03366   return newRWTheorem(constr, d_em->falseExpr(), assump, pf);
03367 }
03368 
03369 Theorem ArithTheoremProducerOld::cycleConflict(const vector<Theorem>& inequalitites) {
03370   Proof pf;
03371   if(withProof()) {
03372       vector<Expr> es;
03373       vector<Proof> pfs;
03374       for(unsigned i = 0; i < inequalitites.size(); i++) {
03375         es.push_back(inequalitites[i].getExpr());
03376         pfs.push_back(inequalitites[i].getProof());
03377       }
03378       pf = newPf("cycleConflict", es, pfs);
03379     }
03380 
03381   Assumptions a;
03382   for(unsigned i = 0; i < inequalitites.size(); i ++)
03383     a.add(inequalitites[i]);
03384 
03385   return newTheorem(d_em->falseExpr(), a, pf);
03386 }
03387 
03388 Theorem ArithTheoremProducerOld::implyEqualities(const std::vector<Theorem>& inequalities) {
03389   Assumptions a;
03390   vector<Expr> conjuncts;
03391   for(unsigned i = 0; i < inequalities.size(); i ++) {
03392     a.add(inequalities[i]);
03393     Expr inequality = inequalities[i].getExpr();
03394     Expr equality = inequality[0].eqExpr(inequality[1]);
03395     conjuncts.push_back(equality);
03396   }
03397 
03398   Proof pf;
03399   if(withProof()) {
03400       vector<Expr> es;
03401       vector<Proof> pfs;
03402       for(unsigned i = 0; i < inequalities.size(); i++) {
03403         es.push_back(inequalities[i].getExpr());
03404         pfs.push_back(inequalities[i].getProof());
03405       }
03406       pf = newPf("implyEqualities", Expr(RAW_LIST,conjuncts),Expr(RAW_LIST,es), pfs);
03407   }
03408 
03409   return newTheorem(andExpr(conjuncts), a, pf);
03410 }
03411 
03412 /*! Takes a Theorem(\\alpha < \\beta) and returns
03413  *  Theorem(\\alpha < \\beta <==> \\alpha <= \\beta -1)
03414  * where \\alpha and \\beta are integer expressions
03415  */
03416 Theorem ArithTheoremProducerOld::lessThanToLERewrite(const Expr& ineq,
03417              const Theorem& isIntLHS,
03418              const Theorem& isIntRHS,
03419              bool changeRight) {
03420 
03421   const Expr& isIntLHSexpr = isIntLHS.getExpr();
03422   const Expr& isIntRHSexpr = isIntRHS.getExpr();
03423 
03424   if(CHECK_PROOFS) {
03425     CHECK_SOUND(isLT(ineq), "ArithTheoremProducerOld::LTtoLE: ineq must be <");
03426     // Integrality check
03427     CHECK_SOUND(isIntPred(isIntLHSexpr) && isIntLHSexpr[0] == ineq[0],
03428     "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
03429     " ineq = "+ineq.toString()+"\n isIntLHS = "
03430     +isIntLHSexpr.toString());
03431     CHECK_SOUND(isIntPred(isIntRHSexpr) && isIntRHSexpr[0] == ineq[1],
03432     "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
03433     " ineq = "+ineq.toString()+"\n isIntRHS = "
03434     +isIntRHSexpr.toString());
03435   }
03436 
03437   vector<Theorem> thms;
03438   thms.push_back(isIntLHS);
03439   thms.push_back(isIntRHS);
03440   Assumptions a(thms);
03441   Proof pf;
03442   Expr le = changeRight? leExpr(ineq[0], ineq[1] + rat(-1)) : leExpr(ineq[0] + rat(1), ineq[1]);
03443   if(withProof()) {
03444     vector<Proof> pfs;
03445     pfs.push_back(isIntLHS.getProof());
03446     pfs.push_back(isIntRHS.getProof());
03447     pf = newPf(changeRight? "lessThan_To_LE_rhs_rwr" : "lessThan_To_LE_lhs_rwr", ineq, le, pfs);
03448   }
03449 
03450   return newRWTheorem(ineq, le, a, pf);
03451 }
03452 
03453 // G ==> (G1 or G2) and (!G1 or !G2),
03454 // where G  = G(x, e, c1, c2),
03455 //       V x = e + i, for i in c1 .. c2
03456 Theorem ArithTheoremProducerOld::splitGrayShadowSmall(const Theorem& gThm) {
03457   const Expr& theShadow = gThm.getExpr();
03458   if(CHECK_PROOFS) {
03459     CHECK_SOUND(isGrayShadow(theShadow),
03460     "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
03461     theShadow.toString());
03462   }
03463 
03464   const Rational& c1 = theShadow[2].getRational();
03465   const Rational& c2 = theShadow[3].getRational();
03466 
03467   if(CHECK_PROOFS) {
03468     CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
03469     "ArithTheoremProducerOld::expandGrayShadow: " +
03470     theShadow.toString());
03471   }
03472 
03473   const Expr& v = theShadow[0];
03474   const Expr& e = theShadow[1];
03475 
03476   vector<Expr> disjuncts;
03477   for (int i = c1.getInt(); i <= c2.getInt(); i ++) {
03478     Expr disjunct = v.eqExpr(e + rat(i));
03479     disjuncts.push_back(disjunct);
03480   }
03481   Expr bigOr = orExpr(disjuncts);
03482 
03483   Proof pf;
03484     if(withProof()){
03485     vector<Expr> exprs;
03486     exprs.push_back(theShadow);
03487     exprs.push_back(bigOr);
03488     pf = newPf("split_gray_shadow", exprs, gThm.getProof());
03489   }
03490 
03491   return newTheorem(bigOr, gThm.getAssumptionsRef(), pf);
03492 }
03493 
03494 Theorem ArithTheoremProducerOld::implyWeakerInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) {
03495   Proof pf;
03496 
03497   if(withProof()) {
03498       vector<Expr> es;
03499       vector<Proof> pfs;
03500       for(unsigned i = 0; i < antecedentThms.size(); i++) {
03501         es.push_back(antecedentThms[i].getExpr());
03502         pfs.push_back(antecedentThms[i].getProof());
03503       }
03504       pf = newPf("implyWeakerInequalityDiffLogic", implied, Expr(RAW_LIST,es), pfs);
03505   }
03506 
03507   Assumptions a;
03508   for(unsigned i = 0; i < antecedentThms.size(); i ++) {
03509     a.add(antecedentThms[i]);
03510   }
03511 
03512   return newTheorem(implied, a, pf);
03513 
03514 }
03515 
03516 Theorem ArithTheoremProducerOld::implyNegatedInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) {
03517   Proof pf;
03518 
03519   if(withProof()) {
03520       vector<Expr> es;
03521       vector<Proof> pfs;
03522       for(unsigned i = 0; i < antecedentThms.size(); i++) {
03523         es.push_back(antecedentThms[i].getExpr());
03524         pfs.push_back(antecedentThms[i].getProof());
03525       }
03526       pf = newPf("implyNegatedInequalityDiffLogic",implied.notExpr(), Expr(RAW_LIST, es), pfs);
03527   }
03528 
03529   Assumptions a;
03530   for(unsigned i = 0; i < antecedentThms.size(); i ++) {
03531     a.add(antecedentThms[i]);
03532   }
03533 
03534   return newTheorem(implied.notExpr(), a, pf);
03535 
03536 }
03537 
03538 
03539 Theorem ArithTheoremProducerOld::expandGrayShadowRewrite(const Expr& theShadow) {
03540 
03541   if(CHECK_PROOFS) {
03542     CHECK_SOUND(isGrayShadow(theShadow),
03543     "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
03544     theShadow.toString());
03545   }
03546 
03547   const Rational& c1 = theShadow[2].getRational();
03548   const Rational& c2 = theShadow[3].getRational();
03549 
03550   if(CHECK_PROOFS) {
03551     CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
03552     "ArithTheoremProducerOld::expandGrayShadow: " +
03553     theShadow.toString());
03554   }
03555 
03556   const Expr& v = theShadow[0];
03557   const Expr& e = theShadow[1];
03558 
03559   Proof pf;
03560   if(withProof())
03561     pf = newPf("expand_gray_shadow", theShadow);
03562   Expr ineq1(leExpr(e+rat(c1), v));
03563   Expr ineq2(leExpr(v, e+rat(c2)));
03564   return newRWTheorem(theShadow, ineq1 && ineq2, Assumptions::emptyAssump(), pf);
03565 }
03566 
03567 Theorem ArithTheoremProducerOld::compactNonLinearTerm(const Expr& nonLinear) {
03568 
03569   // The set of common leaves
03570   multiset<Expr> commonLeaves;
03571   bool first = true;
03572 
03573   // Go through the terms and intersect the leaf sets
03574   for (int i = 0; i < nonLinear.arity(); i ++) {
03575     if (!nonLinear[i].isRational()) {
03576       // Get the current monomial
03577       Expr monomial = nonLinear[i];
03578 
03579       // A set to keep the variables
03580       multiset<Expr> currentLeaves;
03581 
03582       // Get the set of leaves in this term
03583       if (isMult(monomial)) {
03584         for (int j = 0; j < monomial.arity(); j ++)
03585           if (!monomial[j].isRational()) {
03586             if (isPow(monomial[j])) {
03587               for (int p = 0; p < monomial[j][0].getRational().getInt(); p ++)
03588                 currentLeaves.insert(monomial[j][1]);
03589             } else
03590               currentLeaves.insert(monomial[j]);
03591           }
03592       } else if (isPow(monomial)) {
03593         for (int p = 0; p < monomial[0].getRational().getInt(); p ++)
03594           currentLeaves.insert(monomial[1]);
03595       } else
03596         currentLeaves.insert(monomial);
03597 
03598       // And intersect them
03599       if (first) {
03600         commonLeaves.swap(currentLeaves);
03601         first = false;
03602       } else {
03603         multiset<Expr> intersectLeaves;
03604         set_intersection(currentLeaves.begin(), currentLeaves.end(),
03605                   commonLeaves.begin(), commonLeaves.end(),
03606                   insert_iterator< multiset<Expr> >
03607                           (intersectLeaves, intersectLeaves.begin()));
03608         intersectLeaves.swap(commonLeaves);
03609       }
03610     }
03611   }
03612 
03613   Expr result;
03614   if (commonLeaves.size() > 0) {
03615 
03616     // The constant to add in the beginnings
03617     Expr constant = rat(0);
03618 
03619     // The sum of of the rest when we pullout the common factors
03620     vector<Expr> sumChildren;
03621 
03622     // Go through them again and construct the sum of the rest
03623     for (int i = 0; i < nonLinear.arity(); i ++) {
03624       if (!nonLinear[i].isRational()) {
03625         // Get the current monomial
03626         Expr monomial = nonLinear[i];
03627 
03628         // A set to keep the variables
03629         multiset<Expr> currentChildren;
03630 
03631         // Get the set of childrent of this multiplication
03632         if (isMult(monomial)) {
03633           for (int j = 0; j < monomial.arity(); j ++)
03634             if (isPow(monomial[j])) {
03635               for (int p = 0; p < monomial[j][0].getRational().getInt(); p ++)
03636                 currentChildren.insert(monomial[j][1]);
03637             } else
03638               currentChildren.insert(monomial[j]);
03639         } else if (isPow(monomial)) {
03640           for (int p = 0; p < monomial[0].getRational().getInt(); p ++)
03641             currentChildren.insert(monomial[1]);
03642         } else
03643           currentChildren.insert(monomial);
03644 
03645         // Take the difference and construct a multiplication
03646         multiset<Expr> diffChildren;
03647         set_difference(currentChildren.begin(), currentChildren.end(),
03648                  commonLeaves.begin(), commonLeaves.end(),
03649                  insert_iterator< multiset<Expr> >
03650                             (diffChildren, diffChildren.begin()));
03651 
03652         // Go create another sumChildren element
03653         if (diffChildren.size() == 1) {
03654           sumChildren.push_back(*diffChildren.begin());
03655         } else if (diffChildren.size() == 0) {
03656           sumChildren.push_back(rat(1));
03657         } else {
03658           multiset<Expr>::iterator it     = diffChildren.begin();
03659           multiset<Expr>::iterator it_end = diffChildren.end();
03660           vector<Expr> multChildren;
03661           while (it != it_end) {
03662             multChildren.push_back(*it);
03663             it ++;
03664           }
03665           sumChildren.push_back(multExpr(multChildren));
03666         }
03667       } else
03668         constant = nonLinear[i];
03669     }
03670 
03671     // The children of the final multiplication
03672     vector<Expr> multChildren;
03673     multChildren.push_back(plusExpr(sumChildren));
03674     multiset<Expr>::iterator it = commonLeaves.begin();
03675     multiset<Expr>::iterator it_end = commonLeaves.end();
03676     for (; it != it_end; it ++)
03677       multChildren.push_back(*it);
03678     result = plusExpr(constant, multExpr(multChildren));
03679   } else {
03680     // We have no common leaves to take out
03681     result = nonLinear;
03682   }
03683 
03684     Proof pf;
03685   if(withProof())
03686     pf = newPf("compactNonlinear", nonLinear, result);
03687 
03688   return newRWTheorem(nonLinear, result, Assumptions::emptyAssump(), pf);
03689 }
03690 
03691 //
03692 // -c <= x1*x2*...*xn
03693 // if c = 0 then "only even number of x_i's can be negative" or one of them is zero
03694 //               x1 = 0 or x2 = 0 or ... or xn = 0
03695 //               or (x1
03696 // else "only only even number of x_i's can be negative" and none of them is zero"
03697 Theorem ArithTheoremProducerOld::nonLinearIneqSignSplit(const Theorem& ineqThm) {
03698 
03699   // Get the inequality
03700   Expr ineq = ineqThm.getExpr();
03701   Expr rhs = ineq[1];
03702 
03703   // Get the constant
03704   Rational c = (isMult(rhs) ? 0 : rhs[0].getRational());
03705   if(CHECK_PROOFS) {
03706       CHECK_SOUND(c <= 0, "ArithTheoremProducerOld::nonLinearIneqSignSplit: " + ineq.toString());
03707       CHECK_SOUND(isMult(rhs) || (isPlus(rhs) && rhs.arity() == 2), "ArithTheoremProducerOld::nonLinearIneqSignSplit: " + ineq.toString());
03708   }
03709 
03710   Expr signXor = d_em->trueExpr();
03711   Expr mult = (isMult(rhs) ? rhs : rhs[1]);
03712   for (int i = 0; i < mult.arity(); i ++) {
03713     Expr term = mult[i];
03714     if (isPow(term) && term[0].getRational() < 0)
03715       term = Expr(POW, -term[0], term[1]);
03716     signXor = Expr(XOR, signXor, ltExpr(term, rat(0)));
03717   }
03718 
03719   if (c == 0 && ineq.getKind() == LE) {
03720     Expr zeroOr = d_em->falseExpr();
03721     for (int i = 0; i < mult.arity(); i ++) {
03722       Expr term = mult[i];
03723       zeroOr = zeroOr.orExpr(term.eqExpr(rat(0)));
03724     }
03725     signXor = zeroOr.orExpr(signXor);
03726   }
03727 
03728   Proof pf;
03729   if(withProof()) {
03730     vector<Expr> exprs;
03731       exprs.push_back(ineq);
03732       exprs.push_back(signXor);
03733       pf = newPf("nonLinearIneqSignSplit", exprs, ineqThm.getProof());
03734   }
03735 
03736   Assumptions assumptions;
03737   assumptions.add(ineqThm);
03738 
03739   return newTheorem(signXor, assumptions, pf);
03740 }
03741 
03742 Theorem ArithTheoremProducerOld::implyDiffLogicBothBounds(const Expr& x,
03743     std::vector<Theorem>& c1_le_x, Rational c1,
03744       std::vector<Theorem>& x_le_c2, Rational c2)
03745 {
03746   Proof pf;
03747 
03748   if(withProof()) {
03749       vector<Expr> es;
03750       vector<Proof> pfs;
03751       for(unsigned i = 0; i < c1_le_x.size(); i++) {
03752         es.push_back(c1_le_x[i].getExpr());
03753         pfs.push_back(c1_le_x[i].getProof());
03754       }
03755       for(unsigned i = 0; i < x_le_c2.size(); i++) {
03756         es.push_back(x_le_c2[i].getExpr());
03757         pfs.push_back(x_le_c2[i].getProof());
03758       }
03759       pf = newPf("implyDiffLogicBothBounds", es, pfs);
03760   }
03761 
03762   Assumptions a;
03763   for(unsigned i = 0; i < x_le_c2.size(); i ++) {
03764     a.add(c1_le_x[i]);
03765   }
03766   for(unsigned i = 0; i < x_le_c2.size(); i ++) {
03767     a.add(c1_le_x[i]);
03768   }
03769 
03770   Expr implied = grayShadow(x, rat(0), c1, c2);
03771 
03772   return newTheorem(implied, a, pf);
03773 }
03774 
03775 Theorem ArithTheoremProducerOld::addInequalities(const vector<Theorem>& thms) {
03776 
03777   // Check soundness
03778   if (CHECK_PROOFS) {
03779     for (unsigned i = 0; i < thms.size(); i ++) {
03780       Expr expr = thms[i].getExpr();
03781       CHECK_SOUND(isIneq(expr), "addInequalities: expecting an inequality for, got " + expr.toString());
03782       CHECK_SOUND(isLE(expr) || isLT(expr), "addInequalities: expr should be <(=) " + expr.toString());
03783     }
03784   }
03785 
03786   // Create the assumptions
03787   Assumptions a;
03788   for (unsigned i = 0; i < thms.size(); i ++)
03789     a.add(thms[i]);
03790 
03791     // Get the kinds of the inequalitites
03792   int kind = LE;
03793   for (unsigned i = 0; i < thms.size(); i ++)
03794     if (thms[i].getExpr().getKind() == LT) kind = LT;
03795 
03796     // Create the proof object
03797     Proof pf;
03798     if(withProof()) {
03799       vector<Proof> pfs;
03800       vector<Expr> exps;
03801       for (unsigned i = 0; i < thms.size(); i ++) {
03802           pfs.push_back(thms[i].getProof());
03803           exps.push_back(thms[i].getExpr());
03804       }
03805       pf = newPf("addInequalities", exps, pfs);
03806     }
03807 
03808     // Create the new expressions
03809     vector<Expr> summandsLeft;
03810     vector<Expr> summandsRight;
03811     for (unsigned i = 0; i < thms.size(); i ++)  {
03812       summandsLeft.push_back(thms[i].getExpr()[0]);
03813       summandsRight.push_back(thms[i].getExpr()[1]);
03814     }
03815     Expr leftSide  = plusExpr(summandsLeft);
03816     Expr rightSide = plusExpr(summandsRight);
03817 
03818     // Return the theorem
03819     return newTheorem(Expr(kind, leftSide, rightSide), a, pf);
03820 }
03821 
03822 // x^1 <-> x
03823 Theorem ArithTheoremProducerOld::powerOfOne(const Expr& e) {
03824 
03825   if(CHECK_PROOFS) {
03826     CHECK_SOUND(isPow(e), "ArithTheoremProducerOld::powerOfOne: not a power expression" + e.toString());
03827     CHECK_SOUND(e[0].isRational() && e[0].getRational() == 1, "ArithTheoremProducerOld::powerOfOne: not a power of 1" + e.toString());
03828   }
03829 
03830   Proof pf;
03831   if(withProof())
03832     pf = newPf("power_of_one", e);
03833 
03834   return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
03835 }
03836 
03837 
03838 void ArithTheoremProducerOld::getLeaves(const Expr& e, set<Rational>& s, ExprHashMap<bool>& cache)
03839 {
03840   if (e.isRational()) {
03841     s.insert(e.getRational());
03842     return;
03843   }
03844 
03845   if (e.isAtomic() && d_theoryArith->isLeaf(e)) {
03846     return;
03847   }
03848 
03849   ExprHashMap<bool>::iterator it = cache.find(e);
03850   if (it != cache.end()) return;
03851 
03852   cache[e] = true;
03853 
03854   DebugAssert(e.arity() > 0, "Expected non-zero arity");
03855   int k = 0;
03856 
03857   if (e.isITE()) {
03858     k = 1;
03859   }
03860 
03861   for (; k < e.arity(); ++k) {
03862     getLeaves(e[k], s, cache);
03863   }
03864 }
03865 
03866 
03867 Theorem ArithTheoremProducerOld::rewriteLeavesConst(const Expr& e)
03868 {
03869   DebugAssert(e.isPropAtom() && d_theoryArith->leavesAreNumConst(e),
03870               "invariant violated");
03871   DebugAssert(e.getKind() == EQ || e.getKind() == LT || e.getKind() == LE || e.getKind() == GT || e.getKind() == GE,
03872               "Unexpected kind");
03873   set<Rational> lhs, rhs;
03874   ExprHashMap<bool> cache;
03875   getLeaves(e[0], lhs, cache);
03876 
03877   cache.clear();
03878   getLeaves(e[1], rhs, cache);
03879 
03880   Expr res;
03881   switch (e.getKind()) {
03882     case EQ: {
03883       set<Rational> common;
03884       set_intersection(lhs.begin(), lhs.end(), rhs.begin(), rhs.end(),
03885                        inserter(common, common.begin()));
03886       if (common.empty()) {
03887         res = d_em->falseExpr();
03888       }
03889       break;
03890     }
03891     case LT: {
03892       set<Rational>::iterator it;
03893       it = lhs.end();
03894       --it;
03895       if ((*it) < (*(rhs.begin()))) {
03896         res = d_em->trueExpr();
03897       } else {
03898         it = rhs.end();
03899         --it;
03900         if ((*it) <= (*(lhs.begin()))) {
03901           res = d_em->falseExpr();
03902         }
03903       }
03904       break;
03905     }
03906     case LE: {
03907       set<Rational>::iterator it;
03908       it = lhs.end();
03909       --it;
03910       if ((*it) <= (*(rhs.begin()))) {
03911         res = d_em->trueExpr();
03912       }
03913       else {
03914         it = rhs.end();
03915         --it;
03916         if ((*it) < (*(lhs.begin()))) {
03917           res = d_em->falseExpr();
03918           break;
03919         }
03920       }
03921       break;
03922     }
03923     case GT: {
03924       set<Rational>::iterator it;
03925       it = lhs.end();
03926       --it;
03927       if ((*it) > (*(rhs.begin()))) {
03928         res = d_em->trueExpr();
03929       } else {
03930         it = rhs.end();
03931         --it;
03932         if ((*it) >= (*(lhs.begin()))) {
03933           res = d_em->falseExpr();
03934         }
03935       }
03936       break;
03937     }
03938     case GE: {
03939       set<Rational>::iterator it;
03940       it = lhs.end();
03941       --it;
03942       if ((*it) >= (*(rhs.begin()))) {
03943         res = d_em->trueExpr();
03944       }
03945       else {
03946         it = rhs.end();
03947         --it;
03948         if ((*it) > (*(lhs.begin()))) {
03949           res = d_em->falseExpr();
03950           break;
03951         }
03952       }
03953       break;
03954     }
03955     default:
03956       break;
03957     }
03958   if (res.isNull()) return d_theoryArith->reflexivityRule(e);
03959   else {
03960     Proof pf;
03961     if(withProof())
03962       pf = newPf("rewrite_leaves_const", e);
03963     return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
03964   }
03965 }