Refactor common parts of SAT-using optimizations into a helper.

This also aligns the functionality:

- in all cases, the onehot attribute is used to create appropriate
  constraints (previously, opt_dff didn't do it at all, and share
  created one-hot constraints based on $pmux presence alone, which
  is unsound)
- in all cases, shift and mul/div/pow cells are now skipped when
  importing the SAT problem (previously only memory_share did this)
  — this avoids creating clauses for hard cells that are unlikely
  to help with proving the UNSATness needed for optimization

7 files changed, 224 insertions, 153 deletions

diff --git a/Makefile b/Makefile
index 8a7d938df..4e13da31c 100644
--- a/Makefile
+++ b/Makefile
@@ -575,6 +575,7 @@ $(eval $(call add_include_file,kernel/modtools.h))
 $(eval $(call add_include_file,kernel/macc.h))
 $(eval $(call add_include_file,kernel/utils.h))
 $(eval $(call add_include_file,kernel/satgen.h))
+$(eval $(call add_include_file,kernel/qcsat.h))
 $(eval $(call add_include_file,kernel/ff.h))
 $(eval $(call add_include_file,kernel/ffinit.h))
 $(eval $(call add_include_file,kernel/mem.h))
@@ -599,7 +600,7 @@ ifneq ($(ABCEXTERNAL),)
 kernel/yosys.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"'
 endif
 endif
-OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/mem.o kernel/ffmerge.o
+OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o
 
 kernel/log.o: CXXFLAGS += -DYOSYS_SRC='"$(YOSYS_SRC)"'
 kernel/yosys.o: CXXFLAGS += -DYOSYS_DATDIR='"$(DATDIR)"' -DYOSYS_PROGRAM_PREFIX='"$(PROGRAM_PREFIX)"'
diff --git a/kernel/modtools.h b/kernel/modtools.h
index bd393b5d5..4cbaf78d0 100644
--- a/kernel/modtools.h
+++ b/kernel/modtools.h
@@ -380,9 +380,11 @@ struct ModWalker
 		}
 	}
 
-	ModWalker(RTLIL::Design *design) : design(design), module(NULL)
+	ModWalker(RTLIL::Design *design, RTLIL::Module *module = nullptr) : design(design), module(NULL)
 	{
-            ct.setup(design);
+		ct.setup(design);
+		if (module)
+			setup(module);
 	}
 
 	void setup(RTLIL::Module *module, CellTypes *filter_ct = NULL)
diff --git a/kernel/qcsat.cc b/kernel/qcsat.cc
new file mode 100644
index 000000000..b7da958db
--- /dev/null
+++ b/kernel/qcsat.cc
@@ -0,0 +1,102 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2021  Marcelina Kościelnicka <mwk@0x04.net>
+ *
+ *  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.
+ *
+ */
+
+#include "kernel/qcsat.h"
+
+USING_YOSYS_NAMESPACE
+
+std::vector<int> QuickConeSat::importSig(SigSpec sig)
+{
+	sig = modwalker.sigmap(sig);
+	for (auto bit : sig)
+		bits_queue.insert(bit);
+	return satgen.importSigSpec(sig);
+}
+
+int QuickConeSat::importSigBit(SigBit bit)
+{
+	bit = modwalker.sigmap(bit);
+	bits_queue.insert(bit);
+	return satgen.importSigBit(bit);
+}
+
+void QuickConeSat::prepare()
+{
+	while (!bits_queue.empty())
+	{
+		pool<ModWalker::PortBit> portbits;
+		modwalker.get_drivers(portbits, bits_queue);
+
+		for (auto bit : bits_queue)
+			if (bit.wire && bit.wire->get_bool_attribute(ID::onehot) && !imported_onehot.count(bit.wire))
+			{
+				std::vector<int> bits = satgen.importSigSpec(bit.wire);
+				for (int i : bits)
+				for (int j : bits)
+					if (i != j)
+						ez->assume(ez->NOT(i), j);
+				imported_onehot.insert(bit.wire);
+			}
+
+		bits_queue.clear();
+
+		for (auto &pbit : portbits)
+		{
+			if (imported_cells.count(pbit.cell))
+				continue;
+			if (cell_complexity(pbit.cell) > max_cell_complexity)
+				continue;
+			if (max_cell_outs && GetSize(modwalker.cell_outputs[pbit.cell]) > max_cell_outs)
+				continue;
+			auto &inputs = modwalker.cell_inputs[pbit.cell];
+			bits_queue.insert(inputs.begin(), inputs.end());
+			satgen.importCell(pbit.cell);
+			imported_cells.insert(pbit.cell);
+		}
+
+		if (max_cell_count && GetSize(imported_cells) > max_cell_count)
+			break;
+	}
+}
+
+int QuickConeSat::cell_complexity(RTLIL::Cell *cell)
+{
+	if (cell->type.in(ID($concat), ID($slice), ID($pos), ID($_BUF_)))
+		return 0;
+	if (cell->type.in(ID($not), ID($and), ID($or), ID($xor), ID($xnor),
+			ID($reduce_and), ID($reduce_or), ID($reduce_xor),
+			ID($reduce_xnor), ID($reduce_bool),
+			ID($logic_not), ID($logic_and), ID($logic_or),
+			ID($eq), ID($ne), ID($eqx), ID($nex), ID($fa),
+			ID($mux), ID($pmux), ID($lut), ID($sop),
+			ID($_NOT_), ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_),
+			ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_),
+			ID($_MUX_), ID($_NMUX_), ID($_MUX4_), ID($_MUX8_), ID($_MUX16_),
+			ID($_AOI3_), ID($_OAI3_), ID($_AOI4_), ID($_OAI4_)))
+		return 1;
+	if (cell->type.in(ID($neg), ID($add), ID($sub), ID($alu), ID($lcu),
+			ID($lt), ID($le), ID($gt), ID($ge)))
+		return 2;
+	if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)))
+		return 3;
+	if (cell->type.in(ID($mul), ID($macc), ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($pow)))
+		return 4;
+	// Unknown cell.
+	return 5;
+}
diff --git a/kernel/qcsat.h b/kernel/qcsat.h
new file mode 100644
index 000000000..e4d3c3c5d
--- /dev/null
+++ b/kernel/qcsat.h
@@ -0,0 +1,76 @@
+/* -*- c++ -*-
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2021  Marcelina Kościelnicka <mwk@0x04.net>
+ *
+ *  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 QCSAT_H
+#define QCSAT_H
+
+#include "kernel/satgen.h"
+#include "kernel/modtools.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+// This is a helper class meant for easy construction of quick SAT queries
+// to a combinatorial input cone of some set of signals, meant for SAT-based
+// optimizations.  Various knobs are provided to set just how much of the
+// cone should be included in the model — since this class is meant for
+// optimization, it should not be a correctness problem when some cells are
+// skipped and the solver spuriously returns SAT with a solution that
+// cannot exist in reality due to skipped constraints (ie. only UNSAT results
+// from this class should be considered binding).
+struct QuickConeSat {
+	ModWalker &modwalker;
+	ezSatPtr ez;
+	SatGen satgen;
+
+	// The effort level knobs.
+
+	// The maximum "complexity level" of cells that will be imported.
+	// - 1: bitwise operations, muxes, equality comparisons, lut, sop, fa
+	// - 2: addition, subtraction, greater/less than comparisons, lcu
+	// - 3: shifts
+	// - 4: multiplication, division, power
+	int max_cell_complexity = 2;
+	// The maximum number of cells to import, or 0 for no limit.
+	int max_cell_count = 0;
+	// If non-0, skip importing cells with more than this number of output bits.
+	int max_cell_outs = 0;
+
+	// Internal state.
+	pool<RTLIL::Cell*> imported_cells;
+	pool<RTLIL::Wire*> imported_onehot;
+	pool<RTLIL::SigBit> bits_queue;
+
+	QuickConeSat(ModWalker &modwalker) : modwalker(modwalker), ez(), satgen(ez.get(), &modwalker.sigmap) {}
+
+	// Imports a signal into the SAT solver, queues its input cone to be
+	// imported in the next prepare() call.
+	std::vector<int> importSig(SigSpec sig);
+	int importSigBit(SigBit bit);
+
+	// Imports the input cones of all previously importSig'd signals into
+	// the SAT solver.
+	void prepare();
+
+	// Returns the "complexity level" of a given cell.
+	static int cell_complexity(RTLIL::Cell *cell);
+};
+
+YOSYS_NAMESPACE_END
+
+#endif
diff --git a/passes/memory/memory_share.cc b/passes/memory/memory_share.cc
index 4e6a30ef1..91f36ce05 100644
--- a/passes/memory/memory_share.cc
+++ b/passes/memory/memory_share.cc
@@ -18,7 +18,7 @@
  */
 
 #include "kernel/yosys.h"
-#include "kernel/satgen.h"
+#include "kernel/qcsat.h"
 #include "kernel/sigtools.h"
 #include "kernel/modtools.h"
 #include "kernel/mem.h"
@@ -32,7 +32,6 @@ struct MemoryShareWorker
 	RTLIL::Module *module;
 	SigMap sigmap, sigmap_xmux;
 	ModWalker modwalker;
-	CellTypes cone_ct;
 	bool flag_widen;
 
 
@@ -358,56 +357,20 @@ struct MemoryShareWorker
 
 			// Okay, time to actually run the SAT solver.
 
-			ezSatPtr ez;
-			SatGen satgen(ez.get(), &modwalker.sigmap);
+			QuickConeSat qcsat(modwalker);
 
 			// create SAT representation of common input cone of all considered EN signals
 
-			pool<Wire*> one_hot_wires;
-			std::set<RTLIL::Cell*> sat_cells;
-			std::set<RTLIL::SigBit> bits_queue;
 			dict<int, int> port_to_sat_variable;
 
-			for (auto idx : group) {
-				RTLIL::SigSpec sig = modwalker.sigmap(mem.wr_ports[idx].en);
-				port_to_sat_variable[idx] = ez->expression(ez->OpOr, satgen.importSigSpec(sig));
-
-				std::vector<RTLIL::SigBit> bits = sig;
-				bits_queue.insert(bits.begin(), bits.end());
-			}
-
-			while (!bits_queue.empty())
-			{
-				for (auto bit : bits_queue)
-					if (bit.wire && bit.wire->get_bool_attribute(ID::onehot))
-						one_hot_wires.insert(bit.wire);
-
-				pool<ModWalker::PortBit> portbits;
-				modwalker.get_drivers(portbits, bits_queue);
-				bits_queue.clear();
-
-				for (auto &pbit : portbits)
-					if (sat_cells.count(pbit.cell) == 0 && cone_ct.cell_known(pbit.cell->type)) {
-						pool<RTLIL::SigBit> &cell_inputs = modwalker.cell_inputs[pbit.cell];
-						bits_queue.insert(cell_inputs.begin(), cell_inputs.end());
-						sat_cells.insert(pbit.cell);
-					}
-			}
-
-			for (auto wire : one_hot_wires) {
-				log("  Adding one-hot constraint for wire %s.\n", log_id(wire));
-				vector<int> ez_wire_bits = satgen.importSigSpec(wire);
-				for (int i : ez_wire_bits)
-				for (int j : ez_wire_bits)
-					if (i != j) ez->assume(ez->NOT(i), j);
-			}
+			for (auto idx : group)
+				port_to_sat_variable[idx] = qcsat.ez->expression(qcsat.ez->OpOr, qcsat.importSig(mem.wr_ports[idx].en));
 
-			log("  Common input cone for all EN signals: %d cells.\n", int(sat_cells.size()));
+			qcsat.prepare();
 
-			for (auto cell : sat_cells)
-				satgen.importCell(cell);
+			log("  Common input cone for all EN signals: %d cells.\n", GetSize(qcsat.imported_cells));
 
-			log("  Size of unconstrained SAT problem: %d variables, %d clauses\n", ez->numCnfVariables(), ez->numCnfClauses());
+			log("  Size of unconstrained SAT problem: %d variables, %d clauses\n", qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses());
 
 			// now try merging the ports.
 
@@ -422,14 +385,14 @@ struct MemoryShareWorker
 					if (port2.removed)
 						continue;
 
-					if (ez->solve(port_to_sat_variable.at(idx1), port_to_sat_variable.at(idx2))) {
+					if (qcsat.ez->solve(port_to_sat_variable.at(idx1), port_to_sat_variable.at(idx2))) {
 						log("  According to SAT solver sharing of port %d with port %d is not possible.\n", idx1, idx2);
 						continue;
 					}
 
 					log("  Merging port %d into port %d.\n", idx2, idx1);
 					mem.prepare_wr_merge(idx1, idx2);
-					port_to_sat_variable.at(idx1) = ez->OR(port_to_sat_variable.at(idx1), port_to_sat_variable.at(idx2));
+					port_to_sat_variable.at(idx1) = qcsat.ez->OR(port_to_sat_variable.at(idx1), port_to_sat_variable.at(idx2));
 
 					RTLIL::SigSpec last_addr = port1.addr;
 					RTLIL::SigSpec last_data = port1.data;
@@ -511,21 +474,7 @@ struct MemoryShareWorker
 			while (consolidate_wr_by_addr(mem));
 		}
 
-		cone_ct.setup_internals();
-		cone_ct.cell_types.erase(ID($mul));
-		cone_ct.cell_types.erase(ID($mod));
-		cone_ct.cell_types.erase(ID($div));
-		cone_ct.cell_types.erase(ID($modfloor));
-		cone_ct.cell_types.erase(ID($divfloor));
-		cone_ct.cell_types.erase(ID($pow));
-		cone_ct.cell_types.erase(ID($shl));
-		cone_ct.cell_types.erase(ID($shr));
-		cone_ct.cell_types.erase(ID($sshl));
-		cone_ct.cell_types.erase(ID($sshr));
-		cone_ct.cell_types.erase(ID($shift));
-		cone_ct.cell_types.erase(ID($shiftx));
-
-		modwalker.setup(module, &cone_ct);
+		modwalker.setup(module);
 
 		for (auto &mem : memories)
 			consolidate_wr_using_sat(mem);
diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc
index 94d6d5443..ddf08392b 100644
--- a/passes/opt/opt_dff.cc
+++ b/passes/opt/opt_dff.cc
@@ -21,7 +21,8 @@
 #include "kernel/log.h"
 #include "kernel/register.h"
 #include "kernel/rtlil.h"
-#include "kernel/satgen.h"
+#include "kernel/qcsat.h"
+#include "kernel/modtools.h"
 #include "kernel/sigtools.h"
 #include "kernel/ffinit.h"
 #include "kernel/ff.h"
@@ -51,26 +52,23 @@ struct OptDffWorker
 	FfInitVals initvals;
 	dict<SigBit, int> bitusers;
 	dict<SigBit, cell_int_t> bit2mux;
-	dict<SigBit, RTLIL::Cell*> bit2driver;
 
 	typedef std::map<RTLIL::SigBit, bool> pattern_t;
 	typedef std::set<pattern_t> patterns_t;
 	typedef std::pair<RTLIL::SigBit, bool> ctrl_t;
 	typedef std::set<ctrl_t> ctrls_t;
 
-	ezSatPtr ez;
-	SatGen satgen;
-	pool<Cell*> sat_cells;
+	ModWalker modwalker;
+	QuickConeSat qcsat;
 
 	// Used as a queue.
 	std::vector<Cell *> dff_cells;
 
-	OptDffWorker(const OptDffOptions &opt, Module *mod) : opt(opt), module(mod), sigmap(mod), initvals(&sigmap, mod), ez(), satgen(ez.get(), &sigmap) {
-		// Gathering three kinds of information here for every sigmapped SigBit:
+	OptDffWorker(const OptDffOptions &opt, Module *mod) : opt(opt), module(mod), sigmap(mod), initvals(&sigmap, mod), modwalker(module->design, module), qcsat(modwalker) {
+		// Gathering two kinds of information here for every sigmapped SigBit:
 		//
 		// - bitusers: how many users it has (muxes will only be merged into FFs if this is 1, making the FF the only user)
 		// - bit2mux: the mux cell and bit index that drives it, if any
-		// - bit2driver: the cell driving it, if any
 
 		for (auto wire : module->wires())
 		{
@@ -88,10 +86,6 @@ struct OptDffWorker
 
 			for (auto conn : cell->connections()) {
 				bool is_output = cell->output(conn.first);
-				if (is_output) {
-					for (auto bit : sigmap(conn.second))
-						bit2driver[bit] = cell;
-				}
 				if (!is_output || !cell->known()) {
 					for (auto bit : sigmap(conn.second))
 						bitusers[bit]++;
@@ -104,20 +98,6 @@ struct OptDffWorker
 
 	}
 
-	std::function<void(Cell*)> sat_import_cell = [&](Cell *c) {
-		if (!sat_cells.insert(c).second)
-			return;
-		if (!satgen.importCell(c))
-			return;
-		for (auto &conn : c->connections()) {
-			if (!c->input(conn.first))
-				continue;
-			for (auto bit : sigmap(conn.second))
-				if (bit2driver.count(bit))
-					sat_import_cell(bit2driver.at(bit));
-		}
-	};
-
 	State combine_const(State a, State b) {
 		if (a == State::Sx && !opt.keepdc)
 			return b;
@@ -594,19 +574,19 @@ struct OptDffWorker
 						if (!opt.sat)
 							continue;
 						// For each register bit, try to prove that it cannot change from the initial value. If so, remove it
-						if (!bit2driver.count(ff.sig_d[i]))
+						if (!modwalker.has_drivers(ff.sig_d.extract(i)))
 							continue;
 						if (val != State::S0 && val != State::S1)
 							continue;
 
-						sat_import_cell(bit2driver.at(ff.sig_d[i]));
+						int init_sat_pi = qcsat.importSigBit(val);
+						int q_sat_pi = qcsat.importSigBit(ff.sig_q[i]);
+						int d_sat_pi = qcsat.importSigBit(ff.sig_d[i]);
 
-						int init_sat_pi = satgen.importSigSpec(val).front();
-						int q_sat_pi = satgen.importSigBit(ff.sig_q[i]);
-						int d_sat_pi = satgen.importSigBit(ff.sig_d[i]);
+						qcsat.prepare();
 
 						// Try to find out whether the register bit can change under some circumstances
-						bool counter_example_found = ez->solve(ez->IFF(q_sat_pi, init_sat_pi), ez->NOT(ez->IFF(d_sat_pi, init_sat_pi)));
+						bool counter_example_found = qcsat.ez->solve(qcsat.ez->IFF(q_sat_pi, init_sat_pi), qcsat.ez->NOT(qcsat.ez->IFF(d_sat_pi, init_sat_pi)));
 
 						// If the register bit cannot change, we can replace it with a constant
 						if (counter_example_found)
diff --git a/passes/opt/share.cc b/passes/opt/share.cc
index 88c4dee8b..ee1acfb7f 100644
--- a/passes/opt/share.cc
+++ b/passes/opt/share.cc
@@ -18,7 +18,7 @@
  */
 
 #include "kernel/yosys.h"
-#include "kernel/satgen.h"
+#include "kernel/qcsat.h"
 #include "kernel/sigtools.h"
 #include "kernel/modtools.h"
 #include "kernel/utils.h"
@@ -58,8 +58,6 @@ struct ShareWorker
 	std::map<RTLIL::Cell*, std::set<RTLIL::Cell*, cell_ptr_cmp>, cell_ptr_cmp> topo_cell_drivers;
 	std::map<RTLIL::SigBit, std::set<RTLIL::Cell*, cell_ptr_cmp>> topo_bit_drivers;
 
-	std::vector<std::pair<RTLIL::SigBit, RTLIL::SigBit>> exclusive_ctrls;
-
 
 	// ------------------------------------------------------------------------------
 	// Find terminal bits -- i.e. bits that do not (exclusively) feed into a mux tree
@@ -1156,7 +1154,6 @@ struct ShareWorker
 		recursion_state.clear();
 		topo_cell_drivers.clear();
 		topo_bit_drivers.clear();
-		exclusive_ctrls.clear();
 		terminal_bits.clear();
 		shareable_cells.clear();
 		forbidden_controls_cache.clear();
@@ -1171,13 +1168,6 @@ struct ShareWorker
 		log("Found %d cells in module %s that may be considered for resource sharing.\n",
 				GetSize(shareable_cells), log_id(module));
 
-		for (auto cell : module->cells())
-			if (cell->type == ID($pmux))
-				for (auto bit : cell->getPort(ID::S))
-				for (auto other_bit : cell->getPort(ID::S))
-					if (bit < other_bit)
-						exclusive_ctrls.push_back(std::pair<RTLIL::SigBit, RTLIL::SigBit>(bit, other_bit));
-
 		while (!shareable_cells.empty() && config.limit != 0)
 		{
 			RTLIL::Cell *cell = *shareable_cells.begin();
@@ -1256,8 +1246,11 @@ struct ShareWorker
 				optimize_activation_patterns(filtered_cell_activation_patterns);
 				optimize_activation_patterns(filtered_other_cell_activation_patterns);
 
-				ezSatPtr ez;
-				SatGen satgen(ez.get(), &modwalker.sigmap);
+				QuickConeSat qcsat(modwalker);
+				if (config.opt_fast) {
+					qcsat.max_cell_outs = 3;
+					qcsat.max_cell_count = 100;
+				}
 
 				pool<RTLIL::Cell*> sat_cells;
 				std::set<RTLIL::SigBit> bits_queue;
@@ -1267,77 +1260,45 @@ struct ShareWorker
 
 				for (auto &p : filtered_cell_activation_patterns) {
 					log("      Activation pattern for cell %s: %s = %s\n", log_id(cell), log_signal(p.first), log_signal(p.second));
-					cell_active.push_back(ez->vec_eq(satgen.importSigSpec(p.first), satgen.importSigSpec(p.second)));
+					cell_active.push_back(qcsat.ez->vec_eq(qcsat.importSig(p.first), qcsat.importSig(p.second)));
 					all_ctrl_signals.append(p.first);
 				}
 
 				for (auto &p : filtered_other_cell_activation_patterns) {
 					log("      Activation pattern for cell %s: %s = %s\n", log_id(other_cell), log_signal(p.first), log_signal(p.second));
-					other_cell_active.push_back(ez->vec_eq(satgen.importSigSpec(p.first), satgen.importSigSpec(p.second)));
+					other_cell_active.push_back(qcsat.ez->vec_eq(qcsat.importSig(p.first), qcsat.importSig(p.second)));
 					all_ctrl_signals.append(p.first);
 				}
 
-				for (auto &bit : cell_activation_signals.to_sigbit_vector())
-					bits_queue.insert(bit);
-
-				for (auto &bit : other_cell_activation_signals.to_sigbit_vector())
-					bits_queue.insert(bit);
-
-				while (!bits_queue.empty())
-				{
-					pool<ModWalker::PortBit> portbits;
-					modwalker.get_drivers(portbits, bits_queue);
-					bits_queue.clear();
-
-					for (auto &pbit : portbits)
-						if (sat_cells.count(pbit.cell) == 0 && cone_ct.cell_known(pbit.cell->type)) {
-							if (config.opt_fast && modwalker.cell_outputs[pbit.cell].size() >= 4)
-								continue;
-							// log("      Adding cell %s (%s) to SAT problem.\n", log_id(pbit.cell), log_id(pbit.cell->type));
-							bits_queue.insert(modwalker.cell_inputs[pbit.cell].begin(), modwalker.cell_inputs[pbit.cell].end());
-							satgen.importCell(pbit.cell);
-							sat_cells.insert(pbit.cell);
-						}
-
-					if (config.opt_fast && sat_cells.size() > 100)
-						break;
-				}
-
-				for (auto it : exclusive_ctrls)
-					if (satgen.importedSigBit(it.first) && satgen.importedSigBit(it.second)) {
-						log("      Adding exclusive control bits: %s vs. %s\n", log_signal(it.first), log_signal(it.second));
-						int sub1 = satgen.importSigBit(it.first);
-						int sub2 = satgen.importSigBit(it.second);
-						ez->assume(ez->NOT(ez->AND(sub1, sub2)));
-					}
+				qcsat.prepare();
 
-				if (!ez->solve(ez->expression(ez->OpOr, cell_active))) {
+				int sub1 = qcsat.ez->expression(qcsat.ez->OpOr, cell_active);
+				if (!qcsat.ez->solve(sub1)) {
 					log("      According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", log_id(cell));
 					cells_to_remove.insert(cell);
 					break;
 				}
 
-				if (!ez->solve(ez->expression(ez->OpOr, other_cell_active))) {
+				int sub2 = qcsat.ez->expression(qcsat.ez->OpOr, other_cell_active);
+				if (!qcsat.ez->solve(sub2)) {
 					log("      According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", log_id(other_cell));
 					cells_to_remove.insert(other_cell);
 					shareable_cells.erase(other_cell);
 					continue;
 				}
 
-				ez->non_incremental();
+				qcsat.ez->non_incremental();
 
 				all_ctrl_signals.sort_and_unify();
-				std::vector<int> sat_model = satgen.importSigSpec(all_ctrl_signals);
+				std::vector<int> sat_model = qcsat.importSig(all_ctrl_signals);
 				std::vector<bool> sat_model_values;
 
-				int sub1 = ez->expression(ez->OpOr, cell_active);
-				int sub2 = ez->expression(ez->OpOr, other_cell_active);
-				ez->assume(ez->AND(sub1, sub2));
+				qcsat.ez->assume(qcsat.ez->AND(sub1, sub2));
 
 				log("      Size of SAT problem: %d cells, %d variables, %d clauses\n",
-						GetSize(sat_cells), ez->numCnfVariables(), ez->numCnfClauses());
+						GetSize(sat_cells), qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses());
 
-				if (ez->solve(sat_model, sat_model_values)) {
+				if (qcsat.ez->solve(sat_model, sat_model_values)) {
 					log("      According to the SAT solver this pair of cells can not be shared.\n");
 					log("      Model from SAT solver: %s = %d'", log_signal(all_ctrl_signals), GetSize(sat_model_values));
 					for (int i = GetSize(sat_model_values)-1; i >= 0; i--)