From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 22 Feb 2014 10:34:31 +0000 (+0100)
Subject: Added ezMiniSat EZMINISAT_INCREMENTAL compile-time option
X-Git-Tag: yosys-0.3.0~113
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=357f3f6e93df1ebf2aa28a6c433a84f320fad043;p=yosys.git

Added ezMiniSat EZMINISAT_INCREMENTAL compile-time option
---

diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index 4d3301c4d..a1cb80520 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 04a010d68..59fa21348 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>