summaryrefslogtreecommitdiff
path: root/libs/ezsat/ezminisat.cc
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 /libs/ezsat/ezminisat.cc
parent23f0a12c727721478bcb87ec142fb86a329f7cdb (diff)
Added ezSAT::eliminated API to help the SAT solver remember eliminated variables
Diffstat (limited to 'libs/ezsat/ezminisat.cc')
-rw-r--r--libs/ezsat/ezminisat.cc8
1 files changed, 8 insertions, 0 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;