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

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-01-13 20:13:29 +01:00
parent e0215400e2 357ec9e7d1
commit 2f0a049df8
4 changed files with 121 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

98
scripts/mk_util.py
View file

@ -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(

36
src/api/api_fpa.cpp
View file

@ -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);
}

9
src/api/z3_fpa.h
View file

@ -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);

16
src/util/mpf.h
View file

@ -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);