Fixes

lib/dpelim.cpp

@@ -377,7 +377,10 @@ SUBool::DPEliminator::AddClauses(std::vector<Clause> resolvents)
          continue;
       }
       cnf.PushBack(clause);
-      op.AddClause(cnf.Size() - 1);
+      if (mIgnorePolicy != IGNORE_POLICY::NONE)
+      {
+         op.AddClause(cnf.Size() - 1);
+      }
       ++mTotalNewClauses;
       ++mCurrentNewClauses;
       mClauseInfo.emplace_back(std::move(clause), false);

lib/unitprop.cpp

@@ -52,6 +52,11 @@ SUBool::UnitPropagator::AddClauseInner(size_t clause_index)
 void
 SUBool::UnitPropagator::RemoveClause(size_t clause_index)
 {
+   if (mCnf == nullptr)
+   {
+      throw NullPointerException(
+          "UnitPropagator::AddClause", "mCNF is nullptr");
+   }
    const auto &clause = (*mCnf)[clause_index];
    auto &w = mWatchLiterals[clause_index];
    switch (clause.Size())
@@ -75,6 +80,11 @@ SUBool::UnitPropagator::RemoveClause(size_t clause_index)
 void
 SUBool::UnitPropagator::AddClause(size_t clause_index)
 {
+   if (mCnf == nullptr)
+   {
+      throw NullPointerException(
+          "UnitPropagator::AddClause", "mCNF is nullptr");
+   }
    if (clause_index >= mWatchLiterals.size())
    {
       mWatchLiterals.resize(clause_index + 1);
@@ -88,8 +98,7 @@ SUBool::UnitPropagator::AddClause(size_t clause_index)
 
 void
 SUBool::UnitPropagator::UpdateWatch(const Literal &lit,
-                                    std::list<size_t>::iterator &it,
-                                    const PartialAssignment &beta) const
+    std::list<size_t>::iterator &it, const PartialAssignment &beta) const
 {
    int i = *it;
    auto &w1 = mWatchLiterals[i].first;
@@ -155,8 +164,7 @@ SUBool::UnitPropagator::ClauseStatus(int i, const PartialAssignment &beta) const
 
 int
 SUBool::UnitPropagator::UpdateWatches(const Literal &lit,
-                                      std::queue<Literal> &lq,
-                                      const PartialAssignment &beta) const
+    std::queue<Literal> &lq, const PartialAssignment &beta) const
 {
    Literal neg(lit);
    neg.Negate();
@@ -182,9 +190,8 @@ SUBool::UnitPropagator::UpdateWatches(const Literal &lit,
 }
 
 int
-SUBool::UnitPropagator::AddLiteralValue(const Literal &lit,
-                                        std::queue<Literal> &lq,
-                                        PartialAssignment &beta) const
+SUBool::UnitPropagator::AddLiteralValue(
+    const Literal &lit, std::queue<Literal> &lq, PartialAssignment &beta) const
 {
    switch (lit.Value(beta))
    {
@@ -203,8 +210,8 @@ SUBool::UnitPropagator::AddLiteralValue(const Literal &lit,
 }
 
 void
-SUBool::UnitPropagator::PropInit(const PartialAssignment &assump,
-                                 std::queue<Literal> &lq) const
+SUBool::UnitPropagator::PropInit(
+    const PartialAssignment &assump, std::queue<Literal> &lq) const
 {
    for (auto i : mUnitClauses)
    {
@@ -220,8 +227,8 @@ SUBool::UnitPropagator::PropInit(const PartialAssignment &assump,
 }
 
 int
-SUBool::UnitPropagator::Propagate(const PartialAssignment &assump,
-                                  PartialAssignment *conseq) const
+SUBool::UnitPropagator::Propagate(
+    const PartialAssignment &assump, PartialAssignment *conseq) const
 {
    if (!mEmptyClauses.empty())
    {

test/test_glucose.cpp

@@ -11,6 +11,7 @@
 
 #include "cnfutil.h"
 #include "dimacs.h"
+#include "glucose_bind.h"
 #include "random_utils.h"
 #include "solver_bind.h"
 #include "test_glucose.h"