Merge pull request #2015 from boqwxp/qbfsat-bisection

qbfsat: Add an iterative bisection optimization method and make it the default.

1 files changed, 207 insertions, 98 deletions

diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc
index d99ca1b53..c42760488 100644
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -19,22 +19,12 @@
 
 #include "kernel/yosys.h"
 #include "kernel/celltypes.h"
+#include "kernel/consteval.h"
 #include "kernel/log.h"
 #include "kernel/rtlil.h"
 #include "kernel/register.h"
-#include <cstdio>
 #include <algorithm>
 
-#if defined(_WIN32)
-#  define WIFEXITED(x) 1
-#  define WIFSIGNALED(x) 0
-#  define WIFSTOPPED(x) 0
-#  define WEXITSTATUS(x) ((x) & 0xff)
-#  define WTERMSIG(x) SIGTERM
-#else
-#  include <sys/wait.h>
-#endif
-
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
@@ -43,13 +33,13 @@ struct QbfSolutionType {
 	dict<std::string, std::string> hole_to_value;
 	bool sat;
 	bool unknown; //true if neither 'sat' nor 'unsat'
-	bool success; //true if exit code 0
 
-	QbfSolutionType() : sat(false), unknown(true), success(false) {}
+	QbfSolutionType() : sat(false), unknown(true) {}
 };
 
 struct QbfSolveOptions {
 	bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs, assume_neg;
+	bool nooptimize, nobisection;
 	bool sat, unsat, show_smtbmc;
 	std::string specialize_soln_file;
 	std::string write_soln_soln_file;
@@ -57,12 +47,14 @@ struct QbfSolveOptions {
 	size_t argidx;
 	QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false),
 			nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false),
-			sat(false), unsat(false), show_smtbmc(false), argidx(0) {};
+			nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false),
+			argidx(0) {};
 };
 
 void recover_solution(QbfSolutionType &sol) {
 	YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED");
 	YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
+	YS_REGEX_TYPE memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\"");
 	YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
 #ifndef NDEBUG
 	YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+");
@@ -86,6 +78,10 @@ void recover_solution(QbfSolutionType &sol) {
 			sat_regex_found = true;
 		else if (YS_REGEX_NS::regex_search(x, unsat_regex))
 			unsat_regex_found = true;
+		else if (YS_REGEX_NS::regex_search(x, memout_regex)) {
+			sol.unknown = true;
+			log_warning("solver ran out of memory\n");
+		}
 	}
 #ifndef NDEBUG
 	log_assert(!sol.unknown && sol.sat? sat_regex_found : true);
@@ -107,6 +103,40 @@ dict<std::string, std::string> get_hole_loc_name_map(RTLIL::Module *module, cons
 	return hole_loc_to_name;
 }
 
+pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
+	bool found_input = false;
+	bool found_hole = false;
+	bool found_1bit_output = false;
+	bool found_assert_assume = false;
+	pool<std::string> input_wires;
+	for (auto wire : module->wires()) {
+		if (wire->port_input) {
+			found_input = true;
+			input_wires.insert(wire->name.str());
+		}
+		if (wire->port_output && wire->width == 1)
+			found_1bit_output = true;
+	}
+	for (auto cell : module->cells()) {
+		if (cell->type == "$allconst")
+			found_input = true;
+		if (cell->type == "$anyconst")
+			found_hole = true;
+		if (cell->type.in("$assert", "$assume"))
+			found_assert_assume = true;
+	}
+	if (!found_input)
+		log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n");
+	if (!found_hole)
+		log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n");
+	if (!found_1bit_output && !found_assert_assume)
+		log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n");
+	if (!found_assert_assume && !opt.assume_outputs)
+		log_cmd_error("Did not find any $assert/$assume cells. Single-bit outputs were found, but `-assume-outputs` was not specified.\n");
+
+	return input_wires;
+}
+
 void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std::string &file) {
 	std::ofstream fout(file.c_str());
 	if (!fout)
@@ -164,7 +194,7 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) {
 	}
 }
 
-void specialize(RTLIL::Module *module, const QbfSolutionType &sol) {
+void specialize(RTLIL::Module *module, const QbfSolutionType &sol, bool quiet = false) {
 	dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol);
 	pool<RTLIL::Cell *> anyconsts_to_remove;
 	for (auto cell : module->cells())
@@ -189,7 +219,8 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol) {
 		log_assert(wire->width > 0 && GetSize(hole_value) == wire->width);
 #endif
 
-		log("Specializing %s with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str());
+		if (!quiet)
+			log("Specializing %s with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str());
 		std::vector<RTLIL::SigBit> value_bv;
 		value_bv.reserve(wire->width);
 		for (char c : hole_value)
@@ -219,7 +250,6 @@ void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) {
 			value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0);
 		std::reverse(value_bv.begin(), value_bv.end());
 	}
-
 }
 
 void allconstify_inputs(RTLIL::Module *module, const pool<std::string> &input_wires) {
@@ -280,84 +310,153 @@ void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
 	module->addAssume("$assume_qbfsat_miter_outputs", wires_to_assume[0], RTLIL::S1);
 }
 
-QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
+QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, const std::string &tempdir_name, const bool quiet = false, const int iter_num = 0) {
+	//Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]`
 	QbfSolutionType ret;
 	const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc";
+	const std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2";
+	const std::string smtbmc_cmd = yosys_smtbmc_exe + " -s z3 -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2 2>&1";
 	const std::string smtbmc_warning = "z3: WARNING:";
 	const bool show_smtbmc = opt.show_smtbmc;
 
-	const std::string tempdir_name = make_temp_dir("/tmp/yosys-z3-XXXXXX");
-	const std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem.smt2";
-#ifndef NDEBUG
-	log_assert(mod->design != nullptr);
-#endif
 	Pass::call(mod->design, smt2_command);
-	log_header(mod->design, "Solving QBF-SAT problem.\n");
 
-	//Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]`
-	{
-		const std::string cmd = yosys_smtbmc_exe + " -s z3 -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem.smt2 2>&1";
-		auto process_line = [&ret, &smtbmc_warning, &show_smtbmc](const std::string &line) {
-			ret.stdout_lines.push_back(line.substr(0, line.size()-1)); //don't include trailing newline
-			auto warning_pos = line.find(smtbmc_warning);
-			if (warning_pos != std::string::npos)
-				log_warning("%s", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str());
-			else
-				if (show_smtbmc)
-					log("smtbmc output: %s", line.c_str());
-		};
-
-		log("Launching \"%s\".\n", cmd.c_str());
-		int retval = run_command(cmd, process_line);
-		if (retval == 0) {
-			ret.sat = true;
-			ret.unknown = false;
-		} else if (retval == 1) {
-			ret.sat = false;
-			ret.unknown = false;
-		}
+	auto process_line = [&ret, &smtbmc_warning, &show_smtbmc, &quiet](const std::string &line) {
+		ret.stdout_lines.push_back(line.substr(0, line.size()-1)); //don't include trailing newline
+		auto warning_pos = line.find(smtbmc_warning);
+		if (warning_pos != std::string::npos)
+			log_warning("%s", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str());
+		else
+			if (show_smtbmc && !quiet)
+				log("smtbmc output: %s", line.c_str());
+	};
+	log_header(mod->design, "Solving QBF-SAT problem.\n");
+	if (!quiet) log("Launching \"%s\".\n", smtbmc_cmd.c_str());
+	int retval = run_command(smtbmc_cmd, process_line);
+	if (retval == 0) {
+		ret.sat = true;
+		ret.unknown = false;
+	} else if (retval == 1) {
+		ret.sat = false;
+		ret.unknown = false;
 	}
 
-	if(!opt.nocleanup)
-		remove_directory(tempdir_name);
-
 	recover_solution(ret);
-
 	return ret;
 }
 
-pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
-	bool found_input = false;
-	bool found_hole = false;
-	bool found_1bit_output = false;
-	bool found_assert_assume = false;
-	pool<std::string> input_wires;
-	for (auto wire : module->wires()) {
-		if (wire->port_input) {
-			found_input = true;
-			input_wires.insert(wire->name.str());
-		}
-		if (wire->port_output && wire->width == 1)
-			found_1bit_output = true;
+QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
+	QbfSolutionType ret, best_soln;
+	const std::string tempdir_name = make_temp_dir("/tmp/yosys-z3-XXXXXX");
+	RTLIL::Module *module = mod;
+	RTLIL::Design *design = module->design;
+	std::string module_name = module->name.str();
+	RTLIL::Wire *wire_to_optimize = nullptr;
+	RTLIL::IdString wire_to_optimize_name;
+	bool maximize = false;
+	log_assert(module->design != nullptr);
+
+	Pass::call(design, "design -push-copy");
+
+	//Replace input wires with wires assigned $allconst cells:
+	pool<std::string> input_wires = validate_design_and_get_inputs(module, opt);
+	allconstify_inputs(module, input_wires);
+	if (opt.assume_outputs)
+		assume_miter_outputs(module, opt);
+
+	//Find the wire to be optimized, if any:
+	for (auto wire : module->wires())
+		if (wire->get_bool_attribute("\\maximize") || wire->get_bool_attribute("\\minimize"))
+			wire_to_optimize = wire;
+	if (wire_to_optimize != nullptr) {
+		wire_to_optimize_name = wire_to_optimize->name;
+		maximize = wire_to_optimize->get_bool_attribute("\\maximize");
 	}
-	for (auto cell : module->cells()) {
-		if (cell->type == "$allconst")
-			found_input = true;
-		if (cell->type == "$anyconst")
-			found_hole = true;
-		if (cell->type.in("$assert", "$assume"))
-			found_assert_assume = true;
+
+	if (opt.nobisection || opt.nooptimize) {
+		if (wire_to_optimize != nullptr && opt.nooptimize) {
+			wire_to_optimize->set_bool_attribute("\\maximize", false);
+			wire_to_optimize->set_bool_attribute("\\minimize", false);
+		}
+		ret = call_qbf_solver(module, opt, tempdir_name, false, 0);
+	} else {
+		//Do the iterated bisection method:
+		unsigned int iter_num = 1;
+		unsigned int success = 0;
+		unsigned int failure = 0;
+		unsigned int cur_thresh = 0;
+
+		log_assert(wire_to_optimize != nullptr);
+		log("%s wire \"%s\".\n", (maximize? "Maximizing" : "Minimizing"), log_signal(wire_to_optimize));
+
+		//If maximizing, grow until we get a failure.  Then bisect success and failure.
+		while (failure == 0 || success - failure > 1) {
+			Pass::call(design, "design -push-copy");
+			log_header(design, "Preparing QBF-SAT problem.\n");
+
+			if (cur_thresh != 0) {
+				//Add thresholding logic (but not on the initial run when we don't have a sense of where to start):
+				RTLIL::SigSpec comparator = maximize? module->Ge(NEW_ID, module->wire(wire_to_optimize_name), RTLIL::Const(cur_thresh), false)
+				                                    : module->Le(NEW_ID, module->wire(wire_to_optimize_name), RTLIL::Const(cur_thresh), false);
+
+				module->addAssume(wire_to_optimize_name.str() + "__threshold", comparator, RTLIL::Const(1, 1));
+				log("Trying to solve with %s %s %d.\n", wire_to_optimize_name.c_str(), (maximize? ">=" : "<="), cur_thresh);
+			}
+
+			ret = call_qbf_solver(module, opt, tempdir_name, false, iter_num);
+			Pass::call(design, "design -pop");
+			module = design->module(module_name);
+
+			if (!ret.unknown && ret.sat) {
+				Pass::call(design, "design -push-copy");
+				specialize(module, ret, true);
+
+				RTLIL::SigSpec wire, value, undef;
+				RTLIL::SigSpec::parse_sel(wire, design, module, wire_to_optimize_name.str());
+
+				ConstEval ce(module);
+				value = wire;
+				if (!ce.eval(value, undef))
+					log_cmd_error("Failed to evaluate signal %s: Missing value for %s.\n", log_signal(wire), log_signal(undef));
+				log_assert(value.is_fully_const());
+				success = value.as_const().as_int();
+				best_soln = ret;
+				log("Problem is satisfiable with %s = %d.\n", wire_to_optimize_name.c_str(), success);
+				Pass::call(design, "design -pop");
+				module = design->module(module_name);
+
+				//sometimes this happens if we get an 'unknown' or timeout
+				if (!maximize && success < failure)
+					break;
+				else if (maximize && success > failure)
+					break;
+			} else {
+				//Treat 'unknown' as UNSAT
+				failure = cur_thresh;
+				if (failure == 0) {
+					log("Problem is NOT satisfiable.\n");
+					break;
+				}
+				else
+					log("Problem is NOT satisfiable with %s %s %d.\n", wire_to_optimize_name.c_str(), (maximize? ">=" : "<="), failure);
+			}
+
+			iter_num++;
+			cur_thresh = (maximize && failure == 0)? 2 * success //growth
+			                                       : (success + failure) / 2; //bisection
+		}
+		if (success != 0 || failure != 0) {
+			log("Wire %s is %s at %d.\n", wire_to_optimize_name.c_str(), (maximize? "maximized" : "minimized"), success);
+			ret = best_soln;
+		}
 	}
-	if (!found_input)
-		log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n");
-	if (!found_hole)
-		log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n");
-	if (!found_1bit_output && !found_assert_assume)
-		log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n");
-	if (!found_assert_assume && !opt.assume_outputs)
-		log_cmd_error("Did not find any $assert/$assume cells. Single-bit outputs were found, but `-assume-outputs` was not specified.\n");
 
-	return input_wires;
+	if(!opt.nocleanup)
+		remove_directory(tempdir_name);
+
+	Pass::call(design, "design -pop");
+
+	return ret;
 }
 
 QbfSolveOptions parse_args(const std::vector<std::string> &args) {
@@ -379,6 +478,14 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) {
 			opt.assume_neg = true;
 			continue;
 		}
+		else if (args[opt.argidx] == "-nooptimize") {
+			opt.nooptimize = true;
+			continue;
+		}
+		else if (args[opt.argidx] == "-nobisection") {
+			opt.nobisection = true;
+			continue;
+		}
 		else if (args[opt.argidx] == "-sat") {
 			opt.sat = true;
 			continue;
@@ -477,6 +584,17 @@ struct QbfSatPass : public Pass {
 		log("        negative polarity signals and should always be low, for example like the\n");
 		log("        miters created with the `miter` command.\n");
 		log("\n");
+		log("    -nooptimize\n");
+		log("        Ignore \"\\minimize\" and \"\\maximize\" attributes, do not emit \"(maximize)\" or\n");
+		log("        \"(minimize)\" in the SMTLIBv2, and generally make no attempt to optimize anything.\n");
+		log("\n");
+		log("    -nobisection\n");
+		log("        If a wire is marked with the \"\\minimize\" or \"\\maximize\" attribute, do not\n");
+		log("        attempt to optimize that value with the default iterated solving and threshold\n");
+		log("        bisection approach. Instead, have yosys-smtbmc emit a \"(minimize)\" or \"(maximize)\"\n");
+		log("        command in the SMTLIBv2 output and hope that the solver supports optimizing\n");
+		log("        quantified bitvector problems.\n");
+		log("\n");
 		log("    -sat\n");
 		log("        Generate an error if the solver does not return \"sat\".\n");
 		log("\n");
@@ -519,26 +637,16 @@ struct QbfSatPass : public Pass {
 		if (!opt.specialize_from_file) {
 			//Save the design to restore after modiyfing the current module.
 			std::string module_name = module->name.str();
-			Pass::call(design, "design -push-copy");
-
-			//Replace input wires with wires assigned $allconst cells.
-			pool<std::string> input_wires = validate_design_and_get_inputs(module, opt);
-			allconstify_inputs(module, input_wires);
-			if (opt.assume_outputs)
-				assume_miter_outputs(module, opt);
 
 			QbfSolutionType ret = qbf_solve(module, opt);
-			Pass::call(design, "design -pop");
 			module = design->module(module_name);
-
-			if (ret.unknown)
+			if (ret.unknown) {
 				log_warning("solver did not give an answer\n");
-			else if (ret.sat)
+				if (opt.sat || opt.unsat)
+					log_cmd_error("expected problem to be %s\n", opt.sat? "SAT" : "UNSAT");
+			}
+			else if (ret.sat) {
 				print_qed();
-			else
-				print_proof_failed();
-
-			if(!ret.unknown && ret.sat) {
 				if (opt.write_solution) {
 					write_solution(module, ret, opt.write_soln_soln_file);
 				}
@@ -550,10 +658,11 @@ struct QbfSatPass : public Pass {
 				if (opt.unsat)
 					log_cmd_error("expected problem to be UNSAT\n");
 			}
-			else if (!ret.unknown && !ret.sat && opt.sat)
-				log_cmd_error("expected problem to be SAT\n");
-			else if (ret.unknown && (opt.sat || opt.unsat))
-				log_cmd_error("expected problem to be %s\n", opt.sat? "SAT" : "UNSAT");
+			else {
+				print_proof_failed();
+				if (opt.sat)
+					log_cmd_error("expected problem to be SAT\n");
+			}
 		} else
 			specialize_from_file(module, opt.specialize_soln_file);
 		log_pop();