gmp_utils.h

Go to the documentation of this file.

/***
 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
 *
 * Copyright (C) 2025 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_UTIL_GMP_UTILS_H_INCLUDED
#define BZLA_UTIL_GMP_UTILS_H_INCLUDED
 
#include <gmpxx.h>
 
#include <cstdint>
 
namespace stabilizer::util {
 
// GMP wrapper functions to properly handle case where unsigned long is 32 bit
// (Windows builds).
 
void mpz_set_ull(mpz_t rop, uint64_t op);
 
uint64_t mpz_get_ull(const mpz_t op);
 
void mpz_init_set_ull(mpz_t rop, uint64_t op);
 
mpz_class uint64_to_mpz_class(uint64_t op);
 
void mpz_init_set_sll(mpz_t rop, int64_t op);
 
size_t mpz_hash(const mpz_t op, uint64_t start = 0);
 
// These functions only guard their *_ui counterparts with an assertion for the
// Windows 32-bit case. In the cases where these functions are used we should
// never use values that require more than 32 bit.
void mpz_fdiv_q_2exp_ull(mpz_t q, const mpz_t n, uint64_t b);
 
void mpz_fdiv_r_2exp_ull(mpz_t r, const mpz_t n, uint64_t b);
 
void mpz_mul_2exp_ull(mpz_t rop, const mpz_t op1, uint64_t op2);
 
}  // namespace stabilizer::util
 
#endif