luke
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Add solve without model.

This commit is contained in:
nella 2026-08-17 12:19:07 +02:00
parent dbe5b7c03f
commit cd029c0638
2 changed files with 11 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
kernel/qcsat.cc
View File

@ -108,9 +108,17 @@ void SatEffortBudget::charge_import(QuickConeSat &qcsat, int64_t &cells_charged)
cells_charged = GetSize(qcsat.imported_cells);
}
SatEffortBudget::Result SatEffortBudget::solve(QuickConeSat &qcsat, int64_t cap, const std::vector<int> &assumptions)
{
std::vector<bool> modelVals;
return solve(qcsat, cap, {}, modelVals, assumptions);
}
SatEffortBudget::Result SatEffortBudget::solve(QuickConeSat &qcsat, int64_t cap, const std::vector<int> &modelExprs,
std::vector<bool> &modelVals, const std::vector<int> &assumptions)
{
if (spent())
return Result::LimitReached;
if (enabled())
cap = (cap > 0) ? std::min(cap, remaining) : remaining;
qcsat.ez->setSolverPropLimit(cap);

3
kernel/qcsat.h
View File

@ -102,6 +102,9 @@ struct SatEffortBudget {
Result solve(QuickConeSat &qcsat, int64_t cap, const std::vector<int> &modelExprs,
std::vector<bool> &modelVals, const std::vector<int> &assumptions);
// Assumptions-only query without a model
Result solve(QuickConeSat &qcsat, int64_t cap, const std::vector<int> &assumptions);
};
YOSYS_NAMESPACE_END