From 0f6ef777750e9c537d71b37a1698c08d38add2b7 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Tue, 20 Jan 2026 09:28:00 -0800
Subject: [PATCH] Add test for ezCmdlineSAT

---
 tests/various/.gitignore             |  2 +
 tests/various/ezcmdline_dummy_solver | 61 ++++++++++++++++++++++++++++
 tests/various/ezcmdline_plugin.cc    | 53 ++++++++++++++++++++++++
 tests/various/ezcmdline_plugin.sh    |  8 ++++
 4 files changed, 124 insertions(+)
 create mode 100755 tests/various/ezcmdline_dummy_solver
 create mode 100644 tests/various/ezcmdline_plugin.cc
 create mode 100644 tests/various/ezcmdline_plugin.sh

diff --git a/tests/various/.gitignore b/tests/various/.gitignore
index e116179ae..9296a04c0 100644
--- a/tests/various/.gitignore
+++ b/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
diff --git a/tests/various/ezcmdline_dummy_solver b/tests/various/ezcmdline_dummy_solver
new file mode 100755
index 000000000..db5b21b8e
--- /dev/null
+++ b/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"
diff --git a/tests/various/ezcmdline_plugin.cc b/tests/various/ezcmdline_plugin.cc
new file mode 100644
index 000000000..b775829b3
--- /dev/null
+++ b/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
diff --git a/tests/various/ezcmdline_plugin.sh b/tests/various/ezcmdline_plugin.sh
new file mode 100644
index 000000000..cc1ed4bc9
--- /dev/null
+++ b/tests/various/ezcmdline_plugin.sh
@@ -0,0 +1,8 @@
+set -e
+
+DIR=$(cd "$(dirname "$0")" && pwd)
+BASEDIR=$(cd "$DIR/../.." && pwd)
+rm -f "$DIR/ezcmdline_plugin.so"
+chmod +x "$DIR/ezcmdline_dummy_solver"
+"$BASEDIR/yosys-config" --build "$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!"