mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 19:52:31 +00:00
Code Activity

Added ezSAT api support for don't care values in models

Browse source
This commit is contained in:
Clifford Wolf 2013-06-09 14:21:18 +02:00
parent b7ba90910d
commit 41932e8b64
3 changed files with 23 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

21
libs/ezsat/ezminisat.cc
View file

@ -108,14 +108,25 @@ contradiction:
return false; return false;
modelValues.clear(); modelValues.clear();
modelValues.reserve(modelIdx.size()); modelValues.resize(2 * modelIdx.size());
for (auto idx : modelIdx) {
for (size_t i = 0; i < modelIdx.size(); i++)
{
int idx = modelIdx[i];
bool refvalue = true; bool refvalue = true;
if (idx < 0) if (idx < 0)
idx = -idx, refvalue = false; idx = -idx, refvalue = false;
auto value = minisatSolver->modelValue(minisatVars.at(idx-1));
// FIXME: Undef values using namespace Minisat;
modelValues.push_back(value == Minisat::lbool(refvalue)); lbool value = minisatSolver->modelValue(minisatVars.at(idx-1));
if (value == l_Undef) {
modelValues[i] = false;
modelValues[modelIdx.size() + i] = true;
} else {
modelValues[i] = value == Minisat::lbool(refvalue);
modelValues[modelIdx.size() + i] = false;
}
} }
return true; return true;

3
libs/ezsat/ezsat.h
View file

@ -98,6 +98,9 @@ public:
// If you are planning on using the solver API (and not simply create a CNF) you must use a child class // If you are planning on using the solver API (and not simply create a CNF) you must use a child class
// of ezSAT that actually implements a solver backend, such as ezMiniSAT (see ezminisat.h). // of ezSAT that actually implements a solver backend, such as ezMiniSAT (see ezminisat.h).
// Note: Solvers that can output don't-care values for model variables return a twice as big modelValues
// vector. The first half contains the values and the second half the don't-care flags.
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);
bool solve(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions) { bool solve(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions) {

5
passes/sat/sat_solve.cc
View file

@ -419,8 +419,11 @@ rerun_solver:
for (auto &info : modelInfo) for (auto &info : modelInfo)
{ {
RTLIL::Const value; RTLIL::Const value;
for (int i = 0; i < info.width; i++) for (int i = 0; i < info.width; i++) {
value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0); value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
if (modelValues.size() == 2*modelExpressions.size() && modelValues.at(modelExpressions.size()+info.offset+i))
value.bits.back() = RTLIL::State::Sx;
}
if (info.timestep != last_timestep) { if (info.timestep != last_timestep) {
const char *hline = "---------------------------------------------------------------------------------------------------" const char *hline = "---------------------------------------------------------------------------------------------------"