mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fixed: missing library, more compilation errors in debug mode reported by g++ 4.7.1

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-27 22:51:03 -07:00
parent 9fb25e7708
commit ae71a4d514
4 changed files with 27 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
configure.ac
View file

@ -115,6 +115,7 @@ host_os=`uname -s`
AS_IF([test "$host_os" = "Darwin"], [ AS_IF([test "$host_os" = "Darwin"], [
PLATFORM=osx PLATFORM=osx
SO_EXT=.dylib SO_EXT=.dylib
LDFLAGS=
SLIBFLAGS="-dynamiclib -fopenmp" SLIBFLAGS="-dynamiclib -fopenmp"
SLIBEXTRAFLAGS="" SLIBEXTRAFLAGS=""
COMP_VERSIONS="-compatibility_version \$(Z3_VERSION) -current_version \$(Z3_VERSION)" COMP_VERSIONS="-compatibility_version \$(Z3_VERSION) -current_version \$(Z3_VERSION)"
@ -122,6 +123,7 @@ AS_IF([test "$host_os" = "Darwin"], [
], [test "$host_os" = "Linux"], [ ], [test "$host_os" = "Linux"], [
PLATFORM=linux PLATFORM=linux
SO_EXT=.so SO_EXT=.so
LDFLAGS=-lrt
SLIBFLAGS="-shared -fopenmp" SLIBFLAGS="-shared -fopenmp"
SLIBEXTRAFLAGS= SLIBEXTRAFLAGS=
COMP_VERSIONS= COMP_VERSIONS=
@ -140,6 +142,7 @@ AS_IF([test "$host_os" = "Darwin"], [
AC_MSG_ERROR([Unknown host platform: $host_os]) AC_MSG_ERROR([Unknown host platform: $host_os])
]) ])
AC_SUBST(SLIBFLAGS) AC_SUBST(SLIBFLAGS)
AC_SUBST(LDFLAGS)
AC_SUBST(SLIBEXTRAFLAGS) AC_SUBST(SLIBEXTRAFLAGS)
AC_SUBST(SO_EXT) AC_SUBST(SO_EXT)

2
scripts/config-debug.mk.in
View file

@ -10,7 +10,7 @@ AR_FLAGS=rcs
AR_OUTFLAG= AR_OUTFLAG=
EXE_EXT= EXE_EXT=
LINK=@CXX@ LINK=@CXX@
LINK_FLAGS=-lpthread -fopenmp LINK_FLAGS=-lpthread -fopenmp @LDFLAGS@
LINK_OUT_FLAG=-o LINK_OUT_FLAG=-o
SO_EXT=@SO_EXT@ SO_EXT=@SO_EXT@
SLINK=@CXX@ SLINK=@CXX@

2
scripts/config-release.mk.in
View file

@ -10,7 +10,7 @@ AR_FLAGS=rcs
AR_OUTFLAG= AR_OUTFLAG=
EXE_EXT= EXE_EXT=
LINK=@CXX@ LINK=@CXX@
LINK_FLAGS=-lpthread -fopenmp LINK_FLAGS=-lpthread -fopenmp @LDFLAGS@
LINK_OUT_FLAG=-o LINK_OUT_FLAG=-o
SO_EXT=@SO_EXT@ SO_EXT=@SO_EXT@
SLINK=@CXX@ SLINK=@CXX@

40
src/util/interval_skip_list.h
View file

@ -277,7 +277,7 @@ protected:
// the search_key must be in the current bucket, or in the first entry of the next bucket (if the next bucket is not 0). // the search_key must be in the current bucket, or in the first entry of the next bucket (if the next bucket is not 0).
SASSERT(curr->empty() || lt(first_key(curr), k)); SASSERT(curr->empty() || lt(first_key(curr), k));
SASSERT(next == 0 || geq(first_key(next), k)); SASSERT(next == 0 || this->geq(first_key(next), k));
DEBUG_CODE({ DEBUG_CODE({
if (UpdatePredVect && next != 0) if (UpdatePredVect && next != 0)
for (unsigned i = 0; i < next->level(); i++) for (unsigned i = 0; i < next->level(); i++)
@ -327,7 +327,7 @@ protected:
\remark pred_vect contains the predecessors of the successor of bt. \remark pred_vect contains the predecessors of the successor of bt.
*/ */
void merge_first_of_succ_if_possible(manager & m, bucket * bt, bucket * pred_vect[]) { void merge_first_of_succ_if_possible(manager & m, bucket * bt, bucket * pred_vect[]) {
SASSERT(check_pred_vect(bt->get_next(0), pred_vect)); SASSERT(this->check_pred_vect(bt->get_next(0), pred_vect));
bucket * next_bucket = bt->get_next(0); bucket * next_bucket = bt->get_next(0);
if (next_bucket != 0) { if (next_bucket != 0) {
entry & curr_entry = bt->last_entry(); entry & curr_entry = bt->last_entry();
@ -479,7 +479,7 @@ protected:
\brief Keep deleting keys <= k in bt and its successors. \brief Keep deleting keys <= k in bt and its successors.
*/ */
void del_entries_upto_loop(manager & m, bucket * bt, key const & k, bucket * pred_vect []) { void del_entries_upto_loop(manager & m, bucket * bt, key const & k, bucket * pred_vect []) {
SASSERT(check_pred_vect(bt, pred_vect)); SASSERT(this->check_pred_vect(bt, pred_vect));
while (bt != 0) { while (bt != 0) {
key const & bt_last_key = last_key(bt); key const & bt_last_key = last_key(bt);
if (lt(k, bt_last_key)) { if (lt(k, bt_last_key)) {
@ -516,7 +516,7 @@ protected:
*/ */
template<bool INSERT> template<bool INSERT>
bool del_entries_upto(manager & m, bucket * bt, key const & k, bucket * pred_vect[], bucket * next_pred_vect[]) { bool del_entries_upto(manager & m, bucket * bt, key const & k, bucket * pred_vect[], bucket * next_pred_vect[]) {
SASSERT(check_pred_vect(bt, pred_vect)); // pred_vect contains the predecessors of bt. SASSERT(this->check_pred_vect(bt, pred_vect)); // pred_vect contains the predecessors of bt.
if (lt(k, first_key(bt))) { if (lt(k, first_key(bt))) {
// nothing to be done... // nothing to be done...
return false; // didn't manage to recycle entry. return false; // didn't manage to recycle entry.
@ -566,7 +566,7 @@ protected:
*/ */
template<bool INSERT> template<bool INSERT>
bool del_entries_upto(manager & m, bucket * bt, unsigned s_idx, key const & k, bucket * pred_vect[]) { bool del_entries_upto(manager & m, bucket * bt, unsigned s_idx, key const & k, bucket * pred_vect[]) {
SASSERT(check_pred_vect(bt->get_next(0), pred_vect)); // pred_vect contains the predecessors of the successor of bt. SASSERT(this->check_pred_vect(bt->get_next(0), pred_vect)); // pred_vect contains the predecessors of the successor of bt.
SASSERT(s_idx > 0); SASSERT(s_idx > 0);
TRACE("del_entries_upto_bug", TRACE("del_entries_upto_bug",
tout << "INSERT: " << INSERT << "\n"; tout << "INSERT: " << INSERT << "\n";
@ -619,10 +619,10 @@ protected:
*/ */
void insert_begin(manager & m, bucket * bt, key const & b, key const & e, value const & v, bucket * pred_vect[]) { void insert_begin(manager & m, bucket * bt, key const & b, key const & e, value const & v, bucket * pred_vect[]) {
TRACE("interval_skip_list_bug", tout << "insert_begin: [" << b << ", " << e << "] -> " << v << "\n"; this->display(tout, bt);); TRACE("interval_skip_list_bug", tout << "insert_begin: [" << b << ", " << e << "] -> " << v << "\n"; this->display(tout, bt););
SASSERT(check_pred_vect(bt, pred_vect)); SASSERT(this->check_pred_vect(bt, pred_vect));
SASSERT(!bt->empty()); SASSERT(!bt->empty());
SASSERT(bt->size() <= bt->capacity()); SASSERT(bt->size() <= bt->capacity());
SASSERT(leq(b, first_key(bt))); SASSERT(this->leq(b, first_key(bt)));
bucket * next_pred_vect[Traits::max_level]; bucket * next_pred_vect[Traits::max_level];
next_pred_vect[0] = 0; next_pred_vect[0] = 0;
@ -675,7 +675,7 @@ protected:
*/ */
void insert_at(manager & m, bucket * bt, unsigned idx, key const & b, key const & e, value const & v, bucket * pred_vect[]) { void insert_at(manager & m, bucket * bt, unsigned idx, key const & b, key const & e, value const & v, bucket * pred_vect[]) {
SASSERT(idx > 0); SASSERT(idx > 0);
SASSERT(check_pred_vect(bt->get_next(0), pred_vect)); SASSERT(this->check_pred_vect(bt->get_next(0), pred_vect));
this->inc_ref(m, v); this->inc_ref(m, v);
TRACE("insert_at_bug", tout << "before del_entries_upto:\n"; this->display_physical(tout);); TRACE("insert_at_bug", tout << "before del_entries_upto:\n"; this->display_physical(tout););
@ -750,7 +750,7 @@ protected:
*/ */
void insert_inside(manager & m, bucket * bt, key const & b, key const & e, value const & v, bucket * pred_vect[]) { void insert_inside(manager & m, bucket * bt, key const & b, key const & e, value const & v, bucket * pred_vect[]) {
TRACE("interval_skip_list_bug", tout << "insert_inside: [" << b << ", " << e << "] -> " << v << "\n";); TRACE("interval_skip_list_bug", tout << "insert_inside: [" << b << ", " << e << "] -> " << v << "\n";);
SASSERT(check_pred_vect(bt->get_next(0), pred_vect)); SASSERT(this->check_pred_vect(bt->get_next(0), pred_vect));
SASSERT(!bt->empty()); SASSERT(!bt->empty());
SASSERT(bt->size() <= bt->capacity()); SASSERT(bt->size() <= bt->capacity());
// perform binary search to find position to insert [b, e]->v // perform binary search to find position to insert [b, e]->v
@ -833,7 +833,7 @@ protected:
} }
} }
else { else {
SASSERT(eq(b, mid_entry.begin_key())); SASSERT(this->eq(b, mid_entry.begin_key()));
SASSERT(mid > 0); // Reason: insert_begin would have been called instead. SASSERT(mid > 0); // Reason: insert_begin would have been called instead.
insert_at(m, bt, mid, b, e, v, pred_vect); insert_at(m, bt, mid, b, e, v, pred_vect);
} }
@ -919,7 +919,7 @@ protected:
} }
} }
else { else {
SASSERT(eq(b, mid_entry.begin_key())); SASSERT(this->eq(b, mid_entry.begin_key()));
SASSERT(mid > 0); // Reason: remove_begin would have been called instead. SASSERT(mid > 0); // Reason: remove_begin would have been called instead.
del_entries_upto<false>(m, bt, mid, e, pred_vect); del_entries_upto<false>(m, bt, mid, e, pred_vect);
} }
@ -1022,7 +1022,7 @@ private:
SASSERT(pred_vect[i]->get_next(i) == next); SASSERT(pred_vect[i]->get_next(i) == next);
}); });
SASSERT(curr == this->m_header || lt(first_key(curr), k)); SASSERT(curr == this->m_header || lt(first_key(curr), k));
SASSERT(next == 0 || leq(k, first_key(next))); SASSERT(next == 0 || this->leq(k, first_key(next)));
} }
public: public:
@ -1031,7 +1031,7 @@ public:
\brief Insert the entries [i -> v] for every i \in [b, e]. \brief Insert the entries [i -> v] for every i \in [b, e].
*/ */
void insert(manager & m, key const & b, key const & e, value const & v) { void insert(manager & m, key const & b, key const & e, value const & v) {
SASSERT(leq(b, e)); SASSERT(this->leq(b, e));
if (this->empty()) { if (this->empty()) {
insert_first_entry(m, b, e, v); insert_first_entry(m, b, e, v);
return; return;
@ -1059,7 +1059,7 @@ public:
SASSERT(!curr->empty()); SASSERT(!curr->empty());
SASSERT(!next->empty()); SASSERT(!next->empty());
SASSERT(next != 0); SASSERT(next != 0);
SASSERT(eq(first_key(next), b)); SASSERT(this->eq(first_key(next), b));
// Bucket curr is the predecessor of next. // Bucket curr is the predecessor of next.
SASSERT(curr->get_next(0) == next); SASSERT(curr->get_next(0) == next);
@ -1190,7 +1190,7 @@ public:
\brief For each i \in [b, e] remove any entry [i->v] if it is in the list. \brief For each i \in [b, e] remove any entry [i->v] if it is in the list.
*/ */
void remove(manager & m, key const & b, key const & e) { void remove(manager & m, key const & b, key const & e) {
SASSERT(leq(b, e)); SASSERT(this->leq(b, e));
if (this->empty()) if (this->empty())
return; return;
bucket * pred_vect[Traits::max_level]; bucket * pred_vect[Traits::max_level];
@ -1207,7 +1207,7 @@ public:
} }
else { else {
SASSERT(next != 0); SASSERT(next != 0);
SASSERT(eq(first_key(next), b)); SASSERT(this->eq(first_key(next), b));
remove_begin(m, next, b, e, pred_vect); remove_begin(m, next, b, e, pred_vect);
} }
} }
@ -1274,8 +1274,8 @@ public:
for (;;) { for (;;) {
next = curr->get_next(i); next = curr->get_next(i);
if (next != 0 && this->leq(first_key(next), k)) { if (next != 0 && this->leq(first_key(next), k)) {
TRACE("interval_skip_list", tout << "next_bucket(" << k << "), i: " << i << " skipping #" << get_bucket_idx(curr); TRACE("interval_skip_list", tout << "next_bucket(" << k << "), i: " << i << " skipping #" << this->get_bucket_idx(curr);
tout << ", moving to: #" << get_bucket_idx(next) << "\n"; this->display(tout, next);); tout << ", moving to: #" << this->get_bucket_idx(next) << "\n"; this->display(tout, next););
curr = next; curr = next;
if (curr->level() > max) { if (curr->level() > max) {
max = curr->level(); max = curr->level();
@ -1666,7 +1666,7 @@ public:
#ifdef Z3DEBUG #ifdef Z3DEBUG
private: private:
bool check_invariant(entry const & e) const { bool check_invariant(entry const & e) const {
SASSERT(leq(e.begin_key(), e.end_key())); SASSERT(this->leq(e.begin_key(), e.end_key()));
return true; return true;
} }
@ -1705,7 +1705,7 @@ public:
bucket const * next = curr->get_next(i); bucket const * next = curr->get_next(i);
if (next != 0) { if (next != 0) {
SASSERT(next->level() >= i); SASSERT(next->level() >= i);
SASSERT(i == 0 || is_reachable_at_i(curr, next, i-1)); SASSERT(i == 0 || this->is_reachable_at_i(curr, next, i-1));
SASSERT(!next->empty()); SASSERT(!next->empty());
entry const & last_of_curr = curr->last_entry(); entry const & last_of_curr = curr->last_entry();
entry const & first_of_next = next->first_entry(); entry const & first_of_next = next->first_entry();