CaDiCaL: Clean up initialization on creation. (#4516)

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
@@ -64,6 +64,10 @@ CadicalSolver::CadicalSolver(StatisticsRegistry* registry,
       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