mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-23 15:42:32 +00:00
Code Activity

Merge from main

Browse source
This commit is contained in:
Akash Levy 2026-02-13 04:14:08 -08:00
commit 2b247d165b
30 changed files with 722 additions and 125 deletions
Download patch file Download diff file Expand all files Collapse all files

92
libs/ezsat/ezcmdline.cc Normal file
View file

@ -0,0 +1,92 @@
#include "ezcmdline.h"
#include "../../kernel/yosys.h"
ezCmdlineSAT::ezCmdlineSAT(const std::string &cmd) : command(cmd) {}
ezCmdlineSAT::~ezCmdlineSAT() {}
bool ezCmdlineSAT::solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions)
{
#if !defined(YOSYS_DISABLE_SPAWN)
const std::string tempdir_name = Yosys::make_temp_dir(Yosys::get_base_tmpdir() + "/yosys-sat-XXXXXX");
const std::string cnf_filename = Yosys::stringf("%s/problem.cnf", tempdir_name.c_str());
const std::string sat_command = Yosys::stringf("%s %s", command.c_str(), cnf_filename.c_str());
FILE *dimacs = fopen(cnf_filename.c_str(), "w");
if (dimacs == nullptr) {
Yosys::log_cmd_error("Failed to create CNF file `%s`.\n", cnf_filename.c_str());
}
std::vector<int> modelIdx;
for (auto id : modelExpressions)
modelIdx.push_back(bind(id));
std::vector<std::vector<int>> extraClauses;
for (auto id : assumptions)
extraClauses.push_back({bind(id)});
printDIMACS(dimacs, false, extraClauses);
fclose(dimacs);
bool status_sat = false;
bool status_unsat = false;
std::vector<bool> values;
auto line_callback = [&](const std::string &line) {
if (line.empty()) {
return;
}
if (line[0] == 's') {
if (line.substr(0, 5) == "s SAT") {
status_sat = true;
}
if (line.substr(0, 7) == "s UNSAT") {
status_unsat = true;
}
return;
}
if (line[0] == 'v') {
std::stringstream ss(line.substr(1));
int lit;
while (ss >> lit) {
if (lit == 0) {
return;
}
bool val = lit >= 0;
int ind = lit >= 0 ? lit - 1 : -lit - 1;
if (Yosys::GetSize(values) <= ind) {
values.resize(ind + 1);
}
values[ind] = val;
}
}
};
int return_code = Yosys::run_command(sat_command, line_callback);
if (return_code != 0 && return_code != 10 && return_code != 20) {
Yosys::log_cmd_error("Shell command failed!\n");
}
modelValues.clear();
modelValues.resize(modelIdx.size());
if (!status_sat && !status_unsat) {
solverTimeoutStatus = true;
}
if (!status_sat) {
return false;
}
for (size_t i = 0; i < modelIdx.size(); i++) {
int idx = modelIdx[i];
bool refvalue = true;
if (idx < 0)
idx = -idx, refvalue = false;
modelValues[i] = (values.at(idx - 1) == refvalue);
}
return true;
#else
Yosys::log_error("SAT solver command not available in this build!\n");
#endif
}

36
libs/ezsat/ezcmdline.h Normal file
View file

@ -0,0 +1,36 @@
/*
* ezSAT -- A simple and easy to use CNF generator for SAT solvers
*
* Copyright (C) 2013 Claire Xenia Wolf <claire@yosyshq.com>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
*
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
*
*/
#ifndef EZSATCOMMAND_H
#define EZSATCOMMAND_H
#include "ezsat.h"
class ezCmdlineSAT : public ezSAT
{
private:
std::string command;
public:
ezCmdlineSAT(const std::string &cmd);
virtual ~ezCmdlineSAT();
bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions) override;
};
#endif

4
libs/ezsat/ezminisat.cc
View file

@ -103,7 +103,7 @@ bool ezMiniSAT::solver(const std::vector<int> &modelExpressions, std::vector<boo
{
preSolverCallback();
solverTimoutStatus = false;
solverTimeoutStatus = false;
if (0) {
contradiction:
@ -206,7 +206,7 @@ contradiction:
#if defined(HAS_ALARM)
if (solverTimeout > 0) {
if (alarmHandlerTimeout == 0)
solverTimoutStatus = true;
solverTimeoutStatus = true;
alarm(0);
sigaction(SIGALRM, &old_sig_action, NULL);
alarm(old_alarm_timeout);

15
libs/ezsat/ezsat.cc
View file

@ -54,7 +54,7 @@ ezSAT::ezSAT()
cnfClausesCount = 0;
solverTimeout = 0;
solverTimoutStatus = false;
solverTimeoutStatus = false;
literal("CONST_TRUE");
literal("CONST_FALSE");
@ -1222,10 +1222,15 @@ 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 (f == nullptr) {
fprintf(stderr, "Usage error: printDIMACS() must not be called with a null FILE pointer\n");
abort();
}
if (cnfConsumed) {
fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!");
fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!\n");
abort();
}
@ -1259,8 +1264,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);

8
libs/ezsat/ezsat.h
View file

@ -78,7 +78,7 @@ protected:
public:
int solverTimeout;
bool solverTimoutStatus;
bool solverTimeoutStatus;
ezSAT();
virtual ~ezSAT();
@ -153,8 +153,8 @@ public:
solverTimeout = newTimeoutSeconds;
}
bool getSolverTimoutStatus() {
return solverTimoutStatus;
bool getSolverTimeoutStatus() {
return solverTimeoutStatus;
}
// manage CNF (usually only accessed by SAT solvers)
@ -295,7 +295,7 @@ public:
// printing CNF and internal state
void printDIMACS(FILE *f, bool verbose = false) const;
void printDIMACS(FILE *f, bool verbose = false, const std::vector<std::vector<int>> &extraClauses = std::vector<std::vector<int>>()) const;
void printInternalState(FILE *f) const;
// more sophisticated constraints (designed to be used directly with assume(..))