theory_arith_old.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theory_arith_old.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_arith_old.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 // TheoryArithOld::FreeConst Methods                                            //
00040 ///////////////////////////////////////////////////////////////////////////////
00041 
00042 namespace CVC3 {
00043 
00044 ostream& operator<<(ostream& os, const TheoryArithOld::FreeConst& fc) {
00045   os << "FreeConst(r=" << fc.getConst() << ", " 
00046      << (fc.strict()? "strict" : "non-strict") << ")";
00047   return os;
00048 }
00049 
00050 ///////////////////////////////////////////////////////////////////////////////
00051 // TheoryArithOld::Ineq Methods                                                 //
00052 ///////////////////////////////////////////////////////////////////////////////
00053 
00054 ostream& operator<<(ostream& os, const TheoryArithOld::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 // TheoryArithOld Private Methods                                               //
00065 ///////////////////////////////////////////////////////////////////////////////
00066 
00067 
00068 Theorem TheoryArithOld::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 TheoryArithOld::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& TheoryArithOld::freeConstIneq(const Expr& ineq, bool varOnRHS) {
00094   DebugAssert(isIneq(ineq), "TheoryArithOld::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 TheoryArithOld::FreeConst& 
00111 TheoryArithOld::updateSubsumptionDB(const Expr& ineq, bool varOnRHS,
00112          bool& subsumed) {
00113   TRACE("arith ineq", "TheoryArithOld::updateSubsumptionDB(", ineq, 
00114   ", var isolated on "+string(varOnRHS? "RHS" : "LHS")+")");
00115   DebugAssert(isLT(ineq) || isLE(ineq), "TheoryArithOld::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, "TheoryArithOld::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 TheoryArithOld::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: TheoryArithOld::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 TheoryArithOld::canon(const Expr& e)
00213 {
00214   TRACE("arith canon","canon(",e,") {");
00215   DebugAssert(kidsCanonical(e), "TheoryArithOld::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 TheoryArithOld::canonSimplify(const Expr& e) {
00361   TRACE("arith", "canonSimplify(", e, ") {");
00362   DebugAssert(kidsCanonical(e),
00363         "TheoryArithOld::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 TheoryArithOld::canonPred(const Theorem& thm) {
00391   vector<Theorem> thms;
00392   DebugAssert(thm.getExpr().arity() == 2,
00393               "TheoryArithOld::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 TheoryArithOld::canonPredEquiv(const Theorem& thm) {
00405   vector<Theorem> thms;
00406   DebugAssert(thm.getRHS().arity() == 2,
00407               "TheoryArithOld::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 TheoryArithOld::canonConjunctionEquiv(const Theorem& thm) {
00420   vector<Theorem> thms;
00421   return thm;
00422 }
00423 
00424 /*! Psuedo-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 TheoryArithOld::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   if(!isInteger(right)) {
00463     Theorem res;
00464     try {
00465       res = processRealEq(eqnThm);
00466     } catch(ArithException& e) {
00467       res = symmetryRule(eqnThm); // Flip to e' = 0
00468       TRACE("arith eq", "doSolve: failed to solve an equation: ", e, "");
00469       IF_DEBUG(debugger.counter("FAILED to solve real equalities")++);
00470       setIncomplete("Non-linear arithmetic inequalities");
00471     }
00472     IF_DEBUG(debugger.counter("solved real equalities")++);
00473     TRACE("arith eq", "doSolve [real] => ", res, " }");
00474     return res;
00475   }
00476   else {
00477     Theorem res = processIntEq(eqnThm);
00478     IF_DEBUG(debugger.counter("solved int equalities")++);
00479     TRACE("arith eq", "doSolve [int] => ", res, " }");
00480     return res;
00481   }
00482 }
00483 
00484 /*! pick a monomial for the input equation. This function is used only
00485  *  if the equation is an integer equation. Choose the monomial with
00486  *  the smallest absolute value of coefficient.
00487  */
00488 Expr
00489 TheoryArithOld::pickIntEqMonomial(const Expr& right)
00490 {
00491   DebugAssert(isPlus(right) && right.arity() > 2,
00492               "TheoryArithOld::pickIntEqMonomial right is wrong :-): " +
00493               right.toString());
00494   DebugAssert(right[0].isRational(),
00495               "TheoryArithOld::pickIntEqMonomial. right[0] must be const" +
00496               right.toString());
00497   DebugAssert(isInteger(right),
00498               "TheoryArithOld::pickIntEqMonomial: right is of type int: " +
00499               right.toString());
00500   //right is of the form "C + a1x1 + ... + anxn". min is initialized
00501   //to a1
00502   Expr::iterator i = right.begin();
00503   i++; //skip 'C'
00504   Rational min = isMult(*i) ? abs((*i)[0].getRational()) : 1;
00505   Expr pickedMon = *i;
00506   for(Expr::iterator iend = right.end(); i != iend; ++i) {
00507     Rational coeff = isMult(*i) ? abs((*i)[0].getRational()) : 1;
00508     if(min > coeff) {
00509       min = coeff;
00510       pickedMon = *i;
00511     }
00512   }
00513   return pickedMon;
00514 }
00515 
00516 /*! input is e1=e2<==>0=e' Theorem and some of the vars in e' are of
00517  * type REAL. isolate one of them and send back to framework. output
00518  * is "e1=e2 <==> var = e''" Theorem.
00519  */
00520 Theorem 
00521 TheoryArithOld::processRealEq(const Theorem& eqn)
00522 {
00523   Expr right = eqn.getRHS();
00524   // Find variable to isolate and store it in left.  Pick the largest
00525   // (according to the total ordering) variable.  FIXME: change from
00526   // total ordering to the ordering we devised for inequalities.
00527 
00528   // TODO: I have to pick a variable that appears as a variable in the
00529   // term but does not appear as a variable anywhere else.  The variable
00530   // must appear as a single leaf and not in a MULT expression with some
00531   // other variables and nor in a POW expression.
00532 
00533   bool found = false;
00534   
00535   Expr left;
00536   
00537   if (isPlus(right))  {
00538     for(int i = right.arity()-1; i>=0; --i) {
00539       Expr c = right[i];
00540       if(isRational(c))
00541         continue;
00542       if(!isInteger(c))  {
00543         if (isLeaf(c) || 
00544             ((isMult(c) && c.arity() == 2 && isLeaf(c[1])))) {
00545           int numoccurs = 0;
00546           Expr leaf = isLeaf(c) ? c : c[1];
00547           for (int j = 0; j < right.arity(); ++j) {
00548             if (j!= i
00549     && isLeafIn(leaf, right[j])
00550     // && leaf.subExprOf(right[j])
00551     ) {
00552               numoccurs++;
00553               break;
00554             }
00555           }
00556           if (!numoccurs) {
00557             left = c;
00558             found = true;
00559             break;
00560           }
00561         }
00562       }
00563     }
00564   }
00565   else if ((isMult(right) && right.arity() == 2 && isLeaf(right[1])) ||
00566            isLeaf(right)) {
00567     left = right;
00568     found = true;
00569   }
00570   
00571   if (!found) {
00572     // TODO:
00573     // throw an arithmetic exception that this cannot be done.
00574     throw 
00575       ArithException("Can't find a leaf for solve in "+eqn.toString());
00576   }
00577 
00578   Rational r = -1;
00579   if (isMult(left))  {
00580     DebugAssert(left.arity() == 2, "only leaf should be chosen as lhs");
00581     DebugAssert(left[0].getRational() != 0, "left = "+left.toString());
00582     r = -1/left[0].getRational();
00583     left = left[1];
00584   }
00585 
00586   DebugAssert(isReal(getBaseType(left)) && !isInteger(left),
00587               "TheoryArithOld::ProcessRealEq: left is integer:\n left = "
00588         +left.toString());
00589   // Normalize equation so that coefficient of the monomial
00590   // corresponding to "left" in eqn[1] is -1
00591   Theorem result(iffMP(eqn,
00592            d_rules->multEqn(eqn.getLHS(), eqn.getRHS(), rat(r))));
00593   result = canonPred(result);
00594 
00595   // Isolate left
00596   result = iffMP(result, d_rules->plusPredicate(result.getLHS(),
00597             result.getRHS(), left, EQ));
00598   result = canonPred(result);
00599   TRACE("arith","processRealEq => ",result," }");
00600   return result;
00601 }
00602 
00603 /*!
00604  * \param eqn is a single equation 0 = e
00605  * \return an equivalent Theorem (x = t AND 0 = e'), or just x = t
00606  */
00607 Theorem
00608 TheoryArithOld::processSimpleIntEq(const Theorem& eqn)
00609 {
00610   TRACE("arith eq", "processSimpleIntEq(", eqn.getExpr(), ") {");
00611   DebugAssert(eqn.isRewrite(),
00612               "TheoryArithOld::processSimpleIntEq: eqn must be equality" +
00613               eqn.getExpr().toString());
00614 
00615   Expr right = eqn.getRHS();
00616 
00617   DebugAssert(eqn.getLHS().isRational() && 0 == eqn.getLHS().getRational(),
00618               "TheoryArithOld::processSimpleIntEq: LHS must be 0:\n" +
00619               eqn.getExpr().toString());
00620 
00621   //recall that 0 = c case is already handled in doSolve() function.
00622   if(isMult(right)) {
00623     //here we take care of special case 0=c.x
00624     Expr c,x;
00625     separateMonomial(right, c, x);
00626     Theorem isIntx(isIntegerThm(x));
00627     DebugAssert(!isIntx.isNull(), "right = "+right.toString());
00628     Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx)));
00629     TRACE("arith eq", "processSimpleIntEq[0 = a*x] => ", res, " }");
00630     return res;
00631   } else if(isPlus(right)) {
00632     if(2 == right.arity()) {
00633       //we take care of special cases like 0 = c + a.x, 0 = c + x,
00634       Expr c,x;
00635       separateMonomial(right[1], c, x);
00636       Theorem isIntx(isIntegerThm(x));
00637       DebugAssert(!isIntx.isNull(), "right = "+right.toString()
00638       +"\n x = "+x.toString());
00639       Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx)));
00640       TRACE("arith eq", "processSimpleIntEq[0 = c + a*x] => ", res, " }");
00641       return res;
00642     }
00643     DebugAssert(right.arity() > 2,
00644                 "TheoryArithOld::processSimpleIntEq: RHS is not in correct form:"
00645                 +eqn.getExpr().toString());
00646     // Pick a suitable monomial. isolated can be of the form x, a.x, -a.x
00647     Expr isolated = pickIntEqMonomial(right);
00648     TRACE("arith eq", "processSimpleIntEq: isolated = ", isolated, "");
00649 
00650     // First, we compute the 'sign factor' with which to multiply the
00651     // eqn.  if the coeff of isolated is positive (i.e. 'isolated' is
00652     // of the form x or a.x where a>0 ) then r must be -1 and if coeff
00653     // of 'isolated' is negative, r=1.
00654     Rational r = isMult(isolated) ?
00655       ((isolated[0].getRational() > 0) ? -1 : 1) : -1;
00656     Theorem result;
00657     if (-1 == r) {
00658       // r=-1 and hence 'isolated' is 'x' or 'a.x' where a is
00659       // positive.  modify eqn (0=e') to the equation (0=canon(-1*e'))
00660       result = iffMP(eqn, d_rules->multEqn(eqn.getLHS(), right, rat(r)));
00661       result = canonPred(result);
00662       Expr e = result.getRHS();
00663 
00664       // Isolate the 'isolated'
00665       result = iffMP(result,
00666          d_rules->plusPredicate(result.getLHS(),result.getRHS(),
00667               isolated, EQ));
00668     } else {
00669       //r is 1 and hence isolated is -a.x. Make 'isolated' positive.
00670       const Rational& minusa = isolated[0].getRational();
00671       Rational a = -1*minusa;
00672       isolated = (a == 1)? isolated[1] : rat(a) * isolated[1];
00673       
00674       // Isolate the 'isolated'
00675       result = iffMP(eqn, d_rules->plusPredicate(eqn.getLHS(), 
00676              right,isolated,EQ));
00677     }
00678     // Canonize the result
00679     result = canonPred(result);
00680         
00681     //if isolated is 'x' or 1*x, then return result else continue processing.
00682     if(!isMult(isolated) || isolated[0].getRational() == 1) {   
00683       TRACE("arith eq", "processSimpleIntEq[x = rhs] => ", result, " }");
00684       return result;
00685     } else {
00686       DebugAssert(isMult(isolated) && isolated[0].getRational() >= 2,
00687                   "TheoryArithOld::processSimpleIntEq: isolated must be mult "
00688       "with coeff >= 2.\n isolated = " + isolated.toString());
00689 
00690       // Compute IS_INTEGER() for lhs and rhs
00691       Expr lhs = result.getLHS();
00692       Expr rhs = result.getRHS();
00693       Expr a, x;
00694       separateMonomial(lhs, a, x);
00695       Theorem isIntLHS = isIntegerThm(x);
00696       vector<Theorem> isIntRHS;
00697       if(!isPlus(rhs)) { // rhs is a MULT
00698   Expr c, v;
00699   separateMonomial(rhs, c, v);
00700   isIntRHS.push_back(isIntegerThm(v));
00701   DebugAssert(!isIntRHS.back().isNull(), "");
00702       } else { // rhs is a PLUS
00703   DebugAssert(isPlus(rhs), "rhs = "+rhs.toString());
00704   DebugAssert(rhs.arity() >= 2, "rhs = "+rhs.toString());
00705   Expr::iterator i=rhs.begin(), iend=rhs.end();
00706   ++i; // Skip the free constant
00707   for(; i!=iend; ++i) {
00708     Expr c, v;
00709     separateMonomial(*i, c, v);
00710     isIntRHS.push_back(isIntegerThm(v));
00711     DebugAssert(!isIntRHS.back().isNull(), "");
00712   }
00713       }
00714       // Derive (EXISTS (x:INT): x = t2 AND 0 = t3)
00715       result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS);
00716       // Skolemize the quantifier
00717       result = getCommonRules()->skolemize(result);
00718       // Canonize t2 and t3 generated by this rule
00719       DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
00720       "processSimpleIntEq: result = "+result.getExpr().toString());
00721       Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0));
00722       Theorem thm2 = canonPred(getCommonRules()->andElim(result, 1));
00723       Theorem newRes = getCommonRules()->andIntro(thm1, thm2);
00724       if(newRes.getExpr() != result.getExpr()) result = newRes;
00725       
00726       TRACE("arith eq", "processSimpleIntEq => ", result, " }");
00727       return result;
00728     }
00729   } else {
00730     // eqn is 0 = x.  Flip it and return
00731     Theorem result = symmetryRule(eqn);
00732     TRACE("arith eq", "processSimpleIntEq[x = 0] => ", result, " }");
00733     return result;
00734   }
00735 }
00736 
00737 /*! input is e1=e2<==>0=e' Theorem and all of the vars in e' are of
00738  * type INT. isolate one of them and send back to framework. output
00739  * is "e1=e2 <==> var = e''" Theorem and some associated equations in
00740  * solved form.
00741  */
00742 Theorem 
00743 TheoryArithOld::processIntEq(const Theorem& eqn)
00744 {
00745   TRACE("arith eq", "processIntEq(", eqn.getExpr(), ") {");
00746   // Equations in the solved form.  
00747   std::vector<Theorem> solvedAndNewEqs;
00748   Theorem newEq(eqn), result;
00749   bool done(false);
00750   do {
00751     result = processSimpleIntEq(newEq);
00752     // 'result' is of the from (x1=t1)  AND 0=t'
00753     if(result.isRewrite()) {
00754       solvedAndNewEqs.push_back(result);
00755       done = true;
00756     }
00757     else if(!result.getExpr().isFalse()) {
00758       DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
00759       "TheoryArithOld::processIntEq("+eqn.getExpr().toString()
00760       +")\n result = "+result.getExpr().toString());
00761       solvedAndNewEqs.push_back(getCommonRules()->andElim(result, 0));
00762       newEq = getCommonRules()->andElim(result, 1);
00763     } else
00764       done = true;
00765   } while(!done);
00766   Theorem res;
00767   if(result.getExpr().isFalse()) res = result;
00768   else res = solvedForm(solvedAndNewEqs);
00769   TRACE("arith eq", "processIntEq => ", res.getExpr(), " }");
00770   return res;
00771 }
00772 
00773 /*!
00774  * Takes a vector of equations and for every equation x_i=t_i
00775  * substitutes t_j for x_j in t_i for all j>i.  This turns the system
00776  * of equations into a solved form.
00777  *
00778  * Assumption: variables x_j may appear in the RHS terms t_i ONLY for
00779  * i<j, but not for i>=j.
00780  */
00781 Theorem
00782 TheoryArithOld::solvedForm(const vector<Theorem>& solvedEqs) 
00783 {
00784   DebugAssert(solvedEqs.size() > 0, "TheoryArithOld::solvedForm()");
00785 
00786   // Trace code
00787   TRACE_MSG("arith eq", "TheoryArithOld::solvedForm:solvedEqs(\n  [");
00788   IF_DEBUG(if(debugger.trace("arith eq")) {
00789     for(vector<Theorem>::const_iterator j = solvedEqs.begin(),
00790     jend=solvedEqs.end(); j!=jend;++j)
00791       TRACE("arith eq", "", j->getExpr(), ",\n   ");
00792   });
00793   TRACE_MSG("arith eq", "  ]) {");
00794   // End of Trace code
00795   
00796   vector<Theorem>::const_reverse_iterator
00797     i = solvedEqs.rbegin(),
00798     iend = solvedEqs.rend();
00799   // Substitution map: a variable 'x' is mapped to a Theorem x=t.
00800   // This map accumulates the resulting solved form.
00801   ExprMap<Theorem> subst;
00802   for(; i!=iend; ++i) {
00803     if(i->isRewrite()) {
00804       Theorem thm = substAndCanonize(*i, subst);
00805       TRACE("arith eq", "solvedForm: subst["+i->getLHS().toString()+"] = ",
00806       thm.getExpr(), "");
00807       subst[i->getLHS()] = thm;
00808     }
00809     else {
00810       // This is the FALSE case: just return the contradiction
00811       DebugAssert(i->getExpr().isFalse(),
00812       "TheoryArithOld::solvedForm: an element of solvedEqs must "
00813       "be either EQ or FALSE: "+i->toString());
00814       return *i;
00815     }
00816   }
00817   // Now we've collected the solved form in 'subst'.  Wrap it up into
00818   // a conjunction and return.
00819   vector<Theorem> thms;
00820   for(ExprMap<Theorem>::iterator i=subst.begin(), iend=subst.end();
00821       i!=iend; ++i)
00822     thms.push_back(i->second);
00823   return getCommonRules()->andIntro(thms);
00824 }
00825 
00826 
00827 /*!
00828  * ASSUMPTION: 't' is a fully canonized arithmetic term, and every
00829  * element of subst is a fully canonized equation of the form x=e,
00830  * indexed by the LHS variable.
00831  */
00832 
00833 Theorem
00834 TheoryArithOld::substAndCanonize(const Expr& t, ExprMap<Theorem>& subst)
00835 {
00836   TRACE("arith eq", "substAndCanonize(", t, ") {");
00837   // Quick and dirty check: return immediately if subst is empty
00838   if(subst.empty()) {
00839     Theorem res(reflexivityRule(t));
00840     TRACE("arith eq", "substAndCanonize[subst empty] => ", res, " }");
00841     return res;
00842   }
00843   // Check if we can substitute 't' directly
00844   ExprMap<Theorem>::iterator i = subst.find(t), iend=subst.end();
00845   if(i!=iend) {
00846     TRACE("arith eq", "substAndCanonize[subst] => ", i->second, " }");
00847     return i->second;
00848   }
00849   // The base case: t is an i-leaf
00850   if(isLeaf(t)) {
00851     Theorem res(reflexivityRule(t));
00852     TRACE("arith eq", "substAndCanonize[i-leaf] => ", res, " }");
00853     return res;
00854   }
00855   // 't' is an arithmetic term; recurse into the children
00856   vector<Theorem> thms;
00857   vector<unsigned> changed;
00858   for(unsigned j=0, jend=t.arity(); j!=jend; ++j) {
00859     Theorem thm = substAndCanonize(t[j], subst);
00860     if(thm.getRHS() != t[j]) {
00861       thm = canonThm(thm);
00862       thms.push_back(thm);
00863       changed.push_back(j);
00864     }
00865   }
00866   // Do the actual substitution and canonize the result
00867   Theorem res;
00868   if(thms.size() > 0) {
00869     res = substitutivityRule(t, changed, thms);
00870     res = canonThm(res);
00871   }
00872   else
00873     res = reflexivityRule(t);
00874   TRACE("arith eq", "substAndCanonize => ", res, " }");
00875   return res;
00876 }
00877 
00878 
00879 /*!
00880  *  ASSUMPTION: 't' is a fully canonized equation of the form x = t,
00881  *  and so is every element of subst, indexed by the LHS variable.
00882  */
00883 
00884 Theorem
00885 TheoryArithOld::substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst)
00886 {
00887   // Quick and dirty check: return immediately if subst is empty
00888   if(subst.empty()) return eq;
00889 
00890   DebugAssert(eq.isRewrite(), "TheoryArithOld::substAndCanonize: t = "
00891         +eq.getExpr().toString());
00892   const Expr& t = eq.getRHS();
00893   // Do the actual substitution in the term t
00894   Theorem thm = substAndCanonize(t, subst);
00895   // Substitution had no result: return the original equation
00896   if(thm.getRHS() == t) return eq;
00897   // Otherwise substitute the result into the equation
00898   vector<Theorem> thms;
00899   vector<unsigned> changed;
00900   thms.push_back(thm);
00901   changed.push_back(1);
00902   return iffMP(eq, substitutivityRule(eq.getExpr(), changed, thms));
00903 }
00904 
00905 
00906 void TheoryArithOld::processBuffer()
00907 {
00908   // Process the inequalities in the buffer
00909   bool varOnRHS;
00910   for(; !inconsistent() && d_bufferIdx < d_buffer.size();
00911       d_bufferIdx = d_bufferIdx+1) {
00912     const Theorem& ineqThm = d_buffer[d_bufferIdx];
00913     // Skip this inequality if it is stale
00914     if(isStale(ineqThm.getExpr())) continue;
00915     Theorem thm1 = isolateVariable(ineqThm, varOnRHS);
00916     const Expr& ineq = thm1.getExpr();
00917     if((ineq).isFalse())
00918       setInconsistent(thm1);
00919     else if(!ineq.isTrue()) {
00920       // Check that the variable is indeed isolated correctly
00921       DebugAssert(varOnRHS? !isPlus(ineq[1]) : !isPlus(ineq[0]),
00922       "TheoryArithOld::processBuffer(): bad result from "
00923       "isolateVariable:\nineq = "+ineq.toString());
00924       // and project the inequality
00925       projectInequalities(thm1, varOnRHS);
00926     }
00927   }
00928 }
00929 
00930 
00931 void TheoryArithOld::updateStats(const Rational& c, const Expr& v)
00932 {
00933   TRACE("arith ineq", "updateStats("+c.toString()+", ", v, ")");
00934   if(c > 0) {
00935     if(d_countRight.count(v) > 0) d_countRight[v] = d_countRight[v] + 1;
00936     else d_countRight[v] = 1;
00937   }
00938   else
00939     if(d_countLeft.count(v) > 0) d_countLeft[v] = d_countLeft[v] + 1;
00940     else d_countLeft[v] = 1;
00941 }
00942 
00943 
00944 void TheoryArithOld::updateStats(const Expr& monomial)
00945 {
00946   Expr c, m;
00947   separateMonomial(monomial, c, m);
00948   updateStats(c.getRational(), m);
00949 }
00950 
00951 
00952 void TheoryArithOld::addToBuffer(const Theorem& thm) {
00953   // First, turn the inequality into 0 < rhs
00954   // FIXME: check if this can be optimized away
00955   Theorem result(thm);
00956   const Expr& e = thm.getExpr();
00957   // int kind = e.getKind();
00958   if(!(e[0].isRational() && e[0].getRational() == 0)) {
00959     result = iffMP(result, d_rules->rightMinusLeft(e));
00960     result = canonPred(result);
00961   }
00962   TRACE("arith ineq", "addToBuffer(", result.getExpr(), ")");
00963   // Push it into the buffer
00964   d_buffer.push_back(thm);
00965 
00966   // Collect the statistics about variables
00967   const Expr& rhs = thm.getExpr()[1];
00968   if(isPlus(rhs))
00969     for(Expr::iterator i=rhs.begin(), iend=rhs.end(); i!=iend; ++i)
00970       updateStats(*i);
00971   else // It's a monomial
00972     updateStats(rhs);
00973 }
00974 
00975 
00976 Theorem TheoryArithOld::isolateVariable(const Theorem& inputThm, 
00977                                      bool& isolatedVarOnRHS)
00978 {
00979   Theorem result(inputThm);
00980   const Expr& e = inputThm.getExpr();
00981   TRACE("arith","isolateVariable(",e,") {");
00982   TRACE("arith ineq", "isolateVariable(", e, ") {");
00983   //we assume all the children of e are canonized
00984   DebugAssert(isLT(e)||isLE(e),
00985               "TheoryArithOld::isolateVariable: " + e.toString() +
00986               " wrong kind");
00987   int kind = e.getKind();
00988   DebugAssert(e[0].isRational() && e[0].getRational() == 0,
00989               "TheoryArithOld::isolateVariable: theorem must be of "
00990               "the form 0 < rhs: " + inputThm.toString());
00991 
00992   const Expr& zero = e[0];
00993   Expr right = e[1];
00994   // Check for trivial in-equation.
00995   if (right.isRational()) {
00996     result = iffMP(result, d_rules->constPredicate(e));
00997     TRACE("arith ineq","isolateVariable => ",result.getExpr()," }");
00998     TRACE("arith","isolateVariable => ",result," }");
00999     return result;
01000   }
01001 
01002   // Normalization of inequality to make coefficients integer and
01003   // relatively prime.
01004 
01005   Expr factor(computeNormalFactor(right));
01006   TRACE("arith", "isolateVariable: factor = ", factor, "");
01007   DebugAssert(factor.getRational() > 0,
01008               "isolateVariable: factor="+factor.toString());
01009   // Now multiply the inequality by the factor, unless it is 1
01010   if(factor.getRational() != 1) {
01011     result = iffMP(result, d_rules->multIneqn(e, factor));
01012     // And canonize the result
01013     result = canonPred(result);
01014     right = result.getExpr()[1];
01015   }
01016 
01017   // Find monomial to isolate and store it in isolatedMonomial
01018   Expr isolatedMonomial = right;
01019 
01020   if (isPlus(right))
01021     isolatedMonomial = pickMonomial(right);
01022 
01023   Rational r = -1;
01024   isolatedVarOnRHS = true;
01025   if (isMult(isolatedMonomial)) {
01026     r = ((isolatedMonomial[0].getRational()) >= 0)? -1 : 1;
01027     isolatedVarOnRHS = 
01028       ((isolatedMonomial[0].getRational()) >= 0)? true : false;
01029   }
01030   isolatedMonomial = canon(rat(-1)*isolatedMonomial).getRHS();
01031   // Isolate isolatedMonomial on to the LHS
01032   result = iffMP(result, d_rules->plusPredicate(zero, right, 
01033                                                 isolatedMonomial, kind));
01034   // Canonize the resulting inequality
01035   result = canonPred(result);
01036   if(1 != r) {
01037     result = iffMP(result, d_rules->multIneqn(result.getExpr(), rat(r)));
01038     result = canonPred(result);
01039   }
01040   TRACE("arith ineq","isolateVariable => ",result.getExpr()," }");
01041   TRACE("arith","isolateVariable => ",result," }");
01042   return result;
01043 }
01044 
01045 Expr
01046 TheoryArithOld::computeNormalFactor(const Expr& right) {
01047   // Strategy: compute f = lcm(d1...dn)/gcd(c1...cn), where the RHS is
01048   // of the form c1/d1*x1 + ... + cn/dn*xn
01049   Rational factor;
01050   if(isPlus(right)) {
01051     vector<Rational> nums, denoms;
01052     for(int i=0, iend=right.arity(); i<iend; ++i) {
01053       switch(right[i].getKind()) {
01054       case RATIONAL_EXPR: {
01055         Rational c(abs(right[i].getRational()));
01056         nums.push_back(c.getNumerator());
01057         denoms.push_back(c.getDenominator());
01058         break;
01059         }
01060       case MULT: {
01061         Rational c(abs(right[i][0].getRational()));
01062         nums.push_back(c.getNumerator());
01063         denoms.push_back(c.getDenominator());
01064         break;
01065         }
01066       default: // it's a variable
01067         nums.push_back(1);
01068         denoms.push_back(1);
01069         break;
01070       }
01071     }
01072     Rational gcd_nums = gcd(nums);
01073     // x/0 == 0 in our model, as a total extension of arithmetic.  The
01074     // particular value of x/0 is irrelevant, since the DP is guarded
01075     // by the top-level TCCs, and it is safe to return any value in
01076     // cases when terms are undefined.
01077     factor = (gcd_nums==0)? 0 : (lcm(denoms) / gcd_nums);
01078   } else if(isMult(right)) {
01079     const Rational& r = right[0].getRational();
01080     factor = (r==0)? 0 : (1/abs(r));
01081   }
01082   else 
01083     factor = 1;
01084   return rat(factor);
01085 }
01086 
01087 
01088 bool TheoryArithOld::lessThanVar(const Expr& isolatedMonomial, const Expr& var2) 
01089 {
01090   DebugAssert(!isRational(var2) && !isRational(isolatedMonomial),
01091               "TheoryArithOld::findMaxVar: isolatedMonomial cannot be rational" + 
01092               isolatedMonomial.toString());
01093   Expr c, var0, var1;
01094   separateMonomial(isolatedMonomial, c, var0);
01095   separateMonomial(var2, c, var1);
01096   return var0 < var1;
01097 }
01098 
01099 /*! "Stale" means it contains non-simplified subexpressions.  For
01100  *  terms, it checks the expression's find pointer; for formulas it
01101  *  checks the children recursively (no caching!).  So, apply it with
01102  *  caution, and only to simple atomic formulas (like inequality).
01103  */
01104 bool TheoryArithOld::isStale(const Expr& e) {
01105   if(e.isTerm())
01106     return e != find(e).getRHS();
01107   // It's better be a simple predicate (like inequality); we check the
01108   // kids recursively
01109   bool stale=false;
01110   for(Expr::iterator i=e.begin(), iend=e.end(); !stale && i!=iend; ++i)
01111     stale = isStale(*i);
01112   return stale;
01113 }
01114 
01115 
01116 bool TheoryArithOld::isStale(const TheoryArithOld::Ineq& ineq) {
01117   TRACE("arith ineq", "isStale(", ineq, ") {");
01118   const Expr& ineqExpr = ineq.ineq().getExpr();
01119   const Rational& c = freeConstIneq(ineqExpr, ineq.varOnRHS());
01120   bool strict(isLT(ineqExpr));
01121   const FreeConst& fc = ineq.getConst();
01122 
01123   bool subsumed;
01124 
01125   if(ineq.varOnRHS()) {
01126     subsumed = (c < fc.getConst() ||
01127     (c == fc.getConst() && !strict && fc.strict()));
01128   } else {
01129     subsumed = (c > fc.getConst() ||
01130     (c == fc.getConst() && strict && !fc.strict()));
01131   }
01132 
01133   bool res;
01134   if(subsumed) {
01135     res = true;
01136     TRACE("arith ineq", "isStale[subsumed] => ", res? "true" : "false", " }");
01137   }
01138   else {
01139     res = isStale(ineqExpr);
01140     TRACE("arith ineq", "isStale[updated] => ", res? "true" : "false", " }");
01141   }
01142   return res;
01143 }
01144 
01145 
01146 void TheoryArithOld::separateMonomial(const Expr& e, Expr& c, Expr& var) {
01147   TRACE("separateMonomial", "separateMonomial(", e, ")");
01148   DebugAssert(!isPlus(e), 
01149         "TheoryArithOld::separateMonomial(e = "+e.toString()+")");
01150   if(isMult(e)) {
01151     DebugAssert(e.arity() >= 2,
01152     "TheoryArithOld::separateMonomial(e = "+e.toString()+")");
01153     c = e[0];
01154     if(e.arity() == 2) var = e[1];
01155     else {
01156       vector<Expr> kids = e.getKids();
01157       kids[0] = rat(1);
01158       var = multExpr(kids);
01159     }
01160   } else {
01161     c = rat(1);
01162     var = e;
01163   }
01164   DebugAssert(c.isRational(), "TheoryArithOld::separateMonomial(e = "
01165         +e.toString()+", c = "+c.toString()+")");
01166   DebugAssert(!isMult(var) || (var[0].isRational() && var[0].getRational()==1),
01167         "TheoryArithOld::separateMonomial(e = "
01168         +e.toString()+", var = "+var.toString()+")");
01169 }
01170 
01171 
01172 void TheoryArithOld::projectInequalities(const Theorem& theInequality, 
01173                                       bool isolatedVarOnRHS)
01174 {
01175   TRACE("arith ineq", "projectInequalities(", theInequality.getExpr(),
01176         ", isolatedVarOnRHS="+string(isolatedVarOnRHS? "true" : "false")
01177         +") {");
01178   DebugAssert(isLE(theInequality.getExpr()) || 
01179               isLT(theInequality.getExpr()),
01180               "TheoryArithOld::projectIsolatedVar: "\
01181               "theInequality is of the wrong form: " + 
01182               theInequality.toString());
01183   //TODO: DebugAssert to check if the isolatedMonomial is of the right
01184   //form and the whether we are indeed getting inequalities.
01185   Theorem theIneqThm(theInequality);
01186   Expr theIneq = theIneqThm.getExpr();
01187 
01188   Theorem isIntLHS(isIntegerThm(theIneq[0]));
01189   Theorem isIntRHS(isIntegerThm(theIneq[1]));
01190   bool isInt = (!isIntLHS.isNull() && !isIntRHS.isNull());
01191   // If the inequality is strict and integer, change it to non-strict
01192   if(isLT(theIneq) && isInt) {
01193     Theorem thm = d_rules->lessThanToLE(theInequality, isIntLHS, isIntRHS,
01194           !isolatedVarOnRHS);
01195     theIneqThm = canonPred(iffMP(theIneqThm, thm));
01196     theIneq = theIneqThm.getExpr();
01197   }
01198   Expr isolatedMonomial = 
01199     isolatedVarOnRHS ? theIneq[1] : theIneq[0];
01200   
01201   Expr monomialVar, a;
01202   separateMonomial(isolatedMonomial, a, monomialVar);
01203 
01204   bool subsumed;
01205   const FreeConst& bestConst =
01206     updateSubsumptionDB(theIneq, isolatedVarOnRHS, subsumed);
01207 
01208   if(subsumed) {
01209     IF_DEBUG(debugger.counter("subsumed inequalities")++);
01210     TRACE("arith ineq", "subsumed inequality: ", theIneq, "");
01211   } else {
01212     // If the isolated variable is actually a non-linear term, we are
01213     // incomplete
01214     if(isMult(monomialVar) || isPow(monomialVar))
01215       setIncomplete("Non-linear arithmetic inequalities");
01216 
01217     // First, we need to make sure the isolated inequality is
01218     // setup properly.
01219     //    setupRec(theIneq[0]);
01220     //    setupRec(theIneq[1]);
01221     theoryCore()->setupTerm(theIneq[0], this, theIneqThm);
01222     theoryCore()->setupTerm(theIneq[1], this, theIneqThm);
01223     // Add the inequality into the appropriate DB.
01224     ExprMap<CDList<Ineq> *>& db1 =
01225       isolatedVarOnRHS ? d_inequalitiesRightDB : d_inequalitiesLeftDB; 
01226     ExprMap<CDList<Ineq> *>::iterator it1 = db1.find(monomialVar);
01227     if(it1 == db1.end()) {
01228       CDList<Ineq> * list = new(true) CDList<Ineq>(theoryCore()->getCM()->getCurrentContext());
01229       list->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
01230       db1[monomialVar] = list;
01231     }
01232     else 
01233       ((*it1).second)->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
01234   
01235     ExprMap<CDList<Ineq> *>& db2 = 
01236       isolatedVarOnRHS ? d_inequalitiesLeftDB : d_inequalitiesRightDB; 
01237     ExprMap<CDList<Ineq> *>::iterator it = db2.find(monomialVar);
01238     if(it == db2.end()) {
01239       TRACE_MSG("arith ineq", "projectInequalities[not in DB] => }");
01240       return;
01241     }
01242   
01243     CDList<Ineq>& listOfDBIneqs = *((*it).second);
01244     Theorem betaLTt, tLTalpha, thm;
01245     for(size_t i = 0, iend=listOfDBIneqs.size(); i!=iend; ++i) {
01246       const Ineq& ineqEntry = listOfDBIneqs[i];
01247       const Theorem& ineqThm = ineqEntry.ineq();
01248       if(!isStale(ineqEntry)) {
01249   betaLTt = isolatedVarOnRHS ? theIneqThm : ineqThm;
01250   tLTalpha = isolatedVarOnRHS ? ineqThm : theIneqThm;
01251   thm = normalizeProjectIneqs(betaLTt, tLTalpha);
01252   
01253   IF_DEBUG(debugger.counter("real shadows")++);
01254 
01255   // Check for TRUE and FALSE theorems
01256   Expr e(thm.getExpr());  if(e.isFalse()) {
01257     setInconsistent(thm);
01258     TRACE_MSG("arith ineq", "projectInequalities[inconsistent] => }");
01259     return;
01260   }
01261   else {
01262     if(!e.isTrue() && !e.isEq())
01263       addToBuffer(thm);
01264     else if(e.isEq())
01265       enqueueFact(thm);
01266   }
01267       } else {
01268   IF_DEBUG(debugger.counter("stale inequalities")++);
01269       }
01270     }
01271   }
01272   TRACE_MSG("arith ineq", "projectInequalities => }");
01273 }
01274 
01275 Theorem TheoryArithOld::normalizeProjectIneqs(const Theorem& ineqThm1, 
01276                                            const Theorem& ineqThm2)
01277 {
01278   //ineq1 is of the form beta < b.x  or beta < x  [ or with <= ]
01279   //ineq2 is of the form a.x < alpha   or x < alpha.
01280   Theorem betaLTt = ineqThm1, tLTalpha = ineqThm2;
01281   Expr ineq1 = betaLTt.getExpr();
01282   Expr ineq2 = tLTalpha.getExpr();
01283   Expr c,x;
01284   separateMonomial(ineq2[0], c, x);
01285   Theorem isIntx(isIntegerThm(x));
01286   Theorem isIntBeta(isIntegerThm(ineq1[0]));
01287   Theorem isIntAlpha(isIntegerThm(ineq2[1]));
01288   bool isInt = !(isIntx.isNull() || isIntBeta.isNull() || isIntAlpha.isNull());
01289 
01290   TRACE("arith ineq", "normalizeProjectIneqs(", ineq1,
01291         ", "+ineq2.toString()+") {");
01292   DebugAssert((isLE(ineq1) || isLT(ineq1)) &&
01293               (isLE(ineq2) || isLT(ineq2)),
01294               "TheoryArithOld::normalizeProjectIneqs: Wrong Kind inputs: " +
01295               ineq1.toString() + ineq2.toString());
01296   DebugAssert(!isPlus(ineq1[1]) && !isPlus(ineq2[0]),
01297               "TheoryArithOld::normalizeProjectIneqs: Wrong Kind inputs: " +
01298               ineq1.toString() + ineq2.toString());
01299 
01300   //compute the factors to multiply the two inequalities with
01301   //so that they get the form beta < t and t < alpha.
01302   Rational factor1 = 1, factor2 = 1; 
01303   Rational b = isMult(ineq1[1]) ? (ineq1[1])[0].getRational() : 1;
01304   Rational a = isMult(ineq2[0]) ? (ineq2[0])[0].getRational() : 1;
01305   if(b != a) {
01306     factor1 = a;
01307     factor2 = b;
01308   }
01309 
01310   //if the ineqs are of type int then apply one of the gray
01311   //dark shadow rules.
01312   // FIXME: intResult should also be checked for immediate
01313   // optimizations, as those below for 'result'.  Also, if intResult
01314   // is a single inequality, we may want to handle it similarly to the
01315   // 'result' rather than enqueuing directly.
01316   if(isInt && (a >= 2 || b >= 2)) {
01317     Theorem intResult;
01318     if(a <= b)
01319       intResult = d_rules->darkGrayShadow2ab(betaLTt, tLTalpha,
01320                isIntAlpha, isIntBeta, isIntx);
01321     else 
01322       intResult = d_rules->darkGrayShadow2ba(betaLTt, tLTalpha,
01323                isIntAlpha, isIntBeta, isIntx);
01324     enqueueFact(intResult);
01325     // Fetch dark and gray shadows
01326     DebugAssert(intResult.getExpr().isAnd() && intResult.getExpr().arity()==2,
01327     "intResult = "+intResult.getExpr().toString());
01328     const Expr& DorG = intResult.getExpr()[0];
01329     DebugAssert(DorG.isOr() && DorG.arity()==2, "DorG = "+DorG.toString());
01330     const Expr& D = DorG[0];
01331     const Expr& G = DorG[1];
01332     DebugAssert(D.getKind()==DARK_SHADOW, "D = "+D.toString());
01333     DebugAssert(G.getKind()==GRAY_SHADOW, "G = "+G.toString());
01334     // Set the higher splitter priority for dark shadow
01335     Expr tmp = simplifyExpr(D);
01336     if (!tmp.isBoolConst())
01337       addSplitter(tmp, 5);
01338     // Also set a higher priority to the NEGATION of GRAY_SHADOW
01339     tmp = simplifyExpr(!G);
01340     if (!tmp.isBoolConst())
01341       addSplitter(tmp, 1);
01342     IF_DEBUG(debugger.counter("dark+gray shadows")++);
01343   }
01344 
01345   //actually normalize the inequalities
01346   if(1 != factor1) {
01347     std::vector<Theorem> thms1;
01348     Theorem thm2 = iffMP(betaLTt, d_rules->multIneqn(ineq1, rat(factor1)));
01349     betaLTt = canonPred(thm2);
01350     ineq1 = betaLTt.getExpr();
01351   }
01352   if(1 != factor2) {
01353     std::vector<Theorem> thms1;
01354     Theorem thm2 = iffMP(tLTalpha, d_rules->multIneqn(ineq2, rat(factor2)));
01355     tLTalpha = canonPred(thm2);
01356     ineq2 = tLTalpha.getExpr();
01357   }
01358 
01359   //IF_DEBUG(debugger.counter("real shadows")++);
01360 
01361   Expr beta(ineq1[0]);
01362   Expr alpha(ineq2[1]);
01363   // In case of alpha <= t <= alpha, we generate t = alpha
01364   if(isLE(ineq1) && isLE(ineq2) && alpha == beta) {
01365     Theorem result = d_rules->realShadowEq(betaLTt, tLTalpha);
01366     TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
01367     return result;
01368   }
01369 
01370   // Check if this inequality is a finite interval
01371   if(isInt)
01372     processFiniteInterval(betaLTt, tLTalpha);
01373 
01374   //project the normalized inequalities.
01375 
01376   Theorem result = d_rules->realShadow(betaLTt, tLTalpha);
01377 
01378   // FIXME: Clark's changes.  Is 'rewrite' more or less efficient?
01379 //   result = iffMP(result, rewrite(result.getExpr()));
01380 //   TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
01381 
01382   // Now, transform the result into 0 < rhs and see if rhs is a const 
01383   Expr e(result.getExpr());
01384   // int kind = e.getKind();
01385   if(!(e[0].isRational() && e[0].getRational() == 0)) {
01386     result = iffMP(result, d_rules->rightMinusLeft(e));
01387     result = canonPred(result);
01388   }
01389   
01390   //result is "0 kind e'". where e' is equal to canon(e[1]-e[0])
01391   Expr right = result.getExpr()[1];
01392   // Check for trivial inequality
01393   if (right.isRational())
01394     result = iffMP(result, d_rules->constPredicate(result.getExpr()));
01395   TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
01396   return result;
01397 }
01398 
01399 
01400 Expr TheoryArithOld::pickMonomial(const Expr& right)
01401 {
01402   DebugAssert(isPlus(right), "TheoryArithOld::pickMonomial: Wrong Kind: " + 
01403               right.toString());
01404   if(theoryCore()->getFlags()["var-order"].getBool()) {
01405     Expr::iterator i = right.begin();
01406     Expr isolatedMonomial = right[1];
01407     //PLUS always has at least two elements and the first element is
01408     //always a constant. hence ++i in the initialization of the for
01409     //loop.
01410     for(++i; i != right.end(); ++i)
01411       if(lessThanVar(isolatedMonomial,*i))
01412         isolatedMonomial = *i;
01413     return isolatedMonomial;
01414   }
01415   ExprMap<Expr> var2monomial;
01416   vector<Expr> vars;
01417   Expr::iterator i = right.begin(), iend = right.end();
01418   for(;i != iend; ++i) {
01419     if(i->isRational())
01420       continue;
01421     Expr c, var;
01422     separateMonomial(*i, c, var);
01423     var2monomial[var] = *i;
01424     vars.push_back(var);
01425   }
01426   vector<Expr> largest;
01427   d_graph.selectLargest(vars, largest);
01428   DebugAssert(0 < largest.size(),
01429               "TheoryArithOld::pickMonomial: selectLargest: failed!!!!");
01430   if(1 == largest.size())
01431     return var2monomial[largest[0] ];
01432   else {
01433     size_t pickedVar = 0;
01434     // Pick the variable which will generate the fewest number of
01435     // projections
01436     int minProjections(-1);
01437     for(size_t k=0; k< largest.size(); ++k) {
01438       const Expr& var(largest[k]), monom(var2monomial[var]);
01439       // Grab the counters for the variable
01440       int nRight = (d_countRight.count(var) > 0)? d_countRight[var] : 0;
01441       int nLeft = (d_countLeft.count(var) > 0)? d_countLeft[var] : 0;
01442       int n(nRight*nLeft);
01443       TRACE("arith ineq", "pickMonomial: var=", var,
01444             ", nRight="+int2string(nRight)+", nLeft="+int2string(nLeft));
01445       if(minProjections < 0 || minProjections > n) {
01446         minProjections = n;
01447         pickedVar = k;
01448       }
01449       TRACE("arith ineq", "Number of projections for "+var.toString()+" = ",
01450             n, "");
01451     }
01452     
01453     const Expr& largestVar = largest[pickedVar];
01454     // FIXME: TODO: update the counters (subtract counts for the vars
01455     // other than largestVar
01456 
01457     // Update the graph.
01458     for(size_t k = 0; k < largest.size(); ++k) {
01459       if(k != pickedVar)
01460   d_graph.addEdge(largestVar, largest[k]);
01461     }
01462     return var2monomial[largestVar];
01463   }
01464 }
01465 
01466 void TheoryArithOld::VarOrderGraph::addEdge(const Expr& e1, const Expr& e2)
01467 {
01468   TRACE("arith var order", "addEdge("+e1.toString()+" > ", e2, ")");
01469   DebugAssert(e1 != e2, "TheoryArithOld::VarOrderGraph::addEdge("
01470         +e1.toString()+", "+e2.toString()+")");
01471   d_edges[e1].push_back(e2);
01472 }
01473 
01474 //returns true if e1 < e2, else false(i.e e2 < e1 or e1,e2 are not
01475 //comparable)
01476 bool TheoryArithOld::VarOrderGraph::lessThan(const Expr& e1, const Expr& e2) 
01477 {
01478   d_cache.clear();
01479   //returns true if e1 is in the subtree rooted at e2 implying e1 < e2
01480   return dfs(e1,e2);
01481 }
01482 
01483 //returns true if e1 is in the subtree rooted at e2 implying e1 < e2
01484 bool TheoryArithOld::VarOrderGraph::dfs(const Expr& e1, const Expr& e2)
01485 {
01486   if(e1 == e2)
01487     return true;
01488   if(d_cache.count(e2) > 0)
01489     return false;
01490   if(d_edges.count(e2) == 0)
01491     return false;
01492   d_cache[e2] = true;
01493   vector<Expr>& e2Edges = d_edges[e2];
01494   vector<Expr>::iterator i = e2Edges.begin();
01495   vector<Expr>::iterator iend = e2Edges.end();
01496   //if dfs finds e1 then i != iend else i is equal to iend
01497   for(; i != iend && !dfs(e1,*i); ++i);
01498   return (i != iend);
01499 }
01500 
01501 
01502 void TheoryArithOld::VarOrderGraph::selectSmallest(vector<Expr>& v1,
01503                                                vector<Expr>& v2) 
01504 {
01505   int v1Size = v1.size();
01506   vector<bool> v3(v1Size);
01507   for(int j=0; j < v1Size; ++j)
01508     v3[j] = false;
01509 
01510   for(int j=0; j < v1Size; ++j) {
01511     if(v3[j]) continue;
01512     for(int i =0; i < v1Size; ++i) {
01513       if((i == j) || v3[i]) 
01514         continue;
01515       if(lessThan(v1[i],v1[j])) {
01516         v3[j] = true;
01517         break;
01518       }
01519     }
01520   }
01521   vector<Expr> new_v1;
01522 
01523   for(int j = 0; j < v1Size; ++j) 
01524     if(!v3[j]) v2.push_back(v1[j]);
01525     else new_v1.push_back(v1[j]);
01526   v1 = new_v1;
01527 }
01528 
01529 
01530 void TheoryArithOld::VarOrderGraph::selectLargest(const vector<Expr>& v1,
01531                                                vector<Expr>& v2) 
01532 {
01533   int v1Size = v1.size();
01534   vector<bool> v3(v1Size);
01535   for(int j=0; j < v1Size; ++j)
01536     v3[j] = false;
01537 
01538   for(int j=0; j < v1Size; ++j) {
01539     if(v3[j]) continue;
01540     for(int i =0; i < v1Size; ++i) {
01541       if((i == j) || v3[i]) 
01542         continue;
01543       if(lessThan(v1[j],v1[i])) {
01544         v3[j] = true;
01545         break;
01546       }
01547     }
01548   }
01549   
01550   for(int j = 0; j < v1Size; ++j) 
01551     if(!v3[j]) v2.push_back(v1[j]);
01552 }
01553 
01554 ///////////////////////////////////////////////////////////////////////////////
01555 // TheoryArithOld Public Methods                                                //
01556 ///////////////////////////////////////////////////////////////////////////////
01557 
01558 
01559 TheoryArithOld::TheoryArithOld(TheoryCore* core)
01560   : TheoryArith(core, "ArithmeticOld"),
01561     d_diseq(core->getCM()->getCurrentContext()),
01562     d_diseqIdx(core->getCM()->getCurrentContext(), 0, 0),
01563     d_inModelCreation(core->getCM()->getCurrentContext(), false, 0),
01564     d_freeConstDB(core->getCM()->getCurrentContext()),
01565     d_buffer(core->getCM()->getCurrentContext()),
01566     // Initialize index to 0 at scope 0
01567     d_bufferIdx(core->getCM()->getCurrentContext(), 0, 0),
01568     d_bufferThres(&(core->getFlags()["ineq-delay"].getInt())),
01569     d_countRight(core->getCM()->getCurrentContext()),
01570     d_countLeft(core->getCM()->getCurrentContext()),
01571     d_sharedTerms(core->getCM()->getCurrentContext()),
01572     d_sharedVars(core->getCM()->getCurrentContext())
01573 {
01574   IF_DEBUG(d_diseq.setName("CDList[TheoryArithOld::d_diseq]"));
01575   IF_DEBUG(d_buffer.setName("CDList[TheoryArithOld::d_buffer]"));
01576   IF_DEBUG(d_bufferIdx.setName("CDList[TheoryArithOld::d_bufferIdx]"));
01577 
01578   getEM()->newKind(REAL, "_REAL", true);
01579   getEM()->newKind(INT, "_INT", true);
01580   getEM()->newKind(SUBRANGE, "_SUBRANGE", true);
01581 
01582   getEM()->newKind(UMINUS, "_UMINUS");
01583   getEM()->newKind(PLUS, "_PLUS");
01584   getEM()->newKind(MINUS, "_MINUS");
01585   getEM()->newKind(MULT, "_MULT");
01586   getEM()->newKind(DIVIDE, "_DIVIDE");
01587   getEM()->newKind(POW, "_POW");
01588   getEM()->newKind(INTDIV, "_INTDIV");
01589   getEM()->newKind(MOD, "_MOD");
01590   getEM()->newKind(LT, "_LT");
01591   getEM()->newKind(LE, "_LE");
01592   getEM()->newKind(GT, "_GT");
01593   getEM()->newKind(GE, "_GE");
01594   getEM()->newKind(IS_INTEGER, "_IS_INTEGER");
01595   getEM()->newKind(NEGINF, "_NEGINF");
01596   getEM()->newKind(POSINF, "_POSINF");
01597   getEM()->newKind(DARK_SHADOW, "_DARK_SHADOW");
01598   getEM()->newKind(GRAY_SHADOW, "_GRAY_SHADOW");
01599 
01600   getEM()->newKind(REAL_CONST, "_REAL_CONST");
01601 
01602   vector<int> kinds;
01603   kinds.push_back(REAL);
01604   kinds.push_back(INT);
01605   kinds.push_back(SUBRANGE);
01606   kinds.push_back(IS_INTEGER);
01607   kinds.push_back(UMINUS);
01608   kinds.push_back(PLUS);
01609   kinds.push_back(MINUS);
01610   kinds.push_back(MULT);
01611   kinds.push_back(DIVIDE);
01612   kinds.push_back(POW);
01613   kinds.push_back(INTDIV);
01614   kinds.push_back(MOD);
01615   kinds.push_back(LT);
01616   kinds.push_back(LE);
01617   kinds.push_back(GT);
01618   kinds.push_back(GE);
01619   kinds.push_back(RATIONAL_EXPR);
01620   kinds.push_back(NEGINF);
01621   kinds.push_back(POSINF);
01622   kinds.push_back(DARK_SHADOW);
01623   kinds.push_back(GRAY_SHADOW);
01624   kinds.push_back(REAL_CONST);
01625 
01626   registerTheory(this, kinds, true);
01627 
01628   d_rules = createProofRulesOld();
01629 
01630   d_realType = Type(getEM()->newLeafExpr(REAL));
01631   d_intType  = Type(getEM()->newLeafExpr(INT));
01632 }
01633 
01634 
01635 // Destructor: delete the proof rules class if it's present
01636 TheoryArithOld::~TheoryArithOld() {
01637   if(d_rules != NULL) delete d_rules;
01638   // Clear the inequality databases
01639   for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesRightDB.begin(),
01640   iend=d_inequalitiesRightDB.end(); i!=iend; ++i) {
01641     delete (i->second);
01642     free(i->second);
01643   }
01644   for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesLeftDB.begin(),
01645   iend=d_inequalitiesLeftDB.end(); i!=iend; ++i) {
01646     delete (i->second);
01647     free (i->second);
01648   }
01649 }
01650 
01651 void TheoryArithOld::collectVars(const Expr& e, vector<Expr>& vars,
01652             set<Expr>& cache) {
01653   // Check the cache first
01654   if(cache.count(e) > 0) return;
01655   // Not processed yet.  Cache the expression and proceed
01656   cache.insert(e);
01657   if(isLeaf(e)) vars.push_back(e);
01658   else
01659     for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
01660       collectVars(*i, vars, cache);
01661 }
01662 
01663 void
01664 TheoryArithOld::processFiniteInterval(const Theorem& alphaLEax,
01665            const Theorem& bxLEbeta) {
01666   const Expr& ineq1(alphaLEax.getExpr());
01667   const Expr& ineq2(bxLEbeta.getExpr());
01668   DebugAssert(isLE(ineq1), "TheoryArithOld::processFiniteInterval: ineq1 = "
01669         +ineq1.toString());
01670   DebugAssert(isLE(ineq2), "TheoryArithOld::processFiniteInterval: ineq2 = "
01671         +ineq2.toString());
01672   // If the inequalities are not integer, just return (nothing to do)
01673   if(!isInteger(ineq1[0])
01674      || !isInteger(ineq1[1])
01675      || !isInteger(ineq2[0])
01676      || !isInteger(ineq2[1]))
01677     return;
01678 
01679   const Expr& ax = ineq1[1];
01680   const Expr& bx = ineq2[0];
01681   DebugAssert(!isPlus(ax) && !isRational(ax),
01682         "TheoryArithOld::processFiniteInterval:\n ax = "+ax.toString());
01683   DebugAssert(!isPlus(bx) && !isRational(bx),
01684         "TheoryArithOld::processFiniteInterval:\n bx = "+bx.toString());
01685   Expr a = isMult(ax)? ax[0] : rat(1);
01686   Expr b = isMult(bx)? bx[0] : rat(1);
01687 
01688   Theorem thm1(alphaLEax), thm2(bxLEbeta);
01689   // Multiply the inequalities by 'b' and 'a', and canonize them, if necessary
01690   if(a != b) {
01691     thm1 = canonPred(iffMP(alphaLEax, d_rules->multIneqn(ineq1, b)));
01692     thm2 = canonPred(iffMP(bxLEbeta, d_rules->multIneqn(ineq2, a)));
01693   }
01694   // Check that a*beta - b*alpha == c > 0
01695   const Expr& alphaLEt = thm1.getExpr();
01696   const Expr& alpha = alphaLEt[0];
01697   const Expr& t = alphaLEt[1];
01698   const Expr& beta = thm2.getExpr()[1];
01699   Expr c = canon(beta - alpha).getRHS();
01700 
01701   if(c.isRational() && c.getRational() >= 1) {
01702     // This is a finite interval.  First, derive t <= alpha + c:
01703     // canon(alpha+c) => (alpha+c == beta) ==> [symmetry] beta == alpha+c
01704     // Then substitute that in thm2
01705     Theorem bEQac = symmetryRule(canon(alpha + c));
01706     // Substitute beta == alpha+c for the second child of thm2
01707     vector<unsigned> changed;
01708     vector<Theorem> thms;
01709     changed.push_back(1);
01710     thms.push_back(bEQac);
01711     Theorem tLEac = substitutivityRule(thm2.getExpr(), changed, thms);
01712     tLEac = iffMP(thm2, tLEac);
01713     // Derive and enqueue the finite interval constraint
01714     Theorem isInta(isIntegerThm(alpha));
01715     Theorem isIntt(isIntegerThm(t));
01716     enqueueFact(d_rules->finiteInterval(thm1, tLEac, isInta, isIntt));
01717   }
01718 }
01719 
01720 
01721 void
01722 TheoryArithOld::processFiniteIntervals(const Expr& x) {
01723   // If x is not integer, do not bother
01724   if(!isInteger(x)) return;
01725   // Process every pair of the opposing inequalities for 'x'
01726   ExprMap<CDList<Ineq> *>::iterator iLeft, iRight;
01727   iLeft = d_inequalitiesLeftDB.find(x);
01728   if(iLeft == d_inequalitiesLeftDB.end()) return;
01729   iRight = d_inequalitiesRightDB.find(x);
01730   if(iRight == d_inequalitiesRightDB.end()) return;
01731   // There are some opposing inequalities; get the lists
01732   CDList<Ineq>& ineqsLeft = *(iLeft->second);
01733   CDList<Ineq>& ineqsRight = *(iRight->second);
01734   // Get the sizes of the lists
01735   size_t sizeLeft = ineqsLeft.size();
01736   size_t sizeRight = ineqsRight.size();
01737   // Process all the pairs of the opposing inequalities
01738   for(size_t l=0; l<sizeLeft; ++l)
01739     for(size_t r=0; r<sizeRight; ++r)
01740       processFiniteInterval(ineqsRight[r], ineqsLeft[l]);
01741 }
01742 
01743 /*! This function recursively decends expression tree <strong>without
01744  *  caching</strong> until it hits a node that is already setup.  Be
01745  *  careful on what expressions you are calling it.
01746  */
01747 void
01748 TheoryArithOld::setupRec(const Expr& e) {
01749   if(e.hasFind()) return;
01750   // First, set up the kids recursively
01751   for (int k = 0; k < e.arity(); ++k) {
01752     setupRec(e[k]);
01753   }
01754   // Create a find pointer for e
01755   e.setFind(reflexivityRule(e));
01756   // And call our own setup()   
01757   setup(e);
01758 }
01759 
01760 
01761 /*!
01762  * Keep track of all finitely bounded integer variables in shared
01763  * terms.
01764  *
01765  * When a new shared term t is reported, all of its variables x1...xn
01766  * are added to the set d_sharedVars.  
01767  *
01768  * For each newly added variable x, check all of its opposing
01769  * inequalities, find out all the finite bounds and assert the
01770  * corresponding GRAY_SHADOW constraints.
01771  *
01772  * When projecting integer inequalities, the database d_sharedVars is
01773  * consulted, and if the variable is in it, check the shadows for
01774  * being a finite interval, and produce the additional GRAY_SHADOW
01775  * constraints.
01776  */
01777 void TheoryArithOld::addSharedTerm(const Expr& e) {
01778   d_sharedTerms[e] = true;
01779   /*
01780   set<Expr> cache; // Aux. cache for collecting i-leaves
01781   vector<Expr> vars; // Vector of vars in e
01782   collectVars(e, vars, cache);
01783   for(vector<Expr>::iterator i=vars.begin(), iend=vars.end(); i!=iend; ++i) {
01784     if(d_sharedVars.count(*i) == 0) {
01785       TRACE("arith shared", "TheoryArithOld::addSharedTerm: new var = ", *i, "");
01786       processFiniteIntervals(*i);
01787       d_sharedVars[*i]=true;
01788     }
01789   }
01790   */
01791 }
01792 
01793 
01794 void TheoryArithOld::assertFact(const Theorem& e)
01795 {
01796   const Expr& expr = e.getExpr();
01797   if (expr.isNot() && expr[0].isEq()) {
01798     IF_DEBUG(debugger.counter("[arith] received disequalities")++);
01799     d_diseq.push_back(e);
01800   }
01801   else if (!expr.isEq()){
01802     if (expr.isNot()) {
01803       // This can only be negation of dark or gray shadows, or
01804       // disequalities, which we ignore.  Negations of inequalities
01805       // are handled in rewrite, we don't even receive them here.
01806     } 
01807     else if(isDarkShadow(expr)) {
01808       enqueueFact(d_rules->expandDarkShadow(e));
01809       IF_DEBUG(debugger.counter("received DARK_SHADOW")++);
01810     }
01811     else if(isGrayShadow(expr)) {
01812       IF_DEBUG(debugger.counter("received GRAY_SHADOW")++);
01813       const Rational& c1 = expr[2].getRational();
01814       const Rational& c2 = expr[3].getRational();
01815       const Expr& v = expr[0];
01816       const Expr& ee = expr[1];
01817       if(c1 == c2)
01818   enqueueFact(d_rules->expandGrayShadow0(e));
01819       else {
01820   Theorem gThm(e);
01821   // Check if we can reduce the number of cases in G(ax,c,c1,c2)
01822   if(ee.isRational() && isMult(v)
01823      && v[0].isRational() && v[0].getRational() >= 2) {
01824     IF_DEBUG(debugger.counter("reduced const GRAY_SHADOW")++);
01825     gThm = d_rules->grayShadowConst(e);
01826   }
01827   // (Possibly) new gray shadow
01828   const Expr& g = gThm.getExpr();
01829   if(g.isFalse())
01830     setInconsistent(gThm);
01831   else if(g[2].getRational() == g[3].getRational())
01832     enqueueFact(d_rules->expandGrayShadow0(gThm));
01833   else {
01834     // Assert c1+e <= v <= c2+e
01835     enqueueFact(d_rules->expandGrayShadow(gThm));
01836     // Split G into 2 cases (binary search b/w c1 and c2)
01837     Theorem thm2 = d_rules->splitGrayShadow(gThm);
01838     enqueueFact(thm2);
01839     // Fetch the two gray shadows
01840     DebugAssert(thm2.getExpr().isAnd() && thm2.getExpr().arity()==2,
01841           "thm2 = "+thm2.getExpr().toString());
01842     const Expr& G1orG2 = thm2.getExpr()[0];
01843     DebugAssert(G1orG2.isOr() && G1orG2.arity()==2,
01844           "G1orG2 = "+G1orG2.toString());
01845     const Expr& G1 = G1orG2[0];
01846     const Expr& G2 = G1orG2[1];
01847     DebugAssert(G1.getKind()==GRAY_SHADOW, "G1 = "+G1.toString());
01848     DebugAssert(G2.getKind()==GRAY_SHADOW, "G2 = "+G2.toString());
01849     // Split on the left disjunct first (keep the priority low)
01850           Expr tmp = simplifyExpr(G1);
01851           if (!tmp.isBoolConst())
01852             addSplitter(tmp, 1);
01853           tmp = simplifyExpr(G2);
01854     if (!tmp.isBoolConst())
01855             addSplitter(tmp, -1);
01856   }
01857       }
01858     }
01859     else {
01860       DebugAssert(isLE(expr) || isLT(expr) || isIntPred(expr), 
01861       "expected LE or LT: "+expr.toString());
01862       if(isLE(expr) || isLT(expr)) {
01863   IF_DEBUG(debugger.counter("recevied inequalities")++);
01864   
01865         // Assert the equivalent negated inequality
01866         Theorem thm;
01867         if (isLE(expr)) thm = d_rules->negatedInequality(!gtExpr(expr[0],expr[1]));
01868         else thm = d_rules->negatedInequality(!geExpr(expr[0],expr[1]));
01869         thm = symmetryRule(thm);
01870         Theorem thm2 = simplify(thm.getRHS()[0]);
01871         DebugAssert(thm2.getLHS() != thm2.getRHS(), "Expected rewrite");
01872         thm2 = getCommonRules()->substitutivityRule(thm.getRHS(), thm2);
01873         thm = transitivityRule(thm, thm2);
01874         enqueueFact(iffMP(e, thm));
01875 
01876   // Buffer the inequality
01877   addToBuffer(e);
01878   
01879   TRACE("arith ineq", "buffer.size() = ", d_buffer.size(), 
01880         ", index="+int2string(d_bufferIdx)
01881         +", threshold="+int2string(*d_bufferThres));
01882   
01883   if((((int)d_buffer.size()) - (int)d_bufferIdx > *d_bufferThres) 
01884      && !d_inModelCreation)
01885     processBuffer();
01886       } else {
01887   IF_DEBUG(debugger.counter("arith IS_INTEGER")++);
01888       }
01889     }
01890   }
01891   else {
01892     IF_DEBUG(debugger.counter("[arith] received t1=t2")++);
01893   }
01894 }
01895 
01896 
01897 void TheoryArithOld::checkSat(bool fullEffort)
01898 {
01899   //  vector<Expr>::const_iterator e;
01900   //  vector<Expr>::const_iterator eEnd;
01901   // TODO: convert back to use iterators
01902   TRACE("arith ineq", "TheoryArithOld::checkSat(fullEffort=",
01903         fullEffort? "true" : "false", ")");
01904   if (fullEffort) {
01905     while(!inconsistent() && d_bufferIdx < d_buffer.size())
01906       processBuffer();
01907     if(d_inModelCreation) {
01908       for(; d_diseqIdx < d_diseq.size(); d_diseqIdx = d_diseqIdx+1) {
01909   TRACE("model", "[arith] refining diseq: ",
01910         d_diseq[d_diseqIdx].getExpr() , "");    
01911   enqueueFact(d_rules->diseqToIneq(d_diseq[d_diseqIdx]));
01912       }
01913     }
01914   }
01915 }
01916 
01917 
01918 
01919 void TheoryArithOld::refineCounterExample()
01920 {
01921   d_inModelCreation = true;
01922   TRACE("model", "refineCounterExample[TheoryArithOld] ", "", "{");
01923   CDMap<Expr, bool>::iterator it = d_sharedTerms.begin(), it2,
01924     iend = d_sharedTerms.end();
01925   // Add equalities over all pairs of shared terms as suggested
01926   // splitters.  Notice, that we want to split on equality
01927   // (positively) first, to reduce the size of the model.
01928   for(; it!=iend; ++it) {
01929     // Copy by value: the elements in the pair from *it are NOT refs in CDMap
01930     Expr e1 = (*it).first;
01931     for(it2 = it, ++it2; it2!=iend; ++it2) {
01932       Expr e2 = (*it2).first;
01933       DebugAssert(isReal(getBaseType(e1)),
01934       "TheoryArithOld::refineCounterExample: e1 = "+e1.toString()
01935       +"\n type(e1) = "+e1.getType().toString());
01936       if(findExpr(e1) != findExpr(e2)) {
01937   DebugAssert(isReal(getBaseType(e2)),
01938         "TheoryArithOld::refineCounterExample: e2 = "+e2.toString()
01939         +"\n type(e2) = "+e2.getType().toString());
01940   Expr eq = simplifyExpr(e1.eqExpr(e2));
01941         if (!eq.isBoolConst())
01942           addSplitter(eq);
01943       }
01944     }
01945   }
01946   TRACE("model", "refineCounterExample[Theory::Arith] ", "", "}");
01947 }
01948 
01949 
01950 void
01951 TheoryArithOld::findRationalBound(const Expr& varSide, const Expr& ratSide, 
01952              const Expr& var,
01953              Rational &r)
01954 {
01955   Expr c, x;
01956   separateMonomial(varSide, c, x);
01957   
01958   DebugAssert(findExpr(c).isRational(), 
01959         "seperateMonomial failed"); 
01960   DebugAssert(findExpr(ratSide).isRational(), 
01961         "smallest variable in graph, should not have variables"
01962         " in inequalities: ");
01963   DebugAssert(x == var, "separateMonomial found different variable: " 
01964         + var.toString());
01965   r = findExpr(ratSide).getRational() / findExpr(c).getRational();
01966 } 
01967 
01968 bool
01969 TheoryArithOld::findBounds(const Expr& e, Rational& lub, Rational&  glb)
01970 {
01971   bool strictLB=false, strictUB=false;
01972   bool right = (d_inequalitiesRightDB.count(e) > 0
01973            && d_inequalitiesRightDB[e]->size() > 0);
01974   bool left = (d_inequalitiesLeftDB.count(e) > 0
01975          && d_inequalitiesLeftDB[e]->size() > 0);
01976   int numRight = 0, numLeft = 0;
01977   if(right) { //rationals less than e
01978     CDList<Ineq> * ratsLTe = d_inequalitiesRightDB[e];
01979     for(unsigned int i=0; i<ratsLTe->size(); i++) {
01980       DebugAssert((*ratsLTe)[i].varOnRHS(), "variable on wrong side!");
01981       Expr ineq = (*ratsLTe)[i].ineq().getExpr();
01982       Expr leftSide = ineq[0], rightSide = ineq[1];
01983       Rational r;
01984       findRationalBound(rightSide, leftSide, e , r);
01985       if(numRight==0 || r>glb){
01986   glb = r;
01987   strictLB = isLT(ineq);
01988       }
01989       numRight++;
01990     }
01991     TRACE("model", "   =>Lower bound ", glb.toString(), "");
01992   }
01993   if(left) {   //rationals greater than e
01994     CDList<Ineq> * ratsGTe = d_inequalitiesLeftDB[e];
01995     for(unsigned int i=0; i<ratsGTe->size(); i++) { 
01996       DebugAssert((*ratsGTe)[i].varOnLHS(), "variable on wrong side!");
01997       Expr ineq = (*ratsGTe)[i].ineq().getExpr();
01998       Expr leftSide = ineq[0], rightSide = ineq[1];
01999       Rational r;
02000       findRationalBound(leftSide, rightSide, e, r); 
02001       if(numLeft==0 || r<lub) {
02002   lub = r;
02003   strictUB = isLT(ineq);
02004       }
02005       numLeft++;
02006     }
02007     TRACE("model", "   =>Upper bound ", lub.toString(), "");
02008   }
02009   if(!left && !right) {
02010       lub = 0; 
02011       glb = 0;
02012   }
02013   if(!left && right) {lub = glb +2;}
02014   if(!right && left)  {glb =  lub-2;}
02015   DebugAssert(glb <= lub, "Greatest lower bound needs to be smaller "
02016         "than least upper bound"); 
02017   return strictLB;
02018 }
02019 
02020 void TheoryArithOld::assignVariables(std::vector<Expr>&v)
02021 {
02022   int count = 0;
02023   while (v.size() > 0) {
02024     std::vector<Expr> bottom;
02025     d_graph.selectSmallest(v, bottom);
02026     TRACE("model", "Finding variables to assign. Iteration # ", count, "");
02027     for(unsigned int i = 0; i<bottom.size(); i++) {
02028       Expr e = bottom[i];
02029       TRACE("model", "Found: ", e, "");
02030       // Check if it is already a concrete constant
02031       if(e.isRational()) continue;
02032       
02033       Rational lub, glb;
02034       bool strictLB;
02035       strictLB = findBounds(e, lub, glb);
02036       Rational mid;
02037       if(isInteger(e)) {
02038   if(strictLB && glb.isInteger())
02039     mid = glb + 1;
02040   else
02041     mid = ceil(glb);
02042       }
02043       else
02044   mid = (lub + glb)/2;
02045       TRACE("model", "Assigning mid = ", mid, " {");
02046       assignValue(e, rat(mid));
02047       TRACE("model", "Assigned find(e) = ", findExpr(e), " }");
02048       if(inconsistent()) return; // Punt immediately if failed
02049     }
02050     count++;
02051   }
02052 }
02053 
02054 void TheoryArithOld::computeModelBasic(const std::vector<Expr>& v)
02055 {
02056   d_inModelCreation = true;
02057   vector<Expr> reps;
02058   TRACE("model", "Arith=>computeModel ", "", "{");
02059   for(unsigned int i=0; i <v.size(); ++i) {
02060     const Expr& e = v[i];
02061     if(findExpr(e) == e) {
02062       TRACE("model", "arith variable:", e , "");
02063       reps.push_back(e);
02064     }
02065     else {
02066       TRACE("model", "arith variable:", e , "");
02067       TRACE("model", " ==> is defined by: ", findExpr(e) , "");
02068     }
02069   }
02070   assignVariables(reps);
02071   TRACE("model", "Arith=>computeModel", "", "}");
02072   d_inModelCreation = false;
02073 }
02074 
02075 // For any arith expression 'e', if the subexpressions are assigned
02076 // concrete values, then find(e) must already be a concrete value.
02077 void TheoryArithOld::computeModel(const Expr& e, vector<Expr>& vars) {
02078   DebugAssert(findExpr(e).isRational(), "TheoryArithOld::computeModel("
02079         +e.toString()+")\n e is not assigned concrete value.\n"
02080         +" find(e) = "+findExpr(e).toString());
02081   assignValue(simplify(e));
02082   vars.push_back(e);
02083 }
02084 
02085 
02086 
02087 /*! accepts a rewrite theorem over eqn|ineqn and normalizes it
02088  *  and returns a theorem to that effect. assumes e is non-trivial
02089  *  i.e. e is not '0=const' or 'const=0' or '0 <= const' etc.
02090  */
02091 Theorem TheoryArithOld::normalize(const Expr& e) {
02092   //e is an eqn or ineqn. e is not a trivial eqn or ineqn
02093   //trivial means 0 = const or 0 <= const.
02094   TRACE("arith", "normalize(", e, ") {");
02095   DebugAssert(e.isEq() || isIneq(e),
02096         "normalize: input must be Eq or Ineq: " + e.toString());
02097   DebugAssert(!isIneq(e) || (0 == e[0].getRational()),
02098         "normalize: if (e is ineq) then e[0] must be 0" +
02099         e.toString());
02100   if(e.isEq()) {
02101     if(e[0].isRational()) {
02102       DebugAssert(0 == e[0].getRational(),
02103       "normalize: if e is Eq and e[0] is rat then e[0]==0");
02104     }
02105     else {
02106       //if e[0] is not rational then e[1] must be rational.
02107       DebugAssert(e[1].isRational() && 0 == e[1].getRational(),
02108       "normalize: if e is Eq and e[1] is rat then e[1]==0\n"
02109       " e = "+e.toString());
02110     }
02111   }
02112   
02113   Expr factor;
02114   if(e[0].isRational())
02115     factor = computeNormalFactor(e[1]);
02116   else
02117     factor = computeNormalFactor(e[0]);
02118   
02119   TRACE("arith", "normalize: factor = ", factor, "");
02120   DebugAssert(factor.getRational() > 0,
02121               "normalize: factor="+ factor.toString());
02122   
02123   Theorem thm(reflexivityRule(e));
02124   // Now multiply the equality by the factor, unless it is 1
02125   if(factor.getRational() != 1) {
02126     int kind = e.getKind();
02127     switch(kind) {
02128     case EQ:
02129       thm = d_rules->multEqn(e[0], e[1], factor);
02130       // And canonize the result
02131       thm = canonPredEquiv(thm);
02132       break;
02133     case LE:
02134     case LT:
02135     case GE:
02136     case GT:
02137       thm = d_rules->multIneqn(e, factor);
02138       // And canonize the result
02139       thm = canonPredEquiv(thm);
02140       break;
02141     default:
02142       // MS .net doesn't accept "..." + int
02143       ostringstream ss;
02144       ss << "normalize: control should not reach here " << kind;
02145       DebugAssert(false, ss.str());
02146       break;
02147     }
02148   }
02149   TRACE("arith", "normalize => ", thm, " }");
02150   return(thm);
02151 }
02152 
02153 
02154 Theorem TheoryArithOld::normalize(const Theorem& eIffEqn) {
02155   return transitivityRule(eIffEqn, normalize(eIffEqn.getRHS()));
02156 }
02157 
02158 
02159 Theorem TheoryArithOld::rewrite(const Expr& e)
02160 {
02161   DebugAssert(leavesAreSimp(e), "Expected leaves to be simplified");
02162   TRACE("arith", "TheoryArithOld::rewrite(", e, ") {");
02163   Theorem thm;
02164   if (!e.isTerm()) {
02165     if (!e.isAbsLiteral()) {
02166       e.setRewriteNormal();
02167       thm = reflexivityRule(e);
02168       TRACE("arith", "TheoryArithOld::rewrite[non-literal] => ", thm, " }");
02169       return thm;
02170     }
02171     switch(e.getKind()) {
02172     case EQ:
02173     {
02174       // canonical form for an equality of two leaves
02175       // is just l == r instead of 0 + (-1 * l) + r = 0.
02176       if (isLeaf(e[0]) && isLeaf(e[1]))
02177   thm = reflexivityRule(e);
02178       else { // Otherwise, it is "lhs = 0"
02179   //first convert e to the form 0=e'
02180   if((e[0].isRational() && e[0].getRational() == 0)
02181      || (e[1].isRational() && e[1].getRational() == 0))
02182     //already in 0=e' or e'=0 form
02183     thm = reflexivityRule(e);
02184   else {
02185     thm = d_rules->rightMinusLeft(e);
02186     thm = canonPredEquiv(thm);
02187   }
02188   // Check for trivial equation
02189   if ((thm.getRHS())[0].isRational() && (thm.getRHS())[1].isRational()) {
02190     thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
02191   } else {
02192     //else equation is non-trivial
02193     thm = normalize(thm);
02194     // Normalization may yield non-simplified terms
02195     thm = canonPredEquiv(thm);
02196 
02197   }
02198       }
02199 
02200       // Equations must be oriented such that lhs >= rhs as Exprs;
02201       // this ordering is given by operator<(Expr,Expr).
02202       const Expr& eq = thm.getRHS();
02203       if(eq.isEq() && eq[0] < eq[1])
02204   thm = transitivityRule(thm, getCommonRules()->rewriteUsingSymmetry(eq));
02205     }
02206     break;
02207     case GRAY_SHADOW:
02208     case DARK_SHADOW:
02209       thm = reflexivityRule(e);
02210       break;
02211     case IS_INTEGER: {
02212       Theorem res(isIntegerDerive(e, typePred(e[0])));
02213       if(!res.isNull())
02214   thm = getCommonRules()->iffTrue(res);
02215       else 
02216   thm = reflexivityRule(e);
02217       break;
02218     }
02219     case NOT:    
02220       if (!isIneq(e[0]))
02221   //in this case we have "NOT of DARK or GRAY_SHADOW."
02222   thm = reflexivityRule(e);
02223       else {
02224   //In this case we have the "NOT of ineq". get rid of NOT
02225   //and then treat like an ineq
02226   thm = d_rules->negatedInequality(e);
02227   DebugAssert(isGE(thm.getRHS()) || isGT(thm.getRHS()),
02228         "Expected GE or GT");
02229   thm = transitivityRule(thm, d_rules->flipInequality(thm.getRHS()));
02230   thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
02231   thm = canonPredEquiv(thm);
02232 
02233   // Check for trivial inequation
02234   if ((thm.getRHS())[1].isRational())
02235     thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
02236   else {
02237     //else ineq is non-trivial
02238     thm = normalize(thm);
02239     // Normalization may yield non-simplified terms
02240     thm = canonPredEquiv(thm);
02241   }
02242       }
02243       break;
02244     case LE:
02245     case LT:
02246     case GE:
02247     case GT:
02248       if (isGE(e) || isGT(e)) {
02249   thm = d_rules->flipInequality(e);
02250   thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
02251       }
02252       else 
02253   thm = d_rules->rightMinusLeft(e);
02254       thm = canonPredEquiv(thm);
02255    
02256       // Check for trivial inequation
02257       if ((thm.getRHS())[1].isRational()) 
02258   thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
02259       else { // ineq is non-trivial
02260   thm = normalize(thm);
02261   thm = canonPredEquiv(thm);
02262       }
02263       break;
02264     default:
02265       DebugAssert(false,
02266       "Theory_Arith::rewrite: control should not reach here");
02267       break;
02268     }
02269   }
02270   else {
02271     if (e.isAtomic())
02272       thm = canon(e);
02273     else 
02274       thm = reflexivityRule(e);
02275   }
02276   // Arith canonization is idempotent
02277   if (theoryOf(thm.getRHS()) == this)
02278     thm.getRHS().setRewriteNormal();
02279   TRACE("arith", "TheoryArithOld::rewrite => ", thm, " }");
02280   return thm;
02281 }
02282 
02283 
02284 void TheoryArithOld::setup(const Expr& e)
02285 {
02286   if (!e.isTerm()) {
02287     if (e.isNot() || e.isEq() || isDarkShadow(e) || isGrayShadow(e)) return;
02288     if(e.getKind() == IS_INTEGER) {
02289       e[0].addToNotify(this, e);
02290       return;
02291     }
02292     DebugAssert((isLT(e)||isLE(e)) &&
02293                 e[0].isRational() && e[0].getRational() == 0,
02294                 "TheoryArithOld::setup: expected 0 < rhs:" + e.toString());
02295     e[1].addToNotify(this, e);
02296     return;
02297   }
02298   int k(0), ar(e.arity());
02299   for ( ; k < ar; ++k) {
02300     e[k].addToNotify(this, e);
02301     TRACE("arith setup", "e["+int2string(k)+"]: ", *(e[k].getNotify()), "");
02302   }
02303 }
02304 
02305 
02306 void TheoryArithOld::update(const Theorem& e, const Expr& d)
02307 {
02308   if (inconsistent()) return;
02309   IF_DEBUG(debugger.counter("arith update total")++);
02310   if (!d.hasFind()) return;
02311   if (isIneq(d)) {
02312     // Substitute e[1] for e[0] in d and enqueue new inequality
02313     DebugAssert(e.getLHS() == d[1], "Mismatch");
02314     Theorem thm = find(d);
02315     //    DebugAssert(thm.getRHS() == trueExpr(), "Expected find = true");
02316     vector<unsigned> changed;
02317     vector<Theorem> children;
02318     changed.push_back(1);
02319     children.push_back(e);
02320     Theorem thm2 = substitutivityRule(d, changed, children);
02321     if (thm.getRHS() == trueExpr()) {
02322       enqueueFact(iffMP(getCommonRules()->iffTrueElim(thm), thm2));
02323     }
02324     else {
02325       enqueueFact(getCommonRules()->iffFalseElim(
02326         transitivityRule(symmetryRule(thm2), thm)));
02327     }
02328     IF_DEBUG(debugger.counter("arith update ineq")++);
02329   }
02330   else if (find(d).getRHS() == d) {
02331     // Substitute e[1] for e[0] in d and assert the result equal to d
02332     Theorem thm = canonSimp(d);
02333     TRACE("arith", "TheoryArithOld::update(): thm = ", thm, "");
02334     DebugAssert(leavesAreSimp(thm.getRHS()), "updateHelper error: "
02335     +thm.getExpr().toString());
02336     assertEqualities(transitivityRule(thm, rewrite(thm.getRHS())));
02337     IF_DEBUG(debugger.counter("arith update find(d)=d")++);
02338   }
02339 }
02340 
02341 
02342 Theorem TheoryArithOld::solve(const Theorem& thm)
02343 {
02344   DebugAssert(thm.isRewrite() && thm.getLHS().isTerm(), "");
02345   const Expr& lhs = thm.getLHS();
02346   const Expr& rhs = thm.getRHS();
02347 
02348   // Check for already solved equalities.
02349 
02350   // Have to be careful about the types: integer variable cannot be
02351   // assigned a real term.  Also, watch for e[0] being a subexpression
02352   // of e[1]: this would create an unsimplifiable expression.
02353   if (isLeaf(lhs) && !isLeafIn(lhs, rhs) 
02354       && (lhs.getType() != intType() || isInteger(rhs))
02355       // && !e[0].subExprOf(e[1])
02356       )
02357     return thm;
02358 
02359   // Symmetric version is already solved
02360   if (isLeaf(rhs) && !isLeafIn(rhs, lhs)
02361       && (rhs.getType() != intType() || isInteger(lhs))
02362       // && !e[1].subExprOf(e[0])
02363       )
02364     return symmetryRule(thm);
02365 
02366   return doSolve(thm);
02367 }
02368 
02369 
02370 void TheoryArithOld::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
02371   switch(e.getKind()) {
02372   case RATIONAL_EXPR: // Skip the constants
02373     break;
02374   case PLUS:
02375   case MULT:
02376   case DIVIDE:
02377   case POW: // This is not a variable; extract the variables from children
02378     for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
02379       // getModelTerm(*i, v);
02380       v.push_back(*i);
02381     break;
02382   default: { // Otherwise it's a variable.  Check if it has a find pointer
02383     Expr e2(findExpr(e));
02384     if(e==e2) {
02385       TRACE("model", "TheoryArithOld::computeModelTerm(", e, "): a variable");
02386       // Leave it alone (it has no descendants)
02387       // v.push_back(e);
02388     } else {
02389       TRACE("model", "TheoryArithOld::computeModelTerm("+e.toString()
02390       +"): has find pointer to ", e2, "");
02391       v.push_back(e2);
02392     }
02393   }
02394   }
02395 }
02396 
02397 
02398 Expr TheoryArithOld::computeTypePred(const Type& t, const Expr& e) {
02399   Expr tExpr = t.getExpr();
02400   switch(tExpr.getKind()) {
02401   case INT:  
02402     return Expr(IS_INTEGER, e);
02403   case SUBRANGE: {
02404     std::vector<Expr> kids;
02405     kids.push_back(Expr(IS_INTEGER, e));
02406     kids.push_back(leExpr(tExpr[0], e));
02407     kids.push_back(leExpr(e, tExpr[1]));
02408     return andExpr(kids);
02409   }
02410   default:
02411     return e.getEM()->trueExpr();
02412   }
02413 }
02414 
02415 
02416 void TheoryArithOld::checkAssertEqInvariant(const Theorem& e)
02417 {
02418   if (e.isRewrite()) {
02419     DebugAssert(e.getLHS().isTerm(), "Expected equation");
02420     if (isLeaf(e.getLHS())) {
02421       // should be in solved form
02422       DebugAssert(!isLeafIn(e.getLHS(),e.getRHS()),
02423                   "Not in solved form: lhs appears in rhs");
02424     }
02425     else {
02426       DebugAssert(e.getLHS().hasFind(), "Expected lhs to have find");
02427       DebugAssert(!leavesAreSimp(e.getLHS()),
02428                   "Expected at least one unsimplified leaf on lhs");
02429     }
02430     DebugAssert(canonSimp(e.getRHS()).getRHS() == e.getRHS(),
02431                 "Expected canonSimp(rhs) = canonSimp(rhs)");
02432   }
02433   else {
02434     Expr expr = e.getExpr();
02435     if (expr.isFalse()) return;
02436 
02437     vector<Theorem> eqs;
02438     Theorem thm;
02439     int index, index2;
02440 
02441     for (index = 0; index < expr.arity(); ++index) {
02442       thm = getCommonRules()->andElim(e, index);
02443       eqs.push_back(thm);
02444       if (thm.getExpr().isFalse()) return;
02445       DebugAssert(eqs[index].isRewrite() &&
02446                   eqs[index].getLHS().isTerm(), "Expected equation");
02447     }
02448 
02449     // Check for solved form
02450     for (index = 0; index < expr.arity(); ++index) {
02451       DebugAssert(isLeaf(eqs[index].getLHS()), "expected leaf on lhs");
02452       DebugAssert(canonSimp(eqs[index].getRHS()).getRHS() == eqs[index].getRHS(),
02453                   "Expected canonSimp(rhs) = canonSimp(rhs)");
02454       DebugAssert(recursiveCanonSimpCheck(eqs[index].getRHS()),
02455                   "Failed recursive canonSimp check");
02456       for (index2 = 0; index2 < expr.arity(); ++index2) {
02457         DebugAssert(index == index2 ||
02458                     eqs[index].getLHS() != eqs[index2].getLHS(),
02459                     "Not in solved form: repeated lhs");
02460         DebugAssert(!isLeafIn(eqs[index].getLHS(),eqs[index2].getRHS()),
02461                     "Not in solved form: lhs appears in rhs");
02462       }
02463     }    
02464   }
02465 }
02466 
02467 
02468 void TheoryArithOld::checkType(const Expr& e)
02469 {
02470   switch (e.getKind()) {
02471     case INT:
02472     case REAL:
02473       if (e.arity() > 0) {
02474         throw Exception("Ill-formed arithmetic type: "+e.toString());
02475       }
02476       break;
02477     case SUBRANGE:
02478       if (e.arity() != 2 ||
02479           !isIntegerConst(e[0]) ||
02480           !isIntegerConst(e[1]) ||
02481           e[0].getRational() > e[1].getRational()) {
02482         throw Exception("bad SUBRANGE type expression"+e.toString());
02483       }
02484       break;
02485     default:
02486       DebugAssert(false, "Unexpected kind in TheoryArithOld::checkType"
02487                   +getEM()->getKindName(e.getKind()));
02488   }
02489 }
02490 
02491 
02492 void TheoryArithOld::computeType(const Expr& e)
02493 {
02494   switch (e.getKind()) {
02495     case REAL_CONST:
02496       e.setType(d_realType);
02497       break;
02498     case RATIONAL_EXPR:
02499       if(e.getRational().isInteger())
02500         e.setType(d_intType);
02501       else
02502         e.setType(d_realType);
02503       break;
02504     case UMINUS:
02505     case PLUS:
02506     case MINUS:
02507     case MULT:
02508     case POW: {
02509       bool isInt = true;
02510       for(int k = 0; k < e.arity(); ++k) {
02511         if(d_realType != getBaseType(e[k]))
02512           throw TypecheckException("Expecting type REAL with `" +
02513                                    getEM()->getKindName(e.getKind()) + "',\n"+
02514                                    "but got a " + getBaseType(e[k]).toString()+ 
02515                                    " for:\n" + e.toString());
02516         if(isInt && !isInteger(e[k]))
02517           isInt = false;
02518       }
02519       if(isInt)
02520         e.setType(d_intType);
02521       else
02522         e.setType(d_realType);
02523       break;
02524     }
02525     case DIVIDE: {
02526       Expr numerator = e[0];
02527       Expr denominator = e[1];
02528       if (getBaseType(numerator) != d_realType ||
02529           getBaseType(denominator) != d_realType) {
02530         throw TypecheckException("Expecting only REAL types with `DIVIDE',\n"
02531                                  "but got " + getBaseType(numerator).toString()+ 
02532                                  " and " + getBaseType(denominator).toString() +
02533                                  " for:\n" + e.toString());
02534       }
02535       if(denominator.isRational() && 1 == denominator.getRational())
02536         e.setType(numerator.getType());
02537       else
02538         e.setType(d_realType);
02539       break;
02540     }
02541     case LT:
02542     case LE:
02543     case GT:
02544     case GE:
02545     case GRAY_SHADOW:
02546       // Need to know types for all exprs -Clark
02547       //    e.setType(boolType());
02548       //    break;
02549     case DARK_SHADOW:
02550       for (int k = 0; k < e.arity(); ++k) {
02551         if (d_realType != getBaseType(e[k]))
02552           throw TypecheckException("Expecting type REAL with `" +
02553                                    getEM()->getKindName(e.getKind()) + "',\n"+
02554                                    "but got a " + getBaseType(e[k]).toString()+ 
02555                                    " for:\n" + e.toString());
02556       }
02557       
02558       e.setType(boolType());
02559       break;
02560     case IS_INTEGER:
02561       if(d_realType != getBaseType(e[0]))
02562         throw TypecheckException("Expected type REAL, but got "
02563                                  +getBaseType(e[0]).toString()
02564                                  +"\n\nExpr = "+e.toString());
02565       e.setType(boolType());
02566       break;
02567     default:
02568       DebugAssert(false,"TheoryArithOld::computeType: unexpected expression:\n "
02569                   +e.toString());
02570       break;
02571   }
02572 }
02573 
02574 
02575 Type TheoryArithOld::computeBaseType(const Type& t) {
02576   IF_DEBUG(int kind = t.getExpr().getKind());
02577   DebugAssert(kind==INT || kind==REAL || kind==SUBRANGE,
02578         "TheoryArithOld::computeBaseType("+t.toString()+")");
02579   return realType();
02580 }
02581 
02582 
02583 Expr
02584 TheoryArithOld::computeTCC(const Expr& e) {
02585   Expr tcc(Theory::computeTCC(e));
02586   switch(e.getKind()) {
02587   case DIVIDE:
02588     DebugAssert(e.arity() == 2, "");
02589     return tcc.andExpr(!(e[1].eqExpr(rat(0))));
02590   default:
02591     return tcc;
02592   }
02593 }
02594 
02595 ///////////////////////////////////////////////////////////////////////////////
02596 //parseExprOp:
02597 //translating special Exprs to regular EXPR??
02598 ///////////////////////////////////////////////////////////////////////////////
02599 Expr
02600 TheoryArithOld::parseExprOp(const Expr& e) {
02601   TRACE("parser", "TheoryArithOld::parseExprOp(", e, ")");
02602   //std::cout << "Were here";
02603   // If the expression is not a list, it must have been already
02604   // parsed, so just return it as is.
02605   switch(e.getKind()) {
02606   case ID: {
02607     int kind = getEM()->getKind(e[0].getString());
02608     switch(kind) {
02609     case NULL_KIND: return e; // nothing to do
02610     case REAL:
02611     case INT:
02612     case NEGINF: 
02613     case POSINF: return getEM()->newLeafExpr(kind);
02614     default:
02615       DebugAssert(false, "Bad use of bare keyword: "+e.toString());
02616       return e;
02617     }
02618   }
02619   case RAW_LIST: break; // break out of switch, do the hard work
02620   default:
02621     return e;
02622   }
02623 
02624   DebugAssert(e.getKind() == RAW_LIST && e.arity() > 0,
02625         "TheoryArithOld::parseExprOp:\n e = "+e.toString());
02626   
02627   const Expr& c1 = e[0][0];
02628   int kind = getEM()->getKind(c1.getString());
02629   switch(kind) {
02630     case UMINUS: {
02631       if(e.arity() != 2)
02632   throw ParserException("UMINUS requires exactly one argument: "
02633       +e.toString());
02634       return uminusExpr(parseExpr(e[1])); 
02635     }
02636     case PLUS: {
02637       vector<Expr> k;
02638       Expr::iterator i = e.begin(), iend=e.end();
02639       // Skip first element of the vector of kids in 'e'.
02640       // The first element is the operator.
02641       ++i; 
02642       // Parse the kids of e and push them into the vector 'k'
02643       for(; i!=iend; ++i) k.push_back(parseExpr(*i));
02644       return plusExpr(k); 
02645     }
02646     case MINUS: {
02647       if(e.arity() == 2)
02648   return uminusExpr(parseExpr(e[1]));
02649       else if(e.arity() == 3)
02650   return minusExpr(parseExpr(e[1]), parseExpr(e[2]));
02651       else
02652   throw ParserException("MINUS requires one or two arguments:"
02653       +e.toString());
02654     }
02655     case MULT: {
02656       vector<Expr> k;
02657       Expr::iterator i = e.begin(), iend=e.end();
02658       // Skip first element of the vector of kids in 'e'.
02659       // The first element is the operator.
02660       ++i; 
02661       // Parse the kids of e and push them into the vector 'k'
02662       for(; i!=iend; ++i) k.push_back(parseExpr(*i));
02663       return multExpr(k);
02664     }
02665     case POW: { 
02666       return powExpr(parseExpr(e[1]), parseExpr(e[2])); 
02667     }
02668     case DIVIDE:
02669       { return divideExpr(parseExpr(e[1]), parseExpr(e[2]));  }
02670     case LT:  
02671       { return ltExpr(parseExpr(e[1]), parseExpr(e[2]));  }
02672     case LE:  
02673       { return leExpr(parseExpr(e[1]), parseExpr(e[2]));  }
02674     case GT:  
02675       { return gtExpr(parseExpr(e[1]), parseExpr(e[2]));  }
02676     case GE:  
02677       { return geExpr(parseExpr(e[1]), parseExpr(e[2]));  }
02678     case INTDIV:
02679     case MOD:
02680     case SUBRANGE: {
02681       vector<Expr> k;
02682       Expr::iterator i = e.begin(), iend=e.end();
02683       // Skip first element of the vector of kids in 'e'.
02684       // The first element is the operator.
02685       ++i; 
02686       // Parse the kids of e and push them into the vector 'k'
02687       for(; i!=iend; ++i) 
02688         k.push_back(parseExpr(*i));
02689       return Expr(kind, k, e.getEM());
02690     }
02691     case IS_INTEGER: {
02692       if(e.arity() != 2)
02693   throw ParserException("IS_INTEGER requires exactly one argument: "
02694       +e.toString());
02695       return Expr(IS_INTEGER, parseExpr(e[1]));
02696     }
02697     default:
02698       DebugAssert(false,
02699         "TheoryArithOld::parseExprOp: invalid input " + e.toString());
02700       break;
02701   }
02702   return e;
02703 }
02704 
02705 ///////////////////////////////////////////////////////////////////////////////
02706 // Pretty-printing                                                           //
02707 ///////////////////////////////////////////////////////////////////////////////
02708 
02709 
02710 ExprStream&
02711 TheoryArithOld::print(ExprStream& os, const Expr& e) {
02712   switch(os.lang()) {
02713     case SIMPLIFY_LANG:
02714       switch(e.getKind()) {
02715       case RATIONAL_EXPR:
02716   e.print(os);
02717   break;
02718       case SUBRANGE:
02719   os <<"ERROR:SUBRANGE:not supported in Simplify\n";
02720   break;
02721       case IS_INTEGER:
02722   os <<"ERROR:IS_INTEGER:not supported in Simplify\n";
02723   break;
02724       case PLUS:  {
02725   int i=0, iend=e.arity();
02726   os << "(+ "; 
02727   if(i!=iend) os << e[i];
02728   ++i;
02729   for(; i!=iend; ++i) os << " " << e[i];
02730   os <<  ")";
02731   break;
02732       }
02733       case MINUS:
02734   os << "(- " << e[0] << " " << e[1]<< ")";
02735   break;
02736       case UMINUS:
02737   os << "-" << e[0] ;
02738   break;
02739       case MULT:  {
02740   int i=0, iend=e.arity();
02741   os << "(* " ;
02742   if(i!=iend) os << e[i];
02743   ++i;
02744   for(; i!=iend; ++i) os << " " << e[i];
02745   os <<  ")";
02746   break;
02747       }
02748       case POW:
02749           os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
02750           break;
02751       case DIVIDE:
02752   os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
02753   break;
02754       case LT:
02755   if (isInt(e[0].getType()) || isInt(e[1].getType())) {
02756   }
02757   os << "(< " << e[0] << " " << e[1] <<")";
02758   break;
02759       case LE:
02760           os << "(<= " << e[0]  << " " << e[1] << ")";
02761           break;
02762       case GT:
02763   os << "(> " << e[0] << " " << e[1] << ")";
02764   break;
02765       case GE:
02766   os << "(>= " << e[0] << " " << e[1]  << ")";
02767   break;
02768       case DARK_SHADOW:
02769       case GRAY_SHADOW:
02770   os <<"ERROR:SHADOW:not supported in Simplify\n";
02771   break;
02772       default:
02773   // Print the top node in the default LISP format, continue with
02774   // pretty-printing for children.
02775           e.print(os);
02776     
02777           break;
02778       } 
02779       break; // end of case SIMPLIFY_LANG
02780       
02781     case PRESENTATION_LANG:
02782       switch(e.getKind()) {
02783         case REAL:
02784         case INT:
02785         case RATIONAL_EXPR:
02786         case NEGINF:
02787         case POSINF:
02788           e.print(os);
02789           break;
02790         case SUBRANGE:
02791           if(e.arity() != 2) e.printAST(os);
02792           else 
02793             os << "[" << push << e[0] << ".." << e[1] << push << "]";
02794           break;
02795         case IS_INTEGER:
02796     if(e.arity() == 1)
02797       os << "IS_INTEGER(" << push << e[0] << push << ")";
02798     else
02799       e.printAST(os);
02800     break;
02801         case PLUS:  {
02802           int i=0, iend=e.arity();
02803           os << "(" << push;
02804           if(i!=iend) os << e[i];
02805           ++i;
02806           for(; i!=iend; ++i) os << space << "+ " << e[i];
02807           os << push << ")";
02808           break;
02809         }
02810         case MINUS:
02811           os << "(" << push << e[0] << space << "- " << e[1] << push << ")";
02812           break;
02813         case UMINUS:
02814           os << "-(" << push << e[0] << push << ")";
02815           break;
02816         case MULT:  {
02817           int i=0, iend=e.arity();
02818           os << "(" << push;
02819           if(i!=iend) os << e[i];
02820           ++i;
02821           for(; i!=iend; ++i) os << space << "* " << e[i];
02822           os << push << ")";
02823           break;
02824         }
02825         case POW:
02826           os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
02827           break;
02828         case DIVIDE:
02829           os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
02830           break;
02831         case LT:
02832           if (isInt(e[0].getType()) || isInt(e[1].getType())) {
02833           }
02834           os << "(" << push << e[0] << space << "< " << e[1] << push << ")";
02835           break;
02836         case LE:
02837           os << "(" << push << e[0] << space << "<= " << e[1] << push << ")";
02838           break;
02839         case GT:
02840           os << "(" << push << e[0] << space << "> " << e[1] << push << ")";
02841           break;
02842         case GE:
02843           os << "(" << push << e[0] << space << ">= " << e[1] << push << ")";
02844           break;
02845         case DARK_SHADOW:
02846     os << "DARK_SHADOW(" << push << e[0] << ", " << space << e[1] << push << ")";
02847     break;
02848         case GRAY_SHADOW:
02849     os << "GRAY_SHADOW(" << push << e[0] << ","  << space << e[1]
02850        << "," << space << e[2] << "," << space << e[3] << push << ")";
02851     break;
02852         default:
02853           // Print the top node in the default LISP format, continue with
02854           // pretty-printing for children.
02855           e.printAST(os);
02856 
02857           break;
02858       } 
02859       break; // end of case PRESENTATION_LANG
02860     case SMTLIB_LANG: {
02861       switch(e.getKind()) {
02862         case REAL_CONST:
02863           printRational(os, e[0].getRational(), true);
02864           break;
02865         case RATIONAL_EXPR:
02866           printRational(os, e.getRational());
02867           break;
02868         case REAL:
02869           os << "Real";
02870           break;
02871         case INT:
02872           os << "Int";
02873           break;
02874         case SUBRANGE:
02875           throw SmtlibException("TheoryArithOld::print: SMTLIB: SUBRANGE not implemented");
02876 //           if(e.arity() != 2) e.print(os);
02877 //           else 
02878 //             os << "(" << push << "SUBRANGE" << space << e[0]
02879 //         << space << e[1] << push << ")";
02880           break;
02881         case IS_INTEGER:
02882     if(e.arity() == 1)
02883       os << "(" << push << "IsInt" << space << e[0] << push << ")";
02884     else
02885             throw SmtlibException("TheoryArithOld::print: SMTLIB: IS_INTEGER used unexpectedly");
02886     break;
02887         case PLUS:  {
02888           os << "(" << push << "+";
02889           Expr::iterator i = e.begin(), iend = e.end();
02890           for(; i!=iend; ++i) {
02891             os << space << (*i);
02892           }
02893           os << push << ")";
02894           break;
02895         }
02896         case MINUS: {
02897           os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
02898           break;
02899         }
02900         case UMINUS: {
02901           os << "(" << push << "-" << space << e[0] << push << ")";
02902           break;
02903         }
02904         case MULT:  {
02905           int i=0, iend=e.arity();
02906           for(; i!=iend; ++i) {
02907             if (i < iend-1) {
02908               os << "(" << push << "*";
02909             }
02910             os << space << e[i];
02911           }
02912           for (i=0; i < iend-1; ++i) os << push << ")";
02913           break;
02914         }
02915         case POW:
02916           throw SmtlibException("TheoryArithOld::print: SMTLIB: POW not supported");
02917           //          os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
02918           break;
02919         case DIVIDE: {
02920           throw SmtlibException("TheoryArithOld::print: SMTLIB: unexpected use of DIVIDE");
02921           break;
02922         }
02923         case LT: {
02924           Rational r;
02925           os << "(" << push << "<" << space;
02926           os << e[0] << space << e[1] << push << ")";
02927           break;
02928         }
02929         case LE: {
02930           Rational r;
02931           os << "(" << push << "<=" << space;
02932           os << e[0] << space << e[1] << push << ")";
02933           break;
02934         }
02935         case GT: {
02936           Rational r;
02937           os << "(" << push << ">" << space;
02938           os << e[0] << space << e[1] << push << ")";
02939           break;
02940         }
02941         case GE: {
02942           Rational r;
02943           os << "(" << push << ">=" << space;
02944           os << e[0] << space << e[1] << push << ")";
02945           break;
02946         }
02947         case DARK_SHADOW:
02948           throw SmtlibException("TheoryArithOld::print: SMTLIB: DARK_SHADOW not supported");
02949     os << "(" << push << "DARK_SHADOW" << space << e[0]
02950        << space << e[1] << push << ")";
02951     break;
02952         case GRAY_SHADOW:
02953           throw SmtlibException("TheoryArithOld::print: SMTLIB: GRAY_SHADOW not supported");
02954     os << "GRAY_SHADOW(" << push << e[0] << ","  << space << e[1]
02955        << "," << space << e[2] << "," << space << e[3] << push << ")";
02956     break;
02957         default:
02958           throw SmtlibException("TheoryArithOld::print: SMTLIB: default not supported");
02959           // Print the top node in the default LISP format, continue with
02960           // pretty-printing for children.
02961           e.printAST(os);
02962 
02963           break;
02964       } 
02965       break; // end of case SMTLIB_LANG
02966     }
02967     case LISP_LANG:
02968       switch(e.getKind()) {
02969         case REAL:
02970         case INT:
02971         case RATIONAL_EXPR:
02972         case NEGINF:
02973         case POSINF:
02974           e.print(os);
02975           break;
02976         case SUBRANGE:
02977           if(e.arity() != 2) e.printAST(os);
02978           else 
02979             os << "(" << push << "SUBRANGE" << space << e[0]
02980          << space << e[1] << push << ")";
02981           break;
02982         case IS_INTEGER:
02983     if(e.arity() == 1)
02984       os << "(" << push << "IS_INTEGER" << space << e[0] << push << ")";
02985     else
02986       e.printAST(os);
02987     break;
02988         case PLUS:  {
02989           int i=0, iend=e.arity();
02990           os << "(" << push << "+";
02991           for(; i!=iend; ++i) os << space << e[i];
02992           os << push << ")";
02993           break;
02994         }
02995         case MINUS:
02996         //os << "(" << push << e[0] << space << "- " << e[1] << push << ")";
02997     os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
02998           break;
02999         case UMINUS:
03000           os << "(" << push << "-" << space << e[0] << push << ")";
03001           break;
03002         case MULT:  {
03003           int i=0, iend=e.arity();
03004           os << "(" << push << "*";
03005           for(; i!=iend; ++i) os << space << e[i];
03006           os << push << ")";
03007           break;
03008         }
03009         case POW:
03010           os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
03011           break;
03012         case DIVIDE:
03013           os << "(" << push << "/ " << e[0] << space << e[1] << push << ")";
03014           break;
03015         case LT:
03016           os << "(" << push << "< " << e[0] << space << e[1] << push << ")";
03017           break;
03018         case LE:
03019           os << "(" << push << "<= " << e[0] << space << e[1] << push << ")";
03020           break;
03021         case GT:
03022           os << "(" << push << "> " << e[1]  << space << e[0] << push << ")";
03023           break;
03024         case GE:
03025           os << "(" << push << ">= " << e[0] << space << e[1] << push << ")";
03026           break;
03027         case DARK_SHADOW:
03028     os << "(" << push << "DARK_SHADOW" << space << e[0]
03029        << space << e[1] << push << ")";
03030     break;
03031         case GRAY_SHADOW:
03032     os << "(" << push << "GRAY_SHADOW" << space << e[0] << space
03033        << e[1] << space << e[2] << space << e[3] << push << ")";
03034     break;
03035         default:
03036           // Print the top node in the default LISP format, continue with
03037           // pretty-printing for children.
03038           e.printAST(os);
03039 
03040           break;
03041       } 
03042       break; // end of case LISP_LANG
03043     default:
03044      // Print the top node in the default LISP format, continue with
03045      // pretty-printing for children.
03046        e.printAST(os);
03047   }
03048   return os;
03049 }
03050 
03051 
03052 //! Construct the gray shadow expression representing c1 <= e <= c2
03053 // Expr TheoryArithOld::grayShadow(const Expr& v, const Expr& e,
03054 //           const Rational& c1, const Rational& c2) {
03055 //   ExprGrayShadow ev(getEM(), v, e, c1, c2, d_grayShadowMMIndex);
03056 //   return getEM()->newExpr(&ev);
03057 // }
03058 
03059 
03060 //! Access lhs constant in gray shadow
03061 // const Rational& TheoryArithOld::getC1(const Expr& e) {
03062 //   DebugAssert(isGrayShadow(e),
03063 //        "TheoryArithOld::getC1("+e.toString()
03064 //        +"): not a gray shadow");
03065 //   return e.getRatValue(0);
03066 // }
03067 
03068 
03069 //! Access rhs constant in gray shadow
03070 // const Rational& TheoryArithOld::getC2(const Expr& e) {
03071 //   DebugAssert(isGrayShadow(e),
03072 //        "TheoryArithOld::getC2("+e.toString()
03073 //        +"): not a gray shadow");
03074 //   return e.getRatValue(1);
03075 // }
03076 
03077 
03078 //! Access the monomial in gray shadow
03079 // const Expr& TheoryArithOld::getV(const Expr& e) {
03080 //   DebugAssert(isGrayShadow(e),
03081 //        "TheoryArithOld::getV("+e.toString()
03082 //        +"): not a gray shadow");
03083 //   return e.getExprValue(0);
03084 // }
03085 
03086 //! Access the expression in gray shadow
03087 // const Expr& TheoryArithOld::getE(const Expr& e) {
03088 //   DebugAssert(isGrayShadow(e),
03089 //        "TheoryArithOld::getE("+e.toString()
03090 //        +"): not a gray shadow");
03091 //   return e.getExprValue(1);
03092 // }
03093 

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