mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Fix Visual Studio warnings

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-13 09:06:07 -08:00
parent 93f37bdf9f
commit 7312f49f88
5 changed files with 60 additions and 54 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/api/api_rcf.cpp
View file

@ -25,24 +25,24 @@ Notes:
#include"api_context.h"
#include"realclosure.h"
static rcmanager & rcfm(Z3_context c) {
return mk_c(c)->rcfm();
}
static void reset_rcf_cancel(Z3_context c) {
rcfm(c).reset_cancel();
}
static Z3_rcf_num from_rcnumeral(rcnumeral a) {
return reinterpret_cast<Z3_rcf_num>(a.c_ptr());
}
static rcnumeral to_rcnumeral(Z3_rcf_num a) {
return rcnumeral::mk(a);
}
extern "C" {
static rcmanager & rcfm(Z3_context c) {
return mk_c(c)->rcfm();
}
static void reset_rcf_cancel(Z3_context c) {
rcfm(c).reset_cancel();
}
static rcnumeral to_rcnumeral(Z3_rcf_num a) {
return rcnumeral::mk(a);
}
static Z3_rcf_num from_rcnumeral(rcnumeral a) {
return reinterpret_cast<Z3_rcf_num>(a.c_ptr());
}
void Z3_API Z3_rcf_del(Z3_context c, Z3_rcf_num a) {
Z3_TRY;
LOG_Z3_rcf_del(c, a);

5
src/math/realclosure/mpz_matrix.cpp
View file

@ -44,7 +44,8 @@ void mpz_matrix_manager::mk(unsigned m, unsigned n, mpz_matrix & A) {
del(A);
A.m = m;
A.n = n;
A.a_ij = new (m_allocator) mpz[m*n];
void * mem = m_allocator.allocate(sizeof(mpz)*m*n);
A.a_ij = new (mem) mpz[m*n];
}
void mpz_matrix_manager::del(mpz_matrix & A) {
@ -409,7 +410,7 @@ void mpz_matrix_manager::display(std::ostream & out, mpz_matrix const & A, unsig
out << " ";
std::string s = nm().to_string(A(i, j));
if (s.size() < cell_width) {
unsigned space = cell_width - s.size();
unsigned space = cell_width - static_cast<unsigned>(s.size());
for (unsigned k = 0; k < space; k++)
out << " ";
}

31
src/math/realclosure/realclosure.cpp
View file

@ -97,10 +97,10 @@ namespace realclosure {
void set_upper_is_open(bool f) { m_upper_open = f; }
numeral const & lower() const { return m_lower; }
numeral const & upper() const { return m_upper; }
bool lower_is_inf() const { return m_lower_inf; }
bool upper_is_inf() const { return m_upper_inf; }
bool lower_is_open() const { return m_lower_open; }
bool upper_is_open() const { return m_upper_open; }
bool lower_is_inf() const { return m_lower_inf != 0; }
bool upper_is_inf() const { return m_upper_inf != 0; }
bool lower_is_open() const { return m_lower_open != 0; }
bool upper_is_open() const { return m_upper_open != 0; }
};
void set_rounding(bool to_plus_inf) { m_manager.m_to_plus_inf = to_plus_inf; }
@ -112,10 +112,10 @@ namespace realclosure {
numeral const & upper(interval const & a) const { return a.m_upper; }
numeral & lower(interval & a) { return a.m_lower; }
numeral & upper(interval & a) { return a.m_upper; }
bool lower_is_open(interval const & a) const { return a.m_lower_open; }
bool upper_is_open(interval const & a) const { return a.m_upper_open; }
bool lower_is_inf(interval const & a) const { return a.m_lower_inf; }
bool upper_is_inf(interval const & a) const { return a.m_upper_inf; }
bool lower_is_open(interval const & a) const { return a.lower_is_open(); }
bool upper_is_open(interval const & a) const { return a.upper_is_open(); }
bool lower_is_inf(interval const & a) const { return a.lower_is_inf(); }
bool upper_is_inf(interval const & a) const { return a.upper_is_inf(); }
// Setters
void set_lower(interval & a, numeral const & n) { m_manager.set(a.m_lower, n); }
@ -637,7 +637,8 @@ namespace realclosure {
return; // interval was already saved.
to_restore.push_back(v);
inc_ref(v);
v->m_old_interval = new (allocator()) mpbqi();
void * mem = allocator().allocate(sizeof(mpbqi));
v->m_old_interval = new (mem) mpbqi();
set_interval(*(v->m_old_interval), v->m_interval);
}
void save_interval(value * v) {
@ -1201,7 +1202,8 @@ namespace realclosure {
}
sign_condition * mk_sign_condition(unsigned qidx, int sign, sign_condition * prev_sc) {
return new (allocator()) sign_condition(qidx, sign, prev_sc);
void * mem = allocator().allocate(sizeof(sign_condition));
return new (mem) sign_condition(qidx, sign, prev_sc);
}
/**
@ -1748,7 +1750,8 @@ namespace realclosure {
M and scs will be empty after this operation.
*/
sign_det * mk_sign_det(mpz_matrix & M_s, scoped_polynomial_seq const & prs, int_buffer const & taqrs, scoped_polynomial_seq const & qs, scoped_sign_conditions & scs) {
sign_det * r = new (allocator()) sign_det();
void * mem = allocator().allocate(sizeof(sign_det));
sign_det * r = new (mem) sign_det();
r->M_s.swap(M_s);
set_array_p(r->m_prs, prs);
r->m_taqrs.set(allocator(), taqrs.size(), taqrs.c_ptr());
@ -1763,7 +1766,8 @@ namespace realclosure {
*/
algebraic * mk_algebraic(unsigned p_sz, value * const * p, mpbqi const & interval, sign_det * sd, unsigned sc_idx) {
unsigned idx = next_algebraic_idx();
algebraic * r = new (allocator()) algebraic(idx);
void * mem = allocator().allocate(sizeof(algebraic));
algebraic * r = new (mem) algebraic(idx);
m_extensions[extension::ALGEBRAIC].push_back(r);
set_p(r->m_p, p_sz, p);
@ -2495,7 +2499,8 @@ namespace realclosure {
}
rational_value * mk_rational() {
return new (allocator()) rational_value();
void * mem = allocator().allocate(sizeof(rational_value));
return new (mem) rational_value();
}
/**

4
src/math/realclosure/realclosure.h
View file

@ -267,10 +267,10 @@ namespace realclosure {
void clean_denominators(numeral const & a, numeral & p, numeral & q);
};
class value;
struct value;
class num {
friend class manager;
friend class manager::imp;
friend struct manager::imp;
value * m_value;
public:
num():m_value(0) {}

42
src/util/array.h
View file

@ -40,7 +40,7 @@ private:
array & operator=(array const & source);
void set_data(void * mem, size_t sz) {
void set_data(void * mem, unsigned sz) {
size_t * _mem = static_cast<size_t*>(mem);
*_mem = sz;
_mem ++;
@ -48,7 +48,7 @@ private:
}
template<typename Allocator>
void allocate(Allocator & a, size_t sz) {
void allocate(Allocator & a, unsigned sz) {
size_t * mem = reinterpret_cast<size_t*>(a.allocate(space(sz)));
set_data(mem, sz);
}
@ -80,13 +80,13 @@ public:
\brief Store the array in the given chunk of memory (mem).
This chunck should be big enough to store space(sz) bytes.
*/
array(void * mem, size_t sz, T const * vs) {
array(void * mem, unsigned sz, T const * vs) {
DEBUG_CODE(m_data = 0;);
set(mem, sz, vs);
}
// WARNING: the memory allocated will not be automatically freed.
array(void * mem, size_t sz, bool init_mem) {
array(void * mem, unsigned sz, bool init_mem) {
DEBUG_CODE(m_data = 0;);
set_data(mem, sz);
if (init_mem)
@ -95,14 +95,14 @@ public:
// WARNING: the memory allocated will not be automatically freed.
template<typename Allocator>
array(Allocator & a, size_t sz, T const * vs) {
array(Allocator & a, unsigned sz, T const * vs) {
DEBUG_CODE(m_data = 0;);
set(a, sz, vs);
}
// WARNING: the memory allocated will not be automatically freed.
template<typename Allocator>
array(Allocator & a, size_t sz, bool init_mem) {
array(Allocator & a, unsigned sz, bool init_mem) {
DEBUG_CODE(m_data = 0;);
allocate(a, sz);
if (init_mem)
@ -127,41 +127,41 @@ public:
}
}
void set(void * mem, size_t sz, T const * vs) {
void set(void * mem, unsigned sz, T const * vs) {
SASSERT(m_data == 0);
set_data(mem, sz);
init(vs);
}
template<typename Allocator>
void set(Allocator & a, size_t sz, T const * vs) {
void set(Allocator & a, unsigned sz, T const * vs) {
SASSERT(m_data == 0);
allocate(a, sz);
init(vs);
}
template<typename Allocator>
void set(Allocator & a, size_t sz, T const & v = T()) {
void set(Allocator & a, unsigned sz, T const & v = T()) {
SASSERT(m_data == 0);
allocate(a, sz);
init(v);
}
size_t size() const {
unsigned size() const {
if (m_data == 0) {
return 0;
}
return reinterpret_cast<size_t *>(m_data)[SIZE_IDX];
return static_cast<unsigned>(reinterpret_cast<size_t *>(m_data)[SIZE_IDX]);
}
bool empty() const { return m_data == 0; }
T & operator[](size_t idx) {
T & operator[](unsigned idx) {
SASSERT(idx < size());
return m_data[idx];
}
T const & operator[](size_t idx) const {
T const & operator[](unsigned idx) const {
SASSERT(idx < size());
return m_data[idx];
}
@ -195,24 +195,24 @@ template<typename T>
class ptr_array : public array<T *, false> {
public:
ptr_array() {}
ptr_array(void * mem, size_t sz, T * const * vs):array<T*, false>(mem, sz, vs) {}
ptr_array(void * mem, unsigned sz, T * const * vs):array<T*, false>(mem, sz, vs) {}
template<typename Allocator>
ptr_array(Allocator & a, size_t sz, T * const * vs):array<T*, false>(a, sz, vs) {}
ptr_array(void * mem, size_t sz, bool init_mem):array<T*, false>(mem, sz, init_mem) {}
ptr_array(Allocator & a, unsigned sz, T * const * vs):array<T*, false>(a, sz, vs) {}
ptr_array(void * mem, unsigned sz, bool init_mem):array<T*, false>(mem, sz, init_mem) {}
template<typename Allocator>
ptr_array(Allocator & a, size_t sz, bool init_mem):array<T*, false>(a, sz, init_mem) {}
ptr_array(Allocator & a, unsigned sz, bool init_mem):array<T*, false>(a, sz, init_mem) {}
};
template<typename T>
class sarray : public array<T, false> {
public:
sarray() {}
sarray(void * mem, size_t sz, T const * vs):array<T, false>(mem, sz, vs) {}
sarray(void * mem, unsigned sz, T const * vs):array<T, false>(mem, sz, vs) {}
template<typename Allocator>
sarray(Allocator & a, size_t sz, T const * vs):array<T, false>(a, sz, vs) {}
sarray(void * mem, size_t sz, bool init_mem):array<T, false>(mem, sz, init_mem) {}
sarray(Allocator & a, unsigned sz, T const * vs):array<T, false>(a, sz, vs) {}
sarray(void * mem, unsigned sz, bool init_mem):array<T, false>(mem, sz, init_mem) {}
template<typename Allocator>
sarray(Allocator & a, size_t sz, bool init_mem):array<T, false>(a, sz, init_mem) {}
sarray(Allocator & a, unsigned sz, bool init_mem):array<T, false>(a, sz, init_mem) {}
};
#endif