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

diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index f824f50751883b610e2f5cebc8c4920d22d63fcc..48116912b804c3657355d640da9bd24d87b40ea4 100644 (file)
--- 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 6ab0c2850012f00c8b03c08f8d08a3bcd1dc3ab7..1adbfc2d1713c4658297e658530e955a39093461 100644 (file)
--- 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 598ba454386330a45d98dff4733edf7c4d635867..4a8d616ba338c5b4da928a29bdf324ac43a5503b 100644 (file)
--- 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