Merge branch 'master' into fixBetterSkolems

21 files changed, 405 insertions, 135 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index cff31dbcd..011ba6ab5 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -137,8 +137,8 @@ libcvc4_add_sources(
   proof/clause_id.h
   proof/cnf_proof.cpp
   proof/cnf_proof.h
-  proof/dimacs_printer.cpp
-  proof/dimacs_printer.h
+  proof/dimacs.cpp
+  proof/dimacs.h
   proof/drat/drat_proof.cpp
   proof/drat/drat_proof.h
   proof/er/er_proof.cpp
diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index 7b7d93f1d..b1631f369 100644
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -131,6 +131,7 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/LastExceptionBuffer.java
   ${CMAKE_CURRENT_BINARY_DIR}/LogicException.java
   ${CMAKE_CURRENT_BINARY_DIR}/LogicInfo.java
+  ${CMAKE_CURRENT_BINARY_DIR}/Map_ExprExpr.java
   ${CMAKE_CURRENT_BINARY_DIR}/ModalException.java
   ${CMAKE_CURRENT_BINARY_DIR}/OptionException.java
   ${CMAKE_CURRENT_BINARY_DIR}/Options.java
@@ -165,7 +166,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/SExpr.java
   ${CMAKE_CURRENT_BINARY_DIR}/SExprKeyword.java
   ${CMAKE_CURRENT_BINARY_DIR}/SExprType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Statistic.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Model.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Printer.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__api__Solver.java
@@ -178,7 +178,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpq_class.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpz_class.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__istream.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__mapT_CVC4__Expr_CVC4__Expr_t.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__ostream.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__shared_ptrT_CVC4__SygusPrintCallback_t.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__string.java
@@ -201,16 +200,17 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.java
   ${CMAKE_CURRENT_BINARY_DIR}/SortConstructorType.java
   ${CMAKE_CURRENT_BINARY_DIR}/SortType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/Statistic.java
   ${CMAKE_CURRENT_BINARY_DIR}/Statistics.java
   ${CMAKE_CURRENT_BINARY_DIR}/StatisticsBase.java
   ${CMAKE_CURRENT_BINARY_DIR}/StringType.java
   ${CMAKE_CURRENT_BINARY_DIR}/SygusConstraintCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SynthFunCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/SygusGTerm.java
   ${CMAKE_CURRENT_BINARY_DIR}/SygusInvConstraintCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/SygusPrintCallback.java
   ${CMAKE_CURRENT_BINARY_DIR}/SymbolTable.java
   ${CMAKE_CURRENT_BINARY_DIR}/SymbolType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SynthFunCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/TesterType.java
   ${CMAKE_CURRENT_BINARY_DIR}/TheoryId.java
   ${CMAKE_CURRENT_BINARY_DIR}/Timer.java
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 25ffb0778..841f9ea28 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -236,6 +236,38 @@ bool getFreeVariables(TNode n,
   return !fvs.empty();
 }
 
+bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs)
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    std::unordered_set<TNode, TNodeHashFunction>::iterator itv =
+        visited.find(cur);
+    if (itv == visited.end())
+    {
+      if (cur.isVar())
+      {
+        vs.insert(cur);
+      }
+      else
+      {
+        for (const TNode& cn : cur)
+        {
+          visit.push_back(cn);
+        }
+      }
+      visited.insert(cur);
+    }
+  } while (!visit.empty());
+
+  return !vs.empty();
+}
+
 void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms)
 {
   std::unordered_set<TNode, TNodeHashFunction> visited;
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 656f162ae..727f5ba75 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -73,6 +73,14 @@ bool getFreeVariables(TNode n,
                       bool computeFv = true);
 
 /**
+ * Get all variables in n.
+ * @param n The node under investigation
+ * @param vs The set which free variables are added to
+ * @return true iff this node contains a free variable.
+ */
+bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs);
+
+/**
  * For term n, this function collects the symbols that occur as a subterms
  * of n. A symbol is a variable that does not have kind BOUND_VARIABLE.
  * @param n The node under investigation
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 9128bc190..4558f3720 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -772,8 +772,8 @@ void NodeBuilder<nchild_thresh>::clear(Kind k) {
 
 template <unsigned nchild_thresh>
 void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
-  Assert( toSize > d_nvMaxChildren,
-          "attempt to realloc() a NodeBuilder to a smaller/equal size!" );
+  AlwaysAssert(toSize > d_nvMaxChildren,
+               "attempt to realloc() a NodeBuilder to a smaller/equal size!");
   Assert( toSize < (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN),
           "attempt to realloc() a NodeBuilder to size %u (beyond hard limit of %u)",
           toSize, (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1 );
diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp
index cf5f35457..a024c97a7 100644
--- a/src/printer/dagification_visitor.cpp
+++ b/src/printer/dagification_visitor.cpp
@@ -17,6 +17,8 @@
 #include "printer/dagification_visitor.h"
 
 #include "context/context.h"
+#include "expr/node_algorithm.h"
+#include "expr/node_manager_attributes.h"
 #include "theory/substitutions.h"
 
 #include <sstream>
@@ -24,18 +26,20 @@
 namespace CVC4 {
 namespace printer {
 
-DagificationVisitor::DagificationVisitor(unsigned threshold, std::string letVarPrefix) :
-  d_threshold(threshold),
-  d_letVarPrefix(letVarPrefix),
-  d_nodeCount(),
-  d_top(),
-  d_context(new context::Context()),
-  d_substitutions(new theory::SubstitutionMap(d_context)),
-  d_letVar(0),
-  d_done(false),
-  d_uniqueParent(),
-  d_substNodes() {
-
+DagificationVisitor::DagificationVisitor(unsigned threshold,
+                                         std::string letVarPrefix)
+    : d_threshold(threshold),
+      d_letVarPrefix(letVarPrefix),
+      d_nodeCount(),
+      d_reservedLetNames(),
+      d_top(),
+      d_context(new context::Context()),
+      d_substitutions(new theory::SubstitutionMap(d_context)),
+      d_letVar(0),
+      d_done(false),
+      d_uniqueParent(),
+      d_substNodes()
+{
   // 0 doesn't make sense
   AlwaysAssertArgument(threshold > 0, threshold);
 }
@@ -51,8 +55,28 @@ bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) {
   {
     // for quantifiers, we visit them but we don't recurse on them
     visit(current, parent);
+
+    // search for variables that start with the let prefix
+    std::unordered_set<TNode, TNodeHashFunction> vs;
+    expr::getVariables(current, vs);
+    for (const TNode v : vs)
+    {
+      const std::string name = v.getAttribute(expr::VarNameAttr());
+      if (name.compare(0, d_letVarPrefix.size(), d_letVarPrefix) == 0)
+      {
+        d_reservedLetNames.insert(name);
+      }
+    }
     return true;
   }
+  else if (current.isVar())
+  {
+    const std::string name = current.getAttribute(expr::VarNameAttr());
+    if (name.compare(0, d_letVarPrefix.size(), d_letVarPrefix) == 0)
+    {
+      d_reservedLetNames.insert(name);
+    }
+  }
   // don't visit variables, constants, or those exprs that we've
   // already seen more than the threshold: if we've increased
   // the count beyond the threshold already, we've done the same
@@ -137,7 +161,11 @@ void DagificationVisitor::done(TNode node) {
 
     // construct the let binder
     std::stringstream ss;
-    ss << d_letVarPrefix << d_letVar++;
+    do
+    {
+      ss.str("");
+      ss << d_letVarPrefix << d_letVar++;
+    } while (d_reservedLetNames.find(ss.str()) != d_reservedLetNames.end());
     Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType(), "dagification", NodeManager::SKOLEM_NO_NOTIFY | NodeManager::SKOLEM_EXACT_NAME);
 
     // apply previous substitutions to the rhs, enabling cascading LETs
diff --git a/src/printer/dagification_visitor.h b/src/printer/dagification_visitor.h
index 18f31e662..6df5f32b4 100644
--- a/src/printer/dagification_visitor.h
+++ b/src/printer/dagification_visitor.h
@@ -21,6 +21,7 @@
 
 #include <string>
 #include <unordered_map>
+#include <unordered_set>
 #include <vector>
 
 #include "expr/node.h"
@@ -69,6 +70,12 @@ class DagificationVisitor {
   std::unordered_map<TNode, unsigned, TNodeHashFunction> d_nodeCount;
 
   /**
+   * The set of variable names with the let prefix that appear in the
+   * expression.
+   */
+  std::unordered_set<std::string> d_reservedLetNames;
+
+  /**
    * The top-most node we are visiting.
    */
   TNode d_top;
diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp
index eed295b1a..07589fd07 100644
--- a/src/proof/clausal_bitvector_proof.cpp
+++ b/src/proof/clausal_bitvector_proof.cpp
@@ -17,24 +17,35 @@
 #include "cvc4_private.h"
 
 #include <algorithm>
+#include <iostream>
 #include <iterator>
-#include <set>
+#include <unordered_set>
 
 #include "options/bv_options.h"
 #include "proof/clausal_bitvector_proof.h"
+#include "proof/dimacs.h"
 #include "proof/drat/drat_proof.h"
 #include "proof/er/er_proof.h"
 #include "proof/lfsc_proof_printer.h"
 #include "proof/lrat/lrat_proof.h"
 #include "theory/bv/theory_bv.h"
 
+#if CVC4_USE_DRAT2ER
+#include "drat2er_options.h"
+#include "drat_trim_interface.h"
+#endif
+
 namespace CVC4 {
 
 namespace proof {
 
 ClausalBitVectorProof::ClausalBitVectorProof(theory::bv::TheoryBV* bv,
                                              TheoryProofEngine* proofEngine)
-    : BitVectorProof(bv, proofEngine), d_usedClauses(), d_binaryDratProof()
+    : BitVectorProof(bv, proofEngine),
+      d_clauses(),
+      d_originalClauseIndices(),
+      d_binaryDratProof(),
+      d_coreClauseIndices()
 {
 }
 
@@ -69,33 +80,151 @@ void ClausalBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
 void ClausalBitVectorProof::registerUsedClause(ClauseId id,
                                                prop::SatClause& clause)
 {
-  d_usedClauses.emplace_back(id, clause);
+  d_clauses.emplace(id, clause);
+  d_originalClauseIndices.push_back(id);
 };
 
 void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
 {
+  optimizeDratProof();
+
   // Debug dump of DRAT Proof
   if (Debug.isOn("bv::clausal"))
   {
     std::string serializedDratProof = d_binaryDratProof.str();
+    Debug("bv::clausal") << "option: " << options::bvOptimizeSatProof()
+                         << std::endl;
     Debug("bv::clausal") << "binary DRAT proof byte count: "
                          << serializedDratProof.size() << std::endl;
-    Debug("bv::clausal") << "Parsing DRAT proof ... " << std::endl;
-    drat::DratProof dratProof =
-        drat::DratProof::fromBinary(serializedDratProof);
-
-    Debug("bv::clausal") << "Printing DRAT proof ... " << std::endl;
-    dratProof.outputAsText(Debug("bv::clausal"));
+    Debug("bv::clausal") << "clause count: " << d_coreClauseIndices.size()
+                         << std::endl;
   }
 
   // Empty any old record of which atoms were used
   d_atomsInBitblastingProof.clear();
+  Assert(d_atomsInBitblastingProof.size() == 0);
 
   // For each used clause, ask the CNF proof which atoms are used in it
-  for (const auto& usedIndexAndClause : d_usedClauses)
+  for (const ClauseId usedIdx : d_coreClauseIndices)
   {
-    d_cnfProof->collectAtoms(&usedIndexAndClause.second,
-                             d_atomsInBitblastingProof);
+    d_cnfProof->collectAtoms(&d_clauses.at(usedIdx), d_atomsInBitblastingProof);
+  }
+}
+
+void ClausalBitVectorProof::optimizeDratProof()
+{
+  if (options::bvOptimizeSatProof()
+          == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF
+      || options::bvOptimizeSatProof()
+             == theory::bv::BvOptimizeSatProof::
+                    BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
+  {
+    Debug("bv::clausal") << "Optimizing DRAT" << std::endl;
+    char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
+    char dratFilename[] = "/tmp/cvc4-drat-XXXXXX";
+    char optDratFilename[] = "/tmp/cvc4-optimized-drat-XXXXXX";
+    char optFormulaFilename[] = "/tmp/cvc4-optimized-formula-XXXXXX";
+    int r;
+    r = mkstemp(formulaFilename);
+    AlwaysAssert(r > 0);
+    close(r);
+    r = mkstemp(dratFilename);
+    AlwaysAssert(r > 0);
+    close(r);
+    r = mkstemp(optDratFilename);
+    AlwaysAssert(r > 0);
+    close(r);
+    r = mkstemp(optFormulaFilename);
+    AlwaysAssert(r > 0);
+    close(r);
+
+    std::ofstream formStream(formulaFilename);
+    printDimacs(formStream, d_clauses, d_originalClauseIndices);
+    formStream.close();
+
+    std::ofstream dratStream(dratFilename);
+    dratStream << d_binaryDratProof.str();
+    dratStream.close();
+
+#if CVC4_USE_DRAT2ER
+    int dratTrimExitCode =
+        drat2er::drat_trim::OptimizeWithDratTrim(formulaFilename,
+                                                 dratFilename,
+                                                 optFormulaFilename,
+                                                 optDratFilename,
+                                                 drat2er::options::QUIET);
+    AlwaysAssert(
+        dratTrimExitCode == 0, "drat-trim exited with %d", dratTrimExitCode);
+#else
+    Unimplemented(
+        "Proof production when using CryptoMiniSat requires drat2er.\n"
+        "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
+#endif
+
+    d_binaryDratProof.str("");
+    Assert(d_binaryDratProof.str().size() == 0);
+
+    std::ifstream lratStream(optDratFilename);
+    std::copy(std::istreambuf_iterator<char>(lratStream),
+              std::istreambuf_iterator<char>(),
+              std::ostreambuf_iterator<char>(d_binaryDratProof));
+
+    if (options::bvOptimizeSatProof()
+        == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
+    {
+      std::ifstream optFormulaStream{optFormulaFilename};
+      std::vector<prop::SatClause> core = parseDimacs(optFormulaStream);
+      optFormulaStream.close();
+
+      // Now we need to compute the clause indices for the UNSAT core. This is a
+      // bit difficult because drat-trim may have reordered clauses, and/or
+      // removed duplicate literals. We use literal sets as the canonical clause
+      // form.
+      std::unordered_map<
+          std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>,
+          ClauseId,
+          prop::SatClauseSetHashFunction>
+          cannonicalClausesToIndices;
+      for (const auto& kv : d_clauses)
+      {
+        cannonicalClausesToIndices.emplace(
+            std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>{
+                kv.second.begin(), kv.second.end()},
+            kv.first);
+      }
+
+      d_coreClauseIndices.clear();
+      std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
+          coreClauseCanonical;
+      for (const prop::SatClause& coreClause : core)
+      {
+        coreClauseCanonical.insert(coreClause.begin(), coreClause.end());
+        d_coreClauseIndices.push_back(
+            cannonicalClausesToIndices.at(coreClauseCanonical));
+        coreClauseCanonical.clear();
+      }
+      Debug("bv::clausal") << "Optimizing the DRAT proof and the formula"
+                           << std::endl;
+    }
+    else
+    {
+      Debug("bv::clausal") << "Optimizing the DRAT proof but not the formula"
+                           << std::endl;
+      d_coreClauseIndices = d_originalClauseIndices;
+    }
+
+    Assert(d_coreClauseIndices.size() > 0);
+    remove(formulaFilename);
+    remove(dratFilename);
+    remove(optDratFilename);
+    remove(optFormulaFilename);
+    Debug("bv::clausal") << "Optimized DRAT" << std::endl;
+  }
+  else
+  {
+    Debug("bv::clausal") << "Not optimizing the formula or the DRAT proof"
+                         << std::endl;
+    d_coreClauseIndices = d_originalClauseIndices;
   }
 }
 
@@ -120,10 +249,9 @@ void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
   d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap);
 
   os << "\n;; BB-CNF proofs\n";
-  for (const auto& idAndClause : d_usedClauses)
+  for (const ClauseId id : d_coreClauseIndices)
   {
-    d_cnfProof->printCnfProofForClause(
-        idAndClause.first, &idAndClause.second, os, paren);
+    d_cnfProof->printCnfProofForClause(id, &d_clauses.at(id), os, paren);
   }
 }
 
@@ -137,13 +265,8 @@ void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os,
   os << "\n;; Proof of input to SAT solver\n";
   os << "(@ proofOfSatInput ";
   paren << ")";
-  std::vector<ClauseId> usedIds;
-  usedIds.reserve(d_usedClauses.size());
-  for (const auto& idAnd : d_usedClauses)
-  {
-    usedIds.push_back(idAnd.first);
-  };
-  LFSCProofPrinter::printSatInputProof(usedIds, os, "bb");
+
+  LFSCProofPrinter::printSatInputProof(d_coreClauseIndices, os, "bb");
 
   os << "\n;; DRAT Proof Value\n";
   os << "(@ dratProof ";
@@ -166,19 +289,13 @@ void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os,
   os << "\n;; Proof of input to SAT solver\n";
   os << "(@ proofOfCMap ";
   paren << ")";
-  std::vector<ClauseId> usedIds;
-  usedIds.reserve(d_usedClauses.size());
-  for (const auto& idAnd : d_usedClauses)
-  {
-    usedIds.push_back(idAnd.first);
-  };
-  LFSCProofPrinter::printCMapProof(usedIds, os, "bb");
+  LFSCProofPrinter::printCMapProof(d_coreClauseIndices, os, "bb");
 
   os << "\n;; DRAT Proof Value\n";
   os << "(@ lratProof ";
   paren << ")";
-  lrat::LratProof pf =
-      lrat::LratProof::fromDratProof(d_usedClauses, d_binaryDratProof.str());
+  lrat::LratProof pf = lrat::LratProof::fromDratProof(
+      d_clauses, d_coreClauseIndices, d_binaryDratProof.str());
   pf.outputAsLfsc(os);
   os << "\n";
 
@@ -194,8 +311,8 @@ void LfscErBitVectorProof::printEmptyClauseProof(std::ostream& os,
          "the BV theory should only be proving bottom directly in the eager "
          "bitblasting mode");
 
-  er::ErProof pf =
-      er::ErProof::fromBinaryDratProof(d_usedClauses, d_binaryDratProof.str());
+  er::ErProof pf = er::ErProof::fromBinaryDratProof(
+      d_clauses, d_coreClauseIndices, d_binaryDratProof.str());
 
   pf.outputAsLfsc(os);
 }
diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h
index b10b1ad1c..a410b5b38 100644
--- a/src/proof/clausal_bitvector_proof.h
+++ b/src/proof/clausal_bitvector_proof.h
@@ -61,9 +61,16 @@ class ClausalBitVectorProof : public BitVectorProof
 
  protected:
   // A list of all clauses and their ids which are passed into the SAT solver
-  std::vector<std::pair<ClauseId, prop::SatClause>> d_usedClauses;
+  std::unordered_map<ClauseId, prop::SatClause> d_clauses{};
+  std::vector<ClauseId> d_originalClauseIndices{};
   // Stores the proof recieved from the SAT solver.
-  std::ostringstream d_binaryDratProof;
+  std::ostringstream d_binaryDratProof{};
+  std::vector<ClauseId> d_coreClauseIndices{};
+
+ private:
+  // Optimizes the DRAT proof stored in `d_binaryDratProof` and returns a list
+  // of clause actually needed to check that proof (a smaller UNSAT core)
+  void optimizeDratProof();
 };
 
 /**
diff --git a/src/proof/dimacs_printer.cpp b/src/proof/dimacs.cpp
index 04f880e11..cced98660 100644
--- a/src/proof/dimacs_printer.cpp
+++ b/src/proof/dimacs.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file dimacs_printer.cpp
+/*! \file dimacs.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Alex Ozdemir
@@ -14,7 +14,9 @@
  ** Defines serialization for SAT problems as DIMACS
  **/
 
-#include "proof/dimacs_printer.h"
+#include "proof/dimacs.h"
+
+#include "base/cvc4_assert.h"
 
 #include <iostream>
 
@@ -43,14 +45,15 @@ std::ostream& textOut(std::ostream& o, const prop::SatClause& c)
   return o << "0";
 }
 
-void printDimacs(
-    std::ostream& o,
-    const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses)
+void printDimacs(std::ostream& o,
+                 const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+                 const std::vector<ClauseId>& usedIndices)
 {
   size_t maxVar = 0;
-  for (const auto& c : usedClauses)
+  for (const ClauseId i : usedIndices)
   {
-    for (const auto& l : c.second)
+    const prop::SatClause& c = clauses.at(i);
+    for (const auto& l : c)
     {
       if (l.getSatVariable() + 1 > maxVar)
       {
@@ -58,10 +61,11 @@ void printDimacs(
       }
     }
   }
-  o << "p cnf " << maxVar << " " << usedClauses.size() << '\n';
-  for (const auto& idAndClause : usedClauses)
+  o << "p cnf " << maxVar << " " << usedIndices.size() << '\n';
+  for (const ClauseId i : usedIndices)
   {
-    for (const auto& l : idAndClause.second)
+    const prop::SatClause& c = clauses.at(i);
+    for (const auto& l : c)
     {
       if (l.isNegated())
       {
@@ -73,5 +77,44 @@ void printDimacs(
   }
 }
 
+std::vector<prop::SatClause> parseDimacs(std::istream& in)
+{
+  std::string tag;
+  uint64_t nVars;
+  uint64_t nClauses;
+
+  in >> tag;
+  Assert(in.good());
+  Assert(tag == "p");
+
+  in >> tag;
+  Assert(in.good());
+  Assert(tag == "cnf");
+
+  in >> nVars;
+  Assert(nVars >= 0);
+
+  in >> nClauses;
+  Assert(nClauses >= 0);
+
+  std::vector<prop::SatClause> cnf;
+  for (uint64_t i = 0; i < nClauses; ++i)
+  {
+    cnf.emplace_back();
+    int64_t lit;
+    in >> lit;
+    Assert(in.good());
+    while (lit != 0)
+    {
+      cnf.back().emplace_back(std::abs(lit) - 1, lit < 0);
+      in >> lit;
+      Assert(static_cast<uint64_t>(std::abs(lit)) <= nVars);
+      Assert(in.good());
+    }
+  }
+
+  return cnf;
+}
+
 }  // namespace proof
 }  // namespace CVC4
diff --git a/src/proof/dimacs_printer.h b/src/proof/dimacs.h
index 2ae4abefa..5956c5d26 100644
--- a/src/proof/dimacs_printer.h
+++ b/src/proof/dimacs.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file dimacs_printer.h
+/*! \file dimacs.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Alex Ozdemir
@@ -11,16 +11,17 @@
  **
  ** \brief DIMACS SAT Problem Format
  **
- ** Defines serialization for SAT problems as DIMACS
+ ** Defines serialization/deserialization for SAT problems as DIMACS
  **/
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__PROOF__DIMACS_PRINTER_H
-#define CVC4__PROOF__DIMACS_PRINTER_H
+#ifndef CVC4__PROOF__DIMACS_H
+#define CVC4__PROOF__DIMACS_H
 
 #include <iosfwd>
 #include <memory>
+#include <unordered_map>
 
 #include "proof/clause_id.h"
 #include "prop/sat_solver_types.h"
@@ -56,11 +57,13 @@ std::ostream& textOut(std::ostream& o, const prop::SatClause& c);
  * @param o where to print to
  * @param usedClauses the CNF formula
  */
-void printDimacs(
-    std::ostream& o,
-    const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses);
+void printDimacs(std::ostream& o,
+                 const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+                 const std::vector<ClauseId>& usedIndices);
+
+std::vector<prop::SatClause> parseDimacs(std::istream& i);
 
 }  // namespace proof
 }  // namespace CVC4
 
-#endif  // CVC4__PROOF__DIMACS_PRINTER_H
+#endif  // CVC4__PROOF__DIMACS_H
diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp
index 22903c3c9..9160546f9 100644
--- a/src/proof/er/er_proof.cpp
+++ b/src/proof/er/er_proof.cpp
@@ -31,7 +31,7 @@
 
 #include "base/cvc4_assert.h"
 #include "base/map_util.h"
-#include "proof/dimacs_printer.h"
+#include "proof/dimacs.h"
 #include "proof/lfsc_proof_printer.h"
 #include "proof/proof_manager.h"
 
@@ -80,8 +80,10 @@ TraceCheckProof TraceCheckProof::fromText(std::istream& in)
   return pf;
 }
 
-ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
-                                     const std::string& dratBinary)
+ErProof ErProof::fromBinaryDratProof(
+    const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+    const std::vector<ClauseId>& usedIds,
+    const std::string& dratBinary)
 {
   std::ostringstream cmd;
   char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
@@ -101,7 +103,7 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
 
   // Write the formula
   std::ofstream formStream(formulaFilename);
-  printDimacs(formStream, usedClauses);
+  printDimacs(formStream, clauses, usedIds);
   formStream.close();
 
   // Write the (binary) DRAT proof
@@ -126,7 +128,8 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
 
   // Parse the resulting TRACECHECK proof into an ER proof.
   std::ifstream tracecheckStream(tracecheckFilename);
-  ErProof proof(usedClauses, TraceCheckProof::fromText(tracecheckStream));
+  TraceCheckProof pf = TraceCheckProof::fromText(tracecheckStream);
+  ErProof proof(clauses, usedIds, std::move(pf));
   tracecheckStream.close();
 
   remove(formulaFilename);
@@ -136,17 +139,21 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
   return proof;
 }
 
-ErProof::ErProof(const ClauseUseRecord& usedClauses,
+ErProof::ErProof(const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+                 const std::vector<ClauseId>& usedIds,
                  TraceCheckProof&& tracecheck)
     : d_inputClauseIds(), d_definitions(), d_tracecheck(tracecheck)
 {
   // Step zero, save input clause Ids for future printing
-  std::transform(usedClauses.begin(),
-                 usedClauses.end(),
-                 std::back_inserter(d_inputClauseIds),
-                 [](const std::pair<ClauseId, prop::SatClause>& pair) {
-                   return pair.first;
-                 });
+  d_inputClauseIds = usedIds;
+
+  // Make a list of (idx, clause pairs), the used ones.
+  std::vector<std::pair<ClauseId, prop::SatClause>> usedClauses;
+  std::transform(
+      usedIds.begin(),
+      usedIds.end(),
+      std::back_inserter(usedClauses),
+      [&](const ClauseId& i) { return make_pair(i, clauses.at(i)); });
 
   // Step one, verify the formula starts the proof
   if (Configuration::isAssertionBuild())
@@ -162,14 +169,6 @@ ErProof::ErProof(const ClauseUseRecord& usedClauses,
           originalClause{usedClauses[i].second.begin(),
                          usedClauses[i].second.end()};
       Assert(traceCheckClause == originalClause);
-      Assert(d_tracecheck.d_lines[i].d_idx = i + 1);
-      Assert(d_tracecheck.d_lines[i].d_chain.size() == 0);
-      Assert(d_tracecheck.d_lines[i].d_clause.size()
-             == usedClauses[i].second.size());
-      for (size_t j = 0, m = usedClauses[i].second.size(); j < m; ++j)
-      {
-        Assert(usedClauses[i].second[j] == d_tracecheck.d_lines[i].d_clause[j]);
-      }
     }
   }
 
diff --git a/src/proof/er/er_proof.h b/src/proof/er/er_proof.h
index f5af0783b..d6cbd9213 100644
--- a/src/proof/er/er_proof.h
+++ b/src/proof/er/er_proof.h
@@ -27,6 +27,7 @@
 #define CVC4__PROOF__ER__ER_PROOF_H
 
 #include <memory>
+#include <unordered_map>
 #include <vector>
 
 #include "proof/clause_id.h"
@@ -36,8 +37,6 @@ namespace CVC4 {
 namespace proof {
 namespace er {
 
-using ClauseUseRecord = std::vector<std::pair<ClauseId, prop::SatClause>>;
-
 /**
  * A definition of the form:
  *    newVar <-> p v (~x_1 ^ ~x_2 ^ ... ^ ~x_n)
@@ -116,11 +115,14 @@ class ErProof
   /**
    * Construct an ER proof from a DRAT proof, using drat2er
    *
-   * @param usedClauses The CNF formula that we're deriving bottom from.
-   * @param dratBinary  The DRAT proof from the SAT solver, as a binary stream.
+   * @param clauses A store of clauses that might be in our formula
+   * @param usedIds the ids of clauses that are actually in our formula
+   * @param dratBinary  The DRAT proof from the SAT solver, as a binary stream
    */
-  static ErProof fromBinaryDratProof(const ClauseUseRecord& usedClauses,
-                                     const std::string& dratBinary);
+  static ErProof fromBinaryDratProof(
+      const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+      const std::vector<ClauseId>& usedIds,
+      const std::string& dratBinary);
 
   /**
    * Construct an ER proof from a TRACECHECK ER proof
@@ -128,10 +130,13 @@ class ErProof
    * This basically just identifies groups of lines which correspond to
    * definitions, and extracts them.
    *
-   * @param usedClauses The CNF formula that we're deriving bottom from.
+   * @param clauses A store of clauses that might be in our formula
+   * @param usedIds the ids of clauses that are actually in our formula
    * @param tracecheck  The TRACECHECK proof, as a stream.
    */
-  ErProof(const ClauseUseRecord& usedClauses, TraceCheckProof&& tracecheck);
+  ErProof(const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+          const std::vector<ClauseId>& usedIds,
+          TraceCheckProof&& tracecheck);
 
   /**
    * Write the ER proof as an LFSC value of type (holds cln).
diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp
index a1939ec92..e414c64c9 100644
--- a/src/proof/lrat/lrat_proof.cpp
+++ b/src/proof/lrat/lrat_proof.cpp
@@ -26,7 +26,7 @@
 
 #include "base/cvc4_assert.h"
 #include "base/output.h"
-#include "proof/dimacs_printer.h"
+#include "proof/dimacs.h"
 #include "proof/lfsc_proof_printer.h"
 
 #if CVC4_USE_DRAT2ER
@@ -104,6 +104,7 @@ void printHints(std::ostream& o,
  */
 void printIndices(std::ostream& o, const std::vector<ClauseIdx>& indices)
 {
+  Assert(indices.size() > 0);
   // Verify that the indices are sorted!
   for (size_t i = 0, n = indices.size() - 1; i < n; ++i)
   {
@@ -123,7 +124,8 @@ void printIndices(std::ostream& o, const std::vector<ClauseIdx>& indices)
 // Prints the LRAT addition line in textual format
 
 LratProof LratProof::fromDratProof(
-    const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses,
+    const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+    const std::vector<ClauseId> usedIds,
     const std::string& dratBinary)
 {
   std::ostringstream cmd;
@@ -141,7 +143,7 @@ LratProof LratProof::fromDratProof(
   AlwaysAssert(r > 0);
   close(r);
   std::ofstream formStream(formulaFilename);
-  printDimacs(formStream, usedClauses);
+  printDimacs(formStream, clauses, usedIds);
   formStream.close();
 
   std::ofstream dratStream(dratFilename);
@@ -206,10 +208,13 @@ LratProof::LratProof(std::istream& textualProof)
         }
         clauses.push_back(di);
       }
-      std::sort(clauses.begin(), clauses.end());
-      std::unique_ptr<LratInstruction> instr(
-          new LratDeletion(clauseIdx, std::move(clauses)));
-      d_instructions.push_back(std::move(instr));
+      if (clauses.size() > 0)
+      {
+        std::sort(clauses.begin(), clauses.end());
+        std::unique_ptr<LratInstruction> instr(
+            new LratDeletion(clauseIdx, std::move(clauses)));
+        d_instructions.push_back(std::move(instr));
+      }
     }
     else
     {
diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h
index 33b2fad3f..54db1837d 100644
--- a/src/proof/lrat/lrat_proof.h
+++ b/src/proof/lrat/lrat_proof.h
@@ -129,15 +129,13 @@ class LratProof
   /**
    * @brief Construct an LRAT proof from a DRAT proof, using drat-trim
    *
-   * @param usedClauses The CNF formula that we're deriving bottom from.
-   *                    It's a map because other parts of the system represent
-   *                    it this way.
-   * @param clauseOrder A record of the order in which those clauses were
-   *                    given to the SAT solver.
+   * @param clauses A store of clauses that might be in our formula
+   * @param usedIds the ids of clauses that are actually in our formula
    * @param dratBinary  The DRAT proof from the SAT solver, as a binary stream.
    */
   static LratProof fromDratProof(
-      const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses,
+      const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+      const std::vector<ClauseId> usedIds,
       const std::string& dratBinary);
   /**
    * @brief Construct an LRAT proof from its textual representation
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 66198946f..303295112 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -31,6 +31,7 @@
 
 #include "base/configuration.h"
 #include "base/configuration_private.h"
+#include "base/cvc4_check.h"
 #include "base/exception.h"
 #include "base/listener.h"
 #include "base/modal_exception.h"
@@ -888,6 +889,7 @@ SmtEngine::SmtEngine(ExprManager* em)
       d_earlyTheoryPP(true),
       d_globalNegation(false),
       d_status(),
+      d_expectedStatus(),
       d_replayStream(NULL),
       d_private(NULL),
       d_statisticsRegistry(NULL),
@@ -2420,7 +2422,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
       throw OptionException("argument to (set-info :status ..) must be "
                             "`sat' or `unsat' or `unknown'");
     }
-    d_status = Result(s, d_filename);
+    d_expectedStatus = Result(s, d_filename);
     return;
   }
   throw UnrecognizedOptionException();
@@ -3747,6 +3749,13 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
 
     // Remember the status
     d_status = r;
+    if (!d_expectedStatus.isUnknown() && !d_status.isUnknown()
+        && d_status != d_expectedStatus)
+    {
+      CVC4_FATAL() << "Expected result " << d_expectedStatus << " but got "
+                   << d_status;
+    }
+    d_expectedStatus = Result();
 
     setProblemExtended(false);
 
@@ -4428,13 +4437,7 @@ void SmtEngine::checkProof()
 
   std::string logicString = d_logic.getLogicString();
 
-  if (!(
-          // Pure logics
-          logicString == "QF_UF" || logicString == "QF_AX"
-          || logicString == "QF_BV" ||
-          // Non-pure logics
-          logicString == "QF_AUF" || logicString == "QF_UFBV"
-          || logicString == "QF_ABV" || logicString == "QF_AUFBV"))
+  if (!(d_logic <= LogicInfo("QF_AUFBVLRA")))
   {
     // This logic is not yet supported
     Notice() << "Notice: no proof-checking for " << logicString << " proofs yet"
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 165e93997..5913716e6 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -263,6 +263,11 @@ class CVC4_PUBLIC SmtEngine {
   Result d_status;
 
   /**
+   * The expected status of the next satisfiability check.
+   */
+  Result d_expectedStatus;
+
+  /**
    * The input file name (if any) or the name set through setInfo (if any)
    */
   std::string d_filename;
diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
index c054cb666..4018cc3dc 100644
--- a/src/smt/smt_engine.i
+++ b/src/smt/smt_engine.i
@@ -42,6 +42,9 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acsys_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jc
       swigCPtr = 0;
     }
   }
+
+%template(Map_ExprExpr) std::map<CVC4::Expr, CVC4::Expr>;
+
 #endif // SWIGJAVA
 
 %ignore CVC4::SmtEngine::setLogic(const char*);
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index a69cf8c96..fbdce8cd5 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -157,17 +157,17 @@ symbolicRoundingMode traits::RTN(void) { return symbolicRoundingMode(0x08); };
 symbolicRoundingMode traits::RTZ(void) { return symbolicRoundingMode(0x10); };
 void traits::precondition(const bool b)
 {
-  Assert(b);
+  AlwaysAssert(b);
   return;
 }
 void traits::postcondition(const bool b)
 {
-  Assert(b);
+  AlwaysAssert(b);
   return;
 }
 void traits::invariant(const bool b)
 {
-  Assert(b);
+  AlwaysAssert(b);
   return;
 }
 
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 1712bb30a..e21d1f630 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -17,9 +17,10 @@
  **/
 #include "theory/logic_info.h"
 
-#include <string>
 #include <cstring>
+#include <iostream>
 #include <sstream>
+#include <string>
 
 #include "base/cvc4_assert.h"
 #include "expr/kind.h"
@@ -207,13 +208,15 @@ bool LogicInfo::operator==(const LogicInfo& other) const {
 
   PrettyCheckArgument(d_sharingTheories == other.d_sharingTheories, *this,
                       "LogicInfo internal inconsistency");
+  bool res = d_cardinalityConstraints == other.d_cardinalityConstraints
+             && d_higherOrder == other.d_higherOrder;
   if(isTheoryEnabled(theory::THEORY_ARITH)) {
     return d_integers == other.d_integers && d_reals == other.d_reals
            && d_transcendentals == other.d_transcendentals
            && d_linear == other.d_linear
-           && d_differenceLogic == other.d_differenceLogic;
+           && d_differenceLogic == other.d_differenceLogic && res;
   } else {
-    return true;
+    return res;
   }
 }
 
@@ -227,13 +230,15 @@ bool LogicInfo::operator<=(const LogicInfo& other) const {
   }
   PrettyCheckArgument(d_sharingTheories <= other.d_sharingTheories, *this,
                       "LogicInfo internal inconsistency");
+  bool res = (!d_cardinalityConstraints || other.d_cardinalityConstraints)
+             && (!d_higherOrder || other.d_higherOrder);
   if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
     return (!d_integers || other.d_integers) && (!d_reals || other.d_reals)
            && (!d_transcendentals || other.d_transcendentals)
            && (d_linear || !other.d_linear)
-           && (d_differenceLogic || !other.d_differenceLogic);
+           && (d_differenceLogic || !other.d_differenceLogic) && res;
   } else {
-    return true;
+    return res;
   }
 }
 
@@ -247,13 +252,15 @@ bool LogicInfo::operator>=(const LogicInfo& other) const {
   }
   PrettyCheckArgument(d_sharingTheories >= other.d_sharingTheories, *this,
                       "LogicInfo internal inconsistency");
+  bool res = (d_cardinalityConstraints || !other.d_cardinalityConstraints)
+             && (d_higherOrder || !other.d_higherOrder);
   if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
     return (d_integers || !other.d_integers) && (d_reals || !other.d_reals)
            && (d_transcendentals || !other.d_transcendentals)
            && (!d_linear || other.d_linear)
-           && (!d_differenceLogic || other.d_differenceLogic);
+           && (!d_differenceLogic || other.d_differenceLogic) && res;
     } else {
-    return true;
+      return res;
   }
 }
 
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index 4aed27c30..f7e73ca4b 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -441,17 +441,17 @@ rm traits::RTZ(void) { return ::CVC4::roundTowardZero; };
 
 void traits::precondition(const prop &p)
 {
-  Assert(p);
+  AlwaysAssert(p);
   return;
 }
 void traits::postcondition(const prop &p)
 {
-  Assert(p);
+  AlwaysAssert(p);
   return;
 }
 void traits::invariant(const prop &p)
 {
-  Assert(p);
+  AlwaysAssert(p);
   return;
 }
 }