mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-03-17 13:06:21 -07:00
parent 55956df8d8 94054593a4
commit ab82fee398
18 changed files with 508 additions and 192 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
README.md
View file

@ -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). 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 Z3 can be built using [Visual Studio][1], a [Makefile][2] or using [CMake][3]. It provides
[bindings for several programming languages][3]. [bindings for several programming languages][4].
See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z3. See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z3.
[1]: #building-z3-on-windows-using-visual-studio-command-prompt [1]: #building-z3-on-windows-using-visual-studio-command-prompt
[2]: #building-z3-using-make-and-gccclang [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 ## Building Z3 on Windows using Visual Studio Command Prompt

100
scripts/mk_genfile_common.py
View file

@ -9,6 +9,7 @@
# to avoid having this code depend on the # to avoid having this code depend on the
# of the Python build system. # of the Python build system.
import os import os
import pprint
import logging import logging
import re import re
import sys import sys
@ -38,6 +39,43 @@ def check_files_exist(files):
return False return False
return True 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 # Functions for generating constant declarations for language bindings
############################################################################### ###############################################################################
@ -105,9 +143,9 @@ def mk_z3consts_py_internal(api_files, output_dir):
if m: if m:
name = words[1] name = words[1]
z3consts.write('# enum %s\n' % name) z3consts.write('# enum %s\n' % name)
for k in decls: # Iterate over key-value pairs ordered by value
i = decls[k] for k, v in sorted(decls.items(), key=lambda pair: pair[1]):
z3consts.write('%s = %s\n' % (k, i)) z3consts.write('%s = %s\n' % (k, v))
z3consts.write('\n') z3consts.write('\n')
mode = SEARCHING mode = SEARCHING
elif len(words) <= 2: 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_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)')
reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)') reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)')
reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)') reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)')
h_files_full_path = []
for component_src_dir in component_src_dirs: 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)) h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
for h_file in h_files: h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files))
added_include = False h_files_full_path.extend(h_files)
fin = open(os.path.join(component_src_dir, h_file), 'r') 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: for line in fin:
m = reg_pat.match(line) m = reg_pat.match(line)
if m: if m:
if not added_include: if not added_include:
added_include = True 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))) cmds.append((m.group(1)))
m = reg_mod_pat.match(line) m = reg_mod_pat.match(line)
if m: if m:
if not added_include: if not added_include:
added_include = True 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))) mod_cmds.append((m.group(1), m.group(2)))
m = reg_mod_descr_pat.match(line) m = reg_mod_descr_pat.match(line)
if m: if m:
mod_descrs.append((m.group(1), m.group(2))) mod_descrs.append((m.group(1), m.group(2)))
fin.close()
fout.write('void gparams_register_modules() {\n') fout.write('void gparams_register_modules() {\n')
for code in cmds: for code in cmds:
fout.write('{ param_descrs d; %s(d); gparams::register_global(d); }\n' % code) 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): def ADD_PROBE(name, descr, cmd):
ADD_PROBE_DATA.append((name, descr, cmd)) ADD_PROBE_DATA.append((name, descr, cmd))
exec_globals = { eval_globals = {
'ADD_TACTIC': ADD_TACTIC, 'ADD_TACTIC': ADD_TACTIC,
'ADD_PROBE': ADD_PROBE, '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') fout.write('#include"cmd_context.h"\n')
tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)') tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)')
probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)') 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)) h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
for h_file in h_files: h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files))
added_include = False h_files_full_path.extend(h_files)
fin = open(os.path.join(component_src_dir, h_file), 'r') 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: for line in fin:
if tactic_pat.match(line): if tactic_pat.match(line):
if not added_include: if not added_include:
added_include = True added_include = True
fout.write('#include"%s"\n' % h_file) fout.write('#include"%s"\n' % os.path.basename(h_file))
try: try:
exec(line.strip('\n '), exec_globals) eval(line.strip('\n '), eval_globals, None)
except Exception as e: except Exception as e:
_logger.error("Failed processing ADD_TACTIC command at '{}'\n{}".format( _logger.error("Failed processing ADD_TACTIC command at '{}'\n{}".format(
fullname, line)) fullname, line))
@ -280,14 +323,13 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path):
if probe_pat.match(line): if probe_pat.match(line):
if not added_include: if not added_include:
added_include = True added_include = True
fout.write('#include"%s"\n' % h_file) fout.write('#include"%s"\n' % os.path.basename(h_file))
try: try:
exec(line.strip('\n '), exec_globals) eval(line.strip('\n '), eval_globals, None)
except Exception as e: except Exception as e:
_logger.error("Failed processing ADD_PROBE command at '{}'\n{}".format( _logger.error("Failed processing ADD_PROBE command at '{}'\n{}".format(
fullname, line)) fullname, line))
raise e raise e
fin.close()
# First pass will just generate the tactic factories # First pass will just generate the tactic factories
idx = 0 idx = 0
for data in ADD_TACTIC_DATA: for data in ADD_TACTIC_DATA:
@ -335,31 +377,33 @@ def mk_mem_initializer_cpp_internal(component_src_dirs, path):
# ADD_INITIALIZER with priority # ADD_INITIALIZER with priority
initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)')
finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') 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)) h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
for h_file in h_files: h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files))
added_include = False h_files_full_path.extend(h_files)
fin = open(os.path.join(component_src_dir, h_file), 'r') 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: for line in fin:
m = initializer_pat.match(line) m = initializer_pat.match(line)
if m: if m:
if not added_include: if not added_include:
added_include = True 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)) initializer_cmds.append((m.group(1), 0))
m = initializer_prio_pat.match(line) m = initializer_prio_pat.match(line)
if m: if m:
if not added_include: if not added_include:
added_include = True 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)))) initializer_cmds.append((m.group(1), int(m.group(2))))
m = finalizer_pat.match(line) m = finalizer_pat.match(line)
if m: if m:
if not added_include: if not added_include:
added_include = True 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)) finalizer_cmds.append(m.group(1))
fin.close()
initializer_cmds.sort(key=lambda tup: tup[1]) initializer_cmds.sort(key=lambda tup: tup[1])
fout.write('void mem_initialize() {\n') fout.write('void mem_initialize() {\n')
for (cmd, prio) in initializer_cmds: 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, 'def_module_params' : def_module_params,
} }
with open(pyg_file, 'r') as fh: 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 assert len(OUTPUT_HPP_FILE) == 1
return OUTPUT_HPP_FILE[0] return OUTPUT_HPP_FILE[0]

5
src/api/api_ast.cpp
View file

@ -1186,9 +1186,14 @@ extern "C" {
case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV; case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV;
case OP_FPA_INTERNAL_BVWRAP: case OP_FPA_INTERNAL_BVWRAP:
case OP_FPA_INTERNAL_BVUNWRAP: 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_UBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
return Z3_OP_UNINTERPRETED; return Z3_OP_UNINTERPRETED;
default: default:
UNREACHABLE(); UNREACHABLE();

76
src/api/c++/z3++.h
View file

@ -622,12 +622,88 @@ namespace z3 {
\brief Return true if this expression is a variable. \brief Return true if this expression is a variable.
*/ */
bool is_var() const { return kind() == Z3_VAR_AST; } 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). \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; } 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); } operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
/** /**

9
src/api/python/z3.py
View file

@ -8178,8 +8178,13 @@ class FPRef(ExprRef):
return self return self
def __neg__(self): def __neg__(self):
"""Create the Z3 expression `-self`.""" """Create the Z3 expression `-self`.
return FPRef(fpNeg(self))
>>> x = FP('x', Float32())
>>> -x
-x
"""
return fpNeg(self)
def __div__(self, other): def __div__(self, other):
"""Create the Z3 expression `self / other`. """Create the Z3 expression `self / other`.

164
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -980,6 +980,9 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args,
x = args[0]; x = args[0];
y = args[1]; 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); expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m);
mk_nan(f, nan); mk_nan(f, nan);
mk_nzero(f, nzero); 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(x, a_sgn, a_sig, a_exp, a_lz, true);
unpack(y, b_sgn, b_sig, b_exp, b_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); BVSLT(a_exp, b_exp, c6);
v6 = x; 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); unsigned int max_exp_diff_ui = (unsigned int)m_mpz_manager.get_uint64(max_exp_diff);
m_mpz_manager.del(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); 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); dbg_decouple("fpa2bv_rem_exp_diff", exp_diff);
// CMW: This creates _huge_ bit-vectors, which is potentially sub-optimal, // CMW: This creates _huge_ bit-vectors, which is potentially sub-optimal,
// but calculating this via rem = x - y * nearest(x/y) creates huge circuits. // but calculating this via rem = x - y * nearest(x/y) creates huge circuits.
expr_ref huge_sig(m), shifted_sig(m), huge_rem(m); 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); 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)); 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); 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_sgn = a_sgn;
res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits, 0, huge_rem), res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits, 0, huge_rem),
m_bv_util.mk_numeral(0, 3)); 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 // CMW: Actual rounding is not necessary here, this is
// just convenience to get rid of the extra bits. // 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) { 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 << 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(m_util.is_float(s));
SASSERT(au().is_real(x) || au().is_int(x)); SASSERT(au().is_real(x) || au().is_int(x));
SASSERT(is_app_of(rm, m_util.get_family_id(), OP_FPA_INTERNAL_RM)); 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;); tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;);
result = m.mk_ite(x_is_zero, zero, res); 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_inf, mk_to_real_unspecified(ebits, sbits), result);
result = m.mk_ite(x_is_nan, mk_to_real_unspecified(), result); result = m.mk_ite(x_is_nan, mk_to_real_unspecified(ebits, sbits), result);
SASSERT(is_well_sorted(m, 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) { void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1); SASSERT(num == 1);
expr_ref x(m), x_is_nan(m);
expr * sgn, * s, * e; expr * sgn, * s, * e;
split_fp(args[0], sgn, e, s); x = args[0];
result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s); 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) { 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))); c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero)));
else else
c1 = m.mk_or(x_is_nan, x_is_inf); 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); dbg_decouple("fpa2bv_to_bv_c1", c1);
// +-Zero -> 0 // +-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); 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(rnd_has_overflown, mk_to_ubv_unspecified(ebits, sbits, bv_sz), rnd);
result = m.mk_ite(c_in_limits, result, mk_to_ubv_unspecified(bv_sz)); 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(c2, v2, result);
result = m.mk_ite(c1, v1, 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); 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) if (m_hi_fp_unspecified)
return expr_ref(m_bv_util.mk_numeral(0, width), m); result = m_bv_util.mk_numeral(0, width);
else else {
return expr_ref(m_util.mk_internal_to_ubv_unspecified(width), m); 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) if (m_hi_fp_unspecified)
return expr_ref(m_bv_util.mk_numeral(0, width), m); result = m_bv_util.mk_numeral(0, width);
else else {
return expr_ref(m_util.mk_internal_to_sbv_unspecified(width), m); 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) if (m_hi_fp_unspecified)
return expr_ref(m_arith_util.mk_numeral(rational(0), false), m); result = m_arith_util.mk_numeral(rational(0), false);
else else {
return expr_ref(m_util.mk_internal_to_real_unspecified(), m); 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) { void fpa2bv_converter::mk_rm(expr * bv3, expr_ref & result) {

7
src/ast/fpa/fpa2bv_converter.h
View file

@ -134,9 +134,10 @@ public:
void mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); 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); 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_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
expr_ref mk_to_sbv_unspecified(unsigned width); expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
expr_ref mk_to_real_unspecified(); expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits);
expr_ref mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits);
void reset(void); void reset(void);

4
src/ast/fpa/fpa2bv_rewriter.cpp
View file

@ -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_BVUNWRAP:
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_UBV_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: default:
TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; 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;); for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);

77
src/ast/fpa_decl_plugin.cpp
View file

@ -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, 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) { unsigned arity, sort * const * domain, sort * range) {
if (arity != 1) 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])) if (!is_float_sort(domain[0]) && !is_rm_sort(domain[0]))
m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint or RoundingMode sort"); 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, 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) { unsigned arity, sort * const * domain, sort * range) {
if (arity != 1) 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)) if (!is_sort_of(domain[0], m_bv_fid, BV_SORT))
m_manager->raise_exception("sort mismatch, expected argument of bitvector sort"); m_manager->raise_exception("sort mismatch, expected argument of bitvector sort");
if (!is_float_sort(range) && !is_rm_sort(range)) 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) { unsigned arity, sort * const * domain, sort * range) {
if (arity != 0) if (arity != 0)
m_manager->raise_exception("invalid number of arguments to fp.to_ubv_unspecified"); m_manager->raise_exception("invalid number of arguments to fp.to_ubv_unspecified");
if (num_parameters != 1) if (num_parameters != 3)
m_manager->raise_exception("invalid number of parameters to fp.to_ubv_unspecified; expecting 1"); m_manager->raise_exception("invalid number of parameters to fp.to_ubv_unspecified; expecting 3");
if (!parameters[0].is_int()) 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 an integer"); 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, &parameters[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)); 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, decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) { unsigned arity, sort * const * domain, sort * range) {
if (arity != 0) 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) if (num_parameters != 3)
m_manager->raise_exception("invalid number of parameters to fp.to_sbv_unspecified; expecting 1"); m_manager->raise_exception("invalid number of parameters to fp.to_sbv_unspecified; expecting 3");
if (!parameters[0].is_int()) 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 an integer"); 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, parameters);
sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, &parameters[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)); 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, decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) { unsigned arity, sort * const * domain, sort * range) {
if (arity != 0) 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)) 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)); 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, func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) { 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); return mk_internal_to_sbv_unspecified(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
return mk_internal_to_real_unspecified(k, num_parameters, parameters, arity, domain, range); 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: default:
m_manager->raise_exception("unsupported floating point operator"); m_manager->raise_exception("unsupported floating point operator");
return 0; return 0;
@ -1045,25 +1067,26 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) {
return mk_value(v); return mk_value(v);
} }
app * fpa_util::mk_internal_to_ubv_unspecified(unsigned width) { app * fpa_util::mk_internal_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
parameter ps[] = { parameter(width) }; parameter ps[] = { parameter(ebits), parameter(sbits), parameter(width) };
sort * range = m_bv_util.mk_sort(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) { app * fpa_util::mk_internal_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
parameter ps[] = { parameter(width) }; parameter ps[] = { parameter(ebits), parameter(sbits), parameter(width) };
sort * range = m_bv_util.mk_sort(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) { app * fpa_util::mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits) {
parameter ps[] = { parameter(width) }; parameter ps[] = { parameter(ebits), parameter(sbits) };
sort * range = m_bv_util.mk_sort(width); sort * range = m_bv_util.mk_sort(ebits+sbits);
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, 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(); 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);
} }

26
src/ast/fpa_decl_plugin.h
View file

@ -177,11 +177,29 @@ class fpa_decl_plugin : public decl_plugin {
unsigned arity, sort * const * domain, sort * range); unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_to_real_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, func_decl * mk_internal_to_real_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range); 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); virtual void set_manager(ast_manager * m, family_id id);
unsigned mk_id(mpf const & v); unsigned mk_id(mpf const & v);
void recycled_id(unsigned id); 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: public:
fpa_decl_plugin(); 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_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_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
app * mk_internal_to_sbv_unspecified(unsigned width); app * mk_internal_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
app * mk_internal_to_ieee_bv_unspecified(unsigned width); app * mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits);
app * mk_internal_to_real_unspecified(); 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_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); } bool is_unwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVUNWRAP); }

2
src/ast/rewriter/bv_rewriter.cpp
View file

@ -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 (r2.is_zero()) {
if (!hi_div0) { if (!hi_div0) {
result = m().mk_app(get_fid(), OP_BUREM0, arg1); result = m().mk_app(get_fid(), OP_BUREM0, arg1);
return BR_DONE; return BR_REWRITE1;
} }
else { else {
// The "hardware interpretation" for (bvurem x 0) is x // The "hardware interpretation" for (bvurem x 0) is x

87
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -102,11 +102,10 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_FPA_INTERNAL_RM: case OP_FPA_INTERNAL_RM:
SASSERT(num_args == 1); st = mk_rm(args[0], result); break; SASSERT(num_args == 1); st = mk_rm(args[0], result); break;
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: 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: 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: 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_BVWRAP:
case OP_FPA_INTERNAL_BVUNWRAP: 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; return st;
} }
br_status fpa_rewriter::mk_to_ubv_unspecified(func_decl * f, expr_ref & result) { br_status fpa_rewriter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width, 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();
bv_util bu(m()); bv_util bu(m());
if (m_hi_fp_unspecified) if (m_hi_fp_unspecified)
// The "hardware interpretation" is 0. // The "hardware interpretation" is 0.
result = bu.mk_numeral(0, bv_sz); result = bu.mk_numeral(0, width);
else 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; return BR_DONE;
} }
br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result) { br_status fpa_rewriter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width, 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();
bv_util bu(m()); bv_util bu(m());
if (m_hi_fp_unspecified) if (m_hi_fp_unspecified)
// The "hardware interpretation" is 0. // The "hardware interpretation" is 0.
result = bu.mk_numeral(0, bv_sz); result = bu.mk_numeral(0, width);
else 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; return BR_DONE;
} }
br_status fpa_rewriter::mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result) { br_status fpa_rewriter::mk_to_real_unspecified(unsigned ebits, unsigned sbits, 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) {
if (m_hi_fp_unspecified) if (m_hi_fp_unspecified)
// The "hardware interpretation" is 0. // The "hardware interpretation" is 0.
result = m_util.au().mk_numeral(rational(0), false); result = m_util.au().mk_numeral(rational(0), false);
else else
result = m_util.mk_internal_to_real_unspecified(); result = m_util.mk_internal_to_real_unspecified(ebits, sbits);
return BR_DONE; 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) && if (m_util.is_rm_numeral(arg1, rmv) &&
m_util.is_numeral(arg2, v)) { 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)) { 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; 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) if (r >= ll && r <= ul)
result = bu.mk_numeral(r, bv_sz); result = bu.mk_numeral(r, bv_sz);
else else
mk_to_ubv_unspecified(f, result); mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
return BR_DONE; 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) && if (m_util.is_rm_numeral(arg1, rmv) &&
m_util.is_numeral(arg2, v)) { m_util.is_numeral(arg2, v)) {
const mpf & x = v.get();
if (m_fm.is_nan(v) || m_fm.is_inf(v)) { 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; 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) if (r >= ll && r <= ul)
result = bu.mk_numeral(r, bv_sz); result = bu.mk_numeral(r, bv_sz);
else else
mk_to_sbv_unspecified(f, result); mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
return BR_DONE; 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); scoped_mpf v(m_fm);
if (m_util.is_numeral(arg, v)) { 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)) { if (m_fm.is_nan(v)) {
mk_to_ieee_bv_unspecified(f, result); 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; return BR_REWRITE_FULL;
} }
else {
scoped_mpz rz(m_fm.mpq_manager());
m_fm.to_ieee_bv_mpz(v, rz);
bv_util bu(m()); result = bu.mk_numeral(rational(rz), x.get_ebits() + x.get_sbits());
scoped_mpz rz(m_fm.mpq_manager()); return BR_DONE;
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; 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_util.is_numeral(arg, v)) {
if (m_fm.is_nan(v) || m_fm.is_inf(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 { else {
scoped_mpq r(m_fm.mpq_manager()); scoped_mpq r(m_fm.mpq_manager());

7
src/ast/rewriter/fpa_rewriter.h
View file

@ -86,10 +86,9 @@ public:
br_status mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result); 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_real(expr * arg, expr_ref & result);
br_status mk_to_ubv_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(func_decl * f, expr_ref & result); br_status mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result);
br_status mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result); br_status mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result);
br_status mk_to_real_unspecified(expr_ref & result);
}; };
#endif #endif

2
src/model/model_evaluator.cpp
View file

@ -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) { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0; result_pr = 0;
family_id fid = f->get_family_id(); 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); expr * val = m_model.get_const_interp(f);
if (val != 0) { if (val != 0) {
result = val; result = val;

3
src/tactic/core/reduce_args_tactic.cpp
View file

@ -19,6 +19,7 @@ Notes:
#include"tactical.h" #include"tactical.h"
#include"cooperate.h" #include"cooperate.h"
#include"ast_smt2_pp.h" #include"ast_smt2_pp.h"
#include"has_free_vars.h"
#include"map.h" #include"map.h"
#include"rewriter_def.h" #include"rewriter_def.h"
#include"extension_model_converter.h" #include"extension_model_converter.h"
@ -99,7 +100,7 @@ struct reduce_args_tactic::imp {
} else { } else {
base = e; base = e;
} }
return true; return !has_free_vars(base);
} }
static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) { static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) {

80
src/tactic/fpa/fpa2bv_model_converter.cpp
View file

@ -54,7 +54,6 @@ void fpa2bv_model_converter::display(std::ostream & out) {
out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " << out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " <<
mk_ismt2_pp(it->m_value.second, m, indent) << ")"; mk_ismt2_pp(it->m_value.second, m, indent) << ")";
} }
out << ")" << std::endl;
} }
model_converter * fpa2bv_model_converter::translate(ast_translation & translator) { 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; func_decl * f = it->m_key;
unsigned arity = f->get_arity(); unsigned arity = f->get_arity();
sort * rng = f->get_range(); 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); if (arity > 0) {
SASSERT(bv_fi->args_are_values()); func_interp * flt_fi = alloc(func_interp, m, f->get_arity());
for (unsigned i = 0; i < bv_fi->num_entries(); i++) { func_interp * bv_fi = bv_mdl->get_func_interp(it->m_value);
func_entry const * bv_fe = bv_fi->get_entry(i); SASSERT(bv_fi->args_are_values());
expr * const * bv_args = bv_fe->get_args();
expr_ref_buffer new_args(m);
for (unsigned j = 0; j < arity; j++) { for (unsigned i = 0; i < bv_fi->num_entries(); i++) {
sort * dj = f->get_domain(j); func_entry const * bv_fe = bv_fi->get_entry(i);
expr * aj = bv_args[j]; expr * const * bv_args = bv_fe->get_args();
if (fu.is_float(dj)) expr_ref_buffer new_args(m);
new_args.push_back(convert_bv2fp(bv_mdl, dj, aj));
else if (fu.is_rm(dj)) { for (unsigned j = 0; j < arity; j++) {
expr_ref fv(m); sort * dj = f->get_domain(j);
fv = convert_bv2rm(aj); expr * aj = bv_args[j];
new_args.push_back(fv); 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); expr_ref els(m);
ret = bv_fe->get_result(); els = bv_fi->get_else();
if (fu.is_float(rng)) 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)) 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. // Keep all the non-float constants.

14
src/tactic/fpa/qffp_tactic.cpp
View file

@ -23,6 +23,7 @@ Notes:
#include"fpa2bv_tactic.h" #include"fpa2bv_tactic.h"
#include"smt_tactic.h" #include"smt_tactic.h"
#include"propagate_values_tactic.h" #include"propagate_values_tactic.h"
#include"ackermannize_bv_tactic.h"
#include"probe_arith.h" #include"probe_arith.h"
#include"qfnra_tactic.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("arith_lhs", true);
simp_p.set_bool("elim_and", true); simp_p.set_bool("elim_and", true);
tactic * st = and_then(mk_simplify_tactic(m, simp_p), tactic * preamble = and_then(mk_simplify_tactic(m, simp_p),
mk_propagate_values_tactic(m, p), mk_propagate_values_tactic(m, p),
mk_fpa2bv_tactic(m, p), mk_fpa2bv_tactic(m, p),
mk_propagate_values_tactic(m, p), mk_propagate_values_tactic(m, p),
using_params(mk_simplify_tactic(m, p), simp_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), mk_bit_blaster_tactic(m, p),
using_params(mk_simplify_tactic(m, p), simp_p), using_params(mk_simplify_tactic(m, p), simp_p),
cond(mk_is_propositional_probe(), cond(mk_is_propositional_probe(),

26
src/util/mpf.cpp
View file

@ -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) { 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); SASSERT(exp(x) < INT_MAX);
unsigned sbits = x.get_sbits(); unsigned sbits = x.get_sbits();
unsigned ebits = x.get_ebits(); unsigned ebits = x.get_ebits();
scoped_mpz biased_exp(m_mpz_manager);
m_mpz_manager.set(biased_exp, bias_exp(ebits, exp(x))); if (is_inf(x)) {
m_mpz_manager.set(o, sgn(x)); m_mpz_manager.set(o, sgn(x));
m_mpz_manager.mul2k(o, ebits); m_mpz_manager.mul2k(o, ebits);
m_mpz_manager.add(o, biased_exp, o); const mpz & exp = m_powers2.m1(ebits);
m_mpz_manager.mul2k(o, sbits - 1); m_mpz_manager.add(o, exp, o);
m_mpz_manager.add(o, sig(x), 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) { void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {