mirror of
https://github.com/Z3Prover/z3
synced 2025-04-30 04:15:51 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
Nikolaj Bjorner
commit
376076ea9b
22 changed files with 56 additions and 102 deletions
|
|
@ -1,17 +1,8 @@
|
|||
# Enforce some CMake policies
|
||||
cmake_minimum_required(VERSION 2.8.12)
|
||||
cmake_minimum_required(VERSION 3.4)
|
||||
|
||||
if (POLICY CMP0054)
|
||||
# FIXME: This is horrible. With the old behaviour,
|
||||
# quoted strings like "MSVC" in if() conditionals
|
||||
# get implicitly dereferenced. The NEW behaviour
|
||||
# doesn't do this but CMP0054 was only introduced
|
||||
# in CMake 3.1 and we support lower versions as the
|
||||
# minimum. We could set NEW here but it would be very
|
||||
# confusing to use NEW for some builds and OLD for others
|
||||
# which could lead to some subtle bugs. Instead when the
|
||||
# minimum version is 3.1 change this policy to NEW and remove
|
||||
# the hacks in place to work around it.
|
||||
cmake_policy(SET CMP0054 OLD)
|
||||
cmake_policy(SET CMP0054 NEW)
|
||||
endif()
|
||||
|
||||
if (POLICY CMP0042)
|
||||
|
|
@ -22,13 +13,6 @@ endif()
|
|||
set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
|
||||
project(Z3 CXX)
|
||||
|
||||
if ("${CMAKE_VERSION}" VERSION_LESS "3.4")
|
||||
# FIXME: Drop this when we upgrade to newer CMake versions.
|
||||
# HACK: Although we don't need C language support if it is not
|
||||
# enabled CMake's `FindThreads` module fails in old CMake versions.
|
||||
enable_language(C)
|
||||
endif()
|
||||
|
||||
################################################################################
|
||||
# Project version
|
||||
################################################################################
|
||||
|
|
@ -352,12 +336,11 @@ if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" ST
|
|||
list(APPEND Z3_DEPENDENT_LIBS "iomp5")
|
||||
endif()
|
||||
set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
|
||||
# FIXME: Remove "x.." when CMP0054 is set to NEW
|
||||
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")
|
||||
elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
|
||||
elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
|
||||
set(SSE_FLAGS "/arch:SSE2")
|
||||
else()
|
||||
message(FATAL_ERROR "Unknown compiler ${CMAKE_CXX_COMPILER_ID}")
|
||||
|
|
@ -369,17 +352,6 @@ if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" ST
|
|||
unset(SSE_FLAGS)
|
||||
endif()
|
||||
|
||||
|
||||
|
||||
# FIXME: Remove "x.." when CMP0054 is set to NEW
|
||||
if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
|
||||
# This is the default for MSVC already but to replicate the
|
||||
# python/Makefile build system behaviour this flag is set
|
||||
# explicitly.
|
||||
z3_add_cxx_flag("/fp:precise" REQUIRED)
|
||||
endif()
|
||||
# There doesn't seem to be an equivalent for clang/gcc
|
||||
|
||||
################################################################################
|
||||
# Threading support
|
||||
################################################################################
|
||||
|
|
@ -493,8 +465,7 @@ endif()
|
|||
################################################################################
|
||||
# MSVC specific flags inherited from old build system
|
||||
################################################################################
|
||||
# FIXME: Remove "x.." when CMP0054 is set to NEW
|
||||
if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
|
||||
if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
|
||||
include(${CMAKE_SOURCE_DIR}/cmake/msvc_legacy_quirks.cmake)
|
||||
endif()
|
||||
|
||||
|
|
|
|||
|
|
@ -22,8 +22,7 @@ if (LINK_TIME_OPTIMIZATION)
|
|||
("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
|
||||
set(_lto_compiler_flag "-flto")
|
||||
set(_lto_linker_flag "-flto")
|
||||
# FIXME: Remove "x.." when CMP0054 is set to NEW
|
||||
elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
|
||||
elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
|
||||
set(_lto_compiler_flag "/GL")
|
||||
set(_lto_linker_flag "/LTCG")
|
||||
else()
|
||||
|
|
|
|||
|
|
@ -56,8 +56,7 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
|
|||
list(APPEND WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS})
|
||||
list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS})
|
||||
list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${CLANG_WARNINGS_AS_ERRORS})
|
||||
# FIXME: Remove "x.." when CMP0054 is set to NEW
|
||||
elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
|
||||
elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
|
||||
list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS})
|
||||
|
||||
# CMake's default flags include /W3 already so remove them if
|
||||
|
|
@ -111,8 +110,7 @@ if ("${WARNINGS_AS_ERRORS}" STREQUAL "ON")
|
|||
message(STATUS "Treating compiler warnings as errors")
|
||||
if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
|
||||
list(APPEND Z3_COMPONENT_CXX_FLAGS "-Werror")
|
||||
# FIXME: Remove "x.." when CMP0054 is set to NEW
|
||||
elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
|
||||
elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
|
||||
list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX")
|
||||
else()
|
||||
message(AUTHOR_WARNING "Unknown compiler")
|
||||
|
|
@ -126,8 +124,7 @@ elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "SERIOUS_ONLY")
|
|||
endforeach()
|
||||
elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "OFF")
|
||||
message(STATUS "Not treating compiler warnings as errors")
|
||||
# FIXME: Remove "x.." when CMP0054 is set to NEW
|
||||
if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
|
||||
if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
|
||||
# Warnings as errors is off by default for MSVC so setting this
|
||||
# is not necessary but this duplicates the behaviour of the old
|
||||
# build system.
|
||||
|
|
|
|||
|
|
@ -69,14 +69,6 @@ list(APPEND Z3_COMPONENT_CXX_DEFINES ${Z3_MSVC_LEGACY_DEFINES})
|
|||
################################################################################
|
||||
# Compiler flags
|
||||
################################################################################
|
||||
# By default in MSVC this is on but the old build system set this explicitly so
|
||||
# for completeness set it too.
|
||||
# See https://msdn.microsoft.com/en-us/library/dh8che7s.aspx
|
||||
z3_add_cxx_flag("/Zc:wchar_t" REQUIRED)
|
||||
# By default in MSVC this on but the old build system set this explicitly so
|
||||
# for completeness set it too.
|
||||
z3_add_cxx_flag("/Zc:forScope" REQUIRED)
|
||||
|
||||
# FIXME: We might want to move this out somewhere else if we decide
|
||||
# we want to set `-fno-omit-frame-pointer` for gcc/clang.
|
||||
# No omit frame pointer
|
||||
|
|
@ -106,11 +98,6 @@ if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" ST
|
|||
z3_add_cxx_flag("/Gd" REQUIRED)
|
||||
endif()
|
||||
|
||||
# FIXME: The old build system explicitly disables code analysis.
|
||||
# I don't know why. Duplicate this behaviour for now.
|
||||
# See https://msdn.microsoft.com/en-us/library/ms173498.aspx
|
||||
z3_add_cxx_flag("/analyze-" REQUIRED)
|
||||
|
||||
################################################################################
|
||||
# Linker flags
|
||||
################################################################################
|
||||
|
|
|
|||
|
|
@ -262,18 +262,20 @@ macro(z3_add_install_tactic_rule)
|
|||
GLOBAL
|
||||
PROPERTY Z3_${dependency}_TACTIC_HEADERS
|
||||
)
|
||||
list(APPEND _tactic_header_files ${_component_tactic_header_files})
|
||||
list(APPEND _tactic_header_files "${_component_tactic_header_files}")
|
||||
endforeach()
|
||||
unset(_component_tactic_header_files)
|
||||
|
||||
string(REPLACE ";" "\n" _tactic_header_files "${_tactic_header_files}")
|
||||
file(WRITE "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps" ${_tactic_header_files})
|
||||
add_custom_command(OUTPUT "install_tactic.cpp"
|
||||
COMMAND "${PYTHON_EXECUTABLE}"
|
||||
"${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
|
||||
"${CMAKE_CURRENT_BINARY_DIR}"
|
||||
${_tactic_header_files}
|
||||
"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps"
|
||||
DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
|
||||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
${_tactic_header_files}
|
||||
"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps"
|
||||
COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp\""
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
VERBATIM
|
||||
|
|
|
|||
|
|
@ -14,19 +14,22 @@ def main(args):
|
|||
logging.basicConfig(level=logging.INFO)
|
||||
parser = argparse.ArgumentParser(description=__doc__)
|
||||
parser.add_argument("destination_dir", help="destination directory")
|
||||
parser.add_argument("header_files", nargs="+",
|
||||
help="One or more header files to parse")
|
||||
parser.add_argument("deps", help="file with header file names to parse")
|
||||
pargs = parser.parse_args(args)
|
||||
|
||||
if not mk_genfile_common.check_dir_exists(pargs.destination_dir):
|
||||
return 1
|
||||
|
||||
if not mk_genfile_common.check_files_exist(pargs.header_files):
|
||||
if not mk_genfile_common.check_files_exist([pargs.deps]):
|
||||
return 1
|
||||
|
||||
h_files_full_path = []
|
||||
for header_file in pargs.header_files:
|
||||
h_files_full_path.append(os.path.abspath(header_file))
|
||||
with open(pargs.deps, 'r') as f:
|
||||
lines = f.read().split('\n')
|
||||
h_files_full_path = [os.path.abspath(header_file)
|
||||
for header_file in lines if header_file]
|
||||
|
||||
if not mk_genfile_common.check_files_exist(h_files_full_path):
|
||||
return 1
|
||||
|
||||
output = mk_genfile_common.mk_install_tactic_cpp_internal(
|
||||
h_files_full_path,
|
||||
|
|
|
|||
|
|
@ -2725,7 +2725,7 @@ def mk_config():
|
|||
'SLINK_FLAGS=/nologo /LDd\n' % static_opt)
|
||||
if VS_X64:
|
||||
config.write(
|
||||
'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- %s %s\n' % (extra_opt, static_opt))
|
||||
'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /Gd %s %s\n' % (extra_opt, static_opt))
|
||||
config.write(
|
||||
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
|
||||
'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
|
||||
|
|
@ -2734,7 +2734,7 @@ def mk_config():
|
|||
exit(1)
|
||||
else:
|
||||
config.write(
|
||||
'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 %s %s\n' % (extra_opt, static_opt))
|
||||
'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /Gd /arch:SSE2 %s %s\n' % (extra_opt, static_opt))
|
||||
config.write(
|
||||
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
|
||||
'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
|
||||
|
|
@ -2750,7 +2750,7 @@ def mk_config():
|
|||
extra_opt = '%s /D _TRACE ' % extra_opt
|
||||
if VS_X64:
|
||||
config.write(
|
||||
'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _UNICODE /D UNICODE /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP %s %s\n' % (GL, extra_opt, static_opt))
|
||||
'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _UNICODE /D UNICODE /Gm- /EHsc /GS /Gd /TP %s %s\n' % (GL, extra_opt, static_opt))
|
||||
config.write(
|
||||
'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 %s\n'
|
||||
'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt))
|
||||
|
|
@ -2759,7 +2759,7 @@ def mk_config():
|
|||
exit(1)
|
||||
else:
|
||||
config.write(
|
||||
'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 %s %s\n' % (GL, extra_opt, static_opt))
|
||||
'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /Gd /arch:SSE2 %s %s\n' % (GL, extra_opt, static_opt))
|
||||
config.write(
|
||||
'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
|
||||
'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (LTCG, link_extra_opt, LTCG, maybe_disable_dynamic_base, link_extra_opt))
|
||||
|
|
@ -2903,7 +2903,7 @@ def mk_config():
|
|||
config.write('SO_EXT=%s\n' % SO_EXT)
|
||||
config.write('SLINK=%s\n' % CXX)
|
||||
config.write('SLINK_FLAGS=%s\n' % SLIBFLAGS)
|
||||
config.write('SLINK_EXTRA_FLAGS=%s\n' % SLIBEXTRAFLAGS)
|
||||
config.write('SLINK_EXTRA_FLAGS=-lpthread %s\n' % SLIBEXTRAFLAGS)
|
||||
config.write('SLINK_OUT_FLAG=-o \n')
|
||||
config.write('OS_DEFINES=%s\n' % OS_DEFINES)
|
||||
if is_verbose():
|
||||
|
|
|
|||
|
|
@ -48,7 +48,7 @@ extern "C" {
|
|||
env_params::updt_params();
|
||||
}
|
||||
|
||||
std::string g_Z3_global_param_get_buffer;
|
||||
static std::string g_Z3_global_param_get_buffer;
|
||||
|
||||
Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) {
|
||||
memory::initialize(UINT_MAX);
|
||||
|
|
|
|||
|
|
@ -155,8 +155,6 @@ namespace api {
|
|||
m_error_code = Z3_OK;
|
||||
}
|
||||
|
||||
|
||||
|
||||
void context::check_searching() {
|
||||
if (m_searching) {
|
||||
set_error_code(Z3_INVALID_USAGE, "cannot use function while searching"); // TBD: error code could be fixed.
|
||||
|
|
@ -168,8 +166,8 @@ namespace api {
|
|||
return const_cast<char *>(m_string_buffer.c_str());
|
||||
}
|
||||
|
||||
char * context::mk_external_string(std::string const & str) {
|
||||
m_string_buffer = str;
|
||||
char * context::mk_external_string(std::string && str) {
|
||||
m_string_buffer = std::move(str);
|
||||
return const_cast<char *>(m_string_buffer.c_str());
|
||||
}
|
||||
|
||||
|
|
@ -466,17 +464,11 @@ extern "C" {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
Z3_API char const * Z3_get_error_msg(Z3_context c, Z3_error_code err) {
|
||||
LOG_Z3_get_error_msg(c, err);
|
||||
return _get_error_msg(c, err);
|
||||
}
|
||||
|
||||
Z3_API char const * Z3_get_error_msg_ex(Z3_context c, Z3_error_code err) {
|
||||
return Z3_get_error_msg(c, err);
|
||||
}
|
||||
|
||||
|
||||
void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_set_ast_print_mode(c, mode);
|
||||
|
|
|
|||
|
|
@ -179,7 +179,7 @@ namespace api {
|
|||
// Store a copy of str in m_string_buffer, and return a reference to it.
|
||||
// This method is used to communicate local/internal strings with the "external world"
|
||||
char * mk_external_string(char const * str);
|
||||
char * mk_external_string(std::string const & str);
|
||||
char * mk_external_string(std::string && str);
|
||||
|
||||
// Create a numeral of the given sort
|
||||
expr * mk_numeral_core(rational const & n, sort * s);
|
||||
|
|
|
|||
|
|
@ -189,7 +189,7 @@ extern "C" {
|
|||
std::string result = buffer.str();
|
||||
SASSERT(result.size() > 0);
|
||||
result.resize(result.size()-1);
|
||||
return mk_c(c)->mk_external_string(result);
|
||||
return mk_c(c)->mk_external_string(std::move(result));
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
|
|
@ -207,7 +207,7 @@ extern "C" {
|
|||
std::string result = buffer.str();
|
||||
SASSERT(result.size() > 0);
|
||||
result.resize(result.size()-1);
|
||||
return mk_c(c)->mk_external_string(result);
|
||||
return mk_c(c)->mk_external_string(std::move(result));
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -478,7 +478,7 @@ extern "C" {
|
|||
model_v2_pp(buffer, *(to_model_ref(m)), p.partial());
|
||||
result = buffer.str();
|
||||
}
|
||||
return mk_c(c)->mk_external_string(result);
|
||||
return mk_c(c)->mk_external_string(std::move(result));
|
||||
Z3_CATCH_RETURN(nullptr);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -120,8 +120,7 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_INVALID_ARG, "expression is not a string literal");
|
||||
return "";
|
||||
}
|
||||
std::string s = str.encode();
|
||||
return mk_c(c)->mk_external_string(s);
|
||||
return mk_c(c)->mk_external_string(str.encode());
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ extern "C" {
|
|||
result = buffer.str();
|
||||
SASSERT(result.size() > 0);
|
||||
result.resize(result.size()-1);
|
||||
return mk_c(c)->mk_external_string(result);
|
||||
return mk_c(c)->mk_external_string(std::move(result));
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -28,7 +28,7 @@ Notes:
|
|||
#include "util/uint_set.h"
|
||||
#include "util/gparams.h"
|
||||
|
||||
const unsigned g_primes[7] = { 2, 3, 5, 7, 11, 13, 17};
|
||||
static const unsigned g_primes[7] = { 2, 3, 5, 7, 11, 13, 17};
|
||||
|
||||
|
||||
struct pb2bv_rewriter::imp {
|
||||
|
|
|
|||
|
|
@ -41,14 +41,14 @@ Revision History:
|
|||
|
||||
typedef enum { IN_UNSPECIFIED, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_LP, IN_Z3_LOG, IN_MPS } input_kind;
|
||||
|
||||
std::string g_aux_input_file;
|
||||
char const * g_input_file = nullptr;
|
||||
bool g_standard_input = false;
|
||||
input_kind g_input_kind = IN_UNSPECIFIED;
|
||||
static std::string g_aux_input_file;
|
||||
static char const * g_input_file = nullptr;
|
||||
static bool g_standard_input = false;
|
||||
static input_kind g_input_kind = IN_UNSPECIFIED;
|
||||
bool g_display_statistics = false;
|
||||
bool g_display_istatistics = false;
|
||||
static bool g_display_istatistics = false;
|
||||
|
||||
void error(const char * msg) {
|
||||
static void error(const char * msg) {
|
||||
std::cerr << "Error: " << msg << "\n";
|
||||
std::cerr << "For usage information: z3 -h\n";
|
||||
exit(ERR_CMD_LINE);
|
||||
|
|
@ -114,7 +114,7 @@ void display_usage() {
|
|||
std::cout << "Use 'z3 -p' for the complete list of global and module parameters.\n";
|
||||
}
|
||||
|
||||
void parse_cmd_line_args(int argc, char ** argv) {
|
||||
static void parse_cmd_line_args(int argc, char ** argv) {
|
||||
long timeout = 0;
|
||||
int i = 1;
|
||||
char * eq_pos = nullptr;
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ extern void gparams_register_modules();
|
|||
static char const * g_old_params_names[] = {
|
||||
"arith_adaptive","arith_adaptive_assertion_threshold","arith_adaptive_gcd","arith_adaptive_propagation_threshold","arith_add_binary_bounds","arith_blands_rule_threshold","arith_branch_cut_ratio","arith_dump_lemmas","arith_eager_eq_axioms","arith_eager_gcd","arith_eq_bounds","arith_euclidean_solver","arith_expand_eqs","arith_force_simplex","arith_gcd_test","arith_ignore_int","arith_lazy_adapter","arith_lazy_pivoting","arith_max_lemma_size","arith_process_all_eqs","arith_propagate_eqs","arith_propagation_mode","arith_propagation_threshold","arith_prop_strategy","arith_random_initial_value","arith_random_lower","arith_random_seed","arith_random_upper","arith_reflect","arith_skip_big_coeffs","arith_small_lemma_size","arith_solver","arith_stronger_lemmas","array_always_prop_upward","array_canonize","array_cg","array_delay_exp_axiom","array_extensional","array_laziness","array_lazy_ieq","array_lazy_ieq_delay","array_solver","array_weak","async_commands","at_labels_cex","auto_config","bb_eager","bb_ext_gates","bb_quantifiers","bin_clauses","bit2int","bv2int_distribute","bv_blast_max_size","bv_cc","bv_enable_int2bv_propagation","bv_lazy_le","bv_max_sharing","bv_reflect","bv_solver","case_split","check_at_labels","check_proof","cnf_factor","cnf_mode","context_simplifier","dack","dack_eq","dack_factor","dack_gc","dack_gc_inv_decay","dack_threshold","default_qid","default_table","default_table_checked","delay_units","delay_units_threshold","der","display_config","display_dot_proof","display_error_for_visual_studio","display_features","display_proof","display_unsat_core","distribute_forall","dt_lazy_splits","dump_goal_as_smt","elim_and","elim_bounds","elim_nlarith_quantifiers","elim_quantifiers","elim_term_ite","ematching","engine","eq_propagation","hi_div0","ignore_bad_patterns","ignore_setparameter","instruction_max","inst_gen","interactive","internalizer_nnf","lemma_gc_factor","lemma_gc_half","lemma_gc_initial","lemma_gc_new_clause_activity","lemma_gc_new_clause_relevancy","lemma_gc_new_old_ratio","lemma_gc_old_clause_activity","lemma_gc_old_clause_relevancy","lemma_gc_strategy","lift_ite","lookahead_diseq","macro_finder","max_conflicts","max_counterexamples","mbqi","mbqi_force_template","mbqi_max_cexs","mbqi_max_cexs_incr","mbqi_max_iterations","mbqi_trace","minimize_lemmas","model","model_compact","model_completion","model_display_arg_sort","model_hide_unused_partitions","model_on_final_check","model_on_timeout","model_partial","model_v1","model_v2","model_validate","new_core2th_eq","ng_lift_ite","nl_arith","nl_arith_branching","nl_arith_gb","nl_arith_gb_eqs","nl_arith_gb_perturbate","nl_arith_gb_threshold","nl_arith_max_degree","nl_arith_rounds","nnf_factor","nnf_ignore_labels","nnf_mode","nnf_sk_hack","order","order_var_weight","order_weights","phase_selection","pi_arith","pi_arith_weight","pi_avoid_skolems","pi_block_looop_patterns","pi_max_multi_patterns","pi_non_nested_arith_weight","pi_nopat_weight","pi_pull_quantifiers","pi_use_database","pi_warnings","pp_bounded","pp_bv_literals","pp_bv_neg","pp_decimal","pp_decimal_precision","pp_fixed_indent","pp_flat_assoc","pp_max_depth","pp_max_indent","pp_max_num_lines","pp_max_ribbon","pp_max_width","pp_min_alias_size","pp_simplify_implies","pp_single_line","precedence","precedence_gen","pre_demodulator","pre_simplifier","pre_simplify_expr","profile_res_sub","progress_sampling_freq","proof_mode","propagate_booleans","propagate_values","pull_cheap_ite_trees","pull_nested_quantifiers","qi_conservative_final_check","qi_cost","qi_eager_threshold","qi_lazy_instantiation","qi_lazy_quick_checker","qi_lazy_threshold","qi_max_eager_multi_patterns","qi_max_instances","qi_max_lazy_multi_pattern_matching","qi_new_gen","qi_profile","qi_profile_freq","qi_promote_unsat","qi_quick_checker","quasi_macros","random_case_split_freq","random_initial_activity","random_seed","recent_lemma_threshold","reduce_args","refine_inj_axiom","relevancy","relevancy_lemma","rel_case_split_order","restart_adaptive","restart_agility_threshold","restart_factor","restart_initial","restart_strategy","restricted_quasi_macros","simplify_clauses","smtlib2_compliant","smtlib_category","smtlib_dump_lemmas","smtlib_logic","smtlib_source_info","smtlib_trace_path","soft_timeout","solver","spc_bs","spc_es","spc_factor_subsumption_index_opt","spc_initial_subsumption_index_opt","spc_max_subsumption_index_features","spc_min_func_freq_subsumption_index","spc_num_iterations","spc_trace","statistics","strong_context_simplifier","tick","trace","trace_file_name","type_check","user_theory_persist_axioms","user_theory_preprocess_axioms","verbose","warning","well_sorted_check","z3_solver_ll_pp","z3_solver_smt_pp", nullptr };
|
||||
|
||||
bool is_old_param_name(symbol const & name) {
|
||||
static bool is_old_param_name(symbol const & name) {
|
||||
char const * const * it = g_old_params_names;
|
||||
while (*it) {
|
||||
if (name == *it)
|
||||
|
|
@ -66,7 +66,7 @@ static char const * g_params_renames[] = {
|
|||
"pp_min_alias_size", "pp.min_alias_size",
|
||||
nullptr };
|
||||
|
||||
char const * get_new_param_name(symbol const & p) {
|
||||
static char const * get_new_param_name(symbol const & p) {
|
||||
char const * const * it = g_params_renames;
|
||||
while (*it) {
|
||||
if (p == *it) {
|
||||
|
|
|
|||
|
|
@ -96,7 +96,7 @@ uint64_t prime_generator::operator()(unsigned idx) {
|
|||
return m_primes[idx];
|
||||
}
|
||||
|
||||
prime_generator g_prime_generator;
|
||||
static prime_generator g_prime_generator;
|
||||
|
||||
prime_iterator::prime_iterator(prime_generator * g):m_idx(0) {
|
||||
if (g == nullptr) {
|
||||
|
|
|
|||
|
|
@ -20,9 +20,9 @@ Revision History:
|
|||
#include<iostream>
|
||||
#include "util/scoped_ctrl_c.h"
|
||||
|
||||
scoped_ctrl_c * scoped_ctrl_c::g_obj = nullptr;
|
||||
static scoped_ctrl_c * g_obj = nullptr;
|
||||
|
||||
void scoped_ctrl_c::on_ctrl_c(int) {
|
||||
static void on_ctrl_c(int) {
|
||||
if (g_obj->m_first) {
|
||||
g_obj->m_cancel_eh(CTRL_C_EH_CALLER);
|
||||
if (g_obj->m_once) {
|
||||
|
|
|
|||
|
|
@ -29,8 +29,6 @@ struct scoped_ctrl_c {
|
|||
bool m_enabled;
|
||||
void (STD_CALL *m_old_handler)(int);
|
||||
scoped_ctrl_c * m_old_scoped_ctrl_c;
|
||||
static scoped_ctrl_c * g_obj;
|
||||
static void STD_CALL on_ctrl_c(int);
|
||||
public:
|
||||
// If once == true, then the cancel_eh is invoked only at the first Ctrl-C.
|
||||
// The next time, the old signal handler will take over.
|
||||
|
|
|
|||
|
|
@ -39,6 +39,7 @@ void set_verbose_stream(std::ostream& str) {
|
|||
g_verbose_stream = &str;
|
||||
}
|
||||
|
||||
#ifndef _NO_OMP_
|
||||
#ifdef _WINDOWS
|
||||
static int g_thread_id = 0;
|
||||
#else
|
||||
|
|
@ -57,6 +58,7 @@ bool is_threaded() {
|
|||
#endif
|
||||
return g_is_threaded;
|
||||
}
|
||||
#endif
|
||||
|
||||
std::ostream& verbose_stream() {
|
||||
return *g_verbose_stream;
|
||||
|
|
|
|||
|
|
@ -174,7 +174,11 @@ void set_verbosity_level(unsigned lvl);
|
|||
unsigned get_verbosity_level();
|
||||
std::ostream& verbose_stream();
|
||||
void set_verbose_stream(std::ostream& str);
|
||||
#ifdef _NO_OMP_
|
||||
# define is_threaded() false
|
||||
#else
|
||||
bool is_threaded();
|
||||
#endif
|
||||
|
||||
|
||||
#define IF_VERBOSE(LVL, CODE) { \
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue