Partial merge of integers work; this is simple B&B and some pseudoboolean

infrastructure, and takes care not to affect CVC4's performance on LRA
benchmarks.

25 files changed, 704 insertions, 60 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 7f193b9e3..36ab2cd68 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -32,7 +32,9 @@ libarith_la_SOURCES = \
 	simplex.h \
 	simplex.cpp \
 	theory_arith.h \
-	theory_arith.cpp
+	theory_arith.cpp \
+	dio_solver.h \
+	dio_solver.cpp
 
 EXTRA_DIST = \
 	kinds
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index d2ecaffe4..8d12e78fe 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -182,7 +182,6 @@ RewriteResponse ArithRewriter::postRewriteAtomConstantRHS(TNode t){
   TNode left  = t[0];
   TNode right = t[1];
 
-
   Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right));
 
   if(cmp.isBoolean()){
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 77a89b54b..a5fa428c6 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -24,6 +24,9 @@
 
 #include "util/propositional_query.h"
 
+#include "expr/expr.h"
+#include "expr/convenience_node_builders.h"
+
 #include <vector>
 
 using namespace std;
@@ -34,9 +37,10 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
 
-ArithStaticLearner::ArithStaticLearner():
+ArithStaticLearner::ArithStaticLearner(SubstitutionMap& pbSubstitutions) :
   d_miplibTrick(),
   d_miplibTrickKeys(),
+  d_pbSubstitutions(pbSubstitutions),
   d_statistics()
 {}
 
@@ -105,9 +109,11 @@ void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){
   postProcess(learned);
 }
 
+
 void ArithStaticLearner::clear(){
   d_miplibTrick.clear();
   d_miplibTrickKeys.clear();
+  // do not clear d_pbSubstitutions, as it is shared
 }
 
 
@@ -151,11 +157,101 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
     d_minMap[n] = coerceToRational(n);
     d_maxMap[n] = coerceToRational(n);
     break;
+  case OR: {
+    // Look for things like "x = 0 OR x = 1" (that are defTrue) and
+    // turn them into a pseudoboolean.  We catch "x >= 0
+    if(defTrue.find(n) == defTrue.end() ||
+       n.getNumChildren() != 2 ||
+       n[0].getKind() != EQUAL ||
+       n[1].getKind() != EQUAL) {
+      break;
+    }
+    Node var, c1, c2;
+    if(n[0][0].getMetaKind() == metakind::VARIABLE &&
+       n[0][1].getMetaKind() == metakind::CONSTANT) {
+      var = n[0][0];
+      c1 = n[0][1];
+    } else if(n[0][1].getMetaKind() == metakind::VARIABLE &&
+              n[0][0].getMetaKind() == metakind::CONSTANT) {
+      var = n[0][1];
+      c1 = n[0][0];
+    } else {
+      break;
+    }
+    if(!var.getType().isInteger() ||
+       !c1.getType().isReal()) {
+      break;
+    }
+    if(var == n[1][0]) {
+      c2 = n[1][1];
+    } else if(var == n[1][1]) {
+      c2 = n[1][0];
+    } else {
+      break;
+    }
+    if(!c2.getType().isReal()) {
+      break;
+    }
+
+    Integer k1, k2;
+    if(c1.getType().getConst<TypeConstant>() == INTEGER_TYPE) {
+      k1 = c1.getConst<Integer>();
+    } else {
+      Rational r = c1.getConst<Rational>();
+      if(r.getDenominator() == 1) {
+        k1 = r.getNumerator();
+      } else {
+        break;
+      }
+    }
+    if(c2.getType().getConst<TypeConstant>() == INTEGER_TYPE) {
+      k2 = c2.getConst<Integer>();
+    } else {
+      Rational r = c2.getConst<Rational>();
+      if(r.getDenominator() == 1) {
+        k2 = r.getNumerator();
+      } else {
+        break;
+      }
+    }
+    if(k1 > k2) {
+      swap(k1, k2);
+    }
+    if(k1 + 1 == k2) {
+      Debug("arith::static") << "==> found " << n << endl
+                             << "    which indicates " << var << " \\in { "
+                             << k1 << " , " << k2 << " }" << endl;
+      c1 = NodeManager::currentNM()->mkConst(k1);
+      c2 = NodeManager::currentNM()->mkConst(k2);
+      Node lhs = NodeBuilder<2>(kind::GEQ) << var << c1;
+      Node rhs = NodeBuilder<2>(kind::LEQ) << var << c2;
+      Node l = lhs && rhs;
+      Debug("arith::static") << "    learned: " << l << endl;
+      learned << l;
+      if(k1 == 0) {
+        Assert(k2 == 1);
+        replaceWithPseudoboolean(var);
+      }
+    }
+    break;
+  }
   default: // Do nothing
     break;
   }
 }
 
+void ArithStaticLearner::replaceWithPseudoboolean(TNode var) {
+  AssertArgument(var.getMetaKind() == kind::metakind::VARIABLE, var);
+  TypeNode pbType = NodeManager::currentNM()->pseudobooleanType();
+  Node pbVar = NodeManager::currentNM()->mkVar(string("PB[") + var.toString() + ']', pbType);
+  d_pbSubstitutions.addSubstitution(var, pbVar);
+
+  if(Debug.isOn("pb")) {
+    Expr::printtypes::Scope pts(Debug("pb"), true);
+    Debug("pb") << "will replace " << var << " with " << pbVar << endl;
+  }
+}
+
 void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){
   Assert(n.getKind() == kind::ITE);
   Assert(n[0].getKind() != EQUAL);
@@ -341,6 +437,27 @@ void ArithStaticLearner::miplibTrick(TNode var, set<Rational>& values, NodeBuild
   }
 }
 
+void ArithStaticLearner::checkBoundsForPseudobooleanReplacement(TNode n) {
+  NodeToMinMaxMap::iterator minFind = d_minMap.find(n);
+  NodeToMinMaxMap::iterator maxFind = d_maxMap.find(n);
+
+  if( n.getType().isInteger() &&
+      minFind != d_minMap.end() &&
+      maxFind != d_maxMap.end() &&
+      ( ( (*minFind).second.getNoninfinitesimalPart() == 1 &&
+          (*minFind).second.getInfinitesimalPart() == 0 ) ||
+        ( (*minFind).second.getNoninfinitesimalPart() == 0 &&
+          (*minFind).second.getInfinitesimalPart() > 0 ) ) &&
+      ( ( (*maxFind).second.getNoninfinitesimalPart() == 1 &&
+          (*maxFind).second.getInfinitesimalPart() == 0 ) ||
+        ( (*maxFind).second.getNoninfinitesimalPart() == 2 &&
+          (*maxFind).second.getInfinitesimalPart() < 0 ) ) ) {
+    // eligible for pseudoboolean replacement
+    Debug("pb") << "eligible for pseudoboolean replacement: " << n << endl;
+    replaceWithPseudoboolean(n);
+  }
+}
+
 void ArithStaticLearner::addBound(TNode n) {
 
   NodeToMinMaxMap::iterator minFind = d_minMap.find(n[0]);
@@ -349,25 +466,29 @@ void ArithStaticLearner::addBound(TNode n) {
   Rational constant = coerceToRational(n[1]);
   DeltaRational bound = constant;
 
-  switch(n.getKind()) {
+  switch(Kind k = n.getKind()) {
   case kind::LT:
     bound = DeltaRational(constant, -1);
+    /* fall through */
   case kind::LEQ:
     if (maxFind == d_maxMap.end() || maxFind->second > bound) {
       d_maxMap[n[0]] = bound;
       Debug("arith::static") << "adding bound " << n << endl;
+      checkBoundsForPseudobooleanReplacement(n[0]);
     }
     break;
   case kind::GT:
     bound = DeltaRational(constant, 1);
+    /* fall through */
   case kind::GEQ:
     if (minFind == d_minMap.end() || minFind->second < bound) {
       d_minMap[n[0]] = bound;
       Debug("arith::static") << "adding bound " << n << endl;
+      checkBoundsForPseudobooleanReplacement(n[0]);
     }
     break;
   default:
-    // nothing else
+    Unhandled(k);
     break;
   }
 }
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index 0ed9cbe85..c58778215 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -25,6 +25,7 @@
 
 #include "util/stats.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/substitutions.h"
 #include <set>
 #include <list>
 
@@ -45,6 +46,19 @@ private:
   std::list<TNode> d_miplibTrickKeys;
 
   /**
+   * Some integer variables are eligible to be replaced by
+   * pseudoboolean variables.  This map collects those eligible
+   * substitutions.
+   *
+   * This is a reference to the substitution map in TheoryArith; as
+   * it's not "owned" by this static learner, it isn't cleared on
+   * clear().  This makes sense, as the static learner only
+   * accumulates information in the substitution map, it never uses it
+   * (i.e., it's write-only).
+   */
+  SubstitutionMap& d_pbSubstitutions;
+
+  /**
    * Map from a node to it's minimum and maximum.
    */
   typedef __gnu_cxx::hash_map<Node, DeltaRational, NodeHashFunction> NodeToMinMaxMap;
@@ -52,7 +66,7 @@ private:
   NodeToMinMaxMap d_maxMap;
 
 public:
-  ArithStaticLearner();
+  ArithStaticLearner(SubstitutionMap& pbSubstitutions);
   void staticLearning(TNode n, NodeBuilder<>& learned);
 
   void addBound(TNode n);
@@ -64,11 +78,14 @@ private:
 
   void postProcess(NodeBuilder<>& learned);
 
+  void replaceWithPseudoboolean(TNode var);
   void iteMinMax(TNode n, NodeBuilder<>& learned);
   void iteConstant(TNode n, NodeBuilder<>& learned);
 
   void miplibTrick(TNode var, std::set<Rational>& values, NodeBuilder<>& learned);
 
+  void checkBoundsForPseudobooleanReplacement(TNode n);
+
   /** These fields are designed to be accessable to ArithStaticLearner methods. */
   class Statistics {
   public:
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 78b77eb00..2dee26be4 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -143,7 +143,7 @@ inline bool evaluateConstantPredicate(Kind k, const Rational& left, const Ration
 }
 
 /**
- * Returns the appropraite coefficient for the infinitesimal given the kind
+ * Returns the appropriate coefficient for the infinitesimal given the kind
  * for an arithmetic atom inorder to represent strict inequalities as inequalities.
  *   x < c  becomes  x <= c + (-1) * \delta
  *   x > c  becomes  x >= x + ( 1) * \delta
diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h
index aca61878d..df82fde91 100644
--- a/src/theory/arith/arithvar_node_map.h
+++ b/src/theory/arith/arithvar_node_map.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file arithvar_node_map.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 #include "cvc4_private.h"
 
 #ifndef __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h
index f8a23fee0..68937acc4 100644
--- a/src/theory/arith/arithvar_set.h
+++ b/src/theory/arith/arithvar_set.h
@@ -2,10 +2,10 @@
 /*! \file arithvar_set.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: mdeters
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -17,13 +17,14 @@
  ** \todo document this file
  **/
 
-#include <vector>
-#include "theory/arith/arith_utilities.h"
-
+#include "cvc4_private.h"
 
 #ifndef __CVC4__THEORY__ARITH__ARTIHVAR_SET_H
 #define __CVC4__THEORY__ARITH__ARTIHVAR_SET_H
 
+#include <vector>
+#include "theory/arith/arith_utilities.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arith {
@@ -33,7 +34,7 @@ namespace arith {
  * This class is designed to provide constant time insertion, deletion, and element_of
  * and fast iteration.
  *
- * ArithVarSets come in 2 varieties ArithVarSet, and PermissiveBackArithVarSet.
+ * ArithVarSets come in 2 varieties: ArithVarSet, and PermissiveBackArithVarSet.
  * The default ArithVarSet assumes that there is no knowledge assumed about ArithVars
  * that are greater than allocated(). Asking isMember() of such an ArithVar
  * is an assertion failure. The cost of doing this is that it takes O(M)
@@ -324,8 +325,8 @@ public:
   }
 };
 
-}; /* namespace arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__ARITH__ARTIHVAR_SET_H */
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
new file mode 100644
index 000000000..151859f21
--- /dev/null
+++ b/src/theory/arith/dio_solver.cpp
@@ -0,0 +1,118 @@
+/*********************                                                        */
+/*! \file dio_solver.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Diophantine equation solver
+ **
+ ** A Diophantine equation solver for the theory of arithmetic.
+ **/
+
+#include "theory/arith/dio_solver.h"
+
+#include <iostream>
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+/*
+static void printEquation(vector<Rational>& coeffs,
+                          vector<ArithVar>& variables,
+                          ostream& out) {
+  Assert(coeffs.size() == variables.size());
+  vector<Rational>::const_iterator i = coeffs.begin();
+  vector<ArithVar>::const_iterator j = variables.begin();
+  while(i != coeffs.end()) {
+    out << *i << "*" << *j;
+    ++i;
+    ++j;
+    if(i != coeffs.end()) {
+      out << " + ";
+    }
+  }
+  out << " = 0";
+}
+*/
+
+bool DioSolver::solve() {
+  Trace("integers") << "DioSolver::solve()" << endl;
+  if(Debug.isOn("integers")) {
+    ScopedDebug dtab("tableau");
+    d_tableau.printTableau();
+  }
+  for(ArithVarSet::const_iterator i = d_tableau.beginBasic();
+      i != d_tableau.endBasic();
+      ++i) {
+    Debug("integers") << "going through row " << *i << endl;
+
+    Integer m = 1;
+    for(Tableau::RowIterator j = d_tableau.rowIterator(*i); !j.atEnd(); ++j) {
+      Debug("integers") << "  column " << (*j).getCoefficient() << " * " << (*j).getColVar() << endl;
+      m *= (*j).getCoefficient().getDenominator();
+    }
+    Assert(m >= 1);
+    Debug("integers") << "final multiplier is " << m << endl;
+
+    Integer gcd = 0;
+    Rational c = 0;
+    Debug("integers") << "going throw row " << *i << " to find gcd" << endl;
+    for(Tableau::RowIterator j = d_tableau.rowIterator(*i); !j.atEnd(); ++j) {
+      Rational r = (*j).getCoefficient();
+      ArithVar v = (*j).getColVar();
+      r *= m;
+      Debug("integers") << "  column " << r << " * " << v << endl;
+      Assert(r.getDenominator() == 1);
+      bool foundConstant = false;
+      // The tableau doesn't store constants.  Constants int he input
+      // are mapped to slack variables that are constrained with
+      // bounds in the partial model.  So we detect and accumulate all
+      // variables whose upper bound equals their lower bound, which
+      // catches these input constants as well as any (contextually)
+      // eliminated variables.
+      if(d_partialModel.hasUpperBound(v) && d_partialModel.hasLowerBound(v)) {
+        DeltaRational b = d_partialModel.getLowerBound(v);
+        if(b.getInfinitesimalPart() == 0 && b == d_partialModel.getUpperBound(v)) {
+          r *= b.getNoninfinitesimalPart();
+          Debug("integers") << "    var " << v << " == [" << b << "], so found a constant part " << r << endl;
+          c += r;
+          foundConstant = true;
+        }
+      }
+      if(!foundConstant) {
+        // calculate gcd of all (NON-constant) coefficients
+        gcd = (gcd == 0) ? r.getNumerator().abs() : gcd.gcd(r.getNumerator());
+        Debug("integers") << "    gcd now " << gcd << endl;
+      }
+    }
+    Debug("integers") << "addEquation: gcd is " << gcd << ", c is " << c << endl;
+    // The gcd must divide c for this equation to be satisfiable.
+    // If c is not an integer, there's no way it can.
+    if(c.getDenominator() == 1 && gcd == gcd.gcd(c.getNumerator())) {
+      Trace("integers") << "addEquation: this eqn is fine" << endl;
+    } else {
+      Trace("integers") << "addEquation: eqn not satisfiable, returning false" << endl;
+      return false;
+    }
+  }
+
+  return true;
+}
+
+void DioSolver::getSolution() {
+  Unimplemented();
+}
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
new file mode 100644
index 000000000..c91ddd994
--- /dev/null
+++ b/src/theory/arith/dio_solver.h
@@ -0,0 +1,72 @@
+/*********************                                                        */
+/*! \file dio_solver.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Diophantine equation solver
+ **
+ ** A Diophantine equation solver for the theory of arithmetic.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__DIO_SOLVER_H
+#define __CVC4__THEORY__ARITH__DIO_SOLVER_H
+
+#include "context/context.h"
+
+#include "theory/arith/tableau.h"
+#include "theory/arith/partial_model.h"
+#include "theory/arith/arith_utilities.h"
+#include "util/rational.h"
+
+#include <vector>
+#include <utility>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class DioSolver {
+  context::Context* d_context;
+  const Tableau& d_tableau;
+  ArithPartialModel& d_partialModel;
+
+public:
+
+  /** Construct a Diophantine equation solver with the given context. */
+  DioSolver(context::Context* ctxt, const Tableau& tab, ArithPartialModel& pmod) :
+    d_context(ctxt),
+    d_tableau(tab),
+    d_partialModel(pmod) {
+  }
+
+  /**
+   * Solve the set of Diophantine equations in the tableau.
+   *
+   * @return true if the set of equations was solved; false if no
+   * solution
+   */
+  bool solve();
+
+  /**
+   * Get the parameterized solution to this set of Diophantine
+   * equations.  Must be preceded by a call to solve() that returned
+   * true. */
+  void getSolution();
+
+};/* class DioSolver */
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__DIO_SOLVER_H */
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 1871e897a..db47062bb 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -30,18 +30,28 @@ sort INTEGER_TYPE \
         "NodeManager::currentNM()->mkConst(Integer(0))" \
         "expr/node_manager.h" \
     "Integer type"
+sort PSEUDOBOOLEAN_TYPE \
+    2 \
+    well-founded \
+        "NodeManager::currentNM()->mkConst(Pseudoboolean(0))" \
+        "expr/node_manager.h" \
+    "Pseudoboolean type"
 
 constant CONST_RATIONAL \
     ::CVC4::Rational \
     ::CVC4::RationalHashStrategy \
     "util/rational.h" \
     "a multiple-precision rational constant"
-
 constant CONST_INTEGER \
     ::CVC4::Integer \
     ::CVC4::IntegerHashStrategy \
     "util/integer.h" \
     "a multiple-precision integer constant"
+constant CONST_PSEUDOBOOLEAN \
+    ::CVC4::Pseudoboolean \
+    ::CVC4::PseudobooleanHashStrategy \
+    "util/pseudoboolean.h" \
+    "a pseudoboolean constant"
 
 operator LT 2 "less than, x < y"
 operator LEQ 2 "less than or equal, x <= y"
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index aea1a43d8..b529a8077 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -254,6 +254,58 @@ Comparison Comparison::parseNormalForm(TNode n) {
   }
 }
 
+bool Comparison::pbComparison(Kind k, TNode left, const Rational& right, bool& result) {
+  AssertArgument(left.getType().isPseudoboolean(), left);
+  switch(k) {
+  case kind::LT:
+    if(right > 1) {
+      result = true;
+      return true;
+    } else if(right <= 0) {
+      result = false;
+      return true;
+    }
+    break;
+  case kind::LEQ:
+    if(right >= 1) {
+      result = true;
+      return true;
+    } else if(right < 0) {
+      result = false;
+      return true;
+    }
+    break;
+  case kind::EQUAL:
+    if(right != 0 && right != 1) {
+      result = false;
+      return true;
+    }
+    break;
+  case kind::GEQ:
+    if(right > 1) {
+      result = false;
+      return true;
+    } else if(right <= 0) {
+      result = true;
+      return true;
+    }
+    break;
+  case kind::GT:
+    if(right >= 1) {
+      result = false;
+      return true;
+    } else if(right < 0) {
+      result = true;
+      return true;
+    }
+    break;
+  default:
+    CheckArgument(false, k, "Bad comparison operator ?!");
+  }
+
+  return false;
+}
+
 Comparison Comparison::mkComparison(Kind k, const Polynomial& left, const Constant& right) {
   Assert(isRelationOperator(k));
   if(left.isConstant()) {
@@ -261,9 +313,16 @@ Comparison Comparison::mkComparison(Kind k, const Polynomial& left, const Consta
     const Rational& rConst = right.getNode().getConst<Rational>();
     bool res = evaluateConstantPredicate(k, lConst, rConst);
     return Comparison(res);
-  } else {
-    return Comparison(toNode(k, left, right), k, left, right);
   }
+
+  if(left.getNode().getType().isPseudoboolean()) {
+    bool result;
+    if(pbComparison(k, left.getNode(), right.getNode().getConst<Rational>(), result)) {
+      return Comparison(result);
+    }
+  }
+
+  return Comparison(toNode(k, left, right), k, left, right);
 }
 
 Comparison Comparison::addConstant(const Constant& constant) const {
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 5d6ca27e9..d6e79318d 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -702,6 +702,22 @@ private:
   Comparison(TNode n, Kind k, const Polynomial& l, const Constant& r):
     NodeWrapper(n), oper(k), left(l), right(r)
   { }
+
+  /**
+   * Possibly simplify a comparison with a pseudoboolean-typed LHS.  k
+   * is one of LT, LEQ, EQUAL, GEQ, GT, and left must be PB-typed.  If
+   * possible, "left k right" is fully evaluated, "true" is returned,
+   * and the result of the evaluation is returned in "result".  If no
+   * evaluation is possible, false is returned and "result" is
+   * untouched.
+   *
+   * For example, pbComparison(kind::EQUAL, "x", 0.5, result) returns
+   * true, and updates "result" to false, since pseudoboolean variable
+   * "x" can never equal 0.5.  pbComparison(kind::GEQ, "x", 1, result)
+   * returns false, since "x" can be >= 1, but could also be less.
+   */
+  static bool pbComparison(Kind k, TNode left, const Rational& right, bool& result);
+
 public:
   Comparison(bool val) :
     NodeWrapper(NodeManager::currentNM()->mkConst(val)),
diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h
index 43ccd7815..e44ba8687 100644
--- a/src/theory/arith/ordered_set.h
+++ b/src/theory/arith/ordered_set.h
@@ -53,14 +53,18 @@ public:
   void addLeq(TNode leq){
     Assert(leq.getKind() == kind::LEQ);
     Assert(rightHandRational(leq) == getValue());
-    Assert(!hasLeq());
+    // [MGD] With context-dependent pre-registration, we could get the
+    // same one twice
+    Assert(!hasLeq() || d_leq == leq);
     d_leq = leq;
   }
 
   void addGeq(TNode geq){
     Assert(geq.getKind() == kind::GEQ);
     Assert(rightHandRational(geq) == getValue());
-    Assert(!hasGeq());
+    // [MGD] With context-dependent pre-registration, we could get the
+    // same one twice
+    Assert(!hasGeq() || d_geq == geq);
     d_geq = geq;
   }
 
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 171c74942..f07e524aa 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -86,7 +86,7 @@ public:
   /* Initializes a variable to a safe value.*/
   void initialize(ArithVar x, const DeltaRational& r);
 
-  /* Gets the last assignment to a variable that is known to be conistent. */
+  /* Gets the last assignment to a variable that is known to be consistent. */
   const DeltaRational& getSafeAssignment(ArithVar x) const;
   const DeltaRational& getAssignment(ArithVar x, bool safe) const;
 
@@ -183,14 +183,12 @@ private:
     return 0 <= x && x < d_mapSize;
   }
 
-};
+};/* class ArithPartialModel */
 
 
-
-
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
 
 
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 367e90301..b432416bd 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -115,7 +115,7 @@ void Tableau::setColumnUnused(ArithVar v){
     ++colIter;
   }
 }
-void Tableau::printTableau(){
+void Tableau::printTableau() const {
   Debug("tableau") << "Tableau::d_activeRows"  << endl;
 
   ArithVarSet::const_iterator basicIter = beginBasic(), endIter = endBasic();
@@ -125,7 +125,7 @@ void Tableau::printTableau(){
   }
 }
 
-void Tableau::printRow(ArithVar basic){
+void Tableau::printRow(ArithVar basic) const {
   Debug("tableau") << "{" << basic << ":";
   for(RowIterator entryIter = rowIterator(basic); !entryIter.atEnd(); ++entryIter){
     const TableauEntry& entry = *entryIter;
@@ -135,7 +135,7 @@ void Tableau::printRow(ArithVar basic){
   Debug("tableau") << "}" << endl;
 }
 
-void Tableau::printEntry(const TableauEntry& entry){
+void Tableau::printEntry(const TableauEntry& entry) const {
   Debug("tableau") << entry.getColVar() << "*" << entry.getCoefficient();
 }
 
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index fa227757a..e14436f8c 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -224,10 +224,10 @@ private:
   class Iterator {
   private:
     EntryID d_curr;
-    TableauEntryManager& d_entryManager;
+    const TableauEntryManager& d_entryManager;
 
   public:
-    Iterator(EntryID start, TableauEntryManager& manager) :
+    Iterator(EntryID start, const TableauEntryManager& manager) :
       d_curr(start), d_entryManager(manager)
     {}
 
@@ -244,7 +244,7 @@ private:
 
     Iterator& operator++(){
       Assert(!atEnd());
-      TableauEntry& entry = d_entryManager.get(d_curr);
+      const TableauEntry& entry = d_entryManager.get(d_curr);
       d_curr = isRowIterator ? entry.getNextRowID() : entry.getNextColID();
       return *this;
     }
@@ -288,13 +288,13 @@ public:
     return d_basicVariables.end();
   }
 
-  RowIterator rowIterator(ArithVar v){
+  RowIterator rowIterator(ArithVar v) const {
     Assert(v < d_rowHeads.size());
     EntryID head = d_rowHeads[v];
     return RowIterator(head, d_entryManager);
   }
 
-  ColIterator colIterator(ArithVar v){
+  ColIterator colIterator(ArithVar v) const {
     Assert(v < d_colHeads.size());
     EntryID head = d_colHeads[v];
     return ColIterator(head, d_entryManager);
@@ -350,9 +350,9 @@ public:
   /**
    * Prints the contents of the Tableau to Debug("tableau::print")
    */
-  void printTableau();
-  void printRow(ArithVar basic);
-  void printEntry(const TableauEntry& entry);
+  void printTableau() const;
+  void printRow(ArithVar basic) const;
+  void printEntry(const TableauEntry& entry) const;
 
 
 private:
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 3831536e9..2664aaac3 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -61,10 +61,13 @@ typedef expr::Attribute<SlackAttrID, bool> Slack;
 
 TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation) :
   Theory(THEORY_ARITH, c, out, valuation),
+  learner(d_pbSubstitutions),
+  d_nextIntegerCheckVar(0),
   d_partialModel(c),
   d_userVariables(),
   d_diseq(c),
   d_tableau(),
+  d_diosolver(c, d_tableau, d_partialModel),
   d_restartsCounter(0),
   d_rowHasBeenAdded(false),
   d_tableauResetDensity(1.6),
@@ -131,13 +134,26 @@ TheoryArith::Statistics::~Statistics(){
 }
 
 Node TheoryArith::preprocess(TNode atom) {
-  if (atom.getKind() == kind::EQUAL) {
-    Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
-    Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
-    return Rewriter::rewrite(leq.andNode(geq));
-  } else {
-    return atom;
+  Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
+
+  Node a = d_pbSubstitutions.apply(atom);
+
+  if (a != atom) {
+    Debug("pb") << "arith::preprocess() : after pb substitutions: " << a << endl;
+    a = Rewriter::rewrite(a);
+    Debug("pb") << "arith::preprocess() : after pb substitutions and rewriting: " << a << endl;
+    Debug("arith::preprocess") << "arith::preprocess() : after pb substitutions and rewriting: " << a << endl;
+  }
+
+  if (a.getKind() == kind::EQUAL) {
+    Node leq = NodeBuilder<2>(kind::LEQ) << a[0] << a[1];
+    Node geq = NodeBuilder<2>(kind::GEQ) << a[0] << a[1];
+    Node rewritten = Rewriter::rewrite(leq.andNode(geq));
+    Debug("arith::preprocess") << "arith::preprocess() : returning " << rewritten << endl;
+    return rewritten;
   }
+
+  return a;
 }
 
 Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutions) {
@@ -187,8 +203,16 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio
       // Add the substitution if not recursive
       Node rewritten = Rewriter::rewrite(eliminateVar);
       if (!rewritten.hasSubterm(minVar)) {
-        outSubstitutions.addSubstitution(minVar, Rewriter::rewrite(eliminateVar));
-        return SOLVE_STATUS_SOLVED;
+        Node elim = Rewriter::rewrite(eliminateVar);
+        if (!minVar.getType().isInteger() || elim.getType().isInteger()) {
+          // cannot eliminate integers here unless we know the resulting
+          // substitution is integral
+          Debug("simplify") << "TheoryArith::solve(): substitution " << minVar << " |-> " << elim << endl;
+          outSubstitutions.addSubstitution(minVar, elim);
+          return SOLVE_STATUS_SOLVED;
+        } else {
+          Debug("simplify") << "TheoryArith::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl;
+        }
       }
     }
   }
@@ -199,7 +223,7 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio
   case kind::LT:
   case kind::GEQ:
   case kind::GT:
-    if (in[0].getKind() == kind::VARIABLE) {
+    if (in[0].getMetaKind() == kind::metakind::VARIABLE) {
       learner.addBound(in);
     }
     break;
@@ -290,16 +314,19 @@ void TheoryArith::preRegisterTerm(TNode n) {
       } 
     }
   }
-  Debug("arith_preregister") << "end arith::preRegisterTerm("<< n <<")"<< endl;
+  Debug("arith_preregister") << "end arith::preRegisterTerm(" << n <<")" << endl;
 }
 
 
 ArithVar TheoryArith::requestArithVar(TNode x, bool basic){
   Assert(isLeaf(x) || x.getKind() == PLUS);
   Assert(!d_arithvarNodeMap.hasArithVar(x));
+  Assert(x.getType().isReal());// real or integer
 
   ArithVar varX = d_variables.size();
   d_variables.push_back(Node(x));
+  Debug("integers") << "isInteger[[" << x << "]]: " << x.getType().isInteger() << endl;
+  d_integerVars.push_back(x.getType().isPseudoboolean() ? 2 : (x.getType().isInteger() ? 1 : 0));
 
   d_simplex.increaseMax();
 
@@ -570,6 +597,129 @@ void TheoryArith::check(Effort effortLevel){
     }
   }
 
+  if(fullEffort(effortLevel) && d_integerVars.size() > 0) {
+    const ArithVar rrEnd = d_nextIntegerCheckVar;
+    do {
+      ArithVar v = d_nextIntegerCheckVar;
+      short type = d_integerVars[v];
+      if(type > 0) { // integer
+        const DeltaRational& d = d_partialModel.getAssignment(v);
+        const Rational& r = d.getNoninfinitesimalPart();
+        const Rational& i = d.getInfinitesimalPart();
+        Trace("integers") << "integers: assignment to [[" << d_arithvarNodeMap.asNode(v) << "]] is " << r << "[" << i << "]" << endl;
+        if(type == 2) {
+          // pseudoboolean
+          if(r.getDenominator() == 1 && i.getNumerator() == 0 &&
+             (r.getNumerator() == 0 || r.getNumerator() == 1)) {
+            // already pseudoboolean; skip
+            continue;
+          }
+
+          TNode var = d_arithvarNodeMap.asNode(v);
+          Node zero = NodeManager::currentNM()->mkConst(Integer(0));
+          Node one = NodeManager::currentNM()->mkConst(Integer(1));
+          Node eq0 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, var, zero));
+          Node eq1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, var, one));
+          Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq0, eq1);
+          Trace("pb") << "pseudobooleans: branch & bound: " << lem << endl;
+          Trace("integers") << "pseudobooleans: branch & bound: " << lem << endl;
+          //d_out->lemma(lem);
+        }
+        if(r.getDenominator() == 1 && i.getNumerator() == 0) {
+          // already an integer assignment; skip
+          continue;
+        }
+
+        // otherwise, try the Diophantine equation solver
+        //bool result = d_diosolver.solve();
+        //Debug("integers") << "the dio solver returned " << (result ? "true" : "false") << endl;
+
+        // branch and bound
+        if(r.getDenominator() == 1) {
+          // r is an integer, but the infinitesimal might not be
+          if(i.getNumerator() < 0) {
+            // lemma: v <= r - 1 || v >= r
+
+            TNode var = d_arithvarNodeMap.asNode(v);
+            Node nrMinus1 = NodeManager::currentNM()->mkConst(r - 1);
+            Node nr = NodeManager::currentNM()->mkConst(r);
+            Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, nrMinus1));
+            Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, nr));
+
+            Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq);
+            Trace("integers") << "integers: branch & bound: " << lem << endl;
+            if(d_valuation.isSatLiteral(lem[0])) {
+              Debug("integers") << "    " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl;
+            } else {
+              Debug("integers") << "    " << lem[0] << " is not assigned a SAT literal" << endl;
+            }
+            if(d_valuation.isSatLiteral(lem[1])) {
+              Debug("integers") << "    " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl;
+            } else {
+              Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
+            }
+            d_out->lemma(lem);
+
+            // split only on one var
+            break;
+          } else if(i.getNumerator() > 0) {
+            // lemma: v <= r || v >= r + 1
+
+            TNode var = d_arithvarNodeMap.asNode(v);
+            Node nr = NodeManager::currentNM()->mkConst(r);
+            Node nrPlus1 = NodeManager::currentNM()->mkConst(r + 1);
+            Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, nr));
+            Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, nrPlus1));
+
+            Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq);
+            Trace("integers") << "integers: branch & bound: " << lem << endl;
+            if(d_valuation.isSatLiteral(lem[0])) {
+              Debug("integers") << "    " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl;
+            } else {
+              Debug("integers") << "    " << lem[0] << " is not assigned a SAT literal" << endl;
+            }
+            if(d_valuation.isSatLiteral(lem[1])) {
+              Debug("integers") << "    " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl;
+            } else {
+              Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
+            }
+            d_out->lemma(lem);
+
+            // split only on one var
+            break;
+          } else {
+            Unreachable();
+          }
+        } else {
+          // lemma: v <= floor(r) || v >= ceil(r)
+
+          TNode var = d_arithvarNodeMap.asNode(v);
+          Node floor = NodeManager::currentNM()->mkConst(r.floor());
+          Node ceiling = NodeManager::currentNM()->mkConst(r.ceiling());
+          Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, floor));
+          Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, ceiling));
+
+          Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq);
+          Trace("integers") << "integers: branch & bound: " << lem << endl;
+          if(d_valuation.isSatLiteral(lem[0])) {
+            Debug("integers") << "    " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl;
+          } else {
+            Debug("integers") << "    " << lem[0] << " is not assigned a SAT literal" << endl;
+          }
+          if(d_valuation.isSatLiteral(lem[1])) {
+            Debug("integers") << "    " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl;
+          } else {
+            Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
+          }
+          d_out->lemma(lem);
+
+          // split only on one var
+          break;
+        }
+      }// if(arithvar is integer-typed)
+    } while((d_nextIntegerCheckVar = (1 + d_nextIntegerCheckVar == d_variables.size() ? 0 : 1 + d_nextIntegerCheckVar)) != rrEnd);
+  }// if(full effort)
+
   if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
   if(Debug.isOn("arith::print_model")) { debugPrintModel(); }
   Debug("arith") << "TheoryArith::check end" << std::endl;
@@ -866,7 +1016,9 @@ void TheoryArith::presolve(){
     for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
       Node variableNode = *i;
       ArithVar var = d_arithvarNodeMap.asArithVar(variableNode);
-      if(d_userVariables.isMember(var) && !d_atomDatabase.hasAnyAtoms(variableNode)){
+      if(d_userVariables.isMember(var) &&
+         !d_atomDatabase.hasAnyAtoms(variableNode) &&
+         !variableNode.getType().isInteger()){
 	//The user variable is unconstrained.
 	//Remove this variable permanently
 	permanentlyRemoveVariable(var);
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 0c15c824c..7e14f6b06 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -38,6 +38,7 @@
 #include "theory/arith/arith_static_learner.h"
 #include "theory/arith/arith_prop_manager.h"
 #include "theory/arith/arithvar_node_map.h"
+#include "theory/arith/dio_solver.h"
 
 #include "util/stats.h"
 
@@ -69,6 +70,21 @@ private:
   ArithVarNodeMap d_arithvarNodeMap;
 
   /**
+   * List of the types of variables in the system.
+   * "True" means integer, "false" means (non-integer) real.
+   */
+  std::vector<short> d_integerVars;
+
+  /**
+   * On full effort checks (after determining LA(Q) satisfiability), we
+   * consider integer vars, but we make sure to do so fairly to avoid
+   * nontermination (although this isn't a guarantee).  To do it fairly,
+   * we consider variables in round-robin fashion.  This is the
+   * round-robin index.
+   */
+  ArithVar d_nextIntegerCheckVar;
+
+  /**
    * If ArithVar v maps to the node n in d_removednode,
    * then n = (= asNode(v) rhs) where rhs is a term that
    * can be used to determine the value of n using getValue().
@@ -86,8 +102,6 @@ private:
    */
   ArithVarSet d_userVariables;
 
-
-
   /**
    * List of all of the inequalities asserted in the current context.
    */
@@ -98,6 +112,23 @@ private:
    */
   Tableau d_tableau;
 
+  /**
+   * A Diophantine equation solver.  Accesses the tableau and partial
+   * model (each in a read-only fashion).
+   */
+  DioSolver d_diosolver;
+
+  /**
+   * Some integer variables can be replaced with pseudoboolean
+   * variables internally.  This map is built up at static learning
+   * time for top-level asserted expressions of the shape "x = 0 OR x
+   * = 1".  This substitution map is then applied in preprocess().
+   *
+   * Note that expressions of the shape "x >= 0 AND x <= 1" are
+   * already substituted for PB versions at solve() time and won't
+   * appear here.
+   */
+  SubstitutionMap d_pbSubstitutions;
 
   /** Counts the number of notifyRestart() calls to the theory. */
   uint32_t d_restartsCounter;
diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index 70b53a930..09030d331 100644
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -34,7 +34,10 @@ public:
       TNode::iterator child_it = n.begin();
       TNode::iterator child_it_end = n.end();
       for(; child_it != child_it_end; ++child_it) {
-        if((*child_it).getType(check) != booleanType) {
+        if(!(*child_it).getType(check).isBoolean()) {
+          Debug("pb") << "failed type checking: " << *child_it << std::endl;
+          Debug("pb") << "  integer: " << (*child_it).getType(check).isInteger() << std::endl;
+          Debug("pb") << "  real: " << (*child_it).getType(check).isReal() << std::endl;
           throw TypeCheckingExceptionPrivate(n, "expecting a Boolean subexpression");
         }
       }
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index f343848d8..3bfb7fdc5 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -90,7 +90,7 @@ class EqualityTypeRule {
         throw TypeCheckingExceptionPrivate(n, ss.str());
       }
 
-      if ( lhsType == booleanType ) {
+      if ( lhsType == booleanType && rhsType == booleanType ) {
         throw TypeCheckingExceptionPrivate(n, "equality between two boolean terms (use IFF instead)");
       }
     }
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 44aed8b17..d82e628c1 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -92,7 +92,7 @@ public:
    * @param safe - whether it is safe to be interrupted
    */
   virtual void lemma(TNode n, bool safe = false)
-    throw(Interrupted, AssertionException) = 0;
+    throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0;
 
   /**
    * Request a split on a new theory atom.  This is equivalent to
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 8657ed871..76551bc18 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -161,5 +161,5 @@ void SubstitutionMap::print(ostream& out) const {
   }
 }
 
-}
-}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 513300a32..f59c17dc0 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -23,6 +23,7 @@
 
 #include <utility>
 #include <vector>
+#include <algorithm>
 #include "expr/node.h"
 
 namespace CVC4 {
@@ -77,6 +78,25 @@ public:
   }
 
   /**
+   * Clear out the accumulated substitutions, resetting this
+   * SubstitutionMap to the way it was when first constructed.
+   */
+  void clear() {
+    d_substitutions.clear();
+    d_substitutionCache.clear();
+    d_cacheInvalidated = true;
+  }
+
+  /**
+   * Swap the contents of this SubstitutionMap with those of another.
+   */
+  void swap(SubstitutionMap& map) {
+    d_substitutions.swap(map.d_substitutions);
+    d_substitutionCache.swap(map.d_substitutionCache);
+    std::swap(d_cacheInvalidated, map.d_cacheInvalidated);
+  }
+
+  /**
    * Print to the output stream
    */
   void print(std::ostream& out) const;
diff --git a/src/theory/theory.h b/src/theory/theory.h
index d859c60d8..62a8cb4d6 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -442,8 +442,10 @@ public:
   }
 
   /**
-   * Given an atom of the theory, that comes from the input formula, this is method can rewrite the atom
-   * into an equivalent form. This is only called just before an input atom to the engine.
+   * Given an atom of the theory coming from the input formula, this
+   * method can be overridden in a theory implementation to rewrite
+   * the atom into an equivalent form.  This is only called just
+   * before an input atom to the engine.
    */
   virtual Node preprocess(TNode atom) { return atom; }
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 662a4925a..2107bcb66 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -149,7 +149,7 @@ class TheoryEngine {
     }
 
     void lemma(TNode node, bool removable = false)
-      throw(theory::Interrupted, AssertionException) {
+      throw(theory::Interrupted, TypeCheckingExceptionPrivate, AssertionException) {
       Trace("theory") << "EngineOutputChannel::lemma("
                       << node << ")" << std::endl;
       ++(d_engine->d_statistics.d_statLemma);