Merge pull request #4303 from Coloquinte/sat_choice

Infrastructure to run a Sat solver as a command

Makefile

@@ -638,6 +638,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
@@ -683,6 +684,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

kernel/satgen.h

@@ -59,6 +59,7 @@ struct SatSolver
 
 struct ezSatPtr : public std::unique_ptr<ezSAT> {
 	ezSatPtr() : unique_ptr<ezSAT>(yosys_satsolver->create()) { }
+	explicit ezSatPtr(SatSolver *solver) : unique_ptr<ezSAT>((solver ? solver : yosys_satsolver)->create()) { }
 };
 
 struct SatGen

libs/ezsat/ezcmdline.cc

@@ -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
+}

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 <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

libs/ezsat/ezminisat.cc

@@ -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);

libs/ezsat/ezsat.cc

@@ -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);

libs/ezsat/ezsat.h

@@ -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(..))

passes/cmds/scratchpad.cc

@@ -37,7 +37,7 @@ struct ScratchpadPass : public Pass {
 		log("\n");
 		log("    scratchpad [options]\n");
 		log("\n");
-		log("This pass allows to read and modify values from the scratchpad of the current\n");
+		log("This pass allows reading and modifying values from the scratchpad of the current\n");
 		log("design. Options:\n");
 		log("\n");
 		log("    -get <identifier>\n");

passes/sat/sat.cc

@@ -31,6 +31,22 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
+static SatSolver *find_satsolver(const std::string &name)
+{
+	for (auto solver = yosys_satsolver_list; solver != nullptr; solver = solver->next)
+		if (solver->name == name)
+			return solver;
+	return nullptr;
+}
+
+static std::string list_satsolvers()
+{
+	std::string result;
+	for (auto solver = yosys_satsolver_list; solver != nullptr; solver = solver->next)
+		result += result.empty() ? solver->name : ", " + solver->name;
+	return result;
+}
+
 struct SatHelper
 {
 	RTLIL::Design *design;
@@ -60,8 +76,8 @@ struct SatHelper
 	int max_timestep, timeout;
 	bool gotTimeout;
 
-	SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef, bool set_def_formal) :
-		design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap)
+	SatHelper(RTLIL::Design *design, RTLIL::Module *module, SatSolver *solver, bool enable_undef, bool set_def_formal) :
+		design(design), module(module), sigmap(module), ct(design), ez(solver), satgen(ez.get(), &sigmap)
 	{
 		this->enable_undef = enable_undef;
 		satgen.model_undef = enable_undef;
@@ -441,7 +457,7 @@ struct SatHelper
 		log_assert(gotTimeout == false);
 		ez->setSolverTimeout(timeout);
 		bool success = ez->solve(modelExpressions, modelValues, assumptions);
-		if (ez->getSolverTimoutStatus())
+		if (ez->getSolverTimeoutStatus())
 			gotTimeout = true;
 		return success;
 	}
@@ -451,7 +467,7 @@ struct SatHelper
 		log_assert(gotTimeout == false);
 		ez->setSolverTimeout(timeout);
 		bool success = ez->solve(modelExpressions, modelValues, a, b, c, d, e, f);
-		if (ez->getSolverTimoutStatus())
+		if (ez->getSolverTimeoutStatus())
 			gotTimeout = true;
 		return success;
 	}
@@ -1066,6 +1082,10 @@ struct SatPass : public Pass {
 		log("    -timeout <N>\n");
 		log("        Maximum number of seconds a single SAT instance may take.\n");
 		log("\n");
+		log("    -select-solver <name>\n");
+		log("        Select SAT solver implementation for this invocation.\n");
+		log("        If not given, uses scratchpad key 'sat.solver' if set, otherwise default.\n");
+		log("\n");
 		log("    -verify\n");
 		log("        Return an error and stop the synthesis script if the proof fails.\n");
 		log("\n");
@@ -1097,8 +1117,14 @@ struct SatPass : public Pass {
 
 		log_header(design, "Executing SAT pass (solving SAT problems in the circuit).\n");
 
+		std::string solver_name = design->scratchpad_get_string("sat.solver", "");
+
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++) {
+			if (args[argidx] == "-select-solver" && argidx+1 < args.size()) {
+				solver_name = args[++argidx];
+				continue;
+			}
 			if (args[argidx] == "-all") {
 				loopcount = -1;
 				continue;
@@ -1336,6 +1362,14 @@ struct SatPass : public Pass {
 		}
 		extra_args(args, argidx, design);
 
+		SatSolver *solver = yosys_satsolver;
+		if (!solver_name.empty()) {
+			solver = find_satsolver(solver_name);
+			if (solver == nullptr)
+				log_cmd_error("Unknown SAT solver '%s'. Available solvers: %s\n",
+						solver_name, list_satsolvers());
+		}
+
 		RTLIL::Module *module = NULL;
 		for (auto mod : design->selected_modules()) {
 			if (module)
@@ -1398,13 +1432,15 @@ struct SatPass : public Pass {
 				shows.push_back(wire->name.str());
 		}
 
+		log("Using SAT solver `%s`.\n", solver->name.c_str());
+
 		if (tempinduct)
 		{
 			if (loopcount > 0 || max_undef)
 				log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
 
-			SatHelper basecase(design, module, enable_undef, set_def_formal);
-			SatHelper inductstep(design, module, enable_undef, set_def_formal);
+			SatHelper basecase(design, module, solver, enable_undef, set_def_formal);
+			SatHelper inductstep(design, module, solver, enable_undef, set_def_formal);
 
 			basecase.sets = sets;
 			basecase.set_assumes = set_assumes;
@@ -1593,7 +1629,7 @@ struct SatPass : public Pass {
 			if (maxsteps > 0)
 				log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
 
-			SatHelper sathelper(design, module, enable_undef, set_def_formal);
+			SatHelper sathelper(design, module, solver, enable_undef, set_def_formal);
 
 			sathelper.sets = sets;
 			sathelper.set_assumes = set_assumes;

tests/various/.gitignore

@@ -4,6 +4,8 @@
 /plugin.so
 /plugin_search
 /plugin.so.dSYM
+/ezcmdline_plugin.so
+/ezcmdline_plugin.so.dSYM
 /temp
 /smtlib2_module.smt2
 /smtlib2_module-filtered.smt2

tests/various/ezcmdline_dummy_solver

@@ -0,0 +1,61 @@
+#!/bin/sh
+# Dummy SAT solver for ezCmdlineSAT tests.
+# Accepts exactly two CNF shapes:
+#  - SAT:   p cnf 1 1; clause: "1 0"  -> exits 10 with v 1
+#  - UNSAT: p cnf 1 2; clauses: "1 0" and "-1 0" -> exits 20
+set -e
+
+if [ "$#" -ne 1 ]; then
+	echo "usage: $0 <cnf>" >&2
+	exit 1
+fi
+
+awk '
+BEGIN {
+	vars = 0;
+	clauses = 0;
+	clause_count = 0;
+	clause_data = "";
+	current = "";
+}
+$1 == "c" {
+	next;
+}
+$1 == "p" && $2 == "cnf" {
+	vars = $3;
+	clauses = $4;
+	next;
+}
+{
+	for (i = 1; i <= NF; i++) {
+		lit = $i;
+		if (lit == 0) {
+			clause_count++;
+			if (clause_data != "")
+				clause_data = clause_data ";" current;
+			else
+				clause_data = current;
+			current = "";
+		} else {
+			if (current == "")
+				current = lit;
+			else
+				current = current "," lit;
+		}
+	}
+}
+END {
+	if (vars == 1 && clause_count == 1 && clause_data == "1") {
+		print "s SATISFIABLE";
+		print "v 1 0";
+		exit 10;
+	}
+	if (vars == 1 && clause_count == 2 && clause_data == "1;-1") {
+		print "s UNSATISFIABLE";
+		exit 20;
+	}
+	print "c unexpected CNF for dummy solver";
+	print "c vars=" vars " header_clauses=" clauses " parsed_clauses=" clause_count " data=" clause_data;
+	exit 1;
+}
+' "$1"

tests/various/ezcmdline_plugin.cc

@@ -0,0 +1,53 @@
+#include "kernel/yosys.h"
+#include "libs/ezsat/ezcmdline.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct EzCmdlineTestPass : public Pass {
+	EzCmdlineTestPass() : Pass("ezcmdline_test", "smoke-test ezCmdlineSAT") { }
+	void execute(std::vector<std::string> args, RTLIL::Design *design) override
+	{
+		std::string cmd;
+		size_t argidx = 1;
+
+		while (argidx < args.size()) {
+			if (args[argidx] == "-cmd" && argidx + 1 < args.size()) {
+				cmd = args[argidx + 1];
+				argidx += 2;
+				continue;
+			}
+			break;
+		}
+
+		extra_args(args, argidx, design);
+
+		if (cmd.empty())
+			log_error("Missing -cmd <solver> argument.\n");
+
+		ezCmdlineSAT sat(cmd);
+		sat.non_incremental();
+
+		// assume("A") adds a permanent CNF clause "A".
+		sat.assume(sat.VAR("A"));
+
+		std::vector<int> model_expressions;
+		std::vector<bool> model_values;
+		model_expressions.push_back(sat.VAR("A"));
+
+		// Expect SAT with A=true.
+		if (!sat.solve(model_expressions, model_values))
+			log_error("ezCmdlineSAT SAT case failed.\n");
+		if (model_values.size() != 1 || !model_values[0])
+			log_error("ezCmdlineSAT SAT model mismatch.\n");
+
+		// Passing NOT("A") here adds a temporary unit clause for this solve call,
+		// so the solver sees A && !A and must return UNSAT.
+		if (sat.solve(model_expressions, model_values, sat.NOT("A")))
+			log_error("ezCmdlineSAT UNSAT case failed.\n");
+
+		log("ezcmdline_test passed!\n");
+	}
+} EzCmdlineTestPass;
+
+PRIVATE_NAMESPACE_END

tests/various/ezcmdline_plugin.sh

@@ -0,0 +1,12 @@
+set -e
+
+DIR=$(cd "$(dirname "$0")" && pwd)
+BASEDIR=$(cd "$DIR/../.." && pwd)
+rm -f "$DIR/ezcmdline_plugin.so"
+chmod +x "$DIR/ezcmdline_dummy_solver"
+CXXFLAGS=$("$BASEDIR/yosys-config" --cxxflags)
+DATDIR=$("$BASEDIR/yosys-config" --datdir)
+DATDIR=${DATDIR//\//\\\/}
+CXXFLAGS=${CXXFLAGS//$DATDIR/..\/..\/share}
+"$BASEDIR/yosys-config" --exec --cxx ${CXXFLAGS} -I"$BASEDIR" --ldflags -shared -o "$DIR/ezcmdline_plugin.so" "$DIR/ezcmdline_plugin.cc"
+"$BASEDIR/yosys" -m "$DIR/ezcmdline_plugin.so" -p "ezcmdline_test -cmd $DIR/ezcmdline_dummy_solver" | grep -q "ezcmdline_test passed!"