+ ez->assume(ez->vec_eq(ez->vec_ite(s.at(0), b, a), y));
+ return true;
+ }
+
+ if (cell->type == "$pmux" || cell->type == "$safe_pmux") {
+ std::vector<int> a = importSigSpec(cell->connections.at("\\A"));
+ std::vector<int> b = importSigSpec(cell->connections.at("\\B"));
+ std::vector<int> s = importSigSpec(cell->connections.at("\\S"));
+ std::vector<int> y = importSigSpec(cell->connections.at("\\Y"));
+ std::vector<int> tmp = a;
+ for (size_t i = 0; i < s.size(); i++) {
+ std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
+ tmp = ez->vec_ite(s.at(i), part_of_b, tmp);
+ }
+ if (cell->type == "$safe_pmux")
+ tmp = ez->vec_ite(ez->onehot(s, true), tmp, a);
+ ez->assume(ez->vec_eq(tmp, y));
+ return true;
+ }
+
+ if (cell->type == "$pos" || cell->type == "$neg") {
+ std::vector<int> a = importSigSpec(cell->connections.at("\\A"));
+ std::vector<int> y = importSigSpec(cell->connections.at("\\Y"));
+ if (cell->type == "$pos") {
+ ez->assume(ez->vec_eq(a, y));
+ } else {
+ std::vector<int> zero(a.size(), ez->FALSE);
+ ez->assume(ez->vec_eq(ez->vec_sub(zero, a), y));
+ }
+ return true;
+ }
+
+ if (cell->type == "$reduce_and" || cell->type == "$reduce_or" || cell->type == "$reduce_xor" ||
+ cell->type == "$reduce_xnor" || cell->type == "$reduce_bool" || cell->type == "$logic_not") {
+ std::vector<int> a = importSigSpec(cell->connections.at("\\A"));
+ std::vector<int> y = importSigSpec(cell->connections.at("\\Y"));
+ if (cell->type == "$reduce_and")
+ ez->SET(ez->expression(ez->OpAnd, a), y.at(0));
+ if (cell->type == "$reduce_or" || cell->type == "$reduce_bool")
+ ez->SET(ez->expression(ez->OpOr, a), y.at(0));
+ if (cell->type == "$reduce_xor")
+ ez->SET(ez->expression(ez->OpXor, a), y.at(0));
+ if (cell->type == "$reduce_xnor")
+ ez->SET(ez->NOT(ez->expression(ez->OpXor, a)), y.at(0));
+ if (cell->type == "$logic_not")
+ ez->SET(ez->NOT(ez->expression(ez->OpOr, a)), y.at(0));
+ for (size_t i = 1; i < y.size(); i++)
+ ez->SET(0, y.at(0));
+ return true;
+ }
+
+ if (cell->type == "$logic_and" || cell->type == "$logic_or") {
+ int a = ez->expression(ez->OpOr, importSigSpec(cell->connections.at("\\A")));
+ int b = ez->expression(ez->OpOr, importSigSpec(cell->connections.at("\\B")));
+ std::vector<int> y = importSigSpec(cell->connections.at("\\Y"));
+ if (cell->type == "$logic_and")
+ ez->SET(ez->expression(ez->OpAnd, a, b), y.at(0));
+ else
+ ez->SET(ez->expression(ez->OpOr, a, b), y.at(0));
+ for (size_t i = 1; i < y.size(); i++)
+ ez->SET(0, y.at(0));
+ return true;
+ }
+