bitvector.h

Go to the documentation of this file.

/***
 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
 *
 * Copyright (C) 2020 by the authors listed in the AUTHORS file at
 * https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
 *
 * This file is part of Bitwuzla under the MIT license. See COPYING for more
 * information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
 */
// Modified by Xiang Zhang, 2026
// Additional changes licensed under the MIT License
#ifndef BZLA__BV_BITVECTOR_H
#define BZLA__BV_BITVECTOR_H
 
#include <gmpxx.h>
 
#include <cstdint>
#include <functional>
#include <string>
 
namespace stabilizer::util {
 
/* -------------------------------------------------------------------------- */
 
/* -------------------------------------------------------------------------- */
 
class BitVector {
  public:
    // mpz_*_ui functions have unsigned long (or mp_bitcnt_t) arguments, which is
    // represented as 64 bit on Linux and macOS 64-bit systems. On 64-bit Windows
    // unsigned long has a size of 32 bit, which affects the values stored in
    // d_val_uint64 if being passed to a mpz_*_ui function.
    // In order to avoid values being truncated, for Windows we store all values
    // that require more than 32 bit as GMP integer. Else, we store values up to
    // 64-bit in d_val_uint64.
    static constexpr size_t s_native_size = sizeof(unsigned long) * 8;
    static_assert(s_native_size == sizeof(mp_bitcnt_t) * 8, "");
 
    static bool fits_in_size(uint64_t size, const std::string &str, uint32_t base);
    static bool fits_in_size(uint64_t size, uint64_t value, bool sign = false);
 
    static bool fits_in_size(uint64_t size, const mpz_t value);
 
    static BitVector from_ui(uint64_t size, uint64_t value, bool truncate = false);
    static BitVector from_si(uint64_t size, int64_t value, bool truncate = false);
 
    static BitVector mk_true();
    static BitVector mk_false();
    static BitVector mk_zero(uint64_t size);
    static BitVector mk_one(uint64_t size);
    static BitVector mk_ones(uint64_t size);
    static BitVector mk_min_signed(uint64_t size);
    static BitVector mk_max_signed(uint64_t size);
 
    static BitVector bvite(const BitVector &c, const BitVector &t, const BitVector &e);
 
    BitVector();
    BitVector(uint64_t size);
 
    BitVector(uint64_t size, const std::string &value, uint32_t base = 2);
 
    BitVector(uint64_t size, const mpz_t value, bool truncate = false);
 
    BitVector(const BitVector &other);
    BitVector(BitVector &&other);
 
    ~BitVector();
 
    BitVector &operator=(const BitVector &other);
 
    size_t hash() const;
 
    bool is_null() const { return d_size == 0; }
 
    void iset(uint64_t value);
    void iset(const BitVector &bv);
    // /**
    //  * Set the value of this bit-vector to a random value between `from` and
    //  `to`
    //  * (in-place).
    //  * @param rng  The random number generator.
    //  * @param from A bit-vector representing the `from` value.
    //  * @param to   A bit-vector representing the `to` value.
    //  */
    // void iset(RNG& rng,
    //           const BitVector& from,
    //           const BitVector& to,
    //           bool is_signed);
 
    bool operator==(const BitVector &bv) const;
    bool operator!=(const BitVector &bv) const;
 
    std::string str(uint32_t base = 2) const;
    uint64_t to_uint64(bool truncate = false) const;
 
    uint64_t size() const { return d_size; }
 
    int32_t compare(const BitVector &bv) const;
    int32_t signed_compare(const BitVector &bv) const;
 
    bool bit(uint64_t idx) const;
    void set_bit(uint64_t idx, bool value);
    void flip_bit(uint64_t idx);
    bool lsb() const;
    bool msb() const;
 
    bool is_true() const;
    bool is_false() const;
    bool is_zero() const;
    bool is_ones() const;
    bool is_one() const;
    bool is_min_signed() const;
    bool is_max_signed() const;
 
    bool is_power_of_two() const;
 
    bool is_neg_overflow() const;
    bool is_uadd_overflow(const BitVector &bv) const;
    bool is_sadd_overflow(const BitVector &bv) const;
    bool is_usub_overflow(const BitVector &bv) const;
    bool is_ssub_overflow(const BitVector &bv) const;
    bool is_umul_overflow(const BitVector &bv) const;
    bool is_smul_overflow(const BitVector &bv) const;
    bool is_sdiv_overflow(const BitVector &bv) const;
 
    uint64_t count_trailing_zeros() const;
    uint64_t count_trailing_ones() const;
    uint64_t count_leading_zeros() const;
    uint64_t count_leading_ones() const;
 
    /* ----------------------------------------------------------------------- */
    /* Bit-vector operations.                                                  */
    /* ----------------------------------------------------------------------- */
 
    BitVector bvneg() const;
    BitVector bvnot() const;
    BitVector bvinc() const;
    BitVector bvdec() const;
    BitVector bvredand() const;
    BitVector bvredor() const;
    BitVector bvredxor() const;
    BitVector bvnego() const;
 
    BitVector bvadd(const BitVector &bv) const;
    BitVector bvsub(const BitVector &bv) const;
    BitVector bvand(const BitVector &bv) const;
    BitVector bvimplies(const BitVector &bv) const;
    BitVector bvnand(const BitVector &bv) const;
    BitVector bvnor(const BitVector &bv) const;
    BitVector bvor(const BitVector &bv) const;
    BitVector bvxnor(const BitVector &bv) const;
    BitVector bvxor(const BitVector &bv) const;
    BitVector bveq(const BitVector &bv) const;
    BitVector bvne(const BitVector &bv) const;
    BitVector bvult(const BitVector &bv) const;
    BitVector bvule(const BitVector &bv) const;
    BitVector bvugt(const BitVector &bv) const;
    BitVector bvuge(const BitVector &bv) const;
    BitVector bvslt(const BitVector &bv) const;
    BitVector bvsle(const BitVector &bv) const;
    BitVector bvsgt(const BitVector &bv) const;
    BitVector bvsge(const BitVector &bv) const;
    BitVector bvshl(uint64_t shift) const;
    BitVector bvshl(const BitVector &bv) const;
    BitVector bvshr(uint64_t shift) const;
    BitVector bvshr(const BitVector &bv) const;
    BitVector bvashr(uint64_t shift) const;
    BitVector bvashr(const BitVector &bv) const;
    BitVector bvmul(const BitVector &bv) const;
    BitVector bvudiv(const BitVector &bv) const;
    BitVector bvurem(const BitVector &bv) const;
    BitVector bvsdiv(const BitVector &bv) const;
    BitVector bvsrem(const BitVector &bv) const;
    BitVector bvsmod(const BitVector &bv) const;
 
    BitVector bvuaddo(const BitVector &bv) const;
    BitVector bvsaddo(const BitVector &bv) const;
    BitVector bvusubo(const BitVector &bv) const;
    BitVector bvssubo(const BitVector &bv) const;
 
    BitVector bvumulo(const BitVector &bv) const;
    BitVector bvsmulo(const BitVector &bv) const;
    BitVector bvsdivo(const BitVector &bv) const;
 
    BitVector bvconcat(const BitVector &bv) const;
 
    BitVector bvextract(uint64_t idx_hi, uint64_t idx_lo) const;
 
    BitVector bvzext(uint64_t n) const;
    BitVector bvsext(uint64_t n) const;
 
    BitVector bvrepeat(uint64_t n) const;
 
    BitVector bvroli(uint64_t n) const;
    BitVector bvrol(const BitVector &n) const;
 
    BitVector bvrori(uint64_t n) const;
    BitVector bvror(const BitVector &n) const;
 
    BitVector bvmodinv() const;
 
    BitVector bvpow(const mpz_t exp) const;
 
    /* ----------------------------------------------------------------------- */
    /* In-place versions of bit-vector operations.                             */
    /*                                                                         */
    /* Note: This bit-vector may not be null.                                  */
    /*                                                                         */
    /* Result is stored in this bit-vector.                                    */
    /* Return a reference to this bit-vector.                                  */
    /* ----------------------------------------------------------------------- */
 
    BitVector &ibvneg(const BitVector &bv);
    BitVector &ibvneg();
 
    BitVector &ibvnot(const BitVector &bv);
    BitVector &ibvnot();
 
    BitVector &ibvinc(const BitVector &bv);
    BitVector &ibvinc();
 
    BitVector &ibvdec(const BitVector &bv);
    BitVector &ibvdec();
 
    BitVector &ibvredand(const BitVector &bv);
    BitVector &ibvredand();
 
    BitVector &ibvredor(const BitVector &bv);
    BitVector &ibvredor();
 
    BitVector &ibvredxor(const BitVector &bv);
    BitVector &ibvredxor();
 
    BitVector &ibvnego(const BitVector &bv);
    BitVector &ibvnego();
 
    BitVector &ibvadd(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvadd(const BitVector &bv);
 
    BitVector &ibvand(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvand(const BitVector &bv);
 
    BitVector &ibvimplies(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvimplies(const BitVector &bv);
 
    BitVector &ibvnand(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvnand(const BitVector &bv);
 
    BitVector &ibvnor(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvnor(const BitVector &bv);
 
    BitVector &ibvor(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvor(const BitVector &bv);
 
    BitVector &ibvsub(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvsub(const BitVector &bv);
 
    BitVector &ibvxnor(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvxnor(const BitVector &bv);
 
    BitVector &ibvxor(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvxor(const BitVector &bv);
 
    BitVector &ibveq(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibveq(const BitVector &bv);
 
    BitVector &ibvne(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvne(const BitVector &bv);
 
    BitVector &ibvult(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvult(const BitVector &bv);
 
    BitVector &ibvule(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvule(const BitVector &bv);
 
    BitVector &ibvugt(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvugt(const BitVector &bv);
 
    BitVector &ibvuge(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvuge(const BitVector &bv);
 
    BitVector &ibvslt(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvslt(const BitVector &bv);
 
    BitVector &ibvsle(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvsle(const BitVector &bv);
 
    BitVector &ibvsgt(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvsgt(const BitVector &bv);
 
    BitVector &ibvsge(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvsge(const BitVector &bv);
 
    BitVector &ibvshl(const BitVector &bv, uint64_t shift);
    BitVector &ibvshl(uint64_t shift);
 
    BitVector &ibvshl(const BitVector &bv, const BitVector &shift);
    BitVector &ibvshl(const BitVector &bv);
 
    BitVector &ibvshr(const BitVector &bv, uint64_t shift);
    BitVector &ibvshr(uint64_t shift);
 
    BitVector &ibvshr(const BitVector &bv, const BitVector &shift);
    BitVector &ibvshr(const BitVector &bv);
 
    BitVector &ibvashr(const BitVector &bv, uint64_t shift);
    BitVector &ibvashr(uint64_t shift);
 
    BitVector &ibvashr(const BitVector &bv, const BitVector &arithmetic);
    BitVector &ibvashr(const BitVector &bv);
 
    BitVector &ibvmul(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvmul(const BitVector &bv);
 
    BitVector &ibvudiv(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvudiv(const BitVector &bv);
 
    BitVector &ibvurem(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvurem(const BitVector &bv);
 
    BitVector &ibvsdiv(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvsdiv(const BitVector &bv);
 
    BitVector &ibvsrem(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvsrem(const BitVector &bv);
 
    BitVector &ibvsmod(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvsmod(const BitVector &bv);
 
    BitVector &ibvuaddo(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvuaddo(const BitVector &bv);
 
    BitVector &ibvsaddo(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvsaddo(const BitVector &bv);
 
    BitVector &ibvusubo(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvusubo(const BitVector &bv);
 
    BitVector &ibvssubo(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvssubo(const BitVector &bv);
 
    BitVector &ibvumulo(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvumulo(const BitVector &bv);
 
    BitVector &ibvsmulo(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvsmulo(const BitVector &bv);
 
    BitVector &ibvsdivo(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvsdivo(const BitVector &bv);
 
    BitVector &ibvconcat(const BitVector &bv0, const BitVector &bv1);
    BitVector &ibvconcat(const BitVector &bv);
 
    BitVector &ibvextract(const BitVector &bv, uint64_t idx_hi, uint64_t idx_lo);
    BitVector &ibvextract(uint64_t idx_hi, uint64_t idx_lo);
 
    BitVector &ibvzext(const BitVector &bv, uint64_t n);
    BitVector &ibvzext(uint64_t n);
 
    BitVector &ibvsext(const BitVector &bv, uint64_t n);
    BitVector &ibvsext(uint64_t n);
 
    BitVector &ibvrepeat(const BitVector &bv, uint64_t n);
    BitVector &ibvrepeat(uint64_t n);
 
    BitVector &ibvroli(const BitVector &bv, uint64_t n);
    BitVector &ibvroli(uint64_t n);
 
    BitVector &ibvrori(const BitVector &bv, uint64_t n);
    BitVector &ibvrori(uint64_t n);
 
    BitVector &ibvrol(const BitVector &bv, const BitVector &n);
    BitVector &ibvrol(const BitVector &n);
 
    BitVector &ibvror(const BitVector &bv, const BitVector &n);
    BitVector &ibvror(const BitVector &n);
 
    BitVector &ibvite(const BitVector &c, const BitVector &t, const BitVector &e);
 
    BitVector &ibvmodinv(const BitVector &bv);
    BitVector &ibvmodinv();
 
    BitVector &ibvpow(const BitVector &base, const mpz_t exp);
 
    BitVector &ibvpow(const mpz_t exp);
 
    void bvudivurem(const BitVector &bv, BitVector *quot, BitVector *rem) const;
 
    const mpz_t &gmp_value() const;
 
    mpz_class to_mpz() const;
 
  private:
    static uint64_t uint64_fdiv_r_2exp(uint64_t size, uint64_t val);
    uint64_t count_leading(bool zeros) const;
    bool shift_is_uint64(uint64_t *res) const;
    uint64_t get_limb(void *limb, uint64_t nbits_rem, bool zeros) const;
 
    bool is_gmp() const { return d_size > s_native_size; }
 
    uint64_t d_size = 0;
    union {
        uint64_t d_val_uint64;
        mpz_t d_val_gmp;
    };
};
 
std::ostream &operator<<(std::ostream &out, const BitVector &bv);
 
/* -------------------------------------------------------------------------- */
 
}  // namespace stabilizer::util
 
/* -------------------------------------------------------------------------- */
 
#endif