theory_arith3.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theory_arith3.cpp
00004  *
00005  * Author: Clark Barrett, Vijay Ganesh.
00006  *
00007  * Created: Fri Jan 17 18:39:18 2003
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 
00021 
00022 #include "theory_arith3.h"
00023 #include "arith_proof_rules.h"
00024 //#include "arith_expr.h"
00025 #include "arith_exception.h"
00026 #include "typecheck_exception.h"
00027 #include "eval_exception.h"
00028 #include "parser_exception.h"
00029 #include "smtlib_exception.h"
00030 #include "theory_core.h"
00031 #include "command_line_flags.h"
00032 
00033 
00034 using namespace std;
00035 using namespace CVC3;
00036 
00037 
00038 ///////////////////////////////////////////////////////////////////////////////
00039 // TheoryArith3::FreeConst Methods                                            //
00040 ///////////////////////////////////////////////////////////////////////////////
00041 
00042 namespace CVC3 {
00043 
00044 ostream& operator<<(ostream& os, const TheoryArith3::FreeConst& fc) {
00045   os << "FreeConst(r=" << fc.getConst() << ", "
00046      << (fc.strict()? "strict" : "non-strict") << ")";
00047   return os;
00048 }
00049 
00050 ///////////////////////////////////////////////////////////////////////////////
00051 // TheoryArith3::Ineq Methods                                                 //
00052 ///////////////////////////////////////////////////////////////////////////////
00053 
00054 ostream& operator<<(ostream& os, const TheoryArith3::Ineq& ineq) {
00055   os << "Ineq(" << ineq.ineq().getExpr() << ", isolated on "
00056      << (ineq.varOnRHS()? "RHS" : "LHS") << ", const = "
00057      << ineq.getConst() << ")";
00058   return os;
00059 }
00060 } // End of namespace CVC3
00061 
00062 
00063 ///////////////////////////////////////////////////////////////////////////////
00064 // TheoryArith3 Private Methods                                               //
00065 ///////////////////////////////////////////////////////////////////////////////
00066 
00067 
00068 Theorem TheoryArith3::isIntegerThm(const Expr& e) {
00069   // Quick check
00070   if(isReal(e.getType())) return Theorem();
00071   // Try harder
00072   return isIntegerDerive(Expr(IS_INTEGER, e), typePred(e));
00073 }
00074 
00075 
00076 Theorem TheoryArith3::isIntegerDerive(const Expr& isIntE, const Theorem& thm) {
00077   const Expr& e = thm.getExpr();
00078   // We found it!
00079   if(e == isIntE) return thm;
00080 
00081   Theorem res;
00082   // If the theorem is an AND, look inside each child
00083   if(e.isAnd()) {
00084     int i, iend=e.arity();
00085     for(i=0; i<iend; ++i) {
00086       res = isIntegerDerive(isIntE, getCommonRules()->andElim(thm, i));
00087       if(!res.isNull()) return res;
00088     }
00089   }
00090   return res;
00091 }
00092 
00093 const Rational& TheoryArith3::freeConstIneq(const Expr& ineq, bool varOnRHS) {
00094   DebugAssert(isIneq(ineq), "TheoryArith3::freeConstIneq("+ineq.toString()+")");
00095   const Expr& e = varOnRHS? ineq[0] : ineq[1];
00096 
00097   switch(e.getKind()) {
00098   case PLUS:
00099     return e[0].getRational();
00100   case RATIONAL_EXPR:
00101     return e.getRational();
00102   default: { // MULT, DIV, or Variable
00103     static Rational zero(0);
00104     return zero;
00105   }
00106   }
00107 }
00108 
00109 
00110 const TheoryArith3::FreeConst&
00111 TheoryArith3::updateSubsumptionDB(const Expr& ineq, bool varOnRHS,
00112          bool& subsumed) {
00113   TRACE("arith ineq", "TheoryArith3::updateSubsumptionDB(", ineq,
00114   ", var isolated on "+string(varOnRHS? "RHS" : "LHS")+")");
00115   DebugAssert(isLT(ineq) || isLE(ineq), "TheoryArith3::updateSubsumptionDB("
00116         +ineq.toString()+")");
00117   // Indexing expression: same as ineq only without the free const
00118   Expr index;
00119   const Expr& t = varOnRHS? ineq[0] : ineq[1];
00120   bool strict(isLT(ineq));
00121   Rational c(0);
00122   if(isPlus(t)) {
00123     DebugAssert(t.arity() >= 2, "TheoryArith3::updateSubsumptionDB("
00124     +ineq.toString()+")");
00125     c = t[0].getRational(); // Extract the free const in ineq
00126     Expr newT;
00127     if(t.arity() == 2) {
00128       newT = t[1];
00129     } else {
00130       vector<Expr> kids;
00131       Expr::iterator i=t.begin(), iend=t.end();
00132       for(++i; i!=iend; ++i) kids.push_back(*i);
00133       DebugAssert(kids.size() > 0, "kids.size = "+int2string(kids.size())
00134       +", ineq = "+ineq.toString());
00135       newT = plusExpr(kids);
00136     }
00137     if(varOnRHS)
00138       index = leExpr(newT, ineq[1]);
00139     else
00140       index = leExpr(ineq[0], newT);
00141   } else if(isRational(t)) {
00142     c = t.getRational();
00143     if(varOnRHS)
00144       index = leExpr(rat(0), ineq[1]);
00145     else
00146       index = leExpr(ineq[0], rat(0));
00147   } else if(isLT(ineq))
00148     index = leExpr(ineq[0], ineq[1]);
00149   else
00150     index = ineq;
00151   // Now update the database, check for subsumption, and extract the constant
00152   CDMap<Expr, FreeConst>::iterator i=d_freeConstDB.find(index),
00153     iend=d_freeConstDB.end();
00154   if(i == iend) {
00155     subsumed = false;
00156     // Create a new entry
00157     CDOmap<Expr,FreeConst>& obj = d_freeConstDB[index];
00158     obj = FreeConst(c,strict);
00159     TRACE("arith ineq", "freeConstDB["+index.toString()+"] := ", obj, "");
00160     return obj.get();
00161   } else {
00162     CDOmap<Expr,FreeConst>& obj = d_freeConstDB[index];
00163     const FreeConst& fc = obj.get();
00164     if(varOnRHS) {
00165       subsumed = (c < fc.getConst() ||
00166       (c == fc.getConst() && (!strict || fc.strict())));
00167     } else {
00168       subsumed = (c > fc.getConst() ||
00169       (c == fc.getConst() && (strict || !fc.strict())));
00170     }
00171     if(!subsumed) {
00172       obj = FreeConst(c,strict);
00173       TRACE("arith ineq", "freeConstDB["+index.toString()+"] := ", obj, "");
00174     }
00175     return obj.get();
00176   }
00177 }
00178 
00179 
00180 bool TheoryArith3::kidsCanonical(const Expr& e) {
00181   if(isLeaf(e)) return true;
00182   bool res(true);
00183   for(int i=0; res && i<e.arity(); ++i) {
00184     Expr simp(canon(e[i]).getRHS());
00185     res = (e[i] == simp);
00186     IF_DEBUG(if(!res) debugger.getOS() << "\ne[" << i << "] = " << e[i]
00187        << "\nsimplified = " << simp << endl;)
00188   }
00189   return res;
00190 }
00191 
00192 
00193 ///////////////////////////////////////////////////////////////////////////////
00194 //                                                                           //
00195 // Function: TheoryArith3::canon                                              //
00196 // Author: Clark Barrett, Vijay Ganesh.                                      //
00197 // Created: Sat Feb  8 14:46:32 2003                                         //
00198 // Description: Compute a canonical form for expression e and return a       //
00199 //              theorem that e is equal to its canonical form.               //
00200 // Note that canonical form for arith expressions is one of the following:   //
00201 // 1. rational constant                                                      //
00202 // 2. arithmetic leaf                                                        //
00203 //    (i.e. variable or term from some other theory)                         //
00204 // 3. (MULT rat leaf)                                                        //
00205 //    where rat is a non-zero rational constant, leaf is an arithmetic leaf  //
00206 // 4. (PLUS const term_0 term_1 ... term_n)                                  //
00207 //    where each term_i is either a leaf or (MULT rat leaf)                  //
00208 //    and each leaf in term_i must be strictly greater than the leaf in      //
00209 //    term_{i+1}.                                                            //
00210 //                                                                           //
00211 ///////////////////////////////////////////////////////////////////////////////
00212 Theorem TheoryArith3::canon(const Expr& e)
00213 {
00214   TRACE("arith canon","canon(",e,") {");
00215   DebugAssert(kidsCanonical(e), "TheoryArith3::canon("+e.toString()+")");
00216   Theorem result;
00217   switch (e.getKind()) {
00218     case UMINUS: {
00219       Theorem thm = d_rules->uMinusToMult(e[0]);
00220       Expr e2 = thm.getRHS();
00221       result = transitivityRule(thm, canon(e2));
00222     }
00223       break;
00224     case PLUS: /* {
00225       Theorem plusThm, plusThm1;
00226       plusThm = d_rules->canonFlattenSum(e);
00227       plusThm1 = d_rules->canonComboLikeTerms(plusThm.getRHS());
00228       result = transitivityRule(plusThm,plusThm1);
00229     }
00230              */
00231       result = d_rules->canonPlus(e);
00232       break;
00233     case MINUS: {
00234       DebugAssert(e.arity() == 2,"");
00235       Theorem minus_eq_sum = d_rules->minusToPlus(e[0], e[1]);
00236       // this produces e0 + (-1)*e1; we have to canonize it in 2 steps
00237       Expr sum(minus_eq_sum.getRHS());
00238       Theorem thm(canon(sum[1]));
00239       if(thm.getLHS() == thm.getRHS())
00240         result = canonThm(minus_eq_sum);
00241       // The sum changed; do the work
00242       else {
00243         vector<unsigned> changed;
00244         vector<Theorem> thms;
00245         changed.push_back(1);
00246         thms.push_back(thm);
00247         Theorem sum_eq_canon = canonThm(substitutivityRule(sum, changed, thms));
00248         result = transitivityRule(minus_eq_sum, sum_eq_canon);
00249       }
00250       break;
00251     }
00252 
00253     case MULT:
00254       result = d_rules->canonMult(e);
00255       break;
00256   /*
00257     case MULT: {
00258       Theorem thmMult, thmMult1;
00259       Expr exprMult;
00260       Expr e0 = e[0];
00261       Expr e1 = e[1];
00262       if(e0.isRational()) {
00263         if(rat(0) == e0)
00264         result = d_rules->canonMultZero(e1);
00265         else if (rat(1) == e0)
00266         result = d_rules->canonMultOne(e1);
00267         else
00268         switch(e1.getKind()) {
00269         case RATIONAL_EXPR :
00270           result = d_rules->canonMultConstConst(e0,e1);
00271           break;
00272         case MULT:
00273           DebugAssert(e1[0].isRational(),
00274                       "theory_arith::canon:\n  "
00275                       "canon:MULT:MULT child is not canonical: "
00276                       + e1[0].toString());
00277 
00278           thmMult = d_rules->canonMultConstTerm(e0,e1[0],e1[1]);
00279           result = transitivityRule(thmMult,canon(thmMult.getRHS()));
00280           break;
00281         case PLUS:{
00282           Theorem thmPlus, thmPlus1;
00283           Expr ePlus;
00284           std::vector<Theorem> thmPlusVector;
00285           thmPlus = d_rules->canonMultConstSum(e0,e1);
00286           ePlus = thmPlus.getRHS();
00287           Expr::iterator i = ePlus.begin();
00288           for(;i != ePlus.end();++i)
00289             thmPlusVector.push_back(canon(*i));
00290           thmPlus1 = substitutivityRule(PLUS, thmPlusVector);
00291           result = transitivityRule(thmPlus, thmPlus1);
00292           break;
00293         }
00294         default:
00295           result = reflexivityRule(e);
00296           break;
00297         }
00298       }
00299       else {
00300           if(e1.isRational()){
00301 
00302           // canonMultTermConst just reverses the order of the const and the
00303             // term.  Then canon is called again.
00304         Theorem t1 = d_rules->canonMultTermConst(e1,e0);
00305         result = transitivityRule(t1,canon(t1.getRHS()));
00306         }
00307         else
00308 
00309               // This is where the assertion for non-linear multiplication is
00310               // produced.
00311             result =  d_rules->canonMultTerm1Term2(e0,e1);
00312       }
00313       break;
00314       }
00315 
00316   */
00317     case DIVIDE:{
00318   /*
00319       case DIVIDE:{
00320         if (e[1].isRational()) {
00321           if (e[1].getRational() == 0)
00322             throw ArithException("Divide by 0 error in "+e.toString());
00323           Theorem thm = d_rules->canonDivideVar(e[0], e[1]);
00324           Expr e2 = thm.getRHS();
00325           result =  transitivityRule(thm, canon(e2));
00326         }
00327         else
00328         {
00329         // TODO: to be handled
00330         throw ArithException("Divide by a non-const not handled in "+e.toString());
00331         }
00332       break;
00333       }
00334   */
00335 
00336       // Division by 0 is OK (total extension, protected by TCCs)
00337 //       if (e[1].isRational() && e[1].getRational() == 0)
00338 //         throw ArithException("Divide by 0 error in "+e.toString());
00339       if (e[1].getKind() == PLUS)
00340         throw ArithException("Divide by a PLUS expression not handled in"+e.toString());
00341       result = d_rules->canonDivide(e);
00342       break;
00343     }
00344   case POW:
00345     if(e[1].isRational())
00346       result = d_rules->canonPowConst(e);
00347     else
00348       result = reflexivityRule(e);
00349     break;
00350   default:
00351       result = reflexivityRule(e);
00352       break;
00353     }
00354   TRACE("arith canon","canon => ",result," }");
00355   return result;
00356 }
00357 
00358 
00359 Theorem
00360 TheoryArith3::canonSimplify(const Expr& e) {
00361   TRACE("arith", "canonSimplify(", e, ") {");
00362   DebugAssert(kidsCanonical(e),
00363         "TheoryArith3::canonSimplify("+e.toString()+")");
00364   DebugAssert(leavesAreSimp(e), "Expected leaves to be simplified");
00365   Expr tmp(e);
00366   Theorem thm = canon(e);
00367   if(thm.getRHS().hasFind())
00368     thm = transitivityRule(thm, find(thm.getRHS()));
00369   // We shouldn't rely on simplification in this function anymore
00370   DebugAssert(thm.getRHS() == simplifyExpr(thm.getRHS()),
00371         "canonSimplify("+e.toString()+")\n"
00372         +"canon(e) = "+thm.getRHS().toString()
00373         +"\nsimplify(canon(e)) = "+simplifyExpr(thm.getRHS()).toString());
00374 //   if(tmp != thm.getRHS())
00375 //     thm = transitivityRule(thm, simplifyThm(thm.getRHS()));
00376 //   while(tmp != thm.getRHS()) {
00377 //     tmp = thm.getRHS();
00378 //     thm = canon(thm);
00379 //     if(tmp != thm.getRHS())
00380 //       thm = transitivityRule(thm, simplifyThm(thm.getRHS()));
00381 //   }
00382   TRACE("arith", "canonSimplify =>", thm, " }");
00383   return thm;
00384 }
00385 
00386 /*! accepts a theorem, canonizes it, applies iffMP and substituvity to
00387  *  derive the canonized thm
00388  */
00389 Theorem
00390 TheoryArith3::canonPred(const Theorem& thm) {
00391   vector<Theorem> thms;
00392   DebugAssert(thm.getExpr().arity() == 2,
00393               "TheoryArith3::canonPred: bad theorem: "+thm.toString());
00394   Expr e(thm.getExpr());
00395   thms.push_back(canonSimplify(e[0]));
00396   thms.push_back(canonSimplify(e[1]));
00397   return iffMP(thm, substitutivityRule(e.getOp(), thms));
00398 }
00399 
00400 /*! accepts an equivalence theorem, canonizes it, applies iffMP and
00401  *  substituvity to derive the canonized thm
00402  */
00403 Theorem
00404 TheoryArith3::canonPredEquiv(const Theorem& thm) {
00405   vector<Theorem> thms;
00406   DebugAssert(thm.getRHS().arity() == 2,
00407               "TheoryArith3::canonPredEquiv: bad theorem: "+thm.toString());
00408   Expr e(thm.getRHS());
00409   thms.push_back(canonSimplify(e[0]));
00410   thms.push_back(canonSimplify(e[1]));
00411   return transitivityRule(thm, substitutivityRule(e.getOp(), thms));
00412 }
00413 
00414 /*! accepts an equivalence theorem whose RHS is a conjunction,
00415  *  canonizes it, applies iffMP and substituvity to derive the
00416  *  canonized thm
00417  */
00418 Theorem
00419 TheoryArith3::canonConjunctionEquiv(const Theorem& thm) {
00420   vector<Theorem> thms;
00421   return thm;
00422 }
00423 
00424 /*! Pseudo-code for doSolve. (Input is an equation) (output is a Theorem)
00425  *  -# translate e to the form e' = 0
00426  *  -# if (e'.isRational()) then {if e' != 0 return false else true}
00427  *  -# a for loop checks if all the variables are integers.
00428  *      - if not isolate a suitable real variable and call processRealEq().
00429  *      - if all variables are integers then isolate suitable variable
00430  *         and call processIntEq().
00431  */
00432 Theorem TheoryArith3::doSolve(const Theorem& thm)
00433 {
00434   const Expr& e = thm.getExpr();
00435   TRACE("arith eq","doSolve(",e,") {");
00436   DebugAssert(thm.isRewrite(), "thm = "+thm.toString());
00437   Theorem eqnThm;
00438   vector<Theorem> thms;
00439   // Move LHS to the RHS, if necessary
00440   if(e[0].isRational() && e[0].getRational() == 0)
00441     eqnThm = thm;
00442   else {
00443     eqnThm = iffMP(thm, d_rules->rightMinusLeft(e));
00444     eqnThm = canonPred(eqnThm);
00445   }
00446   // eqnThm is of the form 0 = e'
00447   // 'right' is of the form e'
00448   Expr right = eqnThm.getRHS();
00449   // Check for trivial equation
00450   if (right.isRational()) {
00451     Theorem result = iffMP(eqnThm, d_rules->constPredicate(eqnThm.getExpr()));
00452     TRACE("arith eq","doSolve => ",result," }");
00453     return result;
00454   }
00455 
00456   //normalize
00457   eqnThm = iffMP(eqnThm, normalize(eqnThm.getExpr()));
00458   right = eqnThm.getRHS();
00459 
00460   //eqn is of the form 0 = e' and is normalized where 'right' denotes e'
00461   //FIXME: change processRealEq to accept equations as well instead of theorems
00462 
00463   try {
00464     if (isMult(right)) {
00465       DebugAssert(right.arity() > 1, "Expected arity > 1");
00466       if (right[0].isRational()) {
00467         Rational r = right[0].getRational();
00468         if (r == 0) return getCommonRules()->trueTheorem();
00469         else if (r == 1) {
00470           enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr())));
00471           return getCommonRules()->trueTheorem();
00472         }
00473         Theorem res = iffMP(eqnThm,
00474                             d_rules->multEqn(eqnThm.getLHS(),
00475                                              right, rat(1/r)));
00476         res = canonPred(res);
00477         return doSolve(res);
00478       }
00479       else {
00480         enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr())));
00481         return getCommonRules()->trueTheorem();
00482       }
00483     }
00484     else if (isPow(right)) {
00485       DebugAssert(right.arity() == 2, "Expected arity 2");
00486       if (right[0].isRational()) {
00487         return doSolve(iffMP(eqnThm, d_rules->powEqZero(eqnThm.getExpr())));
00488       }
00489       throw ArithException("Can't solve exponential eqn: "+eqnThm.toString());
00490     }
00491     else {
00492       if(!isInteger(right)) {
00493         return processRealEq(eqnThm);
00494       }
00495       else {
00496         return processIntEq(eqnThm);
00497       }
00498     }
00499   } catch(ArithException& e) {
00500 
00501     // Nonlinear heuristics
00502     Theorem res;
00503     if (isPlus(right)) {
00504 
00505       // Search for common factor
00506       if (right[0].getRational() == 0) {
00507         Expr::iterator i = right.begin(), iend = right.end();
00508         ++i;
00509         set<Expr> factors;
00510         set<Expr>::iterator is, isend;
00511         getFactors(*i, factors);
00512         for (++i; i != iend; ++i) {
00513           set<Expr> factors2;
00514           getFactors(*i, factors2);
00515           for (is = factors.begin(), isend = factors.end(); is != isend; ++is) {
00516             if (factors2.find(*is) == factors2.end()) {
00517               factors.erase(is);
00518             }
00519           }
00520           if (factors.empty()) break;
00521         }
00522         if (!factors.empty()) {
00523           enqueueFact(iffMP(eqnThm, d_rules->divideEqnNonConst(rat(0), right, *(factors.begin()))));
00524           return getCommonRules()->trueTheorem();
00525         }
00526       }
00527 
00528       // Solve for something
00529       Expr isolated = right[1];
00530       Rational coeff;
00531       if (isMult(isolated) && isolated[0].isRational()) {
00532         coeff = isolated[0].getRational();
00533         DebugAssert(coeff != 0, "Expected nonzero coeff");
00534         isolated = canon(isolated / rat(coeff)).getRHS();
00535       } else coeff = 1;
00536       res = iffMP(eqnThm, d_rules->multEqn(rat(0), right, rat(-1/coeff)));
00537       res = canonPred(res);
00538       res = iffMP(res, d_rules->plusPredicate(res.getLHS(), res.getRHS(),
00539                                               isolated, EQ));
00540       res = canonPred(res);
00541 
00542       // Look for equal powers
00543       if (isPow(res.getLHS())) {
00544         Expr left = res.getLHS();
00545         if (isInteger(left[0])) {
00546           Rational pow = left[0].getRational();
00547           if (pow > 1) {
00548             right = res.getRHS();
00549             if (isPow(right) && right[0] == left[0]) {
00550               enqueueFact(iffMP(res, d_rules->elimPower(res.getExpr())));
00551               return getCommonRules()->trueTheorem();
00552             }
00553             else if (right.isRational()) {
00554               Rational r = right.getRational();
00555               if (pow % 2 == 0 && r < 0) {
00556                 return iffMP(res, d_rules->evenPowerEqNegConst(res.getExpr()));
00557               }
00558               DebugAssert(r != 0, "Expected nonzero const");
00559               Rational root = ratRoot(r, pow.getUnsigned());
00560               if (root != 0) {
00561                 enqueueFact(iffMP(res, d_rules->elimPowerConst(res.getExpr(), root)));
00562                 return getCommonRules()->trueTheorem();
00563               }
00564               else if (isInt(left[1].getType())) {
00565                 Theorem isIntx(isIntegerThm(left[1]));
00566                 DebugAssert(!isIntx.isNull(), "left = "+left.toString());
00567                 return iffMP(res, d_rules->intEqIrrational(res.getExpr(), isIntx));
00568               }
00569             }
00570           }
00571         }
00572       }
00573     }
00574     else {
00575       res = symmetryRule(eqnThm); // Flip to e' = 0
00576     }
00577     TRACE("arith eq", "doSolve: failed to solve an equation: ", e, "");
00578     IF_DEBUG(debugger.counter("FAILED to solve equalities")++;)
00579     setIncomplete("Non-linear arithmetic equalities");
00580     return res;
00581   }
00582   FatalAssert(false, "");
00583   return Theorem();
00584 }
00585 
00586 /*! pick a monomial for the input equation. This function is used only
00587  *  if the equation is an integer equation. Choose the monomial with
00588  *  the smallest absolute value of coefficient.
00589  */
00590 bool TheoryArith3::pickIntEqMonomial(const Expr& right, Expr& isolated, bool& nonlin)
00591 {
00592   DebugAssert(isPlus(right) && right.arity() > 1,
00593               "TheoryArith3::pickIntEqMonomial right is wrong :-): " +
00594               right.toString());
00595   DebugAssert(right[0].isRational(),
00596               "TheoryArith3::pickIntEqMonomial. right[0] must be const" +
00597               right.toString());
00598   DebugAssert(isInteger(right),
00599               "TheoryArith3::pickIntEqMonomial: right is of type int: " +
00600               right.toString());
00601   //right is of the form "C + a1x1 + ... + anxn". min is initialized
00602   //to a1
00603   Expr::iterator istart = right.begin(), iend = right.end();
00604   istart++;
00605   Expr::iterator i = istart, j;
00606   bool found = false;
00607   nonlin = false;
00608   Rational min, coeff;
00609   Expr leaf;
00610   for(; i != iend; ++i) {
00611     if (isLeaf(*i)) {
00612       leaf = *i;
00613       coeff = 1;
00614     }
00615     else if (isMult(*i) && (*i).arity() == 2 && (*i)[0].isRational() && isLeaf((*i)[1])) {
00616       leaf = (*i)[1];
00617       coeff = abs((*i)[0].getRational());
00618     }
00619     else {
00620       nonlin = true;
00621       continue;
00622     }
00623     for (j = istart; j != iend; ++j) {
00624       if (j != i && isLeafIn(leaf, *j)) break;
00625     }
00626     if (j == iend) {
00627       if (!found || min > coeff) {
00628         min = coeff;
00629         isolated = *i;
00630         found = true;
00631       }
00632     }
00633   }
00634   return found;
00635 }
00636 
00637 /*! input is 0=e' Theorem and some of the vars in e' are of
00638  * type REAL. isolate one of them and send back to framework. output
00639  * is "var = e''" Theorem.
00640  */
00641 Theorem
00642 TheoryArith3::processRealEq(const Theorem& eqn)
00643 {
00644   DebugAssert(eqn.getLHS().isRational() &&
00645               eqn.getLHS().getRational() == 0,
00646               "processRealEq invariant violated");
00647   Expr right = eqn.getRHS();
00648   // Find variable to isolate and store it in left.  Pick the largest
00649   // (according to the total ordering) variable.  FIXME: change from
00650   // total ordering to the ordering we devised for inequalities.
00651 
00652   // TODO: I have to pick a variable that appears as a variable in the
00653   // term but does not appear as a variable anywhere else.  The variable
00654   // must appear as a single leaf and not in a MULT expression with some
00655   // other variables and nor in a POW expression.
00656 
00657   bool found = false;
00658 
00659   Expr left;
00660 
00661   if (isPlus(right))  {
00662     for(int i = right.arity()-1; i>=0; --i) {
00663       Expr c = right[i];
00664       if(isRational(c))
00665         continue;
00666       if(!isInteger(c))  {
00667         if (isLeaf(c) ||
00668             ((isMult(c) && c.arity() == 2 && isLeaf(c[1])))) {
00669           int numoccurs = 0;
00670           Expr leaf = isLeaf(c) ? c : c[1];
00671           for (int j = 0; j < right.arity(); ++j) {
00672             if (j!= i
00673     && isLeafIn(leaf, right[j])
00674     ) {
00675               numoccurs++;
00676               break;
00677             }
00678           }
00679           if (!numoccurs) {
00680             left = c;
00681             found = true;
00682             break;
00683           }
00684         }
00685       }
00686     }
00687   }
00688   else if ((isMult(right) && right.arity() == 2 && isLeaf(right[1])) ||
00689            isLeaf(right)) {
00690     left = right;
00691     found = true;
00692   }
00693 
00694   if (!found) {
00695     throw
00696       ArithException("Can't find a leaf for solve in "+eqn.toString());
00697   }
00698 
00699   Rational r = -1;
00700   if (isMult(left))  {
00701     DebugAssert(left.arity() == 2, "only leaf should be chosen as lhs");
00702     DebugAssert(left[0].getRational() != 0, "left = "+left.toString());
00703     r = -1/left[0].getRational();
00704     left = left[1];
00705   }
00706 
00707   DebugAssert(isReal(getBaseType(left)) && !isInteger(left),
00708               "TheoryArith3::ProcessRealEq: left is integer:\n left = "
00709         +left.toString());
00710   // Normalize equation so that coefficient of the monomial
00711   // corresponding to "left" in eqn[1] is -1
00712   Theorem result(iffMP(eqn,
00713            d_rules->multEqn(eqn.getLHS(), eqn.getRHS(), rat(r))));
00714   result = canonPred(result);
00715 
00716   // Isolate left
00717   result = iffMP(result, d_rules->plusPredicate(result.getLHS(),
00718             result.getRHS(), left, EQ));
00719   result = canonPred(result);
00720   TRACE("arith","processRealEq => ",result," }");
00721   return result;
00722 }
00723 
00724 
00725 void TheoryArith3::getFactors(const Expr& e, set<Expr>& factors)
00726 {
00727   switch (e.getKind()) {
00728     case RATIONAL_EXPR: break;
00729     case MULT: {
00730       Expr::iterator i = e.begin(), iend = e.end();
00731       for (; i != iend; ++i) {
00732         getFactors(*i, factors);
00733       }
00734       break;
00735     }
00736     case POW: {
00737       DebugAssert(e.arity() == 2, "invariant violated");
00738       if (!isIntegerConst(e[0]) || e[0].getRational() <= 0) {
00739         throw ArithException("not positive integer exponent in "+e.toString());
00740       }
00741       if (isLeaf(e[1])) factors.insert(e[1]);
00742       break;
00743     }
00744     default: {
00745       DebugAssert(isLeaf(e), "expected leaf");
00746       DebugAssert(factors.find(e) == factors.end(), "expected new entry");
00747       factors.insert(e);
00748       break;
00749     }
00750   }
00751 }
00752 
00753 
00754 /*!
00755  * \param eqn is a single equation 0 = e
00756  * \return an equivalent Theorem (x = t AND 0 = e'), or just x = t
00757  */
00758 Theorem
00759 TheoryArith3::processSimpleIntEq(const Theorem& eqn)
00760 {
00761   TRACE("arith eq", "processSimpleIntEq(", eqn.getExpr(), ") {");
00762   DebugAssert(eqn.isRewrite(),
00763               "TheoryArith3::processSimpleIntEq: eqn must be equality" +
00764               eqn.getExpr().toString());
00765 
00766   Expr right = eqn.getRHS();
00767 
00768   DebugAssert(eqn.getLHS().isRational() && 0 == eqn.getLHS().getRational(),
00769               "TheoryArith3::processSimpleIntEq: LHS must be 0:\n" +
00770               eqn.getExpr().toString());
00771 
00772   DebugAssert(!isMult(right) && !isPow(right), "should have been handled above");
00773   if (isPlus(right)) {
00774     if (2 == right.arity() &&
00775         (isLeaf(right[1]) ||
00776          (isMult(right[1]) && right[1].arity() == 2 && right[1][0].isRational() && isLeaf(right[1][1])))) {
00777       //we take care of special cases like 0 = c + a.x, 0 = c + x,
00778       Expr c,x;
00779       separateMonomial(right[1], c, x);
00780       Theorem isIntx(isIntegerThm(x));
00781       DebugAssert(!isIntx.isNull(), "right = "+right.toString()
00782       +"\n x = "+x.toString());
00783       Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx)));
00784       TRACE("arith eq", "processSimpleIntEq[0 = c + a*x] => ", res, " }");
00785       return res;
00786     }
00787     // Pick a suitable monomial. isolated can be of the form x, a.x, -a.x
00788     Expr isolated;
00789     bool nonlin;
00790     if (pickIntEqMonomial(right, isolated, nonlin)) {
00791       TRACE("arith eq", "processSimpleIntEq: isolated = ", isolated, "");
00792 
00793       // First, we compute the 'sign factor' with which to multiply the
00794       // eqn.  if the coeff of isolated is positive (i.e. 'isolated' is
00795       // of the form x or a.x where a>0 ) then r must be -1 and if coeff
00796       // of 'isolated' is negative, r=1.
00797       Rational r = isMult(isolated) ?
00798         ((isolated[0].getRational() > 0) ? -1 : 1) : -1;
00799       Theorem result;
00800       if (-1 == r) {
00801         // r=-1 and hence 'isolated' is 'x' or 'a.x' where a is
00802         // positive.  modify eqn (0=e') to the equation (0=canon(-1*e'))
00803         result = iffMP(eqn, d_rules->multEqn(eqn.getLHS(), right, rat(r)));
00804         result = canonPred(result);
00805         Expr e = result.getRHS();
00806 
00807         // Isolate the 'isolated'
00808         result = iffMP(result,
00809                        d_rules->plusPredicate(result.getLHS(),result.getRHS(),
00810               isolated, EQ));
00811       } else {
00812         //r is 1 and hence isolated is -a.x. Make 'isolated' positive.
00813         const Rational& minusa = isolated[0].getRational();
00814         Rational a = -1*minusa;
00815         isolated = (a == 1)? isolated[1] : rat(a) * isolated[1];
00816 
00817         // Isolate the 'isolated'
00818         result = iffMP(eqn, d_rules->plusPredicate(eqn.getLHS(),
00819                                                    right,isolated,EQ));
00820       }
00821       // Canonize the result
00822       result = canonPred(result);
00823 
00824       //if isolated is 'x' or 1*x, then return result else continue processing.
00825       if(!isMult(isolated) || isolated[0].getRational() == 1) {
00826         TRACE("arith eq", "processSimpleIntEq[x = rhs] => ", result, " }");
00827         return result;
00828       } else if (!nonlin) {
00829         DebugAssert(isMult(isolated) && isolated[0].getRational() >= 2,
00830                     "TheoryArith3::processSimpleIntEq: isolated must be mult "
00831                     "with coeff >= 2.\n isolated = " + isolated.toString());
00832 
00833         // Compute IS_INTEGER() for lhs and rhs
00834         Expr lhs = result.getLHS();
00835         Expr rhs = result.getRHS();
00836         Expr a, x;
00837         separateMonomial(lhs, a, x);
00838         Theorem isIntLHS = isIntegerThm(x);
00839         vector<Theorem> isIntRHS;
00840         if(!isPlus(rhs)) { // rhs is a MULT
00841           Expr c, v;
00842           separateMonomial(rhs, c, v);
00843           isIntRHS.push_back(isIntegerThm(v));
00844           DebugAssert(!isIntRHS.back().isNull(), "");
00845         } else { // rhs is a PLUS
00846           DebugAssert(isPlus(rhs), "rhs = "+rhs.toString());
00847           DebugAssert(rhs.arity() >= 2, "rhs = "+rhs.toString());
00848           Expr::iterator i=rhs.begin(), iend=rhs.end();
00849           ++i; // Skip the free constant
00850           for(; i!=iend; ++i) {
00851             Expr c, v;
00852             separateMonomial(*i, c, v);
00853             isIntRHS.push_back(isIntegerThm(v));
00854             DebugAssert(!isIntRHS.back().isNull(), "");
00855           }
00856         }
00857         // Derive (EXISTS (x:INT): x = t2 AND 0 = t3)
00858         result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS);
00859         // Skolemize the quantifier
00860         result = getCommonRules()->skolemize(result);
00861         // Canonize t2 and t3 generated by this rule
00862         DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
00863                     "processSimpleIntEq: result = "+result.getExpr().toString());
00864         Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0));
00865         Theorem thm2 = canonPred(getCommonRules()->andElim(result, 1));
00866         Theorem newRes = getCommonRules()->andIntro(thm1, thm2);
00867         if(newRes.getExpr() != result.getExpr()) result = newRes;
00868 
00869         TRACE("arith eq", "processSimpleIntEq => ", result, " }");
00870         return result;
00871       }
00872     }
00873     throw
00874       ArithException("Can't find a leaf for solve in "+eqn.toString());
00875   } else {
00876     // eqn is 0 = x.  Flip it and return
00877     Theorem result = symmetryRule(eqn);
00878     TRACE("arith eq", "processSimpleIntEq[x = 0] => ", result, " }");
00879     return result;
00880   }
00881 }
00882 
00883 /*! input is 0=e' Theorem and all of the vars in e' are of
00884  * type INT. isolate one of them and send back to framework. output
00885  * is "var = e''" Theorem and some associated equations in
00886  * solved form.
00887  */
00888 Theorem
00889 TheoryArith3::processIntEq(const Theorem& eqn)
00890 {
00891   TRACE("arith eq", "processIntEq(", eqn.getExpr(), ") {");
00892   // Equations in the solved form.
00893   std::vector<Theorem> solvedAndNewEqs;
00894   Theorem newEq(eqn), result;
00895   bool done(false);
00896   do {
00897     result = processSimpleIntEq(newEq);
00898     // 'result' is of the from (x1=t1)  AND 0=t'
00899     if(result.isRewrite()) {
00900       solvedAndNewEqs.push_back(result);
00901       done = true;
00902     }
00903     else if (result.getExpr().isBoolConst()) {
00904       done = true;
00905     }
00906     else {
00907       DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
00908       "TheoryArith3::processIntEq("+eqn.getExpr().toString()
00909       +")\n result = "+result.getExpr().toString());
00910       solvedAndNewEqs.push_back(getCommonRules()->andElim(result, 0));
00911       newEq = getCommonRules()->andElim(result, 1);
00912     }
00913   } while(!done);
00914   Theorem res;
00915   if (result.getExpr().isFalse()) res = result;
00916   else if (solvedAndNewEqs.size() > 0)
00917     res = solvedForm(solvedAndNewEqs);
00918   else res = result;
00919   TRACE("arith eq", "processIntEq => ", res.getExpr(), " }");
00920   return res;
00921 }
00922 
00923 /*!
00924  * Takes a vector of equations and for every equation x_i=t_i
00925  * substitutes t_j for x_j in t_i for all j>i.  This turns the system
00926  * of equations into a solved form.
00927  *
00928  * Assumption: variables x_j may appear in the RHS terms t_i ONLY for
00929  * i<j, but not for i>=j.
00930  */
00931 Theorem
00932 TheoryArith3::solvedForm(const vector<Theorem>& solvedEqs)
00933 {
00934   DebugAssert(solvedEqs.size() > 0, "TheoryArith3::solvedForm()");
00935 
00936   // Trace code
00937   TRACE_MSG("arith eq", "TheoryArith3::solvedForm:solvedEqs(\n  [");
00938   IF_DEBUG(if(debugger.trace("arith eq")) {
00939     for(vector<Theorem>::const_iterator j = solvedEqs.begin(),
00940     jend=solvedEqs.end(); j!=jend;++j)
00941       TRACE("arith eq", "", j->getExpr(), ",\n   ");
00942   })
00943   TRACE_MSG("arith eq", "  ]) {");
00944   // End of Trace code
00945 
00946   vector<Theorem>::const_reverse_iterator
00947     i = solvedEqs.rbegin(),
00948     iend = solvedEqs.rend();
00949   // Substitution map: a variable 'x' is mapped to a Theorem x=t.
00950   // This map accumulates the resulting solved form.
00951   ExprMap<Theorem> subst;
00952   for(; i!=iend; ++i) {
00953     if(i->isRewrite()) {
00954       Theorem thm = substAndCanonize(*i, subst);
00955       TRACE("arith eq", "solvedForm: subst["+i->getLHS().toString()+"] = ",
00956       thm.getExpr(), "");
00957       subst[i->getLHS()] = thm;
00958     }
00959     else {
00960       // This is the FALSE case: just return the contradiction
00961       DebugAssert(i->getExpr().isFalse(),
00962       "TheoryArith3::solvedForm: an element of solvedEqs must "
00963       "be either EQ or FALSE: "+i->toString());
00964       return *i;
00965     }
00966   }
00967   // Now we've collected the solved form in 'subst'.  Wrap it up into
00968   // a conjunction and return.
00969   vector<Theorem> thms;
00970   for(ExprMap<Theorem>::iterator i=subst.begin(), iend=subst.end();
00971       i!=iend; ++i)
00972     thms.push_back(i->second);
00973   if (thms.size() > 1)
00974     return getCommonRules()->andIntro(thms);
00975   else
00976     return thms.back();
00977 }
00978 
00979 
00980 /*!
00981  * ASSUMPTION: 't' is a fully canonized arithmetic term, and every
00982  * element of subst is a fully canonized equation of the form x=e,
00983  * indexed by the LHS variable.
00984  */
00985 
00986 Theorem
00987 TheoryArith3::substAndCanonize(const Expr& t, ExprMap<Theorem>& subst)
00988 {
00989   TRACE("arith eq", "substAndCanonize(", t, ") {");
00990   // Quick and dirty check: return immediately if subst is empty
00991   if(subst.empty()) {
00992     Theorem res(reflexivityRule(t));
00993     TRACE("arith eq", "substAndCanonize[subst empty] => ", res, " }");
00994     return res;
00995   }
00996   // Check if we can substitute 't' directly
00997   ExprMap<Theorem>::iterator i = subst.find(t), iend=subst.end();
00998   if(i!=iend) {
00999     TRACE("arith eq", "substAndCanonize[subst] => ", i->second, " }");
01000     return i->second;
01001   }
01002   // The base case: t is an i-leaf
01003   if(isLeaf(t)) {
01004     Theorem res(reflexivityRule(t));
01005     TRACE("arith eq", "substAndCanonize[i-leaf] => ", res, " }");
01006     return res;
01007   }
01008   // 't' is an arithmetic term; recurse into the children
01009   vector<Theorem> thms;
01010   vector<unsigned> changed;
01011   for(unsigned j=0, jend=t.arity(); j!=jend; ++j) {
01012     Theorem thm = substAndCanonize(t[j], subst);
01013     if(thm.getRHS() != t[j]) {
01014       thm = canonThm(thm);
01015       thms.push_back(thm);
01016       changed.push_back(j);
01017     }
01018   }
01019   // Do the actual substitution and canonize the result
01020   Theorem res;
01021   if(thms.size() > 0) {
01022     res = substitutivityRule(t, changed, thms);
01023     res = canonThm(res);
01024   }
01025   else
01026     res = reflexivityRule(t);
01027   TRACE("arith eq", "substAndCanonize => ", res, " }");
01028   return res;
01029 }
01030 
01031 
01032 /*!
01033  *  ASSUMPTION: 't' is a fully canonized equation of the form x = t,
01034  *  and so is every element of subst, indexed by the LHS variable.
01035  */
01036 
01037 Theorem
01038 TheoryArith3::substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst)
01039 {
01040   // Quick and dirty check: return immediately if subst is empty
01041   if(subst.empty()) return eq;
01042 
01043   DebugAssert(eq.isRewrite(), "TheoryArith3::substAndCanonize: t = "
01044         +eq.getExpr().toString());
01045   const Expr& t = eq.getRHS();
01046   // Do the actual substitution in the term t
01047   Theorem thm = substAndCanonize(t, subst);
01048   // Substitution had no result: return the original equation
01049   if(thm.getRHS() == t) return eq;
01050   // Otherwise substitute the result into the equation
01051   vector<Theorem> thms;
01052   vector<unsigned> changed;
01053   thms.push_back(thm);
01054   changed.push_back(1);
01055   return iffMP(eq, substitutivityRule(eq.getExpr(), changed, thms));
01056 }
01057 
01058 
01059 void TheoryArith3::processBuffer()
01060 {
01061   // Process the inequalities in the buffer
01062   bool varOnRHS;
01063 
01064   for(; !inconsistent() && d_bufferIdx < d_buffer.size();
01065       d_bufferIdx = d_bufferIdx+1) {
01066     const Theorem& ineqThm = d_buffer[d_bufferIdx];
01067     // Skip this inequality if it is stale
01068     if(isStale(ineqThm.getExpr())) continue;
01069     Theorem thm1 = isolateVariable(ineqThm, varOnRHS);
01070     const Expr& ineq = thm1.getExpr();
01071     if((ineq).isFalse())
01072       setInconsistent(thm1);
01073     else if(!ineq.isTrue()) {
01074       // Check that the variable is indeed isolated correctly
01075       DebugAssert(varOnRHS? !isPlus(ineq[1]) : !isPlus(ineq[0]),
01076       "TheoryArith3::processBuffer(): bad result from "
01077       "isolateVariable:\nineq = "+ineq.toString());
01078       // and project the inequality
01079       projectInequalities(thm1, varOnRHS);
01080     }
01081   }
01082 }
01083 
01084 
01085 void TheoryArith3::updateStats(const Rational& c, const Expr& v)
01086 {
01087   TRACE("arith ineq", "updateStats("+c.toString()+", ", v, ")");
01088 
01089   // Dejan: update the max coefficient of the variable
01090   if (c < 0) {
01091     // Goes to the left side
01092     CDMap<Expr, Rational>::iterator maxFind = maxCoefficientLeft.find(v);
01093     if (maxFind == maxCoefficientLeft.end())
01094       maxCoefficientLeft[v] = - c;
01095     else
01096       if ((*maxFind).second < -c)
01097         (*maxFind).second = -c;
01098   } else {
01099     // Stays on the right side
01100     CDMap<Expr, Rational>::iterator maxFind = maxCoefficientRight.find(v);
01101     if (maxFind == maxCoefficientRight.end())
01102       maxCoefficientRight[v] = c;
01103     else
01104       if((*maxFind).second < c)
01105         (*maxFind).second = c;
01106   }
01107 
01108   if(c > 0) {
01109     if(d_countRight.count(v) > 0) d_countRight[v] = d_countRight[v] + 1;
01110     else d_countRight[v] = 1;
01111   }
01112   else
01113     if(d_countLeft.count(v) > 0) d_countLeft[v] = d_countLeft[v] + 1;
01114     else d_countLeft[v] = 1;
01115 }
01116 
01117 
01118 void TheoryArith3::updateStats(const Expr& monomial)
01119 {
01120   Expr c, m;
01121   separateMonomial(monomial, c, m);
01122   updateStats(c.getRational(), m);
01123 }
01124 
01125 
01126 void TheoryArith3::addToBuffer(const Theorem& thm) {
01127   // First, turn the inequality into 0 < rhs
01128   // FIXME: check if this can be optimized away
01129   Theorem result(thm);
01130   const Expr& e = thm.getExpr();
01131   // int kind = e.getKind();
01132   if(!(e[0].isRational() && e[0].getRational() == 0)) {
01133     result = iffMP(result, d_rules->rightMinusLeft(e));
01134     result = canonPred(result);
01135   }
01136   TRACE("arith ineq", "addToBuffer(", result.getExpr(), ")");
01137   // Push it into the buffer
01138   d_buffer.push_back(thm);
01139 
01140   // Collect the statistics about variables
01141   const Expr& rhs = thm.getExpr()[1];
01142   if(isPlus(rhs))
01143     for(Expr::iterator i=rhs.begin(), iend=rhs.end(); i!=iend; ++i)
01144       updateStats(*i);
01145   else // It's a monomial
01146     updateStats(rhs);
01147 }
01148 
01149 
01150 Theorem TheoryArith3::isolateVariable(const Theorem& inputThm,
01151                                      bool& isolatedVarOnRHS)
01152 {
01153   Theorem result(inputThm);
01154   const Expr& e = inputThm.getExpr();
01155   TRACE("arith","isolateVariable(",e,") {");
01156   TRACE("arith ineq", "isolateVariable(", e, ") {");
01157   //we assume all the children of e are canonized
01158   DebugAssert(isLT(e)||isLE(e),
01159               "TheoryArith3::isolateVariable: " + e.toString() +
01160               " wrong kind");
01161   int kind = e.getKind();
01162   DebugAssert(e[0].isRational() && e[0].getRational() == 0,
01163               "TheoryArith3::isolateVariable: theorem must be of "
01164               "the form 0 < rhs: " + inputThm.toString());
01165 
01166   const Expr& zero = e[0];
01167   Expr right = e[1];
01168   // Check for trivial in-equation.
01169   if (right.isRational()) {
01170     result = iffMP(result, d_rules->constPredicate(e));
01171     TRACE("arith ineq","isolateVariable => ",result.getExpr()," }");
01172     TRACE("arith","isolateVariable => ",result," }");
01173     return result;
01174   }
01175 
01176   // Normalization of inequality to make coefficients integer and
01177   // relatively prime.
01178 
01179   Expr factor(computeNormalFactor(right));
01180   TRACE("arith", "isolateVariable: factor = ", factor, "");
01181   DebugAssert(factor.getRational() > 0,
01182               "isolateVariable: factor="+factor.toString());
01183   // Now multiply the inequality by the factor, unless it is 1
01184   if(factor.getRational() != 1) {
01185     result = iffMP(result, d_rules->multIneqn(e, factor));
01186     // And canonize the result
01187     result = canonPred(result);
01188     right = result.getExpr()[1];
01189   }
01190 
01191   // Find monomial to isolate and store it in isolatedMonomial
01192   Expr isolatedMonomial = right;
01193 
01194   if (isPlus(right))
01195     isolatedMonomial = pickMonomial(right);
01196 
01197   Rational r = -1;
01198   isolatedVarOnRHS = true;
01199   if (isMult(isolatedMonomial)) {
01200     r = ((isolatedMonomial[0].getRational()) >= 0)? -1 : 1;
01201     isolatedVarOnRHS =
01202       ((isolatedMonomial[0].getRational()) >= 0)? true : false;
01203   }
01204   isolatedMonomial = canon(rat(-1)*isolatedMonomial).getRHS();
01205   // Isolate isolatedMonomial on to the LHS
01206   result = iffMP(result, d_rules->plusPredicate(zero, right,
01207                                                 isolatedMonomial, kind));
01208   // Canonize the resulting inequality
01209   result = canonPred(result);
01210   if(1 != r) {
01211     result = iffMP(result, d_rules->multIneqn(result.getExpr(), rat(r)));
01212     result = canonPred(result);
01213   }
01214   TRACE("arith ineq","isolateVariable => ",result.getExpr()," }");
01215   TRACE("arith","isolateVariable => ",result," }");
01216   return result;
01217 }
01218 
01219 Expr
01220 TheoryArith3::computeNormalFactor(const Expr& right) {
01221   // Strategy: compute f = lcm(d1...dn)/gcd(c1...cn), where the RHS is
01222   // of the form c1/d1*x1 + ... + cn/dn*xn
01223   Rational factor;
01224   if(isPlus(right)) {
01225     vector<Rational> nums, denoms;
01226     for(int i=0, iend=right.arity(); i<iend; ++i) {
01227       switch(right[i].getKind()) {
01228       case RATIONAL_EXPR: {
01229         Rational c(abs(right[i].getRational()));
01230         nums.push_back(c.getNumerator());
01231         denoms.push_back(c.getDenominator());
01232         break;
01233         }
01234       case MULT: {
01235         Rational c(abs(right[i][0].getRational()));
01236         nums.push_back(c.getNumerator());
01237         denoms.push_back(c.getDenominator());
01238         break;
01239         }
01240       default: // it's a variable
01241         nums.push_back(1);
01242         denoms.push_back(1);
01243         break;
01244       }
01245     }
01246     Rational gcd_nums = gcd(nums);
01247     // x/0 == 0 in our model, as a total extension of arithmetic.  The
01248     // particular value of x/0 is irrelevant, since the DP is guarded
01249     // by the top-level TCCs, and it is safe to return any value in
01250     // cases when terms are undefined.
01251     factor = (gcd_nums==0)? 0 : (lcm(denoms) / gcd_nums);
01252   } else if(isMult(right)) {
01253     const Rational& r = right[0].getRational();
01254     factor = (r==0)? 0 : (1/abs(r));
01255   }
01256   else
01257     factor = 1;
01258   return rat(factor);
01259 }
01260 
01261 
01262 bool TheoryArith3::lessThanVar(const Expr& isolatedMonomial, const Expr& var2)
01263 {
01264   DebugAssert(!isRational(var2) && !isRational(isolatedMonomial),
01265               "TheoryArith3::findMaxVar: isolatedMonomial cannot be rational" +
01266               isolatedMonomial.toString());
01267   Expr c, var0, var1;
01268   separateMonomial(isolatedMonomial, c, var0);
01269   separateMonomial(var2, c, var1);
01270   return var0 < var1;
01271 }
01272 
01273 /*! "Stale" means it contains non-simplified subexpressions.  For
01274  *  terms, it checks the expression's find pointer; for formulas it
01275  *  checks the children recursively (no caching!).  So, apply it with
01276  *  caution, and only to simple atomic formulas (like inequality).
01277  */
01278 bool TheoryArith3::isStale(const Expr& e) {
01279   if(e.isTerm())
01280     return e != find(e).getRHS();
01281   // It's better be a simple predicate (like inequality); we check the
01282   // kids recursively
01283   bool stale=false;
01284   for(Expr::iterator i=e.begin(), iend=e.end(); !stale && i!=iend; ++i)
01285     stale = isStale(*i);
01286   return stale;
01287 }
01288 
01289 
01290 bool TheoryArith3::isStale(const TheoryArith3::Ineq& ineq) {
01291   TRACE("arith ineq", "isStale(", ineq, ") {");
01292   const Expr& ineqExpr = ineq.ineq().getExpr();
01293   const Rational& c = freeConstIneq(ineqExpr, ineq.varOnRHS());
01294   bool strict(isLT(ineqExpr));
01295   const FreeConst& fc = ineq.getConst();
01296 
01297   bool subsumed;
01298 
01299   if(ineq.varOnRHS()) {
01300     subsumed = (c < fc.getConst() ||
01301     (c == fc.getConst() && !strict && fc.strict()));
01302   } else {
01303     subsumed = (c > fc.getConst() ||
01304     (c == fc.getConst() && strict && !fc.strict()));
01305   }
01306 
01307   bool res;
01308   if(subsumed) {
01309     res = true;
01310     TRACE("arith ineq", "isStale[subsumed] => ", res? "true" : "false", " }");
01311   }
01312   else {
01313     res = isStale(ineqExpr);
01314     TRACE("arith ineq", "isStale[updated] => ", res? "true" : "false", " }");
01315   }
01316   return res;
01317 }
01318 
01319 
01320 void TheoryArith3::separateMonomial(const Expr& e, Expr& c, Expr& var) {
01321   TRACE("separateMonomial", "separateMonomial(", e, ")");
01322   DebugAssert(!isPlus(e),
01323         "TheoryArith3::separateMonomial(e = "+e.toString()+")");
01324   if(isMult(e)) {
01325     DebugAssert(e.arity() >= 2,
01326     "TheoryArith3::separateMonomial(e = "+e.toString()+")");
01327     c = e[0];
01328     if(e.arity() == 2) var = e[1];
01329     else {
01330       vector<Expr> kids = e.getKids();
01331       kids[0] = rat(1);
01332       var = multExpr(kids);
01333     }
01334   } else {
01335     c = rat(1);
01336     var = e;
01337   }
01338   DebugAssert(c.isRational(), "TheoryArith3::separateMonomial(e = "
01339         +e.toString()+", c = "+c.toString()+")");
01340   DebugAssert(!isMult(var) || (var[0].isRational() && var[0].getRational()==1),
01341         "TheoryArith3::separateMonomial(e = "
01342         +e.toString()+", var = "+var.toString()+")");
01343 }
01344 
01345 
01346 void TheoryArith3::projectInequalities(const Theorem& theInequality,
01347                                       bool isolatedVarOnRHS)
01348 {
01349   TRACE("arith ineq", "projectInequalities(", theInequality.getExpr(),
01350         ", isolatedVarOnRHS="+string(isolatedVarOnRHS? "true" : "false")
01351         +") {");
01352   DebugAssert(isLE(theInequality.getExpr()) ||
01353               isLT(theInequality.getExpr()),
01354               "TheoryArith3::projectIsolatedVar: "\
01355               "theInequality is of the wrong form: " +
01356               theInequality.toString());
01357   //TODO: DebugAssert to check if the isolatedMonomial is of the right
01358   //form and the whether we are indeed getting inequalities.
01359   Theorem theIneqThm(theInequality);
01360   Expr theIneq = theIneqThm.getExpr();
01361 
01362   Theorem isIntLHS(isIntegerThm(theIneq[0]));
01363   Theorem isIntRHS(isIntegerThm(theIneq[1]));
01364   bool isInt = (!isIntLHS.isNull() && !isIntRHS.isNull());
01365   // If the inequality is strict and integer, change it to non-strict
01366   if(isLT(theIneq) && isInt) {
01367     Theorem thm = d_rules->lessThanToLE(theInequality, isIntLHS, isIntRHS,
01368           !isolatedVarOnRHS);
01369     theIneqThm = canonPred(iffMP(theIneqThm, thm));
01370     theIneq = theIneqThm.getExpr();
01371   }
01372   Expr isolatedMonomial =
01373     isolatedVarOnRHS ? theIneq[1] : theIneq[0];
01374 
01375   Expr monomialVar, a;
01376   separateMonomial(isolatedMonomial, a, monomialVar);
01377 
01378   bool subsumed;
01379   const FreeConst& bestConst =
01380     updateSubsumptionDB(theIneq, isolatedVarOnRHS, subsumed);
01381 
01382   if(subsumed) {
01383     IF_DEBUG(debugger.counter("subsumed inequalities")++;)
01384     TRACE("arith ineq", "subsumed inequality: ", theIneq, "");
01385   } else {
01386     // If the isolated variable is actually a non-linear term, we are
01387     // incomplete
01388     if(isMult(monomialVar) || isPow(monomialVar))
01389       setIncomplete("Non-linear arithmetic inequalities");
01390 
01391     // First, we need to make sure the isolated inequality is
01392     // setup properly.
01393     //    setupRec(theIneq[0]);
01394     //    setupRec(theIneq[1]);
01395     theoryCore()->setupTerm(theIneq[0], this, theIneqThm);
01396     theoryCore()->setupTerm(theIneq[1], this, theIneqThm);
01397     // Add the inequality into the appropriate DB.
01398     ExprMap<CDList<Ineq> *>& db1 =
01399       isolatedVarOnRHS ? d_inequalitiesRightDB : d_inequalitiesLeftDB;
01400     ExprMap<CDList<Ineq> *>::iterator it1 = db1.find(monomialVar);
01401     if(it1 == db1.end()) {
01402       CDList<Ineq> * list = new(true) CDList<Ineq>(theoryCore()->getCM()->getCurrentContext());
01403       list->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
01404       db1[monomialVar] = list;
01405     }
01406     else
01407       ((*it1).second)->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
01408 
01409     ExprMap<CDList<Ineq> *>& db2 =
01410       isolatedVarOnRHS ? d_inequalitiesLeftDB : d_inequalitiesRightDB;
01411     ExprMap<CDList<Ineq> *>::iterator it = db2.find(monomialVar);
01412     if(it == db2.end()) {
01413       TRACE_MSG("arith ineq", "projectInequalities[not in DB] => }");
01414       return;
01415     }
01416 
01417     CDList<Ineq>& listOfDBIneqs = *((*it).second);
01418     Theorem betaLTt, tLTalpha, thm;
01419     for(size_t i = 0, iend=listOfDBIneqs.size(); i!=iend; ++i) {
01420       const Ineq& ineqEntry = listOfDBIneqs[i];
01421       const Theorem& ineqThm = ineqEntry.ineq();
01422       if(!isStale(ineqEntry)) {
01423   betaLTt = isolatedVarOnRHS ? theIneqThm : ineqThm;
01424   tLTalpha = isolatedVarOnRHS ? ineqThm : theIneqThm;
01425   thm = normalizeProjectIneqs(betaLTt, tLTalpha);
01426 
01427   IF_DEBUG(debugger.counter("real shadows")++;)
01428 
01429   // Check for TRUE and FALSE theorems
01430   Expr e(thm.getExpr());  if(e.isFalse()) {
01431     setInconsistent(thm);
01432     TRACE_MSG("arith ineq", "projectInequalities[inconsistent] => }");
01433     return;
01434   }
01435   else {
01436     if(!e.isTrue() && !e.isEq())
01437       addToBuffer(thm);
01438     else if(e.isEq())
01439       enqueueFact(thm);
01440   }
01441       } else {
01442   IF_DEBUG(debugger.counter("stale inequalities")++;)
01443       }
01444     }
01445   }
01446   TRACE_MSG("arith ineq", "projectInequalities => }");
01447 }
01448 
01449 Theorem TheoryArith3::normalizeProjectIneqs(const Theorem& ineqThm1,
01450                                            const Theorem& ineqThm2)
01451 {
01452   //ineq1 is of the form beta < b.x  or beta < x  [ or with <= ]
01453   //ineq2 is of the form a.x < alpha   or x < alpha.
01454   Theorem betaLTt = ineqThm1, tLTalpha = ineqThm2;
01455   Expr ineq1 = betaLTt.getExpr();
01456   Expr ineq2 = tLTalpha.getExpr();
01457   Expr c,x;
01458   separateMonomial(ineq2[0], c, x);
01459   Theorem isIntx(isIntegerThm(x));
01460   Theorem isIntBeta(isIntegerThm(ineq1[0]));
01461   Theorem isIntAlpha(isIntegerThm(ineq2[1]));
01462   bool isInt = !(isIntx.isNull() || isIntBeta.isNull() || isIntAlpha.isNull());
01463 
01464   TRACE("arith ineq", "normalizeProjectIneqs(", ineq1,
01465         ", "+ineq2.toString()+") {");
01466   DebugAssert((isLE(ineq1) || isLT(ineq1)) &&
01467               (isLE(ineq2) || isLT(ineq2)),
01468               "TheoryArith3::normalizeProjectIneqs: Wrong Kind inputs: " +
01469               ineq1.toString() + ineq2.toString());
01470   DebugAssert(!isPlus(ineq1[1]) && !isPlus(ineq2[0]),
01471               "TheoryArith3::normalizeProjectIneqs: Wrong Kind inputs: " +
01472               ineq1.toString() + ineq2.toString());
01473 
01474   //compute the factors to multiply the two inequalities with
01475   //so that they get the form beta < t and t < alpha.
01476   Rational factor1 = 1, factor2 = 1;
01477   Rational b = isMult(ineq1[1]) ? (ineq1[1])[0].getRational() : 1;
01478   Rational a = isMult(ineq2[0]) ? (ineq2[0])[0].getRational() : 1;
01479   if(b != a) {
01480     factor1 = a;
01481     factor2 = b;
01482   }
01483 
01484   //if the ineqs are of type int then apply one of the gray
01485   //dark shadow rules.
01486   // FIXME: intResult should also be checked for immediate
01487   // optimizations, as those below for 'result'.  Also, if intResult
01488   // is a single inequality, we may want to handle it similarly to the
01489   // 'result' rather than enqueuing directly.
01490   if(isInt && (a >= 2 || b >= 2)) {
01491     Theorem intResult;
01492     if(a <= b)
01493       intResult = d_rules->darkGrayShadow2ab(betaLTt, tLTalpha,
01494                isIntAlpha, isIntBeta, isIntx);
01495     else
01496       intResult = d_rules->darkGrayShadow2ba(betaLTt, tLTalpha,
01497                isIntAlpha, isIntBeta, isIntx);
01498     enqueueFact(intResult);
01499     // Fetch dark and gray shadows
01500     const Expr& DorG = intResult.getExpr();
01501     DebugAssert(DorG.isOr() && DorG.arity()==2, "DorG = "+DorG.toString());
01502     const Expr& D = DorG[0];
01503     const Expr& G = DorG[1];
01504     DebugAssert(D.getKind()==DARK_SHADOW, "D = "+D.toString());
01505     DebugAssert(G.getKind()==GRAY_SHADOW, "G = "+G.toString());
01506     // Set the higher splitter priority for dark shadow
01507     Expr tmp = simplifyExpr(D);
01508     if (!tmp.isBoolConst())
01509       addSplitter(tmp, 5);
01510     // Also set a higher priority to the NEGATION of GRAY_SHADOW
01511     tmp = simplifyExpr(!G);
01512     if (!tmp.isBoolConst())
01513       addSplitter(tmp, 1);
01514     IF_DEBUG(debugger.counter("dark+gray shadows")++;)
01515   }
01516 
01517   //actually normalize the inequalities
01518   if(1 != factor1) {
01519     std::vector<Theorem> thms1;
01520     Theorem thm2 = iffMP(betaLTt, d_rules->multIneqn(ineq1, rat(factor1)));
01521     betaLTt = canonPred(thm2);
01522     ineq1 = betaLTt.getExpr();
01523   }
01524   if(1 != factor2) {
01525     std::vector<Theorem> thms1;
01526     Theorem thm2 = iffMP(tLTalpha, d_rules->multIneqn(ineq2, rat(factor2)));
01527     tLTalpha = canonPred(thm2);
01528     ineq2 = tLTalpha.getExpr();
01529   }
01530 
01531   //IF_DEBUG(debugger.counter("real shadows")++;)
01532 
01533   Expr beta(ineq1[0]);
01534   Expr alpha(ineq2[1]);
01535   // In case of alpha <= t <= alpha, we generate t = alpha
01536   if(isLE(ineq1) && isLE(ineq2) && alpha == beta) {
01537     Theorem result = d_rules->realShadowEq(betaLTt, tLTalpha);
01538     TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
01539     return result;
01540   }
01541 
01542   // Check if this inequality is a finite interval
01543   if(isInt)
01544     processFiniteInterval(betaLTt, tLTalpha);
01545 
01546   //project the normalized inequalities.
01547 
01548   Theorem result = d_rules->realShadow(betaLTt, tLTalpha);
01549 
01550   // FIXME: Clark's changes.  Is 'rewrite' more or less efficient?
01551 //   result = iffMP(result, rewrite(result.getExpr()));
01552 //   TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
01553 
01554   // Now, transform the result into 0 < rhs and see if rhs is a const
01555   Expr e(result.getExpr());
01556   // int kind = e.getKind();
01557   if(!(e[0].isRational() && e[0].getRational() == 0)) {
01558     result = iffMP(result, d_rules->rightMinusLeft(e));
01559     result = canonPred(result);
01560   }
01561 
01562   //result is "0 kind e'". where e' is equal to canon(e[1]-e[0])
01563   Expr right = result.getExpr()[1];
01564   // Check for trivial inequality
01565   if (right.isRational())
01566     result = iffMP(result, d_rules->constPredicate(result.getExpr()));
01567   TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
01568   return result;
01569 }
01570 
01571 Rational TheoryArith3::currentMaxCoefficient(Expr var)
01572 {
01573   bool foundLeft = false;
01574   bool foundRight = false;
01575   Rational leftMax = 1;
01576   Rational rightMax = 1;
01577 
01578   // If the coefitient was found earlier and fixed, just return it
01579   CDMap<Expr, Rational>::iterator findFixed = fixedMaxCoefficient.find(var);
01580   if (findFixed != fixedMaxCoefficient.end())
01581     return (*findFixed).second;
01582 
01583   // Find the biggest left side coefficient
01584   CDMap<Expr, Rational>::iterator findMaxLeft = maxCoefficientLeft.find(var);
01585   if (findMaxLeft != maxCoefficientLeft.end()) {
01586     foundLeft = true;
01587     leftMax = (*findMaxLeft).second;
01588   }
01589 
01590   //
01591   CDMap<Expr, Rational>::iterator findMaxRight = maxCoefficientRight.find(var);
01592   if (findMaxRight != maxCoefficientRight.end()) {
01593     foundRight = true;
01594     rightMax = (*findMaxRight).second;
01595   }
01596 
01597   if (foundLeft && foundRight) {
01598     if (leftMax < rightMax) return rightMax;
01599     else return leftMax;
01600   }
01601 
01602   return Rational(1) / (leftMax * rightMax);
01603 }
01604 
01605 void TheoryArith3::fixCurrentMaxCoefficient(Expr var, Rational max) {
01606   fixedMaxCoefficient[var] = max;
01607 }
01608 
01609 void TheoryArith3::selectSmallestByCoefficient(vector<Expr> input, vector<Expr>& output) {
01610 
01611   // Clear the output vector
01612   output.clear();
01613 
01614   // Get the first variable, and set it as best
01615   Expr best_variable = input[0];
01616   Rational best_coefficient = currentMaxCoefficient(best_variable);
01617   output.push_back(best_variable);
01618 
01619   for(unsigned int i = 1; i < input.size(); i ++) {
01620 
01621     // Get the current variable
01622     Expr current_variable = input[i];
01623     // Get the current variable's max coefficient
01624     Rational current_coefficient = currentMaxCoefficient(current_variable);
01625 
01626     // If strictly better than the current best, remember it
01627     if ((current_coefficient < best_coefficient)) {
01628       best_variable = current_variable;
01629       best_coefficient = current_coefficient;
01630       output.clear();
01631     }
01632 
01633     // If equal to the current best, push it to the stack
01634     if (current_coefficient == best_coefficient)
01635         output.push_back(current_variable);
01636   }
01637 
01638     // Fix the selected best coefficient
01639   fixCurrentMaxCoefficient(best_variable, best_coefficient);
01640 }
01641 
01642 Expr TheoryArith3::pickMonomial(const Expr& right)
01643 {
01644   DebugAssert(isPlus(right), "TheoryArith3::pickMonomial: Wrong Kind: " +
01645               right.toString());
01646   if(theoryCore()->getFlags()["var-order"].getBool()) {
01647     Expr::iterator i = right.begin();
01648     Expr isolatedMonomial = right[1];
01649     //PLUS always has at least two elements and the first element is
01650     //always a constant. hence ++i in the initialization of the for
01651     //loop.
01652     for(++i; i != right.end(); ++i)
01653       if(lessThanVar(isolatedMonomial,*i))
01654         isolatedMonomial = *i;
01655     return isolatedMonomial;
01656   }
01657 
01658   ExprMap<Expr> var2monomial;
01659   vector<Expr> vars;
01660   Expr::iterator i = right.begin(), iend = right.end();
01661   for(;i != iend; ++i) {
01662     if(i->isRational())
01663       continue;
01664     Expr c, var;
01665     separateMonomial(*i, c, var);
01666     var2monomial[var] = *i;
01667     vars.push_back(var);
01668   }
01669 
01670   vector<Expr> largest;
01671   d_graph.selectLargest(vars, largest);
01672   DebugAssert(0 < largest.size(),
01673               "TheoryArith3::pickMonomial: selectLargest: failed!!!!");
01674 
01675   // DEJAN: Rafine the largest by coefficient values
01676   vector<Expr> largest_small_coeff;
01677   selectSmallestByCoefficient(largest, largest_small_coeff);
01678   DebugAssert(0 < largest_small_coeff.size(), "TheoryArith3::pickMonomial: selectLargestByCOefficient: failed!!!!");
01679 
01680   size_t pickedVar = 0;
01681     // Pick the variable which will generate the fewest number of
01682     // projections
01683 
01684   size_t size = largest_small_coeff.size();
01685   int minProjections = -1;
01686   if (size > 1)
01687   for(size_t k=0; k< size; ++k) {
01688       const Expr& var(largest_small_coeff[k]), monom(var2monomial[var]);
01689       // Grab the counters for the variable
01690       int nRight = (d_countRight.count(var) > 0)? d_countRight[var] : 0;
01691       int nLeft = (d_countLeft.count(var) > 0)? d_countLeft[var] : 0;
01692       int n(nRight*nLeft);
01693       TRACE("arith ineq", "pickMonomial: var=", var,
01694             ", nRight="+int2string(nRight)+", nLeft="+int2string(nLeft));
01695       if(minProjections < 0 || minProjections > n) {
01696         minProjections = n;
01697         pickedVar = k;
01698       }
01699       TRACE("arith ineq", "Number of projections for "+var.toString()+" = ", n, "");
01700   }
01701 
01702 
01703   const Expr& largestVar = largest_small_coeff[pickedVar];
01704   // FIXME: TODO: update the counters (subtract counts for the vars
01705   // other than largestVar
01706 
01707   // Update the graph (all edges to the largest in the graph, not just the small coefficients).
01708   for(size_t k = 0; k < vars.size(); ++k) {
01709     if(vars[k] != largestVar)
01710       d_graph.addEdge(largestVar, vars[k]);
01711   }
01712 
01713   return var2monomial[largestVar];
01714 }
01715 
01716 void TheoryArith3::VarOrderGraph::addEdge(const Expr& e1, const Expr& e2)
01717 {
01718   TRACE("arith var order", "addEdge("+e1.toString()+" > ", e2, ")");
01719   DebugAssert(e1 != e2, "TheoryArith3::VarOrderGraph::addEdge("
01720         +e1.toString()+", "+e2.toString()+")");
01721   d_edges[e1].push_back(e2);
01722 }
01723 
01724 //returns true if e1 < e2, else false(i.e e2 < e1 or e1,e2 are not
01725 //comparable)
01726 bool TheoryArith3::VarOrderGraph::lessThan(const Expr& e1, const Expr& e2)
01727 {
01728   d_cache.clear();
01729   //returns true if e1 is in the subtree rooted at e2 implying e1 < e2
01730   return dfs(e1,e2);
01731 }
01732 
01733 //returns true if e1 is in the subtree rooted at e2 implying e1 < e2
01734 bool TheoryArith3::VarOrderGraph::dfs(const Expr& e1, const Expr& e2)
01735 {
01736   if(e1 == e2)
01737     return true;
01738   if(d_cache.count(e2) > 0)
01739     return false;
01740   if(d_edges.count(e2) == 0)
01741     return false;
01742   d_cache[e2] = true;
01743   vector<Expr>& e2Edges = d_edges[e2];
01744   vector<Expr>::iterator i = e2Edges.begin();
01745   vector<Expr>::iterator iend = e2Edges.end();
01746   //if dfs finds e1 then i != iend else i is equal to iend
01747   for(; i != iend && !dfs(e1,*i); ++i);
01748   return (i != iend);
01749 }
01750 
01751 
01752 void TheoryArith3::VarOrderGraph::selectSmallest(vector<Expr>& v1,
01753                                                vector<Expr>& v2)
01754 {
01755   int v1Size = v1.size();
01756   vector<bool> v3(v1Size);
01757   for(int j=0; j < v1Size; ++j)
01758     v3[j] = false;
01759 
01760   for(int j=0; j < v1Size; ++j) {
01761     if(v3[j]) continue;
01762     for(int i =0; i < v1Size; ++i) {
01763       if((i == j) || v3[i])
01764         continue;
01765       if(lessThan(v1[i],v1[j])) {
01766         v3[j] = true;
01767         break;
01768       }
01769     }
01770   }
01771   vector<Expr> new_v1;
01772 
01773   for(int j = 0; j < v1Size; ++j)
01774     if(!v3[j]) v2.push_back(v1[j]);
01775     else new_v1.push_back(v1[j]);
01776   v1 = new_v1;
01777 }
01778 
01779 
01780 void TheoryArith3::VarOrderGraph::selectLargest(const vector<Expr>& v1,
01781                                                vector<Expr>& v2)
01782 {
01783   int v1Size = v1.size();
01784   vector<bool> v3(v1Size);
01785   for(int j=0; j < v1Size; ++j)
01786     v3[j] = false;
01787 
01788   for(int j=0; j < v1Size; ++j) {
01789     if(v3[j]) continue;
01790     for(int i =0; i < v1Size; ++i) {
01791       if((i == j) || v3[i])
01792         continue;
01793       if(lessThan(v1[j],v1[i])) {
01794         v3[j] = true;
01795         break;
01796       }
01797     }
01798   }
01799 
01800   for(int j = 0; j < v1Size; ++j)
01801     if(!v3[j]) v2.push_back(v1[j]);
01802 }
01803 
01804 ///////////////////////////////////////////////////////////////////////////////
01805 // TheoryArith3 Public Methods                                                //
01806 ///////////////////////////////////////////////////////////////////////////////
01807 
01808 
01809 TheoryArith3::TheoryArith3(TheoryCore* core)
01810   : TheoryArith(core, "Arithmetic3"),
01811     d_diseq(core->getCM()->getCurrentContext()),
01812     d_diseqIdx(core->getCM()->getCurrentContext(), 0, 0),
01813     d_inModelCreation(core->getCM()->getCurrentContext(), false, 0),
01814     d_freeConstDB(core->getCM()->getCurrentContext()),
01815     d_buffer(core->getCM()->getCurrentContext()),
01816     // Initialize index to 0 at scope 0
01817     d_bufferIdx(core->getCM()->getCurrentContext(), 0, 0),
01818     d_bufferThres(&(core->getFlags()["ineq-delay"].getInt())),
01819     d_countRight(core->getCM()->getCurrentContext()),
01820     d_countLeft(core->getCM()->getCurrentContext()),
01821     d_sharedTerms(core->getCM()->getCurrentContext()),
01822     d_sharedVars(core->getCM()->getCurrentContext()),
01823     maxCoefficientLeft(core->getCM()->getCurrentContext()),
01824     maxCoefficientRight(core->getCM()->getCurrentContext()),
01825     fixedMaxCoefficient(core->getCM()->getCurrentContext())
01826 {
01827   IF_DEBUG(d_diseq.setName("CDList[TheoryArith3::d_diseq]");)
01828   IF_DEBUG(d_buffer.setName("CDList[TheoryArith3::d_buffer]");)
01829   IF_DEBUG(d_bufferIdx.setName("CDList[TheoryArith3::d_bufferIdx]");)
01830 
01831   getEM()->newKind(REAL, "_REAL", true);
01832   getEM()->newKind(INT, "_INT", true);
01833   getEM()->newKind(SUBRANGE, "_SUBRANGE", true);
01834 
01835   getEM()->newKind(UMINUS, "_UMINUS");
01836   getEM()->newKind(PLUS, "_PLUS");
01837   getEM()->newKind(MINUS, "_MINUS");
01838   getEM()->newKind(MULT, "_MULT");
01839   getEM()->newKind(DIVIDE, "_DIVIDE");
01840   getEM()->newKind(POW, "_POW");
01841   getEM()->newKind(INTDIV, "_INTDIV");
01842   getEM()->newKind(MOD, "_MOD");
01843   getEM()->newKind(LT, "_LT");
01844   getEM()->newKind(LE, "_LE");
01845   getEM()->newKind(GT, "_GT");
01846   getEM()->newKind(GE, "_GE");
01847   getEM()->newKind(IS_INTEGER, "_IS_INTEGER");
01848   getEM()->newKind(NEGINF, "_NEGINF");
01849   getEM()->newKind(POSINF, "_POSINF");
01850   getEM()->newKind(DARK_SHADOW, "_DARK_SHADOW");
01851   getEM()->newKind(GRAY_SHADOW, "_GRAY_SHADOW");
01852 
01853   getEM()->newKind(REAL_CONST, "_REAL_CONST");
01854 
01855   vector<int> kinds;
01856   kinds.push_back(REAL);
01857   kinds.push_back(INT);
01858   kinds.push_back(SUBRANGE);
01859   kinds.push_back(IS_INTEGER);
01860   kinds.push_back(UMINUS);
01861   kinds.push_back(PLUS);
01862   kinds.push_back(MINUS);
01863   kinds.push_back(MULT);
01864   kinds.push_back(DIVIDE);
01865   kinds.push_back(POW);
01866   kinds.push_back(INTDIV);
01867   kinds.push_back(MOD);
01868   kinds.push_back(LT);
01869   kinds.push_back(LE);
01870   kinds.push_back(GT);
01871   kinds.push_back(GE);
01872   kinds.push_back(RATIONAL_EXPR);
01873   kinds.push_back(NEGINF);
01874   kinds.push_back(POSINF);
01875   kinds.push_back(DARK_SHADOW);
01876   kinds.push_back(GRAY_SHADOW);
01877   kinds.push_back(REAL_CONST);
01878 
01879   registerTheory(this, kinds, true);
01880 
01881   d_rules = createProofRules3();
01882 
01883   d_realType = Type(getEM()->newLeafExpr(REAL));
01884   d_intType  = Type(getEM()->newLeafExpr(INT));
01885 }
01886 
01887 
01888 // Destructor: delete the proof rules class if it's present
01889 TheoryArith3::~TheoryArith3() {
01890   if(d_rules != NULL) delete d_rules;
01891   // Clear the inequality databases
01892   for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesRightDB.begin(),
01893   iend=d_inequalitiesRightDB.end(); i!=iend; ++i) {
01894     delete (i->second);
01895     free(i->second);
01896   }
01897   for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesLeftDB.begin(),
01898   iend=d_inequalitiesLeftDB.end(); i!=iend; ++i) {
01899     delete (i->second);
01900     free (i->second);
01901   }
01902 }
01903 
01904 void TheoryArith3::collectVars(const Expr& e, vector<Expr>& vars,
01905             set<Expr>& cache) {
01906   // Check the cache first
01907   if(cache.count(e) > 0) return;
01908   // Not processed yet.  Cache the expression and proceed
01909   cache.insert(e);
01910   if(isLeaf(e)) vars.push_back(e);
01911   else
01912     for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
01913       collectVars(*i, vars, cache);
01914 }
01915 
01916 void
01917 TheoryArith3::processFiniteInterval(const Theorem& alphaLEax,
01918            const Theorem& bxLEbeta) {
01919   const Expr& ineq1(alphaLEax.getExpr());
01920   const Expr& ineq2(bxLEbeta.getExpr());
01921   DebugAssert(isLE(ineq1), "TheoryArith3::processFiniteInterval: ineq1 = "
01922         +ineq1.toString());
01923   DebugAssert(isLE(ineq2), "TheoryArith3::processFiniteInterval: ineq2 = "
01924         +ineq2.toString());
01925   // If the inequalities are not integer, just return (nothing to do)
01926   if(!isInteger(ineq1[0])
01927      || !isInteger(ineq1[1])
01928      || !isInteger(ineq2[0])
01929      || !isInteger(ineq2[1]))
01930     return;
01931 
01932   const Expr& ax = ineq1[1];
01933   const Expr& bx = ineq2[0];
01934   DebugAssert(!isPlus(ax) && !isRational(ax),
01935         "TheoryArith3::processFiniteInterval:\n ax = "+ax.toString());
01936   DebugAssert(!isPlus(bx) && !isRational(bx),
01937         "TheoryArith3::processFiniteInterval:\n bx = "+bx.toString());
01938   Expr a = isMult(ax)? ax[0] : rat(1);
01939   Expr b = isMult(bx)? bx[0] : rat(1);
01940 
01941   Theorem thm1(alphaLEax), thm2(bxLEbeta);
01942   // Multiply the inequalities by 'b' and 'a', and canonize them, if necessary
01943   if(a != b) {
01944     thm1 = canonPred(iffMP(alphaLEax, d_rules->multIneqn(ineq1, b)));
01945     thm2 = canonPred(iffMP(bxLEbeta, d_rules->multIneqn(ineq2, a)));
01946   }
01947   // Check that a*beta - b*alpha == c > 0
01948   const Expr& alphaLEt = thm1.getExpr();
01949   const Expr& alpha = alphaLEt[0];
01950   const Expr& t = alphaLEt[1];
01951   const Expr& beta = thm2.getExpr()[1];
01952   Expr c = canon(beta - alpha).getRHS();
01953 
01954   if(c.isRational() && c.getRational() >= 1) {
01955     // This is a finite interval.  First, derive t <= alpha + c:
01956     // canon(alpha+c) => (alpha+c == beta) ==> [symmetry] beta == alpha+c
01957     // Then substitute that in thm2
01958     Theorem bEQac = symmetryRule(canon(alpha + c));
01959     // Substitute beta == alpha+c for the second child of thm2
01960     vector<unsigned> changed;
01961     vector<Theorem> thms;
01962     changed.push_back(1);
01963     thms.push_back(bEQac);
01964     Theorem tLEac = substitutivityRule(thm2.getExpr(), changed, thms);
01965     tLEac = iffMP(thm2, tLEac);
01966     // Derive and enqueue the finite interval constraint
01967     Theorem isInta(isIntegerThm(alpha));
01968     Theorem isIntt(isIntegerThm(t));
01969     enqueueFact(d_rules->finiteInterval(thm1, tLEac, isInta, isIntt));
01970   }
01971 }
01972 
01973 
01974 void
01975 TheoryArith3::processFiniteIntervals(const Expr& x) {
01976   // If x is not integer, do not bother
01977   if(!isInteger(x)) return;
01978   // Process every pair of the opposing inequalities for 'x'
01979   ExprMap<CDList<Ineq> *>::iterator iLeft, iRight;
01980   iLeft = d_inequalitiesLeftDB.find(x);
01981   if(iLeft == d_inequalitiesLeftDB.end()) return;
01982   iRight = d_inequalitiesRightDB.find(x);
01983   if(iRight == d_inequalitiesRightDB.end()) return;
01984   // There are some opposing inequalities; get the lists
01985   CDList<Ineq>& ineqsLeft = *(iLeft->second);
01986   CDList<Ineq>& ineqsRight = *(iRight->second);
01987   // Get the sizes of the lists
01988   size_t sizeLeft = ineqsLeft.size();
01989   size_t sizeRight = ineqsRight.size();
01990   // Process all the pairs of the opposing inequalities
01991   for(size_t l=0; l<sizeLeft; ++l)
01992     for(size_t r=0; r<sizeRight; ++r)
01993       processFiniteInterval(ineqsRight[r], ineqsLeft[l]);
01994 }
01995 
01996 /*! This function recursively decends expression tree <strong>without
01997  *  caching</strong> until it hits a node that is already setup.  Be
01998  *  careful on what expressions you are calling it.
01999  */
02000 void
02001 TheoryArith3::setupRec(const Expr& e) {
02002   if(e.hasFind()) return;
02003   // First, set up the kids recursively
02004   for (int k = 0; k < e.arity(); ++k) {
02005     setupRec(e[k]);
02006   }
02007   // Create a find pointer for e
02008   e.setFind(reflexivityRule(e));
02009   e.setEqNext(reflexivityRule(e));
02010   // And call our own setup()
02011   setup(e);
02012 }
02013 
02014 
02015 void TheoryArith3::addSharedTerm(const Expr& e) {
02016   d_sharedTerms[e] = true;
02017 }
02018 
02019 
02020 void TheoryArith3::assertFact(const Theorem& e)
02021 {
02022   TRACE("arith assert", "assertFact(", e.getExpr().toString(), ")");
02023   const Expr& expr = e.getExpr();
02024   if (expr.isNot() && expr[0].isEq()) {
02025     IF_DEBUG(debugger.counter("[arith] received disequalities")++;)
02026     d_diseq.push_back(e);
02027   }
02028   else if (!expr.isEq()){
02029     if (expr.isNot()) {
02030       // This can only be negation of dark or gray shadows, or
02031       // disequalities, which we ignore.  Negations of inequalities
02032       // are handled in rewrite, we don't even receive them here.
02033     }
02034     else if(isDarkShadow(expr)) {
02035       enqueueFact(d_rules->expandDarkShadow(e));
02036       IF_DEBUG(debugger.counter("received DARK_SHADOW")++;)
02037     }
02038     else if(isGrayShadow(expr)) {
02039       IF_DEBUG(debugger.counter("received GRAY_SHADOW")++;)
02040       const Rational& c1 = expr[2].getRational();
02041       const Rational& c2 = expr[3].getRational();
02042       const Expr& v = expr[0];
02043       const Expr& ee = expr[1];
02044       if(c1 == c2)
02045   enqueueFact(d_rules->expandGrayShadow0(e));
02046       else {
02047   Theorem gThm(e);
02048   // Check if we can reduce the number of cases in G(ax,c,c1,c2)
02049   if(ee.isRational() && isMult(v)
02050      && v[0].isRational() && v[0].getRational() >= 2) {
02051     IF_DEBUG(debugger.counter("reduced const GRAY_SHADOW")++;)
02052     gThm = d_rules->grayShadowConst(e);
02053   }
02054   // (Possibly) new gray shadow
02055   const Expr& g = gThm.getExpr();
02056   if(g.isFalse())
02057     setInconsistent(gThm);
02058   else if(g[2].getRational() == g[3].getRational())
02059     enqueueFact(d_rules->expandGrayShadow0(gThm));
02060   else {
02061     // Assert c1+e <= v <= c2+e
02062     enqueueFact(d_rules->expandGrayShadow(gThm));
02063     // Split G into 2 cases (binary search b/w c1 and c2)
02064     Theorem thm2 = d_rules->splitGrayShadow(gThm);
02065     enqueueFact(thm2);
02066     // Fetch the two gray shadows
02067     DebugAssert(thm2.getExpr().isAnd() && thm2.getExpr().arity()==2,
02068           "thm2 = "+thm2.getExpr().toString());
02069     const Expr& G1orG2 = thm2.getExpr()[0];
02070     DebugAssert(G1orG2.isOr() && G1orG2.arity()==2,
02071           "G1orG2 = "+G1orG2.toString());
02072     const Expr& G1 = G1orG2[0];
02073     const Expr& G2 = G1orG2[1];
02074     DebugAssert(G1.getKind()==GRAY_SHADOW, "G1 = "+G1.toString());
02075     DebugAssert(G2.getKind()==GRAY_SHADOW, "G2 = "+G2.toString());
02076     // Split on the left disjunct first (keep the priority low)
02077           Expr tmp = simplifyExpr(G1);
02078           if (!tmp.isBoolConst())
02079             addSplitter(tmp, 1);
02080           tmp = simplifyExpr(G2);
02081     if (!tmp.isBoolConst())
02082             addSplitter(tmp, -1);
02083   }
02084       }
02085     }
02086     else {
02087       DebugAssert(isLE(expr) || isLT(expr) || isIntPred(expr),
02088       "expected LE or LT: "+expr.toString());
02089       if(isLE(expr) || isLT(expr)) {
02090   IF_DEBUG(debugger.counter("recevied inequalities")++;)
02091 
02092         // Assert the equivalent negated inequality
02093         Theorem thm;
02094         if (isLE(expr)) thm = d_rules->negatedInequality(!gtExpr(expr[0],expr[1]));
02095         else thm = d_rules->negatedInequality(!geExpr(expr[0],expr[1]));
02096         thm = symmetryRule(thm);
02097         Theorem thm2 = simplify(thm.getRHS()[0]);
02098         DebugAssert(thm2.getLHS() != thm2.getRHS(), "Expected rewrite");
02099         thm2 = getCommonRules()->substitutivityRule(thm.getRHS(), thm2);
02100         thm = transitivityRule(thm, thm2);
02101         enqueueFact(iffMP(e, thm));
02102 
02103   // Buffer the inequality
02104   addToBuffer(e);
02105 
02106   TRACE("arith ineq", "buffer.size() = ", d_buffer.size(),
02107         ", index="+int2string(d_bufferIdx)
02108         +", threshold="+int2string(*d_bufferThres));
02109 
02110   if((((int)d_buffer.size()) - (int)d_bufferIdx > *d_bufferThres)
02111      && !d_inModelCreation)
02112     processBuffer();
02113       } else {
02114   IF_DEBUG(debugger.counter("arith IS_INTEGER")++;)
02115       }
02116     }
02117   }
02118   else {
02119     IF_DEBUG(debugger.counter("[arith] received t1=t2")++;)
02120   }
02121 }
02122 
02123 
02124 void TheoryArith3::checkSat(bool fullEffort)
02125 {
02126   //  vector<Expr>::const_iterator e;
02127   //  vector<Expr>::const_iterator eEnd;
02128   // TODO: convert back to use iterators
02129   TRACE("arith checksat", "checksat(", fullEffort? "true" : "false", ")");
02130   TRACE("arith ineq", "TheoryArith3::checkSat(fullEffort=",
02131         fullEffort? "true" : "false", ")");
02132   if (fullEffort) {
02133     while(!inconsistent() && d_bufferIdx < d_buffer.size())
02134       processBuffer();
02135     if(d_inModelCreation) {
02136       for(; d_diseqIdx < d_diseq.size(); d_diseqIdx = d_diseqIdx+1) {
02137   TRACE("model", "[arith] refining diseq: ",
02138         d_diseq[d_diseqIdx].getExpr() , "");
02139   enqueueFact(d_rules->diseqToIneq(d_diseq[d_diseqIdx]));
02140       }
02141     }
02142   }
02143 }
02144 
02145 
02146 
02147 void TheoryArith3::refineCounterExample()
02148 {
02149   d_inModelCreation = true;
02150   TRACE("model", "refineCounterExample[TheoryArith3] ", "", "{");
02151   CDMap<Expr, bool>::iterator it = d_sharedTerms.begin(), it2,
02152     iend = d_sharedTerms.end();
02153   // Add equalities over all pairs of shared terms as suggested
02154   // splitters.  Notice, that we want to split on equality
02155   // (positively) first, to reduce the size of the model.
02156   for(; it!=iend; ++it) {
02157     // Copy by value: the elements in the pair from *it are NOT refs in CDMap
02158     Expr e1 = (*it).first;
02159     for(it2 = it, ++it2; it2!=iend; ++it2) {
02160       Expr e2 = (*it2).first;
02161       DebugAssert(isReal(getBaseType(e1)),
02162       "TheoryArith3::refineCounterExample: e1 = "+e1.toString()
02163       +"\n type(e1) = "+e1.getType().toString());
02164       if(findExpr(e1) != findExpr(e2)) {
02165   DebugAssert(isReal(getBaseType(e2)),
02166         "TheoryArith3::refineCounterExample: e2 = "+e2.toString()
02167         +"\n type(e2) = "+e2.getType().toString());
02168   Expr eq = simplifyExpr(e1.eqExpr(e2));
02169         if (!eq.isBoolConst())
02170           addSplitter(eq);
02171       }
02172     }
02173   }
02174   TRACE("model", "refineCounterExample[Theory::Arith] ", "", "}");
02175 }
02176 
02177 
02178 void
02179 TheoryArith3::findRationalBound(const Expr& varSide, const Expr& ratSide,
02180              const Expr& var,
02181              Rational &r)
02182 {
02183   Expr c, x;
02184   separateMonomial(varSide, c, x);
02185 
02186   DebugAssert(findExpr(c).isRational(),
02187         "seperateMonomial failed");
02188   DebugAssert(findExpr(ratSide).isRational(),
02189         "smallest variable in graph, should not have variables"
02190         " in inequalities: ");
02191   DebugAssert(x == var, "separateMonomial found different variable: "
02192         + var.toString());
02193   r = findExpr(ratSide).getRational() / findExpr(c).getRational();
02194 }
02195 
02196 bool
02197 TheoryArith3::findBounds(const Expr& e, Rational& lub, Rational&  glb)
02198 {
02199   bool strictLB=false, strictUB=false;
02200   bool right = (d_inequalitiesRightDB.count(e) > 0
02201            && d_inequalitiesRightDB[e]->size() > 0);
02202   bool left = (d_inequalitiesLeftDB.count(e) > 0
02203          && d_inequalitiesLeftDB[e]->size() > 0);
02204   int numRight = 0, numLeft = 0;
02205   if(right) { //rationals less than e
02206     CDList<Ineq> * ratsLTe = d_inequalitiesRightDB[e];
02207     for(unsigned int i=0; i<ratsLTe->size(); i++) {
02208       DebugAssert((*ratsLTe)[i].varOnRHS(), "variable on wrong side!");
02209       Expr ineq = (*ratsLTe)[i].ineq().getExpr();
02210       Expr leftSide = ineq[0], rightSide = ineq[1];
02211       Rational r;
02212       findRationalBound(rightSide, leftSide, e , r);
02213       if(numRight==0 || r>glb){
02214   glb = r;
02215   strictLB = isLT(ineq);
02216       }
02217       numRight++;
02218     }
02219     TRACE("model", "   =>Lower bound ", glb.toString(), "");
02220   }
02221   if(left) {   //rationals greater than e
02222     CDList<Ineq> * ratsGTe = d_inequalitiesLeftDB[e];
02223     for(unsigned int i=0; i<ratsGTe->size(); i++) {
02224       DebugAssert((*ratsGTe)[i].varOnLHS(), "variable on wrong side!");
02225       Expr ineq = (*ratsGTe)[i].ineq().getExpr();
02226       Expr leftSide = ineq[0], rightSide = ineq[1];
02227       Rational r;
02228       findRationalBound(leftSide, rightSide, e, r);
02229       if(numLeft==0 || r<lub) {
02230   lub = r;
02231   strictUB = isLT(ineq);
02232       }
02233       numLeft++;
02234     }
02235     TRACE("model", "   =>Upper bound ", lub.toString(), "");
02236   }
02237   if(!left && !right) {
02238       lub = 0;
02239       glb = 0;
02240   }
02241   if(!left && right) {lub = glb +2;}
02242   if(!right && left)  {glb =  lub-2;}
02243   DebugAssert(glb <= lub, "Greatest lower bound needs to be smaller "
02244         "than least upper bound");
02245   return strictLB;
02246 }
02247 
02248 void TheoryArith3::assignVariables(std::vector<Expr>&v)
02249 {
02250   int count = 0;
02251   while (v.size() > 0) {
02252     std::vector<Expr> bottom;
02253     d_graph.selectSmallest(v, bottom);
02254     TRACE("model", "Finding variables to assign. Iteration # ", count, "");
02255     for(unsigned int i = 0; i<bottom.size(); i++) {
02256       Expr e = bottom[i];
02257       TRACE("model", "Found: ", e, "");
02258       // Check if it is already a concrete constant
02259       if(e.isRational()) continue;
02260 
02261       Rational lub, glb;
02262       bool strictLB;
02263       strictLB = findBounds(e, lub, glb);
02264       Rational mid;
02265       if(isInteger(e)) {
02266   if(strictLB && glb.isInteger())
02267     mid = glb + 1;
02268   else
02269     mid = ceil(glb);
02270       }
02271       else
02272   mid = (lub + glb)/2;
02273       TRACE("model", "Assigning mid = ", mid, " {");
02274       assignValue(e, rat(mid));
02275       TRACE("model", "Assigned find(e) = ", findExpr(e), " }");
02276       if(inconsistent()) return; // Punt immediately if failed
02277     }
02278     count++;
02279   }
02280 }
02281 
02282 void TheoryArith3::computeModelBasic(const std::vector<Expr>& v)
02283 {
02284   d_inModelCreation = true;
02285   vector<Expr> reps;
02286   TRACE("model", "Arith=>computeModel ", "", "{");
02287   for(unsigned int i=0; i <v.size(); ++i) {
02288     const Expr& e = v[i];
02289     if(findExpr(e) == e) {
02290       TRACE("model", "arith variable:", e , "");
02291       reps.push_back(e);
02292     }
02293     else {
02294       TRACE("model", "arith variable:", e , "");
02295       TRACE("model", " ==> is defined by: ", findExpr(e) , "");
02296     }
02297   }
02298   assignVariables(reps);
02299   TRACE("model", "Arith=>computeModel", "", "}");
02300   d_inModelCreation = false;
02301 }
02302 
02303 // For any arith expression 'e', if the subexpressions are assigned
02304 // concrete values, then find(e) must already be a concrete value.
02305 void TheoryArith3::computeModel(const Expr& e, vector<Expr>& vars) {
02306   DebugAssert(findExpr(e).isRational(), "TheoryArith3::computeModel("
02307         +e.toString()+")\n e is not assigned concrete value.\n"
02308         +" find(e) = "+findExpr(e).toString());
02309   assignValue(simplify(e));
02310   vars.push_back(e);
02311 }
02312 
02313 
02314 
02315 /*! accepts a rewrite theorem over eqn|ineqn and normalizes it
02316  *  and returns a theorem to that effect. assumes e is non-trivial
02317  *  i.e. e is not '0=const' or 'const=0' or '0 <= const' etc.
02318  */
02319 Theorem TheoryArith3::normalize(const Expr& e) {
02320   //e is an eqn or ineqn. e is not a trivial eqn or ineqn
02321   //trivial means 0 = const or 0 <= const.
02322   TRACE("arith", "normalize(", e, ") {");
02323   DebugAssert(e.isEq() || isIneq(e),
02324         "normalize: input must be Eq or Ineq: " + e.toString());
02325   DebugAssert(!isIneq(e) || (0 == e[0].getRational()),
02326         "normalize: if (e is ineq) then e[0] must be 0" +
02327         e.toString());
02328   if(e.isEq()) {
02329     if(e[0].isRational()) {
02330       DebugAssert(0 == e[0].getRational(),
02331       "normalize: if e is Eq and e[0] is rat then e[0]==0");
02332     }
02333     else {
02334       //if e[0] is not rational then e[1] must be rational.
02335       DebugAssert(e[1].isRational() && 0 == e[1].getRational(),
02336       "normalize: if e is Eq and e[1] is rat then e[1]==0\n"
02337       " e = "+e.toString());
02338     }
02339   }
02340 
02341   Expr factor;
02342   if(e[0].isRational())
02343     factor = computeNormalFactor(e[1]);
02344   else
02345     factor = computeNormalFactor(e[0]);
02346 
02347   TRACE("arith", "normalize: factor = ", factor, "");
02348   DebugAssert(factor.getRational() > 0,
02349               "normalize: factor="+ factor.toString());
02350 
02351   Theorem thm(reflexivityRule(e));
02352   // Now multiply the equality by the factor, unless it is 1
02353   if(factor.getRational() != 1) {
02354     int kind = e.getKind();
02355     switch(kind) {
02356     case EQ:
02357       thm = d_rules->multEqn(e[0], e[1], factor);
02358       // And canonize the result
02359       thm = canonPredEquiv(thm);
02360       break;
02361     case LE:
02362     case LT:
02363     case GE:
02364     case GT:
02365       thm = d_rules->multIneqn(e, factor);
02366       // And canonize the result
02367       thm = canonPredEquiv(thm);
02368       break;
02369     default:
02370       // MS .net doesn't accept "..." + int
02371       ostringstream ss;
02372       ss << "normalize: control should not reach here " << kind;
02373       DebugAssert(false, ss.str());
02374       break;
02375     }
02376   }
02377   TRACE("arith", "normalize => ", thm, " }");
02378   return(thm);
02379 }
02380 
02381 
02382 Theorem TheoryArith3::normalize(const Theorem& eIffEqn) {
02383   return transitivityRule(eIffEqn, normalize(eIffEqn.getRHS()));
02384 }
02385 
02386 
02387 Theorem TheoryArith3::rewrite(const Expr& e)
02388 {
02389   DebugAssert(leavesAreSimp(e), "Expected leaves to be simplified");
02390   TRACE("arith", "TheoryArith3::rewrite(", e, ") {");
02391   Theorem thm;
02392   if (!e.isTerm()) {
02393     if (!e.isAbsLiteral()) {
02394       e.setRewriteNormal();
02395       thm = reflexivityRule(e);
02396       TRACE("arith", "TheoryArith3::rewrite[non-literal] => ", thm, " }");
02397       return thm;
02398     }
02399     switch(e.getKind()) {
02400     case EQ:
02401     {
02402       // canonical form for an equality of two leaves
02403       // is just l == r instead of 0 + (-1 * l) + r = 0.
02404       if (isLeaf(e[0]) && isLeaf(e[1]))
02405   thm = reflexivityRule(e);
02406       else { // Otherwise, it is "lhs = 0"
02407   //first convert e to the form 0=e'
02408   if((e[0].isRational() && e[0].getRational() == 0)
02409      || (e[1].isRational() && e[1].getRational() == 0))
02410     //already in 0=e' or e'=0 form
02411     thm = reflexivityRule(e);
02412   else {
02413     thm = d_rules->rightMinusLeft(e);
02414     thm = canonPredEquiv(thm);
02415   }
02416   // Check for trivial equation
02417   if ((thm.getRHS())[0].isRational() && (thm.getRHS())[1].isRational()) {
02418     thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
02419   } else {
02420     //else equation is non-trivial
02421     thm = normalize(thm);
02422     // Normalization may yield non-simplified terms
02423     thm = canonPredEquiv(thm);
02424 
02425   }
02426       }
02427 
02428       // Equations must be oriented such that lhs >= rhs as Exprs;
02429       // this ordering is given by operator<(Expr,Expr).
02430       const Expr& eq = thm.getRHS();
02431       if(eq.isEq() && eq[0] < eq[1])
02432   thm = transitivityRule(thm, getCommonRules()->rewriteUsingSymmetry(eq));
02433     }
02434     break;
02435     case GRAY_SHADOW:
02436     case DARK_SHADOW:
02437       thm = reflexivityRule(e);
02438       break;
02439     case IS_INTEGER: {
02440       Theorem res(isIntegerDerive(e, typePred(e[0])));
02441       if(!res.isNull())
02442   thm = getCommonRules()->iffTrue(res);
02443       else
02444   thm = reflexivityRule(e);
02445       break;
02446     }
02447     case NOT:
02448       if (!isIneq(e[0]))
02449   //in this case we have "NOT of DARK or GRAY_SHADOW."
02450   thm = reflexivityRule(e);
02451       else {
02452   //In this case we have the "NOT of ineq". get rid of NOT
02453   //and then treat like an ineq
02454   thm = d_rules->negatedInequality(e);
02455   DebugAssert(isGE(thm.getRHS()) || isGT(thm.getRHS()),
02456         "Expected GE or GT");
02457   thm = transitivityRule(thm, d_rules->flipInequality(thm.getRHS()));
02458   thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
02459   thm = canonPredEquiv(thm);
02460 
02461   // Check for trivial inequation
02462   if ((thm.getRHS())[1].isRational())
02463     thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
02464   else {
02465     //else ineq is non-trivial
02466     thm = normalize(thm);
02467     // Normalization may yield non-simplified terms
02468     thm = canonPredEquiv(thm);
02469   }
02470       }
02471       break;
02472     case LE:
02473     case LT:
02474     case GE:
02475     case GT:
02476       if (isGE(e) || isGT(e)) {
02477   thm = d_rules->flipInequality(e);
02478   thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
02479       }
02480       else
02481   thm = d_rules->rightMinusLeft(e);
02482       thm = canonPredEquiv(thm);
02483 
02484       // Check for trivial inequation
02485       if ((thm.getRHS())[1].isRational())
02486   thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
02487       else { // ineq is non-trivial
02488   thm = normalize(thm);
02489   thm = canonPredEquiv(thm);
02490       }
02491       break;
02492     default:
02493       DebugAssert(false,
02494       "Theory_Arith::rewrite: control should not reach here");
02495       break;
02496     }
02497   }
02498   else {
02499     if (e.isAtomic())
02500       thm = canon(e);
02501     else
02502       thm = reflexivityRule(e);
02503   }
02504   // Arith canonization is idempotent
02505   if (theoryOf(thm.getRHS()) == this)
02506     thm.getRHS().setRewriteNormal();
02507   TRACE("arith", "TheoryArith3::rewrite => ", thm, " }");
02508   return thm;
02509 }
02510 
02511 
02512 void TheoryArith3::setup(const Expr& e)
02513 {
02514   if (!e.isTerm()) {
02515     if (e.isNot() || e.isEq() || isDarkShadow(e) || isGrayShadow(e)) return;
02516     if(e.getKind() == IS_INTEGER) {
02517       e[0].addToNotify(this, e);
02518       return;
02519     }
02520     DebugAssert((isLT(e)||isLE(e)) &&
02521                 e[0].isRational() && e[0].getRational() == 0,
02522                 "TheoryArith3::setup: expected 0 < rhs:" + e.toString());
02523     e[1].addToNotify(this, e);
02524     return;
02525   }
02526   int k(0), ar(e.arity());
02527   for ( ; k < ar; ++k) {
02528     e[k].addToNotify(this, e);
02529     TRACE("arith setup", "e["+int2string(k)+"]: ", *(e[k].getNotify()), "");
02530   }
02531 }
02532 
02533 
02534 void TheoryArith3::update(const Theorem& e, const Expr& d)
02535 {
02536   if (inconsistent()) return;
02537   IF_DEBUG(debugger.counter("arith update total")++;)
02538   if (!d.hasFind()) return;
02539   if (isIneq(d)) {
02540     // Substitute e[1] for e[0] in d and enqueue new inequality
02541     DebugAssert(e.getLHS() == d[1], "Mismatch");
02542     Theorem thm = find(d);
02543     //    DebugAssert(thm.getRHS() == trueExpr(), "Expected find = true");
02544     vector<unsigned> changed;
02545     vector<Theorem> children;
02546     changed.push_back(1);
02547     children.push_back(e);
02548     Theorem thm2 = substitutivityRule(d, changed, children);
02549     if (thm.getRHS() == trueExpr()) {
02550       enqueueFact(iffMP(getCommonRules()->iffTrueElim(thm), thm2));
02551     }
02552     else {
02553       enqueueFact(getCommonRules()->iffFalseElim(
02554         transitivityRule(symmetryRule(thm2), thm)));
02555     }
02556     IF_DEBUG(debugger.counter("arith update ineq")++;)
02557   }
02558   else if (find(d).getRHS() == d) {
02559     Theorem thm = canonSimp(d);
02560     TRACE("arith", "TheoryArith3::update(): thm = ", thm, "");
02561     DebugAssert(leavesAreSimp(thm.getRHS()), "updateHelper error: "
02562     +thm.getExpr().toString());
02563     assertEqualities(transitivityRule(thm, rewrite(thm.getRHS())));
02564     IF_DEBUG(debugger.counter("arith update find(d)=d")++;)
02565   }
02566 }
02567 
02568 
02569 Theorem TheoryArith3::solve(const Theorem& thm)
02570 {
02571   DebugAssert(thm.isRewrite() && thm.getLHS().isTerm(), "");
02572   const Expr& lhs = thm.getLHS();
02573   const Expr& rhs = thm.getRHS();
02574 
02575   // Check for already solved equalities.
02576 
02577   // Have to be careful about the types: integer variable cannot be
02578   // assigned a real term.  Also, watch for e[0] being a subexpression
02579   // of e[1]: this would create an unsimplifiable expression.
02580   if (isLeaf(lhs) && !isLeafIn(lhs, rhs)
02581       && (lhs.getType() != intType() || isInteger(rhs))
02582       // && !e[0].subExprOf(e[1])
02583       )
02584     return thm;
02585 
02586   // Symmetric version is already solved
02587   if (isLeaf(rhs) && !isLeafIn(rhs, lhs)
02588       && (rhs.getType() != intType() || isInteger(lhs))
02589       // && !e[1].subExprOf(e[0])
02590       )
02591     return symmetryRule(thm);
02592 
02593   return doSolve(thm);
02594 }
02595 
02596 
02597 void TheoryArith3::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
02598   switch(e.getKind()) {
02599   case RATIONAL_EXPR: // Skip the constants
02600     break;
02601   case PLUS:
02602   case MULT:
02603   case DIVIDE:
02604   case POW: // This is not a variable; extract the variables from children
02605     for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
02606       // getModelTerm(*i, v);
02607       v.push_back(*i);
02608     break;
02609   default: { // Otherwise it's a variable.  Check if it has a find pointer
02610     Expr e2(findExpr(e));
02611     if(e==e2) {
02612       TRACE("model", "TheoryArith3::computeModelTerm(", e, "): a variable");
02613       // Leave it alone (it has no descendants)
02614       // v.push_back(e);
02615     } else {
02616       TRACE("model", "TheoryArith3::computeModelTerm("+e.toString()
02617       +"): has find pointer to ", e2, "");
02618       v.push_back(e2);
02619     }
02620   }
02621   }
02622 }
02623 
02624 
02625 Expr TheoryArith3::computeTypePred(const Type& t, const Expr& e) {
02626   Expr tExpr = t.getExpr();
02627   switch(tExpr.getKind()) {
02628   case INT:
02629     return Expr(IS_INTEGER, e);
02630   case SUBRANGE: {
02631     std::vector<Expr> kids;
02632     kids.push_back(Expr(IS_INTEGER, e));
02633     kids.push_back(leExpr(tExpr[0], e));
02634     kids.push_back(leExpr(e, tExpr[1]));
02635     return andExpr(kids);
02636   }
02637   default:
02638     return e.getEM()->trueExpr();
02639   }
02640 }
02641 
02642 
02643 void TheoryArith3::checkAssertEqInvariant(const Theorem& e)
02644 {
02645   if (e.isRewrite()) {
02646     DebugAssert(e.getLHS().isTerm(), "Expected equation");
02647     if (isLeaf(e.getLHS())) {
02648       // should be in solved form
02649       DebugAssert(!isLeafIn(e.getLHS(),e.getRHS()),
02650                   "Not in solved form: lhs appears in rhs");
02651     }
02652     else {
02653       DebugAssert(e.getLHS().hasFind(), "Expected lhs to have find");
02654       DebugAssert(!leavesAreSimp(e.getLHS()),
02655                   "Expected at least one unsimplified leaf on lhs");
02656     }
02657     DebugAssert(canonSimp(e.getRHS()).getRHS() == e.getRHS(),
02658                 "Expected canonSimp(rhs) = canonSimp(rhs)");
02659   }
02660   else {
02661     Expr expr = e.getExpr();
02662     if (expr.isFalse()) return;
02663 
02664     vector<Theorem> eqs;
02665     Theorem thm;
02666     int index, index2;
02667 
02668     for (index = 0; index < expr.arity(); ++index) {
02669       thm = getCommonRules()->andElim(e, index);
02670       eqs.push_back(thm);
02671       if (thm.getExpr().isFalse()) return;
02672       DebugAssert(eqs[index].isRewrite() &&
02673                   eqs[index].getLHS().isTerm(), "Expected equation");
02674     }
02675 
02676     // Check for solved form
02677     for (index = 0; index < expr.arity(); ++index) {
02678       DebugAssert(isLeaf(eqs[index].getLHS()), "expected leaf on lhs");
02679       DebugAssert(canonSimp(eqs[index].getRHS()).getRHS() == eqs[index].getRHS(),
02680                   "Expected canonSimp(rhs) = canonSimp(rhs)");
02681       DebugAssert(recursiveCanonSimpCheck(eqs[index].getRHS()),
02682                   "Failed recursive canonSimp check");
02683       for (index2 = 0; index2 < expr.arity(); ++index2) {
02684         DebugAssert(index == index2 ||
02685                     eqs[index].getLHS() != eqs[index2].getLHS(),
02686                     "Not in solved form: repeated lhs");
02687         DebugAssert(!isLeafIn(eqs[index].getLHS(),eqs[index2].getRHS()),
02688                     "Not in solved form: lhs appears in rhs");
02689       }
02690     }
02691   }
02692 }
02693 
02694 
02695 void TheoryArith3::checkType(const Expr& e)
02696 {
02697   switch (e.getKind()) {
02698     case INT:
02699     case REAL:
02700       if (e.arity() > 0) {
02701         throw Exception("Ill-formed arithmetic type: "+e.toString());
02702       }
02703       break;
02704     case SUBRANGE:
02705       if (e.arity() != 2 ||
02706           !isIntegerConst(e[0]) ||
02707           !isIntegerConst(e[1]) ||
02708           e[0].getRational() > e[1].getRational()) {
02709         throw Exception("bad SUBRANGE type expression"+e.toString());
02710       }
02711       break;
02712     default:
02713       DebugAssert(false, "Unexpected kind in TheoryArith3::checkType"
02714                   +getEM()->getKindName(e.getKind()));
02715   }
02716 }
02717 
02718 
02719 Cardinality TheoryArith3::finiteTypeInfo(Expr& e, Unsigned& n,
02720                                            bool enumerate, bool computeSize)
02721 {
02722   Cardinality card = CARD_INFINITE;
02723   switch (e.getKind()) {
02724     case SUBRANGE: {
02725       card = CARD_FINITE;
02726       Expr typeExpr = e;
02727       if (enumerate) {
02728         Rational r = typeExpr[0].getRational() + n;
02729         if (r <= typeExpr[1].getRational()) {
02730           e = rat(r);
02731         }
02732         else e = Expr();
02733       }
02734       if (computeSize) {
02735         Rational r = typeExpr[1].getRational() - typeExpr[0].getRational() + 1;
02736         n = r.getUnsigned();
02737       }
02738       break;
02739     }
02740     default:
02741       break;
02742   }
02743   return card;
02744 }
02745 
02746 
02747 void TheoryArith3::computeType(const Expr& e)
02748 {
02749   switch (e.getKind()) {
02750     case REAL_CONST:
02751       e.setType(d_realType);
02752       break;
02753     case RATIONAL_EXPR:
02754       if(e.getRational().isInteger())
02755         e.setType(d_intType);
02756       else
02757         e.setType(d_realType);
02758       break;
02759     case UMINUS:
02760     case PLUS:
02761     case MINUS:
02762     case MULT:
02763     case POW: {
02764       bool isInt = true;
02765       for(int k = 0; k < e.arity(); ++k) {
02766         if(d_realType != getBaseType(e[k]))
02767           throw TypecheckException("Expecting type REAL with `" +
02768                                    getEM()->getKindName(e.getKind()) + "',\n"+
02769                                    "but got a " + getBaseType(e[k]).toString()+
02770                                    " for:\n" + e.toString());
02771         if(isInt && !isInteger(e[k]))
02772           isInt = false;
02773       }
02774       if(isInt)
02775         e.setType(d_intType);
02776       else
02777         e.setType(d_realType);
02778       break;
02779     }
02780     case DIVIDE: {
02781       Expr numerator = e[0];
02782       Expr denominator = e[1];
02783       if (getBaseType(numerator) != d_realType ||
02784           getBaseType(denominator) != d_realType) {
02785         throw TypecheckException("Expecting only REAL types with `DIVIDE',\n"
02786                                  "but got " + getBaseType(numerator).toString()+
02787                                  " and " + getBaseType(denominator).toString() +
02788                                  " for:\n" + e.toString());
02789       }
02790       if(denominator.isRational() && 1 == denominator.getRational())
02791         e.setType(numerator.getType());
02792       else
02793         e.setType(d_realType);
02794       break;
02795     }
02796     case LT:
02797     case LE:
02798     case GT:
02799     case GE:
02800     case GRAY_SHADOW:
02801       // Need to know types for all exprs -Clark
02802       //    e.setType(boolType());
02803       //    break;
02804     case DARK_SHADOW:
02805       for (int k = 0; k < e.arity(); ++k) {
02806         if (d_realType != getBaseType(e[k]))
02807           throw TypecheckException("Expecting type REAL with `" +
02808                                    getEM()->getKindName(e.getKind()) + "',\n"+
02809                                    "but got a " + getBaseType(e[k]).toString()+
02810                                    " for:\n" + e.toString());
02811       }
02812 
02813       e.setType(boolType());
02814       break;
02815     case IS_INTEGER:
02816       if(d_realType != getBaseType(e[0]))
02817         throw TypecheckException("Expected type REAL, but got "
02818                                  +getBaseType(e[0]).toString()
02819                                  +"\n\nExpr = "+e.toString());
02820       e.setType(boolType());
02821       break;
02822     default:
02823       DebugAssert(false,"TheoryArith3::computeType: unexpected expression:\n "
02824                   +e.toString());
02825       break;
02826   }
02827 }
02828 
02829 
02830 Type TheoryArith3::computeBaseType(const Type& t) {
02831   IF_DEBUG(int kind = t.getExpr().getKind();)
02832   DebugAssert(kind==INT || kind==REAL || kind==SUBRANGE,
02833         "TheoryArith3::computeBaseType("+t.toString()+")");
02834   return realType();
02835 }
02836 
02837 
02838 Expr
02839 TheoryArith3::computeTCC(const Expr& e) {
02840   Expr tcc(Theory::computeTCC(e));
02841   switch(e.getKind()) {
02842   case DIVIDE:
02843     DebugAssert(e.arity() == 2, "");
02844     return tcc.andExpr(!(e[1].eqExpr(rat(0))));
02845   default:
02846     return tcc;
02847   }
02848 }
02849 
02850 ///////////////////////////////////////////////////////////////////////////////
02851 //parseExprOp:
02852 //translating special Exprs to regular EXPR??
02853 ///////////////////////////////////////////////////////////////////////////////
02854 Expr
02855 TheoryArith3::parseExprOp(const Expr& e) {
02856   TRACE("parser", "TheoryArith3::parseExprOp(", e, ")");
02857   //std::cout << "Were here";
02858   // If the expression is not a list, it must have been already
02859   // parsed, so just return it as is.
02860   switch(e.getKind()) {
02861   case ID: {
02862     int kind = getEM()->getKind(e[0].getString());
02863     switch(kind) {
02864     case NULL_KIND: return e; // nothing to do
02865     case REAL:
02866     case INT:
02867     case NEGINF:
02868     case POSINF: return getEM()->newLeafExpr(kind);
02869     default:
02870       DebugAssert(false, "Bad use of bare keyword: "+e.toString());
02871       return e;
02872     }
02873   }
02874   case RAW_LIST: break; // break out of switch, do the hard work
02875   default:
02876     return e;
02877   }
02878 
02879   DebugAssert(e.getKind() == RAW_LIST && e.arity() > 0,
02880         "TheoryArith3::parseExprOp:\n e = "+e.toString());
02881 
02882   const Expr& c1 = e[0][0];
02883   int kind = getEM()->getKind(c1.getString());
02884   switch(kind) {
02885     case UMINUS: {
02886       if(e.arity() != 2)
02887   throw ParserException("UMINUS requires exactly one argument: "
02888       +e.toString());
02889       return uminusExpr(parseExpr(e[1]));
02890     }
02891     case PLUS: {
02892       vector<Expr> k;
02893       Expr::iterator i = e.begin(), iend=e.end();
02894       // Skip first element of the vector of kids in 'e'.
02895       // The first element is the operator.
02896       ++i;
02897       // Parse the kids of e and push them into the vector 'k'
02898       for(; i!=iend; ++i) k.push_back(parseExpr(*i));
02899       return plusExpr(k);
02900     }
02901     case MINUS: {
02902       if(e.arity() == 2)
02903   return uminusExpr(parseExpr(e[1]));
02904       else if(e.arity() == 3)
02905   return minusExpr(parseExpr(e[1]), parseExpr(e[2]));
02906       else
02907   throw ParserException("MINUS requires one or two arguments:"
02908       +e.toString());
02909     }
02910     case MULT: {
02911       vector<Expr> k;
02912       Expr::iterator i = e.begin(), iend=e.end();
02913       // Skip first element of the vector of kids in 'e'.
02914       // The first element is the operator.
02915       ++i;
02916       // Parse the kids of e and push them into the vector 'k'
02917       for(; i!=iend; ++i) k.push_back(parseExpr(*i));
02918       return multExpr(k);
02919     }
02920     case POW: {
02921       return powExpr(parseExpr(e[1]), parseExpr(e[2]));
02922     }
02923     case DIVIDE:
02924       { return divideExpr(parseExpr(e[1]), parseExpr(e[2]));  }
02925     case LT:
02926       { return ltExpr(parseExpr(e[1]), parseExpr(e[2]));  }
02927     case LE:
02928       { return leExpr(parseExpr(e[1]), parseExpr(e[2]));  }
02929     case GT:
02930       { return gtExpr(parseExpr(e[1]), parseExpr(e[2]));  }
02931     case GE:
02932       { return geExpr(parseExpr(e[1]), parseExpr(e[2]));  }
02933     case INTDIV:
02934     case MOD:
02935     case SUBRANGE: {
02936       vector<Expr> k;
02937       Expr::iterator i = e.begin(), iend=e.end();
02938       // Skip first element of the vector of kids in 'e'.
02939       // The first element is the operator.
02940       ++i;
02941       // Parse the kids of e and push them into the vector 'k'
02942       for(; i!=iend; ++i)
02943         k.push_back(parseExpr(*i));
02944       return Expr(kind, k, e.getEM());
02945     }
02946     case IS_INTEGER: {
02947       if(e.arity() != 2)
02948   throw ParserException("IS_INTEGER requires exactly one argument: "
02949       +e.toString());
02950       return Expr(IS_INTEGER, parseExpr(e[1]));
02951     }
02952     default:
02953       DebugAssert(false,
02954         "TheoryArith3::parseExprOp: invalid input " + e.toString());
02955       break;
02956   }
02957   return e;
02958 }
02959 
02960 ///////////////////////////////////////////////////////////////////////////////
02961 // Pretty-printing                                                           //
02962 ///////////////////////////////////////////////////////////////////////////////
02963 
02964 
02965 ExprStream&
02966 TheoryArith3::print(ExprStream& os, const Expr& e) {
02967   switch(os.lang()) {
02968     case SIMPLIFY_LANG:
02969       switch(e.getKind()) {
02970       case RATIONAL_EXPR:
02971   e.print(os);
02972   break;
02973       case SUBRANGE:
02974   os <<"ERROR:SUBRANGE:not supported in Simplify\n";
02975   break;
02976       case IS_INTEGER:
02977   os <<"ERROR:IS_INTEGER:not supported in Simplify\n";
02978   break;
02979       case PLUS:  {
02980   int i=0, iend=e.arity();
02981   os << "(+ ";
02982   if(i!=iend) os << e[i];
02983   ++i;
02984   for(; i!=iend; ++i) os << " " << e[i];
02985   os <<  ")";
02986   break;
02987       }
02988       case MINUS:
02989   os << "(- " << e[0] << " " << e[1]<< ")";
02990   break;
02991       case UMINUS:
02992   os << "-" << e[0] ;
02993   break;
02994       case MULT:  {
02995   int i=0, iend=e.arity();
02996   os << "(* " ;
02997   if(i!=iend) os << e[i];
02998   ++i;
02999   for(; i!=iend; ++i) os << " " << e[i];
03000   os <<  ")";
03001   break;
03002       }
03003       case POW:
03004           os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
03005           break;
03006       case DIVIDE:
03007   os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
03008   break;
03009       case LT:
03010   if (isInt(e[0].getType()) || isInt(e[1].getType())) {
03011   }
03012   os << "(< " << e[0] << " " << e[1] <<")";
03013   break;
03014       case LE:
03015           os << "(<= " << e[0]  << " " << e[1] << ")";
03016           break;
03017       case GT:
03018   os << "(> " << e[0] << " " << e[1] << ")";
03019   break;
03020       case GE:
03021   os << "(>= " << e[0] << " " << e[1]  << ")";
03022   break;
03023       case DARK_SHADOW:
03024       case GRAY_SHADOW:
03025   os <<"ERROR:SHADOW:not supported in Simplify\n";
03026   break;
03027       default:
03028   // Print the top node in the default LISP format, continue with
03029   // pretty-printing for children.
03030           e.print(os);
03031 
03032           break;
03033       }
03034       break; // end of case SIMPLIFY_LANG
03035 
03036     case TPTP_LANG:
03037       switch(e.getKind()) {
03038       case RATIONAL_EXPR:
03039   e.print(os);
03040   break;
03041       case SUBRANGE:
03042   os <<"ERROR:SUBRANGE:not supported in TPTP\n";
03043   break;
03044       case IS_INTEGER:
03045   os <<"ERROR:IS_INTEGER:not supported in TPTP\n";
03046   break;
03047       case PLUS:  {
03048   if(!isInteger(e[0])){
03049     os<<"ERRPR:plus only supports inteters now in TPTP\n";
03050     break;
03051   }
03052 
03053   int i=0, iend=e.arity();
03054   if(iend <=1){
03055     os<<"ERROR,plus must have more than two numbers in TPTP\n";
03056     break;
03057   }
03058 
03059   for(i=0; i <= iend-2; ++i){
03060     os << "$plus_int(";
03061     os << e[i] << ",";
03062   }
03063 
03064   os<< e[iend-1];
03065 
03066   for(i=0 ; i <= iend-2; ++i){
03067     os << ")";
03068   }
03069 
03070   break;
03071       }
03072       case MINUS:
03073   if(!isInteger(e[0])){
03074     os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
03075     break;
03076   }
03077 
03078   os << "$minus_int(" << e[0] << "," << e[1]<< ")";
03079   break;
03080       case UMINUS:
03081   if(!isInteger(e[0])){
03082     os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
03083     break;
03084   }
03085 
03086   os << "$uminus_int(" << e[0] <<")" ;
03087   break;
03088       case MULT:  {
03089   if(!isInteger(e[0])){
03090     os<<"ERRPR:times only supports inteters now in TPTP\n";
03091     break;
03092   }
03093 
03094   int i=0, iend=e.arity();
03095   if(iend <=1){
03096     os<<"ERROR:times must have more than two numbers in TPTP\n";
03097     break;
03098   }
03099 
03100   for(i=0; i <= iend-2; ++i){
03101     os << "$times_int(";
03102     os << e[i] << ",";
03103   }
03104 
03105   os<< e[iend-1];
03106 
03107   for(i=0 ; i <= iend-2; ++i){
03108     os << ")";
03109   }
03110 
03111   break;
03112       }
03113       case POW:
03114 
03115   if(!isInteger(e[0])){
03116     os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
03117     break;
03118   }
03119 
03120   os << "$power_int(" << push << e[1] << space << "^ " << e[0] << push << ")";
03121   break;
03122 
03123       case DIVIDE:
03124   if(!isInteger(e[0])){
03125     os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
03126     break;
03127   }
03128 
03129   os << "divide_int(" <<e[0]  << "," << e[1] << ")";
03130   break;
03131 
03132       case LT:
03133   if(!isInteger(e[0])){
03134     os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
03135     break;
03136   }
03137   os << "$less_int(" << e[0] << "," << e[1] <<")";
03138   break;
03139 
03140       case LE:
03141   if(!isInteger(e[0])){
03142     os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
03143     break;
03144   }
03145 
03146           os << "$lesseq_int(" << e[0]  << "," << e[1] << ")";
03147           break;
03148 
03149       case GT:
03150   if(!isInteger(e[0])){
03151     os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
03152     break;
03153   }
03154 
03155   os << "$greater_int(" << e[0] << "," << e[1] << ")";
03156   break;
03157 
03158       case GE:
03159   if(!isInteger(e[0])){
03160     os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
03161     break;
03162   }
03163 
03164   os << "$greatereq_int(" << e[0] << "," << e[1]  << ")";
03165   break;
03166       case DARK_SHADOW:
03167       case GRAY_SHADOW:
03168   os <<"ERROR:SHADOW:not supported in TPTP\n";
03169   break;
03170 
03171       case INT:
03172   os <<"$int";
03173   break;
03174       case REAL:
03175   os <<"ERROR:REAL not supported in TPTP\n";
03176       default:
03177   // Print the top node in the default LISP format, continue with
03178   // pretty-printing for children.
03179   e.print(os);
03180 
03181           break;
03182       }
03183       break; // end of case TPTP_LANG
03184 
03185     case PRESENTATION_LANG:
03186       switch(e.getKind()) {
03187         case REAL:
03188           os << "REAL";
03189           break;
03190         case INT:
03191           os << "INT";
03192           break;
03193         case RATIONAL_EXPR:
03194           e.print(os);
03195           break;
03196         case NEGINF:
03197           os << "NEGINF";
03198           break;
03199         case POSINF:
03200           os << "POSINF";
03201           break;
03202         case SUBRANGE:
03203           if(e.arity() != 2) e.printAST(os);
03204           else
03205             os << "[" << push << e[0] << ".." << e[1] << push << "]";
03206           break;
03207         case IS_INTEGER:
03208     if(e.arity() == 1)
03209       os << "IS_INTEGER(" << push << e[0] << push << ")";
03210     else
03211       e.printAST(os);
03212     break;
03213         case PLUS:  {
03214           int i=0, iend=e.arity();
03215           os << "(" << push;
03216           if(i!=iend) os << e[i];
03217           ++i;
03218           for(; i!=iend; ++i) os << space << "+ " << e[i];
03219           os << push << ")";
03220           break;
03221         }
03222         case MINUS:
03223           os << "(" << push << e[0] << space << "- " << e[1] << push << ")";
03224           break;
03225         case UMINUS:
03226           os << "-(" << push << e[0] << push << ")";
03227           break;
03228         case MULT:  {
03229           int i=0, iend=e.arity();
03230           os << "(" << push;
03231           if(i!=iend) os << e[i];
03232           ++i;
03233           for(; i!=iend; ++i) os << space << "* " << e[i];
03234           os << push << ")";
03235           break;
03236         }
03237         case POW:
03238           os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
03239           break;
03240         case DIVIDE:
03241           os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
03242           break;
03243         case LT:
03244           if (isInt(e[0].getType()) || isInt(e[1].getType())) {
03245           }
03246           os << "(" << push << e[0] << space << "< " << e[1] << push << ")";
03247           break;
03248         case LE:
03249           os << "(" << push << e[0] << space << "<= " << e[1] << push << ")";
03250           break;
03251         case GT:
03252           os << "(" << push << e[0] << space << "> " << e[1] << push << ")";
03253           break;
03254         case GE:
03255           os << "(" << push << e[0] << space << ">= " << e[1] << push << ")";
03256           break;
03257         case DARK_SHADOW:
03258     os << "DARK_SHADOW(" << push << e[0] << ", " << space << e[1] << push << ")";
03259     break;
03260         case GRAY_SHADOW:
03261     os << "GRAY_SHADOW(" << push << e[0] << ","  << space << e[1]
03262        << "," << space << e[2] << "," << space << e[3] << push << ")";
03263     break;
03264         default:
03265           // Print the top node in the default LISP format, continue with
03266           // pretty-printing for children.
03267           e.printAST(os);
03268 
03269           break;
03270       }
03271       break; // end of case PRESENTATION_LANG
03272     case SMTLIB_LANG: {
03273       switch(e.getKind()) {
03274         case REAL_CONST:
03275           printRational(os, e[0].getRational(), true);
03276           break;
03277         case RATIONAL_EXPR:
03278           printRational(os, e.getRational());
03279           break;
03280         case REAL:
03281           os << "Real";
03282           break;
03283         case INT:
03284           os << "Int";
03285           break;
03286         case SUBRANGE:
03287           throw SmtlibException("TheoryArith3::print: SMTLIB: SUBRANGE not implemented");
03288 //           if(e.arity() != 2) e.print(os);
03289 //           else
03290 //             os << "(" << push << "SUBRANGE" << space << e[0]
03291 //         << space << e[1] << push << ")";
03292           break;
03293         case IS_INTEGER:
03294     if(e.arity() == 1)
03295       os << "(" << push << "IsInt" << space << e[0] << push << ")";
03296     else
03297             throw SmtlibException("TheoryArith3::print: SMTLIB: IS_INTEGER used unexpectedly");
03298     break;
03299         case PLUS:  {
03300           os << "(" << push << "+";
03301           Expr::iterator i = e.begin(), iend = e.end();
03302           for(; i!=iend; ++i) {
03303             os << space << (*i);
03304           }
03305           os << push << ")";
03306           break;
03307         }
03308         case MINUS: {
03309           os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
03310           break;
03311         }
03312         case UMINUS: {
03313           os << "(" << push << "-" << space << e[0] << push << ")";
03314           break;
03315         }
03316         case MULT:  {
03317           int i=0, iend=e.arity();
03318           for(; i!=iend; ++i) {
03319             if (i < iend-1) {
03320               os << "(" << push << "*";
03321             }
03322             os << space << e[i];
03323           }
03324           for (i=0; i < iend-1; ++i) os << push << ")";
03325           break;
03326         }
03327         case POW:
03328           throw SmtlibException("TheoryArith3::print: SMTLIB: POW not supported");
03329           //          os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
03330           break;
03331         case DIVIDE: {
03332           throw SmtlibException("TheoryArith3::print: SMTLIB: unexpected use of DIVIDE");
03333           break;
03334         }
03335         case LT: {
03336           Rational r;
03337           os << "(" << push << "<" << space;
03338           os << e[0] << space << e[1] << push << ")";
03339           break;
03340         }
03341         case LE: {
03342           Rational r;
03343           os << "(" << push << "<=" << space;
03344           os << e[0] << space << e[1] << push << ")";
03345           break;
03346         }
03347         case GT: {
03348           Rational r;
03349           os << "(" << push << ">" << space;
03350           os << e[0] << space << e[1] << push << ")";
03351           break;
03352         }
03353         case GE: {
03354           Rational r;
03355           os << "(" << push << ">=" << space;
03356           os << e[0] << space << e[1] << push << ")";
03357           break;
03358         }
03359         case DARK_SHADOW:
03360           throw SmtlibException("TheoryArith3::print: SMTLIB: DARK_SHADOW not supported");
03361     os << "(" << push << "DARK_SHADOW" << space << e[0]
03362        << space << e[1] << push << ")";
03363     break;
03364         case GRAY_SHADOW:
03365           throw SmtlibException("TheoryArith3::print: SMTLIB: GRAY_SHADOW not supported");
03366     os << "GRAY_SHADOW(" << push << e[0] << ","  << space << e[1]
03367        << "," << space << e[2] << "," << space << e[3] << push << ")";
03368     break;
03369         default:
03370           throw SmtlibException("TheoryArith3::print: SMTLIB: default not supported");
03371           // Print the top node in the default LISP format, continue with
03372           // pretty-printing for children.
03373           e.printAST(os);
03374 
03375           break;
03376       }
03377       break; // end of case SMTLIB_LANG
03378     }
03379     case LISP_LANG:
03380       switch(e.getKind()) {
03381         case REAL:
03382         case INT:
03383         case RATIONAL_EXPR:
03384         case NEGINF:
03385         case POSINF:
03386           e.print(os);
03387           break;
03388         case SUBRANGE:
03389           if(e.arity() != 2) e.printAST(os);
03390           else
03391             os << "(" << push << "SUBRANGE" << space << e[0]
03392          << space << e[1] << push << ")";
03393           break;
03394         case IS_INTEGER:
03395     if(e.arity() == 1)
03396       os << "(" << push << "IS_INTEGER" << space << e[0] << push << ")";
03397     else
03398       e.printAST(os);
03399     break;
03400         case PLUS:  {
03401           int i=0, iend=e.arity();
03402           os << "(" << push << "+";
03403           for(; i!=iend; ++i) os << space << e[i];
03404           os << push << ")";
03405           break;
03406         }
03407         case MINUS:
03408         //os << "(" << push << e[0] << space << "- " << e[1] << push << ")";
03409     os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
03410           break;
03411         case UMINUS:
03412           os << "(" << push << "-" << space << e[0] << push << ")";
03413           break;
03414         case MULT:  {
03415           int i=0, iend=e.arity();
03416           os << "(" << push << "*";
03417           for(; i!=iend; ++i) os << space << e[i];
03418           os << push << ")";
03419           break;
03420         }
03421         case POW:
03422           os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
03423           break;
03424         case DIVIDE:
03425           os << "(" << push << "/ " << e[0] << space << e[1] << push << ")";
03426           break;
03427         case LT:
03428           os << "(" << push << "< " << e[0] << space << e[1] << push << ")";
03429           break;
03430         case LE:
03431           os << "(" << push << "<= " << e[0] << space << e[1] << push << ")";
03432           break;
03433         case GT:
03434           os << "(" << push << "> " << e[1]  << space << e[0] << push << ")";
03435           break;
03436         case GE:
03437           os << "(" << push << ">= " << e[0] << space << e[1] << push << ")";
03438           break;
03439         case DARK_SHADOW:
03440     os << "(" << push << "DARK_SHADOW" << space << e[0]
03441        << space << e[1] << push << ")";
03442     break;
03443         case GRAY_SHADOW:
03444     os << "(" << push << "GRAY_SHADOW" << space << e[0] << space
03445        << e[1] << space << e[2] << space << e[3] << push << ")";
03446     break;
03447         default:
03448           // Print the top node in the default LISP format, continue with
03449           // pretty-printing for children.
03450           e.printAST(os);
03451 
03452           break;
03453       }
03454       break; // end of case LISP_LANG
03455     default:
03456      // Print the top node in the default LISP format, continue with
03457      // pretty-printing for children.
03458        e.printAST(os);
03459   }
03460   return os;
03461 }

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