riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

fixed freduce for Minisat::SimpSolver: use frozen_literal()

This commit is contained in:
Clifford Wolf 2014-03-03 02:14:27 +01:00
parent d5bd93997c
commit 96e753041d
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
passes/sat/freduce.cc
View File

@ -112,13 +112,13 @@ struct FindReducedInputs
size_t idx_bits = get_bits(idx);
if (sat_pi_uniq_bitvec.size() != idx_bits) {
sat_pi_uniq_bitvec.push_back(ez.literal(stringf("uniq_%d", int(idx_bits)-1)));
sat_pi_uniq_bitvec.push_back(ez.frozen_literal(stringf("uniq_%d", int(idx_bits)-1)));
for (auto &it : sat_pi)
ez.assume(ez.OR(ez.NOT(it.second), ez.NOT(sat_pi_uniq_bitvec.back())));
}
log_assert(sat_pi_uniq_bitvec.size() == idx_bits);
sat_pi[bit] = ez.literal(stringf("pi_%s", log_signal(bit)));
sat_pi[bit] = ez.frozen_literal(stringf("p, falsei_%s", log_signal(bit)));
ez.assume(ez.IFF(ez.XOR(sat_a, sat_b), sat_pi[bit]));
for (size_t i = 0; i < idx_bits; i++)