diff --git a/Makefile b/Makefile index 76ac4bb18..400846cef 100644 --- a/Makefile +++ b/Makefile @@ -616,6 +616,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/ezcmdline.h)) ifeq ($(ENABLE_ZLIB),1) $(eval $(call add_include_file,libs/fst/fstapi.h)) endif @@ -657,6 +658,7 @@ OBJS += libs/json11/json11.o OBJS += libs/ezsat/ezsat.o OBJS += libs/ezsat/ezminisat.o +OBJS += libs/ezsat/ezcmdline.o OBJS += libs/minisat/Options.o OBJS += libs/minisat/SimpSolver.o diff --git a/libs/ezsat/ezcmdline.cc b/libs/ezsat/ezcmdline.cc new file mode 100644 index 000000000..dddec1067 --- /dev/null +++ b/libs/ezsat/ezcmdline.cc @@ -0,0 +1,89 @@ + +#include "ezcmdline.h" + +#include "../../kernel/yosys.h" + +ezCmdlineSAT::ezCmdlineSAT(const std::string &cmd) : command(cmd) {} + +ezCmdlineSAT::~ezCmdlineSAT() {} + +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"); + 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"); + + 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; + 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; + } + } + }; + 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) { + 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; +#else + Yosys::log_error("SAT solver command not available in this build!\n"); +#endif +} diff --git a/libs/ezsat/ezcmdline.h b/libs/ezsat/ezcmdline.h new file mode 100644 index 000000000..8ec8c7043 --- /dev/null +++ b/libs/ezsat/ezcmdline.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 ezCmdlineSAT : public ezSAT +{ +private: + std::string command; + +public: + ezCmdlineSAT(const std::string &cmd); + virtual ~ezCmdlineSAT(); + bool solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) override; +}; + +#endif diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 20a210abe..fbdfc20f6 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(..))