From a2376b1016e6aed4a76869b735179239cffd65cb Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Mar 2016 22:22:20 +0000 Subject: [PATCH 01/23] Try to fix #510. The breakage was caused by #498. The issue here is that in Python2 ``exec`` is a statement and ``exec`` is a function in Python3. For the ``exec`` statement to work we would need to write ``` exec line.strip(' \n') in exec_globals, None ``` We could write a wrapper function to do the right thing depending on the Python version but a better approach is to actually just use ``eval()`` rather than ``exec()`` because * ``eval()`` is less "evil" than ``exec()`` because it only evaluates a single expression. My testing so far seems to indicate that this is sufficient. * ``eval()`` is function in both Python 2 and 3 so we don't need to specialise the code based on Python version. --- scripts/mk_genfile_common.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 790ce7205..dbb09539e 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -246,7 +246,7 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): def ADD_PROBE(name, descr, cmd): ADD_PROBE_DATA.append((name, descr, cmd)) - exec_globals = { + eval_globals = { 'ADD_TACTIC': ADD_TACTIC, 'ADD_PROBE': ADD_PROBE, } @@ -272,7 +272,7 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): added_include = True fout.write('#include"%s"\n' % h_file) try: - exec(line.strip('\n '), exec_globals) + eval(line.strip('\n '), eval_globals, None) except Exception as e: _logger.error("Failed processing ADD_TACTIC command at '{}'\n{}".format( fullname, line)) @@ -282,7 +282,7 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): added_include = True fout.write('#include"%s"\n' % h_file) try: - exec(line.strip('\n '), exec_globals) + eval(line.strip('\n '), eval_globals, None) except Exception as e: _logger.error("Failed processing ADD_PROBE command at '{}'\n{}".format( fullname, line)) @@ -514,6 +514,6 @@ def mk_hpp_from_pyg(pyg_file, output_dir): 'def_module_params' : def_module_params, } with open(pyg_file, 'r') as fh: - exec(fh.read() + "\n", pyg_globals, None) + eval(fh.read() + "\n", pyg_globals, None) assert len(OUTPUT_HPP_FILE) == 1 return OUTPUT_HPP_FILE[0] From 75af362b2562e792873584a9b043ee656acfcaf0 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Mar 2016 23:27:26 +0000 Subject: [PATCH 02/23] Fix inconsistent emission of ``z3consts.py``. The ordering of emitted enum values is not consistent between python 2 or 3. The root cause of the problem was a dictionary's keys being iterated over which has no defined order. This has been fixed by iterating over the dictionary's items and ordering by values. We could order by key rather than the values but seeing as these represent an enum, ordering by value makes more sense. --- scripts/mk_genfile_common.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index dbb09539e..7ac52738b 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -105,9 +105,9 @@ def mk_z3consts_py_internal(api_files, output_dir): if m: name = words[1] z3consts.write('# enum %s\n' % name) - for k in decls: - i = decls[k] - z3consts.write('%s = %s\n' % (k, i)) + # Iterate over key-value pairs ordered by value + for k, v in sorted(decls.items(), key=lambda pair: pair[1]): + z3consts.write('%s = %s\n' % (k, v)) z3consts.write('\n') mode = SEARCHING elif len(words) <= 2: From 4814555c469bc64821dc01c59abad5cdd4698b06 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 13 Mar 2016 23:00:40 +0000 Subject: [PATCH 03/23] Fix inconsistent emission of ``gparams_register_modules.cpp``, ``install_tactics.cpp`` and ``mem_initialiszer.cpp`` files between the CMake and Python build systems. The problem was that the generated files were * Senstive to the order component directories were traversed * For CMake there are two directories (a source and build directory) for every component rather than a single directory like the Python build system has. To fix this a new function ``sorted_headers_by_component()`` has been added which defines a order that is consistent between both build systems. This function is then used on lists of paths to discovered header files. --- scripts/mk_genfile_common.py | 86 +++++++++++++++++++++++++++--------- 1 file changed, 65 insertions(+), 21 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 7ac52738b..2e2978a61 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -9,6 +9,7 @@ # to avoid having this code depend on the # of the Python build system. import os +import pprint import logging import re import sys @@ -38,6 +39,43 @@ def check_files_exist(files): return False return True +def sorted_headers_by_component(l): + """ + Take a list of header files and sort them by the + path after ``src/``. E.g. for ``src/ast/fpa/fpa2bv_converter.h`` the sorting + key is ``ast/fpa/fpa2bv_converter.h``. + + The sort is done this way because for the CMake build + there are two directories for every component (e.g. + ``/src/ast/fpa`` and ``/src/ast/fpa``). + We don't want to sort based on different ```` + and ```` prefixes so that we can match the Python build + system's behaviour. + """ + assert isinstance(l, list) + def get_key(path): + _logger.debug("get_key({})".format(path)) + path_components = [] + stripped_path = path + assert 'src' in stripped_path.split(os.path.sep) + # Keep stripping off directory components until we hit ``src`` + while os.path.basename(stripped_path) != 'src': + path_components.append(os.path.basename(stripped_path)) + stripped_path = os.path.dirname(stripped_path) + assert len(path_components) > 0 + path_components.reverse() + # For consistency across platforms use ``/`` rather than ``os.sep``. + # This is a sorting key so it doesn't need to a platform suitable + # path + r = '/'.join(path_components) + _logger.debug("return key:'{}'".format(r)) + return r + sorted_headers = sorted(l, key=get_key) + _logger.debug('sorted headers:{}'.format(pprint.pformat(sorted_headers))) + return sorted_headers + + + ############################################################################### # Functions for generating constant declarations for language bindings ############################################################################### @@ -186,28 +224,30 @@ def mk_gparams_register_modules_internal(component_src_dirs, path): reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)') reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)') reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)') + h_files_full_path = [] for component_src_dir in component_src_dirs: h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir)) - for h_file in h_files: - added_include = False - fin = open(os.path.join(component_src_dir, h_file), 'r') + h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files)) + h_files_full_path.extend(h_files) + for h_file in sorted_headers_by_component(h_files_full_path): + added_include = False + with open(h_file, 'r') as fin: for line in fin: m = reg_pat.match(line) if m: if not added_include: added_include = True - fout.write('#include"%s"\n' % h_file) + fout.write('#include"%s"\n' % os.path.basename(h_file)) cmds.append((m.group(1))) m = reg_mod_pat.match(line) if m: if not added_include: added_include = True - fout.write('#include"%s"\n' % h_file) + fout.write('#include"%s"\n' % os.path.basename(h_file)) mod_cmds.append((m.group(1), m.group(2))) m = reg_mod_descr_pat.match(line) if m: mod_descrs.append((m.group(1), m.group(2))) - fin.close() fout.write('void gparams_register_modules() {\n') for code in cmds: fout.write('{ param_descrs d; %s(d); gparams::register_global(d); }\n' % code) @@ -261,16 +301,19 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): fout.write('#include"cmd_context.h"\n') tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)') probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)') - for component_src_dir in component_src_dirs: + h_files_full_path = [] + for component_src_dir in sorted(component_src_dirs): h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir)) - for h_file in h_files: - added_include = False - fin = open(os.path.join(component_src_dir, h_file), 'r') + h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files)) + h_files_full_path.extend(h_files) + for h_file in sorted_headers_by_component(h_files_full_path): + added_include = False + with open(h_file, 'r') as fin: for line in fin: if tactic_pat.match(line): if not added_include: added_include = True - fout.write('#include"%s"\n' % h_file) + fout.write('#include"%s"\n' % os.path.basename(h_file)) try: eval(line.strip('\n '), eval_globals, None) except Exception as e: @@ -280,14 +323,13 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): if probe_pat.match(line): if not added_include: added_include = True - fout.write('#include"%s"\n' % h_file) + fout.write('#include"%s"\n' % os.path.basename(h_file)) try: eval(line.strip('\n '), eval_globals, None) except Exception as e: _logger.error("Failed processing ADD_PROBE command at '{}'\n{}".format( fullname, line)) raise e - fin.close() # First pass will just generate the tactic factories idx = 0 for data in ADD_TACTIC_DATA: @@ -335,31 +377,33 @@ def mk_mem_initializer_cpp_internal(component_src_dirs, path): # ADD_INITIALIZER with priority initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') - for component_src_dir in component_src_dirs: + h_files_full_path = [] + for component_src_dir in sorted(component_src_dirs): h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir)) - for h_file in h_files: - added_include = False - fin = open(os.path.join(component_src_dir, h_file), 'r') + h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files)) + h_files_full_path.extend(h_files) + for h_file in sorted_headers_by_component(h_files_full_path): + added_include = False + with open(h_file, 'r') as fin: for line in fin: m = initializer_pat.match(line) if m: if not added_include: added_include = True - fout.write('#include"%s"\n' % h_file) + fout.write('#include"%s"\n' % os.path.basename(h_file)) initializer_cmds.append((m.group(1), 0)) m = initializer_prio_pat.match(line) if m: if not added_include: added_include = True - fout.write('#include"%s"\n' % h_file) + fout.write('#include"%s"\n' % os.path.basename(h_file)) initializer_cmds.append((m.group(1), int(m.group(2)))) m = finalizer_pat.match(line) if m: if not added_include: added_include = True - fout.write('#include"%s"\n' % h_file) + fout.write('#include"%s"\n' % os.path.basename(h_file)) finalizer_cmds.append(m.group(1)) - fin.close() initializer_cmds.sort(key=lambda tup: tup[1]) fout.write('void mem_initialize() {\n') for (cmd, prio) in initializer_cmds: From 474ce6645ad676b36c7587d6381ac53f021af225 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 14 Mar 2016 08:27:46 +0000 Subject: [PATCH 04/23] Fix omission of CMake build in README.md --- README.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index a3ba1ff24..3985fad27 100644 --- a/README.md +++ b/README.md @@ -5,14 +5,15 @@ under the [MIT license](LICENSE.txt). If you are not familiar with Z3, you can start [here](https://github.com/Z3Prover/z3/wiki#background). -Z3 can be built using [Visual Studio][1] or a [Makefile][2]. It provides -[bindings for several programming languages][3]. +Z3 can be built using [Visual Studio][1], a [Makefile][2] or using [CMake][3]. It provides +[bindings for several programming languages][4]. See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z3. [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang -[3]: #z3-bindings +[3]: #building-z3-using-cmake +[4]: #z3-bindings ## Building Z3 on Windows using Visual Studio Command Prompt From 5463167a84eab728352e906dba08ff0aa670bf27 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 14 Mar 2016 15:52:09 +0000 Subject: [PATCH 05/23] Bugfix for fp.rem (denormal numbers) Fixes #508. --- src/ast/fpa/fpa2bv_converter.cpp | 31 +++++++++++++++++++++++++++---- 1 file changed, 27 insertions(+), 4 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 4a3ec7553..3ae660434 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -980,6 +980,9 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, x = args[0]; y = args[1]; + TRACE("fpa2bv_rem", tout << "X = " << mk_ismt2_pp(x, m) << std::endl; + tout << "Y = " << mk_ismt2_pp(y, m) << std::endl;); + expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m); mk_nan(f, nan); mk_nzero(f, nzero); @@ -1039,6 +1042,15 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, unpack(x, a_sgn, a_sig, a_exp, a_lz, true); unpack(y, b_sgn, b_sig, b_exp, b_lz, true); + dbg_decouple("fpa2bv_rem_a_sgn", a_sgn); + dbg_decouple("fpa2bv_rem_a_sig", a_sig); + dbg_decouple("fpa2bv_rem_a_exp", a_exp); + dbg_decouple("fpa2bv_rem_a_lz", a_lz); + dbg_decouple("fpa2bv_rem_b_sgn", b_sgn); + dbg_decouple("fpa2bv_rem_b_sig", b_sig); + dbg_decouple("fpa2bv_rem_b_exp", b_exp); + dbg_decouple("fpa2bv_rem_b_lz", b_lz); + BVSLT(a_exp, b_exp, c6); v6 = x; @@ -1052,15 +1064,25 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, unsigned int max_exp_diff_ui = (unsigned int)m_mpz_manager.get_uint64(max_exp_diff); m_mpz_manager.del(max_exp_diff); + expr_ref a_exp_ext(m), b_exp_ext(m); + a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp); + b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp); + + expr_ref a_lz_ext(m), b_lz_ext(m); + a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz); + b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz); + expr_ref exp_diff(m); - exp_diff = m_bv_util.mk_bv_sub(a_exp, b_exp); + exp_diff = m_bv_util.mk_bv_sub( + m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext), + m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext)); dbg_decouple("fpa2bv_rem_exp_diff", exp_diff); // CMW: This creates _huge_ bit-vectors, which is potentially sub-optimal, // but calculating this via rem = x - y * nearest(x/y) creates huge circuits. expr_ref huge_sig(m), shifted_sig(m), huge_rem(m); huge_sig = m_bv_util.mk_zero_extend(max_exp_diff_ui, a_sig); - shifted_sig = m_bv_util.mk_bv_shl(huge_sig, m_bv_util.mk_zero_extend(max_exp_diff_ui + sbits - ebits, exp_diff)); + shifted_sig = m_bv_util.mk_bv_shl(huge_sig, m_bv_util.mk_zero_extend(max_exp_diff_ui + sbits - ebits - 2, exp_diff)); huge_rem = m_bv_util.mk_bv_urem(shifted_sig, m_bv_util.mk_zero_extend(max_exp_diff_ui, b_sig)); dbg_decouple("fpa2bv_rem_huge_rem", huge_rem); @@ -1068,7 +1090,8 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, res_sgn = a_sgn; res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits, 0, huge_rem), m_bv_util.mk_numeral(0, 3)); - res_exp = m_bv_util.mk_sign_extend(2, b_exp); + + res_exp = m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext); // CMW: Actual rounding is not necessary here, this is // just convenience to get rid of the extra bits. @@ -2358,7 +2381,7 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) { TRACE("fpa2bv_to_fp_real", tout << "rm: " << mk_ismt2_pp(rm, m) << std::endl << - "x: " << mk_ismt2_pp(x, m) << std::endl;); + "x: " << mk_ismt2_pp(x, m) << std::endl;); SASSERT(m_util.is_float(s)); SASSERT(au().is_real(x) || au().is_int(x)); SASSERT(is_app_of(rm, m_util.get_family_id(), OP_FPA_INTERNAL_RM)); From 176782d62b9b18682ab0957a010525fbd70843fd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Mar 2016 14:38:11 +0000 Subject: [PATCH 06/23] Bugfix for fp.to_ieee_bv for unspecified input/output. --- src/ast/fpa/fpa2bv_converter.cpp | 15 +++++++++++++-- src/ast/fpa/fpa2bv_converter.h | 1 + src/ast/fpa/fpa2bv_rewriter.cpp | 4 +++- src/ast/fpa_decl_plugin.cpp | 2 +- src/ast/rewriter/fpa_rewriter.cpp | 2 ++ 5 files changed, 20 insertions(+), 4 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 3ae660434..ff1d84171 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2925,11 +2925,22 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con mk_ite(c1, v1, v2, result); } +expr_ref fpa2bv_converter::mk_to_ieee_bv_unspecified(unsigned width) { + if (m_hi_fp_unspecified) + return expr_ref(m_bv_util.mk_numeral(0, width), m); + else + return expr_ref(m_util.mk_internal_to_ieee_bv_unspecified(width), m); +} + void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); + expr_ref x(m), x_is_nan(m); expr * sgn, * s, * e; - split_fp(args[0], sgn, e, s); - result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s); + x = args[0]; + split_fp(x, sgn, e, s); + mk_is_nan(x, x_is_nan); + result = m.mk_ite(x_is_nan, mk_to_ieee_bv_unspecified(m_bv_util.get_bv_size(x)), + m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s)); } void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) { diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 8dc3dc019..7724d7673 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -136,6 +136,7 @@ public: expr_ref mk_to_ubv_unspecified(unsigned width); expr_ref mk_to_sbv_unspecified(unsigned width); + expr_ref mk_to_ieee_bv_unspecified(unsigned width); expr_ref mk_to_real_unspecified(); void reset(void); diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 710faf447..27fc8ebc7 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -157,7 +157,9 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co case OP_FPA_INTERNAL_BVUNWRAP: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED; + case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: + return BR_FAILED; default: TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 7d0126d06..b89b9970b 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -1060,7 +1060,7 @@ app * fpa_util::mk_internal_to_sbv_unspecified(unsigned width) { app * fpa_util::mk_internal_to_ieee_bv_unspecified(unsigned width) { parameter ps[] = { parameter(width) }; sort * range = m_bv_util.mk_sort(width); - return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, 1, ps, 0, 0, range); + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED, 1, ps, 0, 0, range); } app * fpa_util::mk_internal_to_real_unspecified() { diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 57fb606ba..8352e14ce 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -107,6 +107,8 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 0); st = mk_to_sbv_unspecified(f, result); break; case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: SASSERT(num_args == 0); st = mk_to_real_unspecified(result); break; + case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: + SASSERT(num_args == 0); st = mk_to_ieee_bv_unspecified(f, result); break; case OP_FPA_INTERNAL_BVWRAP: case OP_FPA_INTERNAL_BVUNWRAP: From ce64999ee27c2409c62d1125ecd3e1c1510b386c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Mar 2016 14:50:59 +0000 Subject: [PATCH 07/23] More bugfixes for fp.to_ieee_bv for unspecified input/output --- src/ast/fpa_decl_plugin.cpp | 28 +++++++++++++++++++++++----- src/ast/fpa_decl_plugin.h | 2 ++ 2 files changed, 25 insertions(+), 5 deletions(-) diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index b89b9970b..168d33829 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -693,7 +693,7 @@ func_decl * fpa_decl_plugin::mk_internal_rm(decl_kind k, unsigned num_parameters func_decl * fpa_decl_plugin::mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 1) - m_manager->raise_exception("invalid number of arguments to internal_bv_wrap"); + m_manager->raise_exception("invalid number of arguments to bv_wrap"); if (!is_float_sort(domain[0]) && !is_rm_sort(domain[0])) m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint or RoundingMode sort"); @@ -714,7 +714,7 @@ func_decl * fpa_decl_plugin::mk_internal_bv_wrap(decl_kind k, unsigned num_param func_decl * fpa_decl_plugin::mk_internal_bv_unwrap(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 1) - m_manager->raise_exception("invalid number of arguments to internal_bv_unwrap"); + m_manager->raise_exception("invalid number of arguments to bv_unwrap"); if (!is_sort_of(domain[0], m_bv_fid, BV_SORT)) m_manager->raise_exception("sort mismatch, expected argument of bitvector sort"); if (!is_float_sort(range) && !is_rm_sort(range)) @@ -741,7 +741,7 @@ func_decl * fpa_decl_plugin::mk_internal_to_sbv_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 0) - m_manager->raise_exception("invalid number of arguments to internal_to_sbv_unspecified"); + m_manager->raise_exception("invalid number of arguments to fp.to_sbv_unspecified"); if (num_parameters != 1) m_manager->raise_exception("invalid number of parameters to fp.to_sbv_unspecified; expecting 1"); if (!parameters[0].is_int()) @@ -754,13 +754,29 @@ func_decl * fpa_decl_plugin::mk_internal_to_real_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 0) - m_manager->raise_exception("invalid number of arguments to internal_to_real_unspecified"); + m_manager->raise_exception("invalid number of arguments to fp.to_real_unspecified"); if (!is_sort_of(range, m_arith_fid, REAL_SORT)) - m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort"); + m_manager->raise_exception("sort mismatch, expected range of Real sort"); return m_manager->mk_func_decl(symbol("fp.to_real_unspecified"), 0, domain, m_real_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); } +func_decl * fpa_decl_plugin::mk_internal_to_ieee_bv_unspecified( + decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + if (arity != 0) + m_manager->raise_exception("invalid number of arguments to fp.to_ieee_bv_unspecified"); + if (num_parameters != 1) + m_manager->raise_exception("invalid number of parameters to fp.to_ieee_bv_unspecified; expecting 1"); + if (!parameters[0].is_int()) + m_manager->raise_exception("invalid parameters type provided to fp.to_ieee_bv_unspecified; expecting an integer"); + if (!is_float_sort(domain[0])) + m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort"); + + sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, parameters); + return m_manager->mk_func_decl(symbol("fp.to_ieee_bv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); +} + func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { @@ -846,6 +862,8 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return mk_internal_to_sbv_unspecified(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: return mk_internal_to_real_unspecified(k, num_parameters, parameters, arity, domain, range); + case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: + return mk_internal_to_ieee_bv_unspecified(k, num_parameters, parameters, arity, domain, range); default: m_manager->raise_exception("unsupported floating point operator"); return 0; diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index a667bc6f8..51f6ecf75 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -177,6 +177,8 @@ class fpa_decl_plugin : public decl_plugin { unsigned arity, sort * const * domain, sort * range); func_decl * mk_internal_to_real_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); + func_decl * mk_internal_to_ieee_bv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); virtual void set_manager(ast_manager * m, family_id id); unsigned mk_id(mpf const & v); From a9df4a208faa40bb4f500d2a42cc378d699f1ffd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Mar 2016 14:58:55 +0000 Subject: [PATCH 08/23] More bugfixes for fp.to_ieee_bv for unspecified input/output. Relates to #507 --- src/ast/fpa/fpa2bv_converter.cpp | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index ff1d84171..9ecac1ec9 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2939,8 +2939,17 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * x = args[0]; split_fp(x, sgn, e, s); mk_is_nan(x, x_is_nan); - result = m.mk_ite(x_is_nan, mk_to_ieee_bv_unspecified(m_bv_util.get_bv_size(x)), - m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s)); + + sort * fp_srt = m.get_sort(x); + unsigned ebits = m_util.get_ebits(fp_srt); + unsigned sbits = m_util.get_sbits(fp_srt); + + expr_ref sig_unspec(s, m); + if (sbits > 2) + sig_unspec = m_bv_util.mk_concat(mk_to_ieee_bv_unspecified(sbits - 2), + m_bv_util.mk_numeral(1, 1)); + + result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), m.mk_ite(x_is_nan, sig_unspec, s)); } void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) { From 371573cbff7f56d7088c4a7f7eca6b83eda3f959 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Mar 2016 15:11:37 +0000 Subject: [PATCH 09/23] More implementation of fp.to_ieee_bv for unspecified input/output Relates to #507 --- src/ast/fpa/fpa2bv_converter.cpp | 7 +++++-- src/ast/rewriter/fpa_rewriter.cpp | 26 +++++++++++++++++--------- src/util/mpf.cpp | 26 ++++++++++++++++++-------- 3 files changed, 40 insertions(+), 19 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 9ecac1ec9..b4c346170 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2946,8 +2946,11 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * expr_ref sig_unspec(s, m); if (sbits > 2) - sig_unspec = m_bv_util.mk_concat(mk_to_ieee_bv_unspecified(sbits - 2), - m_bv_util.mk_numeral(1, 1)); + sig_unspec = m_bv_util.mk_concat( + mk_to_ieee_bv_unspecified(sbits - 2), + m_bv_util.mk_numeral(1, 1)); + else + sig_unspec = m_bv_util.mk_numeral(1, 1); result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), m.mk_ite(x_is_nan, sig_unspec, s)); } diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 8352e14ce..5d9175259 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -158,8 +158,15 @@ br_status fpa_rewriter::mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & resu if (m_hi_fp_unspecified) // The "hardware interpretation" is 0. result = bu.mk_numeral(0, bv_sz); - else - result = m_util.mk_internal_to_ieee_bv_unspecified(bv_sz); + else { + unsigned sbits = m_util.get_sbits(f->get_domain()[0]); + + if (sbits > 2) + result = bu.mk_concat(m_util.mk_internal_to_ieee_bv_unspecified(sbits - 2), + bu.mk_numeral(1, 1)); + else + result = bu.mk_numeral(1, 1); + } return BR_DONE; } @@ -863,16 +870,17 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu if (m_util.is_numeral(arg, v)) { - if (m_fm.is_nan(v) || m_fm.is_inf(v)) { + if (m_fm.is_nan(v)) { mk_to_ieee_bv_unspecified(f, result); return BR_REWRITE_FULL; } - - bv_util bu(m()); - scoped_mpz rz(m_fm.mpq_manager()); - m_fm.to_ieee_bv_mpz(v, rz); - result = bu.mk_numeral(rational(rz), v.get().get_ebits() + v.get().get_sbits()); - return BR_DONE; + else { + bv_util bu(m()); + scoped_mpz rz(m_fm.mpq_manager()); + m_fm.to_ieee_bv_mpz(v, rz); + result = bu.mk_numeral(rational(rz), v.get().get_ebits() + v.get().get_sbits()); + return BR_DONE; + } } return BR_FAILED; diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 1d7ed1bb3..5de4c406a 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1190,18 +1190,28 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o } void mpf_manager::to_ieee_bv_mpz(const mpf & x, scoped_mpz & o) { - SASSERT(!is_nan(x) && !is_inf(x)); + SASSERT(!is_nan(x)); SASSERT(exp(x) < INT_MAX); unsigned sbits = x.get_sbits(); unsigned ebits = x.get_ebits(); - scoped_mpz biased_exp(m_mpz_manager); - m_mpz_manager.set(biased_exp, bias_exp(ebits, exp(x))); - m_mpz_manager.set(o, sgn(x)); - m_mpz_manager.mul2k(o, ebits); - m_mpz_manager.add(o, biased_exp, o); - m_mpz_manager.mul2k(o, sbits - 1); - m_mpz_manager.add(o, sig(x), o); + + if (is_inf(x)) { + m_mpz_manager.set(o, sgn(x)); + m_mpz_manager.mul2k(o, ebits); + const mpz & exp = m_powers2.m1(ebits); + m_mpz_manager.add(o, exp, o); + m_mpz_manager.mul2k(o, sbits - 1); + } + else { + scoped_mpz biased_exp(m_mpz_manager); + m_mpz_manager.set(biased_exp, bias_exp(ebits, exp(x))); + m_mpz_manager.set(o, sgn(x)); + m_mpz_manager.mul2k(o, ebits); + m_mpz_manager.add(o, biased_exp, o); + m_mpz_manager.mul2k(o, sbits - 1); + m_mpz_manager.add(o, sig(x), o); + } } void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) { From 3101d281e4ff03ab65954e25d665879899de65ce Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Mar 2016 15:12:54 +0000 Subject: [PATCH 10/23] Removed unused variable --- src/ast/fpa/fpa2bv_converter.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index b4c346170..7cd470312 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2941,7 +2941,6 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * mk_is_nan(x, x_is_nan); sort * fp_srt = m.get_sort(x); - unsigned ebits = m_util.get_ebits(fp_srt); unsigned sbits = m_util.get_sbits(fp_srt); expr_ref sig_unspec(s, m); From 99d7a47f82fed5ceaeaa396dd5ed812c817ab576 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Mar 2016 21:45:54 +0000 Subject: [PATCH 11/23] Bugfixes for unspecified results from fp.to_* (models are still incomplete). Relates to #507 --- src/ast/fpa/fpa2bv_converter.cpp | 89 +++++++++++++++-------- src/ast/fpa/fpa2bv_converter.h | 8 +- src/ast/fpa_decl_plugin.cpp | 67 +++++++++-------- src/ast/fpa_decl_plugin.h | 8 +- src/ast/rewriter/fpa_rewriter.cpp | 88 +++++++++++++--------- src/ast/rewriter/fpa_rewriter.h | 2 +- src/tactic/fpa/fpa2bv_model_converter.cpp | 32 ++++++++ src/tactic/fpa/fpa2bv_model_converter.h | 9 +++ 8 files changed, 196 insertions(+), 107 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 7cd470312..20d04ebe6 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2647,8 +2647,8 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;); result = m.mk_ite(x_is_zero, zero, res); - result = m.mk_ite(x_is_inf, mk_to_real_unspecified(), result); - result = m.mk_ite(x_is_nan, mk_to_real_unspecified(), result); + result = m.mk_ite(x_is_inf, mk_to_real_unspecified(ebits, sbits), result); + result = m.mk_ite(x_is_nan, mk_to_real_unspecified(ebits, sbits), result); SASSERT(is_well_sorted(m, result)); } @@ -2925,13 +2925,6 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con mk_ite(c1, v1, v2, result); } -expr_ref fpa2bv_converter::mk_to_ieee_bv_unspecified(unsigned width) { - if (m_hi_fp_unspecified) - return expr_ref(m_bv_util.mk_numeral(0, width), m); - else - return expr_ref(m_util.mk_internal_to_ieee_bv_unspecified(width), m); -} - void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); expr_ref x(m), x_is_nan(m); @@ -2941,17 +2934,31 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * mk_is_nan(x, x_is_nan); sort * fp_srt = m.get_sort(x); + unsigned ebits = m_util.get_ebits(fp_srt); unsigned sbits = m_util.get_sbits(fp_srt); - expr_ref sig_unspec(s, m); - if (sbits > 2) - sig_unspec = m_bv_util.mk_concat( - mk_to_ieee_bv_unspecified(sbits - 2), - m_bv_util.mk_numeral(1, 1)); - else - sig_unspec = m_bv_util.mk_numeral(1, 1); + expr_ref nanv(m); + if (m_hi_fp_unspecified) + // The "hardware interpretation" is 01...10...01. + nanv = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1), + m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits), + m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2), + m_bv_util.mk_numeral(1, 1)))); + else { + app_ref unspec(m), mask(m); + unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits); + m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); + mask = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1), + m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits), + m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits-2), + m_bv_util.mk_numeral(1, 1)))); + expr * args[2] = { unspec, mask }; + nanv = m_bv_util.mk_bv_or(2, args); + } - result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), m.mk_ite(x_is_nan, sig_unspec, s)); + result = m.mk_ite(x_is_nan, nanv, m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s)); + + SASSERT(is_well_sorted(m, result)); } void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) { @@ -2987,7 +2994,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero))); else c1 = m.mk_or(x_is_nan, x_is_inf); - v1 = mk_to_ubv_unspecified(bv_sz); + v1 = mk_to_ubv_unspecified(ebits, sbits, bv_sz); dbg_decouple("fpa2bv_to_bv_c1", c1); // +-Zero -> 0 @@ -3086,8 +3093,8 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args dbg_decouple("fpa2bv_to_bv_rnd", rnd); - result = m.mk_ite(rnd_has_overflown, mk_to_ubv_unspecified(bv_sz), rnd); - result = m.mk_ite(c_in_limits, result, mk_to_ubv_unspecified(bv_sz)); + result = m.mk_ite(rnd_has_overflown, mk_to_ubv_unspecified(ebits, sbits, bv_sz), rnd); + result = m.mk_ite(c_in_limits, result, mk_to_ubv_unspecified(ebits, sbits, bv_sz)); result = m.mk_ite(c2, v2, result); result = m.mk_ite(c1, v1, result); @@ -3106,25 +3113,43 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg mk_to_bv(f, num, args, true, result); } -expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned width) { +expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { + expr_ref result(m); if (m_hi_fp_unspecified) - return expr_ref(m_bv_util.mk_numeral(0, width), m); - else - return expr_ref(m_util.mk_internal_to_ubv_unspecified(width), m); + result = m_bv_util.mk_numeral(0, width); + else { + app_ref unspec(m); + unspec = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width); + m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); + result = unspec; + } + return result; } -expr_ref fpa2bv_converter::mk_to_sbv_unspecified(unsigned width) { +expr_ref fpa2bv_converter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { + expr_ref result(m); if (m_hi_fp_unspecified) - return expr_ref(m_bv_util.mk_numeral(0, width), m); - else - return expr_ref(m_util.mk_internal_to_sbv_unspecified(width), m); + result = m_bv_util.mk_numeral(0, width); + else { + app_ref unspec(m); + unspec = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width); + m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); + result = unspec; + } + return result; } -expr_ref fpa2bv_converter::mk_to_real_unspecified() { +expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits) { + expr_ref result(m); if (m_hi_fp_unspecified) - return expr_ref(m_arith_util.mk_numeral(rational(0), false), m); - else - return expr_ref(m_util.mk_internal_to_real_unspecified(), m); + result = m_arith_util.mk_numeral(rational(0), false); + else { + app_ref unspec(m); + unspec = m_util.mk_internal_to_real_unspecified(ebits, sbits); + m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); + result = unspec; + } + return result; } void fpa2bv_converter::mk_rm(expr * bv3, expr_ref & result) { diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 7724d7673..2414b2110 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -41,6 +41,7 @@ protected: obj_map m_const2bv; obj_map m_rm_const2bv; obj_map m_uf2bvuf; + obj_hashtable m_unspecified_ufs; obj_map > m_specials; @@ -134,10 +135,9 @@ public: void mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y); - expr_ref mk_to_ubv_unspecified(unsigned width); - expr_ref mk_to_sbv_unspecified(unsigned width); - expr_ref mk_to_ieee_bv_unspecified(unsigned width); - expr_ref mk_to_real_unspecified(); + expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width); + expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width); + expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits); void reset(void); diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 168d33829..511d36e67 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -728,12 +728,12 @@ func_decl * fpa_decl_plugin::mk_internal_to_ubv_unspecified( unsigned arity, sort * const * domain, sort * range) { if (arity != 0) m_manager->raise_exception("invalid number of arguments to fp.to_ubv_unspecified"); - if (num_parameters != 1) - m_manager->raise_exception("invalid number of parameters to fp.to_ubv_unspecified; expecting 1"); - if (!parameters[0].is_int()) - m_manager->raise_exception("invalid parameters type provided to fp.to_ubv_unspecified; expecting an integer"); + if (num_parameters != 3) + m_manager->raise_exception("invalid number of parameters to fp.to_ubv_unspecified; expecting 3"); + if (!parameters[0].is_int() || !parameters[1].is_int() || !parameters[2].is_int()) + m_manager->raise_exception("invalid parameters type provided to fp.to_ubv_unspecified; expecting 3 integers"); - sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, parameters); + sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ¶meters[2]); return m_manager->mk_func_decl(symbol("fp.to_ubv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); } @@ -742,11 +742,12 @@ func_decl * fpa_decl_plugin::mk_internal_to_sbv_unspecified( unsigned arity, sort * const * domain, sort * range) { if (arity != 0) m_manager->raise_exception("invalid number of arguments to fp.to_sbv_unspecified"); - if (num_parameters != 1) - m_manager->raise_exception("invalid number of parameters to fp.to_sbv_unspecified; expecting 1"); - if (!parameters[0].is_int()) - m_manager->raise_exception("invalid parameters type provided to fp.to_sbv_unspecified; expecting an integer"); - sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, parameters); + if (num_parameters != 3) + m_manager->raise_exception("invalid number of parameters to fp.to_sbv_unspecified; expecting 3"); + if (!parameters[0].is_int() || !parameters[1].is_int() || !parameters[2].is_int()) + m_manager->raise_exception("invalid parameters type provided to fp.to_sbv_unspecified; expecting 3 integers"); + + sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ¶meters[2]); return m_manager->mk_func_decl(symbol("fp.to_sbv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); } @@ -755,6 +756,10 @@ func_decl * fpa_decl_plugin::mk_internal_to_real_unspecified( unsigned arity, sort * const * domain, sort * range) { if (arity != 0) m_manager->raise_exception("invalid number of arguments to fp.to_real_unspecified"); + if (num_parameters != 2) + m_manager->raise_exception("invalid number of parameters to fp.to_real_unspecified; expecting 2"); + if (!parameters[0].is_int() || !parameters[1].is_int()) + m_manager->raise_exception("invalid parameters type provided to fp.to_real_unspecified; expecting 2 integers"); if (!is_sort_of(range, m_arith_fid, REAL_SORT)) m_manager->raise_exception("sort mismatch, expected range of Real sort"); @@ -765,16 +770,15 @@ func_decl * fpa_decl_plugin::mk_internal_to_ieee_bv_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 0) - m_manager->raise_exception("invalid number of arguments to fp.to_ieee_bv_unspecified"); - if (num_parameters != 1) - m_manager->raise_exception("invalid number of parameters to fp.to_ieee_bv_unspecified; expecting 1"); - if (!parameters[0].is_int()) - m_manager->raise_exception("invalid parameters type provided to fp.to_ieee_bv_unspecified; expecting an integer"); - if (!is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort"); + m_manager->raise_exception("invalid number of arguments to to_ieee_bv_unspecified; expecting none"); + if (num_parameters != 2) + m_manager->raise_exception("invalid number of parameters to to_ieee_bv_unspecified; expecting 2"); + if (!parameters[0].is_int() || !parameters[1].is_int()) + m_manager->raise_exception("invalid parameters type provided to to_ieee_bv_unspecified; expecting 2 integers"); - sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, parameters); - return m_manager->mk_func_decl(symbol("fp.to_ieee_bv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); + parameter width_p[1] = { parameter(parameters[0].get_int() + parameters[1].get_int()) }; + sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, width_p); + return m_manager->mk_func_decl(symbol("to_ieee_bv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); } @@ -1063,25 +1067,26 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) { return mk_value(v); } -app * fpa_util::mk_internal_to_ubv_unspecified(unsigned width) { - parameter ps[] = { parameter(width) }; +app * fpa_util::mk_internal_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { + parameter ps[] = { parameter(ebits), parameter(sbits), parameter(width) }; sort * range = m_bv_util.mk_sort(width); - return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, 1, ps, 0, 0, range); + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, 3, ps, 0, 0, range); } -app * fpa_util::mk_internal_to_sbv_unspecified(unsigned width) { - parameter ps[] = { parameter(width) }; +app * fpa_util::mk_internal_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { + parameter ps[] = { parameter(ebits), parameter(sbits), parameter(width) }; sort * range = m_bv_util.mk_sort(width); - return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, 1, ps, 0, 0, range); + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, 3, ps, 0, 0, range); } -app * fpa_util::mk_internal_to_ieee_bv_unspecified(unsigned width) { - parameter ps[] = { parameter(width) }; - sort * range = m_bv_util.mk_sort(width); - return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED, 1, ps, 0, 0, range); +app * fpa_util::mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits) { + parameter ps[] = { parameter(ebits), parameter(sbits) }; + sort * range = m_bv_util.mk_sort(ebits+sbits); + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED, 2, ps, 0, 0, range); } -app * fpa_util::mk_internal_to_real_unspecified() { +app * fpa_util::mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits) { + parameter ps[] = { parameter(ebits), parameter(sbits) }; sort * range = m_a_util.mk_real(); - return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, 0, 0, 0, 0, range); + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, 2, ps, 0, 0, range); } diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 51f6ecf75..84eb5168b 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -346,10 +346,10 @@ public: app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FPA_TO_IEEE_BV, arg1); } - app * mk_internal_to_ubv_unspecified(unsigned width); - app * mk_internal_to_sbv_unspecified(unsigned width); - app * mk_internal_to_ieee_bv_unspecified(unsigned width); - app * mk_internal_to_real_unspecified(); + app * mk_internal_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width); + app * mk_internal_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width); + app * mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits); + app * mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits); bool is_wrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); } bool is_unwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVUNWRAP); } diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 5d9175259..b5d8f6754 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -106,7 +106,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: SASSERT(num_args == 0); st = mk_to_sbv_unspecified(f, result); break; case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: - SASSERT(num_args == 0); st = mk_to_real_unspecified(result); break; + SASSERT(num_args == 0); st = mk_to_real_unspecified(f, result); break; case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: SASSERT(num_args == 0); st = mk_to_ieee_bv_unspecified(f, result); break; @@ -122,61 +122,55 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con } br_status fpa_rewriter::mk_to_ubv_unspecified(func_decl * f, expr_ref & result) { - SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_num_parameters() == 3); SASSERT(f->get_parameter(0).is_int()); - unsigned bv_sz = f->get_parameter(0).get_int(); + SASSERT(f->get_parameter(1).is_int()); + SASSERT(f->get_parameter(2).is_int()); + unsigned ebits = f->get_parameter(0).get_int(); + unsigned sbits = f->get_parameter(1).get_int(); + unsigned width = f->get_parameter(2).get_int(); bv_util bu(m()); if (m_hi_fp_unspecified) // The "hardware interpretation" is 0. - result = bu.mk_numeral(0, bv_sz); + result = bu.mk_numeral(0, ebits+sbits); else - result = m_util.mk_internal_to_ubv_unspecified(bv_sz); + result = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width); return BR_DONE; } br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result) { - SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_num_parameters() == 3); SASSERT(f->get_parameter(0).is_int()); - unsigned bv_sz = f->get_parameter(0).get_int(); + SASSERT(f->get_parameter(1).is_int()); + SASSERT(f->get_parameter(2).is_int()); + unsigned ebits = f->get_parameter(0).get_int(); + unsigned sbits = f->get_parameter(1).get_int(); + unsigned width = f->get_parameter(2).get_int(); bv_util bu(m()); if (m_hi_fp_unspecified) // The "hardware interpretation" is 0. - result = bu.mk_numeral(0, bv_sz); + result = bu.mk_numeral(0, ebits+sbits); else - result = m_util.mk_internal_to_sbv_unspecified(bv_sz); + result = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width); return BR_DONE; } -br_status fpa_rewriter::mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result) { - bv_util bu(m()); - unsigned bv_sz = bu.get_bv_size(f->get_range()); +br_status fpa_rewriter::mk_to_real_unspecified(func_decl * f, expr_ref & result) { + SASSERT(f->get_num_parameters() == 2); + SASSERT(f->get_parameter(0).is_int()); + SASSERT(f->get_parameter(1).is_int()); + unsigned ebits = f->get_parameter(0).get_int(); + unsigned sbits = f->get_parameter(1).get_int(); - if (m_hi_fp_unspecified) - // The "hardware interpretation" is 0. - result = bu.mk_numeral(0, bv_sz); - else { - unsigned sbits = m_util.get_sbits(f->get_domain()[0]); - - if (sbits > 2) - result = bu.mk_concat(m_util.mk_internal_to_ieee_bv_unspecified(sbits - 2), - bu.mk_numeral(1, 1)); - else - result = bu.mk_numeral(1, 1); - } - - return BR_DONE; -} - -br_status fpa_rewriter::mk_to_real_unspecified(expr_ref & result) { if (m_hi_fp_unspecified) // The "hardware interpretation" is 0. result = m_util.au().mk_numeral(rational(0), false); else - result = m_util.mk_internal_to_real_unspecified(); + result = m_util.mk_internal_to_real_unspecified(ebits, sbits); return BR_DONE; } @@ -865,20 +859,43 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ return BR_FAILED; } +br_status fpa_rewriter::mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result) { + SASSERT(f->get_num_parameters() == 2); + SASSERT(f->get_parameter(0).is_int()); + SASSERT(f->get_parameter(1).is_int()); + unsigned ebits = f->get_parameter(0).get_int(); + unsigned sbits = f->get_parameter(1).get_int(); + + bv_util bu(m()); + + if (m_hi_fp_unspecified) + // The "hardware interpretation" is 01...10...01. + result = bu.mk_concat(bu.mk_numeral(0, 1), + bu.mk_concat(bu.mk_numeral(-1, ebits), + bu.mk_concat(bu.mk_numeral(0, sbits - 2), + bu.mk_numeral(1, 1)))); + else + result = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits); + + return BR_DONE; +} + br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result) { scoped_mpf v(m_fm); if (m_util.is_numeral(arg, v)) { + bv_util bu(m()); + const mpf & x = v.get(); if (m_fm.is_nan(v)) { - mk_to_ieee_bv_unspecified(f, result); - return BR_REWRITE_FULL; + result = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits()); + return BR_REWRITE1; } else { - bv_util bu(m()); scoped_mpz rz(m_fm.mpq_manager()); m_fm.to_ieee_bv_mpz(v, rz); - result = bu.mk_numeral(rational(rz), v.get().get_ebits() + v.get().get_sbits()); + + result = bu.mk_numeral(rational(rz), x.get_ebits() + x.get_sbits()); return BR_DONE; } } @@ -891,7 +908,8 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) { if (m_util.is_numeral(arg, v)) { if (m_fm.is_nan(v) || m_fm.is_inf(v)) { - result = m_util.mk_internal_to_real_unspecified(); + const mpf & x = v.get(); + result = m_util.mk_internal_to_real_unspecified(x.get_ebits(), x.get_sbits()); } else { scoped_mpq r(m_fm.mpq_manager()); diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index 0889bba72..b71b12120 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -89,7 +89,7 @@ public: br_status mk_to_ubv_unspecified(func_decl * f, expr_ref & result); br_status mk_to_sbv_unspecified(func_decl * f, expr_ref & result); br_status mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result); - br_status mk_to_real_unspecified(expr_ref & result); + br_status mk_to_real_unspecified(func_decl * f, expr_ref & result); }; #endif diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index a41b92b2d..61f6c8549 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -54,6 +54,14 @@ void fpa2bv_model_converter::display(std::ostream & out) { out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " << mk_ismt2_pp(it->m_value.second, m, indent) << ")"; } + for (obj_hashtable::iterator it = m_unspecified_ufs.begin(); + it != m_unspecified_ufs.end(); + it++) + { + const symbol & n = (*it)->get_name(); + unsigned indent = n.size() + 4; + out << n << " "; + } out << ")" << std::endl; } @@ -99,6 +107,14 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator translator.to().inc_ref(v1); translator.to().inc_ref(v2); } + for (obj_hashtable::iterator it = m_unspecified_ufs.begin(); + it != m_unspecified_ufs.end(); + it++) + { + func_decl * k = translator(*it); + res->m_unspecified_ufs.insert(k); + translator.to().inc_ref(k); + } return res; } @@ -367,6 +383,22 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { float_mdl->register_decl(f, flt_fi); } + // fp.to_*_unspecified UFs. + for (obj_hashtable::iterator it = m_unspecified_ufs.begin(); + it != m_unspecified_ufs.end(); + it++) + { + func_decl * f = *it; + + if (bv_mdl->has_interpretation(f)) { + func_interp * val = bv_mdl->get_func_interp(f)->copy(); + TRACE("fpa2bv_mc", tout << "Keeping interpretation for " << mk_ismt2_pp(f, m) << std::endl;); + float_mdl->register_decl(f, val); + } + else + TRACE("fpa2bv_mc", tout << "No interpretation for " << mk_ismt2_pp(f, m) << std::endl;); + } + // Keep all the non-float constants. unsigned sz = bv_mdl->get_num_constants(); for (unsigned i = 0; i < sz; i++) diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 854543f24..589d3c201 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -28,6 +28,7 @@ class fpa2bv_model_converter : public model_converter { obj_map m_rm_const2bv; obj_map m_uf2bvuf; obj_map > m_specials; + obj_hashtable m_unspecified_ufs; public: fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) : m(m) { @@ -63,6 +64,13 @@ public: m.inc_ref(it->m_value.first); m.inc_ref(it->m_value.second); } + for (obj_hashtable::iterator it = conv.m_unspecified_ufs.begin(); + it != conv.m_unspecified_ufs.end(); + it++) + { + m_unspecified_ufs.insert(*it); + m.inc_ref(*it); + } } virtual ~fpa2bv_model_converter() { @@ -76,6 +84,7 @@ public: m.dec_ref(it->m_value.first); m.dec_ref(it->m_value.second); } + dec_ref_collection_values(m, m_unspecified_ufs); } virtual void operator()(model_ref & md, unsigned goal_idx) { From 57265f6eb164e1662497dfe0602ffad3b1781076 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20Mr=C3=A1zek?= Date: Wed, 16 Mar 2016 00:18:49 +0100 Subject: [PATCH 12/23] Add methods for obtaining numeral values in C++ API --- src/api/c++/z3++.h | 76 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 76 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 341684ca6..68122a941 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -622,11 +622,87 @@ namespace z3 { \brief Return true if this expression is a variable. */ bool is_var() const { return kind() == Z3_VAR_AST; } + /** + \brief Return true if expression is an algebraic number. + */ + bool is_algebraic() const { return Z3_is_algebraic_number(ctx(), m_ast); } /** \brief Return true if this expression is well sorted (aka type correct). */ bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; } + + /** + \brief Return string representation of numeral or algebraic number + This method assumes the expression is numeral or algebraic + + \pre is_numeral() || is_algebraic() + */ + std::string get_decimal_string(int precision) const { + assert(is_numeral() || is_algebraic()); + return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision)); + } + + /** + \brief Return int value of numeral, throw if result cannot fit in + machine int + + \pre is_numeral() + */ + int get_numeral_int() const { + assert(is_numeral()); + int result; + Z3_bool state = Z3_get_numeral_int(ctx(), m_ast, &result); + if (state != Z3_TRUE) + throw exception("numeral does not fit in machine int"); + return result; + } + + /** + \brief Return uint value of numeral, throw if result cannot fit in + machine uint + + \pre is_numeral() + */ + unsigned get_numeral_uint() const { + assert(is_numeral()); + unsigned result; + Z3_bool state = Z3_get_numeral_uint(ctx(), m_ast, &result); + if (state != Z3_TRUE) + throw exception("numeral does not fit in machine uint"); + return result; + } + + /** + \brief Return __int64 value of numeral, throw if result cannot fit in + __int64 + + \pre is_numeral() + */ + __int64 get_numeral_int64() const { + assert(is_numeral()); + __int64 result; + Z3_bool state = Z3_get_numeral_int64(ctx(), m_ast, &result); + if (state != Z3_TRUE) + throw exception("numeral does not fit in machine __int64"); + return result; + } + + /** + \brief Return __uint64 value of numeral, throw if result cannot fit in + __uint64 + + \pre is_numeral() + */ + __uint64 get_numeral_uint64() const { + assert(is_numeral()); + __uint64 result; + Z3_bool state = Z3_get_numeral_uint64(ctx(), m_ast, &result); + if (state != Z3_TRUE) + throw exception("numeral does not fit in machine __uint64"); + return result; + } + operator Z3_app() const { assert(is_app()); return reinterpret_cast(m_ast); } From cdc8e1303ae488c35904f8a43b6cb8ba0e00673b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 16 Mar 2016 16:16:29 +0000 Subject: [PATCH 13/23] Bugfix for fp.to_*_unspecified. Fixes #507 --- src/api/api_ast.cpp | 3 +- src/ast/fpa/fpa2bv_converter.cpp | 80 ++++++++++++---- src/ast/fpa/fpa2bv_converter.h | 2 +- src/ast/rewriter/fpa_rewriter.cpp | 37 ++------ src/tactic/fpa/fpa2bv_model_converter.cpp | 110 +++++++++------------- src/tactic/fpa/fpa2bv_model_converter.h | 9 -- 6 files changed, 121 insertions(+), 120 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index e30da1aa1..3e094e082 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1129,7 +1129,7 @@ extern "C" { case Z3_OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX; case Z3_OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE; case Z3_OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE; - + case Z3_OP_RE_PLUS: return Z3_OP_RE_PLUS; case Z3_OP_RE_STAR: return Z3_OP_RE_STAR; case Z3_OP_RE_OPTION: return Z3_OP_RE_OPTION; @@ -1189,6 +1189,7 @@ extern "C" { case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: return Z3_OP_UNINTERPRETED; default: UNREACHABLE(); diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 20d04ebe6..c958fb67f 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2944,17 +2944,8 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits), m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2), m_bv_util.mk_numeral(1, 1)))); - else { - app_ref unspec(m), mask(m); - unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits); - m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); - mask = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1), - m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits), - m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits-2), - m_bv_util.mk_numeral(1, 1)))); - expr * args[2] = { unspec, mask }; - nanv = m_bv_util.mk_bv_or(2, args); - } + else + nanv = mk_to_ieee_bv_unspecified(ebits, sbits); result = m.mk_ite(x_is_nan, nanv, m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s)); @@ -3120,8 +3111,17 @@ expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, else { app_ref unspec(m); unspec = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width); - m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); - result = unspec; + func_decl * unspec_fd = unspec->get_decl(); + func_decl * fd; + if (!m_uf2bvuf.find(unspec_fd, fd)) { + app_ref bvc(m); + bvc = m.mk_fresh_const(0, unspec_fd->get_range()); + fd = bvc->get_decl(); + m_uf2bvuf.insert(unspec_fd, fd); + m.inc_ref(unspec_fd); + m.inc_ref(fd); + } + result = m.mk_const(fd); } return result; } @@ -3133,8 +3133,17 @@ expr_ref fpa2bv_converter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, else { app_ref unspec(m); unspec = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width); - m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); - result = unspec; + func_decl * unspec_fd = unspec->get_decl(); + func_decl * fd; + if (!m_uf2bvuf.find(unspec_fd, fd)) { + app_ref bvc(m); + bvc = m.mk_fresh_const(0, unspec_fd->get_range()); + fd = bvc->get_decl(); + m_uf2bvuf.insert(unspec_fd, fd); + m.inc_ref(unspec_fd); + m.inc_ref(fd); + } + result = m.mk_const(fd); } return result; } @@ -3146,12 +3155,51 @@ expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits else { app_ref unspec(m); unspec = m_util.mk_internal_to_real_unspecified(ebits, sbits); - m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); + func_decl * unspec_fd = unspec->get_decl(); + func_decl * fd; + if (!m_uf2bvuf.find(unspec_fd, fd)) { + app_ref bvc(m); + bvc = m.mk_fresh_const(0, unspec_fd->get_range()); + fd = bvc->get_decl(); + m_uf2bvuf.insert(unspec_fd, fd); + m.inc_ref(unspec_fd); + m.inc_ref(fd); + } + result = m.mk_const(fd); result = unspec; } return result; } +expr_ref fpa2bv_converter::mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits) { + expr_ref result(m); + + app_ref unspec(m); + unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits); + func_decl * unspec_fd = unspec->get_decl(); + func_decl * fd; + if (!m_uf2bvuf.find(unspec_fd, fd)) { + app_ref bvc(m); + bvc = m.mk_fresh_const(0, unspec_fd->get_range()); + fd = bvc->get_decl(); + m_uf2bvuf.insert(unspec_fd, fd); + m.inc_ref(unspec_fd); + m.inc_ref(fd); + } + result = m.mk_const(fd); + + app_ref mask(m), extra(m); + mask = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1), + m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits), + m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2), + m_bv_util.mk_numeral(1, 1)))); + expr * args[2] = { result, mask }; + extra = m.mk_eq(m.mk_app(m_bv_util.get_fid(), OP_BAND, 2, args), mask); + m_extra_assertions.push_back(extra); + + return result; +} + void fpa2bv_converter::mk_rm(expr * bv3, expr_ref & result) { SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3); result = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_RM, 0, 0, 1, &bv3, m_util.mk_rm_sort()); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 2414b2110..f69351cb2 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -41,7 +41,6 @@ protected: obj_map m_const2bv; obj_map m_rm_const2bv; obj_map m_uf2bvuf; - obj_hashtable m_unspecified_ufs; obj_map > m_specials; @@ -138,6 +137,7 @@ public: expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width); expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width); expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits); + expr_ref mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits); void reset(void); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index b5d8f6754..83372bcf4 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -102,13 +102,10 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_INTERNAL_RM: SASSERT(num_args == 1); st = mk_rm(args[0], result); break; case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: - SASSERT(num_args == 0); st = mk_to_ubv_unspecified(f, result); break; case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: - SASSERT(num_args == 0); st = mk_to_sbv_unspecified(f, result); break; case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: - SASSERT(num_args == 0); st = mk_to_real_unspecified(f, result); break; case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: - SASSERT(num_args == 0); st = mk_to_ieee_bv_unspecified(f, result); break; + st = BR_FAILED; case OP_FPA_INTERNAL_BVWRAP: case OP_FPA_INTERNAL_BVUNWRAP: @@ -859,27 +856,6 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ return BR_FAILED; } -br_status fpa_rewriter::mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result) { - SASSERT(f->get_num_parameters() == 2); - SASSERT(f->get_parameter(0).is_int()); - SASSERT(f->get_parameter(1).is_int()); - unsigned ebits = f->get_parameter(0).get_int(); - unsigned sbits = f->get_parameter(1).get_int(); - - bv_util bu(m()); - - if (m_hi_fp_unspecified) - // The "hardware interpretation" is 01...10...01. - result = bu.mk_concat(bu.mk_numeral(0, 1), - bu.mk_concat(bu.mk_numeral(-1, ebits), - bu.mk_concat(bu.mk_numeral(0, sbits - 2), - bu.mk_numeral(1, 1)))); - else - result = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits); - - return BR_DONE; -} - br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result) { scoped_mpf v(m_fm); @@ -888,8 +864,15 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu const mpf & x = v.get(); if (m_fm.is_nan(v)) { - result = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits()); - return BR_REWRITE1; + if (m_hi_fp_unspecified) { + result = bu.mk_concat(bu.mk_numeral(0, 1), + bu.mk_concat(bu.mk_numeral(-1, x.get_ebits()), + bu.mk_concat(bu.mk_numeral(0, x.get_sbits() - 2), + bu.mk_numeral(1, 1)))); + } + else + result = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits()); + return BR_REWRITE_FULL; } else { scoped_mpz rz(m_fm.mpq_manager()); diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 61f6c8549..627e33a7b 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -54,15 +54,6 @@ void fpa2bv_model_converter::display(std::ostream & out) { out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " << mk_ismt2_pp(it->m_value.second, m, indent) << ")"; } - for (obj_hashtable::iterator it = m_unspecified_ufs.begin(); - it != m_unspecified_ufs.end(); - it++) - { - const symbol & n = (*it)->get_name(); - unsigned indent = n.size() + 4; - out << n << " "; - } - out << ")" << std::endl; } model_converter * fpa2bv_model_converter::translate(ast_translation & translator) { @@ -107,14 +98,6 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator translator.to().inc_ref(v1); translator.to().inc_ref(v2); } - for (obj_hashtable::iterator it = m_unspecified_ufs.begin(); - it != m_unspecified_ufs.end(); - it++) - { - func_decl * k = translator(*it); - res->m_unspecified_ufs.insert(k); - translator.to().inc_ref(k); - } return res; } @@ -337,66 +320,61 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { func_decl * f = it->m_key; unsigned arity = f->get_arity(); sort * rng = f->get_range(); - func_interp * flt_fi = alloc(func_interp, m, f->get_arity()); - func_interp * bv_fi = bv_mdl->get_func_interp(it->m_value); - SASSERT(bv_fi->args_are_values()); + if (arity > 0) { + func_interp * flt_fi = alloc(func_interp, m, f->get_arity()); - for (unsigned i = 0; i < bv_fi->num_entries(); i++) { - func_entry const * bv_fe = bv_fi->get_entry(i); - expr * const * bv_args = bv_fe->get_args(); - expr_ref_buffer new_args(m); + func_interp * bv_fi = bv_mdl->get_func_interp(it->m_value); + SASSERT(bv_fi->args_are_values()); - for (unsigned j = 0; j < arity; j++) { - sort * dj = f->get_domain(j); - expr * aj = bv_args[j]; - if (fu.is_float(dj)) - new_args.push_back(convert_bv2fp(bv_mdl, dj, aj)); - else if (fu.is_rm(dj)) { - expr_ref fv(m); - fv = convert_bv2rm(aj); - new_args.push_back(fv); + for (unsigned i = 0; i < bv_fi->num_entries(); i++) { + func_entry const * bv_fe = bv_fi->get_entry(i); + expr * const * bv_args = bv_fe->get_args(); + expr_ref_buffer new_args(m); + + for (unsigned j = 0; j < arity; j++) { + sort * dj = f->get_domain(j); + expr * aj = bv_args[j]; + if (fu.is_float(dj)) + new_args.push_back(convert_bv2fp(bv_mdl, dj, aj)); + else if (fu.is_rm(dj)) { + expr_ref fv(m); + fv = convert_bv2rm(aj); + new_args.push_back(fv); + } + else + new_args.push_back(aj); } - else - new_args.push_back(aj); + + expr_ref ret(m); + ret = bv_fe->get_result(); + if (fu.is_float(rng)) + ret = convert_bv2fp(bv_mdl, rng, ret); + else if (fu.is_rm(rng)) + ret = convert_bv2rm(ret); + + flt_fi->insert_new_entry(new_args.c_ptr(), ret); } - expr_ref ret(m); - ret = bv_fe->get_result(); + expr_ref els(m); + els = bv_fi->get_else(); if (fu.is_float(rng)) - ret = convert_bv2fp(bv_mdl, rng, ret); + els = convert_bv2fp(bv_mdl, rng, els); else if (fu.is_rm(rng)) - ret = convert_bv2rm(ret); + els = convert_bv2rm(els); - flt_fi->insert_new_entry(new_args.c_ptr(), ret); + flt_fi->set_else(els); + + float_mdl->register_decl(f, flt_fi); } - - expr_ref els(m); - els = bv_fi->get_else(); - if (fu.is_float(rng)) - els = convert_bv2fp(bv_mdl, rng, els); - else if (fu.is_rm(rng)) - els = convert_bv2rm(els); - - flt_fi->set_else(els); - - float_mdl->register_decl(f, flt_fi); - } - - // fp.to_*_unspecified UFs. - for (obj_hashtable::iterator it = m_unspecified_ufs.begin(); - it != m_unspecified_ufs.end(); - it++) - { - func_decl * f = *it; - - if (bv_mdl->has_interpretation(f)) { - func_interp * val = bv_mdl->get_func_interp(f)->copy(); - TRACE("fpa2bv_mc", tout << "Keeping interpretation for " << mk_ismt2_pp(f, m) << std::endl;); - float_mdl->register_decl(f, val); + else { + func_decl * bvf = it->m_value; + expr_ref c(m), e(m); + c = m.mk_const(bvf); + bv_mdl->eval(c, e, true); + float_mdl->register_decl(f, e); + TRACE("fpa2bv_mc", tout << "model value for " << mk_ismt2_pp(f, m) << " is " << mk_ismt2_pp(e, m) << std::endl;); } - else - TRACE("fpa2bv_mc", tout << "No interpretation for " << mk_ismt2_pp(f, m) << std::endl;); } // Keep all the non-float constants. diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 589d3c201..854543f24 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -28,7 +28,6 @@ class fpa2bv_model_converter : public model_converter { obj_map m_rm_const2bv; obj_map m_uf2bvuf; obj_map > m_specials; - obj_hashtable m_unspecified_ufs; public: fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) : m(m) { @@ -64,13 +63,6 @@ public: m.inc_ref(it->m_value.first); m.inc_ref(it->m_value.second); } - for (obj_hashtable::iterator it = conv.m_unspecified_ufs.begin(); - it != conv.m_unspecified_ufs.end(); - it++) - { - m_unspecified_ufs.insert(*it); - m.inc_ref(*it); - } } virtual ~fpa2bv_model_converter() { @@ -84,7 +76,6 @@ public: m.dec_ref(it->m_value.first); m.dec_ref(it->m_value.second); } - dec_ref_collection_values(m, m_unspecified_ufs); } virtual void operator()(model_ref & md, unsigned goal_idx) { From 778c7fcc6419417130b733e7d121535f3d1c2a45 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 16 Mar 2016 16:16:53 +0000 Subject: [PATCH 14/23] Bugfix for model evaluator and internal, uninterpreted FPA functions. Fixes #518 --- src/api/api_ast.cpp | 4 ++++ src/ast/fpa_decl_plugin.h | 16 ++++++++++++++++ src/model/model_evaluator.cpp | 2 +- 3 files changed, 21 insertions(+), 1 deletion(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 3e094e082..34dab3ed6 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1186,6 +1186,10 @@ extern "C" { case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV; case OP_FPA_INTERNAL_BVWRAP: case OP_FPA_INTERNAL_BVUNWRAP: + case OP_FPA_INTERNAL_MIN_I: + case OP_FPA_INTERNAL_MAX_I: + case OP_FPA_INTERNAL_MIN_UNSPECIFIED: + case OP_FPA_INTERNAL_MAX_UNSPECIFIED: case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 84eb5168b..a351b2610 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -184,6 +184,22 @@ class fpa_decl_plugin : public decl_plugin { unsigned mk_id(mpf const & v); void recycled_id(unsigned id); + virtual bool is_considered_uninterpreted(func_decl * f) { + if (f->get_family_id() != get_family_id()) + return false; + switch (f->get_decl_kind()) + { + case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: + return true; + default: + return false; + } + return false; + } + public: fpa_decl_plugin(); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 486111ae4..583a8dad5 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -111,7 +111,7 @@ struct evaluator_cfg : public default_rewriter_cfg { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { result_pr = 0; family_id fid = f->get_family_id(); - if (fid == null_family_id && num == 0) { + if (num == 0 && (fid == null_family_id || m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f))) { expr * val = m_model.get_const_interp(f); if (val != 0) { result = val; From db6b9faabca20648ce57447bc7811d9873d5961d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 16 Mar 2016 16:35:45 +0000 Subject: [PATCH 15/23] Bugfix for FPA rewriter. --- src/ast/rewriter/fpa_rewriter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 83372bcf4..5a25e11ec 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -130,7 +130,7 @@ br_status fpa_rewriter::mk_to_ubv_unspecified(func_decl * f, expr_ref & result) bv_util bu(m()); if (m_hi_fp_unspecified) // The "hardware interpretation" is 0. - result = bu.mk_numeral(0, ebits+sbits); + result = bu.mk_numeral(0, width); else result = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width); @@ -149,7 +149,7 @@ br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result) bv_util bu(m()); if (m_hi_fp_unspecified) // The "hardware interpretation" is 0. - result = bu.mk_numeral(0, ebits+sbits); + result = bu.mk_numeral(0, width); else result = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width); From 7ec70c168699520b31ab44615c3f4f864134810b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 16 Mar 2016 16:57:20 +0000 Subject: [PATCH 16/23] bug fixes for unspecified FP results --- src/ast/rewriter/fpa_rewriter.cpp | 38 ++++++++----------------------- src/ast/rewriter/fpa_rewriter.h | 7 +++--- 2 files changed, 12 insertions(+), 33 deletions(-) diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 5a25e11ec..e948ab624 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -118,15 +118,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con return st; } -br_status fpa_rewriter::mk_to_ubv_unspecified(func_decl * f, expr_ref & result) { - SASSERT(f->get_num_parameters() == 3); - SASSERT(f->get_parameter(0).is_int()); - SASSERT(f->get_parameter(1).is_int()); - SASSERT(f->get_parameter(2).is_int()); - unsigned ebits = f->get_parameter(0).get_int(); - unsigned sbits = f->get_parameter(1).get_int(); - unsigned width = f->get_parameter(2).get_int(); - +br_status fpa_rewriter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) { bv_util bu(m()); if (m_hi_fp_unspecified) // The "hardware interpretation" is 0. @@ -137,15 +129,7 @@ br_status fpa_rewriter::mk_to_ubv_unspecified(func_decl * f, expr_ref & result) return BR_DONE; } -br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result) { - SASSERT(f->get_num_parameters() == 3); - SASSERT(f->get_parameter(0).is_int()); - SASSERT(f->get_parameter(1).is_int()); - SASSERT(f->get_parameter(2).is_int()); - unsigned ebits = f->get_parameter(0).get_int(); - unsigned sbits = f->get_parameter(1).get_int(); - unsigned width = f->get_parameter(2).get_int(); - +br_status fpa_rewriter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) { bv_util bu(m()); if (m_hi_fp_unspecified) // The "hardware interpretation" is 0. @@ -156,13 +140,7 @@ br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result) return BR_DONE; } -br_status fpa_rewriter::mk_to_real_unspecified(func_decl * f, expr_ref & result) { - SASSERT(f->get_num_parameters() == 2); - SASSERT(f->get_parameter(0).is_int()); - SASSERT(f->get_parameter(1).is_int()); - unsigned ebits = f->get_parameter(0).get_int(); - unsigned sbits = f->get_parameter(1).get_int(); - +br_status fpa_rewriter::mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result) { if (m_hi_fp_unspecified) // The "hardware interpretation" is 0. result = m_util.au().mk_numeral(rational(0), false); @@ -799,9 +777,10 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ if (m_util.is_rm_numeral(arg1, rmv) && m_util.is_numeral(arg2, v)) { + const mpf & x = v.get(); if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) { - mk_to_ubv_unspecified(f, result); + mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); return BR_REWRITE_FULL; } @@ -816,7 +795,7 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ if (r >= ll && r <= ul) result = bu.mk_numeral(r, bv_sz); else - mk_to_ubv_unspecified(f, result); + mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); return BR_DONE; } @@ -832,9 +811,10 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ if (m_util.is_rm_numeral(arg1, rmv) && m_util.is_numeral(arg2, v)) { + const mpf & x = v.get(); if (m_fm.is_nan(v) || m_fm.is_inf(v)) { - mk_to_sbv_unspecified(f, result); + mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); return BR_REWRITE_FULL; } @@ -849,7 +829,7 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ if (r >= ll && r <= ul) result = bu.mk_numeral(r, bv_sz); else - mk_to_sbv_unspecified(f, result); + mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); return BR_DONE; } diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index b71b12120..3afc31a9f 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -86,10 +86,9 @@ public: br_status mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result); br_status mk_to_real(expr * arg, expr_ref & result); - br_status mk_to_ubv_unspecified(func_decl * f, expr_ref & result); - br_status mk_to_sbv_unspecified(func_decl * f, expr_ref & result); - br_status mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result); - br_status mk_to_real_unspecified(func_decl * f, expr_ref & result); + br_status mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result); + br_status mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result); + br_status mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result); }; #endif From 6b2d84b2bebe20873cb84926bae2880eb9da8cb1 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 16 Mar 2016 17:46:52 +0000 Subject: [PATCH 17/23] Fixed model evaluation/simplification for to_ieee_bv. --- src/ast/rewriter/fpa_rewriter.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index e948ab624..619d5ffbf 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -850,8 +850,16 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu bu.mk_concat(bu.mk_numeral(0, x.get_sbits() - 2), bu.mk_numeral(1, 1)))); } - else - result = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits()); + else { + app_ref unspec(m()), mask(m()), extra(m()); + unspec = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits()); + mask = bu.mk_concat(bu.mk_numeral(0, 1), + bu.mk_concat(bu.mk_numeral(-1, x.get_ebits()), + bu.mk_concat(bu.mk_numeral(0, x.get_sbits() - 2), + bu.mk_numeral(1, 1)))); + expr * args[2] = { unspec, mask }; + result = m().mk_app(bu.get_fid(), OP_BOR, 2, args); + } return BR_REWRITE_FULL; } else { From 34da0a32b9a9b97b5e5044d32e54bf1b3a3bdcc9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andres=20N=C3=B6tzli?= Date: Wed, 16 Mar 2016 17:12:45 -0700 Subject: [PATCH 18/23] [Z3py] Fix error in FPRef.__neg__() `FPRef.__neg__()` did not work previously because it tried to construct an FPRef from an FPRef (`fpNeg()` already returns an FPRef). --- src/api/python/z3.py | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 5727d2dfb..374c71be4 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8178,8 +8178,13 @@ class FPRef(ExprRef): return self def __neg__(self): - """Create the Z3 expression `-self`.""" - return FPRef(fpNeg(self)) + """Create the Z3 expression `-self`. + + >>> x = FP('x', Float32()) + >>> -x + -x + """ + return fpNeg(self) def __div__(self, other): """Create the Z3 expression `self / other`. From c8af48d7ef3a8a86af7501cb0557b651c7319080 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Mar 2016 13:09:52 +0000 Subject: [PATCH 19/23] Bugfix for bvurem0 model evaluation (+1 rewriting step) --- src/ast/rewriter/bv_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index be9b5f375..7322977a0 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -892,7 +892,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e if (r2.is_zero()) { if (!hi_div0) { result = m().mk_app(get_fid(), OP_BUREM0, arg1); - return BR_DONE; + return BR_REWRITE1; } else { // The "hardware interpretation" for (bvurem x 0) is x From aed4619066f24546ff8370fc86e9be1773a68c4b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 17 Mar 2016 13:14:43 +0000 Subject: [PATCH 20/23] reduce-args: fixed unsoundness introduced in my previous commit skip an UF arg if it's quantified e.g. forall a . f(a, b) -> f(b) (but not f) --- src/tactic/core/reduce_args_tactic.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index 4f6f4c3d7..aee136284 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -96,10 +96,10 @@ struct reduce_args_tactic::imp { expr *lhs, *rhs; if (bv.is_bv_add(e, lhs, rhs) && bv.is_numeral(lhs)) { base = rhs; - } else { - base = e; + return true; } - return true; + base = e; + return !is_var(e); } static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) { From facb42139856fb995fbb0586eac56db351f78483 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 17 Mar 2016 13:27:07 +0000 Subject: [PATCH 21/23] reduce-args: fix unsoundness 2: f(v + 2), where b is quantified --- src/tactic/core/reduce_args_tactic.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index aee136284..cfb9a1eb8 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -96,10 +96,10 @@ struct reduce_args_tactic::imp { expr *lhs, *rhs; if (bv.is_bv_add(e, lhs, rhs) && bv.is_numeral(lhs)) { base = rhs; - return true; + } else { + base = e; } - base = e; - return !is_var(e); + return !is_var(base); } static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) { From f5c4800eecbfcbc94ce0ce491670f96a9fd6ea3c Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 17 Mar 2016 15:29:48 +0000 Subject: [PATCH 22/23] reduce-args: last fix for may_be_unique to support quantified variables in arbitrary exprs --- src/tactic/core/reduce_args_tactic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index cfb9a1eb8..ec7353044 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -19,6 +19,7 @@ Notes: #include"tactical.h" #include"cooperate.h" #include"ast_smt2_pp.h" +#include"has_free_vars.h" #include"map.h" #include"rewriter_def.h" #include"extension_model_converter.h" @@ -99,7 +100,7 @@ struct reduce_args_tactic::imp { } else { base = e; } - return !is_var(base); + return !has_free_vars(base); } static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) { From cc04fdbd706ae42795db31652a50d517c8028a5e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Mar 2016 17:52:26 +0000 Subject: [PATCH 23/23] Added eager ackermannization to QF_FP, so that small numbers of unspecified operators are eliminated upfront. --- src/tactic/fpa/qffp_tactic.cpp | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index 9c94d6cb2..5f431b113 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -23,6 +23,7 @@ Notes: #include"fpa2bv_tactic.h" #include"smt_tactic.h" #include"propagate_values_tactic.h" +#include"ackermannize_bv_tactic.h" #include"probe_arith.h" #include"qfnra_tactic.h" @@ -69,11 +70,14 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { simp_p.set_bool("arith_lhs", true); simp_p.set_bool("elim_and", true); - tactic * st = and_then(mk_simplify_tactic(m, simp_p), - mk_propagate_values_tactic(m, p), - mk_fpa2bv_tactic(m, p), - mk_propagate_values_tactic(m, p), - using_params(mk_simplify_tactic(m, p), simp_p), + tactic * preamble = and_then(mk_simplify_tactic(m, simp_p), + mk_propagate_values_tactic(m, p), + mk_fpa2bv_tactic(m, p), + mk_propagate_values_tactic(m, p), + using_params(mk_simplify_tactic(m, p), simp_p), + if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m, p)))); + + tactic * st = and_then(preamble, mk_bit_blaster_tactic(m, p), using_params(mk_simplify_tactic(m, p), simp_p), cond(mk_is_propositional_probe(), @@ -136,7 +140,7 @@ public: probe * mk_is_qffp_probe() { return alloc(is_qffp_probe); } - + probe * mk_is_qffpbv_probe() { return alloc(is_qffp_probe); }