// direction=false for shift left
// direction=true for shift right
struct SMT_var* generate_shifter (struct SMT_var* X, struct SMT_var* cnt, bool direction)
{
    int w=X->width;

    struct SMT_var* in=X;
    struct SMT_var* out;
    struct SMT_var* tmp;

    // bit vector must have width=2^x, i.e., 8, 16, 32, 64, etc
    assert (popcount64c (w)==1);

    int bits_in_selector=mylog2(w);

    for (int i=0; i<bits_in_selector; i++)
    {
        if (direction==false)
            tmp=generate_shift_left(in, 1<<i);
        else
            tmp=generate_shift_right(in, 1<<i);

        out=create_internal_variable("tmp", TY_BITVEC, w);

        add_Tseitin_ITE_BV (cnt->SAT_var+i, tmp->SAT_var, in->SAT_var, out->SAT_var, w);

        in=out;
    };

    // if any bit is set in high part of "cnt" variable, result is 0
    // i.e., if a 8-bit bitvector is shifted by cnt>8, give a zero
    struct SMT_var *disable_shifter=create_internal_variable("...", TY_BOOL, 1);
    add_Tseitin_OR_list(cnt->SAT_var+bits_in_selector, w-bits_in_selector, disable_shifter->SAT_var);

    return generate_ITE(disable_shifter, generate_const(0, w), in);
};

struct SMT_var* generate_BVSHL (struct SMT_var* X, struct SMT_var* cnt)
{
    return generate_shifter (X, cnt, false);
};