summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-02-22 11:34:31 +0100
committerClifford Wolf <clifford@clifford.at>2014-02-22 11:34:31 +0100
commit357f3f6e93df1ebf2aa28a6c433a84f320fad043 (patch)
tree3d3fef1cdccc23fffb209c12a44b42d8a269f64c
parent1ec01d8c637e611eddd16a492d1eb0f652b95da0 (diff)
Added ezMiniSat EZMINISAT_INCREMENTAL compile-time option
-rw-r--r--libs/ezsat/ezminisat.cc17
-rw-r--r--libs/ezsat/ezminisat.h1
2 files changed, 17 insertions, 1 deletions
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index 4d3301c4..a1cb8052 100644
--- 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 04a010d6..59fa2134 100644
--- 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>