diff --git a/src/btorsim/btorsim.cpp b/src/btorsim/btorsim.cpp index 200bc46..34402c9 100644 --- a/src/btorsim/btorsim.cpp +++ b/src/btorsim/btorsim.cpp @@ -243,6 +243,7 @@ parse_model_line (Btor2Line *l) case BTOR2_TAG_implies: case BTOR2_TAG_inc: case BTOR2_TAG_ite: + case BTOR2_TAG_iff: case BTOR2_TAG_mul: case BTOR2_TAG_nand: case BTOR2_TAG_neg: @@ -256,6 +257,8 @@ parse_model_line (Btor2Line *l) case BTOR2_TAG_redand: case BTOR2_TAG_redor: case BTOR2_TAG_redxor: + case BTOR2_TAG_rol: + case BTOR2_TAG_ror: case BTOR2_TAG_sdiv: case BTOR2_TAG_sext: case BTOR2_TAG_sgt: @@ -264,6 +267,7 @@ parse_model_line (Btor2Line *l) case BTOR2_TAG_sll: case BTOR2_TAG_slt: case BTOR2_TAG_slte: + case BTOR2_TAG_smod: case BTOR2_TAG_sra: case BTOR2_TAG_srem: case BTOR2_TAG_srl: @@ -283,11 +287,8 @@ parse_model_line (Btor2Line *l) case BTOR2_TAG_fair: case BTOR2_TAG_justice: - case BTOR2_TAG_rol: - case BTOR2_TAG_ror: case BTOR2_TAG_saddo: case BTOR2_TAG_sdivo: - case BTOR2_TAG_smod: case BTOR2_TAG_smulo: case BTOR2_TAG_ssubo: case BTOR2_TAG_uaddo: @@ -546,6 +547,20 @@ simulate (int64_t id) assert (args[0].type == BtorSimState::Type::BITVEC); res.bv_state = btorsim_bv_redxor (args[0].bv_state); break; + case BTOR2_TAG_rol: + assert (l->nargs == 2); + assert (res.type == BtorSimState::Type::BITVEC); + assert (args[0].type == BtorSimState::Type::BITVEC); + assert (args[1].type == BtorSimState::Type::BITVEC); + res.bv_state = btorsim_bv_rol (args[0].bv_state, args[1].bv_state); + break; + case BTOR2_TAG_ror: + assert (l->nargs == 2); + assert (res.type == BtorSimState::Type::BITVEC); + assert (args[0].type == BtorSimState::Type::BITVEC); + assert (args[1].type == BtorSimState::Type::BITVEC); + res.bv_state = btorsim_bv_ror (args[0].bv_state, args[1].bv_state); + break; case BTOR2_TAG_slice: assert (l->nargs == 1); assert (res.type == BtorSimState::Type::BITVEC); @@ -609,6 +624,13 @@ simulate (int64_t id) assert (args[1].type == BtorSimState::Type::BITVEC); res.bv_state = btorsim_bv_sll (args[0].bv_state, args[1].bv_state); break; + case BTOR2_TAG_smod: + assert (l->nargs == 2); + assert (res.type == BtorSimState::Type::BITVEC); + assert (args[0].type == BtorSimState::Type::BITVEC); + assert (args[1].type == BtorSimState::Type::BITVEC); + res.bv_state = btorsim_bv_smod (args[0].bv_state, args[1].bv_state); + break; case BTOR2_TAG_srl: assert (l->nargs == 2); assert (res.type == BtorSimState::Type::BITVEC); diff --git a/src/btorsim/btorsimbv.c b/src/btorsim/btorsimbv.c index 3359684..c33fff1 100644 --- a/src/btorsim/btorsimbv.c +++ b/src/btorsim/btorsimbv.c @@ -1736,15 +1736,15 @@ btorsim_bv_sra (const BtorSimBitVector *a, const BtorSimBitVector *b) assert (a->len == b->len); assert (a->width == b->width); - BtorSimBitVector *res, *sign_b, *srl1, *srl2, *not_a; + BtorSimBitVector *res, *sign_a, *srl1, *srl2, *not_a; - sign_b = btorsim_bv_slice (b, b->width - 1, b->width - 1); + sign_a = btorsim_bv_slice (a, a->width - 1, a->width - 1); srl1 = btorsim_bv_srl (a, b); not_a = btorsim_bv_not (a); srl2 = btorsim_bv_srl (not_a, b); - res = btorsim_bv_is_true (not_a) ? btorsim_bv_not (srl2) + res = btorsim_bv_is_true (sign_a) ? btorsim_bv_not (srl2) : btorsim_bv_copy (srl1); - btorsim_bv_free (sign_b); + btorsim_bv_free (sign_a); btorsim_bv_free (srl1); btorsim_bv_free (srl2); btorsim_bv_free (not_a); @@ -1753,6 +1753,38 @@ btorsim_bv_sra (const BtorSimBitVector *a, const BtorSimBitVector *b) return res; } +BtorSimBitVector * +btorsim_bv_rol (const BtorSimBitVector *a, const BtorSimBitVector *b) { + BtorSimBitVector *width = btorsim_bv_uint64_to_bv(a->width, a->width); + BtorSimBitVector *rev = btorsim_bv_sub(width, b); + + BtorSimBitVector *sll_part = btorsim_bv_sll(a, b); + BtorSimBitVector *srl_part = btorsim_bv_srl(a, rev); + BtorSimBitVector *res = btorsim_bv_or(sll_part, srl_part); + + btorsim_bv_free(width); + btorsim_bv_free(rev); + btorsim_bv_free(sll_part); + btorsim_bv_free(srl_part); + return res; +} + +BtorSimBitVector * +btorsim_bv_ror (const BtorSimBitVector *a, const BtorSimBitVector *b) { + BtorSimBitVector *width = btorsim_bv_uint64_to_bv(a->width, a->width); + BtorSimBitVector *rev = btorsim_bv_sub(width, b); + + BtorSimBitVector *srl_part = btorsim_bv_srl(a, b); + BtorSimBitVector *sll_part = btorsim_bv_sll(a, rev); + BtorSimBitVector *res = btorsim_bv_or(srl_part, sll_part); + + btorsim_bv_free(width); + btorsim_bv_free(rev); + btorsim_bv_free(srl_part); + btorsim_bv_free(sll_part); + return res; +} + BtorSimBitVector * btorsim_bv_mul (const BtorSimBitVector *a, const BtorSimBitVector *b) { @@ -2001,6 +2033,66 @@ btorsim_bv_srem (const BtorSimBitVector *a, const BtorSimBitVector *b) return res; } +BtorSimBitVector * +btorsim_bv_smod (const BtorSimBitVector *a, const BtorSimBitVector *b) +{ + assert (a); + assert (b); + assert (a->len == b->len); + assert (a->width == b->width); + + BtorSimBitVector *res = 0, *not_b, *sign_a, *sign_b, *neg_a, *neg_b, *add; + BtorSimBitVector *cond_a, *cond_b, *urem, *neg_urem; + bool a_positive, b_positive; + + if (a->width == 1) + { + not_b = btorsim_bv_not (b); + res = btorsim_bv_and (a, not_b); + btorsim_bv_free (not_b); + } + else + { + sign_a = btorsim_bv_slice (a, a->width - 1, a->width - 1); + sign_b = btorsim_bv_slice (b, b->width - 1, b->width - 1); + a_positive = !btorsim_bv_is_true (sign_a); + b_positive = !btorsim_bv_is_true (sign_b); + + neg_a = btorsim_bv_neg (a); + neg_b = btorsim_bv_neg (b); + cond_a = a_positive ? btorsim_bv_copy (a) + : btorsim_bv_copy (neg_a); + cond_b = b_positive ? btorsim_bv_copy (b) + : btorsim_bv_copy (neg_b); + + + urem = btorsim_bv_urem (cond_a, cond_b); + add = btorsim_bv_is_zero(urem) ? btorsim_bv_zero(b->width) + : btorsim_bv_copy(b); + + neg_urem = btorsim_bv_neg (urem); + + res = a_positive && b_positive ? btorsim_bv_copy(urem) + : !a_positive && b_positive ? btorsim_bv_add(neg_urem, add) + : a_positive && !b_positive ? btorsim_bv_add(urem, add) + : btorsim_bv_copy(neg_urem); + + btorsim_bv_free (sign_a); + btorsim_bv_free (sign_b); + btorsim_bv_free (neg_a); + btorsim_bv_free (neg_b); + btorsim_bv_free (cond_a); + btorsim_bv_free (cond_b); + btorsim_bv_free (urem); + btorsim_bv_free (add); + btorsim_bv_free (neg_urem); + } + + assert (res); + assert (rem_bits_zero_dbg (res)); + return res; +} + BtorSimBitVector * btorsim_bv_concat (const BtorSimBitVector *a, const BtorSimBitVector *b) { diff --git a/src/btorsim/btorsimbv.h b/src/btorsim/btorsimbv.h index 6ed2d69..81a6182 100644 --- a/src/btorsim/btorsimbv.h +++ b/src/btorsim/btorsimbv.h @@ -191,6 +191,12 @@ BtorSimBitVector *btorsim_bv_srl (const BtorSimBitVector *a, BtorSimBitVector *btorsim_bv_sra (const BtorSimBitVector *a, const BtorSimBitVector *b); +BtorSimBitVector *btorsim_bv_rol (const BtorSimBitVector *a, + const BtorSimBitVector *b); + +BtorSimBitVector *btorsim_bv_ror (const BtorSimBitVector *a, + const BtorSimBitVector *b); + BtorSimBitVector *btorsim_bv_mul (const BtorSimBitVector *a, const BtorSimBitVector *b); @@ -206,6 +212,9 @@ BtorSimBitVector *btorsim_bv_urem (const BtorSimBitVector *a, BtorSimBitVector *btorsim_bv_srem (const BtorSimBitVector *a, const BtorSimBitVector *b); +BtorSimBitVector *btorsim_bv_smod (const BtorSimBitVector *a, + const BtorSimBitVector *b); + BtorSimBitVector *btorsim_bv_ite (const BtorSimBitVector *c, const BtorSimBitVector *t, const BtorSimBitVector *e);