From aaaa604853caaecf8dcbfa928914495efb5556c6 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 26 Feb 2014 21:31:34 +0100
Subject: Added support for $bu0 to SatGen

---
 kernel/satgen.h | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 53921044..d9bcb425 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -385,7 +385,7 @@ struct SatGen
 			return true;
 		}
 
-		if (cell->type == "$pos" || cell->type == "$neg")
+		if (cell->type == "$pos" || cell->type == "$bu0" || cell->type == "$neg")
 		{
 			std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep);
 			std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
@@ -393,7 +393,7 @@ struct SatGen
 
 			std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
 
-			if (cell->type == "$pos") {
+			if (cell->type == "$pos" || cell->type == "$bu0") {
 				ez->assume(ez->vec_eq(a, yy));
 			} else {
 				std::vector<int> zero(a.size(), ez->FALSE);
@@ -404,9 +404,9 @@ struct SatGen
 			{
 				std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 				std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
-				extendSignalWidthUnary(undef_a, undef_y, cell, true);
+				extendSignalWidthUnary(undef_a, undef_y, cell, cell->type != "$bu0");
 
-				if (cell->type == "$pos") {
+				if (cell->type == "$pos" || cell->type == "$bu0") {
 					ez->assume(ez->vec_eq(undef_a, undef_y));
 				} else {
 					int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
-- 
cgit v1.2.3