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

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