Interruption, time-out, and deterministic time-out ("resource-out") features.

Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API
This will need more work, but it's a start.

Also implemented TheoryEngine::properPropagation().

Other minor things.

16 files changed, 577 insertions, 40 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 6adcb62a9..84ed78662 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1191,7 +1191,7 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
 
 inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
                                         TypeNode child2, TypeNode child3) {
-  return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();;
+  return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();
 }
 
 // N-ary version for types
diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 30be07d7c..c9442a401 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -12,6 +12,7 @@ libprop_la_SOURCES = \
 	prop_engine.h \
 	sat.h \
 	sat.cpp \
+	sat_timer.h \
 	cnf_stream.h \
 	cnf_stream.cpp
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index e123db0ed..3d5a27d00 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -62,7 +62,12 @@ public:
 PropEngine::PropEngine(TheoryEngine* te, Context* context) :
   d_inCheckSat(false),
   d_theoryEngine(te),
-  d_context(context) {
+  d_context(context),
+  d_satSolver(NULL),
+  d_cnfStream(NULL),
+  d_satTimer(*this),
+  d_interrupted(false) {
+
   Debug("prop") << "Constructing the PropEngine" << endl;
 
   d_satSolver = new SatSolver(this, d_theoryEngine, d_context);
@@ -121,7 +126,7 @@ void PropEngine::printSatisfyingAssignment(){
   }
 }
 
-Result PropEngine::checkSat() {
+Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
   Debug("prop") << "PropEngine::checkSat()" << endl;
 
@@ -133,22 +138,37 @@ Result PropEngine::checkSat() {
   d_theoryEngine->presolve();
 
   if(Options::current()->preprocessOnly) {
+    millis = resource = 0;
     return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
   }
 
+  // Set the timer
+  d_satTimer.set(millis);
+
+  // Reset the interrupted flag
+  d_interrupted = false;
+
   // Check the problem
-  bool result = d_satSolver->solve();
+  SatLiteralValue result = d_satSolver->solve(resource);
+
+  millis = d_satTimer.elapsed();
 
-  if( result && Debug.isOn("prop") ) {
+  if( result == l_Undef ) {
+    Result::UnknownExplanation why =
+      d_satTimer.expired() ? Result::TIMEOUT :
+        (d_interrupted ? Result::INTERRUPTED : Result::RESOURCEOUT);
+    return Result(Result::SAT_UNKNOWN, why);
+  }
+
+  if( result == l_True && Debug.isOn("prop") ) {
     printSatisfyingAssignment();
   }
 
-  Debug("prop") << "PropEngine::checkSat() => "
-                << (result ? "true" : "false") << endl;
-  if(result && d_theoryEngine->isIncomplete()) {
+  Debug("prop") << "PropEngine::checkSat() => " << result << endl;
+  if(result == l_True && d_theoryEngine->isIncomplete()) {
     return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE);
   }
-  return Result(result ? Result::SAT : Result::UNSAT);
+  return Result(result == l_True ? Result::SAT : Result::UNSAT);
 }
 
 Node PropEngine::getValue(TNode node) {
@@ -170,6 +190,10 @@ bool PropEngine::isSatLiteral(TNode node) {
   return d_cnfStream->hasLiteral(node);
 }
 
+bool PropEngine::isTranslatedSatLiteral(TNode node) {
+  return d_cnfStream->isTranslated(node);
+}
+
 bool PropEngine::hasValue(TNode node, bool& value) {
   Assert(node.getType().isBoolean());
   SatLiteral lit = d_cnfStream->getLiteral(node);
@@ -203,5 +227,20 @@ void PropEngine::pop() {
   Debug("prop") << "pop()" << endl;
 }
 
+void PropEngine::interrupt() throw(ModalException) {
+  if(! d_inCheckSat) {
+    throw ModalException("SAT solver is not currently solving anything; "
+                         "cannot interrupt it");
+  }
+
+  d_interrupted = true;
+  d_satSolver->interrupt();
+  Debug("prop") << "interrupt()" << endl;
+}
+
+void PropEngine::spendResource() throw() {
+  // TODO implement me
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 16cb34e04..25697b856 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -26,6 +26,9 @@
 #include "expr/node.h"
 #include "util/options.h"
 #include "util/result.h"
+#include "smt/modal_exception.h"
+
+#include <sys/time.h>
 
 namespace CVC4 {
 
@@ -36,6 +39,80 @@ namespace prop {
 class CnfStream;
 class SatSolver;
 
+class PropEngine;
+
+/**
+ * A helper class to keep track of a time budget and signal
+ * the PropEngine when the budget expires.
+ */
+class SatTimer {
+
+  PropEngine& d_propEngine;
+  unsigned long d_ms;
+  timeval d_limit;
+
+public:
+
+  /** Construct a SatTimer attached to the given PropEngine. */
+  SatTimer(PropEngine& propEngine) :
+    d_propEngine(propEngine),
+    d_ms(0) {
+  }
+
+  /** Is the timer currently active? */
+  bool on() const {
+    return d_ms != 0;
+  }
+
+  /** Set a millisecond timer (0==off). */
+  void set(unsigned long millis) {
+    d_ms = millis;
+    // keep track of when it was set, even if it's disabled (i.e. == 0)
+    Trace("limit") << "SatTimer::set(" << d_ms << ")" << std::endl;
+    gettimeofday(&d_limit, NULL);
+    Trace("limit") << "SatTimer::set(): it's " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
+    d_limit.tv_sec += millis / 1000;
+    d_limit.tv_usec += (millis % 1000) * 1000;
+    if(d_limit.tv_usec > 1000000) {
+      ++d_limit.tv_sec;
+      d_limit.tv_usec -= 1000000;
+    }
+    Trace("limit") << "SatTimer::set(): limit is at " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
+  }
+
+  /** Return the milliseconds elapsed since last set(). */
+  unsigned long elapsed() {
+    timeval tv;
+    gettimeofday(&tv, NULL);
+    Trace("limit") << "SatTimer::elapsed(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl;
+    tv.tv_sec -= d_limit.tv_sec - d_ms / 1000;
+    tv.tv_usec -= d_limit.tv_usec - (d_ms % 1000) * 1000;
+    Trace("limit") << "SatTimer::elapsed(): elapsed time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
+    return tv.tv_sec * 1000 + tv.tv_usec / 1000;
+  }
+
+  bool expired() {
+    if(on()) {
+      timeval tv;
+      gettimeofday(&tv, NULL);
+      Trace("limit") << "SatTimer::expired(): current time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
+      Trace("limit") << "SatTimer::expired(): limit time is " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
+      if(d_limit.tv_sec < tv.tv_sec ||
+         (d_limit.tv_sec == tv.tv_sec && d_limit.tv_usec <= tv.tv_usec)) {
+        Trace("limit") << "SatTimer::expired(): OVER LIMIT!" << std::endl;
+        return true;
+      } else {
+        Trace("limit") << "SatTimer::expired(): within limit" << std::endl;
+      }
+    }
+    return false;
+  }
+
+  /** Check the current time and signal the PropEngine if over-time. */
+  void check();
+
+};/* class SatTimer */
+
 /**
  * PropEngine is the abstraction of a Sat Solver, providing methods for
  * solving the SAT problem and conversion to CNF (via the CnfStream).
@@ -43,7 +120,7 @@ class SatSolver;
 class PropEngine {
 
   /**
-   * Indicates that the sat solver is currently solving something and we should
+   * Indicates that the SAT solver is currently solving something and we should
    * not mess with it's internal state.
    */
   bool d_inCheckSat;
@@ -51,6 +128,7 @@ class PropEngine {
   /** The theory engine we will be using */
   TheoryEngine *d_theoryEngine;
 
+  /** The context */
   context::Context* d_context;
 
   /** The SAT solver proxy */
@@ -62,6 +140,13 @@ class PropEngine {
   /** The CNF converter in use */
   CnfStream* d_cnfStream;
 
+  /** A timer for SAT calls */
+  SatTimer d_satTimer;
+
+  /** Whether we were just interrupted (or not) */
+  bool d_interrupted;
+
+  /** Dump out the satisfying assignment (after SAT result) */
   void printSatisfyingAssignment();
 
 public:
@@ -86,27 +171,34 @@ public:
   void shutdown() { }
 
   /**
-   * Converts the given formula to CNF and assert the CNF to the sat solver.
+   * Converts the given formula to CNF and assert the CNF to the SAT solver.
    * The formula is asserted permanently for the current context.
    * @param node the formula to assert
    */
   void assertFormula(TNode node);
 
   /**
-   * Converts the given formula to CNF and assert the CNF to the sat solver.
-   * The formula can be removed by the sat solver after backtracking lower
+   * Converts the given formula to CNF and assert the CNF to the SAT solver.
+   * The formula can be removed by the SAT solver after backtracking lower
    * than the (SAT and SMT) level at which it was asserted.
    *
    * @param node the formula to assert
-   * @param negated whether the node should be considered to be negated at the top level (or not)
-   * @param removable whether this lemma can be quietly removed based on an activity heuristic (or not)
+   * @param negated whether the node should be considered to be negated
+   * at the top level (or not)
+   * @param removable whether this lemma can be quietly removed based
+   * on an activity heuristic (or not)
    */
   void assertLemma(TNode node, bool negated, bool removable);
 
   /**
    * Checks the current context for satisfiability.
+   *
+   * @param millis the time limit for this call in milliseconds
+   * (0==off); on output, it is set to the milliseconds used
+   * @param on input, resource the number of resource units permitted
+   * for this call (0==off); on output, it is set to the resource used
    */
-  Result checkSat();
+  Result checkSat(unsigned long& millis, unsigned long& resource);
 
   /**
    * Get the value of a boolean variable.
@@ -116,12 +208,19 @@ public:
    */
   Node getValue(TNode node);
 
-  /*
-   * Return true if node has an associated SAT literal
+  /**
+   * Return true if node has an associated SAT literal.
    */
   bool isSatLiteral(TNode node);
 
   /**
+   * Return true if node has an associated SAT literal that is
+   * currently translated (i.e., it's relevant to the current
+   * user push/pop level).
+   */
+  bool isTranslatedSatLiteral(TNode node);
+
+  /**
    * Check if the node has a value and return it if yes.
    */
   bool hasValue(TNode node, bool& value);
@@ -143,8 +242,37 @@ public:
    */
   void pop();
 
+  /**
+   * Check the current time budget.
+   */
+  void checkTime();
+
+  /**
+   * Interrupt a running solver (cause a timeout).
+   */
+  void interrupt() throw(ModalException);
+
+  /**
+   * "Spend" a "resource."  If the sum of these externally-counted
+   * resources and SAT-internal resources exceed the current limit,
+   * SAT should terminate.
+   */
+  void spendResource() throw();
+
 };/* class PropEngine */
 
+
+inline void SatTimer::check() {
+  if(expired()) {
+    Trace("limit") << "SatTimer::check(): interrupt!" << std::endl;
+    d_propEngine.interrupt();
+  }
+}
+
+inline void PropEngine::checkTime() {
+  d_satTimer.check();
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 386fb5aad..5d53bf100 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -83,6 +83,7 @@ TNode SatSolver::getNode(SatLiteral lit) {
 }
 
 void SatSolver::notifyRestart() {
+  d_propEngine->checkTime();
   d_theoryEngine->notifyRestart();
 }
 
@@ -108,6 +109,9 @@ void SatSolver::logDecision(SatLiteral lit) {
 #endif /* CVC4_REPLAY */
 }
 
+void SatSolver::checkTime() {
+  d_propEngine->checkTime();
+}
 
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/sat.h b/src/prop/sat.h
index ee3978555..026193eae 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -114,6 +114,8 @@ public:
   virtual void unregisterVar(SatLiteral lit) = 0;
   /** Register the variable (of the literal) for solving */
   virtual void renewVar(SatLiteral lit, int level = -1) = 0;
+  /** Interrupt the solver */
+  virtual void interrupt() = 0;
 };
 
 /**
@@ -214,7 +216,7 @@ public:
 
   virtual ~SatSolver();
 
-  bool solve();
+  SatLiteralValue solve(unsigned long& resource);
 
   void addClause(SatClause& clause, bool removable);
 
@@ -253,6 +255,8 @@ public:
 
   void renewVar(SatLiteral lit, int level = -1);
 
+  void interrupt();
+
   TNode getNode(SatLiteral lit);
 
   void notifyRestart();
@@ -261,6 +265,8 @@ public:
 
   void logDecision(SatLiteral lit);
 
+  void checkTime();
+
 };/* class SatSolver */
 
 /* Functions that delegate to the concrete SAT solver. */
@@ -293,8 +299,20 @@ inline SatSolver::~SatSolver() {
   delete d_minisat;
 }
 
-inline bool SatSolver::solve() {
-  return d_minisat->solve();
+inline SatLiteralValue SatSolver::solve(unsigned long& resource) {
+  Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
+  if(resource == 0) {
+    d_minisat->budgetOff();
+  } else {
+    d_minisat->setConfBudget(resource);
+  }
+  Minisat::vec<SatLiteral> empty;
+  unsigned long conflictsBefore = d_minisat->conflicts;
+  SatLiteralValue result = d_minisat->solveLimited(empty);
+  d_minisat->clearInterrupt();
+  resource = d_minisat->conflicts - conflictsBefore;
+  Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
+  return result;
 }
 
 inline void SatSolver::addClause(SatClause& clause, bool removable) {
@@ -333,6 +351,10 @@ inline void SatSolver::renewVar(SatLiteral lit, int level) {
   d_minisat->renewVar(lit, level);
 }
 
+inline void SatSolver::interrupt() {
+  d_minisat->interrupt();
+}
+
 #endif /* __CVC4_USE_MINISAT */
 
 inline size_t
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f80d9a135..ecd61c0b4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -180,9 +180,25 @@ using namespace CVC4::smt;
 
 SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_context(em->getContext()),
+  d_userLevels(),
   d_userContext(new UserContext()),
   d_exprManager(em),
   d_nodeManager(d_exprManager->getNodeManager()),
+  d_theoryEngine(NULL),
+  d_propEngine(NULL),
+  d_definedFunctions(NULL),
+  d_assertionList(NULL),
+  d_assignments(NULL),
+  d_logic(""),
+  d_problemExtended(false),
+  d_queryMade(false),
+  d_timeBudgetCumulative(0),
+  d_timeBudgetPerCall(0),
+  d_resourceBudgetCumulative(0),
+  d_resourceBudgetPerCall(0),
+  d_cumulativeTimeUsed(0),
+  d_cumulativeResourceUsed(0),
+  d_status(),
   d_private(new smt::SmtEnginePrivate(*this)),
   d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
   d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
@@ -212,14 +228,22 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
 
   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
 
-  d_assertionList = NULL;
   if(Options::current()->interactive) {
     d_assertionList = new(true) AssertionList(d_userContext);
   }
 
-  d_assignments = NULL;
-  d_problemExtended = false;
-  d_queryMade = false;
+  if(Options::current()->perCallResourceLimit != 0) {
+    setResourceLimit(Options::current()->perCallResourceLimit, false);
+  }
+  if(Options::current()->cumulativeResourceLimit != 0) {
+    setResourceLimit(Options::current()->cumulativeResourceLimit, true);
+  }
+  if(Options::current()->perCallMillisecondLimit != 0) {
+    setTimeLimit(Options::current()->perCallMillisecondLimit, false);
+  }
+  if(Options::current()->cumulativeMillisecondLimit != 0) {
+    setTimeLimit(Options::current()->cumulativeMillisecondLimit, true);
+  }
 }
 
 void SmtEngine::shutdown() {
@@ -719,12 +743,44 @@ void SmtEnginePrivate::simplifyAssertions()
 Result SmtEngine::check() {
   Trace("smt") << "SmtEngine::check()" << endl;
 
-  // make sure the prop layer has all assertions
-  Trace("smt") << "SmtEngine::check(): processing assertion" << endl;
+  // Make sure the prop layer has all of the assertions
+  Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
   d_private->processAssertions();
 
+  unsigned long millis = 0;
+  if(d_timeBudgetCumulative != 0) {
+    millis = getTimeRemaining();
+    if(millis == 0) {
+      return Result(Result::VALIDITY_UNKNOWN, Result::TIMEOUT);
+    }
+  }
+  if(d_timeBudgetPerCall != 0 && (millis == 0 || d_timeBudgetPerCall < millis)) {
+    millis = d_timeBudgetPerCall;
+  }
+
+  unsigned long resource = 0;
+  if(d_resourceBudgetCumulative != 0) {
+    resource = getResourceRemaining();
+    if(resource == 0) {
+      return Result(Result::VALIDITY_UNKNOWN, Result::RESOURCEOUT);
+    }
+  }
+  if(d_resourceBudgetPerCall != 0 && (resource == 0 || d_resourceBudgetPerCall < resource)) {
+    resource = d_resourceBudgetPerCall;
+  }
+
   Trace("smt") << "SmtEngine::check(): running check" << endl;
-  return d_propEngine->checkSat();
+  Result result = d_propEngine->checkSat(millis, resource);
+
+  // PropEngine::checkSat() returns the actual amount used in these
+  // variables.
+  d_cumulativeTimeUsed += millis;
+  d_cumulativeResourceUsed += resource;
+
+  Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
+                 << ", conflicts " << d_cumulativeResourceUsed << std::endl;
+
+  return result;
 }
 
 Result SmtEngine::quickCheck() {
@@ -1082,6 +1138,9 @@ void SmtEngine::pop() {
   if(!Options::current()->incrementalSolving) {
     throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
   }
+  if(d_userContext->getLevel() == 0) {
+    throw ModalException("Cannot pop beyond the first user frame");
+  }
   AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel());
   while (d_userLevels.back() < d_userContext->getLevel()) {
     internalPop();
@@ -1113,6 +1172,56 @@ void SmtEngine::internalPop() {
   }
 }
 
+void SmtEngine::interrupt() throw(ModalException) {
+  d_propEngine->interrupt();
+}
+
+void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {
+  if(cumulative) {
+    Trace("limit") << "SmtEngine: setting cumulative resource limit to " << units << std::endl;
+    d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units);
+  } else {
+    Trace("limit") << "SmtEngine: setting per-call resource limit to " << units << std::endl;
+    d_resourceBudgetPerCall = units;
+  }
+}
+
+void SmtEngine::setTimeLimit(unsigned long millis, bool cumulative) {
+  if(cumulative) {
+    Trace("limit") << "SmtEngine: setting cumulative time limit to " << millis << " ms" << std::endl;
+    d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis);
+  } else {
+    Trace("limit") << "SmtEngine: setting per-call time limit to " << millis << " ms" << std::endl;
+    d_timeBudgetPerCall = millis;
+  }
+}
+
+unsigned long SmtEngine::getResourceUsage() const {
+  return d_cumulativeResourceUsed;
+}
+
+unsigned long SmtEngine::getTimeUsage() const {
+  return d_cumulativeTimeUsed;
+}
+
+unsigned long SmtEngine::getResourceRemaining() const throw(ModalException) {
+  if(d_resourceBudgetCumulative == 0) {
+    throw ModalException("No cumulative resource limit is currently set");
+  }
+
+  return d_resourceBudgetCumulative <= d_cumulativeResourceUsed ? 0 :
+    d_resourceBudgetCumulative - d_cumulativeResourceUsed;
+}
+
+unsigned long SmtEngine::getTimeRemaining() const throw(ModalException) {
+  if(d_timeBudgetCumulative == 0) {
+    throw ModalException("No cumulative time limit is currently set");
+  }
+
+  return d_timeBudgetCumulative <= d_cumulativeTimeUsed ? 0 :
+    d_timeBudgetCumulative - d_cumulativeTimeUsed;
+}
+
 StatisticsRegistry* SmtEngine::getStatisticsRegistry() const {
   return d_exprManager->d_nodeManager->getStatisticsRegistry();
 }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f5036bed7..f898ee76a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -104,7 +104,7 @@ class CVC4_PUBLIC SmtEngine {
 
   /** Our expression manager */
   ExprManager* d_exprManager;
-  /** Out internal expression/node manager */
+  /** Our internal expression/node manager */
   NodeManager* d_nodeManager;
   /** The decision engine */
   TheoryEngine* d_theoryEngine;
@@ -143,6 +143,20 @@ class CVC4_PUBLIC SmtEngine {
    */
   bool d_queryMade;
 
+  /** A user-imposed cumulative time budget, in milliseconds.  0 = no limit. */
+  unsigned long d_timeBudgetCumulative;
+  /** A user-imposed per-call time budget, in milliseconds.  0 = no limit. */
+  unsigned long d_timeBudgetPerCall;
+  /** A user-imposed cumulative resource budget.  0 = no limit. */
+  unsigned long d_resourceBudgetCumulative;
+  /** A user-imposed per-call resource budget.  0 = no limit. */
+  unsigned long d_resourceBudgetPerCall;
+
+  /** The number of milliseconds used by this SmtEngine since its inception. */
+  unsigned long d_cumulativeTimeUsed;
+  /** The amount of resource used by this SmtEngine since its inception. */
+  unsigned long d_cumulativeResourceUsed;
+
   /**
    * Most recent result of last checkSat/query or (set-info :status).
    */
@@ -324,6 +338,104 @@ public:
   void pop();
 
   /**
+   * Interrupt a running query.  This can be called from another thread
+   * or from a signal handler.  Throws a ModalException if the SmtEngine
+   * isn't currently in a query.
+   */
+  void interrupt() throw(ModalException);
+
+  /**
+   * Set a resource limit for SmtEngine operations.  This is like a time
+   * limit, but it's deterministic so that reproducible results can be
+   * obtained.  However, please note that it may not be deterministic
+   * between different versions of CVC4, or even the same version on
+   * different platforms.
+   *
+   * A cumulative and non-cumulative (per-call) resource limit can be
+   * set at the same time.  A call to setResourceLimit() with
+   * cumulative==true replaces any cumulative resource limit currently
+   * in effect; a call with cumulative==false replaces any per-call
+   * resource limit currently in effect.  Time limits can be set in
+   * addition to resource limits; the SmtEngine obeys both.  That means
+   * that up to four independent limits can control the SmtEngine
+   * at the same time.
+   *
+   * When an SmtEngine is first created, it has no time or resource
+   * limits.
+   *
+   * Currently, these limits only cause the SmtEngine to stop what its
+   * doing when the limit expires (or very shortly thereafter); no
+   * heuristics are altered by the limits or the threat of them expiring.
+   * We reserve the right to change this in the future.
+   *
+   * @param units the resource limit, or 0 for no limit
+   * @param cumulative whether this resource limit is to be a cumulative
+   * resource limit for all remaining calls into the SmtEngine (true), or
+   * whether it's a per-call resource limit (false); the default is false
+   */
+  void setResourceLimit(unsigned long units, bool cumulative = false);
+
+  /**
+   * Set a time limit for SmtEngine operations.
+   *
+   * A cumulative and non-cumulative (per-call) time limit can be
+   * set at the same time.  A call to setTimeLimit() with
+   * cumulative==true replaces any cumulative time limit currently
+   * in effect; a call with cumulative==false replaces any per-call
+   * time limit currently in effect.  Resource limits can be set in
+   * addition to time limits; the SmtEngine obeys both.  That means
+   * that up to four independent limits can control the SmtEngine
+   * at the same time.
+   *
+   * Note that the cumulative timer only ticks away when one of the
+   * SmtEngine's workhorse functions (things like assertFormula(),
+   * query(), checkSat(), and simplify()) are running.  Between calls,
+   * the timer is still.
+   *
+   * When an SmtEngine is first created, it has no time or resource
+   * limits.
+   *
+   * Currently, these limits only cause the SmtEngine to stop what its
+   * doing when the limit expires (or very shortly thereafter); no
+   * heuristics are altered by the limits or the threat of them expiring.
+   * We reserve the right to change this in the future.
+   *
+   * @param millis the time limit in milliseconds, or 0 for no limit
+   * @param cumulative whether this time limit is to be a cumulative
+   * time limit for all remaining calls into the SmtEngine (true), or
+   * whether it's a per-call time limit (false); the default is false
+   */
+  void setTimeLimit(unsigned long millis, bool cumulative = false);
+
+  /**
+   * Get the current resource usage count for this SmtEngine.  This
+   * function can be used to ascertain reasonable values to pass as
+   * resource limits to setResourceLimit().
+   */
+  unsigned long getResourceUsage() const;
+
+  /**
+   * Get the current millisecond count for this SmtEngine.
+   */
+  unsigned long getTimeUsage() const;
+
+  /**
+   * Get the remaining resources that can be consumed by this SmtEngine
+   * according to the currently-set cumulative resource limit.  If there
+   * is not a cumulative resource limit set, this function throws a
+   * ModalException.
+   */
+  unsigned long getResourceRemaining() const throw(ModalException);
+
+  /**
+   * Get the remaining number of milliseconds that can be consumed by
+   * this SmtEngine according to the currently-set cumulative time limit.
+   * If there is not a cumulative resource limit set, this function
+   * throws a ModalException.
+   */
+  unsigned long getTimeRemaining() const throw(ModalException);
+
+  /**
    * Permit access to the underlying StatisticsRegistry.
    */
   StatisticsRegistry* getStatisticsRegistry() const;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index 941b9d0b4..851a6893c 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -277,7 +277,7 @@ bool RewriteRule<ReflexivityEq>::applies(Node node) {
 template<>
 Node RewriteRule<ReflexivityEq>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl;
-  return node[1].eqNode(node[0]);;
+  return node[1].eqNode(node[0]);
 }
 
 }
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index f5bf620bf..625abc580 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -105,6 +105,20 @@ public:
    */
   virtual void setIncomplete() throw(AssertionException) = 0;
 
+  /**
+   * "Spend" a "resource."  The meaning is specific to the context in
+   * which the theory is operating, and may even be ignored.  The
+   * intended meaning is that if the user has set a limit on the "units
+   * of resource" that can be expended in a search, and that limit is
+   * exceeded, then the search is terminated.  Note that the check for
+   * termination occurs in the main search loop, so while theories
+   * should call OutputChannel::spendResource() during particularly
+   * long-running operations, they cannot rely on resource() to break
+   * out of infinite or intractable computations.
+   */
+  virtual void spendResource() throw() {
+  }
+
 };/* class OutputChannel */
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2d4672776..2cd3f4d72 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -100,6 +100,8 @@ void TheoryEngine::preRegister(TNode preprocessed) {
  */
 void TheoryEngine::check(Theory::Effort effort) {
 
+  d_propEngine->checkTime();
+
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
@@ -263,20 +265,38 @@ bool TheoryEngine::properConflict(TNode conflict) const {
   bool value;
   if (conflict.getKind() == kind::AND) {
     for (unsigned i = 0; i < conflict.getNumChildren(); ++ i) {
-      if (!getPropEngine()->hasValue(conflict[i], value)) return false;
-      if (!value) return false;
+      if (! getPropEngine()->hasValue(conflict[i], value)) {
+        Debug("properConflict") << "Bad conflict is due to unassigned atom: "
+                                << conflict[i] << endl;
+        return false;
+      }
+      if (! value) {
+        Debug("properConflict") << "Bad conflict is due to false atom: "
+                                << conflict[i] << endl;
+        return false;
+      }
     }
   } else {
-    if (!getPropEngine()->hasValue(conflict, value)) return false;
-    return value;
+    if (! getPropEngine()->hasValue(conflict, value)) {
+      Debug("properConflict") << "Bad conflict is due to unassigned atom: "
+                              << conflict << endl;
+      return false;
+    }
+    if(! value) {
+      Debug("properConflict") << "Bad conflict is due to false atom: "
+                              << conflict << endl;
+      return false;
+    }
   }
   return true;
 }
 
 bool TheoryEngine::properPropagation(TNode lit) const {
-  Assert(!lit.isNull());
-#warning implement TheoryEngine::properPropagation()
-  return true;
+  if(!getPropEngine()->isTranslatedSatLiteral(lit)) {
+    return false;
+  }
+  bool b;
+  return !getPropEngine()->hasValue(lit, b);
 }
 
 bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
@@ -471,6 +491,8 @@ void TheoryEngine::assertFact(TNode node)
 {
   Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
 
+  d_propEngine->checkTime();
+
   // Get the atom
   TNode atom = node.getKind() == kind::NOT ? node[0] : node;
 
@@ -497,6 +519,8 @@ void TheoryEngine::assertFact(TNode node)
 void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
       
   Debug("theory") << "EngineOutputChannel::propagate(" << literal << ")" << std::endl;
+
+  d_propEngine->checkTime();
       
   if(Dump.isOn("t-propagations")) {
     Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid") << std::endl
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 915373074..be3068a45 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -209,6 +209,11 @@ class TheoryEngine {
     void setIncomplete() throw(AssertionException) {
       d_engine->setIncomplete(d_theory);
     }
+
+    void spendResource() throw() {
+      d_engine->spendResource();
+    }
+
   };/* class EngineOutputChannel */
 
   /**
@@ -223,7 +228,7 @@ class TheoryEngine {
 
   void conflict(TNode conflict) {
 
-    Assert(properConflict(conflict));
+    Assert(properConflict(conflict), "not a proper conflict: %s", conflict.toString().c_str());
 
     // Mark that we are in conflict
     d_inConflict = true;
@@ -257,6 +262,13 @@ class TheoryEngine {
   }
 
   /**
+   * "Spend" a resource during a search or preprocessing.
+   */
+  void spendResource() throw() {
+    d_propEngine->spendResource();
+  }
+
+  /**
    * Is the theory active.
    */
   bool isActive(theory::TheoryId theory) {
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 9c438a5cd..a01237fd0 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -138,7 +138,11 @@ static const string optionsDescription = "\
    --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\
    --disable-arithmetic-propagation turns on arithmetic propagation\n\
    --disable-symmetry-breaker turns off UF symmetry breaker (Deharbe et al., CADE 2011)\n\
-   --incremental | -i     enable incremental solving\n";
+   --incremental | -i     enable incremental solving\n\
+   --time-limit=MS        enable time limiting (give milliseconds)\n\
+   --time-limit-per=MS    enable time limiting per query (give milliseconds)\n\
+   --limit=N              enable resource limiting\n\
+   --limit-per=N          enable resource limiting per query\n";
 
 #warning "Change CL options as --disable-variable-removal cannot do anything currently."
 
@@ -296,7 +300,11 @@ enum OptionValue {
   ARITHMETIC_PROPAGATION,
   ARITHMETIC_PIVOT_THRESHOLD,
   ARITHMETIC_PROP_MAX_LENGTH,
-  DISABLE_SYMMETRY_BREAKER
+  DISABLE_SYMMETRY_BREAKER,
+  TIME_LIMIT,
+  TIME_LIMIT_PER,
+  LIMIT,
+  LIMIT_PER
 };/* enum OptionValue */
 
 /**
@@ -371,6 +379,10 @@ static struct option cmdlineOptions[] = {
   { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL },
   { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
   { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER },
+  { "time-limit" , required_argument, NULL, TIME_LIMIT  },
+  { "time-limit-per", required_argument, NULL, TIME_LIMIT_PER },
+  { "limit"      , required_argument, NULL, LIMIT       },
+  { "limit-per"  , required_argument, NULL, LIMIT_PER   },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -677,6 +689,43 @@ throw(OptionException) {
       ufSymmetryBreaker = false;
       break;
 
+    case TIME_LIMIT:
+      {
+        int i = atoi(optarg);
+        if(i < 0) {
+          throw OptionException("--time-limit requires a nonnegative argument.");
+        }
+        cumulativeMillisecondLimit = (unsigned long) i;
+      }
+      break;
+    case TIME_LIMIT_PER:
+      {
+        int i = atoi(optarg);
+        if(i < 0) {
+          throw OptionException("--time-limit-per requires a nonnegative argument.");
+        }
+        perCallMillisecondLimit = (unsigned long) i;
+      }
+      break;
+    case LIMIT:
+      {
+        int i = atoi(optarg);
+        if(i < 0) {
+          throw OptionException("--limit requires a nonnegative argument.");
+        }
+        cumulativeResourceLimit = (unsigned long) i;
+      }
+      break;
+    case LIMIT_PER:
+      {
+        int i = atoi(optarg);
+        if(i < 0) {
+          throw OptionException("--limit-per requires a nonnegative argument.");
+        }
+        perCallResourceLimit = (unsigned long) i;
+        break;
+      }
+
     case RANDOM_SEED:
       satRandomSeed = atof(optarg);
       break;
diff --git a/src/util/options.h b/src/util/options.h
index 7fc894d93..f9dc042d1 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -129,6 +129,16 @@ struct CVC4_PUBLIC Options {
    */
   bool interactiveSetByUser;
 
+  /** Per-query resource limit. */
+  unsigned long perCallResourceLimit;
+  /** Cumulative resource limit. */
+  unsigned long cumulativeResourceLimit;
+
+  /** Per-query time limit in milliseconds. */
+  unsigned long perCallMillisecondLimit;
+  /** Cumulative time limit in milliseconds. */
+  unsigned long cumulativeMillisecondLimit;
+
   /** Whether we should "spin" on a SIG_SEGV. */
   bool segvNoSpin;
 
diff --git a/src/util/result.cpp b/src/util/result.cpp
index 8a2bcf3b2..bdb17f54c 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -55,10 +55,18 @@ Result::Result(const std::string& instr) :
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
     d_unknownExplanation = TIMEOUT;
+  } else if(s == "resourceout") {
+    d_which = TYPE_SAT;
+    d_sat = SAT_UNKNOWN;
+    d_unknownExplanation = RESOURCEOUT;
   } else if(s == "memout") {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
     d_unknownExplanation = MEMOUT;
+  } else if(s == "interrupted") {
+    d_which = TYPE_SAT;
+    d_sat = SAT_UNKNOWN;
+    d_unknownExplanation = INTERRUPTED;
   } else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
@@ -169,8 +177,11 @@ ostream& operator<<(ostream& out,
   case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break;
   case Result::INCOMPLETE: out << "INCOMPLETE"; break;
   case Result::TIMEOUT: out << "TIMEOUT"; break;
+  case Result::RESOURCEOUT: out << "RESOURCEOUT"; break;
   case Result::MEMOUT: out << "MEMOUT"; break;
+  case Result::INTERRUPTED: out << "INTERRUPTED"; break;
   case Result::NO_STATUS: out << "NO_STATUS"; break;
+  case Result::UNSUPPORTED: out << "UNSUPPORTED"; break;
   case Result::OTHER: out << "OTHER"; break;
   case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break;
   default: Unhandled(e);
diff --git a/src/util/result.h b/src/util/result.h
index c4733eab9..ac52ee382 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -59,7 +59,9 @@ public:
     REQUIRES_FULL_CHECK,
     INCOMPLETE,
     TIMEOUT,
+    RESOURCEOUT,
     MEMOUT,
+    INTERRUPTED,
     NO_STATUS,
     UNSUPPORTED,
     OTHER,