From d62a47b8ef768520e120d5cfcd147fcbd5d5aad8 Mon Sep 17 00:00:00 2001 From: Gabriel Gouvine Date: Mon, 25 Mar 2024 11:33:52 +0000 Subject: [PATCH 1/5] ezsat: New Sat class to call an external command --- Makefile | 2 + libs/ezsat/ezcommand.cc | 83 +++++++++++++++++++++++++++++++++++++++++ libs/ezsat/ezcommand.h | 36 ++++++++++++++++++ 3 files changed, 121 insertions(+) create mode 100644 libs/ezsat/ezcommand.cc create mode 100644 libs/ezsat/ezcommand.h diff --git a/Makefile b/Makefile index f8d628010..d73253390 100644 --- a/Makefile +++ b/Makefile @@ -633,6 +633,7 @@ $(eval $(call add_include_file,kernel/yosys_common.h)) $(eval $(call add_include_file,kernel/yw.h)) $(eval $(call add_include_file,libs/ezsat/ezsat.h)) $(eval $(call add_include_file,libs/ezsat/ezminisat.h)) +$(eval $(call add_include_file,libs/ezsat/ezcommand.h)) ifeq ($(ENABLE_ZLIB),1) $(eval $(call add_include_file,libs/fst/fstapi.h)) endif @@ -673,6 +674,7 @@ OBJS += libs/json11/json11.o OBJS += libs/ezsat/ezsat.o OBJS += libs/ezsat/ezminisat.o +OBJS += libs/ezsat/ezcommand.o OBJS += libs/minisat/Options.o OBJS += libs/minisat/SimpSolver.o diff --git a/libs/ezsat/ezcommand.cc b/libs/ezsat/ezcommand.cc new file mode 100644 index 000000000..10104a2cd --- /dev/null +++ b/libs/ezsat/ezcommand.cc @@ -0,0 +1,83 @@ + +#include "ezcommand.h" + +#include "../../kernel/yosys.h" + +ezSATCommand::ezSATCommand(const std::string &cmd) : command(cmd) {} + +ezSATCommand::~ezSATCommand() {} + +bool ezSATCommand::solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) +{ + if (!assumptions.empty()) { + Yosys::log_error("Assumptions are not supported yet by command-based Sat solver\n"); + } + 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"); + printDIMACS(dimacs); + fclose(dimacs); + + std::vector modelIdx; + for (auto id : modelExpressions) + modelIdx.push_back(bind(id)); + + bool status_sat = false; + bool status_unsat = false; + std::vector 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; + } + } + }; + if (Yosys::run_command(sat_command, line_callback) != 0) { + Yosys::log_cmd_error("Shell command failed!\n"); + } + + modelValues.clear(); + modelValues.resize(modelIdx.size()); + + if (!status_sat && !status_unsat) { + solverTimoutStatus = 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; +} \ No newline at end of file diff --git a/libs/ezsat/ezcommand.h b/libs/ezsat/ezcommand.h new file mode 100644 index 000000000..a0e3de4ed --- /dev/null +++ b/libs/ezsat/ezcommand.h @@ -0,0 +1,36 @@ +/* + * ezSAT -- A simple and easy to use CNF generator for SAT solvers + * + * Copyright (C) 2013 Claire Xenia Wolf + * + * 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 ezSATCommand : public ezSAT +{ +private: + std::string command; + +public: + ezSATCommand(const std::string &cmd); + virtual ~ezSATCommand(); + bool solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) override; +}; + +#endif From c807ef44dc5591c7687c6f29f18181ee0d885bad Mon Sep 17 00:00:00 2001 From: Gabriel Gouvine Date: Thu, 28 Mar 2024 09:56:48 +0000 Subject: [PATCH 2/5] ezsat: Support for assumptions in Sat command --- libs/ezsat/ezcommand.cc | 11 ++++++----- libs/ezsat/ezsat.cc | 6 ++++-- libs/ezsat/ezsat.h | 2 +- 3 files changed, 11 insertions(+), 8 deletions(-) diff --git a/libs/ezsat/ezcommand.cc b/libs/ezsat/ezcommand.cc index 10104a2cd..c2925b647 100644 --- a/libs/ezsat/ezcommand.cc +++ b/libs/ezsat/ezcommand.cc @@ -9,19 +9,20 @@ ezSATCommand::~ezSATCommand() {} bool ezSATCommand::solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) { - if (!assumptions.empty()) { - Yosys::log_error("Assumptions are not supported yet by command-based Sat solver\n"); - } 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"); - printDIMACS(dimacs); - fclose(dimacs); std::vector modelIdx; for (auto id : modelExpressions) modelIdx.push_back(bind(id)); + std::vector> extraClauses; + for (auto id : assumptions) + extraClauses.push_back({bind(id)}); + + printDIMACS(dimacs, false, extraClauses); + fclose(dimacs); bool status_sat = false; bool status_unsat = false; diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 3b089ccca..3e210cfe9 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -1222,7 +1222,7 @@ ezSATvec ezSAT::vec(const std::vector &vec) return ezSATvec(*this, vec); } -void ezSAT::printDIMACS(FILE *f, bool verbose) const +void ezSAT::printDIMACS(FILE *f, bool verbose, const std::vector> &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> 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); diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h index 7f3bdf68d..507708cb2 100644 --- a/libs/ezsat/ezsat.h +++ b/libs/ezsat/ezsat.h @@ -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> &extraClauses = std::vector>()) const; void printInternalState(FILE *f) const; // more sophisticated constraints (designed to be used directly with assume(..)) From 316ec3b0b415c8253918815aeeb8389bbd5b1233 Mon Sep 17 00:00:00 2001 From: Gabriel Gouvine Date: Thu, 28 Mar 2024 10:14:30 +0000 Subject: [PATCH 3/5] ezsat: Fix build for emscripten/wasi --- libs/ezsat/ezcommand.cc | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/libs/ezsat/ezcommand.cc b/libs/ezsat/ezcommand.cc index c2925b647..2040d3c1a 100644 --- a/libs/ezsat/ezcommand.cc +++ b/libs/ezsat/ezcommand.cc @@ -9,6 +9,7 @@ ezSATCommand::~ezSATCommand() {} bool ezSATCommand::solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &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()); @@ -81,4 +82,7 @@ bool ezSATCommand::solver(const std::vector &modelExpressions, std::vector< modelValues[i] = (values.at(idx - 1) == refvalue); } return true; +#else + Yosys::log_error("SAT solver command not available in this build!\n"); +#endif } \ No newline at end of file From e16cf967fd242ccba16f69ef7a8b053af3673ae2 Mon Sep 17 00:00:00 2001 From: Gabriel Gouvine Date: Thu, 28 Mar 2024 17:25:19 +0000 Subject: [PATCH 4/5] ezsat: Rename files and class for ezCmdlineSat --- Makefile | 4 ++-- libs/ezsat/{ezcommand.cc => ezcmdline.cc} | 10 +++++----- libs/ezsat/{ezcommand.h => ezcmdline.h} | 6 +++--- 3 files changed, 10 insertions(+), 10 deletions(-) rename libs/ezsat/{ezcommand.cc => ezcmdline.cc} (91%) rename libs/ezsat/{ezcommand.h => ezcmdline.h} (92%) diff --git a/Makefile b/Makefile index d73253390..c70c50a13 100644 --- a/Makefile +++ b/Makefile @@ -633,7 +633,7 @@ $(eval $(call add_include_file,kernel/yosys_common.h)) $(eval $(call add_include_file,kernel/yw.h)) $(eval $(call add_include_file,libs/ezsat/ezsat.h)) $(eval $(call add_include_file,libs/ezsat/ezminisat.h)) -$(eval $(call add_include_file,libs/ezsat/ezcommand.h)) +$(eval $(call add_include_file,libs/ezsat/ezcmdline.h)) ifeq ($(ENABLE_ZLIB),1) $(eval $(call add_include_file,libs/fst/fstapi.h)) endif @@ -674,7 +674,7 @@ OBJS += libs/json11/json11.o OBJS += libs/ezsat/ezsat.o OBJS += libs/ezsat/ezminisat.o -OBJS += libs/ezsat/ezcommand.o +OBJS += libs/ezsat/ezcmdline.o OBJS += libs/minisat/Options.o OBJS += libs/minisat/SimpSolver.o diff --git a/libs/ezsat/ezcommand.cc b/libs/ezsat/ezcmdline.cc similarity index 91% rename from libs/ezsat/ezcommand.cc rename to libs/ezsat/ezcmdline.cc index 2040d3c1a..1b5278fab 100644 --- a/libs/ezsat/ezcommand.cc +++ b/libs/ezsat/ezcmdline.cc @@ -1,13 +1,13 @@ -#include "ezcommand.h" +#include "ezcmdline.h" #include "../../kernel/yosys.h" -ezSATCommand::ezSATCommand(const std::string &cmd) : command(cmd) {} +ezCmdlineSAT::ezCmdlineSAT(const std::string &cmd) : command(cmd) {} -ezSATCommand::~ezSATCommand() {} +ezCmdlineSAT::~ezCmdlineSAT() {} -bool ezSATCommand::solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) +bool ezCmdlineSAT::solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) { #if !defined(YOSYS_DISABLE_SPAWN) const std::string tempdir_name = Yosys::make_temp_dir(Yosys::get_base_tmpdir() + "/yosys-sat-XXXXXX"); @@ -85,4 +85,4 @@ bool ezSATCommand::solver(const std::vector &modelExpressions, std::vector< #else Yosys::log_error("SAT solver command not available in this build!\n"); #endif -} \ No newline at end of file +} diff --git a/libs/ezsat/ezcommand.h b/libs/ezsat/ezcmdline.h similarity index 92% rename from libs/ezsat/ezcommand.h rename to libs/ezsat/ezcmdline.h index a0e3de4ed..8ec8c7043 100644 --- a/libs/ezsat/ezcommand.h +++ b/libs/ezsat/ezcmdline.h @@ -22,14 +22,14 @@ #include "ezsat.h" -class ezSATCommand : public ezSAT +class ezCmdlineSAT : public ezSAT { private: std::string command; public: - ezSATCommand(const std::string &cmd); - virtual ~ezSATCommand(); + ezCmdlineSAT(const std::string &cmd); + virtual ~ezCmdlineSAT(); bool solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) override; }; From ccf04533e674fedc0cdb2facaae6c363965dd099 Mon Sep 17 00:00:00 2001 From: Gabriel Gouvine Date: Tue, 9 Apr 2024 15:56:36 +0100 Subject: [PATCH 5/5] ezsat: Fix handling of error codes --- libs/ezsat/ezcmdline.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/libs/ezsat/ezcmdline.cc b/libs/ezsat/ezcmdline.cc index 1b5278fab..dddec1067 100644 --- a/libs/ezsat/ezcmdline.cc +++ b/libs/ezsat/ezcmdline.cc @@ -58,7 +58,8 @@ bool ezCmdlineSAT::solver(const std::vector &modelExpressions, std::vector< } } }; - if (Yosys::run_command(sat_command, line_callback) != 0) { + 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"); }