diff options
| author | Clifford Wolf <clifford@clifford.at> | 2014-03-01 21:00:34 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2014-03-01 21:00:34 +0100 |
| commit | d500bd749f84c0b05a8ec96d2a5fc33ace0c5b58 (patch) | |
| tree | 90f2dc8cf7195a71ab48c4fea0b9ce1e6e105f71 /libs/ezsat | |
| parent | 23f0a12c727721478bcb87ec142fb86a329f7cdb (diff) | |
| download | yosys-d500bd749f84c0b05a8ec96d2a5fc33ace0c5b58.tar.gz yosys-d500bd749f84c0b05a8ec96d2a5fc33ace0c5b58.tar.bz2 yosys-d500bd749f84c0b05a8ec96d2a5fc33ace0c5b58.zip | |
Added ezSAT::eliminated API to help the SAT solver remember eliminated variables
Diffstat (limited to 'libs/ezsat')
| -rw-r--r-- | libs/ezsat/ezminisat.cc | 8 | ||||
| -rw-r--r-- | libs/ezsat/ezminisat.h | 1 | ||||
| -rw-r--r-- | libs/ezsat/ezsat.cc | 10 | ||||
| -rw-r--r-- | libs/ezsat/ezsat.h | 1 |
4 files changed, 17 insertions, 3 deletions
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc index 287177b1c..d488a9062 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 e7e082891..c634e66e7 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 cc6301e44..4389c7a62 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 8d340b3d6..16f940a1d 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; |