Added ezSAT::eliminated API to help the SAT solver remember eliminated variables

diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index 287177b1c6669244206bf6ac489c62805ce60f62..d488a90623d6f21d5cee307c7c75553180ac9d2e 100644 (file)
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -65,6 +65,14 @@ void ezMiniSAT::freeze(int id)
 {
        cnfFrozenVars.insert(bind(id));
 }
+
+bool ezMiniSAT::eliminated(int idx)
+{
+       idx = idx < 0 ? -idx : idx;
+       if (minisatSolver != NULL && idx > 0 && idx <= int(minisatVars.size()))
+               return minisatSolver->isEliminated(minisatVars.at(idx-1));
+       return false;
+}
 #endif
 
 ezMiniSAT *ezMiniSAT::alarmHandlerThis = NULL;

diff --git a/libs/ezsat/ezminisat.h b/libs/ezsat/ezminisat.h
index e7e0828918b052a5906c5a3d68be3deb5769deda..c634e66e73be144ee590d0a20879df08f64df2cb 100644 (file)
--- a/libs/ezsat/ezminisat.h
+++ b/libs/ezsat/ezminisat.h
@@ -61,6 +61,7 @@ public:
        virtual void clear();
 #if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
        virtual void freeze(int id);
+       virtual bool eliminated(int idx);
 #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 cc6301e441314a0276d6fb7954121d4399944c29..4389c7a62293cc7b9765d818121c2828ab462d14 100644 (file)
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -348,9 +348,13 @@ void ezSAT::freeze(int)
 {
 }
 
-void ezSAT::assume(int id)
+bool ezSAT::eliminated(int)
 {
+       return false;
+}
 
+void ezSAT::assume(int id)
+{
        if (id < 0)
        {
                assert(0 < -id && -id <= int(expressions.size()));
@@ -486,7 +490,7 @@ int ezSAT::bind(int id)
        if (id >= 0) {
                assert(0 < id && id <= int(literals.size()));
                cnfLiteralVariables.resize(literals.size());
-               if (cnfLiteralVariables[id-1] == 0) {
+               if (cnfLiteralVariables[id-1] == 0 || eliminated(cnfLiteralVariables[id-1])) {
                        cnfLiteralVariables[id-1] = ++cnfVariableCount;
                        if (id == TRUE)
                                add_clause(+cnfLiteralVariables[id-1]);
@@ -499,7 +503,7 @@ int ezSAT::bind(int id)
        assert(0 < -id && -id <= int(expressions.size()));
        cnfExpressionVariables.resize(expressions.size());
 
-       if (cnfExpressionVariables[-id-1] == 0)
+       if (cnfExpressionVariables[-id-1] == 0 || eliminated(cnfExpressionVariables[-id-1]))
        {
                OpId op;
                std::vector<int> args;

diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 8d340b3d6bd98531b1be349aad6d918eeb4abad6..16f940a1d98d403ced6852cf0483e9f85479a3b6 100644 (file)
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -141,6 +141,7 @@ public:
 
        virtual void clear();
        virtual void freeze(int id);
+       virtual bool eliminated(int idx);
        void assume(int id);
        int bind(int id);
        int bound(int id) const;