mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-07-15 22:36:02 -07:00
commit 30330c79a1
21 changed files with 199 additions and 165 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/util/cooperate.cpp
View file

@ -16,6 +16,8 @@ Author:
Notes:
--*/
#ifndef _NO_OMP_
#include "util/cooperate.h"
#include "util/trace.h"
#include "util/debug.h"
@ -36,7 +38,7 @@ struct cooperation_lock {
}
};
cooperation_lock g_lock;
static cooperation_lock g_lock;
bool cooperation_ctx::g_cooperate = false;
@ -59,29 +61,4 @@ void cooperation_ctx::checkpoint(char const * task) {
}
}
cooperation_section::cooperation_section() {
SASSERT(!cooperation_ctx::enabled());
SASSERT(!omp_in_parallel());
cooperation_ctx::g_cooperate = true;
}
cooperation_section::~cooperation_section() {
SASSERT(cooperation_ctx::enabled());
cooperation_ctx::g_cooperate = false;
}
init_task::init_task(char const * task) {
SASSERT(cooperation_ctx::enabled());
SASSERT(omp_in_parallel());
cooperation_ctx::checkpoint(task);
}
init_task::~init_task() {
int tid = omp_get_thread_num();
if (g_lock.m_owner_thread == tid) {
g_lock.m_owner_thread = -1;
omp_unset_nest_lock(&(g_lock.m_lock));
}
}
#endif

19
src/util/cooperate.h
View file

@ -19,10 +19,9 @@ Notes:
#ifndef COOPERATE_H_
#define COOPERATE_H_
class cooperation_section;
#ifndef _NO_OMP_
class cooperation_ctx {
friend class cooperation_section;
static bool g_cooperate;
public:
static bool enabled() { return g_cooperate; }
@ -33,18 +32,8 @@ inline void cooperate(char const * task) {
if (cooperation_ctx::enabled()) cooperation_ctx::checkpoint(task);
}
// must be declared before "#pragma parallel" to enable cooperation
class cooperation_section {
public:
cooperation_section();
~cooperation_section();
};
// must be first declaration inside "#pragma parallel for"
class init_task {
public:
init_task(char const * task);
~init_task();
};
#else
inline void cooperate(char const *) {}
#endif
#endif

28
src/util/lp/hnf_cutter.h
View file

@ -186,43 +186,41 @@ public:
bool overflow() const { return m_overflow; }
lia_move create_cut(lar_term& t, mpq& k, explanation& ex, bool & upper
#ifdef Z3DEBUG
,
const vector<mpq> & x0
#endif
) {
lia_move create_cut(lar_term& t, mpq& k, explanation& ex, bool & upper, const vector<mpq> & x0) {
// we suppose that x0 has at least one non integer element
(void)x0;
init_matrix_A();
svector<unsigned> basis_rows;
mpq big_number = m_abs_max.expt(3);
mpq d = hnf_calc::determinant_of_rectangular_matrix(m_A, basis_rows, big_number);
// std::cout << "max = " << m_abs_max << ", d = " << d << ", d/max = " << ceil (d /m_abs_max) << std::endl;
//std::cout << "max cube " << m_abs_max * m_abs_max * m_abs_max << std::endl;
// std::cout << "max = " << m_abs_max << ", d = " << d << ", d/max = " << ceil (d /m_abs_max) << std::endl;
// std::cout << "max cube " << m_abs_max * m_abs_max * m_abs_max << std::endl;
if (d >= big_number) {
return lia_move::undef;
}
if (m_settings.get_cancel_flag())
if (m_settings.get_cancel_flag()) {
return lia_move::undef;
}
if (basis_rows.size() < m_A.row_count()) {
m_A.shrink_to_rank(basis_rows);
shrink_explanation(basis_rows);
}
hnf<general_matrix> h(m_A, d);
// general_matrix A_orig = m_A;
hnf<general_matrix> h(m_A, d);
vector<mpq> b = create_b(basis_rows);
lp_assert(m_A * x0 == b);
// vector<mpq> bcopy = b;
find_h_minus_1_b(h.W(), b);
// lp_assert(bcopy == h.W().take_first_n_columns(b.size()) * b);
int cut_row = find_cut_row_index(b);
if (cut_row == -1)
if (cut_row == -1) {
return lia_move::undef;
}
// the matrix is not square - we can get
// all integers in b's projection

26
src/util/lp/int_solver.cpp
View file

@ -578,17 +578,27 @@ lia_move int_solver::make_hnf_cut() {
return lia_move::undef;
}
settings().st().m_hnf_cutter_calls++;
TRACE("hnf_cut", tout << "settings().st().m_hnf_cutter_calls = " << settings().st().m_hnf_cutter_calls;);
TRACE("hnf_cut", tout << "settings().st().m_hnf_cutter_calls = " << settings().st().m_hnf_cutter_calls << "\n";
for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
m_lar_solver->print_constraint(i, tout);
}
m_lar_solver->print_constraints(tout);
);
#ifdef Z3DEBUG
vector<mpq> x0 = m_hnf_cutter.transform_to_local_columns(m_lar_solver->m_mpq_lar_core_solver.m_r_x);
#else
vector<mpq> x0;
#endif
lia_move r = m_hnf_cutter.create_cut(*m_t, *m_k, *m_ex, *m_upper
#ifdef Z3DEBUG
, x0
#endif
);
CTRACE("hnf_cut", r == lia_move::cut, tout<< "cut:"; m_lar_solver->print_term(*m_t, tout); tout << " <= " << *m_k << std::endl;);
if (r == lia_move::cut) {
lia_move r = m_hnf_cutter.create_cut(*m_t, *m_k, *m_ex, *m_upper, x0);
if (r == lia_move::cut) {
TRACE("hnf_cut",
m_lar_solver->print_term(*m_t, tout << "cut:");
tout << " <= " << *m_k << std::endl;
for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
m_lar_solver->print_constraint(i, tout);
}
);
lp_assert(current_solution_is_inf_on_cut());
settings().st().m_hnf_cuts++;
m_ex->clear();

2
src/util/lp/lar_solver.h
View file

@ -112,7 +112,7 @@ private:
public :
unsigned terms_start_index() const { return m_terms_start_index; }
const vector<lar_term*> terms() const { return m_terms; }
const vector<lar_term*> & terms() const { return m_terms; }
const vector<lar_base_constraint*>& constraints() const {
return m_constraints;
}

10
src/util/mpff.cpp
View file

@ -376,9 +376,11 @@ void mpff_manager::set(mpff & n, unsynch_mpz_manager & m, mpz const & v) {
set_core(n, m, v);
}
#ifndef _NO_OMP_
void mpff_manager::set(mpff & n, synch_mpz_manager & m, mpz const & v) {
set_core(n, m, v);
}
#endif
template<bool SYNCH>
void mpff_manager::set_core(mpff & n, mpq_manager<SYNCH> & m, mpq const & v) {
@ -397,9 +399,11 @@ void mpff_manager::set(mpff & n, unsynch_mpq_manager & m, mpq const & v) {
set_core(n, m, v);
}
#ifndef _NO_OMP_
void mpff_manager::set(mpff & n, synch_mpq_manager & m, mpq const & v) {
set_core(n, m, v);
}
#endif
bool mpff_manager::eq(mpff const & a, mpff const & b) const {
if (is_zero(a) && is_zero(b))
@ -1077,9 +1081,11 @@ void mpff_manager::significand(mpff const & n, unsynch_mpz_manager & m, mpz & t)
significand_core(n, m, t);
}
#ifndef _NO_OMP_
void mpff_manager::significand(mpff const & n, synch_mpz_manager & m, mpz & t) {
significand_core(n, m, t);
}
#endif
template<bool SYNCH>
void mpff_manager::to_mpz_core(mpff const & n, mpz_manager<SYNCH> & m, mpz & t) {
@ -1109,9 +1115,11 @@ void mpff_manager::to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t);
}
#ifndef _NO_OMP_
void mpff_manager::to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t);
}
#endif
template<bool SYNCH>
void mpff_manager::to_mpq_core(mpff const & n, mpq_manager<SYNCH> & m, mpq & t) {
@ -1154,9 +1162,11 @@ void mpff_manager::to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t);
}
#ifndef _NO_OMP_
void mpff_manager::to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t);
}
#endif
void mpff_manager::display_raw(std::ostream & out, mpff const & n) const {
if (is_neg(n))

19
src/util/mpff.h
View file

@ -58,9 +58,14 @@ class mpz;
class mpq;
template<bool SYNCH> class mpz_manager;
template<bool SYNCH> class mpq_manager;
#ifndef _NO_OMP_
typedef mpz_manager<true> synch_mpz_manager;
typedef mpz_manager<false> unsynch_mpz_manager;
typedef mpq_manager<true> synch_mpq_manager;
#else
typedef mpz_manager<false> synch_mpz_manager;
typedef mpq_manager<false> synch_mpq_manager;
#endif
typedef mpz_manager<false> unsynch_mpz_manager;
typedef mpq_manager<false> unsynch_mpq_manager;
class mpff_manager {
@ -213,7 +218,9 @@ public:
\brief Return the significand as a mpz numeral.
*/
void significand(mpff const & n, unsynch_mpz_manager & m, mpz & r);
#ifndef _NO_OMP_
void significand(mpff const & n, synch_mpz_manager & m, mpz & r);
#endif
/**
\brief Return true if n is negative
@ -378,9 +385,11 @@ public:
void set(mpff & n, int64_t num, uint64_t den);
void set(mpff & n, mpff const & v);
void set(mpff & n, unsynch_mpz_manager & m, mpz const & v);
void set(mpff & n, synch_mpz_manager & m, mpz const & v);
void set(mpff & n, unsynch_mpq_manager & m, mpq const & v);
#ifndef _NO_OMP_
void set(mpff & n, synch_mpq_manager & m, mpq const & v);
void set(mpff & n, synch_mpz_manager & m, mpz const & v);
#endif
void set_plus_epsilon(mpff & n);
void set_minus_epsilon(mpff & n);
void set_max(mpff & n);
@ -420,6 +429,7 @@ public:
*/
void to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t);
#ifndef _NO_OMP_
/**
\brief Convert n into a mpz numeral.
@ -428,6 +438,7 @@ public:
\remark if exponent(n) is too big, we may run out of memory.
*/
void to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t);
#endif
/**
\brief Convert n into a mpq numeral.
@ -436,13 +447,15 @@ public:
*/
void to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t);
#ifndef _NO_OMP_
/**
\brief Convert n into a mpq numeral.
\remark if exponent(n) is too big, we may run out of memory.
*/
void to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t);
#endif
/**
\brief Return n as an int64.

8
src/util/mpfx.cpp
View file

@ -272,9 +272,11 @@ void mpfx_manager::set(mpfx & n, unsynch_mpz_manager & m, mpz const & v) {
set_core(n, m, v);
}
#ifndef _NO_OMP_
void mpfx_manager::set(mpfx & n, synch_mpz_manager & m, mpz const & v) {
set_core(n, m, v);
}
#endif
template<bool SYNCH>
void mpfx_manager::set_core(mpfx & n, mpq_manager<SYNCH> & m, mpq const & v) {
@ -309,9 +311,11 @@ void mpfx_manager::set(mpfx & n, unsynch_mpq_manager & m, mpq const & v) {
set_core(n, m, v);
}
#ifndef _NO_OMP_
void mpfx_manager::set(mpfx & n, synch_mpq_manager & m, mpq const & v) {
set_core(n, m, v);
}
#endif
bool mpfx_manager::eq(mpfx const & a, mpfx const & b) const {
if (is_zero(a) && is_zero(b))
@ -714,9 +718,11 @@ void mpfx_manager::to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t);
}
#ifndef _NO_OMP_
void mpfx_manager::to_mpz(mpfx const & n, synch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t);
}
#endif
template<bool SYNCH>
void mpfx_manager::to_mpq_core(mpfx const & n, mpq_manager<SYNCH> & m, mpq & t) {
@ -738,9 +744,11 @@ void mpfx_manager::to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t);
}
#ifndef _NO_OMP_
void mpfx_manager::to_mpq(mpfx const & n, synch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t);
}
#endif
void mpfx_manager::display_raw(std::ostream & out, mpfx const & n) const {
if (is_neg(n))

15
src/util/mpfx.h
View file

@ -51,9 +51,14 @@ class mpz;
class mpq;
template<bool SYNCH> class mpz_manager;
template<bool SYNCH> class mpq_manager;
#ifndef _NO_OMP_
typedef mpz_manager<true> synch_mpz_manager;
typedef mpz_manager<false> unsynch_mpz_manager;
typedef mpq_manager<true> synch_mpq_manager;
#else
typedef mpz_manager<false> synch_mpz_manager;
typedef mpq_manager<false> synch_mpq_manager;
#endif
typedef mpz_manager<false> unsynch_mpz_manager;
typedef mpq_manager<false> unsynch_mpq_manager;
class mpfx_manager {
@ -312,9 +317,11 @@ public:
void set(mpfx & n, int64_t num, uint64_t den);
void set(mpfx & n, mpfx const & v);
void set(mpfx & n, unsynch_mpz_manager & m, mpz const & v);
void set(mpfx & n, synch_mpz_manager & m, mpz const & v);
void set(mpfx & n, unsynch_mpq_manager & m, mpq const & v);
#ifndef _NO_OMP_
void set(mpfx & n, synch_mpz_manager & m, mpz const & v);
void set(mpfx & n, synch_mpq_manager & m, mpq const & v);
#endif
/**
\brief Set n to the smallest representable numeral greater than zero.
@ -359,22 +366,26 @@ public:
*/
void to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t);
#ifndef _NO_OMP_
/**
\brief Convert n into a mpz numeral.
\pre is_int(n)
*/
void to_mpz(mpfx const & n, synch_mpz_manager & m, mpz & t);
#endif
/**
\brief Convert n into a mpq numeral.
*/
void to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t);
#ifndef _NO_OMP_
/**
\brief Convert n into a mpq numeral.
*/
void to_mpq(mpfx const & n, synch_mpq_manager & m, mpq & t);
#endif
/**
\brief Return the biggest k s.t. 2^k <= a.

30
src/util/mpq.cpp
View file

@ -26,12 +26,12 @@ mpq_manager<SYNCH>::mpq_manager() {
template<bool SYNCH>
mpq_manager<SYNCH>::~mpq_manager() {
del(m_n_tmp);
del(m_add_tmp1);
del(m_add_tmp2);
del(m_lt_tmp1);
del(m_lt_tmp2);
del(m_addmul_tmp);
del(m_tmp1);
del(m_tmp2);
del(m_tmp3);
del(m_tmp4);
del(m_q_tmp1);
del(m_q_tmp2);
}
@ -68,9 +68,9 @@ bool mpq_manager<SYNCH>::rat_lt(mpq const & a, mpq const & b) {
return r;
}
else {
mul(na, db, m_lt_tmp1);
mul(nb, da, m_lt_tmp2);
return lt(m_lt_tmp1, m_lt_tmp2);
mul(na, db, m_q_tmp1);
mul(nb, da, m_q_tmp2);
return lt(m_q_tmp1, m_q_tmp2);
}
}
@ -384,8 +384,7 @@ void mpq_manager<SYNCH>::rat_mul(mpq const & a, mpq const & b, mpq & c) {
del(tmp2);
}
else {
mpz& g1 = m_n_tmp, &g2 = m_addmul_tmp.m_num, &tmp1 = m_add_tmp1, &tmp2 = m_add_tmp2;
rat_mul(a, b, c, g1, g2, tmp1, tmp2);
rat_mul(a, b, c, m_tmp1, m_tmp2, m_tmp3, m_tmp4);
}
STRACE("rat_mpq", tout << to_string(c) << "\n";);
}
@ -402,8 +401,7 @@ void mpq_manager<SYNCH>::rat_add(mpq const & a, mpq const & b, mpq & c) {
del(g);
}
else {
mpz& g = m_n_tmp, &tmp1 = m_add_tmp1, &tmp2 = m_add_tmp2, &tmp3 = m_addmul_tmp.m_num;
lin_arith_op<false>(a, b, c, g, tmp1, tmp2, tmp3);
lin_arith_op<false>(a, b, c, m_tmp1, m_tmp2, m_tmp3, m_tmp4);
}
STRACE("rat_mpq", tout << to_string(c) << "\n";);
}
@ -420,13 +418,13 @@ void mpq_manager<SYNCH>::rat_sub(mpq const & a, mpq const & b, mpq & c) {
del(g);
}
else {
mpz& g = m_n_tmp, &tmp1 = m_add_tmp1, &tmp2 = m_add_tmp2, &tmp3 = m_addmul_tmp.m_num;
lin_arith_op<true>(a, b, c, g, tmp1, tmp2, tmp3);
lin_arith_op<true>(a, b, c, m_tmp1, m_tmp2, m_tmp3, m_tmp4);
}
STRACE("rat_mpq", tout << to_string(c) << "\n";);
}
#ifndef _NO_OMP_
template class mpq_manager<true>;
#endif
template class mpq_manager<false>;

47
src/util/mpq.h
View file

@ -41,12 +41,12 @@ inline void swap(mpq & m1, mpq & m2) { m1.swap(m2); }
template<bool SYNCH = true>
class mpq_manager : public mpz_manager<SYNCH> {
mpz m_n_tmp;
mpz m_add_tmp1;
mpz m_add_tmp2;
mpq m_addmul_tmp;
mpq m_lt_tmp1;
mpq m_lt_tmp2;
mpz m_tmp1;
mpz m_tmp2;
mpz m_tmp3;
mpz m_tmp4;
mpq m_q_tmp1;
mpq m_q_tmp2;
void reset_denominator(mpq & a) {
del(a.m_den);
@ -66,11 +66,11 @@ class mpq_manager : public mpz_manager<SYNCH> {
del(tmp);
}
else {
gcd(a.m_num, a.m_den, m_n_tmp);
if (is_one(m_n_tmp))
gcd(a.m_num, a.m_den, m_tmp1);
if (is_one(m_tmp1))
return;
div(a.m_num, m_n_tmp, a.m_num);
div(a.m_den, m_n_tmp, a.m_den);
div(a.m_num, m_tmp1, a.m_num);
div(a.m_den, m_tmp1, a.m_den);
}
}
@ -87,9 +87,9 @@ class mpq_manager : public mpz_manager<SYNCH> {
del(tmp1);
}
else {
mul(b, a.m_den, m_add_tmp1);
mul(b, a.m_den, m_tmp1);
set(c.m_den, a.m_den);
add(a.m_num, m_add_tmp1, c.m_num);
add(a.m_num, m_tmp1, c.m_num);
normalize(c);
}
STRACE("rat_mpq", tout << to_string(c) << "\n";);
@ -320,8 +320,8 @@ public:
del(tmp);
}
else {
mul(b,c,m_addmul_tmp);
add(a, m_addmul_tmp, d);
mul(b, c, m_q_tmp1);
add(a, m_q_tmp1, d);
}
}
}
@ -342,8 +342,8 @@ public:
del(tmp);
}
else {
mul(b,c,m_addmul_tmp);
add(a, m_addmul_tmp, d);
mul(b,c, m_q_tmp1);
add(a, m_q_tmp1, d);
}
}
}
@ -365,8 +365,8 @@ public:
del(tmp);
}
else {
mul(b,c,m_addmul_tmp);
sub(a, m_addmul_tmp, d);
mul(b,c, m_q_tmp1);
sub(a, m_q_tmp1, d);
}
}
}
@ -387,8 +387,8 @@ public:
del(tmp);
}
else {
mul(b,c,m_addmul_tmp);
sub(a, m_addmul_tmp, d);
mul(b,c, m_q_tmp1);
sub(a, m_q_tmp1, d);
}
}
}
@ -814,12 +814,13 @@ public:
bool is_even(mpz const & a) { return mpz_manager<SYNCH>::is_even(a); }
public:
bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); }
friend bool operator==(mpq const & a, mpq const & b) ;
friend bool operator>=(mpq const & a, mpq const & b);
};
#ifndef _NO_OMP_
typedef mpq_manager<true> synch_mpq_manager;
#else
typedef mpq_manager<false> synch_mpq_manager;
#endif
typedef mpq_manager<false> unsynch_mpq_manager;
typedef _scoped_numeral<unsynch_mpq_manager> scoped_mpq;

2
src/util/mpq_inf.cpp
View file

@ -39,5 +39,7 @@ std::string mpq_inf_manager<SYNCH>::to_string(mpq_inf const & a) {
}
#ifndef _NO_OMP_
template class mpq_inf_manager<true>;
#endif
template class mpq_inf_manager<false>;

4
src/util/mpq_inf.h
View file

@ -279,7 +279,11 @@ public:
mpq_manager<SYNCH>& get_mpq_manager() { return m; }
};
#ifndef _NO_OMP_
typedef mpq_inf_manager<true> synch_mpq_inf_manager;
#else
typedef mpq_inf_manager<false> synch_mpq_inf_manager;
#endif
typedef mpq_inf_manager<false> unsynch_mpq_inf_manager;
#endif

2
src/util/mpz.cpp
View file

@ -2369,5 +2369,7 @@ bool mpz_manager<SYNCH>::divides(mpz const & a, mpz const & b) {
return r;
}
#ifndef _NO_OMP_
template class mpz_manager<true>;
#endif
template class mpz_manager<false>;

4
src/util/mpz.h
View file

@ -692,7 +692,11 @@ public:
bool decompose(mpz const & n, svector<digit_t> & digits);
};
#ifndef _NO_OMP_
typedef mpz_manager<true> synch_mpz_manager;
#else
typedef mpz_manager<false> synch_mpz_manager;
#endif
typedef mpz_manager<false> unsynch_mpz_manager;
typedef _scoped_numeral<unsynch_mpz_manager> scoped_mpz;