qbfsat: Clean up and refactor data structures into `qbfsat.h`.

3 files changed, 266 insertions, 248 deletions

diff --git a/CODEOWNERS b/CODEOWNERS
index a73779920..350a62120 100644
--- a/CODEOWNERS
+++ b/CODEOWNERS
@@ -33,5 +33,6 @@ misc/*.py                      @btut
 backends/firrtl                @ucbjrl @azidar
 
 passes/sat/qbfsat.cc           @boqwxp
+passes/sat/qbfsat.h            @boqwxp
 passes/cmds/exec.cc            @boqwxp
 passes/cmds/printattrs.cc      @boqwxp
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc
index 136259558..e4dfcaa0c 100644
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -1,4 +1,4 @@
-/*
+/* -*- c++ -*-
  *  yosys -- Yosys Open SYnthesis Suite
  *
  *  Copyright (C) 2020  Alberto Gonzalez <boqwxp@airmail.cc>
@@ -18,13 +18,8 @@
  */
 
 #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 <algorithm>
-#include <numeric>
+#include "qbfsat.h"
 
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
@@ -36,156 +31,7 @@ static inline unsigned int difference(unsigned int a, unsigned int b) {
 		return a - b;
 }
 
-struct QbfSolutionType {
-	std::vector<std::string> stdout_lines;
-	dict<pool<std::string>, std::string> hole_to_value;
-	double solver_time;
-	bool sat;
-	bool unknown; //true if neither 'sat' nor 'unsat'
-
-	QbfSolutionType() : solver_time(0.0), 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;
-	enum Solver{Z3, Yices, CVC4} solver;
-	enum OptimizationLevel{O0, O1, O2} oflag;
-	int timeout;
-	std::string specialize_soln_file;
-	std::string write_soln_soln_file;
-	std::string dump_final_smt2_file;
-	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),
-			nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false),
-			solver(Yices), oflag(O0), timeout(0), argidx(0) {};
-};
-
-std::string get_solver_name(const QbfSolveOptions &opt) {
-	if (opt.solver == opt.Solver::Z3)
-		return "z3";
-	else if (opt.solver == opt.Solver::Yices)
-		return "yices";
-	else if (opt.solver == opt.Solver::CVC4)
-		return "cvc4";
-	else
-		log_cmd_error("unknown solver specified.\n");
-	return "";
-}
-
-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 unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED");
-	YS_REGEX_TYPE timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)");
-	YS_REGEX_TYPE timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)");
-	YS_REGEX_TYPE unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)");
-	YS_REGEX_TYPE unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver");
-	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]+");
-	YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+");
-#endif
-	YS_REGEX_MATCH_TYPE m;
-	bool sat_regex_found = false;
-	bool unsat_regex_found = false;
-	dict<std::string, bool> hole_value_recovered;
-	for (const std::string &x : sol.stdout_lines) {
-		if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) {
-			std::string loc = m[1].str();
-			std::string val = m[2].str();
-#ifndef NDEBUG
-			log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex));
-			log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex));
-#endif
-			auto locs = split_tokens(loc, "|");
-			pool<std::string> loc_pool(locs.begin(), locs.end());
-			sol.hole_to_value[loc_pool] = val;
-		}
-		else if (YS_REGEX_NS::regex_search(x, sat_regex)) {
-			sat_regex_found = true;
-			sol.sat = true;
-			sol.unknown = false;
-		}
-		else if (YS_REGEX_NS::regex_search(x, unsat_regex)) {
-			unsat_regex_found = true;
-			sol.sat = false;
-			sol.unknown = false;
-		}
-		else if (YS_REGEX_NS::regex_search(x, memout_regex)) {
-			sol.unknown = true;
-			log_warning("solver ran out of memory\n");
-		}
-		else if (YS_REGEX_NS::regex_search(x, timeout_regex)) {
-			sol.unknown = true;
-			log_warning("solver timed out\n");
-		}
-		else if (YS_REGEX_NS::regex_search(x, timeout_regex2)) {
-			sol.unknown = true;
-			log_warning("solver timed out\n");
-		}
-		else if (YS_REGEX_NS::regex_search(x, unknown_regex)) {
-			sol.unknown = true;
-			log_warning("solver returned \"unknown\"\n");
-		}
-		else if (YS_REGEX_NS::regex_search(x, unsat_regex2)) {
-			unsat_regex_found = true;
-			sol.sat = false;
-			sol.unknown = false;
-		}
-		else if (YS_REGEX_NS::regex_search(x, unknown_regex2)) {
-			sol.unknown = true;
-		}
-	}
-#ifndef NDEBUG
-	log_assert(!sol.unknown && sol.sat? sat_regex_found : true);
-	log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true);
-#endif
-}
-
-dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> get_hole_loc_idx_sigbit_map(RTLIL::Module *module, const QbfSolutionType &sol) {
-	dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit;
-	pool<RTLIL::SigBit> anyconst_sigbits;
-	dict<RTLIL::SigBit, RTLIL::SigBit> anyconst_sigbit_to_wire_sigbit;
-
-	for (auto cell : module->cells()) {
-		pool<std::string> cell_src = cell->get_strpool_attribute(ID::src);
-		auto pos = sol.hole_to_value.find(cell_src);
-		if (pos != sol.hole_to_value.end() && cell->type.in("$anyconst", "$anyseq")) {
-			RTLIL::SigSpec port_y = cell->getPort(ID::Y);
-			for (int i = GetSize(port_y) - 1; i >= 0; --i) {
-				hole_loc_idx_to_sigbit[std::make_pair(pos->first, i)] = port_y[i];
-				anyconst_sigbits.insert(port_y[i]);
-			}
-		}
-	}
-
-	for (auto &conn : module->connections()) {
-		auto lhs = conn.first;
-		auto rhs = conn.second;
-		for (auto i = 0; i < GetSize(rhs); ++i) {
-			if (anyconst_sigbits[rhs[i]]) {
-				auto pos = anyconst_sigbit_to_wire_sigbit.find(rhs[i]);
-				if (pos != anyconst_sigbit_to_wire_sigbit.end())
-					log_cmd_error("conflicting names for hole $anyconst sigbit %s\n", log_signal(rhs[i]));
-				anyconst_sigbit_to_wire_sigbit[rhs[i]] = lhs[i];
-			}
-		}
-	}
-
-	for (auto &it : hole_loc_idx_to_sigbit) {
-		auto pos = anyconst_sigbit_to_wire_sigbit.find(it.second);
-		if (pos != anyconst_sigbit_to_wire_sigbit.end())
-			it.second = pos->second;
-	}
-
-	return hole_loc_idx_to_sigbit;
-}
-
-pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
+pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, bool assume_outputs) {
 	bool found_input = false;
 	bool found_hole = false;
 	bool found_1bit_output = false;
@@ -213,48 +59,12 @@ pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const Qb
 		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)
+	if (!found_assert_assume && !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)
-		log_cmd_error("could not open solution file for writing.\n");
-
-	//There is a question here: How exactly shall we identify holes?
-	//There are at least two reasonable options:
-	//1. By the source location of the $anyconst cells
-	//2. By the name(s) of the wire(s) connected to each SigBit of the $anyconst cell->getPort(ID::Y) SigSpec.
-	//
-	//Option 1 has the benefit of being very precise.  There is very limited potential for confusion, as long
-	//as the source attribute has been set.  However, if the source attribute is not set, this won't work.
-	//More importantly, we want to have the ability to port hole assignments to other modules with compatible
-	//hole names and widths.  Obviously in those cases source locations of the $anyconst cells will not match.
-	//
-	//Option 2 has the benefits previously described, but wire names can be changed automatically by 
-	//optimization or techmapping passes, especially when (ex/im)porting from BLIF for optimization with ABC.
-	//
-	//The approach taken here is to allow both options.  We write the assignment information for each bit of
-	//the solution on a separate line.  Each line is of one of two forms:
-	//
-	//location bit name = value
-	//location bit name [offset] = value
-	//
-	//where '[', ']', and '=' are literal symbols, "location" is the $anyconst cell source location attribute,
-	//"bit" is the index of the $anyconst cell, "name" is the `wire->name` field of the SigBit corresponding
-	//to the current bit of the $anyconst cell->getPort(ID::Y), "offset" is the `offset` field of that same
-	//SigBit, and "value", which is either '0' or '1', represents the assignment for that bit.
-	dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol);
-	for (auto &x : sol.hole_to_value) {
-		std::string src_as_str = std::accumulate(x.first.begin(), x.first.end(), std::string(), [](const std::string &a, const std::string &b){return a + "|" + b;});
-		for (auto i = 0; i < GetSize(x.second); ++i)
-			fout << src_as_str.c_str() << " " << i << " " << log_signal(hole_loc_idx_to_sigbit[std::make_pair(x.first, i)]) << " = " << x.second[GetSize(x.second) - 1 - i] << std::endl;
-	}
-}
-
 void specialize_from_file(RTLIL::Module *module, const std::string &file) {
 	YS_REGEX_TYPE hole_bit_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) \\[([0-9]+)] = ([01])$");
 	YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) = ([01])$"); //if no index specified
@@ -318,7 +128,7 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) {
 }
 
 void specialize(RTLIL::Module *module, const QbfSolutionType &sol, bool quiet = false) {
-	dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol);
+	auto hole_loc_idx_to_sigbit = sol.get_hole_loc_idx_sigbit_map(module);
 	pool<RTLIL::Cell *> anyconsts_to_remove;
 	for (auto cell : module->cells())
 		if (cell->type == "$anyconst")
@@ -348,24 +158,6 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol, bool quiet =
 	}
 }
 
-void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) {
-	log("Satisfiable model:\n");
-	dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol);
-	for (auto &it : sol.hole_to_value) {
-		pool<std::string> hole_loc = it.first;
-		std::string hole_value = it.second;
-
-		for (unsigned int i = 0; i < hole_value.size(); ++i) {
-			int bit_idx = GetSize(hole_value) - 1 - i;
-			auto it = hole_loc_idx_to_sigbit.find(std::make_pair(hole_loc, i));
-			log_assert(it != hole_loc_idx_to_sigbit.end());
-
-			RTLIL::SigBit hole_sigbit = it->second;
-			log("\t%s = 1'b%c\n", log_signal(hole_sigbit), hole_value[bit_idx]);
-		}
-	}
-}
-
 void allconstify_inputs(RTLIL::Module *module, const pool<std::string> &input_wires) {
 	for (auto &n : input_wires) {
 		RTLIL::Wire *input = module->wire(n);
@@ -383,7 +175,7 @@ void allconstify_inputs(RTLIL::Module *module, const pool<std::string> &input_wi
 	module->fixup_ports();
 }
 
-void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
+void assume_miter_outputs(RTLIL::Module *module, bool assume_neg) {
 	std::vector<RTLIL::Wire *> wires_to_assume;
 	for (auto w : module->wires())
 		if (w->port_output && w->width == 1)
@@ -398,7 +190,7 @@ void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
 		log("\n");
 	}
 
-	if (opt.assume_neg) {
+	if (assume_neg) {
 		for (unsigned int i = 0; i < wires_to_assume.size(); ++i) {
 			RTLIL::SigSpec n_wire = module->LogicNot(wires_to_assume[i]->name.str() + "__n__qbfsat", wires_to_assume[i], false, wires_to_assume[i]->get_src_attribute());
 			wires_to_assume[i] = n_wire.as_wire();
@@ -430,7 +222,7 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt,
 	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_warning = "z3: WARNING:";
-	const std::string smtbmc_cmd = yosys_smtbmc_exe + " -s " + (get_solver_name(opt)) + (opt.timeout != 0? stringf(" --timeout %d", opt.timeout) : "") + " -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_cmd = yosys_smtbmc_exe + " -s " + (opt.get_solver_name()) + (opt.timeout != 0? stringf(" --timeout %d", opt.timeout) : "") + " -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";
 
 	Pass::call(mod->design, smt2_command);
 
@@ -451,7 +243,7 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt,
 	ret.solver_time = (end - begin) / 1e9f;
 	if (!quiet) log("Solver finished in %.3f seconds.\n", ret.solver_time);
 
-	recover_solution(ret);
+	ret.recover_solution();
 	return ret;
 }
 
@@ -468,10 +260,10 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
 	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);
+	pool<std::string> input_wires = validate_design_and_get_inputs(module, opt.assume_outputs);
 	allconstify_inputs(module, input_wires);
 	if (opt.assume_outputs)
-		assume_miter_outputs(module, opt);
+		assume_miter_outputs(module, opt.assume_neg);
 
 	//Find the wire to be optimized, if any:
 	for (auto wire : module->wires()) {
@@ -699,33 +491,6 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) {
 	return opt;
 }
 
-void print_proof_failed()
-{
-	log("\n");
-	log("   ______                   ___       ___       _ _            _ _ \n");
-	log("  (_____ \\                 / __)     / __)     (_) |          | | |\n");
-	log("   _____) )___ ___   ___ _| |__    _| |__ _____ _| | _____  __| | |\n");
-	log("  |  ____/ ___) _ \\ / _ (_   __)  (_   __|____ | | || ___ |/ _  |_|\n");
-	log("  | |   | |  | |_| | |_| || |       | |  / ___ | | || ____( (_| |_ \n");
-	log("  |_|   |_|   \\___/ \\___/ |_|       |_|  \\_____|_|\\_)_____)\\____|_|\n");
-	log("\n");
-}
-
-void print_qed()
-{
-	log("\n");
-	log("                  /$$$$$$      /$$$$$$$$     /$$$$$$$    \n");
-	log("                 /$$__  $$    | $$_____/    | $$__  $$   \n");
-	log("                | $$  \\ $$    | $$          | $$  \\ $$   \n");
-	log("                | $$  | $$    | $$$$$       | $$  | $$   \n");
-	log("                | $$  | $$    | $$__/       | $$  | $$   \n");
-	log("                | $$/$$ $$    | $$          | $$  | $$   \n");
-	log("                |  $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
-	log("                 \\____ $$$|__/|________/|__/|_______/|__/\n");
-	log("                       \\__/                              \n");
-	log("\n");
-}
-
 struct QbfSatPass : public Pass {
 	QbfSatPass() : Pass("qbfsat", "solve a 2QBF-SAT problem in the circuit") { }
 	void help() override
@@ -827,12 +592,12 @@ struct QbfSatPass : public Pass {
 			else if (ret.sat) {
 				print_qed();
 				if (opt.write_solution) {
-					write_solution(module, ret, opt.write_soln_soln_file);
+					ret.write_solution(module, opt.write_soln_soln_file);
 				}
 				if (opt.specialize) {
 					specialize(module, ret);
 				} else {
-					dump_model(module, ret);
+					ret.dump_model(module);
 				}
 				if (opt.unsat)
 					log_cmd_error("expected problem to be UNSAT\n");
diff --git a/passes/sat/qbfsat.h b/passes/sat/qbfsat.h
new file mode 100644
index 000000000..401f9c7a6
--- /dev/null
+++ b/passes/sat/qbfsat.h
@@ -0,0 +1,252 @@
+/* -*- c++ -*-
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2020  Alberto Gonzalez <boqwxp@airmail.cc>
+ *
+ *  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 QBFSAT_H
+#define QBFSAT_H
+
+#include "kernel/yosys.h"
+#include <numeric>
+
+YOSYS_NAMESPACE_BEGIN
+
+struct QbfSolveOptions {
+	bool specialize = false, specialize_from_file = false, write_solution = false, nocleanup = false;
+	bool dump_final_smt2 = false, assume_outputs = false, assume_neg = false, nooptimize = false;
+	bool nobisection = false, sat = false, unsat = false, show_smtbmc = false;
+	enum Solver{Z3, Yices, CVC4} solver = Yices;
+	enum OptimizationLevel{O0, O1, O2} oflag = O0;
+	int timeout = 0;
+	std::string specialize_soln_file = "";
+	std::string write_soln_soln_file = "";
+	std::string dump_final_smt2_file = "";
+	size_t argidx = 0;
+
+	std::string get_solver_name() const {
+		if (solver == Solver::Z3)
+			return "z3";
+		else if (solver == Solver::Yices)
+			return "yices";
+		else if (solver == Solver::CVC4)
+			return "cvc4";
+
+		log_cmd_error("unknown solver specified.\n");
+		return "";
+	}
+};
+
+struct QbfSolutionType {
+	std::vector<std::string> stdout_lines = {};
+	dict<pool<std::string>, std::string> hole_to_value = {};
+	double solver_time = 0;
+	bool sat = false;
+	bool unknown = true; //true if neither 'sat' nor 'unsat'
+
+	dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> get_hole_loc_idx_sigbit_map(RTLIL::Module *module) const {
+		dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit;
+		pool<RTLIL::SigBit> anyconst_sigbits;
+		dict<RTLIL::SigBit, RTLIL::SigBit> anyconst_sigbit_to_wire_sigbit;
+
+		for (auto cell : module->cells()) {
+			pool<std::string> cell_src = cell->get_strpool_attribute(ID::src);
+			auto pos = hole_to_value.find(cell_src);
+			if (pos != hole_to_value.end() && cell->type.in("$anyconst", "$anyseq")) {
+				RTLIL::SigSpec port_y = cell->getPort(ID::Y);
+				for (int i = GetSize(port_y) - 1; i >= 0; --i) {
+					hole_loc_idx_to_sigbit[std::make_pair(pos->first, i)] = port_y[i];
+					anyconst_sigbits.insert(port_y[i]);
+				}
+			}
+		}
+
+		for (auto &conn : module->connections()) {
+			auto lhs = conn.first;
+			auto rhs = conn.second;
+			for (auto i = 0; i < GetSize(rhs); ++i) {
+				if (anyconst_sigbits[rhs[i]]) {
+					auto pos = anyconst_sigbit_to_wire_sigbit.find(rhs[i]);
+					if (pos != anyconst_sigbit_to_wire_sigbit.end())
+						log_cmd_error("conflicting names for hole $anyconst sigbit %s\n", log_signal(rhs[i]));
+					anyconst_sigbit_to_wire_sigbit[rhs[i]] = lhs[i];
+				}
+			}
+		}
+
+		for (auto &it : hole_loc_idx_to_sigbit) {
+			auto pos = anyconst_sigbit_to_wire_sigbit.find(it.second);
+			if (pos != anyconst_sigbit_to_wire_sigbit.end())
+				it.second = pos->second;
+		}
+
+		return hole_loc_idx_to_sigbit;
+	}
+
+	void dump_model(RTLIL::Module *module) const {
+		log("Satisfiable model:\n");
+		auto hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module);
+		for (auto &it : hole_to_value) {
+			pool<std::string> hole_loc = it.first;
+			std::string hole_value = it.second;
+
+			for (unsigned int i = 0; i < hole_value.size(); ++i) {
+				int bit_idx = GetSize(hole_value) - 1 - i;
+				auto it = hole_loc_idx_to_sigbit.find(std::make_pair(hole_loc, i));
+				log_assert(it != hole_loc_idx_to_sigbit.end());
+
+				RTLIL::SigBit hole_sigbit = it->second;
+				log("\t%s = 1'b%c\n", log_signal(hole_sigbit), hole_value[bit_idx]);
+			}
+		}
+	}
+
+	void write_solution(RTLIL::Module *module, const std::string &file) const {
+		std::ofstream fout(file.c_str());
+		if (!fout)
+			log_cmd_error("could not open solution file for writing.\n");
+
+		//There is a question here: How exactly shall we identify holes?
+		//There are at least two reasonable options:
+		//1. By the source location of the $anyconst cells
+		//2. By the name(s) of the wire(s) connected to each SigBit of the $anyconst cell->getPort(ID::Y) SigSpec.
+		//
+		//Option 1 has the benefit of being very precise.  There is very limited potential for confusion, as long
+		//as the source attribute has been set.  However, if the source attribute is not set, this won't work.
+		//More importantly, we want to have the ability to port hole assignments to other modules with compatible
+		//hole names and widths.  Obviously in those cases source locations of the $anyconst cells will not match.
+		//
+		//Option 2 has the benefits previously described, but wire names can be changed automatically by 
+		//optimization or techmapping passes, especially when (ex/im)porting from BLIF for optimization with ABC.
+		//
+		//The approach taken here is to allow both options.  We write the assignment information for each bit of
+		//the solution on a separate line.  Each line is of one of two forms:
+		//
+		//location bit name = value
+		//location bit name [offset] = value
+		//
+		//where '[', ']', and '=' are literal symbols, "location" is the $anyconst cell source location attribute,
+		//"bit" is the index of the $anyconst cell, "name" is the `wire->name` field of the SigBit corresponding
+		//to the current bit of the $anyconst cell->getPort(ID::Y), "offset" is the `offset` field of that same
+		//SigBit, and "value", which is either '0' or '1', represents the assignment for that bit.
+		auto hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module);
+		for (auto &x : hole_to_value) {
+			std::string src_as_str = std::accumulate(x.first.begin(), x.first.end(), std::string(), [](const std::string &a, const std::string &b){return a + "|" + b;});
+			for (auto i = 0; i < GetSize(x.second); ++i)
+				fout << src_as_str.c_str() << " " << i << " " << log_signal(hole_loc_idx_to_sigbit[std::make_pair(x.first, i)]) << " = " << x.second[GetSize(x.second) - 1 - i] << std::endl;
+		}
+	}
+
+	void recover_solution() {
+		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 unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED");
+		YS_REGEX_TYPE timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)");
+		YS_REGEX_TYPE timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)");
+		YS_REGEX_TYPE unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)");
+		YS_REGEX_TYPE unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver");
+		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]+");
+		YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+");
+#endif
+		YS_REGEX_MATCH_TYPE m;
+		bool sat_regex_found = false;
+		bool unsat_regex_found = false;
+		dict<std::string, bool> hole_value_recovered;
+		for (const std::string &x : stdout_lines) {
+			if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) {
+				std::string loc = m[1].str();
+				std::string val = m[2].str();
+#ifndef NDEBUG
+				log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex));
+				log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex));
+#endif
+				auto locs = split_tokens(loc, "|");
+				pool<std::string> loc_pool(locs.begin(), locs.end());
+				hole_to_value[loc_pool] = val;
+			}
+			else if (YS_REGEX_NS::regex_search(x, sat_regex)) {
+				sat_regex_found = true;
+				sat = true;
+				unknown = false;
+			}
+			else if (YS_REGEX_NS::regex_search(x, unsat_regex)) {
+				unsat_regex_found = true;
+				sat = false;
+				unknown = false;
+			}
+			else if (YS_REGEX_NS::regex_search(x, memout_regex)) {
+				unknown = true;
+				log_warning("solver ran out of memory\n");
+			}
+			else if (YS_REGEX_NS::regex_search(x, timeout_regex)) {
+				unknown = true;
+				log_warning("solver timed out\n");
+			}
+			else if (YS_REGEX_NS::regex_search(x, timeout_regex2)) {
+				unknown = true;
+				log_warning("solver timed out\n");
+			}
+			else if (YS_REGEX_NS::regex_search(x, unknown_regex)) {
+				unknown = true;
+				log_warning("solver returned \"unknown\"\n");
+			}
+			else if (YS_REGEX_NS::regex_search(x, unsat_regex2)) {
+				unsat_regex_found = true;
+				sat = false;
+				unknown = false;
+			}
+			else if (YS_REGEX_NS::regex_search(x, unknown_regex2)) {
+				unknown = true;
+			}
+		}
+		log_assert(!unknown && sat? sat_regex_found : true);
+		log_assert(!unknown && !sat? unsat_regex_found : true);
+	}
+};
+
+void print_proof_failed()
+{
+	log("\n");
+	log("   ______                   ___       ___       _ _            _ _ \n");
+	log("  (_____ \\                 / __)     / __)     (_) |          | | |\n");
+	log("   _____) )___ ___   ___ _| |__    _| |__ _____ _| | _____  __| | |\n");
+	log("  |  ____/ ___) _ \\ / _ (_   __)  (_   __|____ | | || ___ |/ _  |_|\n");
+	log("  | |   | |  | |_| | |_| || |       | |  / ___ | | || ____( (_| |_ \n");
+	log("  |_|   |_|   \\___/ \\___/ |_|       |_|  \\_____|_|\\_)_____)\\____|_|\n");
+	log("\n");
+}
+
+void print_qed()
+{
+	log("\n");
+	log("                  /$$$$$$      /$$$$$$$$     /$$$$$$$    \n");
+	log("                 /$$__  $$    | $$_____/    | $$__  $$   \n");
+	log("                | $$  \\ $$    | $$          | $$  \\ $$   \n");
+	log("                | $$  | $$    | $$$$$       | $$  | $$   \n");
+	log("                | $$  | $$    | $$__/       | $$  | $$   \n");
+	log("                | $$/$$ $$    | $$          | $$  | $$   \n");
+	log("                |  $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
+	log("                 \\____ $$$|__/|________/|__/|_______/|__/\n");
+	log("                       \\__/                              \n");
+	log("\n");
+}
+
+YOSYS_NAMESPACE_END
+
+#endif