theory_arith.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file theory_arith.cpp
 * 
 * Author: Clark Barrett, Vijay Ganesh.
 * 
 * Created: Fri Jan 17 18:39:18 2003
 *
 * <hr>
 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/


#include "theory_arith.h"
#include "arith_proof_rules.h"
//#include "arith_expr.h"
#include "vcl.h"
#include "arith_exception.h"
#include "typecheck_exception.h"
#include "eval_exception.h"
#include "parser_exception.h"
#include "smtlib_exception.h"
#include "theory_core.h"

using namespace std;
using namespace CVCL;


///////////////////////////////////////////////////////////////////////////////
// TheoryArith::FreeConst Methods                                            //
///////////////////////////////////////////////////////////////////////////////

namespace CVCL {

ostream& operator<<(ostream& os, const TheoryArith::FreeConst& fc) {
  os << "FreeConst(r=" << fc.getConst() << ", " 
     << (fc.strict()? "strict" : "non-strict") << ")";
  return os;
}

///////////////////////////////////////////////////////////////////////////////
// TheoryArith::Ineq Methods                                                 //
///////////////////////////////////////////////////////////////////////////////

ostream& operator<<(ostream& os, const TheoryArith::Ineq& ineq) {
  os << "Ineq(" << ineq.ineq().getExpr() << ", isolated on "
     << (ineq.varOnRHS()? "RHS" : "LHS") << ", const = "
     << ineq.getConst() << ")";
  return os;
}
} // End of namespace CVCL


///////////////////////////////////////////////////////////////////////////////
// TheoryArith Private Methods                                               //
///////////////////////////////////////////////////////////////////////////////


Theorem TheoryArith::isIntegerThm(const Expr& e) {
  // Quick check
  if(isReal(e.getType())) return Theorem();
  // Try harder
  return isIntegerDerive(Expr(IS_INTEGER, e), typePred(e));
}


Theorem TheoryArith::isIntegerDerive(const Expr& isIntE, const Theorem& thm) {
  const Expr& e = thm.getExpr();
  // We found it!
  if(e == isIntE) return thm;

  Theorem res;
  // If the theorem is an AND, look inside each child
  if(e.isAnd()) {
    int i, iend=e.arity();
    for(i=0; i<iend; ++i) {
      res = isIntegerDerive(isIntE, getCommonRules()->andElim(thm, i));
      if(!res.isNull()) return res;
    }
  }
  return res;
}

const Rational& TheoryArith::freeConstIneq(const Expr& ineq, bool varOnRHS) {
  DebugAssert(isIneq(ineq), "TheoryArith::freeConstIneq("+ineq.toString()+")");
  const Expr& e = varOnRHS? ineq[0] : ineq[1];
  
  switch(e.getKind()) {
  case PLUS:
    return e[0].getRational();
  case RATIONAL_EXPR:
    return e.getRational();
  default: { // MULT, DIV, or Variable
    static Rational zero(0);
    return zero;
  }
  }
}


const TheoryArith::FreeConst& 
TheoryArith::updateSubsumptionDB(const Expr& ineq, bool varOnRHS,
                                 bool& subsumed) {
  TRACE("arith ineq", "TheoryArith::updateSubsumptionDB(", ineq, 
        ", var isolated on "+string(varOnRHS? "RHS" : "LHS")+")");
  DebugAssert(isLT(ineq) || isLE(ineq), "TheoryArith::updateSubsumptionDB("
              +ineq.toString()+")");
  // Indexing expression: same as ineq only without the free const
  Expr index;
  const Expr& t = varOnRHS? ineq[0] : ineq[1];
  bool strict(isLT(ineq));
  Rational c(0);
  if(isPlus(t)) {
    DebugAssert(t.arity() >= 2, "TheoryArith::updateSubsumptionDB("
                +ineq.toString()+")");
    c = t[0].getRational(); // Extract the free const in ineq
    Expr newT;
    if(t.arity() == 2) {
      newT = t[1];
    } else {
      vector<Expr> kids;
      Expr::iterator i=t.begin(), iend=t.end();
      for(++i; i!=iend; ++i) kids.push_back(*i);
      DebugAssert(kids.size() > 0, "kids.size = "+int2string(kids.size())
                  +", ineq = "+ineq.toString());
      newT = plusExpr(kids);
    }
    if(varOnRHS)
      index = leExpr(newT, ineq[1]);
    else
      index = leExpr(ineq[0], newT);
  } else if(isRational(t)) {
    c = t.getRational();
    if(varOnRHS)
      index = leExpr(rat(0), ineq[1]);
    else
      index = leExpr(ineq[0], rat(0));
  } else if(isLT(ineq))
    index = leExpr(ineq[0], ineq[1]);
  else 
    index = ineq;
  // Now update the database, check for subsumption, and extract the constant
  CDMap<Expr, FreeConst>::iterator i=d_freeConstDB.find(index), 
    iend=d_freeConstDB.end();
  if(i == iend) {
    subsumed = false;
    // Create a new entry
    CDOmap<Expr,FreeConst>& obj = d_freeConstDB[index];
    obj = FreeConst(c,strict);
    TRACE("arith ineq", "freeConstDB["+index.toString()+"] := ", obj, "");
    return obj.get();
  } else {
    CDOmap<Expr,FreeConst>& obj = d_freeConstDB[index];
    const FreeConst& fc = obj.get();
    if(varOnRHS) {
      subsumed = (c < fc.getConst() ||
                  (c == fc.getConst() && (!strict || fc.strict())));
    } else {
      subsumed = (c > fc.getConst() ||
                  (c == fc.getConst() && (strict || !fc.strict())));
    }
    if(!subsumed) {
      obj = FreeConst(c,strict);
      TRACE("arith ineq", "freeConstDB["+index.toString()+"] := ", obj, "");
    }
    return obj.get();
  }
}


bool TheoryArith::kidsCanonical(const Expr& e) {
  if(isLeaf(e)) return true;
  bool res(true);
  for(int i=0; res && i<e.arity(); ++i) {
    Expr simp(canon(e[i]).getRHS());
    res = (e[i] == simp);
    IF_DEBUG(if(!res) debugger.getOS() << "\ne[" << i << "] = " << e[i]
             << "\nsimplified = " << simp << endl);
  }
  return res;
}


///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Function: TheoryArith::canon                                              //
// Author: Clark Barrett, Vijay Ganesh.                                      //
// Created: Sat Feb  8 14:46:32 2003                                         //
// Description: Compute a canonical form for expression e and return a       //
//              theorem that e is equal to its canonical form.               //
// Note that canonical form for arith expressions is one of the following:   //
// 1. rational constant                                                      //
// 2. arithmetic leaf                                                        //
//    (i.e. variable or term from some other theory)                         //
// 3. (MULT rat leaf)                                                        //
//    where rat is a non-zero rational constant, leaf is an arithmetic leaf  //
// 4. (PLUS const term_0 term_1 ... term_n)                                  //
//    where each term_i is either a leaf or (MULT rat leaf)                  //
//    and each leaf in term_i must be strictly greater than the leaf in      //
//    term_{i+1}.                                                            //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
Theorem TheoryArith::canon(const Expr& e)
{
  TRACE("arith canon","canon(",e,") {");
  DebugAssert(kidsCanonical(e), "TheoryArith::canon("+e.toString()+")");
  Theorem result;
  switch (e.getKind()) {
    case UMINUS: {
      Theorem thm = d_rules->uMinusToMult(e[0]);
      Expr e2 = thm.getRHS();
      result = transitivityRule(thm, canon(e2));
    }
      break;
    case PLUS: /* {
      Theorem plusThm, plusThm1;
      plusThm = d_rules->canonFlattenSum(e);
      plusThm1 = d_rules->canonComboLikeTerms(plusThm.getRHS());
      result = transitivityRule(plusThm,plusThm1);
    } 
             */
      result = d_rules->canonPlus(e);
      break;
    case MINUS: {
      DebugAssert(e.arity() == 2,"");
      Theorem minus_eq_sum = d_rules->minusToPlus(e[0], e[1]);
      // this produces e0 + (-1)*e1; we have to canonize it in 2 steps
      Expr sum(minus_eq_sum.getRHS());
      Theorem thm(canon(sum[1]));
      if(thm.getLHS() == thm.getRHS()) 
        result = canon(minus_eq_sum);
      // The sum changed; do the work
      else {
        vector<unsigned> changed;
        vector<Theorem> thms;
        changed.push_back(1);
        thms.push_back(thm);
        Theorem sum_eq_canon = canon(substitutivityRule(sum, changed, thms));
        result = transitivityRule(minus_eq_sum, sum_eq_canon);
      }
      break;
    }
  
    case MULT:
      result = d_rules->canonMult(e);
      break;
  /*
    case MULT: {
      Theorem thmMult, thmMult1;
      Expr exprMult;
      Expr e0 = e[0];
      Expr e1 = e[1];
      if(e0.isRational()) {
        if(rat(0) == e0)
        result = d_rules->canonMultZero(e1);
        else if (rat(1) == e0)
        result = d_rules->canonMultOne(e1);
        else
        switch(e1.getKind()) {
        case RATIONAL_EXPR :
          result = d_rules->canonMultConstConst(e0,e1);
          break;
        case MULT:
          DebugAssert(e1[0].isRational(),
                      "theory_arith::canon:\n  "
                      "canon:MULT:MULT child is not canonical: "
                      + e1[0].toString());
  
          thmMult = d_rules->canonMultConstTerm(e0,e1[0],e1[1]);
          result = transitivityRule(thmMult,canon(thmMult.getRHS()));
          break;
        case PLUS:{
          Theorem thmPlus, thmPlus1;
          Expr ePlus;
          std::vector<Theorem> thmPlusVector;
          thmPlus = d_rules->canonMultConstSum(e0,e1);
          ePlus = thmPlus.getRHS();
          Expr::iterator i = ePlus.begin();
          for(;i != ePlus.end();++i)
            thmPlusVector.push_back(canon(*i));
          thmPlus1 = substitutivityRule(PLUS, thmPlusVector);
          result = transitivityRule(thmPlus, thmPlus1);
          break;
        }
        default:
          result = reflexivityRule(e);
          break;
        }
      }
      else {
          if(e1.isRational()){
  
          // canonMultTermConst just reverses the order of the const and the
            // term.  Then canon is called again.
        Theorem t1 = d_rules->canonMultTermConst(e1,e0);
        result = transitivityRule(t1,canon(t1.getRHS()));
        }
        else
  
              // This is where the assertion for non-linear multiplication is
              // produced. 
            result =  d_rules->canonMultTerm1Term2(e0,e1);
      }
      break;
      }
  
  */
    case DIVIDE:{
  /*
      case DIVIDE:{
        if (e[1].isRational()) {
          if (e[1].getRational() == 0)
            throw ArithException("Divide by 0 error in "+e.toString());
          Theorem thm = d_rules->canonDivideVar(e[0], e[1]);
          Expr e2 = thm.getRHS();
          result =  transitivityRule(thm, canon(e2));
        }
        else 
        {
        // TODO: to be handled
        throw ArithException("Divide by a non-const not handled in "+e.toString());
        }
      break;
      }
  */

      // Division by 0 is OK (total extension, protected by TCCs)
//       if (e[1].isRational() && e[1].getRational() == 0)
//         throw ArithException("Divide by 0 error in "+e.toString());
      if (e[1].getKind() == PLUS)
        throw ArithException("Divide by a PLUS expression not handled in"+e.toString());
      result = d_rules->canonDivide(e);
      break;
    }
  case POW:
    if(e[1].isRational())
      result = d_rules->canonPowConst(e);
    else
      result = reflexivityRule(e);
    break;
  default:
      result = reflexivityRule(e);
      break;
    }
  TRACE("arith canon","canon => ",result," }");
  return result;
}


Theorem
TheoryArith::canonRec(const Expr& e)
{
  if (isLeaf(e)) return reflexivityRule(e);
  int ar = e.arity();
  if (ar > 0) {
    vector<Theorem> newChildrenThm;
    vector<unsigned> changed;
    for(int k = 0; k < ar; ++k) {
      // Recursively canonize the kids
      Theorem thm = canonRec(e[k]);
      if (thm.getLHS() != thm.getRHS()) {
        newChildrenThm.push_back(thm);
        changed.push_back(k);
      }
    }
    if(changed.size() > 0) {
      return canon(substitutivityRule(e, changed, newChildrenThm));
    }
  }
  return canon(e);
}


Theorem
TheoryArith::canonSimplify(const Expr& e) {
  TRACE("arith", "canonSimplify(", e, ") {");
  DebugAssert(kidsCanonical(e),
              "TheoryArith::canonSimplify("+e.toString()+")");
  Expr tmp(e);
  Theorem thm = canon(e);
  if(thm.getRHS().hasFind())
    thm = transitivityRule(thm, find(thm.getRHS()));
  // We shouldn't rely on simplification in this function anymore
  DebugAssert(thm.getRHS() == simplifyExpr(thm.getRHS()),
              "canonSimplify("+e.toString()+")\n"
              +"canon(e) = "+thm.getRHS().toString()
              +"\nsimplify(canon(e)) = "+simplifyExpr(thm.getRHS()).toString());
//   if(tmp != thm.getRHS())
//     thm = transitivityRule(thm, simplifyThm(thm.getRHS()));
//   while(tmp != thm.getRHS()) {
//     tmp = thm.getRHS();
//     thm = canon(thm);
//     if(tmp != thm.getRHS())
//       thm = transitivityRule(thm, simplifyThm(thm.getRHS()));
//   }
  TRACE("arith", "canonSimplify =>", thm, " }");
  return thm;
}

/*! accepts a theorem, canonizes it, applies iffMP and substituvity to
 *  derive the canonized thm
 */
Theorem
TheoryArith::canonPred(const Theorem& thm) {
  vector<Theorem> thms;
  DebugAssert(thm.getExpr().arity() == 2,
              "TheoryArith::canonPred: bad theorem: "+thm.toString());
  Expr e(thm.getExpr());
  thms.push_back(canonSimplify(e[0]));
  thms.push_back(canonSimplify(e[1]));
  return iffMP(thm, substitutivityRule(e.getOp(), thms));
}

/*! accepts an equivalence theorem, canonizes it, applies iffMP and
 *  substituvity to derive the canonized thm
 */
Theorem
TheoryArith::canonPredEquiv(const Theorem& thm) {
  vector<Theorem> thms;
  DebugAssert(thm.getRHS().arity() == 2,
              "TheoryArith::canonPredEquiv: bad theorem: "+thm.toString());
  Expr e(thm.getRHS());
  thms.push_back(canonSimplify(e[0]));
  thms.push_back(canonSimplify(e[1]));
  return transitivityRule(thm, substitutivityRule(e.getOp(), thms));
}

/*! accepts an equivalence theorem whose RHS is a conjunction,
 *  canonizes it, applies iffMP and substituvity to derive the
 *  canonized thm
 */
Theorem
TheoryArith::canonConjunctionEquiv(const Theorem& thm) {
  vector<Theorem> thms;
  return thm;
}

/*! Psuedo-code for doSolve. (Input is an equation) (output is a Theorem)
 *  -# translate e to the form e' = 0
 *  -# if (e'.isRational()) then {if e' != 0 return false else true}
 *  -# a for loop checks if all the variables are integers. 
 *      - if not isolate a suitable real variable and call processRealEq().
 *      - if all variables are integers then isolate suitable variable 
 *         and call processIntEq(). 
 */
Theorem TheoryArith::doSolve(const Theorem& thm)
{ 
  const Expr& e = thm.getExpr();
  TRACE("arith eq","doSolve(",e,") {");
  DebugAssert(thm.isRewrite(), "thm = "+thm.toString());
  Theorem eqnThm;
  vector<Theorem> thms;  
  // Move LHS to the RHS, if necessary
  if(e[0].isRational() && e[0].getRational() == 0)
    eqnThm = thm;
  else {
    eqnThm = iffMP(thm, d_rules->rightMinusLeft(e));
    eqnThm = canonPred(eqnThm);
  }
  // eqnThm is of the form 0 = e'
  // 'right' is of the form e'
  Expr right = eqnThm.getRHS();
  // Check for trivial equation
  if (right.isRational()) {
    Theorem result = iffMP(eqnThm, d_rules->constPredicate(eqnThm.getExpr()));
    TRACE("arith eq","doSolve => ",result," }");
    return result;
  }

  //normalize
  eqnThm = iffMP(eqnThm, normalize(eqnThm.getExpr()));
  right = eqnThm.getRHS();
  
  //eqn is of the form 0 = e' and is normalized where 'right' denotes e'
  //FIXME: change processRealEq to accept equations as well instead of theorems
  if(!isInteger(right)) {
    Theorem res;
    try {
      res = processRealEq(eqnThm);
    } catch(ArithException& e) {
      res = symmetryRule(eqnThm); // Flip to e' = 0
      TRACE("arith eq", "doSolve: failed to solve an equation: ", e, "");
      IF_DEBUG(debugger.counter("FAILED to solve real equalities")++);
      setIncomplete("Non-linear arithmetic inequalities");
    }
    IF_DEBUG(debugger.counter("solved real equalities")++);
    TRACE("arith eq", "doSolve [real] => ", res, " }");
    return res;
  }
  else {
    Theorem res = processIntEq(eqnThm);
    IF_DEBUG(debugger.counter("solved int equalities")++);
    TRACE("arith eq", "doSolve [int] => ", res, " }");
    return res;
  }
}

/*! pick a monomial for the input equation. This function is used only
 *  if the equation is an integer equation. Choose the monomial with
 *  the smallest absolute value of coefficient.
 */
Expr
TheoryArith::pickIntEqMonomial(const Expr& right)
{
  DebugAssert(isPlus(right) && right.arity() > 2,
              "TheoryArith::pickIntEqMonomial right is wrong :-): " +
              right.toString());
  DebugAssert(right[0].isRational(),
              "TheoryArith::pickIntEqMonomial. right[0] must be const" +
              right.toString());
  DebugAssert(isInteger(right),
              "TheoryArith::pickIntEqMonomial: right is of type int: " +
              right.toString());
  //right is of the form "C + a1x1 + ... + anxn". min is initialized
  //to a1
  Expr::iterator i = right.begin();
  i++; //skip 'C'
  Rational min = isMult(*i) ? abs((*i)[0].getRational()) : 1;
  Expr pickedMon = *i;
  for(Expr::iterator iend = right.end(); i != iend; ++i) {
    Rational coeff = isMult(*i) ? abs((*i)[0].getRational()) : 1;
    if(min > coeff) {
      min = coeff;
      pickedMon = *i;
    }
  }
  return pickedMon;
}

/*! input is e1=e2<==>0=e' Theorem and some of the vars in e' are of
 * type REAL. isolate one of them and send back to framework. output
 * is "e1=e2 <==> var = e''" Theorem.
 */
Theorem 
TheoryArith::processRealEq(const Theorem& eqn)
{
  Expr right = eqn.getRHS();
  // Find variable to isolate and store it in left.  Pick the largest
  // (according to the total ordering) variable.  FIXME: change from
  // total ordering to the ordering we devised for inequalities.

  // TODO: I have to pick a variable that appears as a variable in the
  // term but does not appear as a variable anywhere else.  The variable
  // must appear as a single leaf and not in a MULT expression with some
  // other variables and nor in a POW expression.

  bool found = false;
  
  Expr left;
  
  if (isPlus(right))  {
    for(int i = right.arity()-1; i>=0; --i) {
      Expr c = right[i];
      if(isRational(c))
        continue;
      if(!isInteger(c))  {
        if (isLeaf(c) || 
            ((isMult(c) && c.arity() == 2 && isLeaf(c[1])))) {
          int numoccurs = 0;
          Expr leaf = isLeaf(c) ? c : c[1];
          for (int j = 0; j < right.arity(); ++j) {
            if (j!= i
                && isLeafIn(leaf, right[j])
                // && leaf.subExprOf(right[j])
                ) {
              numoccurs++;
              break;
            }
          }
          if (!numoccurs) {
            left = c;
            found = true;
            break;
          }
        }
      }
    }
  }
  else if ((isMult(right) && right.arity() == 2 && isLeaf(right[1])) ||
           isLeaf(right)) {
    left = right;
    found = true;
  }
  
  if (!found) {
    // TODO:
    // throw an arithmetic exception that this cannot be done.
    throw 
      ArithException("Can't find a leaf for solve in "+eqn.toString());
  }

  Rational r = -1;
  if (isMult(left))  {
    DebugAssert(left.arity() == 2, "only leaf should be chosen as lhs");
    DebugAssert(left[0].getRational() != 0, "left = "+left.toString());
    r = -1/left[0].getRational();
    left = left[1];
  }

  DebugAssert(isReal(getBaseType(left)) && !isInteger(left),
              "TheoryArith::ProcessRealEq: left is integer:\n left = "
              +left.toString());
  // Normalize equation so that coefficient of the monomial
  // corresponding to "left" in eqn[1] is -1
  Theorem result(iffMP(eqn,
                       d_rules->multEqn(eqn.getLHS(), eqn.getRHS(), rat(r))));
  result = canonPred(result);

  // Isolate left
  result = iffMP(result, d_rules->plusPredicate(result.getLHS(),
                                                result.getRHS(), left, EQ));
  result = canonPred(result);
  TRACE("arith","processRealEq => ",result," }");
  return result;
}

/*!
 * \param eqn is a single equation 0 = e
 * \return an equivalent Theorem (x = t AND 0 = e'), or just x = t
 */
Theorem
TheoryArith::processSimpleIntEq(const Theorem& eqn)
{
  TRACE("arith eq", "processSimpleIntEq(", eqn.getExpr(), ") {");
  DebugAssert(eqn.isRewrite(),
              "TheoryArith::processSimpleIntEq: eqn must be equality" +
              eqn.getExpr().toString());

  Expr right = eqn.getRHS();

  DebugAssert(eqn.getLHS().isRational() && 0 == eqn.getLHS().getRational(),
              "TheoryArith::processSimpleIntEq: LHS must be 0:\n" +
              eqn.getExpr().toString());

  //recall that 0 = c case is already handled in doSolve() function.
  if(isMult(right)) {
    //here we take care of special case 0=c.x
    Expr c,x;
    separateMonomial(right, c, x);
    Theorem isIntx(isIntegerThm(x));
    DebugAssert(!isIntx.isNull(), "right = "+right.toString());
    Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx)));
    TRACE("arith eq", "processSimpleIntEq[0 = a*x] => ", res, " }");
    return res;
  } else if(isPlus(right)) {
    if(2 == right.arity()) {
      //we take care of special cases like 0 = c + a.x, 0 = c + x,
      Expr c,x;
      separateMonomial(right[1], c, x);
      Theorem isIntx(isIntegerThm(x));
      DebugAssert(!isIntx.isNull(), "right = "+right.toString()
                  +"\n x = "+x.toString());
      Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx)));
      TRACE("arith eq", "processSimpleIntEq[0 = c + a*x] => ", res, " }");
      return res;
    }
    DebugAssert(right.arity() > 2,
                "TheoryArith::processSimpleIntEq: RHS is not in correct form:"
                +eqn.getExpr().toString());
    // Pick a suitable monomial. isolated can be of the form x, a.x, -a.x
    Expr isolated = pickIntEqMonomial(right);
    TRACE("arith eq", "processSimpleIntEq: isolated = ", isolated, "");

    // First, we compute the 'sign factor' with which to multiply the
    // eqn.  if the coeff of isolated is positive (i.e. 'isolated' is
    // of the form x or a.x where a>0 ) then r must be -1 and if coeff
    // of 'isolated' is negative, r=1.
    Rational r = isMult(isolated) ?
      ((isolated[0].getRational() > 0) ? -1 : 1) : -1;
    Theorem result;
    if (-1 == r) {
      // r=-1 and hence 'isolated' is 'x' or 'a.x' where a is
      // positive.  modify eqn (0=e') to the equation (0=canon(-1*e'))
      result = iffMP(eqn, d_rules->multEqn(eqn.getLHS(), right, rat(r)));
      result = canonPred(result);
      Expr e = result.getRHS();

      // Isolate the 'isolated'
      result = iffMP(result,
                     d_rules->plusPredicate(result.getLHS(),result.getRHS(),
                                            isolated, EQ));
    } else {
      //r is 1 and hence isolated is -a.x. Make 'isolated' positive.
      const Rational& minusa = isolated[0].getRational();
      Rational a = -1*minusa;
      isolated = (a == 1)? isolated[1] : rat(a) * isolated[1];
      
      // Isolate the 'isolated'
      result = iffMP(eqn, d_rules->plusPredicate(eqn.getLHS(), 
                                                 right,isolated,EQ));
    }
    // Canonize the result
    result = canonPred(result);
        
    //if isolated is 'x' or 1*x, then return result else continue processing.
    if(!isMult(isolated) || isolated[0].getRational() == 1) {   
      TRACE("arith eq", "processSimpleIntEq[x = rhs] => ", result, " }");
      return result;
    } else {
      DebugAssert(isMult(isolated) && isolated[0].getRational() >= 2,
                  "TheoryArith::processSimpleIntEq: isolated must be mult "
                  "with coeff >= 2.\n isolated = " + isolated.toString());

      // Compute IS_INTEGER() for lhs and rhs
      const Expr& lhs = result.getLHS();
      const Expr& rhs = result.getRHS();
      Expr a, x;
      separateMonomial(lhs, a, x);
      Theorem isIntLHS = isIntegerThm(x);
      vector<Theorem> isIntRHS;
      if(!isPlus(rhs)) { // rhs is a MULT
        Expr c, v;
        separateMonomial(rhs, c, v);
        isIntRHS.push_back(isIntegerThm(v));
        DebugAssert(!isIntRHS.back().isNull(), "");
      } else { // rhs is a PLUS
        DebugAssert(isPlus(rhs), "rhs = "+rhs.toString());
        DebugAssert(rhs.arity() >= 2, "rhs = "+rhs.toString());
        Expr::iterator i=rhs.begin(), iend=rhs.end();
        ++i; // Skip the free constant
        for(; i!=iend; ++i) {
          Expr c, v;
          separateMonomial(*i, c, v);
          isIntRHS.push_back(isIntegerThm(v));
          DebugAssert(!isIntRHS.back().isNull(), "");
        }
      }
      // Derive (EXISTS (x:INT): x = t2 AND 0 = t3)
      result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS);
      // Skolemize the quantifier
      result = getCommonRules()->skolemize(result);
      // Canonize t2 and t3 generated by this rule
      DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
                  "processSimpleIntEq: result = "+result.getExpr().toString());
      Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0));
      Theorem thm2 = canonPred(getCommonRules()->andElim(result, 1));
      Theorem newRes = getCommonRules()->andIntro(thm1, thm2);
      if(newRes.getExpr() != result.getExpr()) result = newRes;
      
      TRACE("arith eq", "processSimpleIntEq => ", result, " }");
      return result;
    }
  } else {
    // eqn is 0 = x.  Flip it and return
    Theorem result = symmetryRule(eqn);
    TRACE("arith eq", "processSimpleIntEq[x = 0] => ", result, " }");
    return result;
  }
}

/*! input is e1=e2<==>0=e' Theorem and all of the vars in e' are of
 * type INT. isolate one of them and send back to framework. output
 * is "e1=e2 <==> var = e''" Theorem and some associated equations in
 * solved form.
 */
Theorem 
TheoryArith::processIntEq(const Theorem& eqn)
{
  TRACE("arith eq", "processIntEq(", eqn.getExpr(), ") {");
  // Equations in the solved form.  
  std::vector<Theorem> solvedAndNewEqs;
  Theorem newEq(eqn), result;
  bool done(false);
  do {
    result = processSimpleIntEq(newEq);
    // 'result' is of the from (x1=t1)  AND 0=t'
    if(result.isRewrite()) {
      solvedAndNewEqs.push_back(result);
      done = true;
    }
    else if(!result.getExpr().isFalse()) {
      DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
                  "TheoryArith::processIntEq("+eqn.getExpr().toString()
                  +")\n result = "+result.getExpr().toString());
      solvedAndNewEqs.push_back(getCommonRules()->andElim(result, 0));
      newEq = getCommonRules()->andElim(result, 1);
    } else
      done = true;
  } while(!done);
  Theorem res;
  if(result.getExpr().isFalse()) res = result;
  else res = solvedForm(solvedAndNewEqs);
  TRACE("arith eq", "processIntEq => ", res.getExpr(), " }");
  return res;
}

/*!
 * Takes a vector of equations and for every equation x_i=t_i
 * substitutes t_j for x_j in t_i for all j>i.  This turns the system
 * of equations into a solved form.
 *
 * Assumption: variables x_j may appear in the RHS terms t_i ONLY for
 * i<j, but not for i>=j.
 */
Theorem
TheoryArith::solvedForm(const vector<Theorem>& solvedEqs) 
{
  DebugAssert(solvedEqs.size() > 0, "TheoryArith::solvedForm()");

  // Trace code
  TRACE_MSG("arith eq", "TheoryArith::solvedForm:solvedEqs(\n  [");
  IF_DEBUG(if(debugger.trace("arith eq")) {
    for(vector<Theorem>::const_iterator j = solvedEqs.begin(),
          jend=solvedEqs.end(); j!=jend;++j)
      TRACE("arith eq", "", j->getExpr(), ",\n   ");
  });
  TRACE_MSG("arith eq", "  ]) {");
  // End of Trace code
  
  vector<Theorem>::const_reverse_iterator
    i = solvedEqs.rbegin(),
    iend = solvedEqs.rend();
  // Substitution map: a variable 'x' is mapped to a Theorem x=t.
  // This map accumulates the resulting solved form.
  ExprMap<Theorem> subst;
  for(; i!=iend; ++i) {
    if(i->isRewrite()) {
      Theorem thm = substAndCanonize(*i, subst);
      TRACE("arith eq", "solvedForm: subst["+i->getLHS().toString()+"] = ",
            thm.getExpr(), "");
      subst[i->getLHS()] = thm;
    }
    else {
      // This is the FALSE case: just return the contradiction
      DebugAssert(i->getExpr().isFalse(),
                  "TheoryArith::solvedForm: an element of solvedEqs must "
                  "be either EQ or FALSE: "+i->toString());
      return *i;
    }
  }
  // Now we've collected the solved form in 'subst'.  Wrap it up into
  // a conjunction and return.
  vector<Theorem> thms;
  for(ExprMap<Theorem>::iterator i=subst.begin(), iend=subst.end();
      i!=iend; ++i)
    thms.push_back(i->second);
  return getCommonRules()->andIntro(thms);
}


/*!
 * ASSUMPTION: 't' is a fully canonized arithmetic term, and every
 * element of subst is a fully canonized equation of the form x=e,
 * indexed by the LHS variable.
 */

Theorem
TheoryArith::substAndCanonize(const Expr& t, ExprMap<Theorem>& subst)
{
  TRACE("arith eq", "substAndCanonize(", t, ") {");
  // Quick and dirty check: return immediately if subst is empty
  if(subst.empty()) {
    Theorem res(reflexivityRule(t));
    TRACE("arith eq", "substAndCanonize[subst empty] => ", res, " }");
    return res;
  }
  // Check if we can substitute 't' directly
  ExprMap<Theorem>::iterator i = subst.find(t), iend=subst.end();
  if(i!=iend) {
    TRACE("arith eq", "substAndCanonize[subst] => ", i->second, " }");
    return i->second;
  }
  // The base case: t is an i-leaf
  if(isLeaf(t)) {
    Theorem res(reflexivityRule(t));
    TRACE("arith eq", "substAndCanonize[i-leaf] => ", res, " }");
    return res;
  }
  // 't' is an arithmetic term; recurse into the children
  vector<Theorem> thms;
  vector<unsigned> changed;
  for(unsigned j=0, jend=t.arity(); j!=jend; ++j) {
    Theorem thm = substAndCanonize(t[j], subst);
    if(thm.getRHS() != t[j]) {
      thm = canon(thm);
      thms.push_back(thm);
      changed.push_back(j);
    }
  }
  // Do the actual substitution and canonize the result
  Theorem res;
  if(thms.size() > 0) {
    res = substitutivityRule(t, changed, thms);
    res = canon(res);
  }
  else
    res = reflexivityRule(t);
  TRACE("arith eq", "substAndCanonize => ", res, " }");
  return res;
}


/*!
 *  ASSUMPTION: 't' is a fully canonized equation of the form x = t,
 *  and so is every element of subst, indexed by the LHS variable.
 */

Theorem
TheoryArith::substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst)
{
  // Quick and dirty check: return immediately if subst is empty
  if(subst.empty()) return eq;

  DebugAssert(eq.isRewrite(), "TheoryArith::substAndCanonize: t = "
              +eq.getExpr().toString());
  const Expr& t = eq.getRHS();
  // Do the actual substitution in the term t
  Theorem thm = substAndCanonize(t, subst);
  // Substitution had no result: return the original equation
  if(thm.getRHS() == t) return eq;
  // Otherwise substitute the result into the equation
  vector<Theorem> thms;
  vector<unsigned> changed;
  thms.push_back(thm);
  changed.push_back(1);
  return iffMP(eq, substitutivityRule(eq.getExpr(), changed, thms));
}


void TheoryArith::processBuffer()
{
  // Process the inequalities in the buffer
  bool varOnRHS;
  for(; !inconsistent() && d_bufferIdx < d_buffer.size();
      d_bufferIdx = d_bufferIdx+1) {
    const Theorem& ineqThm = d_buffer[d_bufferIdx];
    // Skip this inequality if it is stale
    if(isStale(ineqThm.getExpr())) continue;
    Theorem thm1 = isolateVariable(ineqThm, varOnRHS);
    const Expr& ineq = thm1.getExpr();
    if((ineq).isFalse())
      setInconsistent(thm1);
    else if(!ineq.isTrue()) {
      // Check that the variable is indeed isolated correctly
      DebugAssert(varOnRHS? !isPlus(ineq[1]) : !isPlus(ineq[0]),
                  "TheoryArith::processBuffer(): bad result from "
                  "isolateVariable:\nineq = "+ineq.toString());
      // and project the inequality
      projectInequalities(thm1, varOnRHS);
    }
  }
}


void TheoryArith::updateStats(const Rational& c, const Expr& v)
{
  TRACE("arith ineq", "updateStats("+c.toString()+", ", v, ")");
  if(c > 0) {
    if(d_countRight.count(v) > 0) d_countRight[v] = d_countRight[v] + 1;
    else d_countRight[v] = 1;
  }
  else
    if(d_countLeft.count(v) > 0) d_countLeft[v] = d_countLeft[v] + 1;
    else d_countLeft[v] = 1;
}


void TheoryArith::updateStats(const Expr& monomial)
{
  Expr c, m;
  separateMonomial(monomial, c, m);
  updateStats(c.getRational(), m);
}


void TheoryArith::addToBuffer(const Theorem& thm) {
  // First, turn the inequality into 0 < rhs
  // FIXME: check if this can be optimized away
  Theorem result(thm);
  const Expr& e = thm.getExpr();
  // int kind = e.getKind();
  if(!(e[0].isRational() && e[0].getRational() == 0)) {
    result = iffMP(result, d_rules->rightMinusLeft(e));
    result = canonPred(result);
  }
  TRACE("arith ineq", "addToBuffer(", result.getExpr(), ")");
  // Push it into the buffer
  d_buffer.push_back(thm);

  // Collect the statistics about variables
  const Expr& rhs = thm.getExpr()[1];
  if(isPlus(rhs))
    for(Expr::iterator i=rhs.begin(), iend=rhs.end(); i!=iend; ++i)
      updateStats(*i);
  else // It's a monomial
    updateStats(rhs);
}


Theorem TheoryArith::isolateVariable(const Theorem& inputThm, 
                                     bool& isolatedVarOnRHS)
{
  Theorem result(inputThm);
  const Expr& e = inputThm.getExpr();
  TRACE("arith","isolateVariable(",e,") {");
  TRACE("arith ineq", "isolateVariable(", e, ") {");
  //we assume all the children of e are canonized
  DebugAssert(isLT(e)||isLE(e),
              "TheoryArith::isolateVariable: " + e.toString() +
              " wrong kind");
  int kind = e.getKind();
  DebugAssert(e[0].isRational() && e[0].getRational() == 0,
              "TheoryArith::isolateVariable: theorem must be of "
              "the form 0 < rhs: " + inputThm.toString());

  const Expr& zero = e[0];
  Expr right = e[1];
  // Check for trivial in-equation.
  if (right.isRational()) {
    result = iffMP(result, d_rules->constPredicate(e));
    TRACE("arith ineq","isolateVariable => ",result.getExpr()," }");
    TRACE("arith","isolateVariable => ",result," }");
    return result;
  }

  // Normalization of inequality to make coefficients integer and
  // relatively prime.

  Expr factor(computeNormalFactor(right));
  TRACE("arith", "isolateVariable: factor = ", factor, "");
  DebugAssert(factor.getRational() > 0,
              "isolateVariable: factor="+factor.toString());
  // Now multiply the inequality by the factor, unless it is 1
  if(factor.getRational() != 1) {
    result = iffMP(result, d_rules->multIneqn(e, factor));
    // And canonize the result
    result = canonPred(result);
    right = result.getExpr()[1];
  }

  // Find monomial to isolate and store it in isolatedMonomial
  Expr isolatedMonomial = right;

  if (isPlus(right))
    isolatedMonomial = pickMonomial(right);

  Rational r = -1;
  isolatedVarOnRHS = true;
  if (isMult(isolatedMonomial)) {
    r = ((isolatedMonomial[0].getRational()) >= 0)? -1 : 1;
    isolatedVarOnRHS = 
      ((isolatedMonomial[0].getRational()) >= 0)? true : false;
  }
  isolatedMonomial = canon(rat(-1)*isolatedMonomial).getRHS();
  // Isolate isolatedMonomial on to the LHS
  result = iffMP(result, d_rules->plusPredicate(zero, right, 
                                                isolatedMonomial, kind));
  // Canonize the resulting inequality
  result = canonPred(result);
  if(1 != r) {
    result = iffMP(result, d_rules->multIneqn(result.getExpr(), rat(r)));
    result = canonPred(result);
  }
  TRACE("arith ineq","isolateVariable => ",result.getExpr()," }");
  TRACE("arith","isolateVariable => ",result," }");
  return result;
}

Expr
TheoryArith::computeNormalFactor(const Expr& right) {
  // Strategy: compute f = lcm(d1...dn)/gcd(c1...cn), where the RHS is
  // of the form c1/d1*x1 + ... + cn/dn*xn
  Rational factor;
  if(isPlus(right)) {
    vector<Rational> nums, denoms;
    for(int i=0, iend=right.arity(); i<iend; ++i) {
      switch(right[i].getKind()) {
      case RATIONAL_EXPR: {
        Rational c(abs(right[i].getRational()));
        nums.push_back(c.getNumerator());
        denoms.push_back(c.getDenominator());
        break;
        }
      case MULT: {
        Rational c(abs(right[i][0].getRational()));
        nums.push_back(c.getNumerator());
        denoms.push_back(c.getDenominator());
        break;
        }
      default: // it's a variable
        nums.push_back(1);
        denoms.push_back(1);
        break;
      }
    }
    Rational gcd_nums = gcd(nums);
    // x/0 == 0 in our model, as a total extension of arithmetic.  The
    // particular value of x/0 is irrelevant, since the DP is guarded
    // by the top-level TCCs, and it is safe to return any value in
    // cases when terms are undefined.
    factor = (gcd_nums==0)? 0 : (lcm(denoms) / gcd_nums);
  } else if(isMult(right)) {
    const Rational& r = right[0].getRational();
    factor = (r==0)? 0 : (1/abs(r));
  }
  else 
    factor = 1;
  return rat(factor);
}


bool TheoryArith::lessThanVar(const Expr& isolatedMonomial, const Expr& var2) 
{
  DebugAssert(!isRational(var2) && !isRational(isolatedMonomial),
              "TheoryArith::findMaxVar: isolatedMonomial cannot be rational" + 
              isolatedMonomial.toString());
  Expr c, var0, var1;
  separateMonomial(isolatedMonomial, c, var0);
  separateMonomial(var2, c, var1);
  return var0 < var1;
}

/*! "Stale" means it contains non-simplified subexpressions.  For
 *  terms, it checks the expression's find pointer; for formulas it
 *  checks the children recursively (no caching!).  So, apply it with
 *  caution, and only to simple atomic formulas (like inequality).
 */
bool TheoryArith::isStale(const Expr& e) {
  if(e.isTerm())
    return e != find(e).getRHS();
  // It's better be a simple predicate (like inequality); we check the
  // kids recursively
  bool stale=false;
  for(Expr::iterator i=e.begin(), iend=e.end(); !stale && i!=iend; ++i)
    stale = isStale(*i);
  return stale;
}


bool TheoryArith::isStale(const TheoryArith::Ineq& ineq) {
  TRACE("arith ineq", "isStale(", ineq, ") {");
  const Expr& ineqExpr = ineq.ineq().getExpr();
  const Rational& c = freeConstIneq(ineqExpr, ineq.varOnRHS());
  bool strict(isLT(ineqExpr));
  const FreeConst& fc = ineq.getConst();

  bool subsumed;

  if(ineq.varOnRHS()) {
    subsumed = (c < fc.getConst() ||
                (c == fc.getConst() && !strict && fc.strict()));
  } else {
    subsumed = (c > fc.getConst() ||
                (c == fc.getConst() && strict && !fc.strict()));
  }

  bool res;
  if(subsumed) {
    res = true;
    TRACE("arith ineq", "isStale[subsumed] => ", res? "true" : "false", " }");
  }
  else {
    res = isStale(ineqExpr);
    TRACE("arith ineq", "isStale[updated] => ", res? "true" : "false", " }");
  }
  return res;
}


void TheoryArith::separateMonomial(const Expr& e, Expr& c, Expr& var) {
  TRACE("separateMonomial", "separateMonomial(", e, ")");
  DebugAssert(!isPlus(e), 
              "TheoryArith::separateMonomial(e = "+e.toString()+")");
  if(isMult(e)) {
    DebugAssert(e.arity() >= 2,
                "TheoryArith::separateMonomial(e = "+e.toString()+")");
    c = e[0];
    if(e.arity() == 2) var = e[1];
    else {
      vector<Expr> kids = e.getKids();
      kids[0] = rat(1);
      var = multExpr(kids);
    }
  } else {
    c = rat(1);
    var = e;
  }
  DebugAssert(c.isRational(), "TheoryArith::separateMonomial(e = "
              +e.toString()+", c = "+c.toString()+")");
  DebugAssert(!isMult(var) || (var[0].isRational() && var[0].getRational()==1),
              "TheoryArith::separateMonomial(e = "
              +e.toString()+", var = "+var.toString()+")");
}


void TheoryArith::projectInequalities(const Theorem& theInequality, 
                                      bool isolatedVarOnRHS)
{
  TRACE("arith ineq", "projectInequalities(", theInequality.getExpr(),
        ", isolatedVarOnRHS="+string(isolatedVarOnRHS? "true" : "false")
        +") {");
  DebugAssert(isLE(theInequality.getExpr()) || 
              isLT(theInequality.getExpr()),
              "TheoryArith::projectIsolatedVar: "\
              "theInequality is of the wrong form: " + 
              theInequality.toString());
  //TODO: DebugAssert to check if the isolatedMonomial is of the right
  //form and the whether we are indeed getting inequalities.
  Theorem theIneqThm(theInequality);
  Expr theIneq = theIneqThm.getExpr();

  Theorem isIntLHS(isIntegerThm(theIneq[0]));
  Theorem isIntRHS(isIntegerThm(theIneq[1]));
  bool isInt = (!isIntLHS.isNull() && !isIntRHS.isNull());
  // If the inequality is strict and integer, change it to non-strict
  if(isLT(theIneq) && isInt) {
    Theorem thm = d_rules->lessThanToLE(theInequality, isIntLHS, isIntRHS,
                                        !isolatedVarOnRHS);
    theIneqThm = canonPred(iffMP(theIneqThm, thm));
    theIneq = theIneqThm.getExpr();
  }
  Expr isolatedMonomial = 
    isolatedVarOnRHS ? theIneq[1] : theIneq[0];
  
  Expr monomialVar, a;
  separateMonomial(isolatedMonomial, a, monomialVar);

  bool subsumed;
  const FreeConst& bestConst =
    updateSubsumptionDB(theIneq, isolatedVarOnRHS, subsumed);

  if(subsumed) {
    IF_DEBUG(debugger.counter("subsumed inequalities")++);
    TRACE("arith ineq", "subsumed inequality: ", theIneq, "");
  } else {
    // If the isolated variable is actually a non-linear term, we are
    // incomplete
    if(isMult(monomialVar))
      setIncomplete("Non-linear arithmetic inequalities");

    // First, we need to make sure the isolated inequality is
    // setup properly.
    setupRec(theIneq[0]);
    setupRec(theIneq[1]);
    // Add the inequality into the appropriate DB.
    ExprMap<CDList<Ineq> *>& db1 =
      isolatedVarOnRHS ? d_inequalitiesRightDB : d_inequalitiesLeftDB; 
    ExprMap<CDList<Ineq> *>::iterator it1 = db1.find(monomialVar);
    if(it1 == db1.end()) {
      CDList<Ineq> * list = new CDList<Ineq>(theoryCore()->getCM()->getCurrentContext());
      list->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
      db1[monomialVar] = list;
    }
    else 
      ((*it1).second)->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
  
    ExprMap<CDList<Ineq> *>& db2 = 
      isolatedVarOnRHS ? d_inequalitiesLeftDB : d_inequalitiesRightDB; 
    ExprMap<CDList<Ineq> *>::iterator it = db2.find(monomialVar);
    if(it == db2.end()) {
      TRACE_MSG("arith ineq", "projectInequalities[not in DB] => }");
      return;
    }
  
    CDList<Ineq>& listOfDBIneqs = *((*it).second);
    Theorem betaLTt, tLTalpha, thm;
    for(size_t i = 0, iend=listOfDBIneqs.size(); i!=iend; ++i) {
      const Ineq& ineqEntry = listOfDBIneqs[i];
      const Theorem& ineqThm = ineqEntry.ineq();
      if(!isStale(ineqEntry)) {
        betaLTt = isolatedVarOnRHS ? theIneqThm : ineqThm;
        tLTalpha = isolatedVarOnRHS ? ineqThm : theIneqThm;
        thm = normalizeProjectIneqs(betaLTt, tLTalpha);
        
        IF_DEBUG(debugger.counter("real shadows")++);

        // Check for TRUE and FALSE theorems
        Expr e(thm.getExpr());  if(e.isFalse()) {
          setInconsistent(thm);
          TRACE_MSG("arith ineq", "projectInequalities[inconsistent] => }");
          return;
        }
        else {
          if(!e.isTrue() && !e.isEq())
            addToBuffer(thm);
          else if(e.isEq())
            enqueueFact(thm);
        }
      } else {
        IF_DEBUG(debugger.counter("stale inequalities")++);
      }
    }
  }
  TRACE_MSG("arith ineq", "projectInequalities => }");
}

Theorem TheoryArith::normalizeProjectIneqs(const Theorem& ineqThm1, 
                                           const Theorem& ineqThm2)
{
  //ineq1 is of the form beta < b.x  or beta < x  [ or with <= ]
  //ineq2 is of the form a.x < alpha   or x < alpha.
  Theorem betaLTt = ineqThm1, tLTalpha = ineqThm2;
  Expr ineq1 = betaLTt.getExpr();
  Expr ineq2 = tLTalpha.getExpr();
  Expr c,x;
  separateMonomial(ineq2[0], c, x);
  Theorem isIntx(isIntegerThm(x));
  Theorem isIntBeta(isIntegerThm(ineq1[0]));
  Theorem isIntAlpha(isIntegerThm(ineq2[1]));
  bool isInt = !(isIntx.isNull() || isIntBeta.isNull() || isIntAlpha.isNull());

  TRACE("arith ineq", "normalizeProjectIneqs(", ineq1,
        ", "+ineq2.toString()+") {");
  DebugAssert((isLE(ineq1) || isLT(ineq1)) &&
              (isLE(ineq2) || isLT(ineq2)),
              "TheoryArith::normalizeProjectIneqs: Wrong Kind inputs: " +
              ineq1.toString() + ineq2.toString());
  DebugAssert(!isPlus(ineq1[1]) && !isPlus(ineq2[0]),
              "TheoryArith::normalizeProjectIneqs: Wrong Kind inputs: " +
              ineq1.toString() + ineq2.toString());

  //compute the factors to multiply the two inequalities with
  //so that they get the form beta < t and t < alpha.
  Rational factor1 = 1, factor2 = 1; 
  Rational b = isMult(ineq1[1]) ? (ineq1[1])[0].getRational() : 1;
  Rational a = isMult(ineq2[0]) ? (ineq2[0])[0].getRational() : 1;
  if(b != a) {
    factor1 = a;
    factor2 = b;
  }

  //if the ineqs are of type int then apply one of the gray
  //dark shadow rules.
  // FIXME: intResult should also be checked for immediate
  // optimizations, as those below for 'result'.  Also, if intResult
  // is a single inequality, we may want to handle it similarly to the
  // 'result' rather than enqueuing directly.
  if(isInt && (a >= 2 || b >= 2)) {
    Theorem intResult;
    if(a <= b)
      intResult = d_rules->darkGrayShadow2ab(betaLTt, tLTalpha,
                                             isIntAlpha, isIntBeta, isIntx);
    else 
      intResult = d_rules->darkGrayShadow2ba(betaLTt, tLTalpha,
                                             isIntAlpha, isIntBeta, isIntx);
    enqueueFact(intResult);
    // Fetch dark and gray shadows
    DebugAssert(intResult.getExpr().isAnd() && intResult.getExpr().arity()==2,
                "intResult = "+intResult.getExpr().toString());
    const Expr& DorG = intResult.getExpr()[0];
    DebugAssert(DorG.isOr() && DorG.arity()==2, "DorG = "+DorG.toString());
    const Expr& D = DorG[0];
    const Expr& G = DorG[1];
    DebugAssert(D.getKind()==DARK_SHADOW, "D = "+D.toString());
    DebugAssert(G.getKind()==GRAY_SHADOW, "G = "+G.toString());
    // Set the higher splitter priority for dark shadow
    addSplitter(D, 5);
    // Also set a higher priority to the NEGATION of GRAY_SHADOW
    addSplitter(!G, 1);
    IF_DEBUG(debugger.counter("dark+gray shadows")++);
  }

  //actually normalize the inequalities
  if(1 != factor1) {
    std::vector<Theorem> thms1;
    Theorem thm2 = iffMP(betaLTt, d_rules->multIneqn(ineq1, rat(factor1)));
    betaLTt = canonPred(thm2);
    ineq1 = betaLTt.getExpr();
  }
  if(1 != factor2) {
    std::vector<Theorem> thms1;
    Theorem thm2 = iffMP(tLTalpha, d_rules->multIneqn(ineq2, rat(factor2)));
    tLTalpha = canonPred(thm2);
    ineq2 = tLTalpha.getExpr();
  }

  //IF_DEBUG(debugger.counter("real shadows")++);

  Expr beta(ineq1[0]);
  Expr alpha(ineq2[1]);
  // In case of alpha <= t <= alpha, we generate t = alpha
  if(isLE(ineq1) && isLE(ineq2) && alpha == beta) {
    Theorem result = d_rules->realShadowEq(betaLTt, tLTalpha);
    TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
    return result;
  }

  // Check if this inequality is a finite interval
  if(isInt)
    processFiniteInterval(betaLTt, tLTalpha);

  //project the normalized inequalities.

  Theorem result = d_rules->realShadow(betaLTt, tLTalpha);

  // FIXME: Clark's changes.  Is 'rewrite' more or less efficient?
//   result = iffMP(result, rewrite(result.getExpr()));
//   TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");

  // Now, transform the result into 0 < rhs and see if rhs is a const 
  Expr e(result.getExpr());
  // int kind = e.getKind();
  if(!(e[0].isRational() && e[0].getRational() == 0)) {
    result = iffMP(result, d_rules->rightMinusLeft(e));
    result = canonPred(result);
  }
  
  //result is "0 kind e'". where e' is equal to canon(e[1]-e[0])
  Expr right = result.getExpr()[1];
  // Check for trivial inequality
  if (right.isRational())
    result = iffMP(result, d_rules->constPredicate(result.getExpr()));
  TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
  return result;
}


Expr TheoryArith::pickMonomial(const Expr& right)
{
  DebugAssert(isPlus(right), "TheoryArith::pickMonomial: Wrong Kind: " + 
              right.toString());
  if(theoryCore()->getFlags()["var-order"].getBool()) {
    Expr::iterator i = right.begin();
    Expr isolatedMonomial = right[1];
    //PLUS always has at least two elements and the first element is
    //always a constant. hence ++i in the initialization of the for
    //loop.
    for(++i; i != right.end(); ++i)
      if(lessThanVar(isolatedMonomial,*i))
        isolatedMonomial = *i;
    return isolatedMonomial;
  }
  ExprMap<Expr> var2monomial;
  vector<Expr> vars;
  Expr::iterator i = right.begin(), iend = right.end();
  for(;i != iend; ++i) {
    if(i->isRational())
      continue;
    Expr c, var;
    separateMonomial(*i, c, var);
    var2monomial[var] = *i;
    vars.push_back(var);
  }
  vector<Expr> largest;
  d_graph.selectLargest(vars, largest);
  DebugAssert(0 < largest.size(),
              "TheoryArith::pickMonomial: selectLargest: failed!!!!");
  if(1 == largest.size())
    return var2monomial[largest[0] ];
  else {
    size_t pickedVar = 0;
    // Pick the variable which will generate the fewest number of
    // projections
    int minProjections(-1);
    for(size_t k=0; k< largest.size(); ++k) {
      const Expr& var(largest[k]), monom(var2monomial[var]);
      // Grab the counters for the variable
      int nRight = (d_countRight.count(var) > 0)? d_countRight[var] : 0;
      int nLeft = (d_countLeft.count(var) > 0)? d_countLeft[var] : 0;
      int n(nRight*nLeft);
      TRACE("arith ineq", "pickMonomial: var=", var,
            ", nRight="+int2string(nRight)+", nLeft="+int2string(nLeft));
      if(minProjections < 0 || minProjections > n) {
        minProjections = n;
        pickedVar = k;
      }
      TRACE("arith ineq", "Number of projections for "+var.toString()+" = ",
            n, "");
    }
    
    const Expr& largestVar = largest[pickedVar];
    // FIXME: TODO: update the counters (subtract counts for the vars
    // other than largestVar

    // Update the graph.
    for(size_t k = 0; k < largest.size(); ++k) {
      if(k != pickedVar)
        d_graph.addEdge(largestVar, largest[k]);
    }
    return var2monomial[largestVar];
  }
}

void TheoryArith::VarOrderGraph::addEdge(const Expr& e1, const Expr& e2)
{
  TRACE("arith var order", "addEdge("+e1.toString()+" > ", e2, ")");
  DebugAssert(e1 != e2, "TheoryArith::VarOrderGraph::addEdge("
              +e1.toString()+", "+e2.toString()+")");
  d_edges[e1].push_back(e2);
}

//returns true if e1 < e2, else false(i.e e2 < e1 or e1,e2 are not
//comparable)
bool TheoryArith::VarOrderGraph::lessThan(const Expr& e1, const Expr& e2) 
{
  d_cache.clear();
  //returns true if e1 is in the subtree rooted at e2 implying e1 < e2
  return dfs(e1,e2);
}

//returns true if e1 is in the subtree rooted at e2 implying e1 < e2
bool TheoryArith::VarOrderGraph::dfs(const Expr& e1, const Expr& e2)
{
  if(e1 == e2)
    return true;
  if(d_cache.count(e2) > 0)
    return false;
  if(d_edges.count(e2) == 0)
    return false;
  d_cache[e2] = true;
  vector<Expr>& e2Edges = d_edges[e2];
  vector<Expr>::iterator i = e2Edges.begin();
  vector<Expr>::iterator iend = e2Edges.end();
  //if dfs finds e1 then i != iend else i is equal to iend
  for(; i != iend && !dfs(e1,*i); ++i);
  return (i != iend);
}


void TheoryArith::VarOrderGraph::selectSmallest(vector<Expr>& v1,
                                               vector<Expr>& v2) 
{
  int v1Size = v1.size();
  vector<bool> v3(v1Size);
  for(int j=0; j < v1Size; ++j)
    v3[j] = false;

  for(int j=0; j < v1Size; ++j) {
    if(v3[j]) continue;
    for(int i =0; i < v1Size; ++i) {
      if((i == j) || v3[i]) 
        continue;
      if(lessThan(v1[i],v1[j])) {
        v3[j] = true;
        break;
      }
    }
  }
  vector<Expr> new_v1;

  for(int j = 0; j < v1Size; ++j) 
    if(!v3[j]) v2.push_back(v1[j]);
    else new_v1.push_back(v1[j]);
  v1 = new_v1;
}


void TheoryArith::VarOrderGraph::selectLargest(const vector<Expr>& v1,
                                               vector<Expr>& v2) 
{
  int v1Size = v1.size();
  vector<bool> v3(v1Size);
  for(int j=0; j < v1Size; ++j)
    v3[j] = false;

  for(int j=0; j < v1Size; ++j) {
    if(v3[j]) continue;
    for(int i =0; i < v1Size; ++i) {
      if((i == j) || v3[i]) 
        continue;
      if(lessThan(v1[j],v1[i])) {
        v3[j] = true;
        break;
      }
    }
  }
  
  for(int j = 0; j < v1Size; ++j) 
    if(!v3[j]) v2.push_back(v1[j]);
}

///////////////////////////////////////////////////////////////////////////////
// TheoryArith Public Methods                                                //
///////////////////////////////////////////////////////////////////////////////


TheoryArith::TheoryArith(VCL* vcl, TheoryCore* core)
  : Theory(core, "Arithmetic"),
    d_diseq(core->getCM()->getCurrentContext()),
    d_diseqIdx(core->getCM()->getCurrentContext(), 0, 0),
    d_inModelCreation(core->getCM()->getCurrentContext(), false, 0),
    d_realUsed(false), d_intUsed(false), d_intConstUsed(false),
    d_langUsed(NOT_USED),
    d_convertToDiff(core->getFlags()["convert2diff"].getString()),
    d_freeConstDB(core->getCM()->getCurrentContext()),
    d_buffer(core->getCM()->getCurrentContext()),
    // Initialize index to 0 at scope 0
    d_bufferIdx(core->getCM()->getCurrentContext(), 0, 0),
    d_bufferThres(&(core->getFlags()["ineq-delay"].getInt())),
    d_countRight(core->getCM()->getCurrentContext()),
    d_countLeft(core->getCM()->getCurrentContext()),
    d_sharedTerms(core->getCM()->getCurrentContext()),
    d_sharedVars(core->getCM()->getCurrentContext())
{
  IF_DEBUG(d_diseq.setName("CDList[TheoryArith::d_diseq]"));
  IF_DEBUG(d_buffer.setName("CDList[TheoryArith::d_buffer]"));
  IF_DEBUG(d_bufferIdx.setName("CDList[TheoryArith::d_bufferIdx]"));

  getEM()->newKind(REAL, "REAL", true);
  getEM()->newKind(INT, "INT", true);
  getEM()->newKind(SUBRANGE, "SUBRANGE", true);

  getEM()->newKind(UMINUS, "UMINUS");
  getEM()->newKind(PLUS, "PLUS");
  getEM()->newKind(MINUS, "MINUS");
  getEM()->newKind(MULT, "MULT");
  getEM()->newKind(DIVIDE, "DIVIDE");
  getEM()->newKind(POW, "POW");
  getEM()->newKind(INTDIV, "INTDIV");
  getEM()->newKind(MOD, "MOD");
  getEM()->newKind(LT, "LT");
  getEM()->newKind(LE, "LE");
  getEM()->newKind(GT, "GT");
  getEM()->newKind(GE, "GE");
  getEM()->newKind(IS_INTEGER, "IS_INTEGER");
  getEM()->newKind(NEGINF, "NEGINF");
  getEM()->newKind(POSINF, "POSINF");
  getEM()->newKind(DARK_SHADOW, "DARK_SHADOW");
  getEM()->newKind(GRAY_SHADOW, "GRAY_SHADOW");

  vector<int> kinds;
  kinds.push_back(REAL);
  kinds.push_back(INT);
  kinds.push_back(SUBRANGE);
  kinds.push_back(IS_INTEGER);
  kinds.push_back(UMINUS);
  kinds.push_back(PLUS);
  kinds.push_back(MINUS);
  kinds.push_back(MULT);
  kinds.push_back(DIVIDE);
  kinds.push_back(POW);
  kinds.push_back(LT);
  kinds.push_back(LE);
  kinds.push_back(GT);
  kinds.push_back(GE);
  kinds.push_back(RATIONAL_EXPR);
  kinds.push_back(DARK_SHADOW);
  kinds.push_back(GRAY_SHADOW);
  kinds.push_back(INTDIV);
  kinds.push_back(MOD);
  kinds.push_back(NEGINF);
  kinds.push_back(POSINF);

  registerTheory(this, kinds, true);

  d_realType = Type(getEM()->newLeafExpr(REAL));
  d_intType  = Type(getEM()->newLeafExpr(INT));
  d_rules = createProofRules();

  // TODO: This is a hack--access to vcl should be hidden here
  if (d_convertToDiff == "int") {
    d_zeroVar = vcl->varExpr("cvclZero", d_intType);
  }
  else if (d_convertToDiff == "real") {
    d_zeroVar = vcl->varExpr("cvclZero",d_realType);
  }
}


// Destructor: delete the proof rules class if it's present
TheoryArith::~TheoryArith() {
  if(d_rules != NULL) delete d_rules;
  // Clear the inequality databases
  for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesRightDB.begin(),
        iend=d_inequalitiesRightDB.end(); i!=iend; ++i)
    delete (i->second);
  for(ExprMap<CDList<Ineq> *>::iterator i=d_inequalitiesLeftDB.begin(),
        iend=d_inequalitiesLeftDB.end(); i!=iend; ++i)
    delete (i->second);
}

void TheoryArith::collectVars(const Expr& e, vector<Expr>& vars,
                              set<Expr>& cache) {
  // Check the cache first
  if(cache.count(e) > 0) return;
  // Not processed yet.  Cache the expression and proceed
  cache.insert(e);
  if(isLeaf(e)) vars.push_back(e);
  else
    for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
      collectVars(*i, vars, cache);
}

void
TheoryArith::processFiniteInterval(const Theorem& alphaLEax,
                                   const Theorem& bxLEbeta) {
  const Expr& ineq1(alphaLEax.getExpr());
  const Expr& ineq2(bxLEbeta.getExpr());
  DebugAssert(isLE(ineq1), "TheoryArith::processFiniteInterval: ineq1 = "
              +ineq1.toString());
  DebugAssert(isLE(ineq2), "TheoryArith::processFiniteInterval: ineq2 = "
              +ineq2.toString());
  // If the inequalities are not integer, just return (nothing to do)
  if(!isInteger(ineq1[0])
     || !isInteger(ineq1[1])
     || !isInteger(ineq2[0])
     || !isInteger(ineq2[1]))
    return;

  const Expr& ax = ineq1[1];
  const Expr& bx = ineq2[0];
  DebugAssert(!isPlus(ax) && !isRational(ax),
              "TheoryArith::processFiniteInterval:\n ax = "+ax.toString());
  DebugAssert(!isPlus(bx) && !isRational(bx),
              "TheoryArith::processFiniteInterval:\n bx = "+bx.toString());
  Expr a = isMult(ax)? ax[0] : rat(1);
  Expr b = isMult(bx)? bx[0] : rat(1);

  Theorem thm1(alphaLEax), thm2(bxLEbeta);
  // Multiply the inequalities by 'b' and 'a', and canonize them, if necessary
  if(a != b) {
    thm1 = canonPred(iffMP(alphaLEax, d_rules->multIneqn(ineq1, b)));
    thm2 = canonPred(iffMP(bxLEbeta, d_rules->multIneqn(ineq2, a)));
  }
  // Check that a*beta - b*alpha == c > 0
  const Expr& alphaLEt = thm1.getExpr();
  const Expr& alpha = alphaLEt[0];
  const Expr& t = alphaLEt[1];
  const Expr& beta = thm2.getExpr()[1];
  Expr c = canon(beta - alpha).getRHS();

  if(c.isRational() && c.getRational() >= 1) {
    // This is a finite interval.  First, derive t <= alpha + c:
    // canon(alpha+c) => (alpha+c == beta) ==> [symmetry] beta == alpha+c
    // Then substitute that in thm2
    Theorem bEQac = symmetryRule(canon(alpha + c));
    // Substitute beta == alpha+c for the second child of thm2
    vector<unsigned> changed;
    vector<Theorem> thms;
    changed.push_back(1);
    thms.push_back(bEQac);
    Theorem tLEac = substitutivityRule(thm2.getExpr(), changed, thms);
    tLEac = iffMP(thm2, tLEac);
    // Derive and enqueue the finite interval constraint
    Theorem isInta(isIntegerThm(alpha));
    Theorem isIntt(isIntegerThm(t));
    enqueueFact(d_rules->finiteInterval(thm1, tLEac, isInta, isIntt));
  }
}


void
TheoryArith::processFiniteIntervals(const Expr& x) {
  // If x is not integer, do not bother
  if(!isInteger(x)) return;
  // Process every pair of the opposing inequalities for 'x'
  ExprMap<CDList<Ineq> *>::iterator iLeft, iRight;
  iLeft = d_inequalitiesLeftDB.find(x);
  if(iLeft == d_inequalitiesLeftDB.end()) return;
  iRight = d_inequalitiesRightDB.find(x);
  if(iRight == d_inequalitiesRightDB.end()) return;
  // There are some opposing inequalities; get the lists
  CDList<Ineq>& ineqsLeft = *(iLeft->second);
  CDList<Ineq>& ineqsRight = *(iRight->second);
  // Get the sizes of the lists
  size_t sizeLeft = ineqsLeft.size();
  size_t sizeRight = ineqsRight.size();
  // Process all the pairs of the opposing inequalities
  for(size_t l=0; l<sizeLeft; ++l)
    for(size_t r=0; r<sizeRight; ++r)
      processFiniteInterval(ineqsRight[r], ineqsLeft[l]);
}

/*! This function recursively decends expression tree <strong>without
 *  caching</strong> until it hits a node that is already setup.  Be
 *  careful on what expressions you are calling it.
 */
void
TheoryArith::setupRec(const Expr& e) {
  if(e.hasFind()) return;
  // First, set up the kids recursively
  for (int k = 0; k < e.arity(); ++k) {
    setupRec(e[k]);
  }
  // Create a find pointer for e
  e.setFind(reflexivityRule(e));
  // And call our own setup()   
  setup(e);
}


/*!
 * Keep track of all finitely bounded integer variables in shared
 * terms.
 *
 * When a new shared term t is reported, all of its variables x1...xn
 * are added to the set d_sharedVars.  
 *
 * For each newly added variable x, check all of its opposing
 * inequalities, find out all the finite bounds and assert the
 * corresponding GRAY_SHADOW constraints.
 *
 * When projecting integer inequalities, the database d_sharedVars is
 * consulted, and if the variable is in it, check the shadows for
 * being a finite interval, and produce the additional GRAY_SHADOW
 * constraints.
 */
void TheoryArith::addSharedTerm(const Expr& e) {
  d_sharedTerms[e] = true;
  /*
  set<Expr> cache; // Aux. cache for collecting i-leaves
  vector<Expr> vars; // Vector of vars in e
  collectVars(e, vars, cache);
  for(vector<Expr>::iterator i=vars.begin(), iend=vars.end(); i!=iend; ++i) {
    if(d_sharedVars.count(*i) == 0) {
      TRACE("arith shared", "TheoryArith::addSharedTerm: new var = ", *i, "");
      processFiniteIntervals(*i);
      d_sharedVars[*i]=true;
    }
  }
  */
}


void TheoryArith::assertFact(const Theorem& e)
{
  const Expr& expr = e.getExpr();
  if (expr.isNot() && expr[0].isEq()) {
    IF_DEBUG(debugger.counter("[arith] received disequalities")++);
    d_diseq.push_back(e);
  }
  else if (!expr.isEq()){
    if (expr.isNot()) {
      // This can only be negation of dark or gray shadows, or
      // disequalities, which we ignore.  Negations of inequalities
      // are handled in rewrite, we don't even receive them here.
    } 
    else if(isDarkShadow(expr)) {
      enqueueFact(d_rules->expandDarkShadow(e));
      IF_DEBUG(debugger.counter("received DARK_SHADOW")++);
    }
    else if(isGrayShadow(expr)) {
      IF_DEBUG(debugger.counter("received GRAY_SHADOW")++);
      const Rational& c1 = expr[2].getRational();
      const Rational& c2 = expr[3].getRational();
      const Expr& v = expr[0];
      const Expr& ee = expr[1];
      if(c1 == c2)
        enqueueFact(d_rules->expandGrayShadow0(e));
      else {
        Theorem gThm(e);
        // Check if we can reduce the number of cases in G(ax,c,c1,c2)
        if(ee.isRational() && isMult(v)
           && v[0].isRational() && v[0].getRational() >= 2) {
          IF_DEBUG(debugger.counter("reduced const GRAY_SHADOW")++);
          gThm = d_rules->grayShadowConst(e);
        }
        // (Possibly) new gray shadow
        const Expr& g = gThm.getExpr();
        if(g.isFalse())
          setInconsistent(gThm);
        else if(g[2].getRational() == g[3].getRational())
          enqueueFact(d_rules->expandGrayShadow0(gThm));
        else {
          // Assert c1+e <= v <= c2+e
          enqueueFact(d_rules->expandGrayShadow(gThm));
          // Split G into 2 cases (binary search b/w c1 and c2)
          Theorem thm2 = d_rules->splitGrayShadow(gThm);
          enqueueFact(thm2);
          // Fetch the two gray shadows
          DebugAssert(thm2.getExpr().isAnd() && thm2.getExpr().arity()==2,
                      "thm2 = "+thm2.getExpr().toString());
          const Expr& G1orG2 = thm2.getExpr()[0];
          DebugAssert(G1orG2.isOr() && G1orG2.arity()==2,
                      "G1orG2 = "+G1orG2.toString());
          const Expr& G1 = G1orG2[0];
          const Expr& G2 = G1orG2[1];
          DebugAssert(G1.getKind()==GRAY_SHADOW, "G1 = "+G1.toString());
          DebugAssert(G2.getKind()==GRAY_SHADOW, "G2 = "+G2.toString());
          // Split on the left disjunct first (keep the priority low)
          addSplitter(G1, 1);
          addSplitter(G2, -1);
        }
      }
    }
    else {
      DebugAssert(isLE(expr) || isLT(expr) || isIntPred(expr), 
                  "expected LE or LT: "+expr.toString());
      if(isLE(expr) || isLT(expr)) {
        IF_DEBUG(debugger.counter("recevied inequalities")++);
        
        // Buffer the inequality
        addToBuffer(e);
        
        TRACE("arith ineq", "buffer.size() = ", d_buffer.size(), 
              ", index="+int2string(d_bufferIdx)
              +", threshold="+int2string(*d_bufferThres));
        
        if((((int)d_buffer.size()) - (int)d_bufferIdx > *d_bufferThres) 
           && !d_inModelCreation)
          processBuffer();
      } else {
        IF_DEBUG(debugger.counter("arith IS_INTEGER")++);
      }
    }
  }
  else {
    IF_DEBUG(debugger.counter("[arith] received t1=t2")++);
  }
}


void TheoryArith::checkSat(bool fullEffort)
{
  //  vector<Expr>::const_iterator e;
  //  vector<Expr>::const_iterator eEnd;
  // TODO: convert back to use iterators
  TRACE("arith ineq", "TheoryArith::checkSat(fullEffort=",
        fullEffort? "true" : "false", ")");
  if (fullEffort) {
    while(!inconsistent() && d_bufferIdx < d_buffer.size())
      processBuffer();
    if(d_inModelCreation) {
      for(; d_diseqIdx < d_diseq.size(); d_diseqIdx = d_diseqIdx+1) {
        TRACE("model", "[arith] refining diseq: ",
              d_diseq[d_diseqIdx].getExpr() , "");    
        enqueueFact(d_rules->diseqToIneq(d_diseq[d_diseqIdx]));
      }
    }
  }
}



void TheoryArith::refineCounterExample()
{
  d_inModelCreation = true;
  TRACE("model", "refineCounterExample[TheoryArith] ", "", "{");
  CDMap<Expr, bool>::iterator it = d_sharedTerms.begin(), it2,
    iend = d_sharedTerms.end();
  // Add equalities over all pairs of shared terms as suggested
  // splitters.  Notice, that we want to split on equality
  // (positively) first, to reduce the size of the model.
  for(; it!=iend; ++it) {
    // Copy by value: the elements in the pair from *it are NOT refs in CDMap
    Expr e1 = (*it).first;
    for(it2 = it, ++it2; it2!=iend; ++it2) {
      Expr e2 = (*it2).first;
      DebugAssert(isReal(getBaseType(e1)),
                  "TheoryArith::refineCounterExample: e1 = "+e1.toString()
                  +"\n type(e1) = "+e1.getType().toString());
      if(findExpr(e1) != findExpr(e2)) {
        DebugAssert(isReal(getBaseType(e2)),
                    "TheoryArith::refineCounterExample: e2 = "+e2.toString()
                    +"\n type(e2) = "+e2.getType().toString());
        Expr eq = e1.eqExpr(e2);
        addSplitter(eq);
      }
    }
  }
  TRACE("model", "refineCounterExample[Theory::Arith] ", "", "}");
}


void
TheoryArith::findRationalBound(const Expr& varSide, const Expr& ratSide, 
                               const Expr& var,
                               Rational &r)
{
  Expr c, x;
  separateMonomial(varSide, c, x);
  
  DebugAssert(findExpr(c).isRational(), 
              "seperateMonomial failed"); 
  DebugAssert(findExpr(ratSide).isRational(), 
              "smallest variable in graph, should not have variables"
              " in inequalities: ");
  DebugAssert(x == var, "separateMonomial found different variable: " 
              + var.toString());
  r = findExpr(ratSide).getRational() / findExpr(c).getRational();
} 

bool
TheoryArith::findBounds(const Expr& e, Rational& lub, Rational&  glb)
{
  bool strictLB=false, strictUB=false;
  bool right = (d_inequalitiesRightDB.count(e) > 0
                       && d_inequalitiesRightDB[e]->size() > 0);
  bool left = (d_inequalitiesLeftDB.count(e) > 0
               && d_inequalitiesLeftDB[e]->size() > 0);
  int numRight = 0, numLeft = 0;
  if(right) { //rationals less than e
    CDList<Ineq> * ratsLTe = d_inequalitiesRightDB[e];
    for(unsigned int i=0; i<ratsLTe->size(); i++) {
      DebugAssert((*ratsLTe)[i].varOnRHS(), "variable on wrong side!");
      Expr ineq = (*ratsLTe)[i].ineq().getExpr();
      Expr leftSide = ineq[0], rightSide = ineq[1];
      Rational r;
      findRationalBound(rightSide, leftSide, e , r);
      if(numRight==0 || r>glb){
        glb = r;
        strictLB = isLT(ineq);
      }
      numRight++;
    }
    TRACE("model", "   =>Lower bound ", glb.toString(), "");
  }
  if(left) {   //rationals greater than e
    CDList<Ineq> * ratsGTe = d_inequalitiesLeftDB[e];
    for(unsigned int i=0; i<ratsGTe->size(); i++) { 
      DebugAssert((*ratsGTe)[i].varOnLHS(), "variable on wrong side!");
      Expr ineq = (*ratsGTe)[i].ineq().getExpr();
      Expr leftSide = ineq[0], rightSide = ineq[1];
      Rational r;
      findRationalBound(leftSide, rightSide, e, r); 
      if(numLeft==0 || r<lub) {
        lub = r;
        strictUB = isLT(ineq);
      }
      numLeft++;
    }
    TRACE("model", "   =>Upper bound ", lub.toString(), "");
  }
  if(!left && !right) {
      lub = 0; 
      glb = 0;
  }
  if(!left && right) {lub = glb +2;}
  if(!right && left)  {glb =  lub-2;}
  DebugAssert(glb <= lub, "Greatest lower bound needs to be smaller "
              "than least upper bound"); 
  return strictLB;
}

void TheoryArith::assignVariables(std::vector<Expr>&v)
{
  int count = 0;
  while (v.size() > 0) {
    std::vector<Expr> bottom;
    d_graph.selectSmallest(v, bottom);
    TRACE("model", "Finding variables to assign. Iteration # ", count, "");
    for(unsigned int i = 0; i<bottom.size(); i++) {
      Expr e = bottom[i];
      TRACE("model", "Found: ", e, "");
      // Check if it is already a concrete constant
      if(e.isRational()) continue;
      
      Rational lub, glb;
      bool strictLB;
      strictLB = findBounds(e, lub, glb);
      Rational mid;
      if(isInteger(e)) {
        if(strictLB && glb.isInteger())
          mid = glb + 1;
        else
          mid = ceil(glb);
      }
      else
        mid = (lub + glb)/2;
      TRACE("model", "Assigning mid = ", mid, " {");
      assignValue(e, rat(mid));
      TRACE("model", "Assigned find(e) = ", findExpr(e), " }");
      if(inconsistent()) return; // Punt immediately if failed
    }
    count++;
  }
}

void TheoryArith::computeModelBasic(const std::vector<Expr>& v)
{
  d_inModelCreation = true;
  vector<Expr> reps;
  TRACE("model", "Arith=>computeModel ", "", "{");
  for(unsigned int i=0; i <v.size(); ++i) {
    const Expr& e = v[i];
    if(findExpr(e) == e) {
      TRACE("model", "arith variable:", e , "");
      reps.push_back(e);
    }
    else {
      TRACE("model", "arith variable:", e , "");
      TRACE("model", " ==> is defined by: ", findExpr(e) , "");
    }
  }
  assignVariables(reps);
  TRACE("model", "Arith=>computeModel", "", "}");
  d_inModelCreation = false;
}

// For any arith expression 'e', if the subexpressions are assigned
// concrete values, then find(e) must already be a concrete value.
void TheoryArith::computeModel(const Expr& e, vector<Expr>& vars) {
  DebugAssert(findExpr(e).isRational(), "TheoryArith::computeModel("
              +e.toString()+")\n e is not assigned concrete value.\n"
              +" find(e) = "+findExpr(e).toString());
  assignValue(simplify(e));
  vars.push_back(e);
}



/*! accepts a rewrite theorem over eqn|ineqn and normalizes it
 *  and returns a theorem to that effect. assumes e is non-trivial
 *  i.e. e is not '0=const' or 'const=0' or '0 <= const' etc.
 */
Theorem TheoryArith::normalize(const Expr& e) {
  //e is an eqn or ineqn. e is not a trivial eqn or ineqn
  //trivial means 0 = const or 0 <= const.
  TRACE("arith", "normalize(", e, ") {");
  DebugAssert(e.isEq() || isIneq(e),
              "normalize: input must be Eq or Ineq: " + e.toString());
  DebugAssert(!isIneq(e) || (0 == e[0].getRational()),
              "normalize: if (e is ineq) then e[0] must be 0" +
              e.toString());
  if(e.isEq()) {
    if(e[0].isRational()) {
      DebugAssert(0 == e[0].getRational(),
                  "normalize: if e is Eq and e[0] is rat then e[0]==0");
    }
    else {
      //if e[0] is not rational then e[1] must be rational.
      DebugAssert(e[1].isRational() && 0 == e[1].getRational(),
                  "normalize: if e is Eq and e[1] is rat then e[1]==0\n"
                  " e = "+e.toString());
    }
  }
  
  Expr factor;
  if(e[0].isRational())
    factor = computeNormalFactor(e[1]);
  else
    factor = computeNormalFactor(e[0]);
  
  TRACE("arith", "normalize: factor = ", factor, "");
  DebugAssert(factor.getRational() > 0,
              "normalize: factor="+ factor.toString());
  
  Theorem thm(reflexivityRule(e));
  // Now multiply the equality by the factor, unless it is 1
  if(factor.getRational() != 1) {
    int kind = e.getKind();
    switch(kind) {
    case EQ:
      thm = d_rules->multEqn(e[0], e[1], factor);
      // And canonize the result
      thm = canonPredEquiv(thm);
      break;
    case LE:
    case LT:
    case GE:
    case GT:
      thm = d_rules->multIneqn(e, factor);
      // And canonize the result
      thm = canonPredEquiv(thm);
      break;
    default:
      DebugAssert(false,
                  "normalize: control should not reach here" + kind);
      break;
    }
  }
  TRACE("arith", "normalize => ", thm, " }");
  return(thm);
}


Theorem TheoryArith::normalize(const Theorem& eIffEqn) {
  return transitivityRule(eIffEqn, normalize(eIffEqn.getRHS()));
}


Theorem TheoryArith::rewrite(const Expr& e)
{
  TRACE("arith", "TheoryArith::rewrite(", e, ") {");
  Theorem thm;
  if (!e.isTerm()) {
    if (!e.isAbsLiteral()) {
      e.setRewriteNormal();
      thm = reflexivityRule(e);
      TRACE("arith", "TheoryArith::rewrite[non-literal] => ", thm, " }");
      return thm;
    }
    switch(e.getKind()) {
    case EQ:
    {
      // canonical form for an equality of two leaves
      // is just l == r instead of 0 + (-1 * l) + r = 0.
      if (isLeaf(e[0]) && isLeaf(e[1]))
        thm = reflexivityRule(e);
      else { // Otherwise, it is "lhs = 0"
        //first convert e to the form 0=e'
        if((e[0].isRational() && e[0].getRational() == 0)
           || (e[1].isRational() && e[1].getRational() == 0))
          //already in 0=e' or e'=0 form
          thm = reflexivityRule(e);
        else {
          thm = d_rules->rightMinusLeft(e);
          thm = canonPredEquiv(thm);
        }
        // Check for trivial equation
        if ((thm.getRHS())[0].isRational() && (thm.getRHS())[1].isRational()) {
          thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
        } else {
          //else equation is non-trivial
          thm = normalize(thm);
          // Normalization may yield non-simplified terms
          thm = canonPredEquiv(thm);

        }
      }

      // Equations must be oriented such that lhs >= rhs as Exprs;
      // this ordering is given by operator<(Expr,Expr).
      const Expr& eq = thm.getRHS();
      if(eq.isEq() && eq[0] < eq[1])
        thm = transitivityRule(thm, getCommonRules()->rewriteUsingSymmetry(eq));
    }
    break;
    case GRAY_SHADOW:
    case DARK_SHADOW:
      thm = reflexivityRule(e);
      break;
    case IS_INTEGER: {
      Theorem res(isIntegerDerive(e, typePred(e[0])));
      if(!res.isNull())
        thm = getCommonRules()->iffTrue(res);
      else 
        thm = reflexivityRule(e);
      break;
    }
    case NOT:    
      if (!isIneq(e[0]))
        //in this case we have "NOT of DARK or GRAY_SHADOW."
        thm = reflexivityRule(e);
      else {
        //In this case we have the "NOT of ineq". get rid of NOT
        //and then treat like an ineq
        thm = d_rules->negatedInequality(e);
        DebugAssert(isGE(thm.getRHS()) || isGT(thm.getRHS()),
                    "Expected GE or GT");
        thm = transitivityRule(thm, d_rules->flipInequality(thm.getRHS()));
        thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
        thm = canonPredEquiv(thm);

        // Check for trivial inequation
        if ((thm.getRHS())[1].isRational())
          thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
        else {
          //else ineq is non-trivial
          thm = normalize(thm);
          // Normalization may yield non-simplified terms
          thm = canonPredEquiv(thm);
        }
      }
      break;
    case LE:
    case LT:
    case GE:
    case GT:
      if (isGE(e) || isGT(e)) {
        thm = d_rules->flipInequality(e);
        thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
      }
      else 
        thm = d_rules->rightMinusLeft(e);
      thm = canonPredEquiv(thm);
   
      // Check for trivial inequation
      if ((thm.getRHS())[1].isRational()) 
        thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
      else { // ineq is non-trivial
        thm = normalize(thm);
        thm = canonPredEquiv(thm);
      }
      break;
    default:
      DebugAssert(false,
                  "Theory_Arith::rewrite: control should not reach here");
      break;
    }
  }
  else {
    if (e.isAtomic())
      thm = canon(e);
    // Do we still need to simplify? Now that assertEqualities() has a
    // queue and we can safely assume that all children of e are
    // canonized at this point...
    //
    //      thm = canonSimplify(e);
    else 
      thm = reflexivityRule(e);
  }
  // Arith canonization is idempotent
  thm.getRHS().setRewriteNormal();
  TRACE("arith", "TheoryArith::rewrite => ", thm, " }");
  return thm;
}


void TheoryArith::setup(const Expr& e)
{
  if (!e.isTerm()) {
    if (e.isNot() || e.isEq() || isDarkShadow(e) || isGrayShadow(e)) return;
    if(e.getKind() == IS_INTEGER) {
      e[0].addToNotify(this, e);
      return;
    }
    DebugAssert((isLT(e)||isLE(e)) &&
                e[0].isRational() && e[0].getRational() == 0,
                "TheoryArith::setup: expected 0 < rhs:" + e.toString());
    e[1].addToNotify(this, e);
    return;
  }
  int k(0), ar(e.arity());
  for ( ; k < ar; ++k) {
    e[k].addToNotify(this, e);
    TRACE("arith setup", "e["+int2string(k)+"]: ", *(e[k].getNotify()), "");
  }
}


void TheoryArith::update(const Theorem& e, const Expr& d)
{
  if (inconsistent()) return;
  IF_DEBUG(debugger.counter("arith update total")++);
  if (!d.hasFind()) return;
  if (isIneq(d)) {
    // Substitute e[1] for e[0] in d and enqueue new inequality
    DebugAssert(e.getLHS() == d[1], "Mismatch");
    Theorem thm = find(d);
    //    DebugAssert(thm.getRHS() == trueExpr(), "Expected find = true");
    vector<unsigned> changed;
    vector<Theorem> children;
    changed.push_back(1);
    children.push_back(e);
    Theorem thm2 = substitutivityRule(d, changed, children);
    if (thm.getRHS() == trueExpr()) {
      enqueueFact(iffMP(getCommonRules()->iffTrueElim(thm), thm2));
    }
    else {
      enqueueFact(getCommonRules()->iffFalseElim(
        transitivityRule(symmetryRule(thm2), thm)));
    }
    IF_DEBUG(debugger.counter("arith update ineq")++);
  }
  else if (find(d).getRHS() == d) {
    // Substitute e[1] for e[0] in d and assert the result equal to d
    Theorem thm = updateHelper(d);
    TRACE("arith", "TheoryArith::update(): thm = ", thm, "");
    // This no longer holds, due to array theory violating the global invariant
//     DebugAssert(leavesAreSimp(thm.getRHS()), "updateHelper error: "
//              +thm.getExpr().toString());
    enqueueEquality(transitivityRule(thm, rewrite(thm.getRHS())));
//     for (int k(0), ar(d.arity()); k < ar; ++k)
//       d[k].removeFromNotify(this, d);
    IF_DEBUG(debugger.counter("arith update find(d)=d")++);
  } else {
    // We need to update expressions that haven't yet been updated.
    // FIXME: delete 'd' from notify list, once this functionality is
    // merged to the main trunk
    Theorem thm = updateHelper(d);
    TRACE("arith", "TheoryArith::update()[non-rep]: thm = ", thm, "");
    enqueueFact(thm);
//     for (int k(0), ar(d.arity()); k < ar; ++k)
//       d[k].removeFromNotify(this, d);
    IF_DEBUG(debugger.counter("arith update find(d)!=d")++);
  }
}


Theorem TheoryArith::solve(const Theorem& thm)
{
  const Expr& e = thm.getExpr();
  DebugAssert(e.isEq(), "");

  // Check for already solved equalities.

  // Have to be careful about the types: integer variable cannot be
  // assigned a real term.  Also, watch for e[0] being a subexpression
  // of e[1]: this would create an unsimplifiable expression.
  if (isLeaf(e[0]) && !isLeafIn(e[0], e[1]) 
      && (!isInteger(e[0]) || isInteger(e[1]))
      // && !e[0].subExprOf(e[1])
      )
    return thm;

  // Symmetric version is already solved
  if (isLeaf(e[1]) && !isLeafIn(e[1], e[0])
      && (isInteger(e[0]) || !isInteger(e[1]))
      // && !e[1].subExprOf(e[0])
      )
    return symmetryRule(thm);

  return doSolve(thm);
}


void TheoryArith::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
  switch(e.getKind()) {
  case RATIONAL_EXPR: // Skip the constants
    break;
  case PLUS:
  case MULT:
  case DIVIDE:
  case POW: // This is not a variable; extract the variables from children
    for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
      // getModelTerm(*i, v);
      v.push_back(*i);
    break;
  default: { // Otherwise it's a variable.  Check if it has a find pointer
    Expr e2(findExpr(e));
    if(e==e2) {
      TRACE("model", "TheoryArith::computeModelTerm(", e, "): a variable");
      // Leave it alone (it has no descendants)
      // v.push_back(e);
    } else {
      TRACE("model", "TheoryArith::computeModelTerm("+e.toString()
            +"): has find pointer to ", e2, "");
      v.push_back(e2);
    }
  }
  }
}


Expr TheoryArith::computeTypePred(const Type& t, const Expr& e) {
  Expr tExpr = t.getExpr();
  switch(tExpr.getKind()) {
  case INT:  
    return Expr(IS_INTEGER, e);
  case SUBRANGE: {
    std::vector<Expr> kids;
    kids.push_back(Expr(IS_INTEGER, e));
    kids.push_back(leExpr(tExpr[0], e));
    kids.push_back(leExpr(e, tExpr[1]));
    return andExpr(kids);
  }
  default:
    return e.getEM()->trueExpr();
  }
}


void TheoryArith::checkType(const Expr& e)
{
  switch (e.getKind()) {
    case INT:
    case REAL:
      if (e.arity() > 0) {
        throw Exception("Ill-formed arithmetic type: "+e.toString());
      }
      break;
    case SUBRANGE:
      if (e.arity() != 2 ||
          !isIntegerConst(e[0]) ||
          !isIntegerConst(e[1]) ||
          e[0].getRational() > e[1].getRational()) {
        throw Exception("bad SUBRANGE type expression"+e.toString());
      }
      break;
    default:
      DebugAssert(false, "Unexpected kind in TheoryArith::checkType"
                  +getEM()->getKindName(e.getKind()));
  }
}


void TheoryArith::computeType(const Expr& e)
{
  switch (e.getKind()) {
  case RATIONAL_EXPR:
      if(e.getRational().isInteger())
        e.setType(d_intType);
      else
        e.setType(d_realType);
      break;
  case UMINUS:
  case PLUS:
  case MINUS:
  case MULT:
  case POW: {
    bool isInt = true;
    for(int k = 0; k < e.arity(); ++k) {
      if(d_realType != getBaseType(e[k]))
        throw TypecheckException("Expecting type REAL with `" +
                                 getEM()->getKindName(e.getKind()) + "',\n"+
                                 "but got a " + getBaseType(e[k]).toString()+ 
                                 " for:\n" + e.toString());
      if(isInt && !isInteger(e[k]))
        isInt = false;
    }
    if(isInt)
      e.setType(d_intType);
    else
      e.setType(d_realType);
    break;
    }
  case DIVIDE: {
    Expr numerator = e[0];
    Expr denominator = e[1];
    if (getBaseType(numerator) != d_realType ||
        getBaseType(denominator) != d_realType) {
      throw TypecheckException("Expecting only REAL types with `DIVIDE',\n"
                               "but got " + getBaseType(numerator).toString()+ 
                               " and " + getBaseType(denominator).toString() +
                               " for:\n" + e.toString());
    }
    if(denominator.isRational() && 1 == denominator.getRational())
      e.setType(numerator.getType());
    else
      e.setType(d_realType);
    break;
    }
  case LT:
  case LE:
  case GT:
  case GE:
  case GRAY_SHADOW:
    // Need to know types for all exprs -Clark
    //    e.setType(boolType());
    //    break;
  case DARK_SHADOW:
    for (int k = 0; k < e.arity(); ++k) {
      if (d_realType != getBaseType(e[k]))
        throw TypecheckException("Expecting type REAL with `" +
                                 getEM()->getKindName(e.getKind()) + "',\n"+
                                 "but got a " + getBaseType(e[k]).toString()+ 
                                 " for:\n" + e.toString());
    }

    e.setType(boolType());
    break;
  case IS_INTEGER:
    if(d_realType != getBaseType(e[0]))
      throw TypecheckException("Expected type REAL, but got "
                               +getBaseType(e[0]).toString()
                               +"\n\nExpr = "+e.toString());
    e.setType(boolType());
    break;
  default:
    DebugAssert(false,"TheoryArith::computeType: unexpected expression:\n "
                +e.toString());
    break;
  }
}


Type TheoryArith::computeBaseType(const Type& t) {
  IF_DEBUG(int kind = t.getExpr().getKind());
  DebugAssert(kind==INT || kind==REAL || kind==SUBRANGE,
              "TheoryArith::computeBaseType("+t.toString()+")");
  return realType();
}


Expr
TheoryArith::computeTCC(const Expr& e) {
  Expr tcc(Theory::computeTCC(e));
  switch(e.getKind()) {
  case DIVIDE:
    DebugAssert(e.arity() == 2, "");
    return tcc.andExpr(!(e[1].eqExpr(rat(0))));
  default:
    return tcc;
  }
}

///////////////////////////////////////////////////////////////////////////////
//parseExprOp:
//translating special Exprs to regular EXPR??
///////////////////////////////////////////////////////////////////////////////
Expr
TheoryArith::parseExprOp(const Expr& e) {
  TRACE("parser", "TheoryArith::parseExprOp(", e, ")");
  //std::cout << "Were here";
  // If the expression is not a list, it must have been already
  // parsed, so just return it as is.
  switch(e.getKind()) {
  case ID: {
    int kind = getEM()->getKind(e[0].getString());
    switch(kind) {
    case NULL_KIND: return e; // nothing to do
    case REAL:
    case INT:
    case NEGINF: 
    case POSINF: return getEM()->newLeafExpr(kind);
    default:
      DebugAssert(false, "Bad use of bare keyword: "+e.toString());
      return e;
    }
  }
  case RAW_LIST: break; // break out of switch, do the hard work
  default:
    return e;
  }

  DebugAssert(e.getKind() == RAW_LIST && e.arity() > 0,
              "TheoryArith::parseExprOp:\n e = "+e.toString());
  
  const Expr& c1 = e[0][0];
  int kind = getEM()->getKind(c1.getString());
  switch(kind) {
    case UMINUS: {
      if(e.arity() != 2)
        throw ParserException("UMINUS requires exactly one argument: "
                        +e.toString());
      return uminusExpr(parseExpr(e[1])); 
    }
    case PLUS: {
      vector<Expr> k;
      Expr::iterator i = e.begin(), iend=e.end();
      // Skip first element of the vector of kids in 'e'.
      // The first element is the operator.
      ++i; 
      // Parse the kids of e and push them into the vector 'k'
      for(; i!=iend; ++i) k.push_back(parseExpr(*i));
      return plusExpr(k); 
    }
    case MINUS: {
      if(e.arity() == 2)
        return uminusExpr(parseExpr(e[1]));
      else if(e.arity() == 3)
        return minusExpr(parseExpr(e[1]), parseExpr(e[2]));
      else
        throw ParserException("MINUS requires one or two arguments:"
                        +e.toString());
    }
    case MULT: {
      vector<Expr> k;
      Expr::iterator i = e.begin(), iend=e.end();
      // Skip first element of the vector of kids in 'e'.
      // The first element is the operator.
      ++i; 
      // Parse the kids of e and push them into the vector 'k'
      for(; i!=iend; ++i) k.push_back(parseExpr(*i));
      return multExpr(k);
    }
    case POW: { 
      return powExpr(parseExpr(e[1]), parseExpr(e[2])); 
    }
    case DIVIDE:
      { return divideExpr(parseExpr(e[1]), parseExpr(e[2]));    }
    case LT:    
      { return ltExpr(parseExpr(e[1]), parseExpr(e[2]));        }
    case LE:    
      { return leExpr(parseExpr(e[1]), parseExpr(e[2]));        }
    case GT:    
      { return gtExpr(parseExpr(e[1]), parseExpr(e[2]));        }
    case GE:    
      { return geExpr(parseExpr(e[1]), parseExpr(e[2]));        }
    case INTDIV:
    case MOD:
    case SUBRANGE: {
      vector<Expr> k;
      Expr::iterator i = e.begin(), iend=e.end();
      // Skip first element of the vector of kids in 'e'.
      // The first element is the operator.
      ++i; 
      // Parse the kids of e and push them into the vector 'k'
      for(; i!=iend; ++i) 
        k.push_back(parseExpr(*i));
      return Expr(kind, k, e.getEM());
    }
    case IS_INTEGER: {
      if(e.arity() != 2)
        throw ParserException("IS_INTEGER requires exactly one argument: "
                        +e.toString());
      return Expr(IS_INTEGER, parseExpr(e[1]));
    }
    default:
      DebugAssert(false,
                  "TheoryArith::parseExprOp: invalid input " + e.toString());
      break;
  }
  return e;
}

///////////////////////////////////////////////////////////////////////////////
// Pretty-printing                                                           //
///////////////////////////////////////////////////////////////////////////////


// The following 4 functions are helpers for the SMT-LIB output language.

bool TheoryArith::isSyntacticRational(const Expr& e, Rational& r)
{
  if (e.isRational()) {
    r = e.getRational();
    return true;
  }
  else if (isUMinus(e)) {
    if (isSyntacticRational(e[0], r)) {
      r = -r;
      return true;
    }
  }
  else if (isDivide(e)) {
    Rational num;
    if (isSyntacticRational(e[0], num)) {
      Rational den;
      if (isSyntacticRational(e[1], den)) {
        if (den != 0) {
          r = num / den;
          return true;
        }
      }
    }
  }
  return false;
}


void TheoryArith::printRational(ExprStream& os, const Expr& parent, const Expr& e, const Rational& r, bool checkLhs)
{
  if (checkLhs) {
    if (parent.isEq() && parent[0] == e) {
      // If constant is on lhs, switch sides
      if (isMinus(parent[1])) {
        printMinus(os, parent, parent[1]);
        return;
      }
      else if (isPlus(parent[1])) {
        printPlus(os, parent, parent[1]);
        return;
      }
    }
  }

  // Print rational
  if (r.isInteger()) {
    d_intConstUsed = true;
    if (r < 0) {
      os << "(" << push << "~" << space << (-r).toString() << push << ")";
    }
    else os << r.toString();
  }
  else {
    d_realUsed = true;
    os << "(" << push << "/ ";
    Rational tmp = r.getNumerator();
    if (tmp < 0) {
      os << "(" << push << "~" << space << (-tmp).toString() << push << ")";
    }
    else os << tmp.toString();
    os << space;
    tmp = r.getDenominator();
    DebugAssert(tmp > 0 && tmp.isInteger(), "Unexpected rational denominator");
    os << tmp.toString() << push << ")";
  }

  // Figure out language
  if (parent.isNull() || (!parent.isEq() && !isIneq(parent))) {
    if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY;
    return;
  }
  if (d_langUsed == NONLINEAR) return;
  else {
    Expr otherSide = parent[0];
    if (otherSide == e) otherSide = parent[1];
    if (isPlus(otherSide) || isMinus(otherSide))
      return;
  }
  if (d_convertToDiff == "" || parent.isEq()) d_langUsed = LINEAR;
}


bool TheoryArith::isSyntacticUMinusVar(const Expr& e, Expr& var)
{
  if (isUMinus(e)) {
    if (isLeaf(e[0])) {
      var = e[0];
      return true;
    }
  }
  else if (isMult(e)) {
    Expr coeff;
    if (isLeaf(e[0])) {
      var = e[0];
      coeff = e[1];
    }
    else if (isLeaf(e[1])) {
      var = e[1];
      coeff = e[0];
    }
    else return false;
    if (coeff.isRational() && coeff.getRational() == -1) {
      return true;
    }
    else if (isUMinus(coeff) && coeff[0].isRational() &&
             coeff[0].getRational() == 1) {
      return true;
    }
  }
  return false;
}


void TheoryArith::printPlus(ExprStream& os, const Expr& parent, const Expr& e)
{
  int i=0, iend=e.arity();
  bool diff = false;
  Expr var;

  // Write as DIFF if possible
  if (iend == 2 && isLeaf(e[0]) && isSyntacticUMinusVar(e[1], var)) {
    os << "(" << push << "-" << space << e[0]
       << space << var << push << ")";
    diff = true;
  }
  else if (iend == 2 && isLeaf(e[1]) && isSyntacticUMinusVar(e[0], var)) {
    os << "(" << push << "-" << space << e[1]
       << space << var << push << ")";
    diff = true;;
  }
  else {
    for(; i!=iend; ++i) {
      if (i < iend-1) {
        if (i > 0) os << space;
        os << "(" << push << "+";
      }
      os << space << e[i];
    }
    for (i=0; i < iend-1; ++i) os << push << ")";
  }

  // Figure out language
  if (parent.isNull() || (!parent.isEq() && !isIneq(parent))) {
    if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY;
    return;
  }
  if (d_langUsed >= LINEAR) return;
  else if (diff) {
    Expr otherSide = parent[0];
    Rational r;
    if (otherSide == e) otherSide = parent[1];
    if (isSyntacticRational(otherSide, r)) {
      d_langUsed = DIFF_ONLY;
      return;
    }
  }
  d_langUsed = LINEAR;
}


void TheoryArith::printMinus(ExprStream& os, const Expr& parent, const Expr& e)
{
  os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
  // Figure out language
  if (parent.isNull() || (!parent.isEq() && !isIneq(parent))) {
    if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY;
    return;
  }
  if (d_langUsed >= LINEAR) return;
  else if (isLeaf(e[0]) && isLeaf(e[1])) {
    Expr otherSide = parent[0];
    Rational r;
    if (otherSide == e) otherSide = parent[1];
    if (isSyntacticRational(otherSide, r)) {
      d_langUsed = DIFF_ONLY;
      return;
    }
  }
  d_langUsed = LINEAR;
}


void TheoryArith::printLhs(ExprStream& os, const Expr& e)
{
  if (d_convertToDiff != "") {
    switch (e.getKind()) {
      case RATIONAL_EXPR:
      case SUBRANGE:
      case IS_INTEGER:
      case PLUS:
      case MINUS:
      case UMINUS:
      case MULT:
      case POW:
      case DIVIDE:
      case DARK_SHADOW:
      case GRAY_SHADOW:
        break;
      case CONSTDEF:
        if (e.arity() == 2) {
          printLhs(os, e[1]);
          return;
        }
        //fall through
      default:
        os << "(" << push << "-" << space
           << e << space << d_zeroVar << push << ")";
        return;
    }
  }
  os << e;
}


Expr TheoryArith::rewriteToDiff(const Expr& e)
{
  Expr tmp = e[0] - e[1];
  tmp = canonRec(tmp).getRHS();
  switch (tmp.getKind()) {
    case RATIONAL_EXPR: {
      Rational r = tmp.getRational();
      switch (e.getKind()) {
        case LT:
          if (r < 0) return trueExpr();
          else return falseExpr();
        case LE:
          if (r <= 0) return trueExpr();
          else return falseExpr();
        case GT:
          if (r > 0) return trueExpr();
          else return falseExpr();
        case GE:
          if (r >= 0) return trueExpr();
          else return falseExpr();
        case EQ:
          if (r == 0) return trueExpr();
          else return falseExpr();
      }
    }
    case MULT:
      if (d_convertToDiff == "") return e;
      DebugAssert(tmp[0].isRational(), "Unexpected term structure from canon");
      if (tmp[0].getRational() != -1) return e;
      return Expr(e.getOp(), d_zeroVar - tmp[1], rat(0));
    case PLUS: {
      Expr c = tmp[0];
      DebugAssert(c.isRational(), "Unexpected term structure from canon");
      Expr x, y;
      if (tmp.arity() == 2) {
        if (tmp[1].getKind() == MULT) {
          x = d_zeroVar;
          y = tmp[1];
        }
        else {
          x = tmp[1];
          y = rat(-1) * d_zeroVar;
        }
      }
      else if (tmp.arity() == 3) {
        if (tmp[1].getKind() == MULT) {
          x = tmp[2];
          y = tmp[1];
        }
        else if (tmp[2].getKind() == MULT) {
          x = tmp[1];
          y = tmp[2];
        }
        else return e;
      }
      else return e;
      if (x.getKind() == MULT) return e;
      DebugAssert(y[0].isRational(), "Unexpected term structure from canon");
      if (y[0].getRational() != -1) return e;
      return Expr(e.getOp(), x - y[1], -c);
    }
    default:
      if (d_convertToDiff != "") {
        return Expr(e.getOp(), tmp - d_zeroVar, rat(0));
      }
      break;
  }
  return e;
}


bool TheoryArith::isAtomicArithTerm(const Expr& e)
{
  switch (e.getKind()) {
    case RATIONAL_EXPR:
      return true;
    case ITE:
      return false;
    case UMINUS:
    case PLUS:
    case MINUS:
    case MULT:
    case DIVIDE:
    case POW:
    case INTDIV:
    case MOD: {
      int i=0, iend=e.arity();
      for(; i!=iend; ++i) {
        if (!isAtomicArithTerm(e[i])) return false;
      }
      break;
    }
    default:
      break;
  }
  return true;
}


bool TheoryArith::isAtomicArithFormula(const Expr& e)
{
  switch (e.getKind()) {
    case LT:
    case GT:
    case LE:
    case GE:
    case EQ:
      return isAtomicArithTerm(e[0]) && isAtomicArithTerm(e[1]);
  }
  return false;
}


ExprStream&
TheoryArith::print(ExprStream& os, const Expr& e) {
  switch(os.lang()) {
    case PRESENTATION_LANG:
      switch(e.getKind()) {
        case REAL:
        case INT:
        case RATIONAL_EXPR:
        case NEGINF:
        case POSINF:
          e.print(os);
          break;
        case SUBRANGE:
          if(e.arity() != 2) e.printAST(os);
          else 
            os << "[" << push << e[0] << ".." << e[1] << push << "]";
          break;
        case IS_INTEGER:
          if(e.arity() == 1)
            os << "IS_INTEGER(" << push << e[0] << push << ")";
          else
            e.printAST(os);
          break;
        case PLUS:  {
          int i=0, iend=e.arity();
          os << "(" << push;
          if(i!=iend) os << e[i];
          ++i;
          for(; i!=iend; ++i) os << space << "+ " << e[i];
          os << push << ")";
          break;
        }
        case MINUS:
          os << "(" << push << e[0] << space << "- " << e[1] << push << ")";
          break;
        case UMINUS:
          os << "-(" << push << e[0] << push << ")";
          break;
        case MULT:  {
          int i=0, iend=e.arity();
          os << "(" << push;
          if(i!=iend) os << e[i];
          ++i;
          for(; i!=iend; ++i) os << space << "* " << e[i];
          os << push << ")";
          break;
        }
        case POW:
          os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
          break;
        case DIVIDE:
          os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
          break;
        case LT:
          if (isInt(e[0].getType()) || isInt(e[1].getType())) {
          }
          os << "(" << push << e[0] << space << "< " << e[1] << push << ")";
          break;
        case LE:
          os << "(" << push << e[0] << space << "<= " << e[1] << push << ")";
          break;
        case GT:
          os << "(" << push << e[0] << space << "> " << e[1] << push << ")";
          break;
        case GE:
          os << "(" << push << e[0] << space << ">= " << e[1] << push << ")";
          break;
        case DARK_SHADOW:
          os << "DARK_SHADOW(" << push << e[0] << ", " << space << e[1] << push << ")";
          break;
        case GRAY_SHADOW:
          os << "GRAY_SHADOW(" << push << e[0] << ","  << space << e[1]
             << "," << space << e[2] << "," << space << e[3] << push << ")";
          break;
        default:
          // Print the top node in the default LISP format, continue with
          // pretty-printing for children.
          e.printAST(os);

          break;
      } 
      break; // end of case PRESENTATION_LANG
    case SMTLIB_LANG: {
      Expr parent = os.getParent();
      switch(e.getKind()) {
        case RATIONAL_EXPR:
          printRational(os, parent, e, e.getRational());
          break;
        case REAL:
          if(theoryCore()->getFlags()["real2int"].getBool()) {
            d_intUsed = true;
            os << "Int";
          }
          else {
            d_realUsed = true;
            os << "Real";
          }
          break;
        case INT:
          d_intUsed = true;
          os << "Int";
          break;
        case SUBRANGE:
          throw SmtlibException("TheoryArith::print: SMTLIB: SUBRANGE not implemented");
//           if(e.arity() != 2) e.print(os);
//           else 
//             os << "(" << push << "SUBRANGE" << space << e[0]
//             << space << e[1] << push << ")";
          break;
        case IS_INTEGER:
          d_intUsed = true;
          if(e.arity() == 1)
            os << "(" << push << "IsInt" << space << e[0] << push << ")";
          else
            throw SmtlibException("TheoryArith::print: SMTLIB: IS_INTEGER used unexpectedly");
          break;
        case PLUS:  {
          Rational r;
          if (parent.isEq() && isSyntacticRational(parent[0], r)) {
            printRational(os, parent, parent[0], r, false);
          }
          else {
            printPlus(os, parent, e);
          }
          break;
        }
        case MINUS: {
          Rational r;
          if (parent.isEq() && isSyntacticRational(parent[0], r)) {
            printRational(os, parent, parent[0], r, false);
          }
          else {
            printMinus(os, parent, e);
          }
          break;
        }
        case UMINUS: {
          Rational r;
          if (isSyntacticRational(e, r)) {
            printRational(os, parent, e, r);
          }
          else {
            os << "(" << push << "~" << space << e[0] << push << ")";
            if (parent.isNull() || (!parent.isEq() && !isIneq(parent))) {
              if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY;
              break;
            }
            if (d_langUsed >= LINEAR) break;
            d_langUsed = LINEAR;
          }
          break;
        }
        case MULT:  {
          int i=0, iend=e.arity();
          for(; i!=iend; ++i) {
            if (i < iend-1) {
              os << "(" << push << "*";
            }
            os << space << e[i];
          }
          for (i=0; i < iend-1; ++i) os << push << ")";
          // Figure out language
          if (parent.isNull() || (!parent.isEq() && !isIneq(parent))) {
            if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY;
            break;
          }
          if (d_langUsed == NONLINEAR) break;
          d_langUsed = LINEAR;
          bool nonconst = false;
          Rational r;
          for (i=0; i!=iend; ++i) {
            if (isSyntacticRational(e[i], r)) {
              continue;
            }
            if (nonconst) {
              d_langUsed = NONLINEAR;
              break;
            }
            nonconst = true;
          }
          break;
        }
        case POW:
          throw SmtlibException("TheoryArith::print: SMTLIB: POW not supported");
          os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
          break;
        case DIVIDE: {
          Rational r;
          if (isSyntacticRational(e, r)) {
            printRational(os, parent, e, r);
            break;
          }
          else if (e[1].isRational()) {
            r = e[1].getRational();
            if (r != 0) {
              r = 1 / r;
              os << "(" << push << "*" << space << e[0] << space;
              printRational(os, Expr(), Expr(), r, false);
              os << push << ")";
              // Figure out language
              if (parent.isNull() || (!parent.isEq() && !isIneq(parent))) {
                if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY;
                break;
              }
              if (d_langUsed == NONLINEAR) break;
              d_langUsed = LINEAR;
              break;
            }
          }
          throw SmtlibException("TheoryArith::print: SMTLIB: unexpected use of DIVIDE");
          break;
        }
        case LT: {
          Rational r;
          if (isSyntacticRational(e[0], r)) {
            os << "(" << push << ">" << space;
            printLhs(os, e[1]);
            os << space << e[0] << push << ")";
          }
          else {
            os << "(" << push << "<" << space;
            printLhs(os, e[0]);
            os << space << e[1] << push << ")";
          }
          if (d_langUsed >= DIFF_ONLY) break;
          if (!isAtomicArithFormula(e)) d_langUsed = LINEAR;
          else d_langUsed = DIFF_ONLY;
          break;
        }
        case LE: {
          Rational r;
          if (isSyntacticRational(e[0], r)) {
            os << "(" << push << ">=" << space;
            printLhs(os, e[1]);
            os << space << e[0] << push << ")";
          }
          else {
            os << "(" << push << "<=" << space;
            printLhs(os, e[0]);
            os << space << e[1] << push << ")";
          }
          if (d_langUsed >= DIFF_ONLY) break;
          if (!isAtomicArithFormula(e)) d_langUsed = LINEAR;
          else d_langUsed = DIFF_ONLY;
          break;
        }
        case GT: {
          Rational r;
          if (isSyntacticRational(e[0], r)) {
            os << "(" << push << "<" << space;
            printLhs(os, e[1]);
            os << space << e[0] << push << ")";
          }
          else {
            os << "(" << push << ">" << space;
            printLhs(os, e[0]);
            os << space << e[1] << push << ")";
          }
          if (d_langUsed >= DIFF_ONLY) break;
          if (!isAtomicArithFormula(e)) d_langUsed = LINEAR;
          else d_langUsed = DIFF_ONLY;
          break;
        }
        case GE: {
          Rational r;
          if (isSyntacticRational(e[0], r)) {
            os << "(" << push << "<=" << space;
            printLhs(os, e[1]);
            os << space << e[0] << push << ")";
          }
          else {
            os << "(" << push << ">=" << space;
            printLhs(os, e[0]);
            os << space << e[1] << push << ")";
          }
          if (d_langUsed >= DIFF_ONLY) break;
          if (!isAtomicArithFormula(e)) d_langUsed = LINEAR;
          else d_langUsed = DIFF_ONLY;
          break;
        }
        case DARK_SHADOW:
          throw SmtlibException("TheoryArith::print: SMTLIB: DARK_SHADOW not supported");
          os << "(" << push << "DARK_SHADOW" << space << e[0]
             << space << e[1] << push << ")";
          break;
        case GRAY_SHADOW:
          throw SmtlibException("TheoryArith::print: SMTLIB: GRAY_SHADOW not supported");
          os << "GRAY_SHADOW(" << push << e[0] << ","  << space << e[1]
             << "," << space << e[2] << "," << space << e[3] << push << ")";
          break;
        default:
          throw SmtlibException("TheoryArith::print: SMTLIB: default not supported");
          // Print the top node in the default LISP format, continue with
          // pretty-printing for children.
          e.printAST(os);

          break;
      } 
      break; // end of case SMTLIB_LANG
    }
    case LISP_LANG:
      switch(e.getKind()) {
        case REAL:
        case INT:
        case RATIONAL_EXPR:
        case NEGINF:
        case POSINF:
          e.print(os);
          break;
        case SUBRANGE:
          if(e.arity() != 2) e.printAST(os);
          else 
            os << "(" << push << "SUBRANGE" << space << e[0]
               << space << e[1] << push << ")";
          break;
        case IS_INTEGER:
          if(e.arity() == 1)
            os << "(" << push << "IS_INTEGER" << space << e[0] << push << ")";
          else
            e.printAST(os);
          break;
        case PLUS:  {
          int i=0, iend=e.arity();
          os << "(" << push << "+";
          for(; i!=iend; ++i) os << space << e[i];
          os << push << ")";
          break;
        }
        case MINUS:
        //os << "(" << push << e[0] << space << "- " << e[1] << push << ")";
          os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
          break;
        case UMINUS:
          os << "(" << push << "-" << space << e[0] << push << ")";
          break;
        case MULT:  {
          int i=0, iend=e.arity();
          os << "(" << push << "*";
          for(; i!=iend; ++i) os << space << e[i];
          os << push << ")";
          break;
        }
        case POW:
          os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
          break;
        case DIVIDE:
          os << "(" << push << "/ " << e[0] << space << e[1] << push << ")";
          break;
        case LT:
          os << "(" << push << "< " << e[0] << space << e[1] << push << ")";
          break;
        case LE:
          os << "(" << push << "<= " << e[0] << space << e[1] << push << ")";
          break;
        case GT:
          os << "(" << push << "> " << e[1]  << space << e[0] << push << ")";
          break;
        case GE:
          os << "(" << push << ">= " << e[0] << space << e[1] << push << ")";
          break;
        case DARK_SHADOW:
          os << "(" << push << "DARK_SHADOW" << space << e[0]
             << space << e[1] << push << ")";
          break;
        case GRAY_SHADOW:
          os << "(" << push << "GRAY_SHADOW" << space << e[0] << space
             << e[1] << space << e[2] << space << e[3] << push << ")";
          break;
        default:
          // Print the top node in the default LISP format, continue with
          // pretty-printing for children.
          e.printAST(os);

          break;
      } 
      break; // end of case LISP_LANG
    default:
     // Print the top node in the default LISP format, continue with
     // pretty-printing for children.
       e.printAST(os);
  }
  return os;
}


//! Construct the gray shadow expression representing c1 <= e <= c2
// Expr TheoryArith::grayShadow(const Expr& v, const Expr& e,
//                           const Rational& c1, const Rational& c2) {
//   ExprGrayShadow ev(getEM(), v, e, c1, c2, d_grayShadowMMIndex);
//   return getEM()->newExpr(&ev);
// }


//! Access lhs constant in gray shadow
// const Rational& TheoryArith::getC1(const Expr& e) {
//   DebugAssert(isGrayShadow(e),
//            "TheoryArith::getC1("+e.toString()
//            +"): not a gray shadow");
//   return e.getRatValue(0);
// }


//! Access rhs constant in gray shadow
// const Rational& TheoryArith::getC2(const Expr& e) {
//   DebugAssert(isGrayShadow(e),
//            "TheoryArith::getC2("+e.toString()
//            +"): not a gray shadow");
//   return e.getRatValue(1);
// }


//! Access the monomial in gray shadow
// const Expr& TheoryArith::getV(const Expr& e) {
//   DebugAssert(isGrayShadow(e),
//            "TheoryArith::getV("+e.toString()
//            +"): not a gray shadow");
//   return e.getExprValue(0);
// }

//! Access the expression in gray shadow
// const Expr& TheoryArith::getE(const Expr& e) {
//   DebugAssert(isGrayShadow(e),
//            "TheoryArith::getE("+e.toString()
//            +"): not a gray shadow");
//   return e.getExprValue(1);
// }

---