summaryrefslogtreecommitdiff
path: root/passes
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-03-03 02:14:27 +0100
committerClifford Wolf <clifford@clifford.at>2014-03-03 02:14:27 +0100
commit96e753041dbd0abc86ff0a6404f13d29edcb985d (patch)
treeb66c59c5a08f89163accd92324c0c0b86ec787b0 /passes
parentd5bd93997c9ce7c31ef430684700a2096618672e (diff)
fixed freduce for Minisat::SimpSolver: use frozen_literal()
Diffstat (limited to 'passes')
-rw-r--r--passes/sat/freduce.cc4
1 files changed, 2 insertions, 2 deletions
diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index 81250b00..746523f8 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.cc
@@ -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++)