static void integer_divide_remainder(struct solver_Algebra *a, uint64_t lhs, uint64_t rhs, uint64_t *div, uint64_t *rem) {
  if(is_smallint(lhs) && is_smallint(rhs)) {
    *div = pack_smallint(unpack_smallint(lhs) / unpack_smallint(rhs));
    *rem = pack_smallint(unpack_smallint(lhs) % unpack_smallint(rhs));
  } else {
    *div = pack_undefined();
    *rem = pack_undefined();
  }
}

static uint64_t integer_divide(struct solver_Algebra *a, uint64_t lhs, uint64_t rhs) {
  uint64_t div, rem;
  integer_divide_remainder(a, lhs, rhs, &div, &rem);
  return div;
}

static uint64_t integer_remainder(struct solver_Algebra *a, uint64_t lhs, uint64_t rhs) {
  uint64_t div, rem;
  integer_divide_remainder(a, lhs, rhs, &div, &rem);
  return rem;
}

static uint64_t integer_negate(uint64_t expr) {
  return (expr ^ INTEGER_NEG_FLAG_BIT);
}

static bool integer_is_negative(uint64_t expr) {
  return (expr & INTEGER_NEG_FLAG_BIT) == INTEGER_NEG_FLAG_BIT;
}

static uint64_t integer_absolute(uint64_t expr) {
  return (expr & ~INTEGER_NEG_FLAG_BIT);
}

static uint64_t integer_greatest_common_denominator(struct solver_Algebra *a, uint64_t lhs, uint64_t rhs) {
  uint64_t r;
  while(rhs != LITERAL_ZERO) {
    r = integer_remainder(a, lhs, rhs);
    lhs = rhs;
    rhs = r;
  }
  return integer_absolute(lhs);
}

uint64_t solver_Algebra_integer(struct solver_Algebra *a, int64_t value) {
  return pack_smallint(value);
}