mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-01 14:57:57 +00:00
Code Activity

code simplifications

Browse source
This commit is contained in:
Nuno Lopes 2026-01-30 15:26:21 +00:00
parent 70a03c7784
commit 095b2bdf59
5 changed files with 16 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/util/common_msgs.cpp
View file

@ -18,10 +18,10 @@ Notes:
--*/
#include "util/common_msgs.h"
char const * common_msgs::g_canceled_msg = "canceled";
char const * common_msgs::g_max_memory_msg = "max. memory exceeded";
char const * common_msgs::g_max_scopes_msg = "max. scopes exceeded";
char const * common_msgs::g_max_steps_msg = "max. steps exceeded";
char const * common_msgs::g_max_frames_msg = "max. frames exceeded";
char const * common_msgs::g_no_proofs_msg = "component does not support proof generation";
char const * common_msgs::g_max_resource_msg = "max. resource limit exceeded";
char const common_msgs::g_canceled_msg[] = "canceled";
char const common_msgs::g_max_memory_msg[] = "max. memory exceeded";
char const common_msgs::g_max_scopes_msg[] = "max. scopes exceeded";
char const common_msgs::g_max_steps_msg[] = "max. steps exceeded";
char const common_msgs::g_max_frames_msg[] = "max. frames exceeded";
char const common_msgs::g_no_proofs_msg[] = "component does not support proof generation";
char const common_msgs::g_max_resource_msg[] = "max. resource limit exceeded";

14
src/util/common_msgs.h
View file

@ -20,13 +20,13 @@ Notes:
class common_msgs {
public:
static char const * g_canceled_msg;
static char const * g_max_memory_msg;
static char const * g_max_scopes_msg;
static char const * g_max_steps_msg;
static char const * g_max_frames_msg;
static char const * g_no_proofs_msg;
static char const * g_max_resource_msg;
static char const g_canceled_msg[];
static char const g_max_memory_msg[];
static char const g_max_scopes_msg[];
static char const g_max_steps_msg[];
static char const g_max_frames_msg[];
static char const g_no_proofs_msg[];
static char const g_max_resource_msg[];
};
#define Z3_CANCELED_MSG common_msgs::g_canceled_msg

9
src/util/mpz.cpp
View file

@ -188,16 +188,12 @@ template<bool SYNCH>
mpz_cell * mpz_manager<SYNCH>::allocate(unsigned capacity) {
SASSERT(capacity >= m_init_cell_capacity);
mpz_cell * cell;
#ifdef SINGLE_THREAD
cell = reinterpret_cast<mpz_cell*>(m_allocator.allocate(cell_size(capacity)));
#else
if (SYNCH) {
cell = reinterpret_cast<mpz_cell*>(memory::allocate(cell_size(capacity)));
}
else {
cell = reinterpret_cast<mpz_cell*>(m_allocator.allocate(cell_size(capacity)));
}
#endif
cell->m_capacity = capacity;
return cell;
@ -206,17 +202,12 @@ mpz_cell * mpz_manager<SYNCH>::allocate(unsigned capacity) {
template<bool SYNCH>
void mpz_manager<SYNCH>::deallocate(bool is_heap, mpz_cell * ptr) {
if (is_heap) {
#ifdef SINGLE_THREAD
m_allocator.deallocate(cell_size(ptr->m_capacity), ptr);
#else
if (SYNCH) {
memory::deallocate(ptr);
}
else {
m_allocator.deallocate(cell_size(ptr->m_capacity), ptr);
}
#endif
}
}

9
src/util/mpz.h
View file

@ -152,6 +152,7 @@ class mpz_manager {
mutable std::recursive_mutex m_lock;
#define MPZ_BEGIN_CRITICAL() if (SYNCH) m_lock.lock()
#define MPZ_END_CRITICAL() if (SYNCH) m_lock.unlock()
static_assert(false);
#else
#define MPZ_BEGIN_CRITICAL() {}
#define MPZ_END_CRITICAL() {}
@ -211,16 +212,12 @@ class mpz_manager {
mpz_t * allocate() {
mpz_t * cell;
#ifdef SINGLE_THREAD
cell = reinterpret_cast<mpz_t*>(m_allocator.allocate(sizeof(mpz_t)));
#else
if (SYNCH) {
cell = reinterpret_cast<mpz_t*>(memory::allocate(sizeof(mpz_t)));
}
else {
cell = reinterpret_cast<mpz_t*>(m_allocator.allocate(sizeof(mpz_t)));
}
#endif
mpz_init(*cell);
return cell;
}
@ -228,16 +225,12 @@ class mpz_manager {
void deallocate(bool is_heap, mpz_t * ptr) {
mpz_clear(*ptr);
if (is_heap) {
#ifdef SINGLE_THREAD
m_allocator.deallocate(sizeof(mpz_t), ptr);
#else
if (SYNCH) {
memory::deallocate(ptr);
}
else {
m_allocator.deallocate(sizeof(mpz_t), ptr);
}
#endif
}
}

2
src/util/rational.cpp
View file

@ -44,8 +44,8 @@ static DECLARE_MUTEX(g_powers_of_two);
rational rational::power_of_two(unsigned k) {
rational result;
lock_guard lock(*g_powers_of_two);
{
lock_guard lock(*g_powers_of_two);
if (k >= m_powers_of_two.size())
mk_power_up_to(m_powers_of_two, k+1);
result = m_powers_of_two[k];