From 36e6ab9c90d00ff5baf387611a597eb1d356eec3 Mon Sep 17 00:00:00 2001
From: Gabriel Gouvine <gabriel.gouvine_git@m4x.org>
Date: Mon, 25 Mar 2024 11:33:52 +0000
Subject: [PATCH] ezsat: New Sat class to call an external command

---
 Makefile                |  2 +
 libs/ezsat/ezcommand.cc | 81 +++++++++++++++++++++++++++++++++++++++++
 libs/ezsat/ezcommand.h  | 36 ++++++++++++++++++
 3 files changed, 119 insertions(+)
 create mode 100644 libs/ezsat/ezcommand.cc
 create mode 100644 libs/ezsat/ezcommand.h

diff --git a/Makefile b/Makefile
index 391fb7288f3..814656e9009 100644
--- a/Makefile
+++ b/Makefile
@@ -632,6 +632,7 @@ $(eval $(call add_include_file,kernel/yosys.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
@@ -672,6 +673,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 00000000000..f66c0b9c4fd
--- /dev/null
+++ b/libs/ezsat/ezcommand.cc
@@ -0,0 +1,81 @@
+
+#include "ezcommand.h"
+
+#include "../../kernel/yosys.h"
+
+ezSATCommand::ezSATCommand(const std::string &cmd) : command(cmd) {}
+
+ezSATCommand::~ezSATCommand() {}
+
+bool ezSATCommand::solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &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<int> modelIdx;
+	for (auto id : modelExpressions)
+		modelIdx.push_back(bind(id));
+
+	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;
+			}
+		}
+	};
+	Yosys::run_command(sat_command, line_callback);
+
+	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 00000000000..a0e3de4ed59
--- /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 <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 ezSATCommand : public ezSAT
+{
+private:
+	std::string command;
+
+public:
+	ezSATCommand(const std::string &cmd);
+	virtual ~ezSATCommand();
+	bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions) override;
+};
+
+#endif