mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-10 01:41:59 +00:00
Code Activity

Merge ccf04533e6 into 637665c9d3

Browse source
This commit is contained in:
Gabriel Gouvine 2025-10-06 13:38:06 +02:00 • committed by GitHub
commit 16edf64ecb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 132 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
libs/ezsat/ezsat.cc
View file

@ -1222,7 +1222,7 @@ ezSATvec ezSAT::vec(const std::vector<int> &vec)
return ezSATvec(*this, vec);
}
void ezSAT::printDIMACS(FILE *f, bool verbose) const
void ezSAT::printDIMACS(FILE *f, bool verbose, const std::vector<std::vector<int>> &extraClauses) const
{
if (cnfConsumed) {
fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!");
@ -1259,8 +1259,10 @@ void ezSAT::printDIMACS(FILE *f, bool verbose) const
std::vector<std::vector<int>> all_clauses;
getFullCnf(all_clauses);
assert(cnfClausesCount == int(all_clauses.size()));
for (auto c : extraClauses)
all_clauses.push_back(c);
fprintf(f, "p cnf %d %d\n", cnfVariableCount, cnfClausesCount);
fprintf(f, "p cnf %d %d\n", cnfVariableCount, (int) all_clauses.size());
int maxClauseLen = 0;
for (auto &clause : all_clauses)
maxClauseLen = std::max(int(clause.size()), maxClauseLen);