diff --git a/scripts/mk_util.py b/scripts/mk_util.py index ed5df106b..3ca0012e7 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -460,7 +460,7 @@ def find_ocaml_find(): print ("Testing %s..." % OCAMLFIND) r = exec_cmd([OCAMLFIND, 'printconf']) if r != 0: - OCAMLFIND='' + OCAMLFIND = '' def find_ml_lib(): global OCAML_LIB @@ -630,6 +630,7 @@ def display_help(exit_code): print(" JDK_HOME JDK installation directory (only relevant if -j or --java option is provided)") print(" JNI_HOME JNI bindings directory (only relevant if -j or --java option is provided)") print(" OCAMLC Ocaml byte-code compiler (only relevant with --ml)") + print(" OCAMLFIND Ocaml find tool (only relevant with --ml)") print(" OCAMLOPT Ocaml native compiler (only relevant with --ml)") print(" OCAML_LIB Ocaml library directory (only relevant with --ml)") print(" CSC C# Compiler (only relevant if .NET bindings are enabled)") @@ -1753,6 +1754,42 @@ class MLComponent(Component): self.stubs = "z3native_stubs" self.sub_dir = os.path.join('api', 'ml') + self.destdir = "" + self.ldconf = "" + # Calling _init_ocamlfind_paths() is postponed to later because + # OCAMLFIND hasn't been checked yet. + + def _install_bindings(self): + # FIXME: Depending on global state is gross. We can't pre-compute this + # in the constructor because we haven't tested for ocamlfind yet + return OCAMLFIND != '' + + def _init_ocamlfind_paths(self): + """ + Initialises self.destdir and self.ldconf + + Do not call this from the MLComponent constructor because OCAMLFIND + has not been checked at that point + """ + if self.destdir != "" and self.ldconf != "": + # Initialisation already done + return + # Use Ocamlfind to get the default destdir and ldconf path + self.destdir = check_output([OCAMLFIND, 'printconf', 'destdir']) + if self.destdir == "": + raise MKException('Failed to get OCaml destdir') + + if not os.path.isdir(self.destdir): + raise MKException('The destdir reported by {ocamlfind} ({destdir}) does not exist'.format(ocamlfind=OCAMLFIND, destdir=self.destdir)) + + self.ldconf = check_output([OCAMLFIND, 'printconf', 'ldconf']) + if self.ldconf == "": + raise MKException('Failed to get OCaml ldconf path') + + def final_info(self): + if not self._install_bindings(): + print("WARNING: Could not find ocamlfind utility. OCaml bindings will not be installed") + def mk_makefile(self, out): if is_ml_enabled(): src_dir = self.to_src_dir @@ -1832,7 +1869,7 @@ class MLComponent(Component): out.write('\n') def mk_install_deps(self, out): - if is_ml_enabled() and OCAMLFIND != '': + if is_ml_enabled() and self._install_bindings(): out.write(get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT) ') out.write(os.path.join(self.sub_dir, 'META ')) out.write(os.path.join(self.sub_dir, 'z3ml.cma ')) @@ -1840,8 +1877,22 @@ class MLComponent(Component): out.write(os.path.join(self.sub_dir, 'z3ml.cmxs ')) def mk_install(self, out): - if is_ml_enabled() and OCAMLFIND != '': - out.write('\t@%s install Z3 %s' % (OCAMLFIND, (os.path.join(self.sub_dir, 'META')))) + if is_ml_enabled() and self._install_bindings(): + self._init_ocamlfind_paths() + in_prefix = self.destdir.startswith(PREFIX) + maybe_stripped_destdir = strip_path_prefix(self.destdir, PREFIX) + # Note that when doing a staged install with DESTDIR that modifying + # OCaml's ``ld.conf`` may fail. Therefore packagers will need to + # make their packages modify it manually at package install time + # as opposed to ``make install`` time. + MakeRuleCmd.make_install_directory(out, + maybe_stripped_destdir, + in_prefix=in_prefix) + out.write('\t@{ocamlfind} install -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3 {metafile}'.format( + ldconf=self.ldconf, + ocamlfind=OCAMLFIND, + ocaml_destdir=self.destdir, + metafile=os.path.join(self.sub_dir, 'META'))) for m in self.modules: out.write(' ' + os.path.join(self.to_src_dir, m) + '.mli') @@ -1859,8 +1910,12 @@ class MLComponent(Component): out.write('\n') def mk_uninstall(self, out): - if is_ml_enabled() and OCAMLFIND != '': - out.write('\t@%s remove Z3\n' % (OCAMLFIND)) + if is_ml_enabled() and self._install_bindings(): + self._init_ocamlfind_paths() + out.write('\t@{ocamlfind} remove -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3\n'.format( + ldconf=self.ldconf, + ocamlfind=OCAMLFIND, + ocaml_destdir=self.destdir)) def main_component(self): return is_ml_enabled() @@ -2175,6 +2230,7 @@ def mk_config(): print('Java Compiler: %s' % JAVAC) if is_ml_enabled(): print('OCaml Compiler: %s' % OCAMLC) + print('OCaml Find tool: %s' % OCAMLFIND) print('OCaml Native: %s' % OCAMLOPT) print('OCaml Library: %s' % OCAML_LIB) else: @@ -2310,6 +2366,7 @@ def mk_config(): print('Java Compiler: %s' % JAVAC) if is_ml_enabled(): print('OCaml Compiler: %s' % OCAMLC) + print('OCaml Find tool: %s' % OCAMLFIND) print('OCaml Native: %s' % OCAMLOPT) print('OCaml Library: %s' % OCAML_LIB) if is_dotnet_enabled(): @@ -3535,6 +3592,15 @@ class MakeRuleCmd(object): # Note: DESTDIR is to support staged installs return "$(DESTDIR)$(PREFIX)/" + @classmethod + def _is_str(cls, obj): + if sys.version_info.major > 2: + # Python 3 or newer. Strings are always unicode and of type str + return isinstance(obj, str) + else: + # Python 2. Has byte-string and unicode representation, allow both + return isinstance(obj, str) or isinstance(obj, unicode) + @classmethod def _install_root(cls, path, in_prefix, out, is_install=True): if not in_prefix: @@ -3553,9 +3619,9 @@ class MakeRuleCmd(object): @classmethod def install_files(cls, out, src_pattern, dest, in_prefix=True): assert len(dest) > 0 - assert isinstance(src_pattern, str) + assert cls._is_str(src_pattern) assert not ' ' in src_pattern - assert isinstance(dest, str) + assert cls._is_str(dest) assert not ' ' in dest assert not os.path.isabs(src_pattern) install_root = cls._install_root(dest, in_prefix, out) @@ -3568,7 +3634,7 @@ class MakeRuleCmd(object): @classmethod def remove_installed_files(cls, out, pattern, in_prefix=True): assert len(pattern) > 0 - assert isinstance(pattern, str) + assert cls._is_str(pattern) assert not ' ' in pattern install_root = cls._install_root(pattern, in_prefix, out, is_install=False) @@ -3579,7 +3645,7 @@ class MakeRuleCmd(object): @classmethod def make_install_directory(cls, out, dir, in_prefix=True): assert len(dir) > 0 - assert isinstance(dir, str) + assert cls._is_str(dir) assert not ' ' in dir install_root = cls._install_root(dir, in_prefix, out) @@ -3593,8 +3659,8 @@ class MakeRuleCmd(object): Returns True iff ``temp_path`` is a path prefix of ``target_as_abs`` """ - assert isinstance(temp_path, str) - assert isinstance(target_as_abs, str) + assert cls._is_str(temp_path) + assert cls._is_str(target_as_abs) assert len(temp_path) > 0 assert len(target_as_abs) > 0 assert os.path.isabs(temp_path) @@ -3610,8 +3676,8 @@ class MakeRuleCmd(object): @classmethod def create_relative_symbolic_link(cls, out, target, link_name): - assert isinstance(target, str) - assert isinstance(link_name, str) + assert cls._is_str(target) + assert cls._is_str(link_name) assert len(target) > 0 assert len(link_name) > 0 assert not os.path.isabs(target) @@ -3648,8 +3714,8 @@ class MakeRuleCmd(object): @classmethod def create_symbolic_link(cls, out, target, link_name): - assert isinstance(target, str) - assert isinstance(link_name, str) + assert cls._is_str(target) + assert cls._is_str(link_name) assert not os.path.isabs(target) cls.write_cmd(out, 'ln -s {target} {install_root}{link_name}'.format( diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index eaffdd226..33c1448e7 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -912,13 +912,19 @@ extern "C" { ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); + family_id fid = mk_c(c)->get_fpa_fid(); + expr * e = to_expr(t); + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } scoped_mpf val(mpfm); bool r = plugin->is_numeral(to_expr(t), val); if (!r || mpfm.is_nan(val)) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - *sgn = (mpfm.is_nan(val)) ? 0 : mpfm.sgn(val); + *sgn = mpfm.sgn(val); return r; Z3_CATCH_RETURN(0); } @@ -943,17 +949,15 @@ extern "C" { return ""; } scoped_mpf val(mpfm); -// app * a = to_app(e); bool r = plugin->is_numeral(e, val); - if (!r || !mpfm.is_regular(val)) { + if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val))) { SET_ERROR_CODE(Z3_INVALID_ARG) return ""; } unsigned sbits = val.get().get_sbits(); scoped_mpq q(mpqm); - scoped_mpz sn(mpzm); - mpfm.sig_normalized(val, sn); - mpqm.set(q, sn); + mpqm.set(q, mpfm.sig(val)); + if (!mpfm.is_denormal(val)) mpqm.add(q, mpfm.m_powers2(sbits - 1), q); mpqm.div(q, mpfm.m_powers2(sbits - 1), q); std::stringstream ss; mpqm.display_decimal(ss, q, sbits); @@ -981,10 +985,11 @@ extern "C" { return 0; } scoped_mpf val(mpfm); -// app * a = to_app(e); bool r = plugin->is_numeral(e, val); const mpz & z = mpfm.sig(val); - if (!r || mpfm.is_regular(val)|| !mpzm.is_uint64(z)) { + if (!r || + !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val)) || + !mpzm.is_uint64(z)) { SET_ERROR_CODE(Z3_INVALID_ARG); *n = 0; return 0; @@ -1012,13 +1017,14 @@ extern "C" { return ""; } scoped_mpf val(mpfm); -// app * a = to_app(e); bool r = plugin->is_numeral(e, val); - if (!r || !mpfm.is_regular(val)) { + if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val))) { SET_ERROR_CODE(Z3_INVALID_ARG); return ""; } - mpf_exp_t exp = mpfm.exp_normalized(val); + mpf_exp_t exp = mpfm.is_zero(val) ? 0 : + mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) : + mpfm.exp(val); std::stringstream ss; ss << exp; return mk_c(c)->mk_external_string(ss.str()); @@ -1031,6 +1037,7 @@ extern "C" { RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); + unsynch_mpz_manager & mpzm = mpfm.mpz_manager(); family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); SASSERT(plugin != 0); @@ -1044,14 +1051,15 @@ extern "C" { return 0; } scoped_mpf val(mpfm); -// app * a = to_app(e); bool r = plugin->is_numeral(e, val); - if (!r || !mpfm.is_regular(val)) { + if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val))) { SET_ERROR_CODE(Z3_INVALID_ARG); *n = 0; return 0; } - *n = mpfm.exp(val); + *n = mpfm.is_zero(val) ? 0 : + mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) : + mpfm.exp(val); return 1; Z3_CATCH_RETURN(0); } diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index b43e19860..510fa0473 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -829,7 +829,8 @@ extern "C" { \param t a floating-point numeral \param sgn sign - Remarks: sets \c sgn to 0 if the literal is NaN or positive and to 1 otherwise. + Remarks: sets \c sgn to 0 if `t' is positive and to 1 otherwise, except for + NaN, which is an invalid argument. def_API('Z3_fpa_get_numeral_sign', BOOL, (_in(CONTEXT), _in(AST), _out(INT))) */ @@ -841,7 +842,7 @@ extern "C" { \param c logical context \param t a floating-point numeral - Remarks: The significand s is always 0 < s < 2.0; the resulting string is long + Remarks: The significand s is always 0.0 <= s < 2.0; the resulting string is long enough to represent the real significand precisely. def_API('Z3_fpa_get_numeral_significand_string', STRING, (_in(CONTEXT), _in(AST))) @@ -869,6 +870,8 @@ extern "C" { \param c logical context \param t a floating-point numeral + Remarks: This function extracts the exponent in `t`, without normalization. + def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST))) */ Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t); @@ -880,6 +883,8 @@ extern "C" { \param t a floating-point numeral \param n exponent + Remarks: This function extracts the exponent in `t`, without normalization. + def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64))) */ Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n); diff --git a/src/util/mpf.h b/src/util/mpf.h index 80d3f4b47..101491e3b 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -155,12 +155,16 @@ public: } const mpf_exp_t & exp(mpf const & x) const { return x.exponent; } mpf_exp_t exp_normalized(mpf const & x) { - mpf t; - set(t, x); - unpack(t, true); - mpf_exp_t r = t.exponent; - del(t); - return r; + if (is_zero(x)) + return 0; + else { + mpf t; + set(t, x); + unpack(t, true); + mpf_exp_t r = t.exponent; + del(t); + return r; + } } bool is_nan(mpf const & x);