Added ezMiniSat EZMINISAT_INCREMENTAL compile-time option

diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index 4d3301c4d51168b18448eb7ab92d315db16eb653..a1cb805207c908e89b21378b901d7e40b245917f 100644 (file)
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -96,8 +96,12 @@ contradiction:
                minisatSolver->verbosity = EZMINISAT_VERBOSITY;
        }
 
+#if EZMINISAT_INCREMENTAL
        std::vector<std::vector<int>> cnf;
        consumeCnf(cnf);
+#else
+       const std::vector<std::vector<int>> &cnf = this->cnf();
+#endif
 
        while (int(minisatVars.size()) < numCnfVariables())
                minisatVars.push_back(minisatSolver->newVar());
@@ -145,8 +149,14 @@ contradiction:
                alarm(old_alarm_timeout);
        }
 
-       if (!foundSolution)
+       if (!foundSolution) {
+#if !EZMINISAT_INCREMENTAL
+               delete minisatSolver;
+               minisatSolver = NULL;
+               minisatVars.clear();
+#endif
                return false;
+       }
 
        modelValues.clear();
        modelValues.resize(modelIdx.size());
@@ -164,6 +174,11 @@ contradiction:
                modelValues[i] = (value == Minisat::lbool(refvalue));
        }
 
+#if !EZMINISAT_INCREMENTAL
+       delete minisatSolver;
+       minisatSolver = NULL;
+       minisatVars.clear();
+#endif
        return true;
 }
 

diff --git a/libs/ezsat/ezminisat.h b/libs/ezsat/ezminisat.h
index 04a010d68eb2eed729edb55bb8eb99eee7e8c5a2..59fa21348231d3f95939ad1517c50fac25c84747 100644 (file)
--- a/libs/ezsat/ezminisat.h
+++ b/libs/ezsat/ezminisat.h
@@ -22,6 +22,7 @@
 
 #define EZMINISAT_SOLVER Minisat::Solver
 #define EZMINISAT_VERBOSITY 0
+#define EZMINISAT_INCREMENTAL 1
 
 #include "ezsat.h"
 #include <time.h>