Added support for Minisat::SimpSolver + ezSAT frezze() API

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 840700cbd9c9a3835cd1401b9e528f1c9031cb65..539210442f01b406d34b6ca75e61fa0fe4d47ee1 100644 (file)
--- 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 a1cb805207c908e89b21378b901d7e40b245917f..c6126d862e14bbc851b3dd28c78d2221d1462707 100644 (file)
--- 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 59fa21348231d3f95939ad1517c50fac25c84747..e7e0828918b052a5906c5a3d68be3deb5769deda 100644 (file)
--- 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 577625259f3049fd27fc16c00db1a6c5f3ad82a9..e6c005c69efae1197e7dfc145542f016767351f0 100644 (file)
--- 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 547edb93bcc2d1262e784d3a2ae83c78835c84e9..79100b876df0b8b8df34a6094c6ae039250fd73e 100644 (file)
--- 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 {