vcl.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file vcl.cpp
 * 
 * Author: Clark Barrett
 * 
 * Created: Tue Dec 31 18:27:11 2002
 *
 * <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 <fstream>
#include <iostream>
#include "vcl.h"
#include "context.h"
#include "parser.h"
#include "vc_cmd.h"
#include "search.h"
#include "search_simple.h"
#include "search_fast.h"
#include "theorem_manager.h"
#include "variable.h"
#include "theory_core.h"
#include "theory_uf.h"
#include "theory_arith.h"
#include "theory_bitvector.h"
#include "theory_array.h"
#include "theory_quant.h"
#include "theory_records.h"
#include "theory_simulate.h"
#include "theory_datatype.h"
#include "command_line_flags.h"
#include "typecheck_exception.h"
#include "eval_exception.h"
#include "debug.h"

using namespace std;
using namespace CVCL;

ValidityChecker* ValidityChecker::create(const CLFlags& flags)
{
  return new VCL(flags);
}


CLFlags ValidityChecker::createFlags() {
  CLFlags flags;
  // We expect the user to type cvcl -h to get help, which will set
  // the "help" flag to false; that's why it's initially true.

  // Overall system control flags
  flags.addFlag("timeout", CLFlag(0, "Kill cvcl process after given number of seconds (0==no limit)"));
  flags.addFlag("resource", CLFlag(0, "Set finite resource limit (0==no limit)"));
  flags.addFlag("mm", CLFlag("chunks", "Memory manager (chunks, malloc)"));
  // Information printing flags
  flags.addFlag("help",CLFlag(true, "print usage information and exit"));
  flags.addFlag("version",CLFlag(true, "print version information and exit"));
  flags.addFlag("quiet", CLFlag(true, "Be as quiet as possible"));
  flags.addFlag("interactive", CLFlag(false, "Interactive mode"));
  flags.addFlag("stats", CLFlag(false, "Print run-time statistics"));
  flags.addFlag("reorder", CLFlag(false, "Permute and get reordered "
                                  "CVC benchmark (ite should be on)"));
  flags.addFlag("seed", CLFlag(1, "Set the seed for random sequence"));
  flags.addFlag("pq", CLFlag(false, "Print query"));
  flags.addFlag("dump-log", CLFlag("", "Dump API call log in CVCL input "
                                   "format to given file "
                                   "(off when file name is \"\")"));
  flags.addFlag("translate", CLFlag(false, "Produce a complete translation from "
                                           "the input language to output language.  "
                                           "Requires dump-log."));
  flags.addFlag("real2int", CLFlag(false, "When translating, convert reals to integers."));

  // Parser related flags
  flags.addFlag("old-func-syntax",CLFlag(false, "Enable parsing of old-style function syntax"));

  // Pretty-printing related flags
  flags.addFlag("dagify-exprs",
                CLFlag(true, "Print expressions with sharing as DAGs"));
  flags.addFlag("lang", CLFlag("pres", "Input language "
                               "(presentation, smtlib, internal)"));
  flags.addFlag("output-lang", CLFlag("", "Output language "
                                      "(presentation, smtlib, internal, lisp)"));
  flags.addFlag("indent", CLFlag(true, "Print expressions with indentation"));
  flags.addFlag("width", CLFlag(80, "Suggested line width for printing"));
  flags.addFlag("print-depth", CLFlag(-1, "Max. depth to print expressions "));
  flags.addFlag("print-assump", CLFlag(false, "Print assumptions in Theorems "));

  // Search Engine (SAT) related flags
  flags.addFlag("sat",CLFlag("fast", "choose a SAT solver to use "
                             "(fast, simple)"));
  flags.addFlag("de",CLFlag("dfs", "choose a decision engine to use "
                            "(dfs, caching, mbtf)"));
  flags.addFlag("dfs", CLFlag(false, "Use simple DFS splitter heuristic"));
  flags.addFlag("clauses", CLFlag(true, "Build conflict clauses"));
  flags.addFlag("max-clauses",
                CLFlag(100000, "Max. number of conflict clauses (for +sat)"));
  flags.addFlag("berkmin", CLFlag(false, "Use BerkMin splitter heuristic"));
  flags.addFlag("track-literals", CLFlag(false, "Keep a list of literals asserted internally since last user assertion"));

  // Proofs and Assumptions
  flags.addFlag("proofs", CLFlag(false, "Produce proofs (also sets +assump)"));
  flags.addFlag("check-proofs",
                CLFlag(IF_DEBUG(true ||) false, "Check proofs on-the-fly"));
  flags.addFlag("assump", CLFlag(true, "Track assumptions"));

  // Core framework switches
  flags.addFlag("tcc", CLFlag(true, "Check TCCs for each ASSERT and QUERY"));
  flags.addFlag("cnf", CLFlag(false, "Convert top-level Boolean formulas to CNF"));
  flags.addFlag("ignore-cnf-vars", CLFlag(false, "Do not split on aux. CNF vars (with +cnf)"));
  flags.addFlag("orig-formula", CLFlag(false, "Preserve the original formula with +cnf (for splitter heuristics)"));
  flags.addFlag("iflift", CLFlag(false, "Translate if-then-else terms to CNF (with +cnf)"));
  flags.addFlag("circuit", CLFlag(false, "With +cnf, use circuit propagation"));
  flags.addFlag("un-ite-ify", CLFlag(false, "Unconvert ITE expressions"));
  flags.addFlag("ip", CLFlag(false, "Simplify \"in place\""));
  flags.addFlag("ite", CLFlag(false,
                              "Convert to ITE expression in preprocess"));
  flags.addFlag("pp", CLFlag(false, "Use ITE-simplifier in "
                             "preprocess (with +ite)"));
  flags.addFlag("diseq", CLFlag(false, "Exploit structural similarity "
                                "in disequalities"));
  // Concrete model generation (counterexamples) flags
  flags.addFlag("applications", CLFlag(true, "Add relevant function applications and array accesses to the concrete counterexample"));
  // Debugging flags (only for the debug build)
  // #ifdef DEBUG
  vector<pair<string,bool> > sv;
  flags.addFlag("trace", CLFlag(sv, "Tracing.  Multiple flags add up."));
  flags.addFlag("dump-trace", CLFlag("", "Dump debugging trace to "
                                   "given file (off when file name is \"\")"));
  // #endif
  // DP-specific flags

  // Arithmetic
  flags.addFlag("var-order",
                CLFlag(false, "Use simple variable order in arith"));
  flags.addFlag("ineq-delay", CLFlag(10, "Accumulate this many inequalities "
                                     "before processing"));

  // Quantifiers
  flags.addFlag("max-quant-inst", CLFlag(100, "The maximum number of"
                                " quantifier instantiations processed"));

  //Bitvectors
  flags.addFlag("bv-simplify",
                CLFlag(false, "Simplify bitvector facts"));
  flags.addFlag("boolean-rewrite",
                CLFlag(true, "Rewrite booleans on the fly"));
  flags.addFlag("use-boolextract-cache",
                CLFlag(false, "Use cache to construct boolextract exprs"));
  flags.addFlag("bv-rewrite",
                CLFlag(true, "Rewrite bitvector expressions"));
  flags.addFlag("bv-concatnormal-rewrite",
                CLFlag(true, "Concat Normal Form rewrites"));
  flags.addFlag("bv-plusnormal-rewrite",
                CLFlag(true, "Bvplus Normal Form rewrites"));
  flags.addFlag("bv-rw-bitblast",
                CLFlag(false, "Rewrite while bit-blasting"));
  flags.addFlag("bv-cnf-bitblast", 
                CLFlag(true,"Bitblast equalities in CNFconverter with +cnf"));
  flags.addFlag("bv-update",
                CLFlag(true,"Update bitvectors on find pointer changes"));
  flags.addFlag("bv-setup",
                CLFlag(true,"Setup bitvectors for single bit changes"));
  flags.addFlag("bv-shared-setup",
                CLFlag(true,"Setup only subterms of shared terms"));
  flags.addFlag("bv-assert",
                CLFlag(true,"Assert bits corresponding to BOOL_EXTRACT(t,i)"));
  flags.addFlag("bv-delay-eq",
                CLFlag(true, "Queue up equalities"));
  flags.addFlag("bv-bit-eq",
                CLFlag(false, "Expand equalities into 1-bit equalities"));
  flags.addFlag("bv-delay-diseq",
                CLFlag(true, "Queue up disequalities"));
  flags.addFlag("bv-delay-typepred",
                CLFlag(true,"Delay bitvector type predicates"));
  flags.addFlag("bv-nl-remove1",
                CLFlag(true,"BV DP: Remove updated canonical rep from NotifyList"));
  flags.addFlag("bv-nl-remove2",
                CLFlag(true,"BV DP: Remove updated bit expansion from NotifyList"));
  flags.addFlag("bv-lhs-minus-rhs", 
                CLFlag(false,"Do lhs-rhs=0 if both lhs/rhs are BVPLUS"));

  

  // Uninterpreted Functions
  flags.addFlag("trans-closure",
                CLFlag(false,"enables transitive closure of binary relations"));
  return flags;
}


ValidityChecker* ValidityChecker::create()
{
  return new VCL(createFlags());
}


size_t VCL::UserAssertion::s_nextIdx = 0;


//! Recursive assumption graph traversal to find user assumptions
/*!
 *  If an assumption has a TCC, traverse the proof of TCC and add its
 *  assumptions to the set recursively.
 */
void VCL::getAssumptionsRec(const Theorem& thm,
                            set<UserAssertion>& assumptions,
                            bool addTCCs) {
  if(thm.isFlagged()) return;
  thm.setFlag();
  if(thm.isAxiom()) {
    if(d_userAssertions->count(thm.getExpr())>0) {
      const UserAssertion& a = (*d_userAssertions)[thm.getExpr()];
      assumptions.insert(a);
      if(addTCCs) {
        DebugAssert(!a.tcc().isNull(), "getAssumptionsRec(a="
                    +a.thm().toString()+", thm = "+thm.toString()+")");
        getAssumptionsRec(a.tcc(), assumptions, true);
      }
    } else { // it's a splitter
      UserAssertion a(thm, Theorem());
      assumptions.insert(a);
    }
  }
  else {
    Assumptions a(thm.getAssumptions());
    for(Assumptions::iterator i=a.begin(), iend=a.end(); i!=iend; ++i)
      getAssumptionsRec(*i, assumptions, addTCCs);
  }
}


void VCL::getAssumptions(const Assumptions& a, vector<Expr>& assumptions)
{
  set<UserAssertion> assumpSet;
  if(a.isNull()) return;
  Assumptions::iterator i=a.begin(), iend=a.end();
  if(i!=iend) i->clearAllFlags();
  for(; i!=iend; ++i)
    getAssumptionsRec(*i, assumpSet, getFlags()["tcc"].getBool());
  // Order assumptions by their creation time
  for(set<UserAssertion>::iterator i=assumpSet.begin(), iend=assumpSet.end();
      i!=iend; ++i)
    assumptions.push_back(i->thm().getExpr());
}


Theorem3 VCL::deriveClosure(const Theorem3& thm) {
  vector<Expr> assump;
  set<UserAssertion> assumpSet;
  // Compute the vector of assumptions for thm, and iteratively move
  // the assumptions to the RHS until done.  Each closure step may
  // introduce new assumptions from the proofs of TCCs, so those need
  // to be dealt with in the same way, until no assumptions remain.
  Theorem3 res = thm;
  Assumptions a(res.getAssumptions());
  while(!a.empty()) {
    assump.clear();
    assumpSet.clear();
    Assumptions::iterator i=a.begin(), iend=a.end();
    if(i!=iend) i->clearAllFlags();
    // Collect the assumptions of 'res' *without* TCCs
    for(; i!=iend; ++i)
      getAssumptionsRec(*i, assumpSet, false);

    // Build the vectors of assumptions and TCCs
    vector<Theorem> tccs;
    if(getFlags()["tcc"].getBool()) {
      for(set<UserAssertion>::iterator i=assumpSet.begin(),
            iend=assumpSet.end(); i!=iend; ++i) {
        assump.push_back(i->thm().getExpr());
        tccs.push_back(i->tcc());
      }
    }
    // Derive the closure
    res = d_theoryCore->implIntro3(res, assump, tccs);
    a = res.getAssumptions();
  }
  return res;
}


static string fileToSMTLIBIdentifier(const string& filename)
{
  string tmpName;
  string::size_type pos = filename.rfind("/");
  if (pos == string::npos) {
    tmpName = filename;
  }
  else {
    tmpName = filename.substr(pos+1);
  }
  char c = tmpName[0];
  string res;
  if ((c < 'A' || c > 'Z') && (c < 'a' || c > 'z')) {
    res = "B_";
  }
  for (unsigned i = 0; i < tmpName.length(); ++i) {
    c = tmpName[i];
    if ((c < 'A' || c > 'Z') && (c < 'a' || c > 'z') &&
        (c < '0' || c > '9') && (c != '.' && c != '_')) {
      c = '_';
    }
    res += c;
  }
  return res;
}


VCL::VCL(const CLFlags& flags): d_flags(new CLFlags(flags)) // , d_cnf(NULL)
{
  // Set the dependent flags so that they are consistent

  // If proofs are enabled, then enable assumptions too
  if((*d_flags)["proofs"].getBool()) d_flags->setFlag("assump", true);
  // The default SAT solver must always be run with assump enabled
  if((*d_flags)["sat"].getString() != "simple")
    d_flags->setFlag("assump", true);

  d_cm = new ContextManager();
  // Initialize the database of user assertions.  It has to be
  // initialized after d_cm.
  d_userAssertions = new CDMap<Expr,UserAssertion>(getCurrentContext());

  d_tm = new TheoremManager(this, (*d_flags)["proofs"].getBool(),
                            (*d_flags)["assump"].getBool());

  // ExprManager uses Theorem class, so it has to be created after
  // TheoremManager is ready, and deleted before.
  d_em = new ExprManager(d_cm, *d_flags);

  // Initialize TheoremManager
  d_tm->init();

  d_theoryCore = new TheoryCore(this);
  d_theories.push_back(d_theoryCore);

  // Fast rewriting of literals is done by setting their find to true or false.
  falseExpr().setFind(d_theoryCore->reflexivityRule(falseExpr()));
  trueExpr().setFind(d_theoryCore->reflexivityRule(trueExpr()));

  // Must be created after TheoryCore, since it needs it.
  // When we have more than one search engine, select one to create
  // based on flags
  if ((*d_flags)["sat"].getString() == "simple")
    d_se = new SearchSimple(this); 
//   else if ((*d_flags)["sat"].getString() == "default")
//     d_se = new SearchEngineDefault(this);
  else if ((*d_flags)["sat"].getString() == "fast")
    d_se = new SearchEngineFast(this);
  else
    ASSERT_FATAL(false, "Unrecognized SAT solver name: "
                 +(*d_flags)["sat"].getString());

  d_theories.push_back(d_theoryUF = new TheoryUF(this));
  d_theories.push_back(d_theoryArith = new TheoryArith(this));
  d_theories.push_back(d_theoryArray = new TheoryArray(this));
  d_theories.push_back(d_theoryQuant = new TheoryQuant(this));
  d_theories.push_back(d_theoryRecords = new TheoryRecords(this));
  d_theories.push_back(d_theorySimulate = new TheorySimulate(this));
  d_theories.push_back(d_theoryBitvector = new TheoryBitvector(this));
  d_theories.push_back(d_theoryDatatype = new TheoryDatatype(this));

  // Initial scope level should be 1
  d_cm->push();
  d_translate = (*d_flags)["translate"].getBool();
  const string& dumpFile = (*d_flags)["dump-log"].getString();
  if (dumpFile == "") {
    DebugAssert(!d_translate,"Cannot translate without dump file");
    d_translate = false;
  }
  else {
    if (d_translate && d_em->getOutputLang() == SMTLIB_LANG) {
      d_osdump.open(".cvcl__smtlib_temporary_file");
      if(!d_osdump)
        cerr << "*** Warning: cannot open temporary file .cvcl__smtlib_temporary_file"
             << dumpFile << endl;
      d_osdumpTranslate.open(dumpFile.c_str());
      if(!d_osdumpTranslate)
        cerr << "*** Warning: cannot open a log file: " << dumpFile << endl;
      d_osdumpTranslate <<
        "(benchmark " << fileToSMTLIBIdentifier(dumpFile) << endl <<
        "  :source {" << endl;
      string tmpName;
      string::size_type pos = dumpFile.rfind("/");
      if (pos == string::npos) {
        tmpName = "README";
      }
      else {
        tmpName = dumpFile.substr(0,pos+1) + "README";
      }
      d_tmpFile.open(tmpName.c_str());
      char c;
      if (d_tmpFile.is_open()) {
        d_tmpFile.get(c);
        while (!d_tmpFile.eof()) {
          if (c == '{' || c == '}') d_osdumpTranslate << '\\';
          d_osdumpTranslate << c;
          d_tmpFile.get(c);
        }
        d_tmpFile.close();
      }
      else {
        d_osdumpTranslate << "Source unknown";
      }
      d_osdumpTranslate << endl <<
        "This benchmark was automatically translated into SMT-LIB format from" << endl <<
        "CVC format using CVC Lite" << endl << "}" << endl;
    }
    else {
      d_osdump.open(dumpFile.c_str());
      if(!d_osdump)
        cerr << "*** Warning: cannot open a log file: " << dumpFile << endl;
    }
  }

  setResourceLimit((*d_flags)["resource"].getInt());

//   if ((*d_flags)["cnf"].getBool())
//     d_cnf = new CNF(this);
}


VCL::~VCL()
{
//   delete d_cnf;
  if (d_osdump) {
    if (d_translate && d_em->getOutputLang() == SMTLIB_LANG) {
      d_osdumpTranslate << "  :logic ";
      if (d_theoryRecords->theoryUsed() ||
          d_theorySimulate->theoryUsed() ||
          d_theoryBitvector->theoryUsed() ||
          d_theoryDatatype->theoryUsed()) {
        d_osdumpTranslate << "unknown";
      }
      else {
        if (d_theoryArith->theoryUsed() &&
            (d_theoryArith->getLangUsed() == NONLINEAR ||
            (d_theoryArith->realUsed() &&
             d_theoryArith->intUsed()))) {
          d_osdumpTranslate << "unknown";
        }
        else {
          if (!d_theoryQuant->theoryUsed()) {
            d_osdumpTranslate << "QF_";
          }
          if (d_theoryArray->theoryUsed()) {
            if (d_theoryArith->theoryUsed()) {
              if (d_theoryArith->realUsed()) {
                d_osdumpTranslate << "AUFLRA";
              }
              else {
                d_osdumpTranslate << "AUFLIA";
              }
            }
            else {
              d_osdumpTranslate << "AUFLIA";
            }
          }
          else if (d_theoryUF->theoryUsed()) {
            if (d_theoryArith->theoryUsed()) {
              if (d_theoryArith->realUsed()) {
                if (d_theoryArith->getLangUsed() <= DIFF_ONLY) {
                  d_osdumpTranslate << "UFRDL";
                }
                else {
                  d_osdumpTranslate << "UFLRA";
                }
              }                  
              else {
                if (d_theoryArith->getLangUsed() <= DIFF_ONLY) {
                  d_osdumpTranslate << "UFIDL";
                }
                else {
                  d_osdumpTranslate << "UFLIA";
                }
              }
            }
            else {
              d_osdumpTranslate << "UF";
            }
          }
          else if (d_theoryArith->theoryUsed()) {
            if (d_theoryArith->realUsed()) {
              if (d_theoryArith->getLangUsed() == DIFF_ONLY) {
                d_osdumpTranslate << "RDL";
              }
              else {
                d_osdumpTranslate << "LRA";
              }
            }
            else {
              if (d_theoryArith->getLangUsed() == DIFF_ONLY) {
                d_osdumpTranslate << "IDL";
              }
              else {
                d_osdumpTranslate << "LIA";
              }
            }
          }
          else {
            d_osdumpTranslate << "UF";
          }
        }
      }
      d_osdumpTranslate << endl;
      d_osdump.close();
      d_tmpFile.clear();
      d_tmpFile.open(".cvcl__smtlib_temporary_file");
      if (d_tmpFile.is_open()) {
        char c;
        d_tmpFile.get(c);
        while (!d_tmpFile.eof()) {
          d_osdumpTranslate << c;
          d_tmpFile.get(c);
        }
        d_tmpFile.close();
      }
      d_osdumpTranslate << ")" << endl;
    }
    d_osdumpTranslate.close();
  }

  for(size_t i=0; i<d_theories.size(); ++i) {
    string name(d_theories[i]->getName());
    TRACE("delete", "Deleting Theory[", name, "] {");
    delete d_theories[i];
    TRACE("delete", "Finished deleting Theory[", name, "] }");
  }
  TRACE_MSG("delete", "Deleting SearchEngine {");
  delete d_se;
  TRACE_MSG("delete", "Finished deleting SearchEngine }");
  // This map contains expressions and theorems; delete it before
  // d_em, d_tm, and d_cm.
  TRACE_MSG("delete", "Deleting d_userAssertions {");
  delete d_userAssertions;
  TRACE_MSG("delete", "Finished deleting d_userAssertions }");
  // and set these to null so their destructors don't blow up
  d_lastQuery = Theorem3();
  d_lastQueryTCC = Theorem();
  d_lastClosure = Theorem3();
  TRACE_MSG("delete", "Deleting d_vars {");
  d_vars.clear();
  TRACE_MSG("delete", "Finished deleting d_vars }");
  // Delete ExprManager BEFORE TheoremManager, since Exprs use Theorems
  TRACE_MSG("delete", "Clearing d_em {");
  d_em->clear();
  d_tm->clear();
  TRACE_MSG("delete", "Finished clearing d_em }");
  TRACE_MSG("delete", "Deleting d_cm {");
  delete d_cm;
  TRACE_MSG("delete", "Finished deleting d_cm }");
  TRACE_MSG("delete", "Deleting d_em {");
  delete d_em;
  TRACE_MSG("delete", "Finished deleting d_em }");
  // TheoremManager does not call ~Theorem() destructors, and only
  // releases memory.  At worst, we'll lose some Assumptions.
  TRACE_MSG("delete", "Deleting d_tm {");
  delete d_tm;
  TRACE_MSG("delete", "Finished deleting d_tm }");
  TRACE_MSG("delete", "Deleting d_flags [end of ~VCL()]");
  delete d_flags;
  // No more TRACE-ing after this point (it needs d_flags)
}


Type VCL::boolType(){
  return d_theoryCore->boolType();
}


Type VCL::realType()
{
  return d_theoryArith->realType();
}


Type VCL::intType() {
  return d_theoryArith->intType();
}


Type VCL::subrangeType(const Expr& l, const Expr& r) {
  return d_theoryArith->subrangeType(l, r);
}

Type VCL::subtypeType(const Expr& pred) {
  Type predTp(getType(pred));
  if(!predTp.isFunction())
    throw TypecheckException
      ("Non-function type in the predicate subtype:\n\n  "
       +predTp.toString()
       +"\n\nThe predicate is:\n\n  "
       +pred.toString());
  if(!predTp[1].isBool())
    throw TypecheckException
      ("Range is not BOOLEAN in the predicate subtype:\n\n  "
       +predTp.toString()
       +"\n\nThe predicate is:\n\n  "
       +pred.toString());
  // Eliminate CONSTDEF, if the predicate is a user-defined symbol
  Expr p(simplify(pred));
  // Make sure that the supplied predicate is total: construct 
  // 
  //    FORALL (x: domType): getTCC(pred(x))
  //
  // This only needs to be done for LAMBDA-expressions, since
  // uninterpreted predicates are defined for all the arguments
  // of correct (exact) types.
  if(p.isLambda()) {
    Expr quant(forallExpr(p.getVars(), d_theoryCore->getTCC(p.getBody())));
      int scope = scopeLevel();
      d_cm->push();
      if(!query(quant, true)) {
        throw TypecheckException
          ("Subtype predicate is not total in the following type:\n\n  "
           +newExpr(getEM(), SUBTYPE, p).toString()
           +"\n\nThe failed TCC is:\n\n  "
           +quant.toString());
      }
      d_cm->popto(scope);
  }
  return Type(newExpr(getEM(), SUBTYPE, p));
}


Type VCL::tupleType(const Type& type0, const Type& type1)
{
  vector<Type> types;
  types.push_back(type0);
  types.push_back(type1);
  return d_theoryRecords->tupleType(types);
}


Type VCL::tupleType(const Type& type0, const Type& type1, const Type& type2)
{
  vector<Type> types;
  types.push_back(type0);
  types.push_back(type1);
  types.push_back(type2);
  return d_theoryRecords->tupleType(types);
}


Type VCL::tupleType(const vector<Type>& types)
{
  return d_theoryRecords->tupleType(types);
}


//! Comparison of string/Expr pairs for sorting
template<class T>
class StrPairLess {
public:
  bool operator()(const pair<string,T>& p1,
                  const pair<string,T>& p2) const {
    return p1.first < p2.first;
  }
};

template<class T>
static pair<string,T> strPair(const string& f, const T& t) {
  return pair<string,T>(f, t);
}

//! Sort two vectors based on the first vector
template<class T>
static void sort2(vector<string>& keys, vector<T>& vals) {
  DebugAssert(keys.size()==vals.size(), "VCL::sort2()");
  // Create vector of pairs
  vector<pair<string,T> > pairs;
  for(size_t i=0, iend=keys.size(); i<iend; ++i)
    pairs.push_back(strPair(keys[i], vals[i]));
  // Sort pairs
  StrPairLess<T> comp;
  sort(pairs.begin(), pairs.end(), comp);
  DebugAssert(pairs.size() == keys.size(), "VCL::sort2()");
  // Split the pairs back into the original vectors
  for(size_t i=0, iend=pairs.size(); i<iend; ++i) {
    keys[i] = pairs[i].first;
    vals[i] = pairs[i].second;
  }
}

Type VCL::recordType(const string& field, const Type& type)
{
  vector<string> fields;
  vector<Type> kids;
  fields.push_back(field);
  kids.push_back(type);
  return Type(d_theoryRecords->recordType(fields, kids));
}


Type VCL::recordType(const string& field0, const Type& type0,
                     const string& field1, const Type& type1) {
  vector<string> fields;
  vector<Type> kids;
  fields.push_back(field0);
  fields.push_back(field1);
  kids.push_back(type0);
  kids.push_back(type1);
  sort2(fields, kids);
  return Type(d_theoryRecords->recordType(fields, kids));
}


Type VCL::recordType(const string& field0, const Type& type0,
                     const string& field1, const Type& type1,
                     const string& field2, const Type& type2)
{
  vector<string> fields;
  vector<Type> kids;
  fields.push_back(field0);
  fields.push_back(field1);
  fields.push_back(field2);
  kids.push_back(type0);
  kids.push_back(type1);
  kids.push_back(type2);
  sort2(fields, kids);
  return Type(d_theoryRecords->recordType(fields, kids));
}

Type VCL::recordType(const vector<string>& fields,
                     const vector<Type>& types)
{
  DebugAssert(fields.size() == types.size(),
              "VCL::recordType: number of fields is different \n"
              "from the number of types");
  // Create copies of the vectors to sort them
  vector<string> fs(fields);
  vector<Type> ts(types);
  sort2(fs, ts);
  return Type(d_theoryRecords->recordType(fs, ts));
}


Type VCL::dataType(const string& constructor,
                   const vector<string>& selectors, const vector<Type>& types)
{
  vector<string> constructors;
  constructors.push_back(constructor);

  vector<vector<string> > selectorsVec;
  selectorsVec.push_back(selectors);

  vector<vector<Type> > typesVec;
  typesVec.push_back(types);

  return dataType(constructors, selectorsVec, typesVec);
}


Type VCL::dataType(const vector<string>& constructors,
                   const vector<vector<string> >& selectors,
                   const vector<vector<Type> >& types)
{
  return d_theoryDatatype->dataType(constructors, selectors, types);
}


Type VCL::arrayType(const Type& typeIndex, const Type& typeData)
{
  return ::arrayType(typeIndex, typeData);
}


Type VCL::funType(const Type& typeDom, const Type& typeRan)
{
  return typeDom.funType(typeRan);
}


Type VCL::funType(const std::vector<Type>& typeDom, const Type& typeRan) {
  DebugAssert(typeDom.size() >= 1, "VCL::funType: missing domain types");
  return ::funType(typeDom, typeRan);
}


Type VCL::createType(const string& typeName)
{
  if(d_osdump) {
    d_osdump << newExpr(d_em, TYPE, listExpr(idExpr(typeName))) << endl;
  }
  return d_theoryCore->newTypeExpr(typeName);
}


Type VCL::createType(const std::string& typeName, const Type& def)
{
  if(d_osdump && !d_translate) {
    d_osdump << newExpr(d_em, TYPE, idExpr(typeName), def.getExpr())
             << endl;
  }
  return d_theoryCore->newTypeExpr(typeName, def);
}


Type VCL::lookupType(const std::string& typeName)
{
  // TODO: check if it already exists
  return d_theoryCore->newTypeExpr(typeName);
}


Expr VCL::varExpr(const string& name, const Type& type)
{
  // Check if the ofstream is open (as opposed to the command line flag)
  if(d_osdump) {
    d_osdump << newExpr(d_em, CONST, idExpr(name), type.getExpr())
             << endl;
  }
  return d_theoryCore->newVar(name, type);
}


Expr VCL::varExpr(const string& name, const Type& type, const Expr& def)
{
  // Check if the ofstream is open (as opposed to the command line flag)
  if(d_osdump && !d_translate) {
    d_osdump << newExpr(d_em, CONST, idExpr(name), type.getExpr(), def)
             << endl;
  }
  // Prove the TCCs of the definition
  if(getFlags()["tcc"].getBool()) {
    Type tpDef(getType(def)), tpVar(type);
    // Make sure that tpDef is a subtype of tpVar; that is, prove
    // FORALL (x: tpDef): typePred(tpVar)(x)
    if(tpDef != tpVar) {
      // Typecheck the base types
      if(getBaseType(tpDef) != getBaseType(type)) {
        throw TypecheckException("Type mismatch in constant definition:\n"
                                 "Constant "+name+
                                 " is declared with type:\n  "
                                 +type.toString()
                                 +"\nBut the type of definition is\n  "
                                 +tpDef.toString());
      }
      TRACE("tccs", "CONSTDEF: "+name+" : "+tpVar.toString()
            +" := <value> : ", tpDef, ";");
      vector<Expr> boundVars;
      boundVars.push_back(boundVarExpr(name, "tcc", tpDef));
      Expr body(getTypePred(tpVar, boundVars[0]));
      Expr quant(forallExpr(boundVars, body));
      // Query the subtyping formula
      push();
      if(!query(quant, true)) {
        throw TypecheckException
          ("Type mismatch in constant definition:\n"
           "Constant "+name+
           " is declared with type:\n  "
           +type.toString()
           +"\nBut the type of definition is\n  "
           +getType(def).toString()
           +"\n\n which is not a subtype of the constant");
      }
      pop();
    }
  }
  return d_theoryCore->newVar(name, type, def);
}


Expr VCL::boundVarExpr(const string& name, const string& uid, 
                       const Type& type) {
  return d_theoryCore->newBoundVar(name, uid, type);
}


Expr VCL::lookupVar(const string& name, Type* type)
{
  return d_theoryCore->lookupVar(name, type);
}


Type VCL::getType(const Expr& e)
{
  return d_theoryCore->getType(e);
}

Expr VCL::getTypePred(const Type&t, const Expr& e)
{
  return d_theoryCore->getTypePred(t, e);
}


Type VCL::getBaseType(const Expr& e)
{
  return d_theoryCore->getBaseType(e);
}


Type VCL::getBaseType(const Type& t)
{
  return d_theoryCore->getBaseType(t);
}


Expr VCL::importExpr(const Expr& e)
{
  return d_em->rebuildExpr(e);
}


Type VCL::importType(const Type& t)
{
  return Type(d_em->rebuildExpr(t.getExpr()));
}


Expr VCL::eqExpr(const Expr& child0, const Expr& child1)
{
  return child0.eqExpr(child1);
}


Expr VCL::trueExpr()
{
  return d_em->trueExpr();
}


Expr VCL::falseExpr()
{
  return d_em->falseExpr();
}


Expr VCL::notExpr(const Expr& child)
{
  return !child;
}


Expr VCL::andExpr(const Expr& left, const Expr& right)
{
  return left && right;
}


Expr VCL::andExpr(const vector<Expr>& children)
{
  DebugAssert(children.size() > 0, "VCL::andExpr()");
  return Expr(getEM(), AND, children);
}


Expr VCL::orExpr(const Expr& left, const Expr& right)
{
  return left || right;
}


Expr VCL::orExpr(const vector<Expr>& children)
{
  DebugAssert(children.size() > 0, "VCL::orExpr()");
  return Expr(getEM(), OR, children);
}


Expr VCL::impliesExpr(const Expr& hyp, const Expr& conc)
{
  return hyp.impExpr(conc);
}


Expr VCL::iffExpr(const Expr& left, const Expr& right)
{
  return left.iffExpr(right);
}


Expr VCL::iteExpr(const Expr& ifpart, const Expr& thenpart, const Expr& elsepart)
{
  return ifpart.iteExpr(thenpart, elsepart);
}


Expr VCL::ratExpr(int n, int d)
{
  DebugAssert(d != 0,"denominator cannot be 0");
  return newRatExpr(d_em, Rational(n,d));
}


Expr VCL::ratExpr(const string& n, const string& d, int base)
{
  return newRatExpr(d_em, Rational(n.c_str(), d.c_str(), base));
}

Expr VCL::ratExpr(const string& n, int base)
{
  return newRatExpr(d_em, Rational(n.c_str(), base));
}


Expr VCL::uminusExpr(const Expr& child)
{
  return -child;
}


Expr VCL::plusExpr(const Expr& left, const Expr& right)
{
  return left + right;
}


Expr VCL::minusExpr(const Expr& left, const Expr& right)
{
  return left - right;
}


Expr VCL::multExpr(const Expr& left, const Expr& right)
{
  return left * right;
}


Expr VCL::powExpr(const Expr& x, const Expr& n)
{
  return ::powExpr(n, x);
}

Expr VCL::divideExpr(const Expr& num, const Expr& denom)
{
  return ::divideExpr(num,denom);
}


Expr VCL::ltExpr(const Expr& left, const Expr& right)
{
  return ::ltExpr(left, right);
}


Expr VCL::leExpr(const Expr& left, const Expr& right)
{
  return ::leExpr(left, right);
}


Expr VCL::gtExpr(const Expr& left, const Expr& right)
{
  return ::gtExpr(left, right);
}


Expr VCL::geExpr(const Expr& left, const Expr& right)
{
  return ::geExpr(left, right);
}


Expr VCL::recordExpr(const string& field, const Expr& expr)
{
  vector<string> fields;
  vector<Expr> kids;
  kids.push_back(expr);
  fields.push_back(field);
  return d_theoryRecords->recordExpr(fields, kids);
}


Expr VCL::recordExpr(const string& field0, const Expr& expr0,
                     const string& field1, const Expr& expr1)
{
  vector<string> fields;
  vector<Expr> kids;
  fields.push_back(field0);
  fields.push_back(field1);
  kids.push_back(expr0);
  kids.push_back(expr1);
  sort2(fields, kids);
  return d_theoryRecords->recordExpr(fields, kids);
}


Expr VCL::recordExpr(const string& field0, const Expr& expr0,
                     const string& field1, const Expr& expr1,
                     const string& field2, const Expr& expr2)
{
  vector<string> fields;
  vector<Expr> kids;
  fields.push_back(field0);
  fields.push_back(field1);
  fields.push_back(field2);
  kids.push_back(expr0);
  kids.push_back(expr1);
  kids.push_back(expr2);
  sort2(fields, kids);
  return d_theoryRecords->recordExpr(fields, kids);
}


Expr VCL::recordExpr(const vector<string>& fields,
                     const vector<Expr>& exprs)
{
  DebugAssert(fields.size() > 0, "VCL::recordExpr()");
  DebugAssert(fields.size() == exprs.size(),"VCL::recordExpr()");
  // Create copies of the vectors to sort them
  vector<string> fs(fields);
  vector<Expr> es(exprs);
  sort2(fs, es);
  return d_theoryRecords->recordExpr(fs, es);
}


Expr VCL::recSelectExpr(const Expr& record, const string& field)
{
  return d_theoryRecords->recordSelect(record, field);
}


Expr VCL::recUpdateExpr(const Expr& record, const string& field,
                        const Expr& newValue)
{
  return d_theoryRecords->recordUpdate(record, field, newValue);
}


Expr VCL::readExpr(const Expr& array, const Expr& index)
{
  return read(array, index);
}


Expr VCL::writeExpr(const Expr& array, const Expr& index, const Expr& newValue)
{
  return write(array, index, newValue);
}


Expr VCL::tupleExpr(const std::vector<Expr>& exprs) {
  DebugAssert(exprs.size() > 0, "VCL::tupleExpr()");
  return d_theoryRecords->tupleExpr(exprs);
}


Expr VCL::tupleSelectExpr(const Expr& tuple, int index)
{
  return d_theoryRecords->tupleSelect(tuple, index);
}


Expr VCL::tupleUpdateExpr(const Expr& tuple, int index, const Expr& newValue)
{
  return d_theoryRecords->tupleUpdate(tuple, index, newValue);
}


Expr VCL::datatypeConsExpr(const string& constructor, const vector<Expr>& args)
{
  return d_theoryDatatype->datatypeConsExpr(constructor, args);
}


Expr VCL::datatypeSelExpr(const string& selector, const Expr& arg)
{
  return d_theoryDatatype->datatypeSelExpr(selector, arg);
}


Expr VCL::forallExpr(const std::vector<Expr>& vars, const Expr& body) {
  DebugAssert(vars.size() > 0, "VCL::andExpr()");
  return newClosureExpr(d_em, FORALL, vars, body);
}


Expr VCL::existsExpr(const std::vector<Expr>& vars, const Expr& body) {
  return newClosureExpr(d_em, EXISTS, vars, body);
}


Expr VCL::lambdaExpr(const std::vector<Expr>& vars, const Expr& body) {
  return newClosureExpr(d_em, LAMBDA, vars, body);
}


Expr VCL::simulateExpr(const Expr& f, const Expr& s0,
                       const std::vector<Expr>& inputs, const Expr& n) {
  vector<Expr> kids;
  kids.push_back(f);
  kids.push_back(s0);
  kids.insert(kids.end(), inputs.begin(), inputs.end());
  kids.push_back(n);
  return newExpr(getEM(), SIMULATE, kids);
}


Op VCL::createOp(const string& name, const Type& type)
{
  // Check if the ofstream is open (as opposed to the command line flag)
  if(d_osdump) {
    d_osdump << newExpr(d_em, CONST, idExpr(name), type.getExpr())
             << endl;
  }
  return d_theoryCore->newFunction(name, type);
}


Op VCL::createOp(const string& name, const Type& type, const Expr& def)
{
  // Check if the ofstream is open (as opposed to the command line flag)
  if(d_osdump) {
    d_osdump << newExpr(d_em, CONST, idExpr(name), type.getExpr(), def)
             << endl;
  }
  // Prove the TCCs of the definition
  if(getFlags()["tcc"].getBool()) {
    Type tpDef(getType(def)), tpVar(type);
    // Make sure that tpDef is a subtype of tpVar; that is, prove
    // FORALL (x: tpDef): typePred(tpVar)(x)
    if(tpDef != tpVar) {
      TRACE("tccs", "CONSTDEF: "+name+" : "+tpVar.toString()
            +" := <value> : ", tpDef, ";");
      bool typesMatch(true);
      if(tpDef.isFunction() || tpVar.isFunction())
        // For functions, require exact type match
        typesMatch=false;
      else { // Non-function type: check the TCCs
        vector<Expr> boundVars;
        boundVars.push_back(boundVarExpr(name, "tcc", tpDef));
        Expr body(getTypePred(tpVar, boundVars[0]));
        Expr quant(forallExpr(boundVars, body));
        // Query the subtyping formula
        push();
        typesMatch=query(quant, true);
      }
      if(!typesMatch) {
        throw TypecheckException
          ("Type mismatch in constant definition:\n"
           "Constant "+name+
           " is declared with type:\n  "
           +type.toString()
           +"\nBut the type of definition is\n  "
           +getType(def).toString()
           +"\n\n which is not a subtype of the constant");
      }
      pop();
    }
  }
  return d_theoryCore->newFunction(name, type, def);
}


Expr VCL::funExpr(const Op& op, const Expr& child)
{
  return newExpr(op, child);
}


Expr VCL::funExpr(const Op& op, const Expr& left, const Expr& right)
{
  return newExpr(op, left, right);
}


Expr VCL::funExpr(const Op& op, const Expr& child0, const Expr& child1, const Expr& child2)
{
  return newExpr(op, child0, child1, child2);
}


Expr VCL::funExpr(const Op& op, const vector<Expr>& children)
{
  return newExpr(op, children);
}


Expr VCL::stringExpr(const string& str) {
  return newStringExpr(getEM(), str);
}


Expr VCL::idExpr(const string& name) {
  return newExpr(getEM(), ID, stringExpr(name));
}

Expr VCL::listExpr(const vector<Expr>& kids) {
  return newExpr(getEM(), RAW_LIST, kids);
}


Expr VCL::listExpr(const Expr& e1) {
  return newExpr(getEM(), RAW_LIST, e1);
}


Expr VCL::listExpr(const Expr& e1, const Expr& e2) {
  return newExpr(getEM(), RAW_LIST, e1, e2);
}


Expr VCL::listExpr(const Expr& e1, const Expr& e2, const Expr& e3) {
  return newExpr(getEM(), RAW_LIST, e1, e2, e3);
}


Expr VCL::listExpr(const std::string& op, const std::vector<Expr>& kids) {
  vector<Expr> newKids;
  newKids.push_back(idExpr(op));
  newKids.insert(newKids.end(), kids.begin(), kids.end());
  return listExpr(newKids);
}


Expr VCL::listExpr(const std::string& op, const Expr& e1) {
  return newExpr(getEM(), RAW_LIST, idExpr(op), e1);
}


Expr VCL::listExpr(const std::string& op, const Expr& e1,
                   const Expr& e2) {
  return newExpr(getEM(), RAW_LIST, idExpr(op), e1, e2);
}


Expr VCL::listExpr(const std::string& op, const Expr& e1,
                   const Expr& e2, const Expr& e3) {
  vector<Expr> kids;
  kids.push_back(idExpr(op));
  kids.push_back(e1);
  kids.push_back(e2);
  kids.push_back(e3);
  return listExpr(kids);
}


void VCL::printExpr(const Expr& e) {
  printExpr(e, cout);
}


void VCL::printExpr(const Expr& e, ostream& os) {
  if(getFlags()["reorder"].getBool()){
    Expr e1 = (d_theoryCore->preprocess(e)).getRHS();
    srandom(getFlags()["seed"].getInt());
    e1 = d_theoryCore->ite_reorder(e1);
    os << e1 ;
    return;
  }
  if(getFlags()["pq"].getBool()){
    os << e ;
    return;
  }
  os << e << endl;
}





Expr VCL::parseExpr(const Expr& e) {
  return d_theoryCore->parseExprTop(e);
}


Type VCL::parseType(const Expr& e) {
  return Type(d_theoryCore->parseExpr(e));
}


void VCL::assertFormula(const Expr& e)
{
  // Typecheck the user input
  if(!getType(e).isBool()) {
    throw TypecheckException("Non-BOOLEAN formula in ASSERT:\n  "
                             +newExpr(getEM(), ASSERT, e).toString()
                             +"\nDerived type of the formula:\n  "
                             +getType(e).toString());
  }

  // Check if the ofstream is open (as opposed to the command line flag)
  if(d_osdump) {
    if (d_translate && d_em->getOutputLang() == SMTLIB_LANG) {
      d_osdump << "  :assumption" << endl;
      d_osdump << e << endl;
    }
    else {
      d_osdump << newExpr(d_em, ASSERT, e) << endl;
    }
  }
  // Expr e = getFlags()["cnf"].getBool() ? d_cnf->cnf(ee) : ee;

  TRACE("facts", "VCL::assertFormula(", e, ") {");
  // See if e was already asserted before
  if(d_userAssertions->count(e) > 0) {
    TRACE_MSG("facts", "VCL::assertFormula[repeated assertion] => }");
    return;
  }
  // Check the validity of the TCC
  Theorem tccThm;
  if(getFlags()["tcc"].getBool()) {
    Expr tcc(d_theoryCore->getTCC(e));
    int scope = scopeLevel();
    d_cm->push();
    tccThm = d_se->checkValidThm(tcc);
    if(tccThm.isNull()) {
      throw TypecheckException("Failed TCC for the formula in ASSERT:\n\n  "
                               +newExpr(getEM(), ASSERT, e).toString()
                               +"\n\nThe failed TCC is:\n\n  "
                               +tcc.toString()
                               +"\n\nWhich simplified to:\n\n  "
                               +simplify(tcc).toString()
                               +"\n\nAnd the last formula is not valid "
                               "in the current context.");
    }
    else
      d_lastQueryTCC = tccThm;
    d_cm->popto(scope);
  }

  Theorem thm = d_se->newUserAssertion(e);
  (*d_userAssertions)[e] = UserAssertion(thm, tccThm);
  if (!thm.isNull()) {
    d_theoryCore->addFact(d_theoryCore->preprocess(thm));
  }
  TRACE_MSG("facts", "VCL::assertFormula => }");
}


Expr VCL::getImpliedLiteral()
{
  return d_se->getImpliedLiteral();
}


Expr VCL::simplify(const Expr& e) {
  if(getFlags()["tcc"].getBool())
    return simplifyThm(e).getRHS();
  else
    return simplifyThm2(e).getRHS();
}


Theorem3 VCL::simplifyThm(const Expr& e)
{
  DebugAssert(getFlags()["tcc"].getBool(),
              "VCL::simplifyThm() is called without +tcc flag");
  // Typecheck the user input (here it only needs to typecheck without errors)
  getType(e);
  // Assert the type predicates of e
  d_theoryCore->addFact(d_theoryCore->subtypePredicate(e));

  // Now check the TCC
  Expr tcc(d_theoryCore->getTCC(e));
  int scope = scopeLevel();
  d_cm->push();
  Theorem tccThm = d_se->checkValidThm(tcc);
  if(tccThm.isNull()) {
    throw TypecheckException
      ("Failed TCC for the formula in TRANSFORM:\n\n  "
       +newExpr(getEM(), TRANSFORM, e).toString()
       +"\n\nThe failed TCC is:\n\n  "
       +tcc.toString()
       +"\n\nWhich simplified to:\n\n  "
       +simplify(tcc).toString()
       +"\n\nAnd the last formula is not valid in the current context.");
  }
  else
    d_lastQueryTCC = tccThm;
  d_cm->popto(scope);
  // Finally, we are ready to simplify the original expression
  Theorem res2 = d_theoryCore->preprocess(e);
  Theorem simpThm =  d_theoryCore->simplifyThm(res2.getRHS(),
                                               true /* force rebuild */);
  res2 = d_theoryCore->transitivityRule(res2, simpThm);
  Theorem3 res3;
  // For soundness, we have to re-prove the TCC for the entire formula e=e'
  tcc = d_theoryCore->getTCC(res2.getExpr());
  scope = scopeLevel();
  d_cm->push();
  tccThm = d_se->checkValidThm(tcc);
  // We may still fail the TCC if the DPs have some funky total
  // interpretation of partial functions, in which case it should be
  // considered a bug, for any practical purposes.
  DebugAssert(!tccThm.isNull(), "VCL::simplifyThm(): TCC for e=e' failed:"
              "\n res2 = "+res2.getExpr().toString()
              +"\n tcc = "+tcc.toString());
  res3 = d_theoryCore->queryTCC(res2, tccThm);
  d_cm->popto(scope);
  return res3;
}


Theorem VCL::simplifyThm2(const Expr& e)
{
  // Typecheck the user input (here it only needs to typecheck without errors)
  getType(e);
  // Assert the type predicates of e
  d_theoryCore->addFact(d_theoryCore->subtypePredicate(e));

  // We are ready to simplify the original expression
  Theorem res2 = d_theoryCore->preprocess(e);
  Theorem simpThm =  d_theoryCore->simplifyThm(res2.getRHS(),
                                               true /* force rebuild */);
  res2 = d_theoryCore->transitivityRule(res2, simpThm);
  return res2;
}

void VCL::printV(const Expr& e) {
  if(e.getKind() == UCONST || (e.getKind() == APPLY && e.arity() == 0)) {
    Str_To_Expr::iterator it = d_vars.find(e.toString());
    if(it == d_vars.end()){
      cout << e << " : " << getType(e).toString() << ";" << endl;
      d_vars[e.toString()] = e;
    }
    return;
  }
  if(e.getKind() == APPLY) {
    string name = e.getFun().toString();
    Str_To_Expr::iterator it = d_vars.find(name);
    if(it == d_vars.end()) {
      Expr e1 = e.getFun();
      cout << name << " : " << getType(e1).toString() << ";" << endl;
      d_vars[name] = e1;
    }
  }
  
  for(int i=0; i<e.arity(); i++) {
    printV(e[i]);
  }
}

/*!
 * \param e is the queried formula
 *
 * \param isTCC is true when quering a TCC.  In this case, the TCC of
 * e must be TRUE.
 */
bool VCL::query(const Expr& e, bool isTCC)
{
  // Expr e = getFlags()["cnf"].getBool() ? d_cnf->cnf(ee.negate()).negate() : ee;

  TRACE("facts", "VCL::query(", e,
        string(isTCC? ", isTCC=true" : "")+") {");
  // Typecheck the user input
  if(!getType(e).isBool()) {
    throw TypecheckException("Non-BOOLEAN formula in QUERY:\n  "
                             +newExpr(getEM(), QUERY, e).toString()
                             +"\nDerived type of the formula:\n  "
                             +getType(e).toString());
  }

  // Check if the ofstream is open (as opposed to the command line flag)
  if(d_osdump) {
    if (d_translate) {
      d_osdump << "  :formula" << endl;
      d_osdump << !e << endl;
      // For now, just assume status is unknown.
      d_osdumpTranslate << "  :status unknown" << endl;
      return false;
    }
    else {
      d_osdump << newExpr(d_em, QUERY, e) << endl;
    }
  }

  // Check the validity of the TCC
  if(!isTCC && getFlags()["tcc"].getBool()) {
    Expr tcc(d_theoryCore->getTCC(e));
    // FIXME: we have to guarantee that the TCC of 'tcc' is always valid
    int scope = scopeLevel();
    d_cm->push();
    d_lastQueryTCC = d_se->checkValidThm(tcc);
    if(d_lastQueryTCC.isNull()) {
      throw TypecheckException("Failed TCC for the formula in QUERY:\n\n  "
                               +newExpr(getEM(), QUERY, e).toString()
                               +"\n\nThe failed TCC is:\n\n  "
                               +tcc.toString()
                               +"\n\nWhich simplified to:\n\n  "
                               +simplify(tcc).toString()
                               +"\n\nAnd the last formula is not valid "
                               "in the current context.");
    }
    d_cm->popto(scope);
  }
  if(getFlags()["reorder"].getBool() || getFlags()["pq"].getBool()){
    cout << "%% Print query variables:" << endl;
    printV(e);
    cout << "QUERY ";
    printExpr(e);
    cout << ";" << endl;
    cout << "%%";
    return true;
  }
  Theorem res = d_se->checkValidThm(e);
  // Save the result for subsequent commands like DUMP_PROOF
  if(!res.isNull()) {
    if(isTCC)
      d_lastQueryTCC = res;
    else if (getFlags()["tcc"].getBool()) {
      d_lastQuery = d_theoryCore->queryTCC(res, d_lastQueryTCC);
    }
  } else { // Clean up the variables
    d_lastQueryTCC = Theorem();
    d_lastQuery = Theorem3();
    d_lastClosure = Theorem3();
  }
  TRACE("facts", "VCL::query => ", res.isNull()? "false" : "true", " }");

  if(d_translate && d_em->getOutputLang() == SMTLIB_LANG) {
    d_osdumpTranslate << "  :status ";
    if (!res.isNull()) d_osdumpTranslate << "unsat" << endl;
    else if(incomplete()) {
      d_osdumpTranslate << "unknown" << endl;
    }
    else d_osdumpTranslate << "sat" << endl;
  }

  return !res.isNull();
}


bool VCL::checkUnsat(const Expr& e)
{
  return query(!e);
}


bool VCL::checkContinue()
{
  if(d_osdump) {
    d_osdump << newExpr(d_em, CONTINUE) << endl;
  }
  vector<Expr> assertions;
  d_se->getCounterExample(assertions);
  if (assertions.size() == 0) {
    d_se->restart(falseExpr());
    return true;
  }
  Expr eAnd = assertions.size() == 1 ? assertions[0] : andExpr(assertions);
  return d_se->restart(!eAnd);
}


bool VCL::restart(const Expr& e)
{
  if (d_osdump) {
    d_osdump << newExpr(d_em, RESTART, e) << endl;
  }
  return d_se->restart(e);
}


void VCL::getAssertions(vector<Expr>& assertions)
{
  d_se->getAssertions(assertions);
}


void VCL::getConcreteModel(ExprMap<Expr> & m)
{
  if(d_osdump) {
    d_osdump << newExpr(d_em, COUNTEREXAMPLE) << endl;
  }
  d_se->getConcreteModel(m);
}


void VCL::getCounterExample(vector<Expr>& assertions, bool inOrder)
{
  d_se->getCounterExample(assertions, inOrder);
}

bool VCL::inconsistent(vector<Expr>& assumptions)
{
  if (d_theoryCore->inconsistent()) {
    getAssumptions(d_theoryCore->inconsistentThm().getAssumptionsRef(),
                   assumptions);
    return true;
  }
  return false;
}


bool VCL::incomplete() {
  // Return true only after a failed query
  return (d_lastQuery.isNull() && d_theoryCore->incomplete());
}


bool VCL::incomplete(vector<string>& reasons) {
  // Return true only after a failed query
  return (d_lastQuery.isNull() && d_theoryCore->incomplete(reasons));
}


void VCL::setResourceLimit(unsigned limit) {
  d_theoryCore->setResourceLimit(limit);
}


Proof VCL::getProof()
{
  if(d_lastQuery.isNull())
    throw EvalException
      ("Method getProof() (or command DUMP_PROOF)\n"
       " must be called only after a Valid QUERY");
  return d_se->getProof();
}


void VCL::getAssumptions(vector<Expr>& assumptions)
{
  if(d_lastQuery.isNull())
    throw EvalException
      ("Method getAssumptions() (or command DUMP_ASSUMPTIONS)\n"
       " must be called only after a Valid QUERY");
  getAssumptions(d_lastQuery.getAssumptionsRef(), assumptions);
}


void VCL::getAssumptionsTCC(vector<Expr>& assumptions)
{
  if(d_lastQuery.isNull())
    throw EvalException
      ("Method getAssumptionsTCC() (or command DUMP_TCC_ASSUMPTIONS)\n"
       " must be called only after a Valid QUERY");
  getAssumptions(d_lastQueryTCC.getAssumptionsRef(), assumptions);
}


const Expr& VCL::getTCC(){
  static Expr null;
  if(d_lastQueryTCC.isNull()) return null;
  else return d_lastQueryTCC.getExpr();
}


const Proof& VCL::getProofTCC() {
  static Proof null;
  if(d_lastQueryTCC.isNull()) return null;
  else return d_lastQueryTCC.getProof();
}


const Expr& VCL::getClosure() {
  static Expr null;
  if(d_lastClosure.isNull() && !d_lastQuery.isNull()) {
    // Construct the proof of closure and cache it in d_lastClosure
    d_lastClosure = deriveClosure(d_lastQuery);
  }
  if(d_lastClosure.isNull()) return null;
  else return d_lastClosure.getExpr();
}


const Proof& VCL::getProofClosure() {
  static Proof null;
  if(d_lastClosure.isNull() && !d_lastQuery.isNull()) {
    // Construct the proof of closure and cache it in d_lastClosure
    d_lastClosure = deriveClosure(d_lastQuery);
  }
  if(d_lastClosure.isNull()) return null;
  else return d_lastClosure.getProof();
}


int VCL::stackLevel()
{
  return d_scopeStack.size();
}


void VCL::push()
{
  TRACE("vcl", "push(): stack size = ", d_scopeStack.size(), "{ ");
  // Check if the ofstream is open (as opposed to the command line flag)
  if(d_osdump) {
    d_osdump << newExpr(d_em, PUSH) << endl;
  }
  d_scopeStack.push_back(scopeLevel());
  d_cm->push();
  TRACE("vcl", "push => stack size ", d_scopeStack.size(), "}");
}


void VCL::pop()
{
  TRACE("vcl", "pop(): stack size = ", d_scopeStack.size(), "{ ");
  // Check if the ofstream is open (as opposed to the command line flag)
  if(d_osdump) {
    d_osdump << newExpr(d_em, POP) << endl;
  }
  if(d_scopeStack.size() != 0) {
    d_cm->popto(d_scopeStack.back());
    d_scopeStack.pop_back();
  }
  TRACE("vcl", "pop => stack size ", d_scopeStack.size(), "}");
}


void VCL::popto(int toLevel)
{
  // Check if the ofstream is open (as opposed to the command line flag)
  if(d_osdump) {
    d_osdump << newExpr(d_em, POPTO, ratExpr(toLevel, 1)) << endl;
  }
  if (toLevel < 0) toLevel = 0;
  while (stackLevel() > toLevel+1) {
    d_scopeStack.pop_back();
  }
  if (stackLevel() > toLevel) {
    d_cm->popto(d_scopeStack.back());
    d_scopeStack.pop_back();
  }
}


int VCL::scopeLevel()
{
  return d_cm->scopeLevel();
}


void VCL::pushScope()
{
  d_cm->push();
  if(d_osdump) {
    d_osdump << newExpr(d_em, PUSH_SCOPE) << endl;
  }
  IF_DEBUG(if((*d_flags)["dump-trace"].getString() != "")
           debugger.dumpTrace(scopeLevel()));
}


void VCL::popScope()
{
  if(d_osdump) {
    d_osdump << newExpr(d_em, POP_SCOPE) << endl;
  }
  if (scopeLevel() == 1) {
    cout << "Cannot POP from scope level 1" << endl;
  }
  else d_cm->pop();
  IF_DEBUG(if((*d_flags)["dump-trace"].getString() != "")
           debugger.dumpTrace(scopeLevel()));
}


void VCL::poptoScope(int toLevel)
{
  if(d_osdump) {
    d_osdump << newExpr(d_em, POPTO_SCOPE, ratExpr(toLevel, 1)) << endl;
  }
  if (toLevel < 1) {
    d_cm->popto(0);
    d_cm->push();
  }
  else d_cm->popto(toLevel);
  IF_DEBUG(if((*d_flags)["dump-trace"].getString() != "")
           debugger.dumpTrace(scopeLevel()));
}


Context* VCL::getCurrentContext()
{
  return d_cm->getCurrentContext();
}


TheoryCore* VCL::theoryCore()
{
  return d_theoryCore;
}

void VCL::loadFile(const std::string& fileName, InputLanguage lang,
                   bool interactive) {
  Parser parser(this, lang, interactive, fileName);
  VCCmd cmd(this, &parser);
  cmd.processCommands();
}


void VCL::loadFile(std::istream& is, InputLanguage lang,
                   bool interactive) {
  Parser parser(this, lang, is, interactive);
  VCCmd cmd(this, &parser);
  cmd.processCommands();
}


bool VCL::isLiteral(const Expr& e) {
  return d_theoryCore->isLiteral(e);
}


Expr CNF::exprVar(const Expr& e)
{
  TRACE("mycnf", "CNF::exprVar(", e, ") {");
  if (e.arity() == 0 || d_core->isLiteral(e) || d_core->isAtomic(e)) {
    TRACE("mycnf", "CNF::exprVar[literal] => ", e, " }");
    return e;
  }

  if (e.isNot()) {
    Expr res(!exprVar(e[0]));
    TRACE("mycnf", "CNF::exprVar[NOT] => ", res, " }");
    return res;
  }

  map<Expr,Expr>::iterator it = d_exprVars.find(e);
  if (it != d_exprVars.end()) {
    // IF_DEBUG(debugger.counter("Jake CNF cache hits")++);
    d_vcl->getStatistics().counter("Jake CNF cache hits")++;
    TRACE("mycnf", "CNF::exprVar[cache] => ", it->second, " }");
    return it->second;
  }
  else
  {
    string name("_e_");
    name += int2string(d_nextNum++);
    // IF_DEBUG(debugger.counter("Jake new vars") = d_nextNum);
    d_vcl->getStatistics().counter("Jake new vars")++;
    Expr ev = d_vcl->varExpr(name, d_core->getType(e));
    //cerr << name << " : " << d_core->getType(e) << ";" << endl;
    d_exprVars[e] = ev;
    d_q.push_back(e);
    TRACE("mycnf", "CNF::exprVar[new] => ", ev, " }");
    return ev;
  }
}

TheoryCore * CNF::theoryCore() { 
  return d_vcl->theoryCore();
}

Expr CNF::cnf(const Expr& e)
{
  TRACE("mycnf", "CNF::cnf(", e, ") {");
 vector<Expr> clauses;
 // clauses.push_back(exprVar(theoryCore()->simplifyThm(e).getRHS()));
 clauses.push_back(exprVar(e));

  TRACE("cnf-clauses", "cnf call", e, "");
  while (d_q.size() > 0)
  {
    Expr e = d_q.front();
    d_q.pop_front();

    if (e.arity() == 0 || d_core->isLiteral(e) || d_core->isAtomic(e))
      continue;

    bool isBool = (d_core->getType(e) == d_vcl->boolType());
    for (int i=0; i < e.arity() && isBool; i++)
      isBool = (d_core->getType(e[i]) == d_vcl->boolType());

    if (isBool)
    {
      if (e.isAnd())
      {
        if (d_vcl->getFlags()["circuit"].getBool() && e.arity() == 2)
        {
          clauses.push_back(newExpr(d_vcl->getEM(),
                                    AND_R,
                                    exprVar(e),
                                    exprVar(e[0]),
                                    exprVar(e[1])));
        }

        else
        {
          //   (e <=> (a AND b AND c)) <=>
          //   ((NOT e OR a) AND (NOT e OR b) AND (NOT e OR c) AND
          //    (e OR NOT a OR NOT b OR NOT c))

          Expr ev = exprVar(e);
          vector<Expr> v;
          v.push_back(ev);
          for (int i=0; i < e.arity(); i++)
          {
            Expr evi = exprVar(e[i]);
            clauses.push_back(ev.negate() || evi);
            v.push_back(evi.negate());
          }
          clauses.push_back(d_vcl->orExpr(v));
        }
      }

      else if (e.isOr())
      {
        if (d_vcl->getFlags()["circuit"].getBool() && e.arity() == 2)
        {
          clauses.push_back(newExpr(d_vcl->getEM(),
                                    AND_R,
                                    exprVar(e).negate(),
                                    exprVar(e[0]).negate(),
                                    exprVar(e[1]).negate()));
        }

        else
        {
          //   (e <=> (a OR b OR c)) <=>
          //   ((e OR NOT a) AND (e OR NOT b) AND (e OR NOT c) AND
          //    (NOT e OR a OR b OR c))

          Expr ev = exprVar(e);
          vector<Expr> v;
          v.push_back(ev.negate());
          for (int i=0; i < e.arity(); i++)
          {
            Expr evi = exprVar(e[i]);
            clauses.push_back(ev || evi.negate());
            v.push_back(evi);
          }
          clauses.push_back(d_vcl->orExpr(v));
        }
      }

      else if (e.isITE())
      {
        Expr ev = exprVar(e);
        Expr ev0 = exprVar(e[0]);
        Expr ev1 = exprVar(e[1]);
        Expr ev2 = exprVar(e[2]);

        if (d_vcl->getFlags()["circuit"].getBool())
        {
          vector<Expr> v;
          v.push_back(ev);
          v.push_back(ev0);
          v.push_back(ev1);
          v.push_back(ev2);
          clauses.push_back(newExpr(d_vcl->getEM(), ITE_R, v));
        }

        else
        {
          //   (e <=> IF a THEN b ELSE c ENDIF) <=>
          //   ((NOT e OR NOT a OR b) AND
          //    (NOT e OR a OR c) AND
          //    (e OR NOT a OR NOT b) AND
          //    (e OR a OR NOT c))

          clauses.push_back(ev.negate() || ev0.negate() || ev1);
          clauses.push_back(ev.negate() || ev0 || ev2);
          clauses.push_back(ev || ev0.negate() || ev1.negate());
          clauses.push_back(ev || ev0 || ev2.negate());
        }
      }

      else if (e.isImpl())
      {
        Expr ev = exprVar(e);
        Expr ev0 = exprVar(e[0]);
        Expr ev1 = exprVar(e[1]);

        if (d_vcl->getFlags()["circuit"].getBool())
        {
          clauses.push_back(newExpr(d_vcl->getEM(), AND_R,
                                    ev.negate(), ev0, ev1.negate()));
        }

        else
        {
          //   (e <=> (a => b)) <=>
          //   ((NOT e OR NOT a OR b) AND (e OR a) AND (e OR NOT b))

          clauses.push_back(ev.negate() || ev0.negate() || ev1);
          clauses.push_back(ev || ev0);
          clauses.push_back(ev || ev1.negate());
        }
      }

      else if (e.isIff())
      {
        Expr ev = exprVar(e);
        Expr ev0 = exprVar(e[0]);
        Expr ev1 = exprVar(e[1]);

        if (d_vcl->getFlags()["circuit"].getBool())
        {
          clauses.push_back(newExpr(d_vcl->getEM(), IFF_R, ev, ev0, ev1));
        }

        else
        {
          //   (e <=> (a <=> b)) <=>
          //   ((NOT e OR NOT a OR b) AND (NOT e OR a OR NOT b) AND
          //    (e OR a OR b) AND (e OR NOT a OR NOT b))

          clauses.push_back(ev.negate() || ev0.negate() || ev1);
          clauses.push_back(ev.negate() || ev0 || ev1.negate());
          clauses.push_back(ev || ev0 || ev1);
          clauses.push_back(ev || ev0.negate() || ev1.negate());
        }
      }

      else
      {
        cerr << e << endl;
        DebugAssert(false, "unhandled boolean");
      }
    }

    else
    {
      if (e.isITE())
      {
        //   (e = (IF a THEN b ELSE c ENDIF)) <=>
        //   ((a => (e = b)) AND (NOT a => (e = c))) <=>
        //   ((NOT a OR (e = b)) AND (a OR (e = c)))

        Expr ev = exprVar(e);
        Expr ev0 = exprVar(e[0]);
        Expr ev1 = exprVar(e[1]);
        Expr ev2 = exprVar(e[2]);

        clauses.push_back(ev0.negate() || d_vcl->eqExpr(ev, ev1));
        clauses.push_back(ev0 || d_vcl->eqExpr(ev, ev2));
      }

      else
      {
        if (!d_core->isAtomic(e))
        {
          Expr ev = exprVar(e);
          vector<Expr> newKids;
          for (int i=0; i < e.arity(); i++)
          {
            Expr evi = exprVar(e[i]);
            newKids.push_back(evi);
          }

          Expr res = newExpr(d_vcl->getEM(), getOp(e), newKids);
          if (d_core->getType(e) == d_vcl->boolType())
          {
            clauses.push_back(ev || res.negate());
            clauses.push_back(ev.negate() || res);
          }
          else
            clauses.push_back(d_vcl->eqExpr(ev, res));
        }
      }
    }
    TRACE("mycnf", "Jake Clauses", andExpr(clauses), "}");
  }

  //clauses.push_back(e);

  // Expr ee = theoryCore()->simplifyThm(d_vcl->andExpr(clauses)).getRHS();
  Expr ee = d_vcl->andExpr(clauses);
//   for(Expr::iterator i = ee.begin(), iend=ee.end(); i!=iend;++i)
//     TRACE("cnf-clauses", "Jake Clauses", *i, "");
  TRACE("cnf-clauses", "Unsimplified clauses: ", d_vcl->andExpr(clauses), "");
  TRACE("cnf-clauses", "Jake Clauses", ee, "");
  TRACE("mycnf", "CNF::cnf => ", ee, " }");
  return ee;
}

---