search_sat.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 *\file search_sat.cpp
 *\brief Implementation of Search engine with generic external sat solver
 *
 * Author: Clark Barrett
 *
 * Created: Wed Dec  7 21:00:24 2005
 */
/*****************************************************************************/


#include "search_sat.h"
#include "dpllt_basic.h"
#include "theory_core.h"
#include "eval_exception.h"
#include "typecheck_exception.h"
#include "expr_transform.h"
#include "search_rules.h"


using namespace std;
using namespace CVCL;
using namespace SAT;


namespace CVCL {


class SearchSatCoreSatAPI :public TheoryCore::CoreSatAPI {
  SearchSat* d_ss;
public:
  SearchSatCoreSatAPI(SearchSat* ss) : d_ss(ss) {}
  ~SearchSatCoreSatAPI() {}
  void addLemma(const Theorem& thm) { d_ss->addLemma(thm); }
  int getBottomScope() { return d_ss->getBottomScope(); }
  Theorem addAssumption(const Expr& assump)
  { return d_ss->newUserAssumption(assump); }
  void addSplitter(const Expr& e, int priority)
  { d_ss->addSplitter(e, priority); }
};


class SearchSatTheoryAPI :public DPLLT::TheoryAPI {
  ContextManager* d_cm;
  SearchSat* d_ss;
public:
  SearchSatTheoryAPI(SearchSat* ss)
    : d_cm(ss->theoryCore()->getCM()), d_ss(ss) {}
  ~SearchSatTheoryAPI() {}
  void push() { return d_cm->push(); }
  void pop() { return d_cm->pop(); }
  void assertLit(Lit l) { d_ss->assertLit(l); }
  DPLLT::ConsistentResult checkConsistent(Clause& c, bool fullEffort)
    { return d_ss->checkConsistent(c, fullEffort); }
  Lit getImplication() { return d_ss->getImplication(); }
  void getExplanation(Lit l, Clause& c) { return d_ss->getExplanation(l, c); }
  bool getNewClauses(CNF_Formula& cnf) { return d_ss->getNewClauses(cnf); }
};


class SearchSatDecider :public DPLLT::Decider {
  SearchSat* d_ss;
public:
  SearchSatDecider(SearchSat* ss) : d_ss(ss) {}
  ~SearchSatDecider() {}

  Lit makeDecision() { return d_ss->makeDecision(); }
};


}


void SearchSat::addLemma(const Theorem& thm)
{
  //TODO: this should only hapen with new literals--
  //      others are handled by implication mechanism
  if (thm.getExpr().isAbsLiteral()// && !d_cnfManager->getCNFLit(thm.getExpr()).isNull()
      ) return;

  //  DebugAssert(d_inCheckSat, "Should only be used as a call-back");
  d_rootLits.push_back(d_cnfManager->addLemma(thm, d_lemmas));

  // Register any new atoms
  Expr e;
  for (; d_lastRegisteredVar < d_lemmas.numVars(); ) {
    d_lastRegisteredVar = d_lastRegisteredVar + 1;
    e = d_cnfManager->concreteLit(Lit(int(d_lastRegisteredVar)));
    if (!e.isNull() && e.isAbsAtomicFormula()) {
      d_core->registerAtom(e);
    }
  }
  while (d_cnfManager->numVars() >= d_vars.size()) {
    d_vars.push_back(SmartCDO<SAT::Var::Val>(
                       d_core->getCM()->getCurrentContext(),
                       SAT::Var::UNKNOWN, 0));
  }
}


void SearchSat::addSplitter(const Expr& e, int priority)
{
  // TODO: it's called during assertions from theory_arith.  Need to figure out the right invariant here.
  //  DebugAssert(d_inCheckSat, "Should only be used as a call-back");
  // Not implemented yet
}


void SearchSat::assertLit(Lit l)
{
  DebugAssert(d_inCheckSat, "Should only be used as a call-back");
  setValue(l.getVar(), l.isPositive() ? Var::TRUE : Var::FALSE);
  Expr e = d_cnfManager->concreteLit(l);
  DebugAssert(!e.isNull(), "Expected known expr");
  if (!e.isAbsLiteral() || e.isUserAssumption()) return;
  DebugAssert(!e.isIntAssumption(), "Expected new assumption");
  e.setIntAssumption();
  Theorem thm = d_commonRules->assumpRule(e);
  d_intAssumptions.push_back(thm);
  d_core->addFact(thm);
}


DPLLT::ConsistentResult SearchSat::checkConsistent(Clause& c, bool fullEffort)
{
  DebugAssert(d_inCheckSat, "Should only be used as a call-back");
  if (d_core->inconsistent()) {
    d_cnfManager->convertLemma(d_core->inconsistentThm(), c);
    return DPLLT::INCONSISTENT;
  }
  if (fullEffort) {
    if (d_core->checkSATCore()) {
      if (d_core->inconsistent()) {
        d_cnfManager->convertLemma(d_core->inconsistentThm(), c);
        return DPLLT::INCONSISTENT;
      }
      else return DPLLT::CONSISTENT;
    }
  }
  return DPLLT::MAYBE_CONSISTENT;
}


Lit SearchSat::getImplication()
{
  DebugAssert(d_inCheckSat, "Should only be used as a call-back");
  Lit l;
  Theorem imp = d_core->getImpliedLiteral();
  while (!imp.isNull()) {
    l = d_cnfManager->getCNFLit(imp.getExpr());
    DebugAssert(!l.isNull() || imp.getExpr().unnegate().isUserRegisteredAtom(),
                "implied literals should be registered by cnf or by user");
    if (!l.isNull() && getValue(l) != Var::TRUE) {
      d_theorems.insert(imp.getExpr(), imp);
      break;
    }
    l.reset();
    imp = d_core->getImpliedLiteral();
  }
  return l;
}


void SearchSat::getExplanation(Lit l, Clause& c)
{
  DebugAssert(d_inCheckSat, "Should only be used as a call-back");
  DebugAssert(c.size() == 0, "Expected size = 0");
  Expr e = d_cnfManager->concreteLit(l);
  CDMap<Expr, Theorem>::iterator i = d_theorems.find(e);
  DebugAssert(i != d_theorems.end(), "getExplanation: no explanation found");
  d_cnfManager->convertLemma((*i).second, c);  
}


bool SearchSat::getNewClauses(CNF_Formula& cnf)
{
  DebugAssert(d_inCheckSat, "Should only be used as a call-back");
  if (d_lemmasNext == d_lemmas.numClauses()) return false;
  do {
    cnf += d_lemmas[d_lemmasNext];
    d_lemmasNext = d_lemmasNext + 1;
  } while (d_lemmasNext < d_lemmas.numClauses());
  return true;
}


Lit SearchSat::makeDecision()
{
  DebugAssert(d_inCheckSat, "Should only be used as a call-back");
  Lit litDecision;
  CDList<SAT::Lit>::const_iterator i, iend;
  for (i = d_rootLits.begin(), iend = d_rootLits.end(); i != iend; ++i) {
    if (findSplitterRec(*i, getValue(*i), &litDecision)) {
      break;
    }
  }
  return litDecision;
}


bool SearchSat::findSplitterRec(Lit lit, Var::Val value, Lit* litDecision)
{
  unsigned i, n;
  Lit litTmp;
  bool ret;
  Var v = lit.getVar();

  if (lit.isFalse() || lit.isTrue()) return false;
  DebugAssert(value != Var::UNKNOWN, "expected known value");
  DebugAssert(getValue(lit) == value || getValue(lit) == Var::UNKNOWN,
              "invariant violated");

  if (checkJustified(v)) return false;

  if (lit.isInverted()) {
    lit = !lit;
    value = Var::invertValue(value);
  }

  if (d_cnfManager->numFanins(lit) == 0) {
    if (getValue(lit) != Var::UNKNOWN) {
      setJustified(v);
      return false;
    }
    else {
      *litDecision = Lit(v, value == Var::TRUE);
      return true;
    }
  }
  else if (d_cnfManager->concreteLit(lit).isAbsAtomicFormula()) {
    // This node represents a predicate with embedded ITE's
    // We handle this case specially in order to catch the
    // corner case when a variable is in its own fanin.
    n = d_cnfManager->numFanins(lit);
    for (i=0; i < n; ++i) {
      litTmp = d_cnfManager->getFanin(lit, i);
      DebugAssert(!litTmp.isInverted(),"Expected positive fanin");
      if (checkJustified(litTmp.getVar())) continue;
      DebugAssert(d_cnfManager->concreteLit(litTmp.getVar()).getKind() == ITE,
                  "Expected ITE");
      DebugAssert(getValue(litTmp) == Var::TRUE,"Expected TRUE");
      Lit cIf = d_cnfManager->getFanin(litTmp,0);
      Lit cThen = d_cnfManager->getFanin(litTmp,1);
      Lit cElse = d_cnfManager->getFanin(litTmp,2);
      if (getValue(cIf) == Var::UNKNOWN) {
        if (getValue(cElse) == Var::TRUE ||
            getValue(cThen) == Var::FALSE) {
          ret = findSplitterRec(cIf, Var::FALSE, litDecision);
        }
        else {
          ret = findSplitterRec(cIf, Var::TRUE, litDecision);
        }
        if (!ret) {
          cout << d_cnfManager->concreteLit(cIf.getVar()) << endl;
          DebugAssert(false,"No controlling input found (1)");
        }         
        return true;
      }
      else if (getValue(cIf) == Var::TRUE) {
        if (findSplitterRec(cIf, Var::TRUE, litDecision)) {
            return true;
        }
        if (cThen.getVar() != v &&
            (getValue(cThen) == Var::UNKNOWN ||
             getValue(cThen) == Var::TRUE) &&
            findSplitterRec(cThen, Var::TRUE, litDecision)) {
          return true;
        }
      }
      else {
        if (findSplitterRec(cIf, Var::FALSE, litDecision)) {
          return true;
        }
        if (cElse.getVar() != v &&
            (getValue(cElse) == Var::UNKNOWN ||
             getValue(cElse) == Var::TRUE) &&
            findSplitterRec(cElse, Var::TRUE, litDecision)) {
          return true;
        }
      }
      setJustified(litTmp.getVar());
    }
    if (getValue(lit) != Var::UNKNOWN) {
      setJustified(v);
      return false;
    }
    else {
      *litDecision = Lit(v, value == Var::TRUE);
      return true;
    }
  }

  int kind = d_cnfManager->concreteLit(v).getKind();
  Var::Val valHard = Var::FALSE;
  switch (kind) {
    case AND:
      valHard = Var::TRUE;
    case OR:
      if (value == valHard) {
        n = d_cnfManager->numFanins(lit);
        for (i=0; i < n; ++i) {
          litTmp = d_cnfManager->getFanin(lit, i);
          if (findSplitterRec(litTmp, valHard, litDecision)) {
            return true;
          }
        }
        DebugAssert(getValue(lit) == valHard, "Output should be justified");
        setJustified(v);
        return false;
      }
      else {
        Var::Val valEasy = Var::invertValue(valHard);
        n = d_cnfManager->numFanins(lit);
        for (i=0; i < n; ++i) {
          litTmp = d_cnfManager->getFanin(lit, i);
          if (getValue(litTmp) != valHard) {
            if (findSplitterRec(litTmp, valEasy, litDecision)) {
              return true;
            }
            DebugAssert(getValue(lit) == valEasy, "Output should be justified");
            setJustified(v);
            return false;
          }
        }
        DebugAssert(false, "No controlling input found (2)");
      }
      break;
    case IMPLIES:
      DebugAssert(d_cnfManager->numFanins(lit) == 2, "Expected 2 fanins");
      if (value == Var::FALSE) {
        litTmp = d_cnfManager->getFanin(lit, 0);
        if (findSplitterRec(litTmp, Var::TRUE, litDecision)) {
          return true;
        }
        litTmp = d_cnfManager->getFanin(lit, 1);
        if (findSplitterRec(litTmp, Var::FALSE, litDecision)) {
          return true;
        }
        DebugAssert(getValue(lit) == Var::FALSE, "Output should be justified");
        setJustified(v);
        return false;
      }
      else {
        litTmp = d_cnfManager->getFanin(lit, 0);
        if (getValue(litTmp) != Var::TRUE) {
          if (findSplitterRec(litTmp, Var::FALSE, litDecision)) {
            return true;
          }
          DebugAssert(getValue(lit) == Var::TRUE, "Output should be justified");
          setJustified(v);
          return false;
        }
        litTmp = d_cnfManager->getFanin(lit, 1);
        if (getValue(litTmp) != Var::FALSE) {
          if (findSplitterRec(litTmp, Var::TRUE, litDecision)) {
            return true;
          }
          DebugAssert(getValue(lit) == Var::TRUE, "Output should be justified");
          setJustified(v);
          return false;
        }
        DebugAssert(false, "No controlling input found (3)");
      }
      break;
    case IFF: {
      litTmp = d_cnfManager->getFanin(lit, 0);
      Var::Val val = getValue(litTmp);
      if (val != Var::UNKNOWN) {
        if (findSplitterRec(litTmp, val, litDecision)) {
          return true;
        }
        if (value == Var::FALSE) val = Var::invertValue(val);
        litTmp = d_cnfManager->getFanin(lit, 1);
        if (findSplitterRec(litTmp, val, litDecision)) {
          return true;
        }
        DebugAssert(getValue(lit) == value, "Output should be justified");
        setJustified(v);
        return false;
      }
      else {
        val = getValue(d_cnfManager->getFanin(lit, 1));
        if (val == Var::UNKNOWN) val = Var::FALSE;
        if (value == Var::FALSE) val = Var::invertValue(val);
        if (findSplitterRec(litTmp, val, litDecision)) {
          return true;
        }
        DebugAssert(false, "Unable to find controlling input (4)");
      }
      break;
    }
    case XOR: {
      litTmp = d_cnfManager->getFanin(lit, 0);
      Var::Val val = getValue(litTmp);
      if (val != Var::UNKNOWN) {
        if (findSplitterRec(litTmp, val, litDecision)) {
          return true;
        }
        if (value == Var::TRUE) val = Var::invertValue(val);
        litTmp = d_cnfManager->getFanin(lit, 1);
        if (findSplitterRec(litTmp, val, litDecision)) {
          return true;
        }
        DebugAssert(getValue(lit) == value, "Output should be justified");
        setJustified(v);
        return false;
      }
      else {
        val = getValue(d_cnfManager->getFanin(lit, 1));
        if (val == Var::UNKNOWN) val = Var::FALSE;
        if (value == Var::TRUE) val = Var::invertValue(val);
        if (findSplitterRec(litTmp, val, litDecision)) {
          return true;
        }
        DebugAssert(false, "Unable to find controlling input (5)");
      }
      break;
    }
    case ITE: {
      Lit cIf = d_cnfManager->getFanin(lit, 0);
      Lit cThen = d_cnfManager->getFanin(lit, 1);
      Lit cElse = d_cnfManager->getFanin(lit, 2);
      if (getValue(cIf) == Var::UNKNOWN) {
        if (getValue(cElse) == value ||
            getValue(cThen) == Var::invertValue(value)) {
          ret = findSplitterRec(cIf, Var::FALSE, litDecision);
        }
        else {
          ret = findSplitterRec(cIf, Var::TRUE, litDecision);
        }
        if (!ret) {
          cout << d_cnfManager->concreteLit(cIf.getVar()) << endl;
          DebugAssert(false,"No controlling input found (6)");
        }         
        return true;
      }
      else if (getValue(cIf) == Var::TRUE) {
        if (findSplitterRec(cIf, Var::TRUE, litDecision)) {
            return true;
        }
        if (cThen.isVar() && cThen.getVar() != v &&
            (getValue(cThen) == Var::UNKNOWN ||
             getValue(cThen) == value) &&
            findSplitterRec(cThen, value, litDecision)) {
          return true;
        }
      }
      else {
        if (findSplitterRec(cIf, Var::FALSE, litDecision)) {
          return true;
        }
        if (cElse.isVar() && cElse.getVar() != v &&
            (getValue(cElse) == Var::UNKNOWN ||
             getValue(cElse) == value) &&
            findSplitterRec(cElse, value, litDecision)) {
          return true;
        }
      }
      DebugAssert(getValue(lit) == value, "Output should be justified");
      setJustified(v);
      return false;
    }
    default:
      DebugAssert(false, "Unexpected Boolean operator");
      break;
  }
  FatalAssert(false, "Should be unreachable");
  return false;
}


Theorem SearchSat::check(const Expr& e, bool isRestart)
{
  if (!d_dplltReady) {
    throw Exception
      ("SAT solver is not ready: please pop all or none of SAT scopes");
  }
  if (isRestart && d_idxUserAssump != d_userAssumptions.size()) {
    throw Exception
      ("No user assumptions should be added before a restart");
  }
  if (isRestart && d_lastCheck.get().isNull()) {
    throw Exception
      ("restart called without former call to checkValid");
  }

  DebugAssert(!d_inCheckSat, "checkValid should not be called recursively");
  TRACE("searchsat", "checkValid: ", e, "");

  if (!e.getType().isBool())
    throw TypecheckException
      ("checking validity of a non-Boolean expression:\n\n  "
       + e.toString()
       + "\n\nwhich has the following type:\n\n  "
       + e.getType().toString());

  Expr e2 = e;
  Theorem thm;
  CNF_Formula_Impl cnf;
  DPLLT::Result res;

  // Set up and quick exits
  if (isRestart) {
    while (e2.isNot() && e2[0].isNot()) e2 = e2[0][0];
    if (e2.isTrue() || (e2.isNot() && e2[0].isFalse())) return d_lastValid;
    if (e2.isFalse() || (e2.isNot() && e2[0].isTrue())) {
      d_core->getCM()->popto(d_bottomScope);
      res = DPLLT::UNSAT;
      goto finalize;
    }
  }
  else {
    if (e.isTrue()) return (d_lastValid = d_commonRules->trueTheorem());
    d_core->getCM()->push();
    d_bottomScope = d_core->getCM()->scopeLevel();
    d_lastCheck = e;
    e2 = !e;
  }

  d_cnfManager->setBottomScope(d_bottomScope);
  d_dplltReady = false;

  newUserAssumption(e2, d_bottomScope);

  d_inCheckSat = true;

  // Translate user assumptions into cnf
  for (; d_idxUserAssump < d_userAssumptions.size();
         d_idxUserAssump.set(d_idxUserAssump + 1, d_bottomScope) ) {
    thm = d_userAssumptions[d_idxUserAssump];
    e2 = thm.getExpr();
    DebugAssert(e2.isUserAssumption(), "Expected only user assumptions");
    if (isRestart || (e2.isAbsLiteral() && !e2.unnegate().isBoolConst())) {
      d_rootLits.push_back(d_cnfManager->addAssumption(thm, cnf), d_bottomScope);
    }
    else {
      thm = d_core->getExprTrans()->preprocess(thm);
      e2 = thm.getExpr(); 
      if (e2.isFalse()) {
        res = DPLLT::UNSAT;
        goto finalize;
      }
      else if (!e2.isTrue()) {
        d_rootLits.push_back(d_cnfManager->addAssumption(thm, cnf), d_bottomScope);
      }
    }
  }

  // We can't register new atoms in a restart: new atoms have
  // to be registered at the bottom scope
  if (!isRestart) {
    // Register any new atoms
    for (; d_lastRegisteredVar < cnf.numVars(); ) {
      d_lastRegisteredVar = d_lastRegisteredVar + 1;
      e2 = d_cnfManager->concreteLit(Lit(int(d_lastRegisteredVar)));
      if (!e2.isNull() && e2.isAbsAtomicFormula()) {
        d_core->registerAtom(e2);
      }
    }
  }

  // Initialize d_vars vector
  while (d_cnfManager->numVars() >= d_vars.size()) {
    d_vars.push_back(SmartCDO<SAT::Var::Val>(
                       d_core->getCM()->getCurrentContext(),
                       SAT::Var::UNKNOWN, 0));
  }

  // Run DPLLT engine
  res = isRestart ? d_dpllt->continueCheck(cnf) : d_dpllt->checkSat(cnf);

 finalize:
  if (res == DPLLT::UNSAT) {
    DebugAssert(d_core->getCM()->scopeLevel() == d_bottomScope,
                "Expected unchanged context after unsat");
    e2 = d_lastCheck;
    d_core->getCM()->pop();
    // Next line is a place-holder until we can actually get the proof
    d_lastValid = d_commonRules->assumpRule(e2);
  }
  else {
    DebugAssert(d_lemmasNext == d_lemmas.numClauses(),
                "Expected no lemmas after satisfiable check");
    d_dplltReady = true;
    d_lastValid = Theorem();
  }
  d_cnfManager->setBottomScope(-1);
  d_inCheckSat = false;
  return d_lastValid;
}


SearchSat::SearchSat(TheoryCore* core)
  : SearchEngine(core),
    d_name("sat"),
    d_bottomScope(core->getCM()->getCurrentContext(), -1),
    d_lastCheck(core->getCM()->getCurrentContext()),
    d_lastValid(core->getCM()->getCurrentContext(),
                d_commonRules->trueTheorem()),
    d_userAssumptions(core->getCM()->getCurrentContext()),
    d_intAssumptions(core->getCM()->getCurrentContext()),
    d_idxUserAssump(core->getCM()->getCurrentContext(), 0),
    d_theorems(core->getCM()->getCurrentContext()),
    d_inCheckSat(false),
    d_lemmas(core->getCM()->getCurrentContext()),
    d_lemmasNext(core->getCM()->getCurrentContext(), 0),
    d_rootLits(core->getCM()->getCurrentContext()),
    d_lastRegisteredVar(core->getCM()->getCurrentContext(), 0),
    d_dplltReady(core->getCM()->getCurrentContext(), true),
    d_nextImpliedLiteral(core->getCM()->getCurrentContext(), 0),
    d_restorer(core->getCM()->getCurrentContext(), this)
{
  d_cnfManager = new CNF_Manager(core->getTM());
  d_coreSatAPI = new SearchSatCoreSatAPI(this);
  core->registerCoreSatAPI(d_coreSatAPI);
  d_theoryAPI = new SearchSatTheoryAPI(this);
  d_decider = new SearchSatDecider(this);
  d_dpllt = new DPLLTBasic(d_theoryAPI, d_decider);
}


SearchSat::~SearchSat()
{
  delete d_dpllt;
  delete d_decider;
  delete d_theoryAPI;
  delete d_coreSatAPI;
  delete d_cnfManager;
}


void SearchSat::registerAtom(const Expr& e)
{
  d_core->registerAtom(e);
  e.setUserRegisteredAtom();
}


Theorem SearchSat::getImpliedLiteral(void)
{
  Theorem imp;
  while (d_nextImpliedLiteral < d_core->numImpliedLiterals()) {
    imp = d_core->getImpliedLiteralByIndex(d_nextImpliedLiteral);
    d_nextImpliedLiteral = d_nextImpliedLiteral + 1;
    if (imp.getExpr().unnegate().isUserRegisteredAtom()) return imp;
  }
  return Theorem();
}


void SearchSat::returnFromCheck()
{
  if (d_bottomScope < 0) {
    throw Exception
      ("returnFromCheck called with no previous invalid call to checkValid");
  }
  d_core->getCM()->popto(d_bottomScope);
  d_core->getCM()->pop();
}


Theorem SearchSat::newUserAssumption(const Expr& e, int scope)
{
  DebugAssert(!d_inCheckSat,
              "User assumptions should be added before calling checkSat");
  Theorem thm;
  if (!isAssumption(e)) {
    e.setUserAssumption(scope);
    thm = d_commonRules->assumpRule(e, scope);
    d_userAssumptions.push_back(thm, scope);

    // Immediately propagate facts at current scope level
    if ((scope == -1 || scope == d_core->getCM()->scopeLevel()) &&
        thm.getExpr().isAbsLiteral()) d_core->addFact(thm);
  }
  return thm;
}


void SearchSat::getUserAssumptions(vector<Expr>& assumptions)
{
  for(CDList<Theorem>::const_iterator i=d_userAssumptions.begin(),
        iend=d_userAssumptions.end(); i!=iend; ++i)
    assumptions.push_back((*i).getExpr());
}


void SearchSat::getInternalAssumptions(vector<Expr>& assumptions)
{
  for(CDList<Theorem>::const_iterator i=d_intAssumptions.begin(),
        iend=d_intAssumptions.end(); i!=iend; ++i)
    assumptions.push_back((*i).getExpr());
}


void SearchSat::getAssumptions(vector<Expr>& assumptions)
{
  CDList<Theorem>::const_iterator iU=d_userAssumptions.begin(),
    iUend=d_userAssumptions.end(), iI = d_intAssumptions.begin(),
    iIend=d_intAssumptions.end();
  while (true) {
    if (iI == iIend) {
      if (iU == iUend) break;
      assumptions.push_back((*iU).getExpr());
      ++iU;
    }
    else if (iU == iUend) {
      assumptions.push_back((*iI).getExpr());
      ++iI;
    }
    else {
      if ((*iI).getScope() <= (*iU).getScope()) {
        assumptions.push_back((*iI).getExpr());
        ++iI;
      }
      else {
        assumptions.push_back((*iU).getExpr());
        ++iU;
      }
    }
  }
}


bool SearchSat::isAssumption(const Expr& e)
{
  return e.isUserAssumption() || e.isIntAssumption();
}


void SearchSat::getCounterExample(vector<Expr>& assumptions, bool inOrder)
{
  if (!d_lastValid.get().isNull()) {
    throw Exception("Expected last query to be invalid");
  }
  getInternalAssumptions(assumptions);
}


Proof SearchSat::getProof()
{
  FatalAssert(false, "Not Implemented Yet");
  return Proof();
}

---