diff options
author | Clifford Wolf <clifford@clifford.at> | 2015-02-21 12:15:41 +0100 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2015-02-21 12:15:41 +0100 |
commit | 4e6ca7760f801ce5ea16c6ea9be3ad4a86aa3b1d (patch) | |
tree | 2b6f0debe78102a24b1e1cf48cdfa14752cd0892 /passes/opt/share.cc | |
parent | f778a4081c9b509c0a1d886f8668b1931bfc93d6 (diff) | |
download | yosys-4e6ca7760f801ce5ea16c6ea9be3ad4a86aa3b1d.tar.gz yosys-4e6ca7760f801ce5ea16c6ea9be3ad4a86aa3b1d.tar.bz2 yosys-4e6ca7760f801ce5ea16c6ea9be3ad4a86aa3b1d.zip |
Replaced ezDefaultSAT with ezSatPtr
Diffstat (limited to 'passes/opt/share.cc')
-rw-r--r-- | passes/opt/share.cc | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/passes/opt/share.cc b/passes/opt/share.cc index 9cd0ccc03..bf406bcd8 100644 --- a/passes/opt/share.cc +++ b/passes/opt/share.cc @@ -1180,8 +1180,8 @@ struct ShareWorker optimize_activation_patterns(filtered_cell_activation_patterns); optimize_activation_patterns(filtered_other_cell_activation_patterns); - ezDefaultSAT ez; - SatGen satgen(&ez, &modwalker.sigmap); + ezSatPtr ez; + SatGen satgen(ez.get(), &modwalker.sigmap); pool<RTLIL::Cell*> sat_cells; std::set<RTLIL::SigBit> bits_queue; @@ -1191,13 +1191,13 @@ 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(ez->vec_eq(satgen.importSigSpec(p.first), satgen.importSigSpec(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(ez->vec_eq(satgen.importSigSpec(p.first), satgen.importSigSpec(p.second))); all_ctrl_signals.append(p.first); } @@ -1232,36 +1232,36 @@ struct ShareWorker 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))); + ez->assume(ez->NOT(ez->AND(sub1, sub2))); } - if (!ez.solve(ez.expression(ez.OpOr, cell_active))) { + if (!ez->solve(ez->expression(ez->OpOr, cell_active))) { 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))) { + if (!ez->solve(ez->expression(ez->OpOr, other_cell_active))) { 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(); + ez->non_incremental(); all_ctrl_signals.sort_and_unify(); std::vector<int> sat_model = satgen.importSigSpec(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)); + 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()); + GetSize(sat_cells), ez->numCnfVariables(), ez->numCnfClauses()); - if (ez.solve(sat_model, sat_model_values)) { + if (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--) |