summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-03-01 21:00:34 +0100
committerClifford Wolf <clifford@clifford.at>2014-03-01 21:00:34 +0100
commitd500bd749f84c0b05a8ec96d2a5fc33ace0c5b58 (patch)
tree90f2dc8cf7195a71ab48c4fea0b9ce1e6e105f71
parent23f0a12c727721478bcb87ec142fb86a329f7cdb (diff)
Added ezSAT::eliminated API to help the SAT solver remember eliminated variables
-rw-r--r--libs/ezsat/ezminisat.cc8
-rw-r--r--libs/ezsat/ezminisat.h1
-rw-r--r--libs/ezsat/ezsat.cc10
-rw-r--r--libs/ezsat/ezsat.h1
4 files changed, 17 insertions, 3 deletions
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index 287177b1..d488a906 100644
--- 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 e7e08289..c634e66e 100644
--- 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 cc6301e4..4389c7a6 100644
--- 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 8d340b3d..16f940a1 100644
--- 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;