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
diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py
index 790ce7205..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_dir>/src/ast/fpa`` and ``<build_dir>/src/ast/fpa``).
+ We don't want to sort based on different ``<src_dir>``
+ and ``<build_dir>`` 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
###############################################################################
@@ -105,9 +143,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:
@@ -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)
@@ -246,7 +286,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,
}
@@ -261,18 +301,21 @@ 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:
- 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))
@@ -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:
- 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))
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:
@@ -514,6 +558,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]
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index e30da1aa1..34dab3ed6 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;
@@ -1186,9 +1186,14 @@ 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:
+ case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
return Z3_OP_UNINTERPRETED;
default:
UNREACHABLE();
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<Z3_app>(m_ast); }
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`.
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 4a3ec7553..c958fb67f 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));
@@ -2624,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));
}
@@ -2904,9 +2927,29 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
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);
+
+ 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 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
+ 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));
+
+ 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) {
@@ -2942,7 +2985,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
@@ -3041,8 +3084,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);
@@ -3061,25 +3104,100 @@ 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);
+ 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;
}
-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);
+ 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;
}
-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);
+ 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) {
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index 8dc3dc019..f69351cb2 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -134,9 +134,10 @@ 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_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);
+ expr_ref mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits);
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..511d36e67 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))
@@ -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));
}
@@ -741,12 +741,13 @@ 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");
- 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);
+ m_manager->raise_exception("invalid number of arguments to fp.to_sbv_unspecified");
+ 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));
}
@@ -754,13 +755,32 @@ 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 (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 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 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");
+
+ 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));
+}
+
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 +866,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;
@@ -1045,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_SBV_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 a667bc6f8..a351b2610 100644
--- a/src/ast/fpa_decl_plugin.h
+++ b/src/ast/fpa_decl_plugin.h
@@ -177,11 +177,29 @@ 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);
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();
@@ -344,10 +362,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/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
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index 57fb606ba..619d5ffbf 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -102,11 +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(result); break;
+ case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
+ st = BR_FAILED;
case OP_FPA_INTERNAL_BVWRAP:
case OP_FPA_INTERNAL_BVUNWRAP:
@@ -119,55 +118,34 @@ 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() == 1);
- SASSERT(f->get_parameter(0).is_int());
- unsigned bv_sz = f->get_parameter(0).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.
- result = bu.mk_numeral(0, bv_sz);
+ result = bu.mk_numeral(0, width);
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_parameter(0).is_int());
- unsigned bv_sz = f->get_parameter(0).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.
- result = bu.mk_numeral(0, bv_sz);
+ result = bu.mk_numeral(0, width);
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());
-
- 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);
-
- return BR_DONE;
-}
-
-br_status fpa_rewriter::mk_to_real_unspecified(expr_ref & result) {
+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);
else
- result = m_util.mk_internal_to_real_unspecified();
+ result = m_util.mk_internal_to_real_unspecified(ebits, sbits);
return BR_DONE;
}
@@ -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;
}
@@ -860,17 +840,35 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu
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) || m_fm.is_inf(v)) {
- mk_to_ieee_bv_unspecified(f, result);
+ if (m_fm.is_nan(v)) {
+ 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 {
+ 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 {
+ scoped_mpz rz(m_fm.mpq_manager());
+ m_fm.to_ieee_bv_mpz(v, rz);
- 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;
+ result = bu.mk_numeral(rational(rz), x.get_ebits() + x.get_sbits());
+ return BR_DONE;
+ }
}
return BR_FAILED;
@@ -881,7 +879,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..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(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
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;
diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp
index 4f6f4c3d7..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 true;
+ return !has_free_vars(base);
}
static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) {
diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp
index a41b92b2d..627e33a7b 100644
--- a/src/tactic/fpa/fpa2bv_model_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_model_converter.cpp
@@ -54,7 +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) << ")";
}
- out << ")" << std::endl;
}
model_converter * fpa2bv_model_converter::translate(ast_translation & translator) {
@@ -321,50 +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);
+ }
+ 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;);
}
-
- 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);
}
// Keep all the non-float constants.
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);
}
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) {