From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 4 Mar 2018 20:22:20 +0000 (+0100)
Subject: Improve SMT2 encoding of $reduce_{and,or,bool}
X-Git-Tag: yosys-0.8~181
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8b7602e660b15a6a9dd7f773c3f7d7021f36659b;p=yosys.git

Improve SMT2 encoding of $reduce_{and,or,bool}

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---

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);