summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/satgen.h1
-rw-r--r--libs/ezsat/ezminisat.cc37
-rw-r--r--libs/ezsat/ezminisat.h16
-rw-r--r--libs/ezsat/ezsat.cc33
-rw-r--r--libs/ezsat/ezsat.h3
5 files changed, 79 insertions, 11 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h
index 840700cb..53921044 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -72,6 +72,7 @@ struct SatGen
} else {
std::string name = pf + stringf(c.wire->width == 1 ? "%s" : "%s [%d]", RTLIL::id2cstr(c.wire->name), c.offset);
vec.push_back(ez->literal(name));
+ ez->freeze(vec.back());
}
return vec;
}
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index a1cb8052..c6126d86 100644
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -51,9 +51,19 @@ void ezMiniSAT::clear()
}
foundContradiction = false;
minisatVars.clear();
+#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
+ cnfFrozenVars.clear();
+#endif
ezSAT::clear();
}
+#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
+void ezMiniSAT::freeze(int id)
+{
+ cnfFrozenVars.insert(bind(id));
+}
+#endif
+
ezMiniSAT *ezMiniSAT::alarmHandlerThis = NULL;
clock_t ezMiniSAT::alarmHandlerTimeout = 0;
@@ -92,7 +102,7 @@ contradiction:
modelIdx.push_back(bind(id));
if (minisatSolver == NULL) {
- minisatSolver = new EZMINISAT_SOLVER;
+ minisatSolver = new Solver;
minisatSolver->verbosity = EZMINISAT_VERBOSITY;
}
@@ -106,13 +116,27 @@ contradiction:
while (int(minisatVars.size()) < numCnfVariables())
minisatVars.push_back(minisatSolver->newVar());
+#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
+ for (auto idx : cnfFrozenVars)
+ minisatSolver->setFrozen(minisatVars.at(idx > 0 ? idx-1 : -idx-1), true);
+ cnfFrozenVars.clear();
+#endif
+
for (auto &clause : cnf) {
Minisat::vec<Minisat::Lit> ps;
- for (auto idx : clause)
+ for (auto idx : clause) {
if (idx > 0)
ps.push(Minisat::mkLit(minisatVars.at(idx-1)));
else
ps.push(Minisat::mkLit(minisatVars.at(-idx-1), true));
+#if EZMINISAT_SIMPSOLVER
+ if (minisatSolver->isEliminated(minisatVars.at(idx > 0 ? idx-1 : -idx-1))) {
+ fprintf(stderr, "Assert in %s:%d failed! Missing call to ezsat->freeze(): %s (lit=%d)\n",
+ __FILE__, __LINE__, cnfLiteralInfo(idx).c_str(), idx);
+ abort();
+ }
+#endif
+ }
if (!minisatSolver->addClause(ps))
goto contradiction;
}
@@ -122,11 +146,18 @@ contradiction:
Minisat::vec<Minisat::Lit> assumps;
- for (auto idx : extraClauses)
+ for (auto idx : extraClauses) {
if (idx > 0)
assumps.push(Minisat::mkLit(minisatVars.at(idx-1)));
else
assumps.push(Minisat::mkLit(minisatVars.at(-idx-1), true));
+#if EZMINISAT_SIMPSOLVER
+ if (minisatSolver->isEliminated(minisatVars.at(idx > 0 ? idx-1 : -idx-1))) {
+ fprintf(stderr, "Assert in %s:%d failed! Missing call to ezsat->freeze(): %s\n", __FILE__, __LINE__, cnfLiteralInfo(idx).c_str());
+ abort();
+ }
+#endif
+ }
sighandler_t old_alarm_sighandler = NULL;
int old_alarm_timeout = 0;
diff --git a/libs/ezsat/ezminisat.h b/libs/ezsat/ezminisat.h
index 59fa2134..e7e08289 100644
--- a/libs/ezsat/ezminisat.h
+++ b/libs/ezsat/ezminisat.h
@@ -20,7 +20,7 @@
#ifndef EZMINISAT_H
#define EZMINISAT_H
-#define EZMINISAT_SOLVER Minisat::Solver
+#define EZMINISAT_SIMPSOLVER 0
#define EZMINISAT_VERBOSITY 0
#define EZMINISAT_INCREMENTAL 1
@@ -38,10 +38,19 @@ namespace Minisat {
class ezMiniSAT : public ezSAT
{
private:
- EZMINISAT_SOLVER *minisatSolver;
+#if EZMINISAT_SIMPSOLVER
+ typedef Minisat::SimpSolver Solver;
+#else
+ typedef Minisat::Solver Solver;
+#endif
+ Solver *minisatSolver;
std::vector<int> minisatVars;
bool foundContradiction;
+#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
+ std::set<int> cnfFrozenVars;
+#endif
+
static ezMiniSAT *alarmHandlerThis;
static clock_t alarmHandlerTimeout;
static void alarmHandler(int);
@@ -50,6 +59,9 @@ public:
ezMiniSAT();
virtual ~ezMiniSAT();
virtual void clear();
+#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
+ virtual void freeze(int id);
+#endif
virtual bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions);
};
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index 57762525..e6c005c6 100644
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -29,18 +29,18 @@ const int ezSAT::FALSE = 2;
ezSAT::ezSAT()
{
- literal("TRUE");
- literal("FALSE");
-
- assert(literal("TRUE") == TRUE);
- assert(literal("FALSE") == FALSE);
-
cnfConsumed = false;
cnfVariableCount = 0;
cnfClausesCount = 0;
solverTimeout = 0;
solverTimoutStatus = false;
+
+ freeze(literal("TRUE"));
+ freeze(literal("FALSE"));
+
+ assert(literal("TRUE") == TRUE);
+ assert(literal("FALSE") == FALSE);
}
ezSAT::~ezSAT()
@@ -345,6 +345,10 @@ void ezSAT::clear()
cnfAssumptions.clear();
}
+void ezSAT::freeze(int)
+{
+}
+
void ezSAT::assume(int id)
{
cnfAssumptions.insert(id);
@@ -462,6 +466,23 @@ int ezSAT::bound(int id) const
return 0;
}
+std::string ezSAT::cnfLiteralInfo(int idx) const
+{
+ for (size_t i = 0; i < cnfLiteralVariables.size(); i++) {
+ if (cnfLiteralVariables[i] == idx)
+ return to_string(i+1);
+ if (cnfLiteralVariables[i] == -idx)
+ return "NOT " + to_string(i+1);
+ }
+ for (size_t i = 0; i < cnfExpressionVariables.size(); i++) {
+ if (cnfExpressionVariables[i] == idx)
+ return to_string(-i-1);
+ if (cnfExpressionVariables[i] == -idx)
+ return "NOT " + to_string(-i-1);
+ }
+ return "<unnamed>";
+}
+
int ezSAT::bind(int id)
{
if (id >= 0) {
diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 547edb93..79100b87 100644
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -141,6 +141,7 @@ public:
// manage CNF (usually only accessed by SAT solvers)
virtual void clear();
+ virtual void freeze(int id);
void assume(int id);
int bind(int id);
@@ -154,6 +155,8 @@ public:
void consumeCnf();
void consumeCnf(std::vector<std::vector<int>> &cnf);
+ std::string cnfLiteralInfo(int idx) const;
+
// simple helpers for build expressions easily
struct _V {
generated by cgit v1.2.3 (git 2.25.1) at 2024-04-25 00:18:13 +0000