mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
Merge branch 'upstream-master' into develop
This commit is contained in:
commit
8029b6b889
|
@ -67,7 +67,6 @@ add_custom_target(api_docs ${ALWAYS_BUILD_DOCS_ARG}
|
|||
${JAVA_API_OPTIONS}
|
||||
DEPENDS
|
||||
${DOC_EXTRA_DEPENDS}
|
||||
BYPRODUCTS "${DOC_DEST_DIR}"
|
||||
COMMENT "Generating documentation"
|
||||
${ADD_CUSTOM_TARGET_USES_TERMINAL_ARG}
|
||||
)
|
||||
|
|
|
@ -103,15 +103,17 @@ def parse_options():
|
|||
TEMP_DIR = pargs.temp_dir
|
||||
OUTPUT_DIRECTORY = pargs.output_dir
|
||||
Z3PY_PACKAGE_PATH = pargs.z3py_package_path
|
||||
if not os.path.exists(Z3PY_PACKAGE_PATH):
|
||||
raise Exception('"{}" does not exist'.format(Z3PY_PACKAGE_PATH))
|
||||
if not os.path.basename(Z3PY_PACKAGE_PATH) == 'z3':
|
||||
raise Exception('"{}" does not end with "z3"'.format(Z3PY_PACKAGE_PATH))
|
||||
Z3PY_ENABLED = not pargs.no_z3py
|
||||
DOTNET_ENABLED = not pargs.no_dotnet
|
||||
JAVA_ENABLED = not pargs.no_java
|
||||
DOTNET_API_SEARCH_PATHS = pargs.dotnet_search_paths
|
||||
JAVA_API_SEARCH_PATHS = pargs.java_search_paths
|
||||
|
||||
if Z3PY_ENABLED:
|
||||
if not os.path.exists(Z3PY_PACKAGE_PATH):
|
||||
raise Exception('"{}" does not exist'.format(Z3PY_PACKAGE_PATH))
|
||||
if not os.path.basename(Z3PY_PACKAGE_PATH) == 'z3':
|
||||
raise Exception('"{}" does not end with "z3"'.format(Z3PY_PACKAGE_PATH))
|
||||
return
|
||||
|
||||
def mk_dir(d):
|
||||
|
|
|
@ -1633,6 +1633,8 @@ class DotNetDLLComponent(Component):
|
|||
|
||||
if not self.key_file is None:
|
||||
print("%s.dll will be signed using key '%s'." % (self.dll_name, self.key_file))
|
||||
if (self.key_file.find(' ') != -1):
|
||||
self.key_file = '"' + self.key_file + '"'
|
||||
cscCmdLine.append('/keyfile:{}'.format(self.key_file))
|
||||
|
||||
cscCmdLine.extend( ['/unsafe+',
|
||||
|
@ -2419,6 +2421,7 @@ def mk_config():
|
|||
FOCI2 = False
|
||||
if GIT_HASH:
|
||||
CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)
|
||||
CXXFLAGS = '%s -std=c++11' % CXXFLAGS
|
||||
CXXFLAGS = '%s -fvisibility=hidden -c' % CXXFLAGS
|
||||
FPMATH = test_fpmath(CXX)
|
||||
CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS)
|
||||
|
@ -2443,8 +2446,8 @@ def mk_config():
|
|||
CXXFLAGS = '%s -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value' % CXXFLAGS
|
||||
sysname, _, _, _, machine = os.uname()
|
||||
if sysname == 'Darwin':
|
||||
SO_EXT = '.dylib'
|
||||
SLIBFLAGS = '-dynamiclib'
|
||||
SO_EXT = '.dylib'
|
||||
SLIBFLAGS = '-dynamiclib'
|
||||
elif sysname == 'Linux':
|
||||
CXXFLAGS = '%s -fno-strict-aliasing -D_LINUX_' % CXXFLAGS
|
||||
OS_DEFINES = '-D_LINUX_'
|
||||
|
|
|
@ -1434,6 +1434,7 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
|
|||
* (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn))
|
||||
*/
|
||||
br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
|
||||
return BR_FAILED;
|
||||
TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";);
|
||||
zstring str_lo, str_hi;
|
||||
if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) {
|
||||
|
|
|
@ -505,7 +505,7 @@ namespace smt {
|
|||
struct var_value_eq {
|
||||
theory_arith & m_th;
|
||||
var_value_eq(theory_arith & th):m_th(th) {}
|
||||
bool operator()(theory_var v1, theory_var v2) const { return m_th.get_value(v1) == m_th.get_value(v2) && m_th.is_int(v1) == m_th.is_int(v2); }
|
||||
bool operator()(theory_var v1, theory_var v2) const { return m_th.get_value(v1) == m_th.get_value(v2) && m_th.is_int_src(v1) == m_th.is_int_src(v2); }
|
||||
};
|
||||
|
||||
typedef int_hashtable<var_value_hash, var_value_eq> var_value_table;
|
||||
|
|
|
@ -2201,16 +2201,19 @@ namespace smt {
|
|||
int num = get_num_vars();
|
||||
for (theory_var v = 0; v < num; v++) {
|
||||
enode * n = get_enode(v);
|
||||
TRACE("func_interp_bug", tout << "#" << n->get_owner_id() << " -> " << m_value[v] << "\n";);
|
||||
if (!is_relevant_and_shared(n))
|
||||
TRACE("func_interp_bug", tout << mk_pp(n->get_owner(), get_manager()) << " -> " << m_value[v] << " root #" << n->get_root()->get_owner_id() << " " << is_relevant_and_shared(n) << "\n";);
|
||||
if (!is_relevant_and_shared(n)) {
|
||||
continue;
|
||||
}
|
||||
theory_var other = null_theory_var;
|
||||
other = m_var_value_table.insert_if_not_there(v);
|
||||
if (other == v)
|
||||
if (other == v) {
|
||||
continue;
|
||||
}
|
||||
enode * n2 = get_enode(other);
|
||||
if (n->get_root() == n2->get_root())
|
||||
if (n->get_root() == n2->get_root()) {
|
||||
continue;
|
||||
}
|
||||
TRACE("func_interp_bug", tout << "adding to assume_eq queue #" << n->get_owner_id() << " #" << n2->get_owner_id() << "\n";);
|
||||
m_assume_eq_candidates.push_back(std::make_pair(other, v));
|
||||
result = true;
|
||||
|
|
Loading…
Reference in a new issue