theory_core.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file theory_core.cpp
 * 
 * Author: Clark Barrett, Vijay Ganesh (CNF converter)
 * 
 * Created: Thu Jan 30 16:57:52 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 "command_line_flags.h"
#include "expr.h"
#include "notifylist.h"
#include "pretty_printer.h"
#include "common_proof_rules.h"
#include "parser_exception.h"
#include "typecheck_exception.h"
#include "smtlib_exception.h"
#include "eval_exception.h"
#include "theory_core.h"
#include "expr_transform.h"
#include "core_proof_rules.h"
#include "theorem_manager.h"


using namespace std;


namespace CVCL {


  //! Implementation of PrettyPrinter class
  /*! \ingroup PrettyPrinting */
  class PrettyPrinterCore: public PrettyPrinter {
  private:
    TheoryCore *d_core;
    //! Disable the default constructor
    PrettyPrinterCore() { }
  public:
    //! Constructor
    PrettyPrinterCore(TheoryCore* core): d_core(core) { }
    ExprStream& print(ExprStream& os, const Expr& e) {
      if(e.isString())
        return e.print(os);
      else if (e.isApply())
        return d_core->theoryOf(e)->print(os, e);
      else if(d_core->hasTheory(e.getKind()))
        return d_core->theoryOf(e.getKind())->print(os, e);
      else
        return e.print(os);
    }
  };


  class TypeComputerCore: public ExprManager::TypeComputer {
    TheoryCore *d_core;
  public:
    TypeComputerCore(TheoryCore* core): d_core(core) { }
    void computeType(const Expr& e) {
      DebugAssert(!e.isVar(), "Variables should have a type: "+e.toString());
      Theory* i = d_core->theoryOf(e.getKind());
      if (e.isApply()) i = d_core->theoryOf(e);
      TRACE("types", "computeType["+i->getName()+"](", e, ") {");
      TRACE("types verbose", "kind = ", d_core->getEM()->getKindName(e.getKind()), "");
      i->computeType(e);
      DebugAssert(!e.lookupType().getExpr().isNull(), "Type not set by computeType");
      TRACE("types", "computeType["+i->getName()+"] => ", e.getType(), " }");
    }
    void checkType(const Expr& e) {
      if (!e.isType()) throw Exception
          ("Tried to use non-type as a type: "+e.toString());
      d_core->theoryOf(e)->checkType(e);
      e.setValidType();
    }
  };


  ostream& operator<<(ostream& os, const NotifyList& l) {
    os << "NotifyList(\n";
    for(size_t i=0,iend=l.size(); i<iend; ++i) {
      os << "[" << l.getTheory(i)->getName() << ", " << l.getExpr(i) << "]\n";
    }
    return os << ")";
  }


}


using namespace CVCL;


// File-static helper functions

IF_DEBUG(
//! Check if the vector<Expr> is sorted w.r.t. operator<
static bool isSorted(const vector<Expr>& v) {
  Expr prev;
  for(vector<Expr>::const_iterator i=v.begin(), iend=v.end(); i!=iend;
      prev = *i, ++i) {
    if(prev.isNull()) continue;
    if(!(prev < *i)) return false;
  }
  return true;
}
)

//! Intersection of sorted vectors of Exprs: res := \f$a \cap b\f$
/*! ASSUMPTION: a and b are sorted in ascending order w.r.t. operator<
 */
static void intersect(const vector<Expr>& a, const vector<Expr>& b,
               vector<Expr>& res) {
  DebugAssert(isSorted(a) && isSorted(b), "intersect()");
  size_t i(0), j(0), iend(a.size()), jend(b.size());
  while(i<iend && j<jend) {
    if(a[i] == b[j]) {
      res.push_back(a[i]);
      i++; j++;
    } else if(a[i] < b[j]) i++;
    else j++; // a[i] > b[j]
  }
}

//! Set difference of sorted vectors of Exprs: res := a - b
/*! ASSUMPTION: a and b are sorted in ascending order w.r.t. operator<
 */
static void difference(const vector<Expr>& a, const vector<Expr>& b,
                vector<Expr>& res) {
  DebugAssert(isSorted(a) && isSorted(b), "difference()");
  size_t i(0), j(0), iend(a.size()), jend(b.size());
  while(i < iend) {
    if(j >= jend) { res.push_back(a[i]); i++; }
    else if(a[i]==b[j]) { i++; j++; }
    else if(a[i]<b[j]) { res.push_back(a[i]); i++; }
    else j++; // a[i] > b[j]
  }
}

void
TheoryCore::enqueueSE(const Theorem& thm) {
  TRACE("enqueueSE", "enqueueSE(", thm.getExpr(), ")");
  DebugAssert(d_inAddFact || d_inCheckSATCore || d_inRegisterAtom, "enqueueSE()");
  if(thm.isRewrite() || !thm.getExpr().isTrue())
    d_queueSE.push_back(thm);
}


Theorem TheoryCore::getModelValue(const Expr& e) {
  ExprHashMap<Theorem>::iterator i=d_varAssignments.find(e),
    iend=d_varAssignments.end();
  if(i!=iend) return (*i).second;
  else return find(e);
}


///////////////////////////////////////////////////////////////////////////////
/*!
 * Function: TheoryCore::TheoryCore
 *
 * Author: Clark Barrett
 * 
 * Created: Sat Feb  8 14:57:36 2003
 *
 * Description: Constructor.  Since we are in the middle of creating
 * TheoryCore, we set the pointer to TheoryCore in the Theory base
 * class ourselves.
*/
///////////////////////////////////////////////////////////////////////////////
TheoryCore::TheoryCore(ContextManager* cm,
                       ExprManager* em,
                       TheoremManager* tm,
                       const CLFlags& flags,
                       Statistics& statistics)
  : Theory(), d_cm(cm), d_tm(tm), d_flags(flags), d_statistics(statistics),
    d_inconsistent(cm->getCurrentContext(), false, 0), 
    d_incomplete(cm->getCurrentContext()),
    d_diseq(cm->getCurrentContext()),
    d_incThm(cm->getCurrentContext()),
    d_terms(cm->getCurrentContext()),
    d_vars(cm->getCurrentContext()),
    d_sharedTerms(cm->getCurrentContext()),
    d_solver(NULL),
    d_simplifyInPlace(&(flags["ip"].getBool())),
    d_currentRecursiveSimplifier(NULL),
    d_cnfOption(&(flags["cnf"].getBool())),
    d_resourceLimit(0),
#ifdef DEBUG
    d_dumpTrace(&(flags["dump-trace"].getString())),
    d_inCheckSATCore(false), d_inAddFact(false), d_inSimplify(false),
    d_inRegisterAtom(false),
#endif
    d_notifyObj(this, cm->getCurrentContext()),
    d_impliedLiterals(cm->getCurrentContext()),
    d_impliedLiteralsIdx(cm->getCurrentContext(), 0, 0),
    d_coreSatAPI(NULL)
{
  IF_DEBUG(d_diseq.setName("CDList[TheoryCore::d_diseq]"));
  d_em = em;
  d_theoryCore = this;
  d_commonRules = tm->getRules();
  d_name = "Core";
  d_theoryUsed = false;

  d_rules = createProofRules(tm);
  d_printer = new PrettyPrinterCore(this);
  d_typeComputer = new TypeComputerCore(this);
  d_em->registerTypeComputer(d_typeComputer);
  d_exprTrans = new ExprTransform(this);

  // Register the pretty-printer
  d_em->registerPrettyPrinter(*d_printer);

  // for (int i = 0; i < LAST_KIND; ++i) d_theoryMap[i] = NULL;

  vector<int> kinds;
  kinds.push_back(RAW_LIST);
  kinds.push_back(BOOLEAN);
  kinds.push_back(SUBTYPE);
  kinds.push_back(STRING_EXPR);
  kinds.push_back(ID);
  kinds.push_back(TRUE);
  kinds.push_back(FALSE);
  kinds.push_back(UCONST);
  kinds.push_back(BOUND_VAR);
  kinds.push_back(SKOLEM_VAR);
  kinds.push_back(EQ);
  kinds.push_back(NEQ);
  kinds.push_back(ECHO);
  kinds.push_back(DBG);
  kinds.push_back(TRACE);
  kinds.push_back(UNTRACE);
  kinds.push_back(OPTION);
  kinds.push_back(HELP);
  kinds.push_back(AND);
  kinds.push_back(OR);
  kinds.push_back(IFTHEN);
  kinds.push_back(IF);
  kinds.push_back(ELSE);
  kinds.push_back(COND);
  kinds.push_back(XOR);
  kinds.push_back(NOT);
  kinds.push_back(ITE);
  kinds.push_back(IFF);
  kinds.push_back(IMPLIES);
  kinds.push_back(APPLY);
  // For printing LET expressions (in DAG printing mode)
  kinds.push_back(LET);
  kinds.push_back(LETDECLS);
  kinds.push_back(LETDECL);
  // For printing raw parsed quantifier expressions
  kinds.push_back(VARLIST);
  kinds.push_back(VARDECLS);
  kinds.push_back(VARDECL);

  // Type declarations and definitions
  kinds.push_back(TYPE);
  // For printing type declarations (or definitions)
  kinds.push_back(CONST);

  kinds.push_back(CONSTDEF);
  kinds.push_back(TYPEDEF);
  kinds.push_back(DEFUN);
  // Printing proofs
  kinds.push_back(PF_APPLY);
  kinds.push_back(PF_HOLE);
  // Register commands for pretty-printing.  Currently, only ASSERT
  // needs to be printed.
  kinds.push_back(ASSERT);
  kinds.push_back(QUERY);
  kinds.push_back(PRINT);

  kinds.push_back(DUMP_PROOF);
  kinds.push_back(DUMP_ASSUMPTIONS);
  kinds.push_back(DUMP_SIG);
  kinds.push_back(DUMP_TCC);
  kinds.push_back(DUMP_TCC_ASSUMPTIONS);
  kinds.push_back(DUMP_TCC_PROOF);
  kinds.push_back(DUMP_CLOSURE);
  kinds.push_back(DUMP_CLOSURE_PROOF);
  kinds.push_back(TRANSFORM);
  kinds.push_back(CALL);
  kinds.push_back(WHERE);
  kinds.push_back(ASSERTIONS);
  kinds.push_back(ASSUMPTIONS);
  kinds.push_back(COUNTEREXAMPLE);
  kinds.push_back(COUNTERMODEL);
  kinds.push_back(PUSH);
  kinds.push_back(POP);
  kinds.push_back(POPTO);
  kinds.push_back(PUSH_SCOPE);
  kinds.push_back(POP_SCOPE);
  kinds.push_back(POPTO_SCOPE);
  kinds.push_back(CONTEXT);
  kinds.push_back(FORGET);
  kinds.push_back(GET_TYPE);
  kinds.push_back(CHECK_TYPE);
  kinds.push_back(GET_CHILD);
  kinds.push_back(SUBSTITUTE);
  kinds.push_back(SEQ);

  
  kinds.push_back(AND_R);
  kinds.push_back(IFF_R);
  kinds.push_back(ITE_R);

  registerTheory(this, kinds);
}


TheoryCore::~TheoryCore()
{
  delete d_exprTrans;
  delete d_rules;
  delete d_typeComputer;
  d_em->unregisterPrettyPrinter();
  delete d_printer;
}


///////////////////////////////////////////////////////////////////////////////
// Theory interface implementaion                                            //
///////////////////////////////////////////////////////////////////////////////

void TheoryCore::assertFact(const Theorem& e) {
  DebugAssert(e.getExpr().unnegate().getKind() == SKOLEM_VAR ||
              e.getExpr().unnegate().getKind() == UCONST,
              "TheoryCore::assertFact("+e.toString()+")");
}


void TheoryCore::checkSat(bool fullEffort) {
  // Handle all asserted disequalities
  for (CDList<Theorem>::const_iterator i = d_diseq.begin(), iend=d_diseq.end();
       i!=iend; ++i) {
    const Expr& expr = ((*i).getExpr())[0];
    Theorem thm0 = find(expr[0]);
    Theorem thm1 = find(expr[1]);
    if (thm0.getRHS() == thm1.getRHS()) {
      Theorem leftEqRight = transitivityRule(thm0, symmetryRule(thm1));
      IF_DEBUG(debugger.counter("conflicts from disequalities")++);
      setInconsistent(iffMP(leftEqRight, d_commonRules->notToIff(*i)));
      return;
    }
  }
}


Theorem TheoryCore::rewriteLitCore(const Expr& e)
{
  switch (e.getKind()) {
    case EQ:
      if (e[0] == e[1])
        return d_commonRules->rewriteReflexivity(e);
      else if (e[0] < e[1])
        return d_commonRules->rewriteUsingSymmetry(e);
      break;
    case NOT:
      if (e[0].isTrue())
        return d_commonRules->rewriteNotTrue(e);
      else if (e[0].isFalse())
        return d_commonRules->rewriteNotFalse(e);
      else if (e[0].isNot())
        return d_commonRules->rewriteNotNot(e);
      break;
    default:
      DebugAssert(false,
                  "TheoryCore::rewriteLitCore("
                  + e.toString()
                  + "): Not implemented");
      break;
  }
  return reflexivityRule(e);
}


Theorem TheoryCore::rewriteN(const Expr& e, int n) {
  if(n <= 0) return reflexivityRule(e);
  if(theoryOf(e) != this) return reflexivityRule(e);
  if(n==1) return rewrite(e);
  vector<Theorem> thms;
  vector<unsigned> changed;
  for(int i=0; i<e.arity(); ++i) {
    Theorem thm = rewriteN(e[i], n-1);
    if(e[i] != thm.getRHS()) {
      thms.push_back(thm);
      changed.push_back(i);
    }
  }
  Theorem res;
  if(changed.size()>0) {
    res = substitutivityRule(e, changed, thms);
    res = transitivityRule(res, rewrite(res.getRHS()));
  } else {
    res = rewrite(e);
  }
  return res;
}


Theorem TheoryCore::rewrite(const Expr& e) {
  TRACE("core rewrite", "TheoryCore::rewrite(", e, ") {");
  Theorem thm;
  switch (e.getKind()) {
    case TRUE:
    case FALSE:
    case UCONST:
    case BOUND_VAR:
    case SKOLEM_VAR:
      thm = reflexivityRule(e);
      break; // do not rewrite
    case LETDECL:
      // Replace LETDECL and CONSTDEF with their definitions.  The
      // typechecker makes sure it's type-safe to do so.
      thm = d_rules->rewriteLetDecl(e);
      break;
    case CONSTDEF:
      thm = d_rules->rewriteConstDef(e);
      break;
    case EQ:
    case NOT:
      thm = rewriteLitCore(e);
      break;
    case IMPLIES: {
      thm = d_rules->rewriteImplies(e);
      const Expr& rhs = thm.getRHS();
      // rhs = OR(!e1, e2).  Rewrite !e1, then top-level OR().
      DebugAssert(rhs.isOr() && rhs.arity() == 2,
                  "TheoryCore::rewrite[IMPLIES]: rhs = "+rhs.toString());
      Theorem rw = rewriteCore(rhs[0]);
      if(rw.getLHS() != rw.getRHS()) {
        vector<unsigned> changed;
        vector<Theorem> thms;
        changed.push_back(0);
        thms.push_back(rw);
        rw = substitutivityRule(rhs, changed, thms);
        // Simplify to the find pointer of the result
        rw = transitivityRule(rw, find(rw.getRHS()));
        // Now rw = Theorem(rhs = rhs')
        rw = transitivityRule(rw, rewrite(rw.getRHS()));
      } else
        rw = rewrite(rhs);
      thm = transitivityRule(thm, rw);
      //       thm = transitivityRule(thm, simplify(thm.getRHS()));
      break;
    }
    case IFF: {
      thm = d_commonRules->rewriteIff(e);
      const Expr& e1 = thm.getRHS();
      // The only time we need to rewrite the result (e1) is when
      // e==(FALSE<=>e[1]) or (e[1]<=>FALSE), so e1==!e[1].
      if (e != e1 && e1.isNot())
        thm = transitivityRule(thm, rewriteCore(e1));
      else if(e1.isIff()) {
        TRACE_MSG("core rewrite",
                  "rewrite[Core]: checking for (a|b)<=>(a|c)...");
        // Check for OR or AND-factoring:
        // ((a|b)<=>(a|c))<=>(a|(b<=>c))
        // ((a&b)<=>(a&c))<=>(!a | (b<=>c))
        vector<Expr> lhs, rhs, av;
        int kind(NULL_KIND);
        Op op(NULL_KIND);
        if ((e1[0].isOr() || e1[0].isAnd()) && e1[0].arity() > 0) {
          kind = e1[0].getKind();
          op = e1[0].getOp();
        }
        if (kind==NULL_KIND && (e1[1].isOr() || e1[1].isAnd()) &&
            e1[1].arity() > 0) {
          kind = e1[1].getKind();
          op = e1[1].getOp();
        }
        if(kind==NULL_KIND) break; // Nothing to do
        // Keep matching for the and/or/iff distributivity rules
        if(e1[0].getKind()==kind) lhs=e1[0].getKids();
        else lhs.push_back(e1[0]);
        if(e1[1].getKind()==kind) rhs=e1[1].getKids();
        else rhs.push_back(e1[1]);
        TRACE("core rewrite", "lhs = ", Expr(RAW_LIST, lhs, d_em), "");
        TRACE("core rewrite", "rhs = ", Expr(RAW_LIST, rhs, d_em), "");
        intersect(lhs, rhs, av);
        TRACE("core rewrite", "intersect(lhs,rhs) = ",
              Expr(RAW_LIST, av, d_em), "");
        if(av.size()>0) {
          vector<Expr> bv, cv;
          difference(lhs, av, bv);
          difference(rhs, av, cv);
          TRACE("core rewrite", "bv = ", Expr(RAW_LIST, bv, d_em), "");
          TRACE("core rewrite", "cv = ", Expr(RAW_LIST, cv, d_em), "");
          Expr empty((kind==AND)? d_em->trueExpr() : d_em->falseExpr());
          Expr a((av.size()==1)? av[0] : Expr(op, av));
          Expr b((bv.size()==0)? empty : (bv.size()==1)? bv[0]
                 : Expr(op, bv));
          Expr c((cv.size()==0)? empty :(cv.size()==1)? cv[0]
                 : Expr(op, cv));
          TRACE("core rewrite", "a = ", a, "");
          TRACE("core rewrite", "b = ", b, "");
          TRACE("core rewrite", "c = ", c, "");
          // Convert e1 to the "normal" form (a|b)<=>(a|c)
          vector<Theorem> thms;
          vector<unsigned> changed;
          Theorem t = rewrite(Expr(op, a, b));
          if(t.getLHS() != t.getRHS()) {
            thms.push_back(symmetryRule(t));
            changed.push_back(0);
          }
          t = rewrite(Expr(op, a, c));
          if(t.getLHS() != t.getRHS()) {
            thms.push_back(symmetryRule(t));
            changed.push_back(1);
          }
          if(changed.size()>0) {
            t = substitutivityRule(e1, changed, thms);
            thm = transitivityRule(thm, t);
          }
          TRACE("core rewrite", "normalize => ", thm.getRHS(), "");
          thms.clear();
          changed.clear();
          if(kind==OR)
            t =  d_rules->iffOrDistrib(thm.getRHS());
          else
            t =  d_rules->iffAndDistrib(thm.getRHS());
          thm = transitivityRule(thm, t);
          TRACE("core rewrite", "iffOrDistrib => ", thm.getRHS(), "");
          // Rewrite !a when the kind is AND
          if(kind==AND) {
            t = simplifyRec(!a); // Push negation all the way down
          } else { // otherwise just rewrite 'a'
            t = rewriteCore(a);
          }
          if(t.getLHS() != t.getRHS()) {
            thms.push_back(t);
            changed.push_back(0);
          }
          // Rewrite (b<=>c) 2 levels deep (i.e. rewrite b and c)
          t = rewriteN(b.iffExpr(c), 2);
          if(t.getLHS() != t.getRHS()) {
            // If b is FALSE, we get NOT c (resp. NOT b when c is
            // FALSE).  In this case, we should re-simplify the result
            // to push the negation down.
            if(t.getRHS().isNot())
              t = transitivityRule(t, simplifyRec(t.getRHS()));
            thms.push_back(t);
            changed.push_back(1);
          }
          if(changed.size()>0) {
            t = substitutivityRule(thm.getRHS(), changed, thms);
            thm = transitivityRule(thm, t);
          }
          // Finally, rewrite the new top-level OR
          thm = transitivityRule(thm, rewrite(thm.getRHS()));
        }
      }
      break;
    }
    case ITE:
      if (e[0].isTrue())
        thm = d_rules->rewriteIteTrue(e);
      else if (e[0].isFalse())
        thm = d_rules->rewriteIteFalse(e);
      else if (e[1] == e[2])
        thm = d_rules->rewriteIteSame(e);
      else if (getFlags()["un-ite-ify"].getBool()) {
        // undo the rewriting of Boolean connectives to ITEs.
        // helpful for examples converted from SVC.
        // must rewrite again because we might create expressions
        // that can be further rewritten, and we must normalize.
        if (e[1].isFalse() && e[2].isTrue())
          thm = rewriteCore(d_rules->rewriteIteToNot(e));
        else if (e[1].isTrue())
          thm = rewriteCore(d_rules->rewriteIteToOr(e));
        else if (e[2].isFalse())
          thm = rewriteCore(d_rules->rewriteIteToAnd(e));
        else if (e[2].isTrue())
          thm = rewriteCore(d_rules->rewriteIteToImp(e));
        else if (e[1] == e[2].negate())
          thm = rewriteCore(d_rules->rewriteIteToIff(e));
        else thm = reflexivityRule(e);
      }
      else if(getFlags()["ite-cond-simp"].getBool()) {
        thm = d_rules->rewriteIteCond(e);
        if(e != thm.getRHS())
          thm = transitivityRule(thm, simplifyRec(thm.getRHS()));
      }
      else thm = reflexivityRule(e);    
      break;
    case AND: {
      thm = rewriteAnd(e);
      const Expr ee = thm.getRHS();
    
      //stop further processing if ee is not an AND expr
      if(!ee.isAnd()) break;

      TRACE("core rewrite", "rewrite[Core]: checking for (a|b) & (a|c) in ",
            ee, "");
      
      //store the common factor of the OR kids of ee in setIntersect
      std::vector<Expr> setIntersect;
      //discover the common factor from the OR kids of the AND
      if(ee[0].isOr())
        setIntersect = ee[0].getKids();
      else
        setIntersect.push_back(ee[0]);
      TRACE("core rewrite", "setIntersect = ",
            Expr(RAW_LIST, setIntersect, d_em), "");
      for(Expr::iterator i=ee.begin(),iend=ee.end();
          i!=iend && !setIntersect.empty();++i) {
        vector<Expr> Ai, result;
        //isolate the ith kid of the expr ee
        if(i->isOr())
          Ai = i->getKids();
        else
          Ai.push_back(*i);
        TRACE("core rewrite", "Ai = ", Expr(RAW_LIST, Ai, d_em), "");
        //compute the intersection of all Ai's of ee, iteratively
        intersect(setIntersect,Ai,result);
        setIntersect = result;
        TRACE("core rewrite", "setIntersect = ",
              Expr(RAW_LIST, setIntersect, d_em), "");
      }
      //if setIntersect is empty exit this processing and return 'thm' as is
      if(setIntersect.empty()) break;

      Expr A = orExpr(setIntersect);
      TRACE("core rewrite", "A = ", A, "");
      //compute the unique fractor of each AND kid of the OR    
      vector<Theorem> substThms;
      vector<unsigned> changed;
      int j(0);
      for(Expr::iterator i=ee.begin(),iend=ee.end();i!=iend; ++i, ++j) {
        vector<Expr> Ai, setDiff;
        //isolate the ith kid of the input expr ee
        if(i->isOr())
          Ai = i->getKids();
        else
          Ai.push_back(*i);
        TRACE("core rewrite", "Ai = ", Expr(RAW_LIST, Ai, d_em), "");
        //compute (Ai - setIntersect) and return value in 'setDiff'
        difference(Ai,setIntersect,setDiff);  
        TRACE("core rewrite", "setDiff = ",
              Expr(RAW_LIST, setDiff, d_em), "");
        Expr Bi = (setDiff.empty())? d_em->falseExpr()
          : (setDiff.size()==1)? setDiff[0] : orExpr(setDiff);
        //iKid is A | Bi
        Expr iKid = A.orExpr(Bi);
        TRACE("core rewrite", "Bi = ", Bi, "");
        TRACE("core rewrite", "iKid = ", iKid, "");
        // Ai <=> A | Bi
        Theorem thm0 = symmetryRule(rewriteOr(iKid));
        TRACE("core rewrite", "rewriteOr(iKid) = ", thm0.getLHS(), "");
        if(thm0.getLHS() != thm0.getRHS()) {
          DebugAssert(thm0.getLHS() == ee[j],
                      "ee["+int2string(j)+"]="+ee[j].toString()
                      +"\n thm0 = "+thm0.getExpr().toString());
          substThms.push_back(thm0);
          changed.push_back(j);
        }
      }
      Theorem t = substitutivityRule(ee, changed, substThms);
      thm = transitivityRule(thm, t);
      t = d_rules->andDistributivityRule(thm.getRHS());
      thm = transitivityRule(thm, t);
      DebugAssert(thm.getRHS().isOr() && thm.getRHS().arity()==2,
                  "TheoryCore::rewrite[AND over OR]: thm = "
                  +thm.getExpr().toString());
      t = rewrite(thm.getRHS()[0]);
      substThms.clear();
      changed.clear();
      if(t.getLHS() != t.getRHS()) {
        substThms.push_back(t);
        changed.push_back(0);
      }
      t = rewriteN(thm.getRHS()[1], 2);
      if(t.getLHS() != t.getRHS()) {
        substThms.push_back(t);
        changed.push_back(1);
      }
      if(changed.size()>0) {
        t = substitutivityRule(thm.getRHS(), changed, substThms);
        thm = transitivityRule(thm, t);
      }
      t = rewriteOr(thm.getRHS());
      thm = transitivityRule(thm, t);
      break;
    }
    case OR: {
      thm = rewriteOr(e);
      const Expr ee = thm.getRHS();
    
      //stop further processing if ee is not an OR expr
      if(!ee.isOr()) break;
      
      TRACE("core rewrite", "rewrite[Core]: checking for (a&b) | (a&c) in ",
            ee, "");
      
      //store the common factor of the AND kids of ee in setIntersect
      std::vector<Expr> setIntersect;
      //discover the common factor from the AND kids of the OR
      if(ee[0].isAnd())
        setIntersect = ee[0].getKids();
      else
        setIntersect.push_back(ee[0]);
      TRACE("core rewrite", "setIntersect = ",
            Expr(RAW_LIST, setIntersect, d_em), "");
      for(Expr::iterator i=ee.begin(),iend=ee.end();
          i!=iend && !setIntersect.empty();++i) {
        vector<Expr> Ai, result;
        //isolate the ith kid of the expr ee
        if(i->isAnd())
          Ai = i->getKids();
        else
          Ai.push_back(*i);
        TRACE("core rewrite", "Ai = ", Expr(RAW_LIST, Ai, d_em), "");
        //compute the intersection of all Ai's of ee, iteratively
        intersect(setIntersect,Ai,result);
        setIntersect = result;
        TRACE("core rewrite", "setIntersect = ",
              Expr(RAW_LIST, setIntersect, d_em), "");
      }
      //if setIntersect is empty exit this processing and return 'thm' as is
      if(setIntersect.empty()) break;

      Expr A = andExpr(setIntersect);
      TRACE("core rewrite", "A = ", A, "");
      //compute the unique fractor of each AND kid of the OR    
      vector<Theorem> substThms;
      vector<unsigned> changed;
      int j(0);
      for(Expr::iterator i=ee.begin(),iend=ee.end();i!=iend; ++i, ++j) {
        vector<Expr> Ai, setDiff;
        //isolate the ith kid of the input expr ee
        if(i->isAnd())
          Ai = i->getKids();
        else
          Ai.push_back(*i);
        TRACE("core rewrite", "Ai = ", Expr(RAW_LIST, Ai, d_em), "");
        //compute (Ai - setIntersect) and return value in 'setDiff'
        difference(Ai,setIntersect,setDiff);  
        TRACE("core rewrite", "setDiff = ",
              Expr(RAW_LIST, setDiff, d_em), "");
        Expr Bi = (setDiff.empty())? d_em->trueExpr()
          : (setDiff.size()==1)? setDiff[0] : andExpr(setDiff);
        //iKid is A & Bi
        Expr iKid = A.andExpr(Bi);
        TRACE("core rewrite", "Bi = ", Bi, "");
        TRACE("core rewrite", "iKid = ", iKid, "");
        // Ai <=> A & Bi
        Theorem thm0 = symmetryRule(rewriteAnd(iKid));
        //thm0 is Ai <=> A & Bi
        if(thm0.getLHS() != thm0.getRHS()) {
          substThms.push_back(thm0);
          changed.push_back(j);
        }
      }
      Theorem t = substitutivityRule(ee, changed, substThms);
      thm = transitivityRule(thm, t);
      t = d_rules->orDistributivityRule(thm.getRHS());
      thm = transitivityRule(thm, t);
      DebugAssert(thm.getRHS().isAnd() && thm.getRHS().arity()==2,
                  "TheoryCore::rewrite[OR over AND]: thm = "
                  +thm.getExpr().toString());
      t = rewrite(thm.getRHS()[0]);
      substThms.clear();
      changed.clear();
      if(t.getLHS() != t.getRHS()) {
        substThms.push_back(t);
        changed.push_back(0);
      }
      t = rewriteN(thm.getRHS()[1], 2);
      if(t.getLHS() != t.getRHS()) {
        substThms.push_back(t);
        changed.push_back(1);
      }
      if(changed.size()>0) {
        t = substitutivityRule(thm.getRHS(), changed, substThms);
        thm = transitivityRule(thm, t);
      }
      t = rewriteAnd(thm.getRHS());
      thm = transitivityRule(thm, t);
      break;
    }
      // Quantifiers
    case FORALL:
    case EXISTS:
      thm = d_commonRules->reflexivityRule(e);      
      break;
      // don't need to rewrite these
    case AND_R:
    case IFF_R:
    case ITE_R:
      thm = reflexivityRule(e);
      break;    
    default:
      DebugAssert(false,
                  "TheoryCore::rewrite("
                  + e.toString() + " : " + e.getType().toString()
                  + "): Not implemented");
      break;
  }

  DebugAssert(thm.getLHS() == e, "TheoryCore::rewrite("+e.toString()
              +") = "+thm.getExpr().toString());
  
  Expr rhs = thm.getRHS();
  // Advanced Boolean rewrites
  switch(rhs.getKind()) {
  case AND:
    if(getFlags()["simp-and"].getBool()) {
      Theorem tmp(reflexivityRule(rhs));
      for(int i=0, iend=rhs.arity(); i<iend; ++i) {
        tmp = transitivityRule
          (tmp, d_rules->rewriteAndSubterms(tmp.getRHS(), i));
      }
      if(tmp.getRHS() != rhs) { // Something changed: simplify recursively
        thm = transitivityRule(thm, tmp);
        thm = transitivityRule(thm, simplifyRec(thm.getRHS()));
        rhs = thm.getRHS();
      }
    }
    break;
  case OR:
    if(getFlags()["simp-or"].getBool()) {
      Theorem tmp(reflexivityRule(rhs));
      for(int i=0, iend=rhs.arity(); i<iend; ++i) {
        tmp = transitivityRule
          (tmp, d_rules->rewriteOrSubterms(tmp.getRHS(), i));
      }
      if(tmp.getRHS() != rhs) { // Something changed: simplify recursively
        thm = transitivityRule(thm, tmp);
        thm = transitivityRule(thm, simplifyRec(thm.getRHS()));
        rhs = thm.getRHS();
      }
    }
    break;
  default:
    break;
  }
  if (theoryOf(rhs) == this) {
    // Core rewrites are idempotent (FIXME: are they, still?)
    rhs.setRewriteNormal();
  }  
  TRACE("core rewrite", "TheoryCore::rewrite => ", thm.getExpr(), " }");
  return thm;
}


Theorem TheoryCore::simplifyOp(const Expr& e) {
  TRACE("core simplifyOp", "TheoryCore::simplifyOp(", e, ") {");
  int kind(e.getKind());
  Theorem res;

  if(getFlags()["ite-lift-unary"].getBool()
     && e.arity()==1 && e[0].isITE()) {
    res = d_rules->ifLiftUnaryRule(e);
    res = transitivityRule(res, simplifyOp(res.getRHS()));
    TRACE("core simplifyOp", "TheoryCore::simplifyOp[unary ite] => ",
          res.getExpr(), " }");
    return res;
  }
  
  switch(kind) {
  case AND:
  case OR: {
    // Stop when a child has this kind
    int endKind = (kind==AND)? FALSE : TRUE;
    int ar = e.arity();
    // Optimization: before simplifying anything recursively, check if
    // any kid is already TRUE or FALSE, and just return at that point
    int l(0);
    for(; l<ar && e[l].getKind() != endKind; ++l);
    if(l < ar) { // Found TRUE or FALSE: e simplifies to a const
      IF_DEBUG(debugger.counter("simplified AND/OR topdown")++);
      if(kind==AND)
        res = rewriteAnd(e);
      else
        res = rewriteOr(e);
      break; // Break out of switch()
    }
    vector<Theorem> newChildrenThm;
    vector<unsigned> changed;
    for(int k = 0; k < ar; ++k) {
      // Recursively simplify the kids
      Theorem thm = simplifyRec(e[k]);
      if (thm.getLHS() != thm.getRHS()) {
        if (thm.getRHS().getKind() == endKind) {
          newChildrenThm.clear();
          changed.clear();
          newChildrenThm.push_back(thm);
          changed.push_back(k);
          thm = substitutivityRule(e, changed, newChildrenThm);
          // Simplify to TRUE or FALSE
          if(kind==AND)
            thm = transitivityRule(thm, rewriteAnd(thm.getRHS()));
          else
            thm = transitivityRule(thm, rewriteOr(thm.getRHS()));
          IF_DEBUG(debugger.counter("simplified AND/OR: skipped kids")
                   += ar-k-1);
          TRACE("core simplifyOp",
                "TheoryCore::simplifyOp[TRUE/FALSE in OR/AND] => ",
                thm.getExpr(), " }");
          return thm;
        } else { // Child simplified to something else
          newChildrenThm.push_back(thm);
          changed.push_back(k);
        }
      }
    }
    if(changed.size() > 0)
      res = substitutivityRule(e, changed, newChildrenThm);
    break;
  }
  case ITE: {
    DebugAssert(e.arity()==3, "Bad ITE in TheoryCore::simplify(e="
                +e.toString()+")");
    // Optimization: check if the two branches are the same, so we
    // don't have to simplify the condition
    if(e[1]==e[2]) {
      res = d_rules->rewriteIteSame(e);
      res = transitivityRule(res, simplifyRec(res.getRHS()));
      IF_DEBUG(debugger.counter("simplified ITE(c,e,e)")++);
      break; // break out of switch()
    }
    // First, simplify the conditional
    vector<Theorem> newChildrenThm;
    vector<unsigned> changed;
    Theorem thm = simplifyRec(e[0]);
    if(thm.getLHS() != thm.getRHS()) {
      newChildrenThm.push_back(thm);
      changed.push_back(0);
    }
    const Expr& cond = thm.getRHS();
    for(int k=1; k<=2; ++k) {
      // If condition value is known, only the appropriate branch
      // needs to be simplified
      if((k==1 && cond.isFalse()) || (k==2 && cond.isTrue())) {
        IF_DEBUG(debugger.counter("simplified ITE: skiped one branch")++);
        continue;
      }
      thm = simplifyRec(e[k]);
      if(thm.getLHS() != thm.getRHS()) {
        newChildrenThm.push_back(thm);
        changed.push_back(k);
      }
    }
    if(changed.size() > 0)
      res = substitutivityRule(e, changed, newChildrenThm);
    break;
  }
  case NOT: { // Push negation down
    if(getFlags()["pushneg"].getBool()) {
      res = d_exprTrans->pushNegation1(e);
      if(res.getLHS() != res.getRHS())
        // Recurse; there may be shortcuts to take advantage of
        res = transitivityRule(res, simplifyOp(res.getRHS()));
      else {
        res = Theory::simplifyOp(e);
        // Try pushing negation once more
        Theorem thm = d_exprTrans->pushNegation1(res.getRHS());
        if(thm.getLHS() != thm.getRHS()) {
          thm = transitivityRule(thm, simplifyRec(thm.getRHS()));
          res = transitivityRule(res, thm);
        }
      }
    } else {
      res = Theory::simplifyOp(e);
    }
    break;
  }
  case IMPLIES:
    res = d_rules->rewriteImplies(e);
    res = transitivityRule(res, simplifyOp(res.getRHS()));
    break;
  default:
    res = Theory::simplifyOp(e);
  }
  if(res.isNull())
    res = reflexivityRule(e);
  TRACE("core simplifyOp", "TheoryCore::simplifyOp => ", res.getExpr(), " }");
  return res;
}


/*! Only Boolean constants (TRUE and FALSE) and variables of
  uninterpreted types should appear here (they come from records and
  tuples).  Just ignore them. */
void TheoryCore::setup(const Expr& e) { }


/*! We use the update method of theory core to track registered atomic
 * formulas.  Updates are recorded and then processed by calling processUpdates
 * once all equalities have been processed. */
void TheoryCore::update(const Theorem& e, const Expr& d)
{
  d_update_thms.push_back(e);
  d_update_data.push_back(d);
}

void TheoryCore::processUpdates()
{
  Theorem e;
  Expr d;
  DebugAssert(d_update_thms.size() == d_update_data.size(),
              "Expected same size");
  while (!d_update_thms.empty()) {
    e = d_update_thms.back();
    d_update_thms.pop_back();
    d = d_update_data.back();
    d_update_data.pop_back();

    DebugAssert(d.isAbsAtomicFormula(), "Expected atomic formula");
    Theorem thm = simplify(d);
    if (thm.getRHS().isTrue()) {
      if (d.isImpliedLiteral()) continue;
      d.setImpliedLiteral();
      d_impliedLiterals.push_back(d_commonRules->iffTrueElim(thm));
    }
    else if (thm.getRHS().isFalse()) {
      Expr notd = !d;
      if (notd.isImpliedLiteral()) continue;
      notd.setImpliedLiteral();
      d_impliedLiterals.push_back(d_commonRules->iffFalseElim(thm));
    }
    else {
      DebugAssert(e.isRewrite(), "Unexpected theorem in TheoryCore::update");
      if (e.getRHS().getType().isBool()) continue;
      find(e.getRHS()).getRHS().addToNotify(this, d);
      if (thm.getRHS().isAbsAtomicFormula()) thm.getRHS().addToNotify(this, d);
    }
  }
}


Expr TheoryCore::computeTypePred(const Type& t, const Expr& e)
{
  Expr tExpr = t.getExpr();
  switch(tExpr.getKind()) {
    case SUBTYPE: {
      Expr pred = tExpr[0];
      // pred may be a named function (CONSTDEF).  Strip CONSTDEFs off.
      while(pred.getKind()==CONSTDEF) pred = pred[1];
      const Type& argTp = pred.lookupType()[0];
      return Expr(pred.mkOp(), e).andExpr(getTypePred(argTp, e));
    }
    case APPLY: {
      Theory* i = theoryOf(e);
      if (i != this) return i->computeTypePred(t, e);
      // fall through
    }
    default:
      return e.getEM()->trueExpr();
  }
}


void TheoryCore::checkType(const Expr& e)
{
  switch (e.getKind()) {
    case BOOLEAN:
      if (e.arity() > 0) {
        throw Exception("Ill-formed Boolean type:\n\n"+e.toString());
      }
      break;
    case SUBTYPE: {
        if (e.arity() != 1)
          throw Exception("Ill-formed SUBTYPE expression:\n\n"+e.toString());
        Type t = e[0].getType();
        if (!t.isFunction())
          throw Exception
            ("Non-function argument to SUBTYPE:\n\n"
             +e.toString());
        if (!t[1].isBool())
          throw Exception
            ("Non-predicate argument to SUBTYPE:\n\n"
             +e.toString());
      }
      break;
    default:
      DebugAssert(false, "Unexpected kind in TheoryCore::checkType"
                  +getEM()->getKindName(e.getKind()));
  }
}


void TheoryCore::computeType(const Expr& e)
{
  switch (e.getKind()) {
    case ITE: {
      Type t1(getBaseType(e[1])), t2(getBaseType(e[2]));
      if (e[0].getType() != boolType())
        throw TypecheckException
          ("The conditional in IF-THEN-ELSE must be BOOLEAN, but is:\n\n"
           +e[0].getType().toString()
           +"\n\nIn the expression:\n\n  "
           +e.toString());
      if(t1 != t2) {
        throw TypecheckException
          ("The types of the IF-THEN-ELSE branches do not match.\n"
           "THEN branch has the type:\n\n  "
           +e[1].getType().toString()
           +"\n\nELSE branch has the type:\n\n  "
           +e[2].getType().toString()
           +"\n\nIn expression:\n\n  "+e.toString());
      }
      Type res(e[1].getType());
      // If the precise types match in both branches, use it as the
      // result type.
      if(res == e[2].getType()) {
        IF_DEBUG(if(res != t1) // Trace ITEs with strict subtypes
                 TRACE("ite", "ITE: setting type "+res.toString()
                       +" to:\n\n  ", e, ""));
        e.setType(res);
      }
      else
        // Note: setting the base type, since e[1] and e[2] have
        // different exact types, and the base type is a conservative
        // approximation we can easily compute.
        e.setType(t1);
    }
      break;
    case EQ: {
      Type t0(getBaseType(e[0])), t1(getBaseType(e[1]));
      if (t0.isBool() || t1.isBool()) {
        throw TypecheckException
          ("Cannot use EQ ('=') for BOOLEAN type; use IFF ('<=>') instead.\n"
           "Error in the following expression:\n"+e.toString());
      }
      if (t0 != t1) {
        throw TypecheckException
          ("Type mismatch in equality:\n\n LHS type:\n"+t0.toString()
           +"\n\n RHS type: \n"+t1.toString()
           +"\n\n in expression: \n"+e.toString());
      }
      e.setType(boolType());
    }
      break;
    case NOT:
    case AND:
    case OR:
    case XOR:
    case IFF:
    case IMPLIES:

    case AND_R:
    case IFF_R:
    case ITE_R:
    
      for (int k = 0; k < e.arity(); ++k) {
        if (e[k].getType() != boolType()) {
          throw TypecheckException(e.toString());
        }
      }
      e.setType(boolType());
      break;
    case CONSTDEF: 
    case LETDECL: {
      Type varTp(getBaseType(e[0]));
      Type valTp(getBaseType(e[1]));
      if(valTp != varTp) {
        throw TypecheckException("Type mismatch for "+e[0].toString()+":"
                                 +"\n  declared: "
                                 + varTp.toString()
                                 +"\n  derived: "+ valTp.toString());
      }
      e.setType(e[0].getType());
    }
      break;
    default:
      DebugAssert(false,"TheoryCore::computeType(" + e.toString()
                  + "):\nNot implemented");
      break;
  }
}


Type
TheoryCore::computeBaseType(const Type& tp) {
  const Expr& e = tp.getExpr();
  Type res;
  switch(e.getKind()) {
  case SUBTYPE: {
    DebugAssert(e.arity() == 1, "Expr::computeBaseType(): "+e.toString());
    Type lambdaTp = e[0].getType();
    Type lambdaBaseTp = getBaseType(lambdaTp);
    DebugAssert(lambdaBaseTp.isFunction(), 
                "Expr::computeBaseType(): lambdaBaseTp = "
                +lambdaBaseTp.toString()+" in e = "+e.toString());
    res = lambdaBaseTp[0];
    break;
  }
  case BOOLEAN:
    res = tp; break;
  case TYPEDEF: // Compute the base type of the definition
    res = getBaseType(Type(e[1]));
    break;
  default:
    DebugAssert(false, "TheoryCore::computeBaseType("+tp.toString()+")");
    res = tp;
  }
  return res;
}


Expr 
TheoryCore::computeTCC(const Expr& e) {
  Expr res;
  switch (e.getKind()) {
  case NOT:
    res = getTCC(e[0]);
    break;
  case AND: {
    // ( (tcc(e1) & !e1) \/ ... \/ (tcc(en) & !en) \/ (tcc(e1)&...&tcc(en))
    vector<Expr> tccs;
    for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
      tccs.push_back(getTCC(*i));
    vector<Expr> pairs;
    pairs.push_back(rewriteAnd(andExpr(tccs)).getRHS());
    for(size_t i=0, iend=tccs.size(); i<iend; ++i)
      pairs.push_back(rewriteAnd(tccs[i].andExpr(e[i].negate())).getRHS());
    res = rewriteOr(orExpr(pairs)).getRHS();
    break;
  }
  case OR: {
    // ( (tcc(e1) & e1) \/ ... \/ (tcc(en) & en) \/ (tcc(e1)&...&tcc(en))
    vector<Expr> tccs;
    for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
      tccs.push_back(getTCC(*i));
    vector<Expr> pairs;
    pairs.push_back(rewriteAnd(andExpr(tccs)).getRHS());
    for(size_t i=0, iend=tccs.size(); i<iend; ++i)
      pairs.push_back(rewriteAnd(tccs[i].andExpr(e[i])).getRHS());
    res = rewriteOr(orExpr(pairs)).getRHS();
    break;
  }
  case ITE: {
    Expr tcc1(getTCC(e[1])), tcc2(getTCC(e[2]));
    // Optimize: if TCCs on both branches are the same, skip the ITE
    Expr tccITE((tcc1 == tcc2)? tcc1 : e[0].iteExpr(tcc1, tcc2));
    res = rewriteAnd(getTCC(e[0]).andExpr(tccITE)).getRHS();
    break;
  }
  case IMPLIES:
    res = getTCC(e[0].negate().orExpr(e[1]));
    break;
  case APPLY: {
    Theory* i = theoryOf(e);
    if (i != this) return i->computeTCC(e);
    // fall through
  }
  default: // All the other operators are strict
    res = Theory::computeTCC(e);
    break;
  }
  return res;
}

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

ExprStream&
TheoryCore::print(ExprStream& os, const Expr& e)   
{
  switch(os.lang()) {
  case PRESENTATION_LANG:
    switch(e.getKind()) {
    case TRUE:
    case FALSE:
    case UCONST:
    case BOOLEAN:
    case STRING_EXPR:
      e.print(os); break;
    case TYPE:
      if(e.arity() == 0) os << "TYPE";
      else if(e.arity() == 1)
        os << e[0] << ": TYPE;";
      else if(e.arity() == 2)
        os << e[0] << ":" << push << " TYPE = " << e[1] << push << ";";
      else e.printAST(os);
      break;
    case ID:
      if(e.arity() == 1 && e[0].isString()) os << e[0].getString();
      else e.printAST(os);
      break;
    case CONST:
      if(e.arity() == 2) {
        if(e[0].getKind() == RAW_LIST) {
          bool first(true);
          for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
            if(first) first = false;
            else os << push << "," << pop << space;
            os << (*i);
          }
        }
        else
          os << e[0];
        os << ":" << push << space << e[1] << push << ";";
      } else if(e.arity() == 3)
        os << e[0] << ":" << push << space << e[1]
           << space << "=" << space << push << e[2] << push << ";";
      else
        e.printAST(os);
      break;
    case SUBTYPE:
      os << "SUBTYPE(" << push << e[0] << push << ")";
      break;
    case TYPEDEF: {
      // This is used when dumping declarations to file.  Print just
      // the name of the type, unless it's a messed-up expression.
      if(e.arity() != 2) e.printAST(os);
      else if(e[0].isString()) os << e[0].getString();
      else e[0].print(os);
      break;
    }
    case EQ:
      // When a separator starts with a space (like " = "), add the
      // leading space with 'space' modifier.  If this separator goes
      // to the next line, the leading spaces must be eaten up to get
      // the indentation right; 'space' will tell the indentation
      // engine that it is a space that can be eaten.  A space in a
      // string (like " ") will never be eaten.
      os << "(" << push << e[0] << space << "= " << e[1] << push << ")";
      break;
    case NOT: os << "NOT " << e[0]; break;
    case AND: {
      int i=0, iend=e.arity();
      os << "(" << push;
      if(i!=iend) { os << e[i]; ++i; }
      for(; i!=iend; ++i) os << space << "AND " << e[i];
      os << push << ")";
    }
      break;
    case OR: {
      int i=0, iend=e.arity();
      os << "(" << push;
      if(i!=iend) { os << e[i]; ++i; }
      for(; i!=iend; ++i) os << space << "OR " << e[i];
      os << push << ")";
    }
      break;
    case ITE:
      os << push << "IF " << push << e[0] << popSave
         << space << "THEN " << pushRestore << e[1] << popSave
         << space << "ELSE " << pushRestore << e[2] << pop
         << space << "ENDIF";
      break;
    case IFF:
      if(e.arity() == 2)
        os << "(" << push << e[0] << space << "<=> " << e[1] << push << ")";
      else
        e.printAST(os);
      break;
    case IMPLIES:
      os << "(" << push << e[0] << space << "=> " << e[1] << push << ")";
      break;
      // Commands
    case ASSERT:
      os << "ASSERT " << push << e[0] << push << ";";
      break;
    case TRANSFORM:
      os << "TRANSFORM " << push << e[0] << push << ";";
      break;
    case QUERY:
      os << "QUERY " << push << e[0] << push << ";";
      break;
    case WHERE:
      os << "WHERE;";
      break;
    case ASSERTIONS:
      os << "ASSERTIONS;";
      break;
    case ASSUMPTIONS:
      os << "ASSUMPTIONS;";
      break;
    case COUNTEREXAMPLE:
      os << "COUNTEREXAMPLE;";
      break;
    case COUNTERMODEL:
      os << "COUNTERMODEL;";
      break;
    case PUSH:
      if(e.arity()==0)
        os << "PUSH;";
      else
        os << "PUSH" << space << e[0] << push << ";";
      break;
    case POP:
      if(e.arity()==0)
        os << "POP;";
      else
        os << "POP" << space << e[0] << push << ";";
      break;
    case POPTO:
      os << "POPTO" << space << e[0] << push << ";"; break;
    case PUSH_SCOPE:
      if(e.arity()==0)
        os << "PUSH_SCOPE;";
      else
        os << "PUSH_SCOPE" << space << e[0] << push << ";";
      break;
    case POP_SCOPE:
      if(e.arity()==0)
        os << "POP_SCOPE;";
      else
        os << "POP_SCOPE" << space << e[0] << push << ";";
      break;
    case POPTO_SCOPE:
      os << "POPTO_SCOPE" << space << e[0] << push << ";"; break;
    case CONSTDEF:
    case LETDECL:
      if(e.arity() == 2) os << e[1];
      else e.printAST(os);
      break;
    case LET: {
      // (LET (LETDECLS (LETDECL var [ type ] val) .... ) body)
      bool first(true);
      os << "(" << push << "LET" << space << push;
      for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
        if(!first) os << push << "," << pop << endl;
        else first = false;
        if(i->arity() == 3) {
          os << (*i)[0] << ":" << space << push << (*i)[1]
             << space << "= " << push << nodag << (*i)[2] << pop << pop;
        } else {
          os << (*i)[0];
          Type tp((*i)[0].lookupType());
          if(!tp.isNull()) os << ":" << space << push << tp.getExpr();
          else os << push;
          os << space << "= " << push << nodag << (*i)[1] << pop << pop;
        }
      }
      os << pop << endl << "IN" << space << push << e[1] << push << ")";
      break;
    }
    case BOUND_VAR:
      os << e.getName()+"_"+e.getUid();
      break;
    case SKOLEM_VAR:
      os << "SKOLEM_" + int2string(e.getIndex());
      break;
    case PF_APPLY: // FIXME: this will eventually go to the "symsim" theory
      DebugAssert(e.arity() > 0, "TheoryCore::print(): "
                  "Proof rule application must have at "
                  "least one argument (rule name):\n "+e.toString());
      os << e[0];
      if(e.arity() > 1) { // Print the arguments
        os << push << "(" << push;
        bool first(true);
        for(int i=1; i<e.arity(); i++) {
          if(first) first=false;
          else os << push << "," << pop << space;
          os << e[i];
        }
        os << push << ")";
      }
      break;
    case RAW_LIST: {
      os << "[" << push;
      bool firstTime(true);
      for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
        if(firstTime) firstTime = false;
        else os << push << "," << pop << space;
        os << *i;
      }
      os << push << "]";
      break;
    }
    case PF_HOLE: // FIXME: implement this (now fall through to default)
    default:
      // Print the top node in the default LISP format, continue with
      // pretty-printing for children.
      e.printAST(os);
    }
    break; // end of case PRESENTATION_LANG
  case SMTLIB_LANG:
    switch(e.getKind()) {
    case TRUE: os << "true"; break;
    case FALSE: os << "false"; break;
    case UCONST: e.print(os); break;
    case BOOLEAN: e.printAST(os); break;
    case STRING_EXPR: e.print(os); break;
    case TYPE:
      if (e.arity() == 1) {
        os << "  :extrasorts (";
        for (int i=0; i < e[0].arity(); ++i) {
          if (i != 0) os << push << space;
          os << push << e[0][i];
        }
        os << push << ")";
      }
      else if (e.arity() == 2) {
        break;
      }
      else {
        throw SmtlibException("TheoryCore::print: SMTLIB: Unexpected TYPE expression");
      }
      break;
    case ID: // FIXME: when lisp becomes case-insensitive, fix printing of IDs
      if(e.arity() == 1 && e[0].isString()) os << e[0].getString();
      else e.printAST(os);
      break;
    case CONST:
      if(e.arity() == 2) {
        if (e[1].getKind() == BOOLEAN) {
          os << "  :extrapreds ((" << push << e[0]
             << push << "))";
        }
        else if (e[1].getKind() == ARROW && e[1][e[1].arity()-1].getKind() == BOOLEAN) {
          os << "  :extrapreds ((" << push << e[0]
             << space << e[1] << push << "))";
        }
        else {
          os << "  :extrafuns ((" << push << e[0]
             << space << e[1] << push << "))";
        }
      }
      else if (e.arity() == 0) e.printAST(os);
      else {
        throw SmtlibException("TheoryCore::print: SMTLIB: CONST not implemented");
      }
      break;
    case SUBTYPE:
      throw SmtlibException("TheoryCore::print: SMTLIB: SUBTYPE not implemented");
      break;
    case TYPEDEF: {
      throw SmtlibException("TheoryCore::print: SMTLIB: TYPEDEF not implemented");
      break;
    }
    case EQ:
      os << "(" << push << "=" << space << e[0]
         << space << e[1] << push << ")";
      break;
    case NOT:
      os << "(" << push << "not" << space << e[0] << push << ")";
      break;
    case AND: {
      int i=0, iend=e.arity();
      os << "(" << push << "and";
      for(; i!=iend; ++i) os << space << e[i];
      os << push << ")";
    }
      break;
    case OR: {
      int i=0, iend=e.arity();
      os << "(" << push << "or";
      for(; i!=iend; ++i) os << space << e[i] << space;
      os << push << ")";
      break;
    }
    case XOR: {
      int i=0, iend=e.arity();
      os << "(" << push << "xor";
      for(; i!=iend; ++i) os << space << e[i] << space;
      os << push << ")";
      break;
    }
    case ITE:
      os << "(" << push;
      if (e.getType().isBool()) os << "if_then_else";
      else os << "ite";
      os << space << e[0]
         << space << e[1] << space << e[2] << push << ")";
      break;
    case IFF:
      os << "(" << push << "iff" << space
         << e[0] << space << e[1] << push << ")";
      break;
    case IMPLIES:
      os << "(" << push << "implies" << space
         << e[0] << space << e[1] << push << ")";
      break;
      // Commands
    case ASSERT:
      //      throw SmtlibException("TheoryCore::print: SMTLIB: ASSERT not implemented");
      os << "(" << push << "ASSERT" << space << e[0] << push << ")";
      break;
    case TRANSFORM:
      throw SmtlibException("TheoryCore::print: SMTLIB: TRANSFORM not implemented");
      os << "(" << push << "TRANSFORM" << space << e[0] << push << ")";
      break;
    case QUERY:
      throw SmtlibException("TheoryCore::print: SMTLIB: QUERY not implemented");
      os << "(" << push << "QUERY" << space << e[0] << push << ")";
      break;
    case CONSTDEF:
    case LETDECL:
      //      throw SmtlibException("TheoryCore::print: SMTLIB: CONSTDEF, LETDECL not implemented");
      if(e.arity() == 2) os << e[1];
      else e.printAST(os);
      break;
    case LET: {
      // (LET ((var [ type ] val) .... ) body)
      for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
        os << "(" << push;
        Type tp(i->arity() == 3 ? (*i)[2].getType() : (*i)[1].getType());
        DebugAssert(!tp.isNull(), "Unexpected Null type");
        if (tp.getExpr().getKind() == BOOLEAN) {
          os << "flet" << space << "(" << push;
        }
        else {
          os << "let" << space << "(" << push;
        }
        if(i->arity() == 3) {
          os << (*i)[0] << space << nodag << (*i)[2];
        } else {
          os << (*i)[0] << space << nodag << (*i)[1];
        }
        os << push << ")" << pop << pop << space;
      }
      os << e[1] << push;
      for (int j = 0; j < e[0].arity(); ++j)
        os << ")";
      break;
    }
    case BOUND_VAR:
      os << e.getName()+"_"+e.getUid();
      break;
    case SKOLEM_VAR:
      os << "SKOLEM_" + int2string(e.getIndex());
      break;
    case PF_APPLY: {// FIXME: this will eventually go to the "symsim" theory
      throw SmtlibException("TheoryCore::print: SMTLIB: PF_APPLY not implemented");
      break;
    }
    case RAW_LIST: {
      os << "(" << push;
      bool firstTime(true);
      for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
        if(firstTime) firstTime = false;
        else os << space;
        os << *i;
      }
      os << push << ")";
      break;
    }
    case PUSH:
    case POP:
    case POPTO:
    case PUSH_SCOPE:
    case POP_SCOPE:
    case POPTO_SCOPE:
      throw SmtlibException("TheoryCore::print: SMTLIB: Stack operations not implemented");
      break;
    case PF_HOLE: // FIXME: implement this (now fall through to default)
    default:
      throw SmtlibException("TheoryCore::print: SMTLIB_LANG: Unexpected expression: "
                            +getEM()->getKindName(e.getKind()));
    }
    break; // end of case SMTLIB_LANG
  case LISP_LANG:
    switch(e.getKind()) {
    case TRUE:
    case FALSE:
    case UCONST:
      e.print(os); break;
    case TYPE:
      if(e.arity() == 0) os << "TYPE";
      else if(e.arity() == 1)
        os << "(" << push << "TYPE" << space << e[0] << push << ")";
      else if(e.arity() == 2)
        os << "(" << push << "TYPE" << space << e[0]
           << space << e[1] << push << ")";
      else e.printAST(os);
      break;
    case ID: // FIXME: when lisp becomes case-insensitive, fix printing of IDs
      if(e.arity() == 1 && e[0].isString()) os << e[0].getString();
      else e.printAST(os);
      break;
    case CONST:
      if(e.arity() == 2)
        os << "(" << push << "CONST" << space << e[0]
           << space << e[1] << push << ")";
      else
        e.printAST(os);
      break;
    case SUBTYPE:
      os << "SUBTYPE(" << push << e[0] << push << ")";
      break;
    case TYPEDEF: {
      // This is used when dumping declarations to file.  Print just
      // the name of the type, unless it's a messed-up expression.
      if(e.arity() != 2) e.printAST(os);
      else if(e[0].isString()) os << e[0].getString();
      else e[0].print(os);
      break;
    }
    case EQ:
      // When a separator starts with a space (like " = "), add the
      // leading space with 'space' modifier.  If this separator goes
      // to the next line, the leading spaces must be eaten up to get
      // the indentation right; 'space' will tell the indentation
      // engine that it is a space that can be eaten.  A space in a
      // string (like " ") will never be eaten.
      os << "(" << push << "=" << space << e[0]
         << space << e[1] << push << ")";
      break;
    case NOT:
      os << "(" << push << "NOT" << space << e[0] << push << ")";
      break;
    case AND: {
      int i=0, iend=e.arity();
      os << "(" << push << "AND";
      for(; i!=iend; ++i) os << space << e[i];
      os << push << ")";
    }
      break;
    case OR: {
      int i=0, iend=e.arity();
      os << "(" << push << "OR";
      for(; i!=iend; ++i) os << space << e[i] << space;
      os << push << ")";
    }
      break;
    case ITE:
      os << "(" << push << "IF" << space << e[0]
         << space << e[1] << space << e[2] << push << ")";
      break;
    case IFF:
      os << "(" << push << "<=>" << space
         << e[0] << space << e[1] << push << ")";
      break;
    case IMPLIES:
      os << "(" << push << "=>" << space
         << e[0] << space << e[1] << push << ")";
      break;
      // Commands
    case ASSERT:
      os << "(" << push << "ASSERT" << space << e[0] << push << ")";
      break;
    case TRANSFORM:
      os << "(" << push << "TRANSFORM" << space << e[0] << push << ")";
      break;
    case QUERY:
      os << "(" << push << "QUERY" << space << e[0] << push << ")";
      break;
    case PUSH:
      os << "(PUSH)"; break;
    case POP:
      os << "(POP)"; break;
    case POPTO:
      os << "(" << push << "POPTO" << space << e[0] << push << ")"; break;
    case CONSTDEF:
    case LETDECL:
      if(e.arity() == 2) os << e[1];
      else if(e.arity()==3) // It's a declaration of a named Expr
        os << e[0] << push << ":" << space << push << e[1] << push << " ="
           << pop << pop << space << e[2];
      else e.printAST(os);
      break;
    case LET: {
      // (LET ((var [ type ] val) .... ) body)
      bool first(true);
      os << "(" << push << "LET" << space << "(" << push;
      for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
        if(!first) os << space;
        else first = false;
        os << "(" << push;
        if(i->arity() == 3) {
          os << (*i)[0] << space << (*i)[1]
             << space << nodag << (*i)[2];
        } else {
          os << (*i)[0];
          Type tp((*i)[0].lookupType());
          if(!tp.isNull()) os << space << tp.getExpr();
          os << space << nodag << (*i)[1];
        }
        os << push << ")" << pop << pop;
      }
      os << push << ")" << pop << pop << space << e[1] << push << ")";
      break;
    }
    case BOUND_VAR:
      os << e.getName()+"_"+e.getUid();
      break;
    case SKOLEM_VAR:
      os << "SKOLEM_" + int2string(e.getIndex());
      break;
    case PF_APPLY: {// FIXME: this will eventually go to the "symsim" theory
      DebugAssert(e.arity() > 0, "TheoryCore::print(): "
                  "Proof rule application must have at "
                  "least one argument (rule name):\n "+e.toString());
      os << push << "(" << push;
      bool first(true);
      for(int i=0; i<e.arity(); i++) {
        if(first) first=false;
        else os << space;
        os << e[i];
      }
      os << push << ")";
      break;
    }
    case RAW_LIST: {
      os << "(" << push;
      bool firstTime(true);
      for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
        if(firstTime) firstTime = false;
        else os << space;
        os << *i;
      }
      os << push << ")";
      break;
    }
    case PF_HOLE: // FIXME: implement this (now fall through to default)
    default:
      // Print the top node in the default LISP format, continue with
      // pretty-printing for children.
      e.printAST(os);
    }
    break; // end of case LISP_LANGUAGE
  default:
    // Print the top node in the default LISP format, continue with
    // pretty-printing for children.
    e.printAST(os);
  }
  return os;
}

///////////////////////////////////////////////////////////////////////////////
//parseExpr:
//translates intermediate representation to internal language for use in VCCmd
///////////////////////////////////////////////////////////////////////////////
Expr TheoryCore::parseExpr(const Expr& e) {
  TRACE("parseExpr", "parseExpr(", e, ") {");
  // Remember the current size of the bound variable stack
  size_t boundVarSize = d_boundVarStack.size();
  TRACE("parseExpr", "#bound vars = ", d_boundVarStack.size(), "");

  // Compute the kind to determine what to do with the expression
  int kind = NULL_KIND;

  switch(e.getKind()) {
  case ID: {
    TRACE("parser verbose", "resolving variable/operator(", e[0], ")");
    const Expr c1 = e[0];
    kind = getEM()->getKind(c1.getString());
    if(kind == NULL_KIND) { // It's an identifier; try to resolve it
      Expr res = resolveID(e[0].getString());
      if(res.isNull())
        throw ParserException("cannot resolve an identifier: "
                              +e[0].toString());
      else {
        TRACE("parseExpr", "#bound vars = ", d_boundVarStack.size(), "");
        TRACE("parseExpr", "parseExpr => ", res, " }");
        DebugAssert(!e.isApply(), "Unexpected apply function");
        return res;
      }
    }
    // Otherwise exit the switch and use DP-specific parsing
    break;
  }
  case RAW_LIST: {
    TRACE("parser verbose", "constructing Expr from list(", e, ")");
    if(e.arity() == 0)
      throw ParserException("Empty list is not an expression!");
    const Expr& op = e[0];
    // First, resolve the operator
    switch(op.getKind()) {
    case ID: { // The operator in the list is ID: is it keyword or variable?
      kind = getEM()->getKind(op[0].getString());
      if(kind == NULL_KIND) {
        // It's a named function application.  Resolve the ID.
        Expr res = resolveID(op[0].getString());
        if(res.isNull())
          throw ParserException("cannot resolve an identifier: "
                                +op[0].toString());
        if(e.arity() < 2)
          throw ParserException("Bad function application: "+e.toString());
        Expr::iterator i=e.begin(), iend=e.end();
        ++i;
        vector<Expr> args;
        for(; i!=iend; ++i) args.push_back(parseExpr(*i));
        return Expr(res.mkOp(), args);
      }
      // Proceed to DP-specific parsing
      break;
    }
    case RAW_LIST: 
      // This can only be a lambda expression application.
      kind = LAMBDA;
      break;
    default:
      throw ParserException("Bad operator in "+e.toString());
    }
    break; // Exit the top-level switch, proceed to DP-specific parsing
  }
  default: // Can only be a string or a number.
    TRACE("parseExpr", "parseExpr => ", e, " }");
    return e;
  }

  // DP-specific parsing
  if(hasTheory(kind)) {
    TRACE("parseExpr", "parseExprOp["+theoryOf(kind)->getName()+"](",
          e, ") {");
    Expr res = theoryOf(kind)->parseExprOp(e);
    TRACE("parseExpr",
          "parseExprOp["+theoryOf(kind)->getName()+"] => ", res, " }");
    TRACE("parseExpr", "#bound vars = ", d_boundVarStack.size(), "");
    // Restore the bound variable stack
    while(d_boundVarStack.size() > boundVarSize) {
      TRACE("parseExpr", "Pop bound var "+d_boundVarStack.back().first+": ",
            d_boundVarStack.back().second, "");
      d_boundVarStack.pop_back();
    }
    TRACE("parseExpr", "#bound vars = ", d_boundVarStack.size(), "");
    TRACE("parseExpr", "parseExpr => ", res, " }");
    return res;
  }
  else {
    TRACE("parseExpr", "parseExpr => ", e, " }");
    return e;
  }
}

//! An auxiliary recursive function to process COND expressions into ITE
Expr TheoryCore::processCond(const Expr& e, int i) {
  DebugAssert(i < e.arity()-1, "e = "+e.toString()+", i = "+int2string(i));
  if(i == e.arity()-2) {
    if(e[i].getKind() == RAW_LIST && e[i].arity() == 2
       && e[i+1].getKind() == RAW_LIST  && e[i+1].arity() == 2
       && e[i+1][0].getKind() == ID && e[i+1][0][0].getString() == "ELSE") {
      Expr c(parseExpr(e[i][0]));
      Expr e1(parseExpr(e[i][1]));
      Expr e2(parseExpr(e[i+1][1]));
      return c.iteExpr(e1,e2);
    }
  } else {
    if(e[i].getKind() == RAW_LIST && e[i].arity() == 2
       && e[i+1].getKind() == RAW_LIST  && e[i+1].arity() == 2) {
      Expr c(parseExpr(e[i][0]));
      Expr e1(parseExpr(e[i][1]));
      Expr e2(processCond(e, i+1));
      return c.iteExpr(e1,e2);
    }
  }
  throw ParserException("Parse Error: bad COND expression: "+e.toString());
}

///////////////////////////////////////////////////////////////////////////////
//parseExprOp:
//Recursive call of parseExpr defined in theory_ libaries based on kind of expr 
//being built
///////////////////////////////////////////////////////////////////////////////
Expr
TheoryCore::parseExprOp(const Expr& e) {
  TRACE("parser", "TheoryCore::parseExprOp(", e, ")");
  // 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 TRUE:
    case FALSE:
    case TYPE:
    case BOOLEAN: 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 work
  default:
    return e;
  }
  DebugAssert(e.getKind()==RAW_LIST && e.arity() > 0 && e[0].getKind()==ID,
              "TheoryCore::parseExprOp:\n e = "+e.toString());
  /* The first element of the list (e[0] is an ID of the operator. 
     ID string values are the dirst element of the expression */              
  const Expr& c1 = e[0][0];
  int kind = getEM()->getKind(c1.getString());
  TRACE("parser verbose", "building kind(", kind, ")");
  switch(kind) {
  case VARDECLS: 
  case LETDECLS:
  case HELP: 
  case DUMP_PROOF:
  case DUMP_ASSUMPTIONS:
  case DUMP_SIG:
  case DUMP_TCC:
  case DUMP_TCC_ASSUMPTIONS:
  case DUMP_TCC_PROOF:
  case DUMP_CLOSURE:
  case DUMP_CLOSURE_PROOF:
  case WHERE:
  case ASSERTIONS:
  case ASSUMPTIONS:
  case COUNTEREXAMPLE:
  case COUNTERMODEL:
  case ASSERT:
  case PRINT:
  case QUERY:
  case CHECKSAT:
  case CONTINUE:
  case RESTART:
  case TRACE:
  case ECHO:
  case UNTRACE:
  case VARLIST:
  case SUBTYPE: 
  case FORGET: 
  case GET_TYPE: 
  case IFF: 
  case IMPLIES: 
  case TYPEDEF: 
  case OPTION:
  case AND:
  case OR:
  case XOR:
  case NOT:
  case EQ: 
  case CALL: 
  case TRANSFORM: 
  case CHECK_TYPE: 
  case VARDECL: 
  case GET_CHILD: 
  case SUBSTITUTE: 
  case SEQ:
  case CONSTDEF: 
  case DBG: 
  case PUSH:
  case POP:
  case POPTO:
  case PUSH_SCOPE:
  case POP_SCOPE:
  case POPTO_SCOPE:
  case LETDECL:
  case ELSE:
  case CONTEXT:{
    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 NEQ:
    if(e.arity()==3)
      return !(parseExpr(e[1]).eqExpr(parseExpr(e[2])));
    else
      throw ParserException("Disequality requires exactly two arguments: "
                            +e.toString());
    break;
  case CONST: {
    if(e.arity()==3) {
      vector<Expr> names;
      const Expr& vars = e[1];
      if(vars.getKind() == RAW_LIST) {
        for(Expr::iterator i=vars.begin(), iend=vars.end(); i!=iend; ++i)
          names.push_back(*i);
      } else if(vars.getKind() == ID)
        names.push_back(vars);
      return Expr(CONST, Expr(RAW_LIST, names, getEM()),
                  parseExpr(e[2]));
    }
    else if(e.arity() == 4 && e[1].getKind() == ID)
      return Expr(CONSTDEF, e[1],
                  parseExpr(e[2]), parseExpr(e[3]));
    throw ParserException("Bad CONST declaration: "+e.toString());
    break;
  }
  case TYPE: {
    if(e.arity()==2) {
      const Expr& types = e[1];
      if(types.getKind() == RAW_LIST) {
        vector<Expr> names;
        for(Expr::iterator i=types.begin(), iend=types.end(); i!=iend; ++i)
          names.push_back(*i);
        return Expr(TYPEDECL, names, getEM());
      }
    }
    else if(e.arity() == 3 && e[1].getKind() == ID)
      return Expr(TYPEDEF, e[1], parseExpr(e[2]));
    throw ParserException("Bad TYPE declaration: "+e.toString());
    break;
  }
  case IF: 
    if(e.arity() == 4) {
      Expr c(parseExpr(e[1]));
      Expr e1(parseExpr(e[2]));
      Expr e2(parseExpr(e[3]));
      return c.iteExpr(e1, e2);
    } else
      throw ParserException("Bad IF-THEN-ELSE expression: "
                      +e.toString());
  case COND: {
    if(e.arity() >= 3)
      return processCond(e, 1);
    else
      throw ParserException("Bad COND expression: "+e.toString());
    break;
  }
  case LET: { // (LET ((v1 [ type1 ] e1) ... ) body)
    if(!(e.arity() == 3 && e[1].getKind() == RAW_LIST && e[1].arity() > 0))
      throw ParserException("Bad LET expression: "+e.toString());

    // Iterate through the bound variables
    for(Expr::iterator i=e[1].begin(), iend=e[1].end(); i!=iend; ++i) {
      const Expr& decl = *i;
      if(decl.getKind() != RAW_LIST
         || !(decl.arity() == 2 || decl.arity() == 3))
        throw ParserException("Bad variable declaration block in LET "
                              "expression: "+decl.toString()+
                              "\n e = "+e.toString());
      if(decl[0].getKind() != ID)
        throw ParserException("Variable must be an identifier in LET "
                              "expression: "+decl[0].toString()+
                              "\n e = "+e.toString());
      Type type;
      Expr def;
      if(decl.arity()==3) {
        type = Type(parseExpr(decl[1]));
        def = parseExpr(decl[2]);
      } else 
        def = parseExpr(decl[1]);
      addBoundVar(decl[0][0].getString(), type, def);
    }
    // Parse the body recursively and return it (nuke the LET)
    return parseExpr(e[2]);
  }
//     {
//     vector<Expr> letDecls, lvars;
//     Expr letDeclsExpr;
//     for(Expr::iterator i = e[1].begin(), iend=e[1].end(); i!=iend; ++i) {
//       lvars = i->getKids();
//       lvars.insert(lvars.begin(), Expr(e.getEM(), ID, Expr(e.getEM(), STRING_EXPR, "LETDECL")));
//       letDecls.push_back(Expr(e.getEM(), RAW_LIST, lvars));
//       }
//     letDecls.insert(letDecls.begin(), Expr(e.getEM(), ID, Expr(e.getEM(), STRING_EXPR, "LETDECLS")));
//     letDeclsExpr = Expr(e.getEM(), RAW_LIST, letDecls);
//     return Expr(e.getEM(), kind, parseExpr(letDeclsExpr), parseExpr(e[2]));
//   }
  case TRUE:    { return e.getEM()->trueExpr(); }
  case FALSE:   { return e.getEM()->falseExpr();}
  case BOOLEAN: { return e.getEM()->boolExpr(); }
    break;
  default:
    DebugAssert(false,
                "TheoryCore::parseExprOp: invalid command or expression: "
                + e.toString());
    break;
  }
  return e;
}

///////////////////////////////////////////////////////////////////////////////
// Theory-cooperation framework helper functions                             //
///////////////////////////////////////////////////////////////////////////////


void TheoryCore::processFactQueue() {
  Theorem thm;
  int i;
  do {
    while (!d_queue.empty() && !d_inconsistent) {
      thm = d_queue.front();
      d_queue.pop();
      assertFactCore(thm);
    }
    if (d_inconsistent) {
      while(d_queue.size()) d_queue.pop();
      d_queueSE.clear();
      TRACE_MSG("facts addFact", "addFact[top level] => (inconsistent) }");
      return;
    }
    IF_DEBUG(debugger.counter("DP checkSAT calls")++);
    for(i=0; i<getNumTheories() && !d_inconsistent && d_queue.empty(); ++i) {
      TRACE("facts checkSat", "checkSat[", d_theories[i]->getName(), "]() {");
      d_theories[i]->checkSat(false);
      TRACE("facts checkSat", "checkSat[", d_theories[i]->getName(), "]() => }");
    }
    // Flush search engine queue inside the main loop; search engine
    // may add new facts to d_queue in the process.
    if(d_queue.empty()) {
      TRACE_MSG("facts addFact",
                "TheoryCore::processFactQueue(): flushing queueSE");
      // The queue may be emptied in the process due to
      // setInconsistent() call from the SearchEngine.  Monitor it at
      // every iteration.
      while(!d_queueSE.empty()) {
        // Copy a Theorem by value, to guarantee valid reference down
        // the call chain
        Theorem thm(d_queueSE.back());
        d_queueSE.pop_back();
        d_coreSatAPI->addLemma(thm);
      }
    }
  } while (!d_queue.empty());
}


#ifdef DEBUG
static void checkRewriteType(TheoryCore* core, const Theorem& thm) {
  Type t1(core->getBaseType(thm.getLHS()));
  Type t2(core->getBaseType(thm.getRHS()));
  DebugAssert(t1 == t2, "TheoryCore::rewriteCore: type-unsafe rewrite:\n"
              "type1 = "+t1.toString()+"\ntype2 = "+t2.toString()+"\n\n"
              +thm.toString());
}
#endif


///////////////////////////////////////////////////////////////////////////////
// Theory-cooperation framework code implementation                          //
///////////////////////////////////////////////////////////////////////////////


void TheoryCore::setInconsistent(const Theorem& e) {
  TRACE("setInconsistent", "setInconsistent(", e, ") {");
  d_inconsistent = true; d_incThm = e;
  d_queueSE.clear();
  // Theory 0 is TheoryCore, skip it
  for(int i=1; i<getNumTheories(); ++i) {
    TRACE("facts notifyInconsistent", "notifyInconsistent[", d_theories[i]->getName(), "]() {");
    d_theories[i]->notifyInconsistent(e);
    TRACE("facts notifyInconsistent", "notifyInconsistent[", d_theories[i]->getName(), "]() => }");
  }
  TRACE_MSG("setInconsistent", "setInconsistent => }");
}


void TheoryCore::enqueueFact(const Theorem& e) {
  TRACE("enqueueFact", "enqueueFact[Core](", e.getExpr(), ")");
  // The theorem scope shouldn't be higher than current
  DebugAssert(e.getScope() <= d_cm->scopeLevel(),
              "\n e.getScope()="+int2string(e.getScope())
              +"\n scopeLevel="+int2string(d_cm->scopeLevel())
              +"\n e = "+e.getExpr().toString());
  DebugAssert(d_inAddFact || d_inCheckSATCore || d_inRegisterAtom,
              "enqueueFact() is called outside of addFact()"
              " or checkSATCore() or registerAtom()");
  // No need to enqueue when already inconsistent
  if(inconsistent()) return;
             
  IF_DEBUG(if(*d_dumpTrace != "")
           dumpTrace(e.getExpr(), "enqueueFact"));
  // The theorem scope shouldn't be higher than current
  DebugAssert(e.getScope() <= d_cm->scopeLevel(),
              "\n e.getScope()="+int2string(e.getScope())
              +"\n scopeLevel="+int2string(d_cm->scopeLevel())
              +"\n e = "+e.getExpr().toString());
  if(!e.isRewrite() && e.getExpr().isFalse()) {
    IF_DEBUG(debugger.counter("conflicts enqueued from DPs")++);
    setInconsistent(e);
  } else if(getResource()) {
    d_queue.push(e);
  } else {
    // No more resources: ignore all the remaining facts and fail
    // gracefully
    setIncomplete("Exhausted user-specified resource");
  }
}


void TheoryCore::addFact(const Theorem& e)
{
  TRACE("facts addFact", "addFact[top level](", e, ") {");
  DebugAssert(!d_inAddFact, "Recursive call to addFact() is not allowed");
  DebugAssert(d_queue.empty(), "addFact[start]: Expected empty queue");
  DebugAssert(d_queueSE.empty(), "addFact[start]: Expected empty queue");
  DebugAssert(d_update_thms.empty() && d_update_data.empty(),
              "adFact[start]: Expected empty update list");
  IF_DEBUG(ScopeWatcher sw(&d_inAddFact));
  IF_DEBUG(if(*d_dumpTrace != "") dumpTrace(e.getExpr(), "addFact"));

  if(!d_inconsistent) enqueueFact(e);

  processFactQueue();

  DebugAssert(d_queue.empty(), "addFact[end]: Expected empty queue");
  DebugAssert(d_queueSE.empty(), "addFact[end]: Expected empty queue");

  TRACE_MSG("facts addFact", "addFact[top level] => }");
}


void TheoryCore::assertFactCore(const Theorem& e)
{
  TRACE("facts assertFact", "assertFactCore(", e, ") {");
  const Expr& e2 = e.getExpr();
  Theorem equiv = simplify(e2);

  Theorem estarThm(iffMP(e, equiv));
  Expr estar = estarThm.getExpr();

  if(estar.isExists()) {
    Theorem sk(d_commonRules->skolemize(estarThm));
    enqueueFact(sk);
    TRACE("skolem", "assertFactCore: created Skolemized assumption:\n ",
          sk.getExpr(), "");
  }

  // Make sure originally asserted atomic formulas have a find pointer
  if(e2 != estar && !e2.isTrue() && e2.isAbsLiteral())
    setFindLiteral(e, true);
  
  if(estar.isAnd()) {
    for(int i=0,iend=estar.arity(); i<iend; ++i)
      assertFactCore(d_commonRules->andElim(estarThm, i));
    TRACE_MSG("facts assertFact", "assertFactCore[AND] => }");
    return;
  }

  if (estar.isAbsLiteral()) {
    if (estar.isEq()) {
      // Notify the search engine
      enqueueSE(estarThm);
      Theorem solvedThm(solve(estarThm));
      // Search engine doesn't have to know about estar at this point
      if(estar != solvedThm.getExpr()) setFindLiteral(estarThm, false);
      assertEqualities(solvedThm);
    }
    else if (estar.isFalse()) {
      IF_DEBUG(debugger.counter("conflicts from simplifier")++);
      setInconsistent(estarThm);
    }
    else if (!estar.isTrue()) {
      assertFormula(estarThm);
      processUpdates();
    }
  } else {
    // Notify the search engine
    enqueueSE(estarThm);
  }

  DebugAssert(!e2.isAbsLiteral() || e2.hasFind()
              || (e2.isNot() && e2[0].hasFind()),
              "assertFactCore: e2 = "+e2.toString());
  DebugAssert(!estar.isAbsLiteral() || estar.hasFind()
              || (estar.isNot() && estar[0].hasFind()),
              "assertFactCore: estar = "+estar.toString());
  TRACE_MSG("facts assertFact", "assertFactCore => }");
}


/*!
 * Invariants: 
 * - The input theorem e is either an equality or a conjunction of
 *   equalities;
 * - In each equality e1=e2, the RHS e2 i-leaf-simplified;
 * - At the time of calling update(), all equalities in the queue are
 *   processed by assertFormula() and the equivalence classes are merged
 *   in the union-find database.
 *
 * In other words, the entire equality queue is processed "in parallel".
 */

void TheoryCore::assertEqualities(const Theorem& e)
{
  TRACE("facts eq", "assertEqualities(", e, ") {");
  DebugAssert(d_equalityQueue.empty(), "TheoryCore::assertEqualities()");
  enqueueEquality(e);

  while(!d_equalityQueue.empty()) {
    // We need to be careful: first copy the queue to a separate map
    // (to eliminate duplicates) and empty the "official" queue, so
    // that DPs can safely enqueue new equalities.

    ExprMap<Theorem> q;
    for(vector<Theorem>::iterator i=d_equalityQueue.begin(),
          iend=d_equalityQueue.end(); i!=iend; ++i) {
      if(processEquality(*i, q)) {
        // Derived inconsistency
        TRACE_MSG("facts eq", "assertEqualities[FALSE] => }");
        d_equalityQueue.clear();
        return;
      }
    }
    d_equalityQueue.clear();

    // Check invariants and assert the equations to the DPs
    for(ExprMap<Theorem>::iterator i=q.begin(), iend=q.end(); i!=iend; ++i) {
      const Theorem& e = i->second;
      DebugAssert(e.isRewrite(), "");
      DebugAssert(e.getLHS().isTerm(), "term expected");

      assertFormula(e);
    }

    // Merge the equivalence classes
    for(ExprMap<Theorem>::iterator i=q.begin(), iend=q.end(); i!=iend; ++i) {
      const Theorem& e = i->second;
      DebugAssert(find(e.getLHS()).getRHS() == e.getLHS(),
                  "find error: e = "+e.getExpr().toString()
                  +"\n\n  find(e.getLHS()) = "
                  +find(e.getLHS()).getRHS().toString());
      DebugAssert(find(e.getRHS()).getRHS() == e.getRHS(),
                  "find error: e = "+e.getExpr().toString()
                  +"\n\n  find(e.getRHS()) = "
                  +find(e.getRHS()).getRHS().toString());
//       DebugAssert(leavesAreSimp(e.getRHS()), "assertEqualities("
//                +e.toString()+")");
      
      e.getLHS().setFind(e);
    }

    d_em->invalidateSimpCache();
  
    // Call the update() functions (process NotifyLists).  

    for(ExprMap<Theorem>::iterator i=q.begin(), iend=q.end(); i!=iend; ++i) {
      const Theorem& e = i->second;
      NotifyList *L = e.getLHS().getNotify();
      if (L) processNotify(e, L);
    }
  }
  processUpdates();
  TRACE_MSG("facts eq", "assertEqualities => }");
}


void TheoryCore::assertFormula(const Theorem& thm)
{
  TRACE("facts assertFact", "assertFormula(", thm, ") {");
  const Expr& e = thm.getExpr();
  if (e.isAbsLiteral()) {
    Theory* i = theoryOf(e);
    // (Dis)equalities should also be asserted to the theories of
    // their types for concrete model generation 
    Theory* i2(NULL);
    // Treat disequality as a separate theory, so that terms are
    // reported as shared
    if(e.isNot() && e[0].isEq())
      setupTerm(e, this);
    else
      setupTerm(e,i);

    // Use find to force af to rewrite to TRUE and NOT af to rewrite to FALSE,
    // where af is an atomic formula.  If af is an equality, make sure its lhs
    // is greater than its rhs so the simplifier will be able to use the find.
    enqueueSE(thm);
    Theorem findThm;
    NotifyList* L;
    if (e.isNot()) {
      DebugAssert(!e[0].hasFind(), "already has find");
      if (e[0].isEq()) {
        // Save the disequality for later processing
        d_diseq.push_back(thm);
        // For concrete model generation
        i2 = theoryOf(getBaseType(e[0][0]).getExpr()); 

        if(e[0][0] < e[0][1]) {
          Expr e2 = e[0][1].eqExpr(e[0][0]);
          DebugAssert(!e2.hasFind(), "already has find");
          findThm = transitivityRule(d_commonRules->rewriteUsingSymmetry(e2),
                                     d_commonRules->notToIff(thm));
          e2.setFind(findThm);
          d_em->invalidateSimpCache();
          L = e2.getNotify();
          if (L) processNotify(findThm, L);
        }
      }
      findThm = d_commonRules->notToIff(thm);
      e[0].setFind(findThm);
      d_em->invalidateSimpCache();
      L = e[0].getNotify();
      if (L) processNotify(findThm, L);
    }
    else {
      // If we are called from assertEqualities(), we may get e1=e2
      // for which there is a known fact e1/=e2 or e2/=e1.  In this
      // case, we should derive a contradiction.
      // Note, that this is not necessarily detected by the DPs.
      if(e.hasFind()) {
        // Why would find(e) be always false?  Not if we set find to
        // all atomic formulas...
//      DebugAssert(find(e).getRHS().isFalse(), "e = "+e.toString()
//                  +"\nfind(e) = "+find(e).getRHS().toString());
        findThm = find(e);
        if(findThm.getExpr().isFalse()) {
          IF_DEBUG(debugger.counter("conflicts from find pointers")++);
          setInconsistent(d_commonRules->contradictionRule(thm,
                            d_commonRules->iffFalseElim(find(e))));
          TRACE_MSG("facts assertFact", "assertFormula[contradiction] => }");
          return;
        }
      }
      else {
        findThm = d_commonRules->iffTrue(thm);
        e.setFind(findThm);
        d_em->invalidateSimpCache();
        L = e.getNotify();
        if (L) processNotify(findThm, L);
      }

      if(e.isEq()) {
        if(e[0] < e[1]) {
          Expr e2 = e[1].eqExpr(e[0]);
          if(e2.hasFind()) {
//          DebugAssert(find(e2).getRHS().isFalse(), "e2 = "+e2.toString()
//                      +"\nfind(e2) = "+find(e2).getRHS().toString());
            findThm = find(e2);
            if(findThm.getExpr().isFalse()) {
              IF_DEBUG(debugger.counter("conflicts from find pointers")++);
              setInconsistent(d_commonRules->contradictionRule(
                                symmetryRule(thm),
                                d_commonRules->iffFalseElim(find(e2))));
              TRACE_MSG("facts assertFact", "assertFormula[e[1]/=e[0]] => }");
              return;
            }
          } else {
            findThm = transitivityRule(d_commonRules->rewriteUsingSymmetry(e2),
                                       d_commonRules->iffTrue(thm));
            e2.setFind(findThm);
            d_em->invalidateSimpCache();
            L = e2.getNotify();
            if (L) processNotify(findThm, L);
          }
        }
      }
    }
    d_em->invalidateSimpCache();
    // Do not send existential quantifiers to DPs; skolemize them and
    // notify the Search Engine about it.
    if(thm.getExpr().isExists())
      enqueueFact(d_commonRules->skolemize(thm));
    else {
      TRACE("facts assertFact", ("assertFact[->" + i->getName() + "]("), thm, ") {");
      i->assertFact(thm);
      TRACE("facts assertFact", "assertFact[->", i->getName(),"] => }");
      if(i2 != NULL && i != i2) {
        TRACE("facts assertFact", ("assertFact[->" + i2->getName() + "]("), thm, ") {");
        IF_DEBUG(debugger.counter("assertFact(diseq) by type")++);
        i2->assertFact(thm);
        TRACE("facts assertFact", "assertFact[->", i2->getName(),"] => }");
      }
    }
  }
  else {
    DebugAssert(false,"assertFormula: nonliteral asserted:\n  "
                +thm.toString());
  }
  TRACE_MSG("facts assertFact", "assertFormula => }");
}


void TheoryCore::setupTerm(const Expr& t, Theory* i)
{
  TRACE("facts setup", "setupTerm(", t, ", i="+i->getName()+") {");

  // Even if t is already setup, it may become shared with another theory
  Theory* j = theoryOf(t);
  if(i != j && t.isTerm()) {
    TRACE("facts setup", "addSharedTerm[->"+j->getName()+"](", t, ") {");
    j->addSharedTerm(t);
    TRACE_MSG("facts setup", "addSharedTerm[->"+j->getName()+"] => }");
    TRACE("facts setup", "addSharedTerm[->"+i->getName()+"](", t, ") {");
    i->addSharedTerm(t);
    TRACE_MSG("facts setup", "addSharedTerm[->"+i->getName()+"] => }");
    d_sharedTerms.insert(t, j);
  }
  
  int k;

  // Atomic formulas (non-terms) may have find pointers without the
  // subterms being setup.  Recurse down to the terms before checking
  // for find pointers.
  if (!t.isTerm()) {
    if(t.isAbsLiteral()) {
      for (k = 0; k < t.arity(); ++k) {
        setupTerm(t[k], i);
      }
      TRACE("facts setup", "setup[->"+j->getName()+"](", t, ") {");
      j->setup(t);
      TRACE("facts setup", "setup[->",j->getName(),"] => }");
    }
    TRACE_MSG("facts setup", "setupTerm[not term] => }");
    return;
  }

  // If already setup, nothing else to do
  if (t.hasFind()) {
    TRACE_MSG("facts setup", "setupTerm[has find] => }");
    return;
  }

  // Proceed with the setup

  // Add the term into the set of all terms
  d_terms.push_back(t);

  for (k = 0; k < t.arity(); ++k) {
    setupTerm(t[k],theoryOf(t));
  }
  Theorem thm = d_commonRules->reflexivityRule(t);
  t.setFind(thm);
  TRACE("facts setup", "setup[->"+j->getName()+"](", t, ") {");
  j->setup(t);
  TRACE("facts setup", "setup[->",j->getName(),"] => }");

  // Assert the subtyping predicate AFTER the setup is complete
  Theorem pred = d_rules->typePred(t);
  // pred = d_commonRules->iffMP(pred, simplify(pred.getExpr()));
  const Expr& predExpr = pred.getExpr();
  // TRACE("tccs", "setupTerm: subtype predicate:\n", predExpr, "");
  if(predExpr.isFalse()) {
    IF_DEBUG(debugger.counter("conflicts from type preficate")++);
    setInconsistent(pred); 
  }
  else if(!predExpr.isTrue()) {
    Theory* k = theoryOf(t.getType().getExpr());
    TRACE("facts setup", "assertTypePred[->"+k->getName()+"]("
          +t.toString()+", ", pred, ") {");
    k->assertTypePred(t, pred);
    TRACE_MSG("facts setup", "assertTypePred[->"+k->getName()+"] => }");
  }

  d_typePredAsserted[t] = true;
  TRACE_MSG("facts setup", "setupTerm => }");
}


Theorem TheoryCore::rewriteCore(const Expr& e)
{
  TRACE("rewrite", "rewriteCore(", e, ") {");
  if (e.hasFind()) {
    TRACE("rewrite", "rewriteCore[hasFind] => ", find(e), " }");
    IF_DEBUG(checkRewriteType(this, find(e)));
    return find(e);
  }
  if (e.isRewriteNormal()) {
    IF_DEBUG(
      // Check that the RewriteNormal flag is set properly.  Note that we
      // assume theory-specific rewrites are idempotent
      e.clearRewriteNormal();
      Expr rewritten(rewriteCore(e).getRHS());
      e.setRewriteNormal(); // Restore the flag
      DebugAssert(rewritten == e, 
                  "Expected no change: e = " + e.toString()
                  +"\n rewriteCore(e) = "+rewritten.toString());
    )
    TRACE("rewrite", "rewriteCore[isRewriteNormal] => ", reflexivityRule(e), " }");
    return reflexivityRule(e);
  }
  Theorem thm;
  if (e.isNot() || e.isEq()) {
    TRACE("rewrite", "rewriteLitCore(", e, ") {");
    thm = rewriteLitCore(e);
    IF_DEBUG(checkRewriteType(this, thm));
    TRACE("rewrite", "rewriteLitCore => ", thm, "}");
    if(e != thm.getRHS()) {
      thm = rewriteCore(thm);
      TRACE("rewrite", "rewriteCore => ", thm, " }");
      return thm;
    }
  }
  TRACE("rewrite", ("rewrite["+theoryOf(e)->getName()+"]("), e, ") {");
  thm = theoryOf(e)->rewrite(e);
  TRACE("rewrite", ("rewrite["+theoryOf(e)->getName()+"] => "), thm, "}");
  IF_DEBUG(checkRewriteType(this, thm));

  const Expr& e2 = thm.getRHS();

  // Theory-specific rewrites for equality should ensure that lhs >= rhs, or
  // there is danger of an infinite loop.
  DebugAssert(!e2.isEq() || e2[0] >= e2[1],
              "theory-specific rewrites for equality should ensure lhs >= rhs");

  if (e != e2) {
    thm = rewriteCore(thm);
    TRACE("rewrite", "rewriteCore => ", thm, " }");
    return thm;
  }

  TRACE("rewrite", "rewriteCore[refl] => ", thm, " }");
  return thm;
}


bool TheoryCore::checkSATCore() {
  TRACE_MSG("facts checkSat", "checkSATCore() {");
  DebugAssert(d_queue.empty(), "checkSATCore[start]: Expected empty queue");
  DebugAssert(d_queueSE.empty(), "checkSATCore[start]: Expected empty queue");
  DebugAssert(!d_inCheckSATCore, "Recursive call to checkSATCore is not allowed!");
  IF_DEBUG(ScopeWatcher sw(&d_inCheckSATCore));
  IF_DEBUG(debugger.counter("DP checkSAT(fullEffort) calls")++);
  for(int i=0; i<getNumTheories() && !d_inconsistent && d_queue.empty(); ++i) {
    TRACE("facts checkSat", "checkSAT (full effort) [",
          d_theories[i]->getName(), "]() {");
    d_theories[i]->checkSat(true);
    TRACE("facts checkSat", "checkSAT (full effort) [",
          d_theories[i]->getName(), "]() }");
  }

  if(d_queue.empty()) {
    DebugAssert(d_queueSE.empty(),
                "checkSATCore[start]: Expected empty queue");
    TRACE_MSG("facts checkSat", "checkSATCore[queue empty] => true }");
    return true;
  } 

  // Process enqueued facts
  processFactQueue();
 
  TRACE("facts checkSat", "checkSATCore => ",
        d_inconsistent? "true" : "false", " }");

  DebugAssert(d_queue.empty(), "checkSATCore[start]: Expected empty queue");
  DebugAssert(d_queueSE.empty(), "checkSATCore[start]: Expected empty queue");

  return(d_inconsistent); 
}


void TheoryCore::addToVarDB(const Expr&  e)
{
  TRACE("model", "TheoryCore::addToVarDB(", e, ")");
  d_vars.push_back(e);
}


void TheoryCore::refineCounterExample()
{
  // Theory 0 is TheoryCore, skip it
  for(int i = 1; i<getNumTheories(); i++) {
    if(d_theories[i] != this)
      d_theories[i]->refineCounterExample();
    if(inconsistent()) {
      vector<Expr> assump;
      inconsistentThm().getLeafAssumptions(assump);
      Expr a = Expr(RAW_LIST, assump, d_em);
      throw EvalException("Theory["+d_theories[i]->getName()
                      +"]: Model Creation failed due "
                      "to the following assumptions:\n\n"
                      +a.toString()
                      +"\n\nYou might be using an incomplete logical fragment.");
    }
  }
}


void TheoryCore::computeModelBasic(const vector<Expr>& v) {
  for(vector<Expr>::const_iterator i=v.begin(), iend=v.end(); i!=iend; ++i) {
    TRACE("model", "Model var "+i->toString()+" = ", find(*i).getRHS(), "");
    DebugAssert((*i).getType().isBool(), "TheoryCore::computeModel: *i = "
                +(*i).toString());
    Expr val = find(*i).getRHS();
    if(!val.isBoolConst()) val = d_em->trueExpr();
    assignValue(*i, val);
  }
}


void TheoryCore::collectBasicVars() {
  TRACE_MSG("model", "collectBasicVars() {");
  // Clear caches
  d_varModelMap.clear();
  d_varAssignments.clear();
  // Current stack of variables to process
  vector<Expr> stack(d_vars.begin(), d_vars.end());
  size_t lastSize(0);
  while(stack.size() > 0) {
    Expr var(stack.back());
    stack.pop_back();
    if(d_varModelMap.count(var) > 0) continue; // Already processed
    Theorem findThm(find(var));
    if(findThm.getRHS()!=var) { // Replace var with its find
      d_simplifiedModelVars[var] = findThm;
      stack.push_back(findThm.getRHS());
      TRACE("model", "collectBasicVars: simplified var: ", findThm.getExpr(), "");
      continue; // Recycle to the beginning of the loop
    }
    lastSize = stack.size();
    TRACE("model", "getModelTerm(", var, ") {");
    getModelTerm(var, stack);
    TRACE("model", "getModelTerm => ",
          Expr(RAW_LIST, stack, getEM()), " }");
    if(stack.size() == lastSize) {
      // Add a primitive variable
      TRACE("model", "collectBasicVars: adding primitive var: ", var, "");
      d_basicModelVars.push_back(var);
      if(var.isTerm()) {
        Theory* t1 = theoryOf(var);
        Theory* t2 = theoryOf(getBaseType(var).getExpr().getKind());
        if(t1 != t2) {
          TRACE("model", "collectBasicVars: adding shared var: ", var, "");
          d_sharedTerms.insert(var, t1);
          t1->addSharedTerm(var);
          t2->addSharedTerm(var);
        }
      }
    } else { // Record the descendants of var
      vector<Expr>& kids = d_varModelMap[var];
      for(size_t i=lastSize; i<stack.size(); ++i) {
        DebugAssert(stack[i] != var, "Primitive var was pushed on "
                    "the stack in computeModelTerm(): "+var.toString());
        kids.push_back(stack[i]);
      }
      TRACE("model", "collectBasicVars: var="+var.toString()
            +" maps into vars=", Expr(RAW_LIST, kids, getEM()), "");
    }
  }
  TRACE_MSG("model", "collectBasicVars() => }");
}


void TheoryCore::buildModel(ExprMap<Expr>& m) {
  TRACE_MSG("model", "buildModel() {");

  size_t numTheories = getNumTheories();
  // Use STL set to prune duplicate variables in theories
  set<Expr> theoryExprs[numTheories+1];
  // Sort out model vars by theories
  for(size_t j = 0 ; j<d_basicModelVars.size() ; j++) {
    const Expr& var = d_basicModelVars[j];
    Theorem findThm(find(var));
    if(findThm.getRHS()!=var) { // Replace var with its find and skip it
      TRACE("model", "buildModel: replace var="+var.toString(),
            " with find(var)=", findThm.getRHS());
      d_simplifiedModelVars[var] = findThm;
      continue;
    }

    Theory *th = theoryOf(getBaseType(var).getExpr().getKind());
    size_t i=0;
    for(; i<numTheories && d_theories[i] != th; ++i);
    DebugAssert(i<numTheories && d_theories[i] == th,
                "TheoryCore::buildModel: cannot find the theory ["
                +th->getName()+"] for the variable: "
                +var.toString());
    theoryExprs[i].insert(var);
    TRACE("model", "buildModel: adding ", var,
          " to theory "+d_theories[i]->getName());
  }
  // Build a model for the basic-type variables
  for(int i=0; i<getNumTheories(); i++) {
    if(theoryExprs[i].size() > 0) {
      TRACE("model", "computeModelBasic[", d_theories[i]->getName(), "] {");
      // Copy the corresponding variables into a vector
      vector<Expr> vars;
      vars.insert(vars.end(), theoryExprs[i].begin(), theoryExprs[i].end());
      d_theories[i]->computeModelBasic(vars);
      TRACE("model", "computeModelBasic[", d_theories[i]->getName(), "] => }");
      if(inconsistent()) {
        vector<Expr> assump;
        inconsistentThm().getLeafAssumptions(assump);
        Expr a = Expr(RAW_LIST, assump, d_em);
        throw EvalException
          ("Model Creation failed in Theory["
           +d_theories[i]->getName()
           +"] due to the following assumptions:\n\n"
           +a.toString()
           +"\n\nYou might be using an incomplete logical fragment.");
      }
    }
  }
  // Recombine the values for the compound-type variables
  ExprHashMap<Theorem>::iterator k, kend=d_simplifiedModelVars.end();
  for(CDList<Expr>::const_iterator i=d_vars.begin(), iend=d_vars.end(); i!=iend; ++i) {
    Expr var(*i);
    TRACE("model", "buildModel: recombining var=", var, "");
    k=d_simplifiedModelVars.find(var);
    Theorem simp; // Null by default
    if(k!=kend) { // This var is simplified
      simp = k->second;
      TRACE("model", "buildModel: simplified var="+var.toString()+" to ",
            simp.getRHS(), "");
      var = simp.getRHS();
    }
    collectModelValues(var, m);
    if(d_varAssignments.count(var) > 0) {
      if(!simp.isNull()) {
        Theorem thm(transitivityRule(simp, d_varAssignments[var]));
        assignValue(thm);
        DebugAssert(thm.getLHS() == *i, "");
        m[*i] = thm.getRHS();
      } else
        m[*i] = d_varAssignments[var].getRHS();
    }
//     else if(simp.isNull())
//       m[*i] = *i;
//     else
//       m[*i] = simp.getRHS();
  }
  TRACE_MSG("model", "buildModel => }");
}


// Recursively build a compound-type variable assignment for e
/*! Not all theories may implement aggregation of compound values.  If
 *  a compound variable is not assigned by a theory, add the more
 *  primitive variable assignments to 'm'.
 *
 * Some variables may simplify to something else (simplifiedVars map).
 * INVARIANT: e is always simplified (it's not in simplifiedVars map).
 * Also, if v simplifies to e, and e is assigned, then v must be assigned.
 */
void TheoryCore::collectModelValues(const Expr& e, ExprMap<Expr>& m) {
  TRACE("model", "collectModelValues(", e, ") {");
  if(d_varAssignments.count(e) > 0) {
    TRACE("model", "collectModelValues[cached] => ",
          d_varAssignments[e].getRHS(), " }");
    return; // Got it already
  }
  ExprHashMap<Theorem>::iterator k, kend=d_simplifiedModelVars.end();
  k=d_simplifiedModelVars.find(e);
  if(k!=kend) {
    const Theorem& findThm = k->second;
    const Expr& ee = findThm.getRHS();
    collectModelValues(ee, m);
    if(d_varAssignments.count(ee) > 0) {
      Theorem thm = transitivityRule(findThm, d_varAssignments[ee]);
      assignValue(thm);
    }
    TRACE("model", "collectModelValues[simplified] => ",
          d_varAssignments[e].getRHS(), " }");
    return;
  }
  if(d_varModelMap.count(e) == 0) { // Consider it a value of itself
    assignValue(reflexivityRule(e));
    TRACE("model", "collectModelValues[e=e] => ", e, " }");
    return; // Got it already
  }
  // Get the vector of more primitive vars
  const vector<Expr>& vars = d_varModelMap[e];
  // Recurse
  bool gotAll(true);  // Whether we got all the values
  for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end(); i!=iend; ++i) {
    Expr var(*i);
//     k=d_simplifiedModelVars.find(var);
//     Theorem simp; // Null by default
//     if(k!=kend) { // This var is simplified
//       simp = k->second;
//       var = simp.getRHS();
//     }
    collectModelValues(var, m);
    if(d_varAssignments.count(var) == 0) {
      gotAll = false;
    }
//     else if(!simp.isNull()) {
//       Theorem thm(transitivityRule(simp, d_varAssignments[var]));
//       DebugAssert(thm.getLHS() == *i, "");
//       assignValue(thm);
//     }
  }
  IF_DEBUG(vector<Expr> res);
  if(gotAll) {
    vector<Expr> assigned; // What DP actually assigns
    Theory* th = theoryOf(getBaseType(e).getExpr());
    TRACE("model", "computeModel["+th->getName()+"](", e, ") {");
    th->computeModel(e, assigned);
    TRACE("model", "computeModel["+th->getName()+"] => ",
          Expr(RAW_LIST, assigned, getEM()), " }");
    // Check if the assigned vars are different from e
    if(!(assigned.size()==1 && assigned[0]==e)) {
      //    if(d_varAssignments.count(e) == 0) {
      for(vector<Expr>::iterator i=assigned.begin(), iend=assigned.end();
          i!=iend; ++i) {
        if(*i == e) continue; // Skip the original var
        m[*i] = getModelValue(*i).getRHS();
        IF_DEBUG(res.push_back(getModelValue(*i).getExpr()));
      }
    } else {
      IF_DEBUG(res.push_back(getModelValue(e).getExpr()));
    }
  }
  TRACE("model", "collectModelValues => ",
        Expr(RAW_LIST, res, getEM()), " }");
}


void TheoryCore::enqueueEquality(const Theorem& e) {
  TRACE("enqueueEquality", "enqueueEquality["+getName()+"](",
        e.getExpr(), ")");
  IF_DEBUG(if(*d_dumpTrace != "")
           dumpTrace(e.getExpr(), "enqueueEquality"));
  IF_DEBUG(const Expr& expr = e.getExpr());
  IF_DEBUG(int kind = expr.getKind());
  DebugAssert(kind == EQ || kind == AND || kind == EXISTS || kind == FALSE,
              "enqueueEnquality: bad input: "+expr.toString());
  // The theorem scope shouldn't be higher than current
  DebugAssert(e.getScope() <= d_cm->scopeLevel(),
              "\n e.getScope()="+int2string(e.getScope())
              +"\n scopeLevel="+int2string(d_cm->scopeLevel())
              +"\n e = "+expr.toString());
//   DebugAssert(kind != EQ || !expr[0].subExprOf(expr[1]),
//            "enqueueEquality("+expr.toString()+")");
  d_equalityQueue.push_back(e);
}


/*!
 * Fill in the copy of the equality queue with single equalities by
 * processing the input 'eq', which can be an equality, a conjunction
 * of equalities, or an existential quantifier of the above.
 */
bool TheoryCore::processEquality(const Theorem& thm, ExprMap<Theorem>& q) {
  const Expr& e = thm.getExpr();
  TRACE("facts eq", "processEquality(", e, ") {");
  bool res(false);

  switch(e.getKind()) {
  case FALSE:
    IF_DEBUG(debugger.counter("conflicts from solver")++);
    setInconsistent(thm);
    res = true;
    break;
  case EXISTS:
    // Skolemize the quantifier and expect an equality or a
    // conjunction of equalities inside
    res = processEquality(d_commonRules->skolemize(thm), q);
    break;
  case AND: 
    for(int i=0, iend=e.arity(); i!=iend; ++i)
      if(res = processEquality(d_commonRules->andElim(thm, i), q)) break;
    break;
  case EQ:
    // find(e0) != e1 && find(e1) != e0
    if(find(e[0]).getRHS() != e[1] && e[0] != find(e[1]).getRHS()) {
      DebugAssert(e[0] != e[1], "processEquality: e = "+e.toString());
      DebugAssert(!e[1].hasFind() || find(e[1]).getRHS() == e[1],
                  "processEquality: e = "+e.toString()
                  +"\nfind(e[1]) = "+find(e[1]).getRHS().toString());
//       DebugAssert(!e[0].subExprOf(e[1]), "processEquality: e = "+e.toString());
      q[e] = thm;
      TRACE("facts eq", "  [new]  ", e, ",\n");
    } else if(find(e).getRHS().isFalse()) {
      TRACE("facts eq", " [FALSE] ", e,  "]");
      IF_DEBUG(debugger.counter("conflicts from find pointers")++);
      setInconsistent(d_commonRules->contradictionRule(thm,
                        d_commonRules->iffFalseElim(find(e))));
      res = true;
    } else {
      TRACE("facts eq", "         ", e, ",");
    }
    break;
  default:
    DebugAssert(false,
                "TheoryCore::processEquality(): bad input:\n "
                +thm.toString());
  }
  TRACE("facts eq", "processEquality => ", res? "true" : "false", " }");
  return res;
}


void TheoryCore::processNotify(const Theorem& e, NotifyList *L)
{
  DebugAssert(L, "Expected non-NULL notify list");
  // L may be changing during update() call; copy it to a local
  // vector before calling update()
  //  vector<pair<Theory*, Expr> > l;
  //  for (unsigned k = 0, size = L->size(); k < size; ++k) {
  //    l.push_back(pair<Theory*,Expr>(L->getTheory(k), L->getExpr(k)));
  //  }
  for(unsigned k = 0; k < L->size(); ++k) {
    TRACE("facts update", "update["+L->getTheory(k)->getName()+"]("
          +e.toString()+", ", L->getExpr(k), ") {");
    L->getTheory(k)->update(e, L->getExpr(k));
    TRACE("facts update", "update[", L->getTheory(k)->getName(), "] => }");
  }
}


void TheoryCore::setIncomplete(const string& reason) {
  d_incomplete.insert(reason, true);
}


void
TheoryCore::setResourceLimit(unsigned limit) {
  d_resourceLimit = limit;
}


IF_DEBUG(static ExprMap<bool> simpStack);

Theorem TheoryCore::simplify(const Expr& e, bool forceRebuild)
{
  TRACE("simplify", "simplify(", e, ") {");
  IF_DEBUG(ScopeWatcher sw(&d_inSimplify));
  Theorem (TheoryCore::*oldSimplifier)(const Expr&) = d_currentRecursiveSimplifier;

  if (*d_simplifyInPlace) {
    if (!forceRebuild) {
      d_currentRecursiveSimplifier = &CVCL::TheoryCore::simplifyInPlaceRec;
      Theorem res(simplifyRec(e));
      d_currentRecursiveSimplifier = oldSimplifier;
      TRACE("simplify", "simplify[in place] => ", res.getRHS(), " }");
      return res;
    }
    else {
      d_currentRecursiveSimplifier = &CVCL::TheoryCore::simplifyFullRec;
      d_em->invalidateSimpCache();
      Theorem thm = simplifyRec(e);
      d_em->invalidateSimpCache();
      if (!e.isAbsLiteral() && e != thm.getRHS()) {
        e.setFind(thm);
      }
      d_currentRecursiveSimplifier = oldSimplifier;
      TRACE("simplify", "simplify[rebuild] => ", thm.getRHS(), " }");
      return thm;
    }
  }
  d_currentRecursiveSimplifier = &CVCL::TheoryCore::simplifyFullRec;
  Theorem res(simplifyRec(e));
  d_currentRecursiveSimplifier = oldSimplifier;
  TRACE("simplify", "simplify => ", res.getRHS(), " }");
  return res;
}


Theorem TheoryCore::simplifyRec(const Expr& e)
{
  DebugAssert(d_currentRecursiveSimplifier, "unexpected call to simplifyRec");
  return (this->*d_currentRecursiveSimplifier)(e);
}


Theorem TheoryCore::simplifyFullRec(const Expr& e)
{
  TRACE("simplifyRec", "simplifyRec(", e, ") {");
  DebugAssert(simpStack.count(e) == 0, "TheoryCore::simplifyRec: loop detected over e =\n"
              +e.toString());
  TRACE("simplify stack", "simpStack.size = ", simpStack.size(), "");
  DebugAssert(simpStack.size() < 10000,
              "TheoryCore::simplify: too deep recursion depth");
  IF_DEBUG(simpStack[e] = true);
  Theorem thm;
  if(e.hasFind()) {
    thm = find(e);
    const Expr& e2 = thm.getRHS();
    if (e2.hasFind()) {
      DebugAssert(e2.isTrue() || e2.isFalse() || e2.isTerm(),
                  "Unexpected find pointer");
      TRACE_MSG("simplifyRec", "Using find");
      TRACE("simplifyRec", "simplify => ", thm, "}\n");
      IF_DEBUG(simpStack.erase(e));
      return thm;
    }
    else {
      DebugAssert(!e.isAbsLiteral(), "Expected non-literal: e = "+e.toString()
                  +"\n e2 = "+e2.toString());
      DebugAssert(*d_simplifyInPlace, "Expected in-place flag: e = "
                  +e.toString()+"\n e2 = "+e2.toString());
      Theorem thm2 = simplifyRec(e2);
      if (thm2.getLHS() != thm2.getRHS()) {
        e.setFind(transitivityRule(thm,thm2));
        TRACE_MSG("simplifyRec", "Using find 2");
        TRACE("simplifyRec", "simplify => ", e.getFind(), "}\n");
        IF_DEBUG(simpStack.erase(e));
        return e.getFind();
      }
      TRACE_MSG("simplifyRec", "Using find 3");
      TRACE("simplifyRec", "simplify => ", thm, "}\n");
      IF_DEBUG(simpStack.erase(e));
      return thm;
    }
 }

  if(e.validSimpCache()) {
    TRACE_MSG("simplifyRec", "Using cached result");
    TRACE("simplifyRec", "simplify => ", e.getSimpCache(), "}\n");
    IF_DEBUG(simpStack.erase(e));
    return e.getSimpCache();
  }

  // Optimization: check both sides of = or <=> for syntactic equality
  switch(e.getKind()) {
  case EQ:
  case IFF:
    if(e[0]==e[1]) {
      thm = d_commonRules->iffTrue(reflexivityRule(e[0]));
      IF_DEBUG(debugger.counter("simplified x=x")++);
      break; // Break out of switch()
    }
    // Otherwise fall through
  default: // Make a recursive call
    TRACE("simplifyRec", "simplifyOp["+theoryOf(e)->getName()+"](",
          e, ") {");
    thm = theoryOf(e)->simplifyOp(e);
    TRACE("simplifyRec", "simplifyOp["+theoryOf(e)->getName()+"] => ",
          thm.getRHS(), " }");
    thm = rewriteCore(thm);
  }

  const Expr& e2 = thm.getRHS();
#ifdef DEBUG
  // The "ite-lift-unary" option will break this check (experimental)
  if(!getFlags()["ite-lift-unary"].getBool()) {
    if (!e2.isTerm() || !e2.hasFind()) {
      // The rewriter should guarantee that all of its children are simplified.
      for (int k=0; k<e2.arity(); ++k) {
        Expr simplified(simplifyRec(e2[k]).getRHS());
        DebugAssert(e2[k]==simplified,"Simplify Error 1:\n e2[k="+int2string(k)
                    +"] = "
                    +e2[k].toString() + "\nSimplified = "
                    +simplified.toString()
                    +"\ne2 = "+e2.toString());
//      Expr rewritten(rewriteCore(e2[k]).getRHS());
//      DebugAssert(e2[k]==rewritten,"Simplify Error 2: e2[k] = \n"
//                  +e2[k].toString() + "\nSimplified rewritten = \n"
//                  +rewritten.toString());
      }
    }
    Expr rewritten(rewriteCore(e2).getRHS());
    DebugAssert(e2==rewritten,"Simplify Error 2: e2 = \n"
                +e2.toString() + "\nSimplified rewritten = \n"
                +rewritten.toString());
  }
#endif
  e.setSimpCache(thm);
  if (e != e2) {
    e2.setSimpCache(reflexivityRule(e2));
  }
  TRACE("simplifyRec", "simplify => ", thm, "}\n");
  IF_DEBUG(simpStack.erase(e));
  return thm;
}


// This needs to be reviewed -- I'm not sure it's working properly
Theorem TheoryCore::simplifyInPlaceRec(const Expr& e)
{
  TRACE("simplifyRec", "simplifyInPlaceRec(", e, ") {");
  Theorem thm;
  if (e.hasFind()) {
    thm = find(e);
    const Expr& e2 = thm.getRHS();
    if (e2.hasFind()) {
      DebugAssert(e2.isTrue() || e2.isFalse() || e2.isTerm(),
                  "Unexpected find pointer");
      TRACE_MSG("simplifyRec", "Using find");
      TRACE("simplifyRec", "simplifyInPlaceRec => ", thm, "}\n");
      return thm;
    }
    else {
      DebugAssert(!e.isAbsLiteral(), "huh?");
      Theorem thm2 = simplifyInPlaceRec(e2);
      if (thm2.getLHS() != thm2.getRHS()) {
        e.setFind(transitivityRule(thm,thm2));
        TRACE_MSG("simplifyRec", "Using find 2");
        TRACE("simplifyRec", "simplifyInPlaceRec => ", e.getFind(), "}\n");
        return e.getFind();
      }
      TRACE_MSG("simplifyRec", "Using find 3");
      TRACE("simplifyRec", "simplifyInPlaceRec => ", thm, "}\n");
      return thm;
    }
  }

  if (e.validSimpCache()) {
    TRACE_MSG("simplifyRec", "Using cached result");
    TRACE("simplifyRec", "simplifyInPlaceRec => ", e.getSimpCache(), "}\n");
    return e.getSimpCache();
  }

  int k, ar = e.arity();
  if (ar > 0) {
    vector<Theorem> newChildrenThm;
    vector<unsigned> changed;
    const vector<Expr>& kids = e.getKids();
    for(k = 0; k < ar; ++k) {
      thm = simplifyRec(kids[k]);
      if (thm.getLHS() != thm.getRHS()) {
        if ((e.getKind() == OR && thm.getRHS().isTrue()) ||
            (e.getKind() == AND && thm.getRHS().isFalse())) {
          newChildrenThm.clear();
          changed.clear();
          newChildrenThm.push_back(thm);
          changed.push_back(k);
          break;
        }
        else if (k == 0 && e.getKind() == ITE && (thm.getRHS().isBoolConst())) {
          newChildrenThm.push_back(thm);
          changed.push_back(k);
          if (thm.getRHS().isTrue()) k += 1;
          else k += 2;
          thm = simplifyRec(kids[k]);
          newChildrenThm.push_back(thm);
          changed.push_back(k);          
          break;
        }
        else {
          newChildrenThm.push_back(thm);
          changed.push_back(k);
        }
      }
    }
    if (changed.size() == 0) thm = rewriteCore(e);
    else {
      thm = substitutivityRule(e, changed, newChildrenThm);
      Theorem thm2 = rewriteCore(thm.getRHS());
      const Expr& e2 = thm2.getLHS();
      if (e2 == thm2.getRHS()) {
        if (!e.isAbsLiteral() && !e2.isAtomic() && !e2.isAbsLiteral()) {
          e.setFind(thm);
          thm = reflexivityRule(e);
        }
      }
      else thm = transitivityRule(thm, thm2);
    }
  } else {
    thm = rewriteCore(e);
  }
  e.setSimpCache(thm);
  const Expr& e2 = thm.getRHS();
  if (e != e2) {
    e2.setSimpCache(reflexivityRule(e2));
  }
  TRACE("simplifyRec", "simplifyInPlaceRec => ", thm, "}\n");
  return thm;
}


bool TheoryCore::incomplete(vector<string>& reasons) {
  if(d_incomplete.size() > 0) {
    for(CDMap<string,bool>::iterator i=d_incomplete.begin(),
          iend=d_incomplete.end(); i!=iend; ++i)
      reasons.push_back((*i).first);
    return true;
  }
  else
    return false;
}


Theorem TheoryCore::rewriteCore(const Theorem& e) {
  DebugAssert(e.isRewrite(),
              "rewriteCore(thm): not equality or iff:\n  " + e.toString());
  return transitivityRule(e, rewriteCore(e.getRHS()));
}


Theorem TheoryCore::rewriteLiteral(const Expr& e) {
  DebugAssert(e.isAbsLiteral(), "rewriteLiteral("+e.toString()
              +")\nExpected a literal.");
  Theorem res;
  //Theory* i = theoryOf(getBaseType(e).getExpr());
  bool neg(e.isNot());
  const Expr a = neg? e[0] : e;
  Theory * i;
  if(a.isEq())
    i = theoryOf(getBaseType(a[0]).getExpr());  
  else if (a.arity() > 1)
    i = theoryOf(getBaseType(a[0]).getExpr());
  else
    i = theoryOf(a);
  TRACE("rewrite", ("rewriteAtomic["+i->getName()+"]("), e, ") {");
  res = i->rewriteAtomic(a);
  TRACE("rewrite", ("rewriteAtomic["+i->getName()+"] => "), res, "}");
  if(neg) res = d_commonRules->iffContrapositive(res);
  return res;
}

/*****************************************************************************/
/*!
 * Function: TheoryCore::solve
 *
 * Author: Clark Barrett
 *
 * Created: Wed Feb 26 16:17:54 2003
 *
 * This is a generalization of what's in my thesis.  The goal is to rewrite e
 * into an equisatisfiable conjunction of equations such that the left-hand
 * side of each equation is a variable which does not appear as an i-leaf of
 * the rhs, where i is the theory of the primary solver.  Any solution which
 * satisfies this is fine.  "Solvers" from other theories can do whatever they
 * want as long as we eventually reach this form.
 */
/*****************************************************************************/
Theorem TheoryCore::solve(const Theorem& eThm)
{
  const Expr& e = eThm.getExpr();
  TRACE("facts solve", "solve[Core](", e, ") {");
  Theorem thm;
  Expr e2;
  if (d_solver) {
    TRACE("facts solve", "solve["+d_solver->getName()+"](", e,") {");
    thm = d_solver->solve(eThm);
    TRACE("facts solve", "solve["+d_solver->getName()+"] => ", thm.getExpr(), " }");
    e2 = thm.getExpr();
    // FIXME: this stops other solvers from being run when arithmetic
    // solves into a system of equations.  This results in
    // INCOMPLETENESS.  In my opinion (Sergey), the correct fix is to
    // allow multiple independent solvers, just like rewriters.
    if (!e2.isEq() || theoryOf(e2) == d_solver) {
      TRACE("facts solve", "solve[Core](non-eq) => ", thm, " }");
      // setIncomplete("Not all solvers have been run (this is a bug)");
      return thm;
    }
  }
  else {
    thm = eThm;
    e2 = e;
  }
  Theory* i = theoryOf(e2);
  TRACE("facts solve", "solve["+i->getName()+"](", e2,") {");
  Theorem thm2 = i->solve(thm);
  TRACE("facts solve", "solve["+i->getName()+"] => ", thm2.getExpr(), " }");
  IF_DEBUG(
    // Check that the result is in solved form according to the primary solver
    if (d_solver) {
      e2 = thm2.getExpr();
      if(e2.isEq()) {
        Expr solved(d_solver->solve(thm2).getExpr());
        DebugAssert(solved == e2, "e2 = "+e2.toString()
                    +"\nsolved = "+solved.toString());
      }
      // FIXME: how do we check it for AND and EXISTS?
    }
    );
  TRACE("facts solve", "solve[Core] => ", thm2, " }");
  return thm2;
}


Theorem TheoryCore::typePred(const Expr& e) {
  return d_rules->typePred(e);
}


Theorem TheoryCore::subtypePredicate(const Expr& e) {
  TRACE("tccs", "subtypePredicate(", e, ") {");
  Theorem pred(e.lookupSubtypePred());
  if(pred.isNull()) {
    vector<Theorem> thms;
    thms.push_back(d_rules->typePred(e));
    TRACE("tccs", "subtypePredicate: typePred(e) = ", thms[0].getExpr(), "");
    for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
      thms.push_back(subtypePredicate(*i));
    pred = d_commonRules->andIntro(thms);
    pred = d_commonRules->rewriteAnd(pred);
    e.setSubtypePred(pred);
  }
  TRACE("tccs", "subtypePredicate => ", pred.getExpr(), " }");
  return pred;
}


IF_DEBUG(
void TheoryCore::dumpTrace(const Expr& e, const string& title) {
  vector<StrPair> fields;
  fields.push_back(strPair("op", d_em->getKindName(e.getKind())));
  fields.push_back(strPair("theory", theoryOf(e)->getName()));
  debugger.dumpTrace(title, fields);
}
)


void TheoryCore::setFindLiteral(const Theorem& thm, bool notifySAT) {
  const Expr& e = thm.getExpr();
  if (e.isNot()) {
    if (!e[0].hasFind()) {
      if(notifySAT) enqueueSE(thm);
      e[0].setFind(d_commonRules->notToIff(thm));
      d_em->invalidateSimpCache();
    }
  }
  else if (!e.hasFind()) {
    e.setFind(d_commonRules->iffTrue(thm));
    if(notifySAT) enqueueSE(thm);
    d_em->invalidateSimpCache();
  }
}


Theorem TheoryCore::rewriteIte(const Expr& e) {
  if (e[0].isTrue())
    return d_rules->rewriteIteTrue(e);
  if (e[0].isFalse())
    return d_rules->rewriteIteFalse(e);
  if (e[1] == e[2])
    return d_rules->rewriteIteSame(e);
  // This results in exponential blowup
//   if(!isTerm(e1) && !isTerm(e2))
//     return d_commonRules->rewriteIteBool(c, e1, e2);
  // Default case: no rewrite
  return reflexivityRule(e);
}


/* Recurse through s looking for atomic formulas (or terms in the case of
 * then/else branches of ite's) and use the notifylist mechanism to indicate
 * that the atomic formula e depends on these atomic formulas and terms.  Used
 * by registerAtom. */
void TheoryCore::setupSubFormulas(const Expr& s, const Expr& e)
{
  if (s.isAtomic()) {
    setupTerm(s, theoryOf(s));
    s.addToNotify(this, e);
    processFactQueue();
  }
  else if (s.isAbsAtomicFormula()) {
    setupTerm(s, theoryOf(s));
    for (int i = 0; i < s.arity(); ++i) {
      s[i].addToNotify(this, e);
    }
    s.addToNotify(this, e);
    processFactQueue();
  }
  else {
    for (int i = 0; i < s.arity(); ++i) {
      setupSubFormulas(s[i], e);
    }
  }
}


void TheoryCore::registerAtom(const Expr& e)
{
  // TODO: don't change state by calling this function
  DebugAssert(e.isAbsAtomicFormula(), "Expected atomic formula");
  IF_DEBUG(ScopeWatcher sw(&d_inRegisterAtom));
  Theorem thm = simplify(e);
  if (thm.getRHS().isTrue()) {
    if (e.isImpliedLiteral()) return;
    e.setImpliedLiteral();
    d_impliedLiterals.push_back(d_commonRules->iffTrueElim(thm));
  }
  else if (thm.getRHS().isFalse()) {
    Expr not_e = !e;
    if (not_e.isImpliedLiteral()) return;
    not_e.setImpliedLiteral();
    d_impliedLiterals.push_back(d_commonRules->iffFalseElim(thm));
  }
  else {
    setupSubFormulas(thm.getRHS(), e);
  }
}


Theorem TheoryCore::getImpliedLiteral(void)
{
  Theorem res;
  if (d_impliedLiteralsIdx < d_impliedLiterals.size()) {
    res = d_impliedLiterals[d_impliedLiteralsIdx];
    d_impliedLiteralsIdx = d_impliedLiteralsIdx + 1;
  }
  return res;
}


Theorem TheoryCore::getImpliedLiteralByIndex(unsigned index)
{
  DebugAssert(index < d_impliedLiterals.size(), "index out of bounds");
  return d_impliedLiterals[index];
}


void TheoryCore::assignValue(const Expr& t, const Expr& val) {
  DebugAssert(d_varAssignments.count(t) == 0
              || d_varAssignments[t].getRHS() == val,
              "TheoryCore::assignValue("+t.toString()+" := "+val.toString()
              +")\n variable already has a different value");
  // Check if the assignment theorem can be derived from the find of t
  Theorem thm(find(t));
  const Expr& t2 = thm.getRHS();

  if(t2!=val) {
    bool isBool(t2.getType().isBool());
    Expr assump = (isBool)? t2.iffExpr(val) : t2.eqExpr(val);
    Theorem assertThm = d_coreSatAPI->addAssumption(assump);
    addFact(assertThm);
    thm = transitivityRule(thm, assertThm);
  }
  d_varAssignments[t] = thm;
}


void TheoryCore::assignValue(const Theorem& thm) {
  DebugAssert(thm.isRewrite(), "TheoryCore::assignValue("+thm.toString()+")");
  const Expr& t = thm.getLHS();
  const Expr& val = thm.getRHS();
  DebugAssert(d_varAssignments.count(t) == 0
              || d_varAssignments[t].getRHS() == val,
              "TheoryCore::assignValue("+thm.getExpr().toString()
              +")\n variable already has a different value:\n "
              +d_varAssignments[t].getExpr().toString());
  d_varAssignments[t] = thm;
  // Check if the assignment theorem can be derived from the find of t
  Theorem findThm(find(t));
  const Expr& t2 = findThm.getRHS();

  if(t2!=val) {
    Theorem thm2 = transitivityRule(symmetryRule(findThm), thm);
    addFact(thm2);
  }
}


bool TheoryCore::getResource() {
  // Unlimited resource
  if(d_resourceLimit == 0) return true;
  // Resource is limited: check and consume it
  if(d_resourceLimit > 1) {
    d_resourceLimit--;
    return true;
  }
  else
    return false;
}


Theorem3 TheoryCore::queryTCC(const Theorem& phi, const Theorem& D_phi)
{
  return d_rules->queryTCC(phi, D_phi);
}


Theorem3 TheoryCore::implIntro3(const Theorem3& phi,
                                const std::vector<Expr>& assump,
                                const std::vector<Theorem>& tccs)
{
  return d_rules->implIntro3(phi, assump, tccs);
}

---