Added support for $bu0 to SatGen

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 539210442f01b406d34b6ca75e61fa0fe4d47ee1..d9bcb425004fde2cfb34c3f03ce45d4e341dc3ec 100644 (file)
--- 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);