diff options
Diffstat (limited to 'kernel/satgen.h')
| -rw-r--r-- | kernel/satgen.h | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h index bd6259ba1..cf2db733f 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -262,6 +262,18 @@ struct SatGen } } + std::pair<std::vector<int>, std::vector<int>> mux(int s, int undef_s, const std::vector<int> &a, const std::vector<int> &undef_a, const std::vector<int> &b, const std::vector<int> &undef_b) { + std::vector<int> res; + std::vector<int> undef_res; + res = ez->vec_ite(s, b, a); + if (model_undef) { + std::vector<int> unequal_ab = ez->vec_not(ez->vec_iff(a, b)); + std::vector<int> undef_ab = ez->vec_or(unequal_ab, ez->vec_or(undef_a, undef_b)); + undef_res = ez->vec_ite(undef_s, undef_ab, ez->vec_ite(s, undef_b, undef_a)); + } + return std::make_pair(res, undef_res); + } + void undefGating(int y, int yy, int undef) { ez->assume(ez->OR(undef, ez->IFF(y, yy))); |