def make_enum(menv, v_name: str, enum_size: int):
    bool_type = msat_get_bool_type(menv)
    num_bits = ceil(log(enum_size, 2))
    b_vars = []
    for idx in range(num_bits):
        c_name = '{}{}'.format(v_name, idx)
        b_vars.append(tuple(decl_consts(menv, c_name, bool_type)))
    vals = []
    x_vals = []
    for enum_val in range(enum_size):
        bit_val = format(enum_val, '0{}b'.format(num_bits))
        assert (len(bit_val) == num_bits)
        assert all(((c in {'0', '1'}) for c in bit_val))
        assign = [(b_vars[idx] if (c == '1') else (msat_make_not(menv, b_vars[idx][0]), msat_make_not(menv, b_vars[idx][1]))) for (idx, c) in enumerate(reversed(bit_val))]
        pred = assign[0][0]
        x_pred = assign[0][1]
        for it in assign[1:]:
            pred = msat_make_and(menv, pred, it[0])
            x_pred = msat_make_and(menv, x_pred, it[1])
        vals.append(pred)
        x_vals.append(x_pred)
    assert (len(vals) == enum_size)
    assert (len(x_vals) == enum_size)
    return (b_vars, vals, x_vals)
def make_enum(menv, v_name: str, enum_size: int):
    bool_type = msat_get_bool_type(menv)
    num_bits = ceil(log(enum_size, 2))
    b_vars = []
    for idx in range(num_bits):
        c_name = '{}{}'.format(v_name, idx)
        b_vars.append(tuple(decl_consts(menv, c_name, bool_type)))
    vals = []
    x_vals = []
    for enum_val in range(enum_size):
        bit_val = format(enum_val, '0{}b'.format(num_bits))
        assert (len(bit_val) == num_bits)
        assert all(((c in {'0', '1'}) for c in bit_val))
        assign = [(b_vars[idx] if (c == '1') else (msat_make_not(menv, b_vars[idx][0]), msat_make_not(menv, b_vars[idx][1]))) for (idx, c) in enumerate(reversed(bit_val))]
        pred = assign[0][0]
        x_pred = assign[0][1]
        for it in assign[1:]:
            pred = msat_make_and(menv, pred, it[0])
            x_pred = msat_make_and(menv, x_pred, it[1])
        vals.append(pred)
        x_vals.append(x_pred)
    assert (len(vals) == enum_size)
    assert (len(x_vals) == enum_size)
    return (b_vars, vals, x_vals)