btorsim: implement smod

smod is defined as the remainder of a signed division, but with the sign
of the divisor. Delegate to srem and adjust the sign afterward to avoid
duplicating the division logic.

Signed-off-by: Ferdinand Bachmann <[email protected]>

Author: Ferdi265

src/btorsim/btorsim.cpp

@@ -267,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:
@@ -288,7 +289,6 @@ parse_model_line (Btor2Line *l)
     case BTOR2_TAG_justice:
     case BTOR2_TAG_saddo:
     case BTOR2_TAG_sdivo:
-    case BTOR2_TAG_smod:
     case BTOR2_TAG_smulo:
     case BTOR2_TAG_ssubo:
     case BTOR2_TAG_uaddo:
@@ -624,6 +624,12 @@ 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);
       case BTOR2_TAG_srl:
         assert (l->nargs == 2);
         assert (res.type == BtorSimState::Type::BITVEC);

src/btorsim/btorsimbv.c

@@ -2033,6 +2033,29 @@ btorsim_bv_srem (const BtorSimBitVector *a, const BtorSimBitVector *b)
   return res;
 }
 
+BtorSimBitVector *
+btorsim_bv_smod (const BtorSimBitVector *a, const BtorSimBitVector *b)
+{
+  BtorSimBitVector *srem, *sign_srem, *srem_abs, *sign_b, *res;
+
+  // take absolute value of srem
+  srem = btorsim_bv_srem(a, b);
+  sign_srem = btorsim_bv_slice(srem, srem->width - 1, srem->width - 1);
+  srem_abs = btorsim_bv_is_true(sign_srem) ? btorsim_bv_neg(srem)
+                                           : btorsim_bv_copy(srem);
+
+  // apply sign of divisor
+  sign_b = btorsim_bv_slice (b, b->width - 1, b->width - 1);
+  res = btorsim_bv_is_true(sign_b) ? btorsim_bv_neg(srem_abs) :
+                                     btorsim_bv_copy(srem_abs);
+
+  btorsim_bv_free(srem);
+  btorsim_bv_free(sign_srem);
+  btorsim_bv_free(srem_abs);
+  btorsim_bv_free(sign_b);
+  return res;
+}
+
 BtorSimBitVector *
 btorsim_bv_concat (const BtorSimBitVector *a, const BtorSimBitVector *b)
 {

src/btorsim/btorsimbv.h

@@ -212,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);