From: Clifford Wolf Date: Sun, 23 Feb 2014 00:35:59 +0000 (+0100) Subject: Added support for Minisat::SimpSolver + ezSAT frezze() API X-Git-Tag: yosys-0.3.0~108 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dab1612f81212d1bc1c07ee77b265167861ec883;p=yosys.git Added support for Minisat::SimpSolver + ezSAT frezze() API --- diff --git a/kernel/satgen.h b/kernel/satgen.h index 840700cbd..539210442 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 a1cb80520..c6126d862 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 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 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 59fa21348..e7e082891 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 minisatVars; bool foundContradiction; +#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL + std::set 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 &modelExpressions, std::vector &modelValues, const std::vector &assumptions); }; diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 577625259..e6c005c69 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 ""; +} + int ezSAT::bind(int id) { if (id >= 0) { diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h index 547edb93b..79100b876 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> &cnf); + std::string cnfLiteralInfo(int idx) const; + // simple helpers for build expressions easily struct _V {