Merge branch 'master' of https://github.com/CVC4/CVC4.git

Conflicts:
	proofs/signatures/Makefile.am
	src/Makefile.am
	src/expr/datatype.cpp
	src/options/datatypes_options
	src/options/options_template.cpp
	src/options/quantifiers_options
	src/proof/arith_proof.cpp
	src/proof/arith_proof.h
	src/proof/array_proof.cpp
	src/proof/array_proof.h
	src/proof/bitvector_proof.cpp
	src/proof/bitvector_proof.h
	src/proof/cnf_proof.cpp
	src/proof/cnf_proof.h
	src/proof/proof_manager.cpp
	src/proof/proof_manager.h
	src/proof/sat_proof.h
	src/proof/sat_proof_implementation.h
	src/proof/skolemization_manager.h
	src/proof/theory_proof.cpp
	src/proof/theory_proof.h
	src/proof/uf_proof.cpp
	src/proof/uf_proof.h
	src/prop/cnf_stream.cpp
	src/prop/cnf_stream.h
	src/prop/minisat/core/Solver.cc
	src/prop/prop_engine.cpp
	src/prop/prop_engine.h
	src/prop/theory_proxy.cpp
	src/smt/smt_engine.cpp
	src/smt/smt_engine_check_proof.cpp
	src/theory/arrays/array_proof_reconstruction.cpp
	src/theory/arrays/theory_arrays.cpp
	src/theory/bv/eager_bitblaster.cpp
	src/theory/bv/lazy_bitblaster.cpp
	src/theory/datatypes/theory_datatypes.cpp
	src/theory/quantifiers/alpha_equivalence.cpp
	src/theory/quantifiers/candidate_generator.cpp
	src/theory/quantifiers/candidate_generator.h
	src/theory/quantifiers/ce_guided_single_inv.cpp
	src/theory/quantifiers/ceg_instantiator.cpp
	src/theory/quantifiers/conjecture_generator.cpp
	src/theory/quantifiers/equality_infer.cpp
	src/theory/quantifiers/equality_infer.h
	src/theory/quantifiers/inst_match_generator.cpp
	src/theory/quantifiers/inst_propagator.cpp
	src/theory/quantifiers/inst_propagator.h
	src/theory/quantifiers/inst_strategy_e_matching.cpp
	src/theory/quantifiers/inst_strategy_e_matching.h
	src/theory/quantifiers/instantiation_engine.cpp
	src/theory/quantifiers/model_builder.cpp
	src/theory/quantifiers/model_engine.cpp
	src/theory/quantifiers/quant_conflict_find.cpp
	src/theory/quantifiers/quant_conflict_find.h
	src/theory/quantifiers/quant_split.cpp
	src/theory/quantifiers/quant_util.cpp
	src/theory/quantifiers/quantifiers_rewriter.cpp
	src/theory/quantifiers/quantifiers_rewriter.h
	src/theory/quantifiers/term_database.cpp
	src/theory/quantifiers/term_database.h
	src/theory/quantifiers/trigger.cpp
	src/theory/quantifiers/trigger.h
	src/theory/quantifiers_engine.cpp
	src/theory/quantifiers_engine.h
	src/theory/sets/kinds
	src/theory/sets/theory_sets_private.cpp
	src/theory/sets/theory_sets_private.h
	src/theory/sets/theory_sets_rewriter.cpp
	src/theory/sets/theory_sets_type_rules.h
	src/theory/strings/theory_strings.cpp
	src/theory/strings/theory_strings.h
	src/theory/theory_engine.cpp
	src/theory/theory_engine.h
	src/theory/uf/equality_engine.cpp
	test/regress/regress0/fmf/Makefile.am
	test/regress/regress0/quantifiers/Makefile.am
	test/regress/regress0/strings/Makefile.am
	test/regress/regress0/sygus/Makefile.am
	test/regress/regress0/sygus/max2-univ.sy

14 files changed, 477 insertions, 48 deletions

diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 20724efd2..56a7c61e2 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -78,6 +78,10 @@ public:
 
   ClauseId addClause(SatClause& clause, bool removable);
 
+  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) {
+    Unreachable("Minisat does not support native XOR reasoning");
+  }
+  
   SatValue propagate();
 
   SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index aa1fc9587..eda736b8a 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -120,7 +120,7 @@ bool CnfStream::hasLiteral(TNode n) const {
   return find != d_nodeToLiteralMap.end();
 }
 
-void TseitinCnfStream::ensureLiteral(TNode n) {
+void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) {
   // These are not removable and have no proof ID
   d_removable = false;
 
@@ -163,7 +163,7 @@ void TseitinCnfStream::ensureLiteral(TNode n) {
     d_literalToNodeMap.insert_safe(~lit, n.notNode());
   } else {
     // We have a theory atom or variable.
-    lit = convertAtom(n);
+    lit = convertAtom(n, noPreregistration);
   }
 
   Assert(hasLiteral(n) && getNode(lit) == n);
@@ -232,7 +232,7 @@ void CnfStream::setProof(CnfProof* proof) {
   d_cnfProof = proof;
 }
 
-SatLiteral CnfStream::convertAtom(TNode node) {
+SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) {
   Debug("cnf") << "convertAtom(" << node << ")" << endl;
 
   Assert(!hasLiteral(node), "atom already mapped!");
@@ -247,7 +247,7 @@ SatLiteral CnfStream::convertAtom(TNode node) {
   } else {
     theoryLiteral = true;
     canEliminate = false;
-    preRegister = true;
+    preRegister = !noPreregistration;
   }
 
   // Make a new literal (variables are not considered theory literals)
@@ -258,7 +258,11 @@ SatLiteral CnfStream::convertAtom(TNode node) {
 
 SatLiteral CnfStream::getLiteral(TNode node) {
   Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node");
-  Assert(d_nodeToLiteralMap.contains(node), "Literal not in the CNF Cache: %s\n", node.toString().c_str());
+
+  Assert(d_nodeToLiteralMap.contains(node),
+         "Literal not in the CNF Cache: %s\n",
+         node.toString().c_str());
+
   SatLiteral literal = d_nodeToLiteralMap[node];
   Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
   return literal;
@@ -675,7 +679,7 @@ void TseitinCnfStream::convertAndAssert(TNode node,
                                         bool negated,
                                         ProofRule proof_id,
                                         TNode from,
-                                        theory::TheoryId ownerTheory) {
+                                        LemmaProofRecipe* proofRecipe) {
   Debug("cnf") << "convertAndAssert(" << node
                << ", removable = " << (removable ? "true" : "false")
                << ", negated = " << (negated ? "true" : "false") << ")" << endl;
@@ -685,7 +689,12 @@ void TseitinCnfStream::convertAndAssert(TNode node,
       Node assertion = negated ? node.notNode() : (Node)node;
       Node from_assertion = negated? from.notNode() : (Node) from;
 
-      d_cnfProof->setExplainerTheory(ownerTheory);
+      if (proofRecipe) {
+        Debug("pf::sat") << "TseitinCnfStream::convertAndAssert: setting proof recipe" << std::endl;
+        proofRecipe->dump("pf::sat");
+        d_cnfProof->setProofRecipe(proofRecipe);
+      }
+
       if (proof_id != RULE_INVALID) {
         d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion);
         d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id);
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index cf9d519a7..6cc10d878 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -36,6 +36,9 @@
 #include "smt_util/lemma_channels.h"
 
 namespace CVC4 {
+
+class LemmaProofRecipe;
+
 namespace prop {
 
 class PropEngine;
@@ -174,7 +177,7 @@ protected:
    * structure in this expression.  Assumed to not be in the
    * translation cache.
    */
-  SatLiteral convertAtom(TNode node);
+  SatLiteral convertAtom(TNode node, bool noPreprocessing = false);
 
 public:
 
@@ -207,14 +210,10 @@ public:
    * @param node node to convert and assert
    * @param removable whether the sat solver can choose to remove the clauses
    * @param negated whether we are asserting the node negated
-   * @param ownerTheory indicates the theory that should invoked to prove the formula.
+   * @param proofRecipe contains the proof recipe for proving this node
    */
-  virtual void convertAndAssert(TNode node,
-                                bool removable,
-                                bool negated,
-                                ProofRule proof_id,
-                                TNode from = TNode::null(),
-                                theory::TheoryId ownerTheory = theory::THEORY_LAST) = 0;
+  virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null(), LemmaProofRecipe* proofRecipe = NULL) = 0;
+
   /**
    * Get the node that is represented by the given SatLiteral.
    * @param literal the literal from the sat solver
@@ -235,7 +234,7 @@ public:
    * this is like a "convert-but-don't-assert" version of
    * convertAndAssert().
    */
-  virtual void ensureLiteral(TNode n) = 0;
+  virtual void ensureLiteral(TNode n, bool noPreregistration = false) = 0;
 
   /**
    * Returns the literal that represents the given node in the SAT CNF
@@ -284,7 +283,7 @@ public:
    */
   void convertAndAssert(TNode node, bool removable,
                         bool negated, ProofRule rule, TNode from = TNode::null(),
-                        theory::TheoryId ownerTheory = theory::THEORY_LAST);
+                        LemmaProofRecipe* proofRecipe = NULL);
 
   /**
    * Constructs the stream to use the given sat solver.
@@ -337,7 +336,7 @@ private:
    */
   SatLiteral toCNF(TNode node, bool negated = false);
 
-  void ensureLiteral(TNode n);
+  void ensureLiteral(TNode n, bool noPreregistration = false);
 
 };/* class TseitinCnfStream */
 
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
new file mode 100644
index 000000000..d8f25a786
--- /dev/null
+++ b/src/prop/cryptominisat.cpp
@@ -0,0 +1,230 @@
+/*********************                                                        */
+/*! \file cryptominisat.cpp
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2014  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 SAT Solver.
+ **
+ ** Implementation of the cryptominisat for cvc4 (bitvectors).
+ **/
+
+#include "prop/cryptominisat.h"
+
+#include "proof/clause_id.h"
+#include "proof/sat_proof.h"
+
+using namespace CVC4;
+using namespace prop;
+
+#ifdef CVC4_USE_CRYPTOMINISAT
+
+CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
+                                         const std::string& name)
+: d_solver(new CMSat::SATSolver())
+, d_numVariables(0)
+, d_okay(true)
+, d_statistics(registry, name)
+{
+  d_true = newVar();
+  d_false = newVar();
+
+  std::vector<CMSat::Lit> clause(1);
+  clause[0] = CMSat::Lit(d_true, false);
+  d_solver->add_clause(clause);
+  
+  clause[0] = CMSat::Lit(d_false, true);
+  d_solver->add_clause(clause);
+}
+
+
+CryptoMinisatSolver::~CryptoMinisatSolver() throw(AssertionException) {
+  delete d_solver;
+}
+
+ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause,
+				       bool rhs,
+				       bool removable) {
+  Debug("sat::cryptominisat") << "Add xor clause " << clause <<" = " << rhs << "\n";
+
+  if (!d_okay) {
+    Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n";
+    return ClauseIdError;
+  }
+
+  ++(d_statistics.d_xorClausesAdded);
+  
+  // ensure all sat literals have positive polarity by pushing
+  // the negation on the result
+  std::vector<CMSat::Var> xor_clause;
+  for (unsigned i = 0; i < clause.size(); ++i) {
+    xor_clause.push_back(toInternalLit(clause[i]).var());
+    rhs ^= clause[i].isNegated();
+  }
+  bool res = d_solver->add_xor_clause(xor_clause, rhs);
+  d_okay &= res;
+  return ClauseIdError;
+}
+
+ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){
+  Debug("sat::cryptominisat") << "Add clause " << clause <<"\n";
+
+  if (!d_okay) {
+    Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n";
+    return ClauseIdError;
+  }
+
+  ++(d_statistics.d_clausesAdded);
+  
+  std::vector<CMSat::Lit> internal_clause;
+  toInternalClause(clause, internal_clause);
+  bool res = d_solver->add_clause(internal_clause);
+  d_okay &= res;
+  return ClauseIdError;
+}
+
+bool CryptoMinisatSolver::ok() const {
+  return d_okay; 
+}
+
+
+SatVariable  CryptoMinisatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){
+  d_solver->new_var();
+  ++d_numVariables;
+  Assert (d_numVariables == d_solver->nVars());
+  return d_numVariables - 1;
+}
+
+SatVariable CryptoMinisatSolver::trueVar() {
+  return d_true;
+}
+
+SatVariable CryptoMinisatSolver::falseVar() {
+  return d_false;
+}
+
+void CryptoMinisatSolver::markUnremovable(SatLiteral lit) {
+  // cryptominisat supports dynamically adding back variables (?)
+  // so this is a no-op
+  return;
+}
+
+void CryptoMinisatSolver::interrupt(){
+  d_solver->interrupt_asap();
+}
+
+SatValue CryptoMinisatSolver::solve(){
+  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
+  ++d_statistics.d_statCallsToSolve;
+  return toSatLiteralValue(d_solver->solve());
+}
+
+SatValue CryptoMinisatSolver::solve(long unsigned int& resource) {
+  // CMSat::SalverConf conf = d_solver->getConf();
+  Unreachable("Not sure how to set different limits for calls to solve in Cryptominisat"); 
+  return solve();
+}
+
+SatValue CryptoMinisatSolver::value(SatLiteral l){
+  const std::vector<CMSat::lbool> model = d_solver->get_model();
+  CMSat::Var var = l.getSatVariable();
+  Assert (var < model.size());
+  CMSat::lbool value = model[var];
+  return toSatLiteralValue(value);
+}
+
+SatValue CryptoMinisatSolver::modelValue(SatLiteral l){
+  return value(l); 
+}
+
+unsigned CryptoMinisatSolver::getAssertionLevel() const {
+  Unreachable("No interface to get assertion level in Cryptominisat");
+  return -1; 
+}
+
+// converting from internal sat solver representation
+
+SatVariable CryptoMinisatSolver::toSatVariable(CMSat::Var var) {
+  if (var == CMSat::var_Undef) {
+    return undefSatVariable;
+  }
+  return SatVariable(var);
+}
+
+CMSat::Lit CryptoMinisatSolver::toInternalLit(SatLiteral lit) {
+  if (lit == undefSatLiteral) {
+    return CMSat::lit_Undef;
+  }
+  return CMSat::Lit(lit.getSatVariable(), lit.isNegated());
+}
+
+SatLiteral CryptoMinisatSolver::toSatLiteral(CMSat::Lit lit) {
+  Assert (lit != CMSat::lit_Error);
+  if (lit == CMSat::lit_Undef) {
+    return undefSatLiteral;
+  }
+
+  return SatLiteral(SatVariable(lit.var()),
+                    lit.sign());
+}
+
+SatValue CryptoMinisatSolver::toSatLiteralValue(CMSat::lbool res) {
+  if(res == CMSat::l_True) return SAT_VALUE_TRUE;
+  if(res == CMSat::l_Undef) return SAT_VALUE_UNKNOWN;
+  Assert(res == CMSat::l_False);
+  return SAT_VALUE_FALSE;
+}
+
+void CryptoMinisatSolver::toInternalClause(SatClause& clause,
+                                           std::vector<CMSat::Lit>& internal_clause) {
+  for (unsigned i = 0; i < clause.size(); ++i) {
+    internal_clause.push_back(toInternalLit(clause[i]));
+  }
+  Assert(clause.size() == internal_clause.size());
+}
+
+void CryptoMinisatSolver::toSatClause(std::vector<CMSat::Lit>& clause,
+                                       SatClause& sat_clause) {
+  for (unsigned i = 0; i < clause.size(); ++i) {
+    sat_clause.push_back(toSatLiteral(clause[i]));
+  }
+  Assert(clause.size() == sat_clause.size());
+}
+
+
+// Satistics for CryptoMinisatSolver
+
+CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry* registry,
+                                            const std::string& prefix) :
+  d_registry(registry),
+  d_statCallsToSolve("theory::bv::"+prefix+"::cryptominisat::calls_to_solve", 0),
+  d_xorClausesAdded("theory::bv::"+prefix+"::cryptominisat::xor_clauses", 0),
+  d_clausesAdded("theory::bv::"+prefix+"::cryptominisat::clauses", 0),
+  d_solveTime("theory::bv::"+prefix+"::cryptominisat::solve_time"),
+  d_registerStats(!prefix.empty())
+{
+  if (!d_registerStats)
+    return;
+
+  d_registry->registerStat(&d_statCallsToSolve);
+  d_registry->registerStat(&d_xorClausesAdded);
+  d_registry->registerStat(&d_clausesAdded);
+  d_registry->registerStat(&d_solveTime);
+}
+
+CryptoMinisatSolver::Statistics::~Statistics() {
+  if (!d_registerStats)
+    return;
+  d_registry->unregisterStat(&d_statCallsToSolve);
+  d_registry->unregisterStat(&d_xorClausesAdded);
+  d_registry->unregisterStat(&d_clausesAdded);
+  d_registry->unregisterStat(&d_solveTime);
+}
+#endif
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
new file mode 100644
index 000000000..54d52af0e
--- /dev/null
+++ b/src/prop/cryptominisat.h
@@ -0,0 +1,138 @@
+/*********************                                                        */
+/*! \file cryptominisat.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2014  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 SAT Solver.
+ **
+ ** Implementation of the cryptominisat sat solver for cvc4 (bitvectors).
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "prop/sat_solver.h"
+
+#ifdef CVC4_USE_CRYPTOMINISAT
+#include <cryptominisat4/cryptominisat.h>
+namespace CVC4 {
+namespace prop {
+
+class CryptoMinisatSolver : public SatSolver {
+
+private:
+  CMSat::SATSolver* d_solver;
+  unsigned d_numVariables;
+  bool d_okay;
+  SatVariable d_true;
+  SatVariable d_false;
+public:
+  CryptoMinisatSolver(StatisticsRegistry* registry,
+                      const std::string& name = "");
+  ~CryptoMinisatSolver() throw(AssertionException);
+
+  ClauseId addClause(SatClause& clause, bool removable);
+  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable);
+
+  bool nativeXor() { return true; }
+  
+  SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
+
+  SatVariable trueVar();
+  SatVariable falseVar();
+
+  void markUnremovable(SatLiteral lit);
+
+  void interrupt();
+  
+  SatValue solve();
+  SatValue solve(long unsigned int&);
+  bool ok() const;
+  SatValue value(SatLiteral l);
+  SatValue modelValue(SatLiteral l);
+
+  unsigned getAssertionLevel() const;
+
+
+  // helper methods for converting from the internal Minisat representation
+
+  static SatVariable toSatVariable(CMSat::Var var);
+  static CMSat::Lit toInternalLit(SatLiteral lit);
+  static SatLiteral toSatLiteral(CMSat::Lit lit);
+  static SatValue toSatLiteralValue(bool res);
+  static SatValue toSatLiteralValue(CMSat::lbool res);
+
+  static void  toInternalClause(SatClause& clause, std::vector<CMSat::Lit>& internal_clause);
+  static void  toSatClause (std::vector<CMSat::Lit>& clause, SatClause& sat_clause);
+
+  class Statistics {
+  public:
+    StatisticsRegistry* d_registry;
+    IntStat d_statCallsToSolve;
+    IntStat d_xorClausesAdded;
+    IntStat d_clausesAdded;
+    TimerStat d_solveTime;
+    bool d_registerStats;
+    Statistics(StatisticsRegistry* registry,
+               const std::string& prefix);
+    ~Statistics();
+  };
+
+  Statistics d_statistics;
+};
+} // CVC4::prop
+} // CVC4
+
+#else // CVC4_USE_CRYPTOMINISAT
+
+namespace CVC4 {
+namespace prop {
+
+class CryptoMinisatSolver : public SatSolver {
+
+public:
+  CryptoMinisatSolver(StatisticsRegistry* registry,
+                      const std::string& name = "") { Unreachable(); }
+  /** Assert a clause in the solver. */
+  ClauseId addClause(SatClause& clause, bool removable) {
+    Unreachable();
+  }
+
+  /** Return true if the solver supports native xor resoning */
+  bool nativeXor() { Unreachable(); }
+
+  /** Add a clause corresponding to rhs = l1 xor .. xor ln  */
+  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) {
+    Unreachable();
+  }
+  
+  SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) { Unreachable(); }
+  SatVariable trueVar() { Unreachable(); }
+  SatVariable falseVar() { Unreachable(); }
+  SatValue solve() { Unreachable(); }
+  SatValue solve(long unsigned int&) { Unreachable(); }
+  void interrupt() { Unreachable(); }
+  SatValue value(SatLiteral l) { Unreachable(); }
+  SatValue modelValue(SatLiteral l) { Unreachable(); }
+  unsigned getAssertionLevel() const { Unreachable(); }
+  bool ok() const { return false;};
+  
+
+};/* class CryptoMinisatSolver */
+} // CVC4::prop
+} // CVC4
+
+#endif // CVC4_USE_CRYPTOMINISAT
+
+
+
+
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 411b89514..a682a893b 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -232,6 +232,8 @@ CRef Solver::reason(Var x) {
     vec<Lit> explanation;
     MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
 
+    Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl << std::endl;
+
     // Sort the literals by trail index level
     lemma_lt lt(*this);
     sort(explanation, lt);
@@ -266,6 +268,12 @@ CRef Solver::reason(Var x) {
     }
     explanation.shrink(i - j);
 
+    Debug("pf::sat") << "Solver::reason: explanation = " ;
+    for (int i = 0; i < explanation.size(); ++i) {
+      Debug("pf::sat") << explanation[i] << " ";
+    }
+    Debug("pf::sat") << std::endl;
+
     // We need an explanation clause so we add a fake literal
     if (j == 1) {
       // Add not TRUE to the clause
@@ -276,6 +284,7 @@ CRef Solver::reason(Var x) {
     CRef real_reason = ca.alloc(explLevel, explanation, true);
     // FIXME: at some point will need more information about where this explanation
     // came from (ie. the theory/sharing)
+    Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl;
     PROOF (ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA);
            ProofManager::getCnfProof()->registerConvertedClause(id, true);
            // no need to pop current assertion as this is not converted to cnf
@@ -336,6 +345,12 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 
     // If we are in solve or decision level > 0
     if (minisat_busy || decisionLevel() > 0) {
+      Debug("pf::sat") << "Add clause adding a new lemma: ";
+      for (int k = 0; k < ps.size(); ++k) {
+        Debug("pf::sat") << ps[k] << " ";
+      }
+      Debug("pf::sat") << std::endl;
+
       lemmas.push();
       ps.copyTo(lemmas.last());
       lemmas_removable.push(removable);
@@ -379,7 +394,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 
         cr = ca.alloc(clauseLevel, ps, false);
         clauses_persistent.push(cr);
-	attachClause(cr);
+        attachClause(cr);
 
         if(PROOF_ON()) {
           PROOF(
@@ -1234,12 +1249,12 @@ lbool Solver::search(int nof_conflicts)
 
         } else {
 
-	    // If this was a final check, we are satisfiable
+            // If this was a final check, we are satisfiable
             if (check_type == CHECK_FINAL) {
-	      bool decisionEngineDone = proxy->isDecisionEngineDone();
+              bool decisionEngineDone = proxy->isDecisionEngineDone();
               // Unless a lemma has added more stuff to the queues
               if (!decisionEngineDone  &&
-		  (!order_heap.empty() || qhead < trail.size()) ) {
+                  (!order_heap.empty() || qhead < trail.size()) ) {
                 check_type = CHECK_WITH_THEORY;
                 continue;
               } else if (recheck) {
@@ -1666,6 +1681,13 @@ CRef Solver::updateLemmas() {
     {
       // The current lemma
       vec<Lit>& lemma = lemmas[i];
+
+      Debug("pf::sat") << "Solver::updateLemmas: working on lemma: ";
+      for (int k = 0; k < lemma.size(); ++k) {
+        Debug("pf::sat") << lemma[k] << " ";
+      }
+      Debug("pf::sat") << std::endl;
+
       // If it's an empty lemma, we have a conflict at zero level
       if (lemma.size() == 0) {
         Assert (! PROOF_ON());
@@ -1725,6 +1747,7 @@ CRef Solver::updateLemmas() {
          TNode cnf_assertion = lemmas_cnf_assertion[i].first;
          TNode cnf_def = lemmas_cnf_assertion[i].second;
 
+         Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl;
          ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA);
          ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
          ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
@@ -1741,6 +1764,7 @@ CRef Solver::updateLemmas() {
          Node cnf_assertion = lemmas_cnf_assertion[i].first;
          Node cnf_def = lemmas_cnf_assertion[i].second;
 
+         Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3)" << std::endl;
          ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA);
          ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
          ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index bfbf9da6f..ff726e299 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -150,7 +150,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
   // FIXME: This relies on the invariant that when ok() is false
   // the SAT solver does not add the clause (which is what Minisat currently does)
   if (!ok()) {
-    return ClauseIdUndef; 
+    return ClauseIdUndef;
   }
   d_minisat->addClause(minisat_clause, removable, clause_id);
   PROOF( Assert (clause_id != ClauseIdError););
@@ -185,7 +185,7 @@ SatValue MinisatSatSolver::solve() {
 }
 
 bool MinisatSatSolver::ok() const {
-  return d_minisat->okay(); 
+  return d_minisat->okay();
 }
 
 void MinisatSatSolver::interrupt() {
@@ -204,20 +204,20 @@ bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const
   return true;
 }
 
-void MinisatSatSolver::requirePhase(SatLiteral lit) { 
+void MinisatSatSolver::requirePhase(SatLiteral lit) {
   Assert(!d_minisat->rnd_pol);
   Debug("minisat") << "requirePhase(" << lit << ")" << " " <<  lit.getSatVariable() << " " << lit.isNegated() << std::endl;
   SatVariable v = lit.getSatVariable();
   d_minisat->freezePolarity(v, lit.isNegated());
 }
 
-bool MinisatSatSolver::flipDecision() { 
+bool MinisatSatSolver::flipDecision() {
   Debug("minisat") << "flipDecision()" << std::endl;
   return d_minisat->flipDecision();
 }
 
-bool MinisatSatSolver::isDecision(SatVariable decn) const { 
-  return d_minisat->isDecision( decn ); 
+bool MinisatSatSolver::isDecision(SatVariable decn) const {
+  return d_minisat->isDecision( decn );
 }
 
 /** Incremental interface */
@@ -291,7 +291,7 @@ namespace CVC4 {
 template<>
 prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) {
   return prop::MinisatSatSolver::toSatLiteral(lit);
-} 
+}
 
 template<>
 void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl,
@@ -300,5 +300,3 @@ void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause&
 }
 
 } /* namespace CVC4 */
-
-
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 535ce1a47..ec5297bb7 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -44,6 +44,9 @@ public:
   void initialize(context::Context* context, TheoryProxy* theoryProxy);
 
   ClauseId addClause(SatClause& clause, bool removable);
+  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) {
+    Unreachable("Minisat does not support native XOR reasoning");
+  }
 
   SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase);
   SatVariable trueVar() { return d_minisat->trueVar(); }
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 54cf4c457..eb607e901 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -132,13 +132,13 @@ void PropEngine::assertFormula(TNode node) {
 void PropEngine::assertLemma(TNode node, bool negated,
                              bool removable,
                              ProofRule rule,
-                             theory::TheoryId ownerTheory,
+                             LemmaProofRecipe* proofRecipe,
                              TNode from) {
   //Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
   // Assert as (possibly) removable
-  d_cnfStream->convertAndAssert(node, removable, negated, rule, from, ownerTheory);
+  d_cnfStream->convertAndAssert(node, removable, negated, rule, from, proofRecipe);
 }
 
 void PropEngine::requirePhase(TNode n, bool phase) {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index b9ce7ca7e..c02015931 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -37,6 +37,7 @@ namespace CVC4 {
 class ResourceManager;
 class DecisionEngine;
 class TheoryEngine;
+class LemmaProofRecipe;
 
 namespace theory {
   class TheoryRegistrar;
@@ -134,7 +135,7 @@ public:
    * @param removable whether this lemma can be quietly removed based
    * on an activity heuristic (or not)
    */
-  void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, theory::TheoryId ownerTheory, TNode from = TNode::null());
+  void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, LemmaProofRecipe* proofRecipe, TNode from = TNode::null());
 
   /**
    * If ever n is decided upon, it must be in the given phase.  This
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 92696ae25..81fb94242 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -49,6 +49,12 @@ public:
   virtual ClauseId addClause(SatClause& clause,
                              bool removable) = 0;
 
+  /** Return true if the solver supports native xor resoning */
+  virtual bool nativeXor() { return false; }
+
+  /** Add a clause corresponding to rhs = l1 xor .. xor ln  */
+  virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0;
+  
   /**
    * Create a new boolean variable in the solver.
    * @param isTheoryAtom is this a theory atom that needs to be asserted to theory
@@ -84,7 +90,8 @@ public:
 
   /** Check if the solver is in an inconsistent state */
   virtual bool ok() const = 0;
-
+  
+  virtual void setProofLog( BitVectorProof * bvp ) {}
   
 };/* class SatSolver */
 
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 092ec72f2..7fdc44e66 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -16,6 +16,7 @@
 
 #include "prop/sat_solver_factory.h"
 
+#include "prop/cryptominisat.h"
 #include "prop/minisat/minisat.h"
 #include "prop/bvminisat/bvminisat.h"
 
@@ -26,6 +27,12 @@ BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatC
   return new BVMinisatSatSolver(registry, mainSatContext, name);
 }
 
+SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry,
+                                                   const std::string& name) {
+return new CryptoMinisatSolver(registry, name);
+}
+  
+
 DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(StatisticsRegistry* registry) {
   return new MinisatSatSolver(registry);
 }
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index 7cc23a8e8..a04bcaaf4 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -35,6 +35,8 @@ public:
                                              StatisticsRegistry* registry,
                                              const std::string& name = "");
   static DPLLSatSolverInterface* createDPLLMinisat(StatisticsRegistry* registry);
+  static SatSolver* createCryptoMinisat(StatisticsRegistry* registry,
+                                        const std::string& name = "");
 
 };/* class SatSolverFactory */
 
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 4a4515eb9..6e8f1fbbf 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -99,29 +99,34 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   TNode lNode = d_cnfStream->getNode(l);
   Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
 
-  NodeTheoryPair theoryExplanation = d_theoryEngine->getExplanationAndExplainer(lNode);
-  Node explanationNode = theoryExplanation.node;
-  theory::TheoryId explainerTheory = theoryExplanation.theory;
+  LemmaProofRecipe* proofRecipe = NULL;
+  PROOF(proofRecipe = new LemmaProofRecipe;);
+
+  Node theoryExplanation = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe);
 
   PROOF({
-      ProofManager::getCnfProof()->pushCurrentAssertion(explanationNode);
-      ProofManager::getCnfProof()->setExplainerTheory(explainerTheory);
+      ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
+      ProofManager::getCnfProof()->setProofRecipe(proofRecipe);
+
+      Debug("pf::sat") << "TheoryProxy::explainPropagation: setting lemma recipe to: "
+                       << std::endl;
+      proofRecipe->dump("pf::sat");
 
-      Debug("pf::sat") << "TheoryProxy::explainPropagation: setting explainer theory to: "
-                        << explainerTheory << std::endl;
+      delete proofRecipe;
+      proofRecipe = NULL;
     });
 
-  Debug("prop-explain") << "explainPropagation() => " << explanationNode << std::endl;
-  if (explanationNode.getKind() == kind::AND) {
-    Node::const_iterator it = explanationNode.begin();
-    Node::const_iterator it_end = explanationNode.end();
+  Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl;
+  if (theoryExplanation.getKind() == kind::AND) {
+    Node::const_iterator it = theoryExplanation.begin();
+    Node::const_iterator it_end = theoryExplanation.end();
     explanation.push_back(l);
     for (; it != it_end; ++ it) {
       explanation.push_back(~d_cnfStream->getLiteral(*it));
     }
   } else {
     explanation.push_back(l);
-    explanation.push_back(~d_cnfStream->getLiteral(explanationNode));
+    explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
   }
 }
 
@@ -175,7 +180,9 @@ void TheoryProxy::notifyRestart() {
           if(lemmaCount % 1 == 0) {
             Debug("shared") << "=) " << asNode << std::endl;
           }
-          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, theory::THEORY_LAST);
+
+          LemmaProofRecipe* noProofRecipe = NULL;
+          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, noProofRecipe);
         } else {
           Debug("shared") << "=(" << asNode << std::endl;
         }