mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

fix build of unit tests

Browse source
This commit is contained in:
Nuno Lopes 2017-10-14 20:41:08 +01:00
parent 468e0207f7
commit 912a729097
6 changed files with 43 additions and 65 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/interval/interval.h
View file

@ -162,7 +162,7 @@ private:
void checkpoint(); void checkpoint();
public: public:
interval_manager(reslimit& lim, C const & c); interval_manager(reslimit& lim, C && c);
~interval_manager(); ~interval_manager();
numeral_manager & m() const { return m_c.m(); } numeral_manager & m() const { return m_c.m(); }

2
src/math/interval/interval_def.h
View file

@ -31,7 +31,7 @@ Revision History:
// #define TRACE_NTH_ROOT // #define TRACE_NTH_ROOT
template<typename C> template<typename C>
interval_manager<C>::interval_manager(reslimit& lim, C const & c): m_limit(lim), m_c(c) { interval_manager<C>::interval_manager(reslimit& lim, C && c): m_limit(lim), m_c(std::move(c)) {
m().set(m_minus_one, -1); m().set(m_minus_one, -1);
m().set(m_one, 1); m().set(m_one, 1);
m_pi_n = 0; m_pi_n = 0;

6
src/test/im_float_config.h
View file

@ -63,10 +63,4 @@ public:
numeral_manager & m() const { return const_cast<numeral_manager&>(m_manager); } numeral_manager & m() const { return const_cast<numeral_manager&>(m_manager); }
}; };
template<typename fmanager>
inline void del_f_interval(im_float_config<fmanager> & cfg, typename im_float_config<fmanager>::interval & a) {
cfg.m().del(a.m_lower);
cfg.m().del(a.m_upper);
}
#endif #endif

78
src/test/interval.cpp
View file

@ -125,7 +125,8 @@ static bool mk_interval(im_default_config & cfg, interval & a, bool l_inf, bool
} }
#endif #endif
static void mk_random_interval(im_default_config & cfg, interval & a, unsigned magnitude) { template <typename T>
static void mk_random_interval(T & cfg, interval & a, unsigned magnitude) {
switch (rand()%3) { switch (rand()%3) {
case 0: case 0:
// Neg, Neg // Neg, Neg
@ -195,11 +196,6 @@ static void mk_random_interval(im_default_config & cfg, interval & a, unsigned m
} }
} }
static void del_interval(im_default_config & cfg, interval & a) {
cfg.m().del(a.m_lower);
cfg.m().del(a.m_upper);
}
#define BUFFER_SZ 256 #define BUFFER_SZ 256
static int g_problem_id = 0; static int g_problem_id = 0;
static char g_buffer[BUFFER_SZ]; static char g_buffer[BUFFER_SZ];
@ -238,19 +234,18 @@ static void display_lemmas(unsynch_mpq_manager & nm, char const * result_term,
static void tst_ ## NAME(unsigned N, unsigned magnitude) { \ static void tst_ ## NAME(unsigned N, unsigned magnitude) { \
reslimit rl; \ reslimit rl; \
unsynch_mpq_manager nm; \ unsynch_mpq_manager nm; \
im_default_config imc(nm); \ interval_manager<im_default_config> im(rl, nm); \
interval_manager<im_default_config> im(rl, imc); \
interval a, b, r; \ interval a, b, r; \
\ \
for (unsigned i = 0; i < N; i++) { \ for (unsigned i = 0; i < N; i++) { \
mk_random_interval(imc, a, magnitude); \ mk_random_interval(im, a, magnitude); \
mk_random_interval(imc, b, magnitude); \ mk_random_interval(im, b, magnitude); \
interval_deps deps; \ interval_deps deps; \
im.NAME(a, b, r, deps); \ im.NAME(a, b, r, deps); \
\ \
display_lemmas(nm, RES_TERM, a, b, r, deps); \ display_lemmas(nm, RES_TERM, a, b, r, deps); \
} \ } \
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); \ im.del(a); im.del(b); im.del(r); \
} }
MK_BINARY(mul, "(* a b)"); MK_BINARY(mul, "(* a b)");
@ -260,56 +255,52 @@ MK_BINARY(sub, "(- a b)");
static void tst_neg(unsigned N, unsigned magnitude) { static void tst_neg(unsigned N, unsigned magnitude) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval a, b, r; interval a, b, r;
for (unsigned i = 0; i < N; i++) { for (unsigned i = 0; i < N; i++) {
mk_random_interval(imc, a, magnitude); mk_random_interval(im, a, magnitude);
interval_deps deps; interval_deps deps;
im.neg(a, r, deps); im.neg(a, r, deps);
display_lemmas(nm, "(- a)", a, b, r, deps); display_lemmas(nm, "(- a)", a, b, r, deps);
} }
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); im.del(a); im.del(b); im.del(r);
} }
static void tst_pw_2(unsigned N, unsigned magnitude) { static void tst_pw_2(unsigned N, unsigned magnitude) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval a, b, r; interval a, b, r;
for (unsigned i = 0; i < N; i++) { for (unsigned i = 0; i < N; i++) {
mk_random_interval(imc, a, magnitude); mk_random_interval(im, a, magnitude);
interval_deps deps; interval_deps deps;
im.power(a, 2, r, deps); im.power(a, 2, r, deps);
display_lemmas(nm, "(* a a)", a, b, r, deps); display_lemmas(nm, "(* a a)", a, b, r, deps);
} }
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); im.del(a); im.del(b); im.del(r);
} }
static void tst_pw_3(unsigned N, unsigned magnitude) { static void tst_pw_3(unsigned N, unsigned magnitude) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval a, b, r; interval a, b, r;
for (unsigned i = 0; i < N; i++) { for (unsigned i = 0; i < N; i++) {
mk_random_interval(imc, a, magnitude); mk_random_interval(im, a, magnitude);
interval_deps deps; interval_deps deps;
im.power(a, 3, r, deps); im.power(a, 3, r, deps);
display_lemmas(nm, "(* a a a)", a, b, r, deps); display_lemmas(nm, "(* a a a)", a, b, r, deps);
} }
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); im.del(a); im.del(b); im.del(r);
} }
static void tst_root_2(unsigned N, unsigned magnitude, unsigned precision) { static void tst_root_2(unsigned N, unsigned magnitude, unsigned precision) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval a, b, r; interval a, b, r;
scoped_mpq p(nm); scoped_mpq p(nm);
p = precision; p = precision;
@ -317,7 +308,7 @@ static void tst_root_2(unsigned N, unsigned magnitude, unsigned precision) {
unsigned i = 0; unsigned i = 0;
while (i < N) { while (i < N) {
mk_random_interval(imc, a, magnitude); mk_random_interval(im, a, magnitude);
if (!im.lower_is_neg(a)) { if (!im.lower_is_neg(a)) {
i++; i++;
interval_deps deps; interval_deps deps;
@ -325,14 +316,13 @@ static void tst_root_2(unsigned N, unsigned magnitude, unsigned precision) {
display_lemmas(nm, "(^ a (/ 1.0 2.0))", a, b, r, deps); display_lemmas(nm, "(^ a (/ 1.0 2.0))", a, b, r, deps);
} }
} }
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); im.del(a); im.del(b); im.del(r);
} }
static void tst_root_3(unsigned N, unsigned magnitude, unsigned precision) { static void tst_root_3(unsigned N, unsigned magnitude, unsigned precision) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval a, b, r; interval a, b, r;
scoped_mpq p(nm); scoped_mpq p(nm);
p = precision; p = precision;
@ -340,25 +330,24 @@ static void tst_root_3(unsigned N, unsigned magnitude, unsigned precision) {
unsigned i = 0; unsigned i = 0;
while (i < N) { while (i < N) {
mk_random_interval(imc, a, magnitude); mk_random_interval(im, a, magnitude);
i++; i++;
interval_deps deps; interval_deps deps;
im.nth_root(a, 3, p, r, deps); im.nth_root(a, 3, p, r, deps);
display_lemmas(nm, "(^ a (/ 1.0 3.0))", a, b, r, deps); display_lemmas(nm, "(^ a (/ 1.0 3.0))", a, b, r, deps);
} }
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); im.del(a); im.del(b); im.del(r);
} }
static void tst_inv(unsigned N, unsigned magnitude) { static void tst_inv(unsigned N, unsigned magnitude) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval a, b, r; interval a, b, r;
for (unsigned i = 0; i < N; i++) { for (unsigned i = 0; i < N; i++) {
while (true) { while (true) {
mk_random_interval(imc, a, magnitude); mk_random_interval(im, a, magnitude);
if (!im.contains_zero(a)) if (!im.contains_zero(a))
break; break;
} }
@ -366,20 +355,19 @@ static void tst_inv(unsigned N, unsigned magnitude) {
im.inv(a, r, deps); im.inv(a, r, deps);
display_lemmas(nm, "(/ 1 a)", a, b, r, deps); display_lemmas(nm, "(/ 1 a)", a, b, r, deps);
} }
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); im.del(a); im.del(b); im.del(r);
} }
static void tst_div(unsigned N, unsigned magnitude) { static void tst_div(unsigned N, unsigned magnitude) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval a, b, r; interval a, b, r;
for (unsigned i = 0; i < N; i++) { for (unsigned i = 0; i < N; i++) {
mk_random_interval(imc, a, magnitude); mk_random_interval(im, a, magnitude);
while (true) { while (true) {
mk_random_interval(imc, b, magnitude); mk_random_interval(im, b, magnitude);
if (!im.contains_zero(b)) if (!im.contains_zero(b))
break; break;
} }
@ -387,7 +375,7 @@ static void tst_div(unsigned N, unsigned magnitude) {
im.div(a, b, r, deps); im.div(a, b, r, deps);
display_lemmas(nm, "(/ a b)", a, b, r, deps); display_lemmas(nm, "(/ a b)", a, b, r, deps);
} }
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); im.del(a); im.del(b); im.del(r);
} }
#include "test/im_float_config.h" #include "test/im_float_config.h"
@ -396,8 +384,7 @@ static void tst_div(unsigned N, unsigned magnitude) {
static void tst_float() { static void tst_float() {
unsynch_mpq_manager qm; unsynch_mpq_manager qm;
mpf_manager fm; mpf_manager fm;
im_float_config<mpf_manager> ifc(fm); interval_manager<im_float_config<mpf_manager> > im(fm);
interval_manager<im_float_config<mpf_manager> > im(ifc);
im_float_config<mpf_manager>::interval a, b, c; im_float_config<mpf_manager>::interval a, b, c;
scoped_mpq minus_one_third(qm), one_third(qm), two_third(qm), minus_two_third(qm); scoped_mpq minus_one_third(qm), one_third(qm), two_third(qm), minus_two_third(qm);
qm.set(minus_one_third, -1, 3); qm.set(minus_one_third, -1, 3);
@ -424,15 +411,14 @@ static void tst_float() {
im.display(std::cout, c); im.display(std::cout, c);
std::cout << "\n"; std::cout << "\n";
del_f_interval(ifc, a); del_f_interval(ifc, b); del_f_interval(ifc, c); im.del(a); im.del(b); im.del(r);
} }
#endif #endif
void tst_pi() { void tst_pi() {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval r; interval r;
for (unsigned i = 0; i < 8; i++) { for (unsigned i = 0; i < 8; i++) {
im.pi(i, r); im.pi(i, r);
@ -440,7 +426,7 @@ void tst_pi() {
nm.display_decimal(std::cout, im.upper(r), 32); std::cout << "\n"; nm.display_decimal(std::cout, im.upper(r), 32); std::cout << "\n";
ENSURE(nm.lt(im.lower(r), im.upper(r))); ENSURE(nm.lt(im.lower(r), im.upper(r)));
} }
del_interval(imc, r); im.del(r);
} }
#if 0 #if 0

17
src/test/trigo.cpp
View file

@ -39,9 +39,8 @@ static void tst_sine_core(std::ostream & out, unsynch_mpq_manager & nm, interval
static void tst_sine(std::ostream & out, unsigned N, unsigned k) { static void tst_sine(std::ostream & out, unsigned N, unsigned k) {
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm);
reslimit rl; reslimit rl;
interval_manager<im_default_config> im(rl, imc); interval_manager<im_default_config> im(rl, nm);
scoped_mpq a(nm); scoped_mpq a(nm);
nm.set(a, 0); nm.set(a, 0);
tst_sine_core(out, nm, im, a, 1); tst_sine_core(out, nm, im, a, 1);
@ -67,8 +66,7 @@ static void tst_cosine_core(std::ostream & out, unsynch_mpq_manager & nm, interv
static void tst_cosine(std::ostream & out, unsigned N, unsigned k) { static void tst_cosine(std::ostream & out, unsigned N, unsigned k) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
scoped_mpq a(nm); scoped_mpq a(nm);
nm.set(a, 0); nm.set(a, 0);
tst_cosine_core(out, nm, im, a, 1); tst_cosine_core(out, nm, im, a, 1);
@ -100,8 +98,7 @@ template<typename fmanager>
static void tst_float_sine(std::ostream & out, unsigned N, unsigned k) { static void tst_float_sine(std::ostream & out, unsigned N, unsigned k) {
reslimit rl; reslimit rl;
fmanager fm; fmanager fm;
im_float_config<fmanager> ifc(fm, EBITS, SBITS); interval_manager<im_float_config<fmanager> > im(rl, { fm, EBITS, SBITS });
interval_manager<im_float_config<fmanager> > im(rl, ifc);
_scoped_numeral<fmanager> a(fm); _scoped_numeral<fmanager> a(fm);
fm.set(a, EBITS, SBITS, static_cast<int>(0)); fm.set(a, EBITS, SBITS, static_cast<int>(0));
tst_float_sine_core(out, fm, im, a, 1); tst_float_sine_core(out, fm, im, a, 1);
@ -136,8 +133,7 @@ static void tst_mpf_bug() {
static void tst_e(std::ostream & out) { static void tst_e(std::ostream & out) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
im_default_config::interval r; im_default_config::interval r;
for (unsigned i = 0; i < 64; i++) { for (unsigned i = 0; i < 64; i++) {
im.e(i, r); im.e(i, r);
@ -152,8 +148,7 @@ static void tst_e_float(std::ostream & out) {
reslimit rl; reslimit rl;
unsynch_mpq_manager qm; unsynch_mpq_manager qm;
mpf_manager fm; mpf_manager fm;
im_float_config<mpf_manager> ifc(fm); interval_manager<im_float_config<mpf_manager> > im(rl, fm);
interval_manager<im_float_config<mpf_manager> > im(rl, ifc);
scoped_mpq q(qm); scoped_mpq q(qm);
im_float_config<mpf_manager>::interval r; im_float_config<mpf_manager>::interval r;
for (unsigned i = 0; i < 64; i++) { for (unsigned i = 0; i < 64; i++) {
@ -161,7 +156,7 @@ static void tst_e_float(std::ostream & out) {
out << fm.to_rational_string(im.lower(r)) << " <= E\n"; out << fm.to_rational_string(im.lower(r)) << " <= E\n";
out << "E <= " << fm.to_rational_string(im.upper(r)) << "\n"; out << "E <= " << fm.to_rational_string(im.upper(r)) << "\n";
} }
del_f_interval(ifc, r); im.del(r);
} }
void tst_trigo() { void tst_trigo() {

3
src/util/f2n.h
View file

@ -46,6 +46,9 @@ public:
m_manager.set(m_one, ebits, sbits, 1); m_manager.set(m_one, ebits, sbits, 1);
} }
f2n(f2n && other) : m_manager(other.m_manager), m_mode(other.m_mode), m_ebits(other.m_ebits), m_sbits(other.m_sbits),
m_tmp1(std::move(other.m_tmp1)), m_one(std::move(other.m_one)) {}
~f2n() { ~f2n() {
m().del(m_tmp1); m().del(m_tmp1);
m().del(m_one); m().del(m_one);