From 29a555ec7eaa0e561f76c65258a50c54b6468546 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 29 Dec 2014 17:10:37 +0100 Subject: Added statehash to ezSAT --- passes/opt/share.cc | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'passes/opt') diff --git a/passes/opt/share.cc b/passes/opt/share.cc index e2c31bec..7ab50991 100644 --- a/passes/opt/share.cc +++ b/passes/opt/share.cc @@ -1226,7 +1226,9 @@ struct ShareWorker 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)); - ez.assume(ez.NOT(ez.AND(satgen.importSigBit(it.first), satgen.importSigBit(it.second)))); + int sub1 = satgen.importSigBit(it.first); + int sub2 = satgen.importSigBit(it.second); + ez.assume(ez.NOT(ez.AND(sub1, sub2))); } if (!ez.solve(ez.expression(ez.OpOr, cell_active))) { @@ -1248,7 +1250,9 @@ struct ShareWorker std::vector sat_model = satgen.importSigSpec(all_ctrl_signals); std::vector sat_model_values; - ez.assume(ez.AND(ez.expression(ez.OpOr, cell_active), ez.expression(ez.OpOr, other_cell_active))); + int sub1 = ez.expression(ez.OpOr, cell_active); + int sub2 = ez.expression(ez.OpOr, other_cell_active); + ez.assume(ez.AND(sub1, sub2)); log(" Size of SAT problem: %d cells, %d variables, %d clauses\n", GetSize(sat_cells), ez.numCnfVariables(), ez.numCnfClauses()); -- cgit v1.2.3