From 46501b092b2d9419273d42f28a7a543ae9b2e338 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 22 May 2020 09:47:55 -0700
Subject: [PATCH] Cryptominisat: Clean up initialization on creation. (#4515)

---
 src/prop/cryptominisat.cpp      |  7 +++--
 src/prop/cryptominisat.h        | 49 +++++++++++++++++++++------------
 src/prop/sat_solver_factory.cpp |  4 ++-
 3 files changed, 40 insertions(+), 20 deletions(-)

diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index 9893f1d6c..6ad67de04 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -68,6 +68,10 @@ CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
       d_numVariables(0),
       d_okay(true),
       d_statistics(registry, name)
+{
+}
+
+void CryptoMinisatSolver::init()
 {
   d_true = newVar();
   d_false = newVar();
@@ -75,12 +79,11 @@ CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
   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() {}
 
 ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause,
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index d3c5aeb30..25d6cce02 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -36,18 +36,11 @@ namespace CMSat {
 namespace CVC4 {
 namespace prop {
 
-class CryptoMinisatSolver : public SatSolver {
+class CryptoMinisatSolver : public SatSolver
+{
+  friend class SatSolverFactory;
 
-private:
-  std::unique_ptr<CMSat::SATSolver> d_solver;
-  proof::ClausalBitVectorProof* d_bvp;
-  unsigned d_numVariables;
-  bool d_okay;
-  SatVariable d_true;
-  SatVariable d_false;
-public:
-  CryptoMinisatSolver(StatisticsRegistry* registry,
-                      const std::string& name = "");
+ public:
   ~CryptoMinisatSolver() override;
 
   ClauseId addClause(SatClause& clause, bool removable) override;
@@ -55,7 +48,9 @@ public:
 
   bool nativeXor() override { return true; }
 
-  SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true) override;
+  SatVariable newVar(bool isTheoryAtom = false,
+                     bool preRegister = false,
+                     bool canErase = true) override;
 
   SatVariable trueVar() override;
   SatVariable falseVar() override;
@@ -63,7 +58,7 @@ public:
   void markUnremovable(SatLiteral lit);
 
   void interrupt() override;
-  
+
   SatValue solve() override;
   SatValue solve(long unsigned int&) override;
   SatValue solve(const std::vector<SatLiteral>& assumptions) override;
@@ -75,19 +70,39 @@ public:
   unsigned getAssertionLevel() const override;
   void setClausalProofLog(proof::ClausalBitVectorProof* bvp) override;
 
-  class Statistics {
-  public:
+ private:
+  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(StatisticsRegistry* registry, const std::string& prefix);
     ~Statistics();
   };
 
+  /**
+   * Private to disallow creation outside of SatSolverFactory.
+   * Function init() must be called after creation.
+   */
+  CryptoMinisatSolver(StatisticsRegistry* registry,
+                      const std::string& name = "");
+  /**
+   * Initialize SAT solver instance.
+   * Note: Split out to not call virtual functions in constructor.
+   */
+  void init();
+
+  std::unique_ptr<CMSat::SATSolver> d_solver;
+  proof::ClausalBitVectorProof* d_bvp;
+  unsigned d_numVariables;
+  bool d_okay;
+  SatVariable d_true;
+  SatVariable d_false;
+
   Statistics d_statistics;
 };
 
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 8f18a6055..598ba4543 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -43,7 +43,9 @@ SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry,
                                                  const std::string& name)
 {
 #ifdef CVC4_USE_CRYPTOMINISAT
-  return new CryptoMinisatSolver(registry, name);
+  CryptoMinisatSolver* res = new CryptoMinisatSolver(registry, name);
+  res->init();
+  return res;
 #else
   Unreachable() << "CVC4 was not compiled with Cryptominisat support.";
 #endif
-- 
2.30.2