diff options
| author | Clifford Wolf <clifford@clifford.at> | 2018-03-04 21:22:20 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2018-03-04 21:22:20 +0100 |
| commit | 8b7602e660b15a6a9dd7f773c3f7d7021f36659b (patch) | |
| tree | d58f95ab42dd4457bf1708e21805e99bb7fc9ac5 /backends/smt2 | |
| parent | 45a6fce92c595bf406f771c97d5a1de359f465f9 (diff) | |
| download | yosys-8b7602e660b15a6a9dd7f773c3f7d7021f36659b.tar.gz yosys-8b7602e660b15a6a9dd7f773c3f7d7021f36659b.tar.bz2 yosys-8b7602e660b15a6a9dd7f773c3f7d7021f36659b.zip | |
Improve SMT2 encoding of $reduce_{and,or,bool}
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'backends/smt2')
| -rw-r--r-- | backends/smt2/smt2.cc | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 124364120..47c993d05 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -379,7 +379,8 @@ struct Smt2Worker if (type == 's' || type == 'd' || type == 'b') { width = max(width, GetSize(cell->getPort("\\A"))); - width = max(width, GetSize(cell->getPort("\\B"))); + if (cell->hasPort("\\B")) + width = max(width, GetSize(cell->getPort("\\B"))); } if (cell->hasPort("\\A")) { @@ -561,6 +562,13 @@ struct Smt2Worker if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)", 'd'); if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)", 'd'); + if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool") && + 2*GetSize(cell->getPort("\\A").chunks()) < GetSize(cell->getPort("\\A"))) { + bool is_and = cell->type == "$reduce_and"; + string bits(GetSize(cell->getPort("\\A")), is_and ? '1' : '0'); + return export_bvop(cell, stringf("(%s A #b%s)", is_and ? "=" : "distinct", bits.c_str()), 'b'); + } + if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true); if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false); if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false); |