Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix build on Mac #6146

Merged
merged 3 commits into from
Jul 11, 2022
Merged

Fix build on Mac #6146

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
b0f7172
Fix finding Python on Mac
victorpaleologue Jul 8, 2022
8c793f1
Ignore CMake build directories from index
victorpaleologue Jul 8, 2022
530034d
Fix warning about unused variable in release
victorpaleologue Jul 8, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ bld_rel/*
bld_dbg_x64/*
bld_rel_x64/*
.vscode
*build*/**
# Auto generated files.
config.log
config.status
Expand Down
10 changes: 5 additions & 5 deletions CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -160,7 +160,7 @@ list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:RelWithDebInfo>:_EXTERNAL_RELEAS
################################################################################
# Find Python
################################################################################
find_package(PythonInterp REQUIRED)
find_package(PythonInterp 3 REQUIRED)
message(STATUS "PYTHON_EXECUTABLE: ${PYTHON_EXECUTABLE}")

################################################################################
Expand Down Expand Up @@ -230,7 +230,7 @@ else()
message(FATAL_ERROR "Platform \"${CMAKE_SYSTEM_NAME}\" not recognised")
endif()

list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS
list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS
"${PROJECT_BINARY_DIR}/src"
"${PROJECT_SOURCE_DIR}/src"
)
Expand Down Expand Up @@ -293,8 +293,8 @@ if ((TARGET_ARCHITECTURE STREQUAL "x86_64") OR (TARGET_ARCHITECTURE STREQUAL "i6
set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
elseif (CMAKE_CXX_COMPILER_ID MATCHES "Intel")
set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
# Intel's compiler requires linking with libiomp5
list(APPEND Z3_DEPENDENT_LIBS "iomp5")
# Intel's compiler requires linking with libiomp5
list(APPEND Z3_DEPENDENT_LIBS "iomp5")
elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
set(SSE_FLAGS "/arch:SSE2")
else()
Expand Down Expand Up @@ -624,7 +624,7 @@ install(
################################################################################
# Examples
################################################################################
cmake_dependent_option(Z3_ENABLE_EXAMPLE_TARGETS
cmake_dependent_option(Z3_ENABLE_EXAMPLE_TARGETS
"Build Z3 api examples" ON
"CMAKE_SOURCE_DIR STREQUAL PROJECT_SOURCE_DIR" OFF)
if (Z3_ENABLE_EXAMPLE_TARGETS)
Expand Down
26 changes: 13 additions & 13 deletions src/util/parray.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ class parray_manager {
}

void dec_ref(unsigned sz, value * vs) {
if (C::ref_count)
if (C::ref_count)
for (unsigned i = 0; i < sz; i++)
m_vmanager.dec_ref(vs[i]);
}
Expand Down Expand Up @@ -151,7 +151,7 @@ class parray_manager {
size_t new_capacity = curr_capacity == 0 ? 2 : (3 * curr_capacity + 1) >> 1;
value * new_vs = allocate_values(new_capacity);
if (curr_capacity > 0) {
for (size_t i = 0; i < curr_capacity; i++)
for (size_t i = 0; i < curr_capacity; i++)
new_vs[i] = vs[i];
deallocate_values(vs);
}
Expand All @@ -177,7 +177,7 @@ class parray_manager {
inc_ref(v);
vs[sz] = v;
sz++;
}
}

void rpush_back(cell * c, value const & v) {
SASSERT(c->kind() == ROOT);
Expand Down Expand Up @@ -269,7 +269,7 @@ class parray_manager {
}

value_manager & manager() { return m_vmanager; }

void mk(ref & r) {
dec_ref(r.m_ref);
cell * new_c = mk(ROOT);
Expand All @@ -283,12 +283,12 @@ class parray_manager {
r.m_ref = nullptr;
r.m_updt_counter = 0;
}

void copy(ref const & s, ref & t) {
inc_ref(s.m_ref);
dec_ref(t.m_ref);
t.m_ref = s.m_ref;
t.m_updt_counter = 0;
t.m_updt_counter = 0;
}

unsigned size(ref const & r) const {
Expand All @@ -310,7 +310,7 @@ class parray_manager {
}

void check_size(cell* c) const {
unsigned r;
[[maybe_unused]] unsigned r;
while (c) {
switch (c->kind()) {
case SET:
Expand All @@ -333,7 +333,7 @@ class parray_manager {

value const & get(ref const & r, unsigned i) const {
SASSERT(i < size(r));

unsigned trail_sz = 0;
cell * c = r.m_ref;

Expand Down Expand Up @@ -451,7 +451,7 @@ class parray_manager {
inc_ref(v);
new_c->m_elem = v;
new_c->m_next = r.m_ref;
r.m_ref = new_c;
r.m_ref = new_c;
SASSERT(new_c->m_ref_count == 1);
}

Expand Down Expand Up @@ -536,7 +536,7 @@ class parray_manager {
r.m_updt_counter = 0;
SASSERT(r.root());
}

void reroot(ref & r) {
if (r.root())
return;
Expand All @@ -545,7 +545,7 @@ class parray_manager {
unsigned r_sz = size(r);
unsigned trail_split_idx = r_sz / C::factor;
unsigned i = 0;
cell * c = r.m_ref;
cell * c = r.m_ref;
while (c->kind() != ROOT && i < trail_split_idx) {
cs.push_back(c);
c = c->next();
Expand All @@ -556,7 +556,7 @@ class parray_manager {
unfold(c);
}
DEBUG_CODE(check_size(c););
SASSERT(c->kind() == ROOT);
SASSERT(c->kind() == ROOT);
for (i = cs.size(); i-- > 0; ) {
cell * p = cs[i];
SASSERT(c->m_kind == ROOT);
Expand All @@ -574,7 +574,7 @@ class parray_manager {
case PUSH_BACK:
c->m_kind = POP_BACK;
if (sz == capacity(vs))
expand(vs);
expand(vs);
vs[sz] = p->m_elem;
++sz;
c->m_idx = sz;
Expand Down