From 5c8601e638fcbfcd29eceeea4f83a0c1ca578316 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 22 May 2020 14:09:54 -0700
Subject: [PATCH] CaDiCaL: Clean up initialization on creation. (#4516)

---
 src/prop/cadical.cpp            |  4 ++++
 src/prop/cadical.h              | 15 +++++++++++++--
 src/prop/sat_solver_factory.cpp |  4 +++-
 3 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index f824f5075..48116912b 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -63,6 +63,10 @@ CadicalSolver::CadicalSolver(StatisticsRegistry* registry,
       //       literals are represented as the negation of the index.
       d_nextVarIdx(1),
       d_statistics(registry, name)
+{
+}
+
+void CadicalSolver::init()
 {
   d_true = newVar();
   d_false = newVar();
diff --git a/src/prop/cadical.h b/src/prop/cadical.h
index 6ab0c2850..1adbfc2d1 100644
--- a/src/prop/cadical.h
+++ b/src/prop/cadical.h
@@ -30,9 +30,9 @@ namespace prop {
 
 class CadicalSolver : public SatSolver
 {
- public:
-  CadicalSolver(StatisticsRegistry* registry, const std::string& name = "");
+  friend class SatSolverFactory;
 
+ public:
   ~CadicalSolver() override;
 
   ClauseId addClause(SatClause& clause, bool removable) override;
@@ -62,6 +62,17 @@ class CadicalSolver : public SatSolver
   bool ok() const override;
 
  private:
+  /**
+   * Private to disallow creation outside of SatSolverFactory.
+   * Function init() must be called after creation.
+   */
+  CadicalSolver(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<CaDiCaL::Solver> d_solver;
 
   unsigned d_nextVarIdx;
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 598ba4543..4a8d616ba 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -55,7 +55,9 @@ SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry,
                                            const std::string& name)
 {
 #ifdef CVC4_USE_CADICAL
-  return new CadicalSolver(registry, name);
+  CadicalSolver* res = new CadicalSolver(registry, name);
+  res->init();
+  return res;
 #else
   Unreachable() << "CVC4 was not compiled with CaDiCaL support.";
 #endif
-- 
2.30.2