mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-03 21:09:12 +00:00
Code Activity

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

Browse source
This commit is contained in:
Clifford Wolf 2014-03-01 21:00:34 +01:00
parent 23f0a12c72
commit d500bd749f
4 changed files with 17 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
libs/ezsat/ezminisat.cc
View file

@ -65,6 +65,14 @@ void ezMiniSAT::freeze(int id)
{ {
cnfFrozenVars.insert(bind(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 #endif
ezMiniSAT *ezMiniSAT::alarmHandlerThis = NULL; ezMiniSAT *ezMiniSAT::alarmHandlerThis = NULL;

1
libs/ezsat/ezminisat.h
View file

@ -61,6 +61,7 @@ public:
virtual void clear(); virtual void clear();
#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL #if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
virtual void freeze(int id); virtual void freeze(int id);
virtual bool eliminated(int idx);
#endif #endif
virtual bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions); virtual bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions);
}; };

10
libs/ezsat/ezsat.cc
View file

@ -348,9 +348,13 @@ void ezSAT::freeze(int)
{ {
} }
bool ezSAT::eliminated(int)
{
return false;
}
void ezSAT::assume(int id) void ezSAT::assume(int id)
{ {
if (id < 0) if (id < 0)
{ {
assert(0 < -id && -id <= int(expressions.size())); assert(0 < -id && -id <= int(expressions.size()));
@ -486,7 +490,7 @@ int ezSAT::bind(int id)
if (id >= 0) { if (id >= 0) {
assert(0 < id && id <= int(literals.size())); assert(0 < id && id <= int(literals.size()));
cnfLiteralVariables.resize(literals.size()); cnfLiteralVariables.resize(literals.size());
if (cnfLiteralVariables[id-1] == 0) { if (cnfLiteralVariables[id-1] == 0 || eliminated(cnfLiteralVariables[id-1])) {
cnfLiteralVariables[id-1] = ++cnfVariableCount; cnfLiteralVariables[id-1] = ++cnfVariableCount;
if (id == TRUE) if (id == TRUE)
add_clause(+cnfLiteralVariables[id-1]); add_clause(+cnfLiteralVariables[id-1]);
@ -499,7 +503,7 @@ int ezSAT::bind(int id)
assert(0 < -id && -id <= int(expressions.size())); assert(0 < -id && -id <= int(expressions.size()));
cnfExpressionVariables.resize(expressions.size()); cnfExpressionVariables.resize(expressions.size());
if (cnfExpressionVariables[-id-1] == 0) if (cnfExpressionVariables[-id-1] == 0 || eliminated(cnfExpressionVariables[-id-1]))
{ {
OpId op; OpId op;
std::vector<int> args; std::vector<int> args;

1
libs/ezsat/ezsat.h
View file

@ -141,6 +141,7 @@ public:
virtual void clear(); virtual void clear();
virtual void freeze(int id); virtual void freeze(int id);
virtual bool eliminated(int idx);
void assume(int id); void assume(int id);
int bind(int id); int bind(int id);
int bound(int id) const; int bound(int id) const;