diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 660db61d8..af972a36b 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1019,6 +1019,83 @@ void extract_example() { std::cout << y << " " << y.hi() << " " << y.lo() << "\n"; } +void sudoku_example() { + std::cout << "sudoku example\n"; + + context c; + + // 9x9 matrix of integer variables + expr_vector x(c); + for (unsigned i = 0; i < 9; ++i) + for (unsigned j = 0; j < 9; ++j) { + std::stringstream x_name; + + x_name << "x_" << i << '_' << j; + x.push_back(c.int_const(x_name.str().c_str())); + } + + solver s(c); + + // each cell contains a value in {1, ..., 9} + for (unsigned i = 0; i < 9; ++i) + for (unsigned j = 0; j < 9; ++j) { + s.add(x[i * 9 + j] >= 1 && x[i * 9 + j] <= 9); + } + + // each row contains a digit at most once + for (unsigned i = 0; i < 9; ++i) { + expr_vector t(c); + for (unsigned j = 0; j < 9; ++j) + t.push_back(x[i * 9 + j]); + s.add(distinct(t)); + } + + // each column contains a digit at most once + for (unsigned j = 0; j < 9; ++j) { + expr_vector t(c); + for (unsigned i = 0; i < 9; ++i) + t.push_back(x[i * 9 + j]); + s.add(distinct(t)); + } + + // each 3x3 square contains a digit at most once + for (unsigned i0 = 0; i0 < 3; i0++) { + for (unsigned j0 = 0; j0 < 3; j0++) { + expr_vector t(c); + for (unsigned i = 0; i < 3; i++) + for (unsigned j = 0; j < 3; j++) + t.push_back(x[(i0 * 3 + i) * 9 + j0 * 3 + j]); + s.add(distinct(t)); + } + } + + // sudoku instance, we use '0' for empty cells + int instance[9][9] = {{0,0,0,0,9,4,0,3,0}, + {0,0,0,5,1,0,0,0,7}, + {0,8,9,0,0,0,0,4,0}, + {0,0,0,0,0,0,2,0,8}, + {0,6,0,2,0,1,0,5,0}, + {1,0,2,0,0,0,0,0,0}, + {0,7,0,0,0,0,5,2,0}, + {9,0,0,0,6,5,0,0,0}, + {0,4,0,9,7,0,0,0,0}}; + + for (unsigned i = 0; i < 9; i++) + for (unsigned j = 0; j < 9; j++) + if (instance[i][j] != 0) + s.add(x[i * 9 + j] == instance[i][j]); + + std::cout << s.check() << std::endl; + std::cout << s << std::endl; + + model m = s.get_model(); + for (unsigned i = 0; i < 9; ++i) { + for (unsigned j = 0; j < 9; ++j) + std::cout << m.eval(x[i * 9 + j]); + std::cout << '\n'; + } +} + int main() { try { @@ -1060,6 +1137,7 @@ int main() { substitute_example(); std::cout << "\n"; opt_example(); std::cout << "\n"; extract_example(); std::cout << "\n"; + sudoku_example(); std::cout << "\n"; std::cout << "done\n"; } catch (exception & ex) { diff --git a/scripts/mk_util.py b/scripts/mk_util.py index d0b834e04..dff9051e8 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -8,7 +8,6 @@ ############################################ import sys import os -import glob import re import getopt import shutil @@ -17,7 +16,6 @@ from fnmatch import fnmatch import distutils.sysconfig import compileall import subprocess -import string def getenv(name, default): try: @@ -182,6 +180,8 @@ def exec_cmd(cmd): except: # Failed to create process return 1 + finally: + null.close() # rm -f fname def rmf(fname): @@ -282,7 +282,7 @@ def check_java(): if is_verbose(): print("Finding javac ...") - if JDK_HOME != None: + if JDK_HOME is not None: if IS_WINDOWS: JAVAC = os.path.join(JDK_HOME, 'bin', 'javac.exe') else: @@ -292,7 +292,7 @@ def check_java(): raise MKException("Failed to detect javac at '%s/bin'; the environment variable JDK_HOME is probably set to the wrong path." % os.path.join(JDK_HOME)) else: # Search for javac in the path. - ind = 'javac'; + ind = 'javac' if IS_WINDOWS: ind = ind + '.exe' paths = os.getenv('PATH', None) @@ -304,7 +304,7 @@ def check_java(): JAVAC = cmb break - if JAVAC == None: + if JAVAC is None: raise MKException('No java compiler in the path, please adjust your PATH or set JDK_HOME to the location of the JDK.') if is_verbose(): @@ -339,7 +339,7 @@ def check_java(): if is_verbose(): print("Finding jni.h...") - if JNI_HOME != None: + if JNI_HOME is not None: if not os.path.exists(os.path.join(JNI_HOME, 'jni.h')): raise MKException("Failed to detect jni.h '%s'; the environment variable JNI_HOME is probably set to the wrong path." % os.path.join(JNI_HOME)) else: @@ -355,6 +355,7 @@ def check_java(): q = os.path.dirname(libdir) if cdirs.count(q) == 0: cdirs.append(q) + t.close() # ... plus some heuristic ones. extra_dirs = [] @@ -371,10 +372,10 @@ def check_java(): for dir in cdirs: q = find_jni_h(dir) - if q != False: + if q is not False: JNI_HOME = q - if JNI_HOME == None: + if JNI_HOME is None: raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.") def check_ml(): @@ -416,11 +417,14 @@ def find_ml_lib(): print ('Finding OCAML_LIB...') t = TempFile('output') null = open(os.devnull, 'wb') - try: + try: subprocess.call([OCAMLC, '-where'], stdout=t.fname, stderr=null) t.commit() except: raise MKException('Failed to find Ocaml library; please set OCAML_LIB') + finally: + null.close() + t = open('output', 'r') for line in t: OCAML_LIB = line[:-1] @@ -437,12 +441,12 @@ def is64(): def check_ar(): if is_verbose(): print("Testing ar...") - if which('ar')== None: + if which('ar') is None: raise MKException('ar (archive tool) was not found') def find_cxx_compiler(): global CXX, CXX_COMPILERS - if CXX != None: + if CXX is not None: if test_cxx_compiler(CXX): return CXX for cxx in CXX_COMPILERS: @@ -453,7 +457,7 @@ def find_cxx_compiler(): def find_c_compiler(): global CC, C_COMPILERS - if CC != None: + if CC is not None: if test_c_compiler(CC): return CC for c in C_COMPILERS: @@ -479,6 +483,7 @@ def is_cr_lf(fname): # Check whether text files use cr/lf f = open(fname, 'r') line = f.readline() + f.close() sz = len(line) return sz >= 2 and line[sz-2] == '\r' and line[sz-1] == '\n' @@ -559,7 +564,7 @@ def display_help(exit_code): print(" --optimize generate optimized code during linking.") print(" -j, --java generate Java bindings.") print(" --ml generate OCaml bindings.") - print(" --staticlib build Z3 static library.") + print(" --staticlib build Z3 static library.") if not IS_WINDOWS: print(" -g, --gmp use GMP.") print(" --gprof enable gprof") @@ -674,6 +679,7 @@ def extract_c_includes(fname): elif not system_inc_pat.match(line) and non_std_inc_pat.match(line): raise MKException("Invalid #include directive at '%s':%s" % (fname, line)) linenum = linenum + 1 + f.close() return result @@ -805,7 +811,7 @@ class Component: global BUILD_DIR, SRC_DIR, REV_BUILD_DIR if name in _ComponentNames: raise MKException("Component '%s' was already defined." % name) - if path == None: + if path is None: path = name self.name = name path = norm_path(path) @@ -1019,7 +1025,7 @@ def sort_components(cnames): class ExeComponent(Component): def __init__(self, name, exe_name, path, deps, install): Component.__init__(self, name, path, deps) - if exe_name == None: + if exe_name is None: exe_name = name self.exe_name = exe_name self.install = install @@ -1113,7 +1119,7 @@ def get_so_ext(): class DLLComponent(Component): def __init__(self, name, dll_name, path, deps, export_files, reexports, install, static): Component.__init__(self, name, path, deps) - if dll_name == None: + if dll_name is None: dll_name = name self.dll_name = dll_name self.export_files = export_files @@ -1147,7 +1153,7 @@ class DLLComponent(Component): out.write(' ') out.write(obj) for dep in deps: - if not dep in self.reexports: + if dep not in self.reexports: c_dep = get_component(dep) out.write(' ' + c_dep.get_link_name()) out.write('\n') @@ -1156,7 +1162,7 @@ class DLLComponent(Component): out.write(' ') out.write(obj) for dep in deps: - if not dep in self.reexports: + if dep not in self.reexports: c_dep = get_component(dep) out.write(' ' + c_dep.get_link_name()) out.write(' ' + FOCI2LIB) @@ -1249,9 +1255,9 @@ class DLLComponent(Component): class DotNetDLLComponent(Component): def __init__(self, name, dll_name, path, deps, assembly_info_dir): Component.__init__(self, name, path, deps) - if dll_name == None: + if dll_name is None: dll_name = name - if assembly_info_dir == None: + if assembly_info_dir is None: assembly_info_dir = "." self.dll_name = dll_name self.assembly_info_dir = assembly_info_dir @@ -1315,7 +1321,7 @@ class DotNetDLLComponent(Component): class JavaDLLComponent(Component): def __init__(self, name, dll_name, package_name, manifest_file, path, deps): Component.__init__(self, name, path, deps) - if dll_name == None: + if dll_name is None: dll_name = name self.dll_name = dll_name self.package_name = package_name @@ -1406,7 +1412,7 @@ class JavaDLLComponent(Component): class MLComponent(Component): def __init__(self, name, lib_name, path, deps): Component.__init__(self, name, path, deps) - if lib_name == None: + if lib_name is None: lib_name = name self.lib_name = lib_name @@ -1426,7 +1432,7 @@ class MLComponent(Component): fout.close() if VERBOSE: print("Updated '%s'" % ml_meta_out) - + def mk_makefile(self, out): if is_ml_enabled(): @@ -1470,20 +1476,47 @@ class MLComponent(Component): archives = archives + ' ' + os.path.join(sub_dir,m) + '.cma' mls = mls + ' ' + os.path.join(sub_dir, m) + '.ml' - out.write('%s: %s %s\n' % - (os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)'), - os.path.join(sub_dir, 'z3native_stubs.c'), - get_component(Z3_DLL_COMPONENT).dll_name+'$(SO_EXT)')); - out.write('\t$(CC) $(CXXFLAGS_OCAML) -I %s -I %s %s $(CXX_OUT_FLAG)%s$(OBJ_EXT)\n' % + out.write('%s: %s %s\n' % + (os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)'), + os.path.join(sub_dir, 'z3native_stubs.c'), + get_component(Z3_DLL_COMPONENT).dll_name+'$(SO_EXT)')) + out.write('\t$(CC) $(CXXFLAGS_OCAML) -I %s -I %s %s $(CXX_OUT_FLAG)%s$(OBJ_EXT)\n' % (OCAML_LIB, api_src, os.path.join(sub_dir, 'z3native_stubs.c'), os.path.join(sub_dir, 'z3native_stubs'))) out.write('%s: %s %s %s$(SO_EXT)' % ( - os.path.join(sub_dir, "z3ml.cmxa"), - cmis, + os.path.join(sub_dir, "z3ml.cmxa"), + cmis, archives, get_component(Z3_DLL_COMPONENT).dll_name)) out.write(' %s\n' % (os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)'))) out.write('\tocamlmklib -o %s -I %s -ldopt \"-L. -lz3\" ' % (os.path.join(sub_dir, 'z3ml'), sub_dir)) + + # Add ocamlfind destdir to rpath + if OCAMLFIND != '': + if is_verbose(): + print ("Finding ocamlfind destdir") + t = TempFile('output') + null = open(os.devnull, 'wb') + try: + subprocess.call([OCAMLFIND, 'printconf', 'destdir'], stdout=t.fname, stderr=null) + t.commit() + except: + raise MKException('Failed to find Ocamlfind destdir') + t = open('output', 'r') + for line in t: + ocamlfind_destdir = line[:-1] + if is_verbose(): + print ('ocamlfind destdir=%s' % ocamlfind_destdir) + t.close() + rmf('output') + # DLLs are installed into stublibs if it exists, Z3 if not + if os.path.exists(os.path.join(ocamlfind_destdir, 'stublibs')): + dll_path = os.path.join(ocamlfind_destdir, 'stublibs') + else: + dll_path = os.path.join(ocamlfind_destdir, 'Z3') + out.write("-rpath %s " % dll_path) + out.write("-L%s" % dll_path) + for m in modules: out.write(' %s' % (os.path.join(sub_dir, m+'.ml'))) out.write(' %s\n' % (os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)'))) @@ -1518,7 +1551,7 @@ class MLComponent(Component): out.write(' ' + get_component(Z3_DLL_COMPONENT).dll_name + '$(LIB_EXT)') out.write('\n\n') - + def main_component(self): return is_ml_enabled() @@ -1642,7 +1675,7 @@ class MLExampleComponent(ExampleComponent): if ML_ENABLED: out.write('ml_example.byte: api/ml/z3ml.cmxa ') for mlfile in get_ml_files(self.ex_dir): - out.write(' %s' % os.path.join(self.to_ex_dir, mlfile)) + out.write(' %s' % os.path.join(self.to_ex_dir, mlfile)) out.write('\n') out.write('\t%s ' % OCAMLC) if DEBUG_MODE: @@ -1653,7 +1686,7 @@ class MLExampleComponent(ExampleComponent): out.write('\n') out.write('ml_example$(EXE_EXT): api/ml/z3ml.cmxa ml_example.byte') for mlfile in get_ml_files(self.ex_dir): - out.write(' %s' % os.path.join(self.to_ex_dir, mlfile)) + out.write(' %s' % os.path.join(self.to_ex_dir, mlfile)) out.write('\n') out.write('\t%s ' % OCAMLOPT) if DEBUG_MODE: @@ -1818,7 +1851,7 @@ def mk_config(): if is_verbose(): print('64-bit: %s' % is64()) print('OpenMP: %s' % HAS_OMP) - if is_java_enabled(): + if is_java_enabled(): print('JNI Bindings: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) if is_ml_enabled(): @@ -1892,6 +1925,11 @@ def mk_config(): LDFLAGS = '%s -lrt' % LDFLAGS SLIBFLAGS = '-shared' SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS + elif sysname == 'OpenBSD': + CXXFLAGS = '%s -fno-strict-aliasing -D_OPENBSD_' % CXXFLAGS + OS_DEFINES = '-D_OPENBSD_' + SO_EXT = '.so' + SLIBFLAGS = '-shared' elif sysname[:6] == 'CYGWIN': CXXFLAGS = '%s -D_CYGWIN -fno-strict-aliasing' % CXXFLAGS OS_DEFINES = '-D_CYGWIN' @@ -1943,10 +1981,10 @@ def mk_config(): print('OpenMP: %s' % HAS_OMP) print('Prefix: %s' % PREFIX) print('64-bit: %s' % is64()) - print('FP math: %s' % FPMATH) + print('FP math: %s' % FPMATH) if GPROF: print('gprof: enabled') - print('Python version: %s' % distutils.sysconfig.get_python_version()) + print('Python version: %s' % distutils.sysconfig.get_python_version()) if is_java_enabled(): print('JNI Bindings: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) @@ -1955,6 +1993,8 @@ def mk_config(): print('OCaml Native: %s' % OCAMLOPT) print('OCaml Library: %s' % OCAML_LIB) + config.close() + def mk_install(out): out.write('install: ') for c in get_components(): @@ -2028,6 +2068,7 @@ def mk_makefile(): if not IS_WINDOWS: mk_install(out) mk_uninstall(out) + out.close() # Finalize if VERBOSE: print("Makefile was successfully generated.") @@ -2102,7 +2143,7 @@ def to_c_method(s): def def_module_params(module_name, export, params, class_name=None, description=None): pyg = get_curr_pyg() dirname = os.path.split(get_curr_pyg())[0] - if class_name == None: + if class_name is None: class_name = '%s_params' % module_name hpp = os.path.join(dirname, '%s.hpp' % class_name) out = open(hpp, 'w') @@ -2128,7 +2169,7 @@ def def_module_params(module_name, export, params, class_name=None, description= if export: out.write(' /*\n') out.write(" REG_MODULE_PARAMS('%s', '%s::collect_param_descrs')\n" % (module_name, class_name)) - if description != None: + if description is not None: out.write(" REG_MODULE_DESCRIPTION('%s', '%s')\n" % (module_name, description)) out.write(' */\n') # Generated accessors @@ -2141,6 +2182,7 @@ def def_module_params(module_name, export, params, class_name=None, description= (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) out.write('};\n') out.write('#endif\n') + out.close() if is_verbose(): print("Generated '%s'" % hpp) @@ -2183,6 +2225,8 @@ def mk_pat_db(): for line in fin: fout.write('"%s\\n"\n' % line.strip('\n')) fout.write(';\n') + fin.close() + fout.close() if VERBOSE: print("Generated '%s'" % os.path.join(c.src_dir, 'database.h')) @@ -2192,7 +2236,7 @@ def update_version(): minor = VER_MINOR build = VER_BUILD revision = VER_REVISION - if major == None or minor == None or build == None or revision == None: + if major is None or minor is None or build is None or revision is None: raise MKException("set_version(major, minor, build, revision) must be used before invoking update_version()") if not ONLY_MAKEFILES: mk_version_dot_h(major, minor, build, revision) @@ -2208,6 +2252,7 @@ def mk_version_dot_h(major, minor, build, revision): fout.write('#define Z3_MINOR_VERSION %s\n' % minor) fout.write('#define Z3_BUILD_NUMBER %s\n' % build) fout.write('#define Z3_REVISION_NUMBER %s\n' % revision) + fout.close() if VERBOSE: print("Generated '%s'" % os.path.join(c.src_dir, 'version.h')) @@ -2299,6 +2344,7 @@ def mk_install_tactic_cpp(cnames, path): exec(line.strip('\n '), globals()) except: raise MKException("Failed processing ADD_PROBE command at '%s'\n%s" % (fullname, line)) + fin.close() # First pass will just generate the tactic factories idx = 0 for data in ADD_TACTIC_DATA: @@ -2314,6 +2360,7 @@ def mk_install_tactic_cpp(cnames, path): for data in ADD_PROBE_DATA: fout.write(' ADD_PROBE("%s", "%s", %s);\n' % data) fout.write('}\n') + fout.close() if VERBOSE: print("Generated '%s'" % fullname) @@ -2366,6 +2413,7 @@ def mk_mem_initializer_cpp(cnames, path): added_include = True fout.write('#include"%s"\n' % 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: @@ -2377,6 +2425,7 @@ def mk_mem_initializer_cpp(cnames, path): fout.write(cmd) fout.write('\n') fout.write('}\n') + fout.close() if VERBOSE: print("Generated '%s'" % fullname) @@ -2426,6 +2475,7 @@ def mk_gparams_register_modules(cnames, path): 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) @@ -2434,6 +2484,7 @@ def mk_gparams_register_modules(cnames, path): for (mod, descr) in mod_descrs: fout.write('gparams::register_module_descr("%s", "%s");\n' % (mod, descr)) fout.write('}\n') + fout.close() if VERBOSE: print("Generated '%s'" % fullname) @@ -2467,6 +2518,8 @@ def mk_def_file(c): fout.write('\t%s @%s\n' % (f, num)) i = i + 1 num = num + 1 + api.close() + fout.close() if VERBOSE: print("Generated '%s'" % defname) @@ -2528,7 +2581,7 @@ def mk_bindings(api_files): # Extract enumeration types from API files, and add python definitions. def mk_z3consts_py(api_files): - if Z3PY_SRC_DIR == None: + if Z3PY_SRC_DIR is None: raise MKException("You must invoke set_z3py_dir(path):") blank_pat = re.compile("^ *$") @@ -2601,6 +2654,8 @@ def mk_z3consts_py(api_files): decls[words[1]] = idx idx = idx + 1 linenum = linenum + 1 + api.close() + z3consts.close() if VERBOSE: print("Generated '%s'" % os.path.join(Z3PY_SRC_DIR, 'z3consts.py')) @@ -2622,7 +2677,7 @@ def mk_z3consts_dotnet(api_files): z3consts.write('using System;\n\n' '#pragma warning disable 1591\n\n' 'namespace Microsoft.Z3\n' - '{\n'); + '{\n') for api_file in api_files: api_file_c = dotnet.find_file(api_file, dotnet.name) @@ -2686,7 +2741,9 @@ def mk_z3consts_dotnet(api_files): decls[words[1]] = idx idx = idx + 1 linenum = linenum + 1 + api.close() z3consts.write('}\n'); + z3consts.close() if VERBOSE: print("Generated '%s'" % os.path.join(dotnet.src_dir, 'Enumerations.cs')) @@ -2754,7 +2811,7 @@ def mk_z3consts_java(api_files): if name not in DeprecatedEnums: efile = open('%s.java' % os.path.join(gendir, name), 'w') efile.write('/**\n * Automatically generated file\n **/\n\n') - efile.write('package %s.enumerations;\n\n' % java.package_name); + efile.write('package %s.enumerations;\n\n' % java.package_name) efile.write('/**\n') efile.write(' * %s\n' % name) @@ -2765,7 +2822,7 @@ def mk_z3consts_java(api_files): for k in decls: i = decls[k] if first: - first = False + first = False else: efile.write(',\n') efile.write(' %s (%s)' % (k, i)) @@ -2793,6 +2850,7 @@ def mk_z3consts_java(api_files): decls[words[1]] = idx idx = idx + 1 linenum = linenum + 1 + api.close() if VERBOSE: print("Generated '%s'" % ('%s' % gendir)) @@ -2835,7 +2893,7 @@ def mk_z3consts_ml(api_files): m2 = comment_pat.match(line) if m1 or m2: # skip blank lines and comments - linenum = linenum + 1 + linenum = linenum + 1 elif mode == SEARCHING: m = typedef_pat.match(line) if m: @@ -2888,6 +2946,8 @@ def mk_z3consts_ml(api_files): decls[words[1]] = idx idx = idx + 1 linenum = linenum + 1 + api.close() + efile.close() if VERBOSE: print ('Generated "%s/z3enums.ml"' % ('%s' % gendir)) efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w') @@ -2913,7 +2973,7 @@ def mk_z3consts_ml(api_files): m2 = comment_pat.match(line) if m1 or m2: # skip blank lines and comments - linenum = linenum + 1 + linenum = linenum + 1 elif mode == SEARCHING: m = typedef_pat.match(line) if m: @@ -2958,6 +3018,8 @@ def mk_z3consts_ml(api_files): decls[words[1]] = idx idx = idx + 1 linenum = linenum + 1 + api.close() + efile.close() if VERBOSE: print ('Generated "%s/z3enums.mli"' % ('%s' % gendir)) @@ -3094,6 +3156,7 @@ def mk_vs_proj(name, components): f.write(' \n') f.write(' \n') f.write('\n') + f.close() if is_verbose(): print("Generated '%s'" % proj_name) diff --git a/scripts/update_api.py b/scripts/update_api.py index 0d57a29ac..0b6ddfb32 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -217,16 +217,16 @@ def type2ml(ty): return Type2ML[ty] def _in(ty): - return (IN, ty); + return (IN, ty) def _in_array(sz, ty): - return (IN_ARRAY, ty, sz); + return (IN_ARRAY, ty, sz) def _out(ty): - return (OUT, ty); + return (OUT, ty) def _out_array(sz, ty): - return (OUT_ARRAY, ty, sz, sz); + return (OUT_ARRAY, ty, sz, sz) # cap contains the position of the argument that stores the capacity of the array # sz contains the position of the output argument that stores the (real) size of the array @@ -234,7 +234,7 @@ def _out_array2(cap, sz, ty): return (OUT_ARRAY, ty, cap, sz) def _inout_array(sz, ty): - return (INOUT_ARRAY, ty, sz, sz); + return (INOUT_ARRAY, ty, sz, sz) def _out_managed_array(sz,ty): return (OUT_MANAGED_ARRAY, ty, 0, sz) @@ -314,7 +314,7 @@ def param2javaw(p): else: return "jlongArray" elif k == OUT_MANAGED_ARRAY: - return "jlong"; + return "jlong" else: return type2javaw(param_type(p)) @@ -336,7 +336,7 @@ def param2ml(p): elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: return "%s array" % type2ml(param_type(p)) elif k == OUT_MANAGED_ARRAY: - return "%s array" % type2ml(param_type(p)); + return "%s array" % type2ml(param_type(p)) else: return type2ml(param_type(p)) @@ -422,14 +422,14 @@ def mk_dotnet(): dotnet.write('using System.Collections.Generic;\n') dotnet.write('using System.Text;\n') dotnet.write('using System.Runtime.InteropServices;\n\n') - dotnet.write('#pragma warning disable 1591\n\n'); + dotnet.write('#pragma warning disable 1591\n\n') dotnet.write('namespace Microsoft.Z3\n') dotnet.write('{\n') for k in Type2Str: v = Type2Str[k] if is_obj(k): dotnet.write(' using %s = System.IntPtr;\n' % v) - dotnet.write('\n'); + dotnet.write('\n') dotnet.write(' public class Native\n') dotnet.write(' {\n\n') dotnet.write(' [UnmanagedFunctionPointer(CallingConvention.Cdecl)]\n') @@ -437,7 +437,7 @@ def mk_dotnet(): dotnet.write(' public unsafe class LIB\n') dotnet.write(' {\n') dotnet.write(' const string Z3_DLL_NAME = \"libz3.dll\";\n' - ' \n'); + ' \n') dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n') dotnet.write(' public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n') for name, result, params in _dotnet_decls: @@ -448,7 +448,7 @@ def mk_dotnet(): else: dotnet.write('public extern static %s %s(' % (type2dotnet(result), name)) first = True - i = 0; + i = 0 for param in params: if first: first = False @@ -480,7 +480,7 @@ def mk_dotnet_wrappers(): else: dotnet.write(' public static %s %s(' % (type2dotnet(result), name)) first = True - i = 0; + i = 0 for param in params: if first: first = False @@ -491,9 +491,9 @@ def mk_dotnet_wrappers(): dotnet.write(') {\n') dotnet.write(' ') if result == STRING: - dotnet.write('IntPtr r = '); + dotnet.write('IntPtr r = ') elif result != VOID: - dotnet.write('%s r = ' % type2dotnet(result)); + dotnet.write('%s r = ' % type2dotnet(result)) dotnet.write('LIB.%s(' % (name)) first = True i = 0 @@ -504,14 +504,14 @@ def mk_dotnet_wrappers(): dotnet.write(', ') if param_kind(param) == OUT: if param_type(param) == STRING: - dotnet.write('out '); + dotnet.write('out ') else: dotnet.write('ref ') elif param_kind(param) == OUT_MANAGED_ARRAY: - dotnet.write('out '); + dotnet.write('out ') dotnet.write('a%d' % i) i = i + 1 - dotnet.write(');\n'); + dotnet.write(');\n') if name not in Unwrapped: if name in NULLWrapped: dotnet.write(" if (r == IntPtr.Zero)\n") @@ -578,7 +578,7 @@ def mk_java(): for name, result, params in _dotnet_decls: java_native.write(' protected static native %s INTERNAL%s(' % (type2java(result), java_method_name(name))) first = True - i = 0; + i = 0 for param in params: if first: first = False @@ -592,7 +592,7 @@ def mk_java(): for name, result, params in _dotnet_decls: java_native.write(' public static %s %s(' % (type2java(result), java_method_name(name))) first = True - i = 0; + i = 0 for param in params: if first: first = False @@ -610,7 +610,7 @@ def mk_java(): java_native.write('%s res = ' % type2java(result)) java_native.write('INTERNAL%s(' % (java_method_name(name))) first = True - i = 0; + i = 0 for param in params: if first: first = False @@ -698,7 +698,7 @@ def mk_java(): java_wrapper.write('') for name, result, params in _dotnet_decls: java_wrapper.write('DLL_VIS JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name))) - i = 0; + i = 0 for param in params: java_wrapper.write(', ') java_wrapper.write('%s a%d' % (param2javaw(param), i)) @@ -804,10 +804,10 @@ def mk_log_header(file, name, params): i = 0 for p in params: if i > 0: - file.write(", "); + file.write(", ") file.write("%s a%s" % (param2str(p), i)) i = i + 1 - file.write(")"); + file.write(")") def log_param(p): kind = param_kind(p) @@ -964,7 +964,7 @@ def def_API(name, result, params): log_c.write(" I(a%s);\n" % i) exe_c.write("in.get_bool(%s)" % i) elif ty == PRINT_MODE or ty == ERROR_CODE: - log_c.write(" U(static_cast(a%s));\n" % i); + log_c.write(" U(static_cast(a%s));\n" % i) exe_c.write("static_cast<%s>(in.get_uint(%s))" % (type2str(ty), i)) else: error("unsupported parameter for %s, %s" % (name, p)) @@ -1081,10 +1081,10 @@ def ml_method_name(name): return name[3:] # Remove Z3_ def is_out_param(p): - if param_kind(p) == OUT or param_kind(p) == INOUT or param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT_MANAGED_ARRAY: - return True - else: - return False + if param_kind(p) == OUT or param_kind(p) == INOUT or param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT_MANAGED_ARRAY: + return True + else: + return False def outparams(params): op = [] @@ -1169,7 +1169,7 @@ def mk_ml(): ml_native.write('(** The native (raw) interface to the dynamic Z3 library. *)\n\n') ml_i.write('(* Automatically generated file *)\n\n') ml_i.write('(** The native (raw) interface to the dynamic Z3 library. *)\n\n') - ml_i.write('(**/**)\n\n'); + ml_i.write('(**/**)\n\n') ml_native.write('open Z3enums\n\n') ml_native.write('(**/**)\n') ml_native.write('type ptr\n') @@ -1232,7 +1232,7 @@ def mk_ml(): ml_native.write(' = "n_%s"\n' % ml_method_name(name)) ml_native.write('\n') ml_native.write(' end\n\n') - ml_i.write('\n(**/**)\n'); + ml_i.write('\n(**/**)\n') # Exception wrappers for name, result, params in _dotnet_decls: @@ -1241,11 +1241,11 @@ def mk_ml(): ml_native.write(' let %s ' % ml_method_name(name)) first = True - i = 0; + i = 0 for p in params: if is_in_param(p): if first: - first = False; + first = False else: ml_native.write(' ') ml_native.write('a%d' % i) @@ -1262,7 +1262,7 @@ def mk_ml(): if len(ip) == 0: ml_native.write(' ()') first = True - i = 0; + i = 0 for p in params: if is_in_param(p): ml_native.write(' a%d' % i) @@ -1476,7 +1476,7 @@ def mk_ml(): if len(op) > 0: if result != VOID: ml_wrapper.write(' %s\n' % ml_set_wrap(result, "res_val", "z3_result")) - i = 0; + i = 0 for p in params: if param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY: ml_wrapper.write(' _a%s_val = caml_alloc(_a%s, 0);\n' % (i, param_array_capacity_pos(p))) @@ -1499,7 +1499,7 @@ def mk_ml(): for p in params: if is_out_param(p): ml_wrapper.write(' Store_field(result, %s, _a%s_val);\n' % (j, i)) - j = j + 1; + j = j + 1 i = i + 1 # local array cleanup diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index a5d943e95..10865deab 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -647,13 +647,7 @@ namespace z3 { */ friend expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; } - friend expr implies(expr const & a, expr const & b) { - check_context(a, b); - assert(a.is_bool() && b.is_bool()); - Z3_ast r = Z3_mk_implies(a.ctx(), a, b); - a.check_error(); - return expr(a.ctx(), r); - } + friend expr implies(expr const & a, expr const & b); friend expr implies(expr const & a, bool b); friend expr implies(bool a, expr const & b); @@ -897,6 +891,13 @@ namespace z3 { }; + inline expr implies(expr const & a, expr const & b) { + check_context(a, b); + assert(a.is_bool() && b.is_bool()); + Z3_ast r = Z3_mk_implies(a.ctx(), a, b); + a.check_error(); + return expr(a.ctx(), r); + } inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); } inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); } @@ -1911,7 +1912,7 @@ namespace z3 { -}; +} /*@}*/ /*@}*/ diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 0aee3f7d8..df502f115 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -37,8 +37,11 @@ namespace Microsoft.Z3 public Context() : base() { - m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero); - InitContext(); + lock (creation_lock) + { + m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero); + InitContext(); + } } /// @@ -64,12 +67,15 @@ namespace Microsoft.Z3 { Contract.Requires(settings != null); - IntPtr cfg = Native.Z3_mk_config(); - foreach (KeyValuePair kv in settings) - Native.Z3_set_param_value(cfg, kv.Key, kv.Value); - m_ctx = Native.Z3_mk_context_rc(cfg); - Native.Z3_del_config(cfg); - InitContext(); + lock (creation_lock) + { + IntPtr cfg = Native.Z3_mk_config(); + foreach (KeyValuePair kv in settings) + Native.Z3_set_param_value(cfg, kv.Key, kv.Value); + m_ctx = Native.Z3_mk_context_rc(cfg); + Native.Z3_del_config(cfg); + InitContext(); + } } #endregion @@ -4381,6 +4387,7 @@ namespace Microsoft.Z3 #region Internal internal IntPtr m_ctx = IntPtr.Zero; internal Native.Z3_error_handler m_n_err_handler = null; + internal static Object creation_lock = new Object(); internal IntPtr nCtx { get { return m_ctx; } } internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode) diff --git a/src/api/dotnet/Probe.cs b/src/api/dotnet/Probe.cs index c10755263..3c5e5adc9 100644 --- a/src/api/dotnet/Probe.cs +++ b/src/api/dotnet/Probe.cs @@ -28,7 +28,7 @@ namespace Microsoft.Z3 /// which solver and/or preprocessing step will be used. /// The complete list of probes may be obtained using the procedures Context.NumProbes /// and Context.ProbeNames. - /// It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end. + /// It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end. /// [ContractVerification(true)] public class Probe : Z3Object diff --git a/src/api/dotnet/Tactic.cs b/src/api/dotnet/Tactic.cs index 8399490d5..0a6f79494 100644 --- a/src/api/dotnet/Tactic.cs +++ b/src/api/dotnet/Tactic.cs @@ -26,7 +26,7 @@ namespace Microsoft.Z3 /// Tactics are the basic building block for creating custom solvers for specific problem domains. /// The complete list of tactics may be obtained using Context.NumTactics /// and Context.TacticNames. - /// It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end. + /// It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end. /// [ContractVerification(true)] public class Tactic : Z3Object diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 6b5493bf9..dc73c7ae7 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -33,7 +33,7 @@ public class AST extends Z3Object implements Comparable { AST casted = null; - try + try { casted = AST.class.cast(o); } catch (ClassCastException e) @@ -41,13 +41,12 @@ public class AST extends Z3Object implements Comparable return false; } - return - (this == casted) || - (this != null) && - (casted != null) && - (getContext().nCtx() == casted.getContext().nCtx()) && - (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject())); -} + return (this == casted) || + (this != null) && + (casted != null) && + (getContext().nCtx() == casted.getContext().nCtx()) && + (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject())); + } /** * Object Comparison. diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java index 2ceaddcff..26b33ed35 100644 --- a/src/api/java/Constructor.java +++ b/src/api/java/Constructor.java @@ -80,11 +80,20 @@ public class Constructor extends Z3Object /** * Destructor. + * @throws Throwable * @throws Z3Exception on error **/ - protected void finalize() + protected void finalize() throws Throwable { - Native.delConstructor(getContext().nCtx(), getNativeObject()); + try { + Native.delConstructor(getContext().nCtx(), getNativeObject()); + } + catch (Throwable t) { + throw t; + } + finally { + super.finalize(); + } } private int n = 0; diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java index 2b3aa94e2..82b119513 100644 --- a/src/api/java/ConstructorList.java +++ b/src/api/java/ConstructorList.java @@ -24,11 +24,20 @@ public class ConstructorList extends Z3Object { /** * Destructor. + * @throws Throwable * @throws Z3Exception on error **/ - protected void finalize() + protected void finalize() throws Throwable { - Native.delConstructorList(getContext().nCtx(), getNativeObject()); + try { + Native.delConstructorList(getContext().nCtx(), getNativeObject()); + } + catch (Throwable t) { + throw t; + } + finally { + super.finalize(); + } } ConstructorList(Context ctx, long obj) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 0955f79ca..1bc01857b 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -18,6 +18,7 @@ Notes: package com.microsoft.z3; import java.util.Map; +import java.util.concurrent.atomic.AtomicInteger; import com.microsoft.z3.enumerations.Z3_ast_print_mode; @@ -30,10 +31,12 @@ public class Context extends IDisposable * Constructor. **/ public Context() - { + { super(); - m_ctx = Native.mkContextRc(0); - initContext(); + synchronized (creation_lock) { + m_ctx = Native.mkContextRc(0); + initContext(); + } } /** @@ -56,12 +59,14 @@ public class Context extends IDisposable public Context(Map settings) { super(); - long cfg = Native.mkConfig(); - for (Map.Entry kv : settings.entrySet()) - Native.setParamValue(cfg, kv.getKey(), kv.getValue()); - m_ctx = Native.mkContextRc(cfg); - Native.delConfig(cfg); - initContext(); + synchronized (creation_lock) { + long cfg = Native.mkConfig(); + for (Map.Entry kv : settings.entrySet()) + Native.setParamValue(cfg, kv.getKey(), kv.getValue()); + m_ctx = Native.mkContextRc(cfg); + Native.delConfig(cfg); + initContext(); + } } /** @@ -365,16 +370,15 @@ public class Context extends IDisposable * Update a datatype field at expression t with value v. * The function performs a record update at t. The field * that is passed in as argument is updated with value v, - * the remainig fields of t are unchanged. + * the remainig fields of t are unchanged. **/ public Expr MkUpdateField(FuncDecl field, Expr t, Expr v) - throws Z3Exception + throws Z3Exception { - return Expr.create - (this, - Native.datatypeUpdateField - (nCtx(), field.getNativeObject(), - t.getNativeObject(), v.getNativeObject())); + return Expr.create (this, + Native.datatypeUpdateField + (nCtx(), field.getNativeObject(), + t.getNativeObject(), v.getNativeObject())); } @@ -3638,7 +3642,8 @@ public class Context extends IDisposable Native.updateParamValue(nCtx(), id, value); } - long m_ctx = 0; + protected long m_ctx = 0; + protected static Object creation_lock = new Object(); long nCtx() { @@ -3761,29 +3766,23 @@ public class Context extends IDisposable return m_Optimize_DRQ; } - protected long m_refCount = 0; + protected AtomicInteger m_refCount = new AtomicInteger(0); /** * Finalizer. + * @throws Throwable **/ - protected void finalize() + protected void finalize() throws Throwable { - dispose(); - - if (m_refCount == 0) - { - try - { - Native.delContext(m_ctx); - } catch (Z3Exception e) - { - // OK. - } - m_ctx = 0; - } - /* - else - CMW: re-queue the finalizer? */ + try { + dispose(); + } + catch (Throwable t) { + throw t; + } + finally { + super.finalize(); + } } /** @@ -3809,5 +3808,17 @@ public class Context extends IDisposable m_boolSort = null; m_intSort = null; m_realSort = null; + + synchronized (creation_lock) { + if (m_refCount.get() == 0 && m_ctx != 0) { + try { + Native.delContext(m_ctx); + } catch (Z3Exception e) { + // OK? + System.out.println("Context deletion failed; memory leak possible."); + } + m_ctx = 0; + } + } } } diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 05746af5d..47a128643 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -35,8 +35,11 @@ public class InterpolationContext extends Context **/ public InterpolationContext() { - m_ctx = Native.mkInterpolationContext(0); - initContext(); + super(); + synchronized(creation_lock) { + m_ctx = Native.mkInterpolationContext(0); + initContext(); + } } /** @@ -48,12 +51,15 @@ public class InterpolationContext extends Context **/ public InterpolationContext(Map settings) { - long cfg = Native.mkConfig(); - for (Map.Entry kv : settings.entrySet()) - Native.setParamValue(cfg, kv.getKey(), kv.getValue()); - m_ctx = Native.mkInterpolationContext(cfg); - Native.delConfig(cfg); - initContext(); + super(); + synchronized(creation_lock) { + long cfg = Native.mkConfig(); + for (Map.Entry kv : settings.entrySet()) + Native.setParamValue(cfg, kv.getKey(), kv.getValue()); + m_ctx = Native.mkInterpolationContext(cfg); + Native.delConfig(cfg); + initContext(); + } } /** diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java index e190229df..625b41e09 100644 --- a/src/api/java/Probe.java +++ b/src/api/java/Probe.java @@ -22,7 +22,7 @@ package com.microsoft.z3; * may be used to decide which solver and/or preprocessing step will be used. * The complete list of probes may be obtained using the procedures * {@code Context.NumProbes} and {@code Context.ProbeNames}. It may - * also be obtained using the command {@code (help-tactics)} in the SMT 2.0 + * also be obtained using the command {@code (help-tactic)} in the SMT 2.0 * front-end. **/ public class Probe extends Z3Object diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java index 81d886537..786f8a6ec 100644 --- a/src/api/java/Tactic.java +++ b/src/api/java/Tactic.java @@ -21,7 +21,7 @@ package com.microsoft.z3; * Tactics are the basic building block for creating custom solvers for specific * problem domains. The complete list of tactics may be obtained using * {@code Context.NumTactics} and {@code Context.TacticNames}. It may - * also be obtained using the command {@code (help-tactics)} in the SMT 2.0 + * also be obtained using the command {@code (help-tactic)} in the SMT 2.0 * front-end. **/ public class Tactic extends Z3Object diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java index 877e22cac..574a2820c 100644 --- a/src/api/java/Z3Object.java +++ b/src/api/java/Z3Object.java @@ -25,10 +25,19 @@ public class Z3Object extends IDisposable { /** * Finalizer. + * @throws Throwable **/ - protected void finalize() + protected void finalize() throws Throwable { - dispose(); + try { + dispose(); + } + catch (Throwable t) { + throw t; + } + finally { + super.finalize(); + } } /** @@ -43,8 +52,9 @@ public class Z3Object extends IDisposable } if (m_ctx != null) - { - m_ctx.m_refCount--; + { + if (m_ctx.m_refCount.decrementAndGet() == 0) + m_ctx.dispose(); m_ctx = null; } } @@ -54,13 +64,13 @@ public class Z3Object extends IDisposable Z3Object(Context ctx) { - ctx.m_refCount++; + ctx.m_refCount.incrementAndGet(); m_ctx = ctx; } Z3Object(Context ctx, long obj) { - ctx.m_refCount++; + ctx.m_refCount.incrementAndGet(); m_ctx = ctx; incRef(obj); m_n_obj = obj; diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index dba15c85d..02f29d080 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -2779,7 +2779,7 @@ end which solver and/or preprocessing step will be used. The complete list of probes may be obtained using the procedures [Context.NumProbes] and [Context.ProbeNames]. - It may also be obtained using the command [(help-tactics)] in the SMT 2.0 front-end. + It may also be obtained using the command [(help-tactic)] in the SMT 2.0 front-end. *) module Probe : sig @@ -2841,7 +2841,7 @@ end Tactics are the basic building block for creating custom solvers for specific problem domains. The complete list of tactics may be obtained using [Context.get_num_tactics] and [Context.get_tactic_names]. - It may also be obtained using the command [(help-tactics)] in the SMT 2.0 front-end. + It may also be obtained using the command [(help-tactic)] in the SMT 2.0 front-end. *) module Tactic : sig diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 5763db916..408b88e65 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -2637,7 +2637,7 @@ def _py2expr(a, ctx=None): _z3_assert(False, "Python bool, int, long or float expected") def IntSort(ctx=None): - """Return the interger sort in the given context. If `ctx=None`, then the global context is used. + """Return the integer sort in the given context. If `ctx=None`, then the global context is used. >>> IntSort() Int @@ -3920,8 +3920,8 @@ class ArrayRef(ExprRef): arg = self.domain().cast(arg) return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx) - def mk_default(self): - return _to_expr_ref(Z3_mk_array_default(self.ctx_ref(), self.as_ast()), self.ctx) + def default(self): + return _to_expr_ref(Z3_mk_array_default(self.ctx_ref(), self.as_ast()), self.ctx) def is_array(a): @@ -4064,7 +4064,7 @@ def Default(a): """ if __debug__: _z3_assert(is_array(a), "First argument must be a Z3 array expression") - return a.mk_default() + return a.default() def Store(a, i, v): @@ -7520,7 +7520,7 @@ def Interpolant(a,ctx=None): The argument is an interpolation pattern (see tree_interpolant). >>> x = Int('x') - >>> print Interpolant(x>0) + >>> print(Interpolant(x>0)) interp(x > 0) """ ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx)) @@ -7565,14 +7565,14 @@ def tree_interpolant(pat,p=None,ctx=None): >>> x = Int('x') >>> y = Int('y') - >>> print tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y)) + >>> print(tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y))) [Not(x >= 0), Not(y <= 2)] - >>> g = And(Interpolant(x<0),x<2) - >>> try: - ... print tree_interpolant(g).sexpr() - ... except ModelRef as m: - ... print m.sexpr() + # >>> g = And(Interpolant(x<0),x<2) + # >>> try: + # ... print tree_interpolant(g).sexpr() + # ... except ModelRef as m: + # ... print m.sexpr() (define-fun x () Int (- 1)) """ @@ -7631,7 +7631,7 @@ def sequence_interpolant(v,p=None,ctx=None): >>> x = Int('x') >>> y = Int('y') - >>> print sequence_interpolant([x < 0, y == x , y > 2]) + >>> print(sequence_interpolant([x < 0, y == x , y > 2])) [Not(x >= 0), Not(y >= 0)] """ f = v[0] @@ -7756,7 +7756,7 @@ def Float64(ctx=None): ctx = _get_ctx(ctx) return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx) -def FloatSingle(ctx=None): +def FloatDouble(ctx=None): """Floating-point 64-bit (double) sort.""" ctx = _get_ctx(ctx) return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx) @@ -7766,7 +7766,7 @@ def Float128(ctx=None): ctx = _get_ctx(ctx) return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx) -def FloatSingle(ctx=None): +def FloatQuadruple(ctx=None): """Floating-point 128-bit (quadruple) sort.""" ctx = _get_ctx(ctx) return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx) @@ -7835,7 +7835,7 @@ class FPRef(ExprRef): return fpLEQ(self, other) def __lt__(self, other): - return fpLEQ(self, other) + return fpLT(self, other) def __ge__(self, other): return fpGEQ(self, other) @@ -8626,13 +8626,13 @@ def fpToSBV(rm, x, s): >>> x = FP('x', FPSort(8, 24)) >>> y = fpToSBV(RTZ(), x, BitVecSort(32)) - >>> print is_fp(x) + >>> print(is_fp(x)) True - >>> print is_bv(y) + >>> print(is_bv(y)) True - >>> print is_fp(y) + >>> print(is_fp(y)) False - >>> print is_bv(x) + >>> print(is_bv(x)) False """ if __debug__: @@ -8646,13 +8646,13 @@ def fpToUBV(rm, x, s): >>> x = FP('x', FPSort(8, 24)) >>> y = fpToUBV(RTZ(), x, BitVecSort(32)) - >>> print is_fp(x) + >>> print(is_fp(x)) True - >>> print is_bv(y) + >>> print(is_bv(y)) True - >>> print is_fp(y) + >>> print(is_fp(y)) False - >>> print is_bv(x) + >>> print(is_bv(x)) False """ if __debug__: @@ -8666,13 +8666,13 @@ def fpToReal(x): >>> x = FP('x', FPSort(8, 24)) >>> y = fpToReal(x) - >>> print is_fp(x) + >>> print(is_fp(x)) True - >>> print is_real(y) + >>> print(is_real(y)) True - >>> print is_fp(y) + >>> print(is_fp(y)) False - >>> print is_real(x) + >>> print(is_real(x)) False """ if __debug__: @@ -8690,13 +8690,13 @@ def fpToIEEEBV(x): >>> x = FP('x', FPSort(8, 24)) >>> y = fpToIEEEBV(x) - >>> print is_fp(x) + >>> print(is_fp(x)) True - >>> print is_bv(y) + >>> print(is_bv(y)) True - >>> print is_fp(y) + >>> print(is_fp(y)) False - >>> print is_bv(x) + >>> print(is_bv(x)) False """ if __debug__: diff --git a/src/api/z3_algebraic.h b/src/api/z3_algebraic.h index 5e4762551..42a5fc460 100644 --- a/src/api/z3_algebraic.h +++ b/src/api/z3_algebraic.h @@ -234,7 +234,7 @@ extern "C" { /*@}*/ #ifdef __cplusplus -}; +} #endif // __cplusplus #endif diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 212fa12fd..d0bf20188 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -184,7 +184,7 @@ typedef enum Z3_PARAMETER_SYMBOL, Z3_PARAMETER_SORT, Z3_PARAMETER_AST, - Z3_PARAMETER_FUNC_DECL, + Z3_PARAMETER_FUNC_DECL } Z3_parameter_kind; /** @@ -4237,7 +4237,7 @@ END_MLAPI_EXCLUDE /** \brief Return Z3_L_TRUE if \c a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise. - def_API('Z3_get_bool_value', UINT, (_in(CONTEXT), _in(AST))) + def_API('Z3_get_bool_value', INT, (_in(CONTEXT), _in(AST))) */ Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a); @@ -6650,7 +6650,7 @@ END_MLAPI_EXCLUDE /** \brief Return a tactic associated with the given name. The complete list of tactics may be obtained using the procedures #Z3_get_num_tactics and #Z3_get_tactic_name. - It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end. + It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end. Tactics are the basic building block for creating custom solvers for specific problem domains. @@ -6677,7 +6677,7 @@ END_MLAPI_EXCLUDE /** \brief Return a probe associated with the given name. The complete list of probes may be obtained using the procedures #Z3_get_num_probes and #Z3_get_probe_name. - It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end. + It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end. Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used. @@ -7587,7 +7587,7 @@ END_MLAPI_EXCLUDE \deprecated To be moved outside of API. - def_API('Z3_get_implied_equalities', UINT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT))) + def_API('Z3_get_implied_equalities', INT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT))) */ Z3_lbool Z3_API Z3_get_implied_equalities( Z3_context c, @@ -8116,7 +8116,7 @@ END_MLAPI_EXCLUDE #ifndef CAMLIDL #ifdef __cplusplus -}; +} #endif // __cplusplus #else } diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index b29534621..ee23c7b5d 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -935,7 +935,7 @@ extern "C" { /*@}*/ #ifdef __cplusplus -}; +} #endif // __cplusplus #endif diff --git a/src/api/z3_interp.h b/src/api/z3_interp.h index d775ff3ba..84df7a874 100644 --- a/src/api/z3_interp.h +++ b/src/api/z3_interp.h @@ -287,7 +287,7 @@ extern "C" { /*@}*/ #ifdef __cplusplus -}; +} #endif // __cplusplus #endif diff --git a/src/api/z3_polynomial.h b/src/api/z3_polynomial.h index f3e40b3b2..06c492acf 100644 --- a/src/api/z3_polynomial.h +++ b/src/api/z3_polynomial.h @@ -55,7 +55,7 @@ extern "C" { /*@}*/ #ifdef __cplusplus -}; +} #endif // __cplusplus #endif diff --git a/src/api/z3_rcf.h b/src/api/z3_rcf.h index 10903750f..1736b0eba 100644 --- a/src/api/z3_rcf.h +++ b/src/api/z3_rcf.h @@ -208,7 +208,7 @@ extern "C" { /*@}*/ #ifdef __cplusplus -}; +} #endif // __cplusplus #endif diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 840222e89..111f1df78 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -516,7 +516,7 @@ inline unsigned ast_array_hash(T * const * array, unsigned size, unsigned init_v switch (size) { case 2: b += array[1]->hash(); - __fallthrough; + Z3_fallthrough; case 1: c += array[0]->hash(); } diff --git a/src/ast/ast.h b/src/ast/ast.h index 32a5c78ba..8547675a8 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1146,7 +1146,7 @@ typedef app proof; /* a proof is just an applicaton */ enum label_op_kind { OP_LABEL, - OP_LABEL_LIT, + OP_LABEL_LIT }; /** diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 2d6419d69..6c4d2dc1d 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -27,15 +27,19 @@ Notes: #define BVULT(X,Y,R) { expr_ref bvult_eq(m), bvult_not(m); m_simp.mk_eq(X, Y, bvult_eq); m_simp.mk_not(bvult_eq, bvult_not); expr_ref t(m); t = m_bv_util.mk_ule(X,Y); m_simp.mk_and(t, bvult_not, R); } #define BVSLT(X,Y,R) { expr_ref bvslt_eq(m), bvslt_not(m); m_simp.mk_eq(X, Y, bvslt_eq); m_simp.mk_not(bvslt_eq, bvslt_not); expr_ref t(m); t = m_bv_util.mk_sle(X,Y); m_simp.mk_and(t, bvslt_not, R); } -fpa2bv_converter::fpa2bv_converter(ast_manager & m) : +fpa2bv_converter::fpa2bv_converter(ast_manager & m) : m(m), m_simp(m), m_util(m), m_bv_util(m), m_arith_util(m), m_mpf_manager(m_util.fm()), - m_mpz_manager(m_mpf_manager.mpz_manager()), + m_mpz_manager(m_mpf_manager.mpz_manager()), m_hi_fp_unspecified(true), + m_min_pn_zeros(0, m), + m_min_np_zeros(0, m), + m_max_pn_zeros(0, m), + m_max_np_zeros(0, m), m_extra_assertions(m) { m_plugin = static_cast(m.get_plugin(m.mk_family_id("fpa"))); } @@ -45,35 +49,48 @@ fpa2bv_converter::~fpa2bv_converter() { } void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { - SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_FP)); - SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_FP)); + if (is_float(a) && is_float(b)) { + SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_FP)); + SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_FP)); - TRACE("fpa2bv", tout << "mk_eq a=" << mk_ismt2_pp(a, m) << std::endl; - tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;); + TRACE("fpa2bv", tout << "mk_eq a=" << mk_ismt2_pp(a, m) << std::endl; + tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;); - expr_ref eq_sgn(m), eq_exp(m), eq_sig(m); - m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), eq_sgn); - m_simp.mk_eq(to_app(a)->get_arg(1), to_app(b)->get_arg(1), eq_exp); - m_simp.mk_eq(to_app(a)->get_arg(2), to_app(b)->get_arg(2), eq_sig); + expr_ref eq_sgn(m), eq_exp(m), eq_sig(m); + m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), eq_sgn); + m_simp.mk_eq(to_app(a)->get_arg(1), to_app(b)->get_arg(1), eq_exp); + m_simp.mk_eq(to_app(a)->get_arg(2), to_app(b)->get_arg(2), eq_sig); - dbg_decouple("fpa2bv_eq_sgn", eq_sgn); - dbg_decouple("fpa2bv_eq_exp", eq_exp); - dbg_decouple("fpa2bv_eq_sig", eq_sig); + dbg_decouple("fpa2bv_eq_sgn", eq_sgn); + dbg_decouple("fpa2bv_eq_exp", eq_exp); + dbg_decouple("fpa2bv_eq_sig", eq_sig); - expr_ref both_the_same(m); - m_simp.mk_and(eq_sgn, eq_exp, eq_sig, both_the_same); - dbg_decouple("fpa2bv_eq_both_the_same", both_the_same); + expr_ref both_the_same(m); + m_simp.mk_and(eq_sgn, eq_exp, eq_sig, both_the_same); + dbg_decouple("fpa2bv_eq_both_the_same", both_the_same); - // The SMT FPA theory asks for _one_ NaN value, but the bit-blasting - // has many, like IEEE754. This encoding of equality makes it look like - // a single NaN again. - expr_ref a_is_nan(m), b_is_nan(m), both_are_nan(m); - mk_is_nan(a, a_is_nan); - mk_is_nan(b, b_is_nan); - m_simp.mk_and(a_is_nan, b_is_nan, both_are_nan); - dbg_decouple("fpa2bv_eq_both_are_nan", both_are_nan); + // The SMT FPA theory asks for _one_ NaN value, but the bit-blasting + // has many, like IEEE754. This encoding of equality makes it look like + // a single NaN again. + expr_ref a_is_nan(m), b_is_nan(m), both_are_nan(m); + mk_is_nan(a, a_is_nan); + mk_is_nan(b, b_is_nan); + m_simp.mk_and(a_is_nan, b_is_nan, both_are_nan); + dbg_decouple("fpa2bv_eq_both_are_nan", both_are_nan); - m_simp.mk_or(both_are_nan, both_the_same, result); + m_simp.mk_or(both_are_nan, both_the_same, result); + } + else if (is_rm(a) && is_rm(b)) { + SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_INTERNAL_RM)); + SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_INTERNAL_RM)); + + TRACE("fpa2bv", tout << "mk_eq_rm a=" << mk_ismt2_pp(a, m) << std::endl; + tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;); + + m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), result); + } + else + UNREACHABLE(); } void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) { @@ -94,8 +111,8 @@ void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) { } void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - // Note: in SMT there is only one NaN, so multiple of them are considered - // equal, thus (distinct NaN NaN) is false, even if the two NaNs have + // Note: in SMT there is only one NaN, so multiple of them are considered + // equal, thus (distinct NaN NaN) is false, even if the two NaNs have // different bitwise representations (see also mk_eq). result = m.mk_true(); for (unsigned i = 0; i < num; i++) { @@ -104,10 +121,10 @@ void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * a mk_eq(args[i], args[j], eq); m_simp.mk_and(result, m.mk_not(eq), result); } - } + } } -void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { +void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 0); SASSERT(f->get_num_parameters() == 1); SASSERT(f->get_parameter(0).is_external()); @@ -139,9 +156,9 @@ void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * ar mk_bias(e, biased_exp); mk_fp(bv_sgn, biased_exp, bv_sig, result); - TRACE("fpa2bv_dbg", tout << "value of [" << sign << " " << m_mpz_manager.to_string(sig) << " " << exp << "] is " + TRACE("fpa2bv_dbg", tout << "value of [" << sign << " " << m_mpz_manager.to_string(sig) << " " << exp << "] is " << mk_ismt2_pp(result, m) << std::endl;); - + } } @@ -170,7 +187,7 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) { sgn = mk_fresh_const((p + "_sgn_" + name).c_str(), 1); s = mk_fresh_const((p + "_sig_" + name).c_str(), sbits - 1); - e = mk_fresh_const((p + "_exp_" + name).c_str(), ebits); + e = mk_fresh_const((p + "_exp_" + name).c_str(), ebits); #else app_ref bv(m); unsigned bv_sz = 1 + ebits + (sbits - 1); @@ -184,12 +201,12 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) { SASSERT(m_bv_util.get_bv_size(s) == sbits-1); SASSERT(m_bv_util.get_bv_size(e) == ebits); #endif - + mk_fp(sgn, e, s, result); m_const2bv.insert(f, result); m.inc_ref(f); - m.inc_ref(result); + m.inc_ref(result); } } @@ -197,8 +214,8 @@ void fpa2bv_converter::mk_var(unsigned base_inx, sort * srt, expr_ref & result) SASSERT(is_float(srt)); unsigned ebits = m_util.get_ebits(srt); unsigned sbits = m_util.get_sbits(srt); - - expr_ref sgn(m), s(m), e(m); + + expr_ref sgn(m), s(m), e(m); sgn = m.mk_var(base_inx, m_bv_util.mk_sort(1)); s = m.mk_var(base_inx + 1, m_bv_util.mk_sort(sbits-1)); @@ -220,6 +237,11 @@ void fpa2bv_converter::mk_uninterpreted_output(sort * rng, func_decl * fbv, expr m_bv_util.mk_extract(sbits - 2, 0, na), result); } + else if (m_util.is_rm(rng)) { + app_ref na(m); + na = m.mk_app(fbv, new_args.size(), new_args.c_ptr()); + mk_rm(na, result); + } else result = m.mk_app(fbv, new_args.size(), new_args.c_ptr()); } @@ -238,11 +260,15 @@ void fpa2bv_converter::mk_uninterpreted_function(func_decl * f, unsigned num, ex expr * args[3] = { sgn, exp, sig }; new_args.push_back(m_bv_util.mk_concat(3, args)); } + else if (is_rm(args[i])) { + SASSERT(is_app_of(args[i], m_util.get_family_id(), OP_FPA_INTERNAL_RM)); + new_args.push_back(to_app(args[i])->get_arg(0)); + } else new_args.push_back(args[i]); } - func_decl * fd; + func_decl * fd; if (m_uf2bvuf.find(f, fd)) mk_uninterpreted_output(f->get_range(), fd, new_args, result); else { @@ -273,7 +299,7 @@ void fpa2bv_converter::mk_uninterpreted_function(func_decl * f, unsigned num, ex m.inc_ref(f); m.inc_ref(fbv); - mk_uninterpreted_output(f->get_range(), fbv, new_args, result); + mk_uninterpreted_output(f->get_range(), fbv, new_args, result); } TRACE("fpa2bv", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; ); @@ -291,7 +317,8 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) { else { SASSERT(is_rm(f->get_range())); - result = m.mk_fresh_const( + expr_ref bv3(m); + bv3 = m.mk_fresh_const( #ifdef Z3DEBUG "fpa2bv_rm" #else @@ -299,12 +326,13 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) { #endif , m_bv_util.mk_sort(3)); + mk_rm(bv3, result); m_rm_const2bv.insert(f, result); m.inc_ref(f); m.inc_ref(result); expr_ref rcc(m); - rcc = bu().mk_ule(result, bu().mk_numeral(4, 3)); + rcc = bu().mk_ule(bv3, bu().mk_numeral(4, 3)); m_extra_assertions.push_back(rcc); } } @@ -344,7 +372,7 @@ void fpa2bv_converter::mk_nan(func_decl * f, expr_ref & result) { mk_top_exp(ebits, top_exp); mk_fp(m_bv_util.mk_numeral(0, 1), top_exp, - m_bv_util.mk_numeral(1, sbits-1), + m_bv_util.mk_numeral(1, sbits-1), result); } @@ -385,17 +413,17 @@ void fpa2bv_converter::mk_one(func_decl *f, expr_ref sign, expr_ref & result) { result); } -void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm, +void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & c_sgn, expr_ref & c_sig, expr_ref & c_exp, expr_ref & d_sgn, expr_ref & d_sig, expr_ref & d_exp, expr_ref & res_sgn, expr_ref & res_sig, expr_ref & res_exp) -{ +{ // c/d are now such that c_exp >= d_exp. expr_ref exp_delta(m); exp_delta = m_bv_util.mk_bv_sub(c_exp, d_exp); dbg_decouple("fpa2bv_add_exp_delta", exp_delta); - // cap the delta + // cap the delta expr_ref cap(m), cap_le_delta(m); cap = m_bv_util.mk_numeral(sbits+2, ebits); cap_le_delta = m_bv_util.mk_ule(cap, exp_delta); @@ -413,7 +441,7 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm, // Alignment shift with sticky bit computation. expr_ref big_d_sig(m); big_d_sig = m_bv_util.mk_concat(d_sig, m_bv_util.mk_numeral(0, sbits+3)); - + SASSERT(is_well_sorted(m, big_d_sig)); expr_ref shifted_big(m), shifted_d_sig(m), sticky_raw(m), sticky(m); @@ -421,14 +449,14 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm, shifted_d_sig = m_bv_util.mk_extract((2*(sbits+3)-1), (sbits+3), shifted_big); SASSERT(is_well_sorted(m, shifted_d_sig)); - sticky_raw = m_bv_util.mk_extract(sbits+2, 0, shifted_big); - expr_ref sticky_eq(m), nil_sbit3(m), one_sbit3(m); + sticky_raw = m_bv_util.mk_extract(sbits+2, 0, shifted_big); + expr_ref sticky_eq(m), nil_sbit3(m), one_sbit3(m); nil_sbit3 = m_bv_util.mk_numeral(0, sbits+3); one_sbit3 = m_bv_util.mk_numeral(1, sbits+3); m_simp.mk_eq(sticky_raw, nil_sbit3, sticky_eq); m_simp.mk_ite(sticky_eq, nil_sbit3, one_sbit3, sticky); SASSERT(is_well_sorted(m, sticky)); - + expr * or_args[2] = { shifted_d_sig, sticky }; shifted_d_sig = m_bv_util.mk_bv_or(2, or_args); SASSERT(is_well_sorted(m, shifted_d_sig)); @@ -437,8 +465,8 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm, m_simp.mk_eq(c_sgn, d_sgn, eq_sgn); // dbg_decouple("fpa2bv_add_eq_sgn", eq_sgn); - TRACE("fpa2bv_add_core", tout << "EQ_SGN = " << mk_ismt2_pp(eq_sgn, m) << std::endl; ); - + TRACE("fpa2bv_add_core", tout << "EQ_SGN = " << mk_ismt2_pp(eq_sgn, m) << std::endl; ); + // two extra bits for catching the overflow. c_sig = m_bv_util.mk_zero_extend(2, c_sig); shifted_d_sig = m_bv_util.mk_zero_extend(2, shifted_d_sig); @@ -450,22 +478,22 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm, dbg_decouple("fpa2bv_add_shifted_d_sig", shifted_d_sig); expr_ref sum(m); - m_simp.mk_ite(eq_sgn, + m_simp.mk_ite(eq_sgn, m_bv_util.mk_bv_add(c_sig, shifted_d_sig), - m_bv_util.mk_bv_sub(c_sig, shifted_d_sig), + m_bv_util.mk_bv_sub(c_sig, shifted_d_sig), sum); SASSERT(is_well_sorted(m, sum)); - dbg_decouple("fpa2bv_add_sum", sum); + dbg_decouple("fpa2bv_add_sum", sum); expr_ref sign_bv(m), n_sum(m); - sign_bv = m_bv_util.mk_extract(sbits+4, sbits+4, sum); + sign_bv = m_bv_util.mk_extract(sbits+4, sbits+4, sum); n_sum = m_bv_util.mk_bv_neg(sum); - dbg_decouple("fpa2bv_add_sign_bv", sign_bv); - dbg_decouple("fpa2bv_add_n_sum", n_sum); - + dbg_decouple("fpa2bv_add_sign_bv", sign_bv); + dbg_decouple("fpa2bv_add_n_sum", n_sum); + family_id bvfid = m_bv_util.get_fid(); expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m); @@ -476,7 +504,7 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm, res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_c_sgn, d_sgn, sign_bv); res_sgn_c2 = m.mk_app(bvfid, OP_BAND, c_sgn, not_d_sgn, not_sign_bv); res_sgn_c3 = m.mk_app(bvfid, OP_BAND, c_sgn, d_sgn); - expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 }; + expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 }; res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args); expr_ref res_sig_eq(m), sig_abs(m), one_1(m); @@ -492,15 +520,16 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm, void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 3); - - expr_ref rm(m), x(m), y(m); - rm = args[0]; + SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM)); + + expr_ref bv_rm(m), x(m), y(m); + bv_rm = to_app(args[0])->get_arg(0); x = args[1]; y = args[2]; expr_ref nan(m), nzero(m), pzero(m); mk_nan(f, nan); - mk_nzero(f, nzero); + mk_nzero(f, nzero); mk_pzero(f, pzero); expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_neg(m), x_is_inf(m); @@ -529,29 +558,29 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m); expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m); - + m_simp.mk_or(x_is_nan, y_is_nan, c1); v1 = nan; - + mk_is_inf(x, c2); - expr_ref nx(m), ny(m), nx_xor_ny(m), inf_xor(m); + expr_ref nx(m), ny(m), nx_xor_ny(m), inf_xor(m); mk_is_neg(x, nx); mk_is_neg(y, ny); m_simp.mk_xor(nx, ny, nx_xor_ny); m_simp.mk_and(y_is_inf, nx_xor_ny, inf_xor); mk_ite(inf_xor, nan, x, v2); - + mk_is_inf(y, c3); - expr_ref xy_is_neg(m), v3_and(m); + expr_ref xy_is_neg(m), v3_and(m); m_simp.mk_xor(x_is_neg, y_is_neg, xy_is_neg); m_simp.mk_and(x_is_inf, xy_is_neg, v3_and); mk_ite(v3_and, nan, y, v3); - + expr_ref rm_is_to_neg(m), signs_and(m), signs_xor(m), v4_and(m), rm_and_xor(m), neg_cond(m); m_simp.mk_and(x_is_zero, y_is_zero, c4); m_simp.mk_and(x_is_neg, y_is_neg, signs_and); m_simp.mk_xor(x_is_neg, y_is_neg, signs_xor); - mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); + mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); m_simp.mk_and(rm_is_to_neg, signs_xor, rm_and_xor); m_simp.mk_or(signs_and, rm_and_xor, neg_cond); mk_ite(neg_cond, nzero, pzero, v4); @@ -566,7 +595,7 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, // Actual addition. unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m); unpack(x, a_sgn, a_sig, a_exp, a_lz, false); @@ -588,11 +617,11 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, m_simp.mk_ite(swap_cond, b_exp, a_exp, c_exp); // has ebits m_simp.mk_ite(swap_cond, a_sgn, b_sgn, d_sgn); m_simp.mk_ite(swap_cond, a_sig, b_sig, d_sig); // has sbits - m_simp.mk_ite(swap_cond, a_exp, b_exp, d_exp); // has ebits + m_simp.mk_ite(swap_cond, a_exp, b_exp, d_exp); // has ebits expr_ref res_sgn(m), res_sig(m), res_exp(m); - add_core(sbits, ebits, rm, - c_sgn, c_sig, c_exp, d_sgn, d_sig, d_exp, + add_core(sbits, ebits, + c_sgn, c_sig, c_exp, d_sgn, d_sig, d_exp, res_sgn, res_sig, res_exp); expr_ref is_zero_sig(m), nil_sbit4(m); @@ -602,15 +631,15 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, SASSERT(is_well_sorted(m, is_zero_sig)); dbg_decouple("fpa2bv_add_is_zero_sig", is_zero_sig); - + expr_ref zero_case(m); mk_ite(rm_is_to_neg, nzero, pzero, zero_case); expr_ref rounded(m); - round(f->get_range(), rm, res_sgn, res_sig, res_exp, rounded); + round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, rounded); mk_ite(is_zero_sig, zero_case, rounded, v7); - + mk_ite(c6, v6, v7, result); mk_ite(c5, v5, result, result); mk_ite(c4, v4, result, result); @@ -636,8 +665,8 @@ void fpa2bv_converter::mk_neg(func_decl * f, unsigned num, expr * const * args, expr * sgn, * s, * e; split_fp(args[0], sgn, e, s); expr_ref c(m), nsgn(m); - mk_is_nan(args[0], c); - nsgn = m_bv_util.mk_bv_not(sgn); + mk_is_nan(args[0], c); + nsgn = m_bv_util.mk_bv_not(sgn); expr_ref r_sgn(m); m_simp.mk_ite(c, sgn, nsgn, r_sgn); mk_fp(r_sgn, e, s, result); @@ -645,15 +674,16 @@ void fpa2bv_converter::mk_neg(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 3); - - expr_ref rm(m), x(m), y(m); - rm = args[0]; + SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM)); + + expr_ref bv_rm(m), x(m), y(m); + bv_rm = to_app(args[0])->get_arg(0); x = args[1]; y = args[2]; expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m); mk_nan(f, nan); - mk_nzero(f, nzero); + mk_nzero(f, nzero); mk_pzero(f, pzero); mk_ninf(f, ninf); mk_pinf(f, pinf); @@ -684,26 +714,26 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, // (x is NaN) || (y is NaN) -> NaN m_simp.mk_or(x_is_nan, y_is_nan, c1); v1 = nan; - + // (x is +oo) -> if (y is 0) then NaN else inf with y's sign. mk_is_pinf(x, c2); expr_ref y_sgn_inf(m); mk_ite(y_is_pos, pinf, ninf, y_sgn_inf); mk_ite(y_is_zero, nan, y_sgn_inf, v2); - + // (y is +oo) -> if (x is 0) then NaN else inf with x's sign. mk_is_pinf(y, c3); expr_ref x_sgn_inf(m); mk_ite(x_is_pos, pinf, ninf, x_sgn_inf); mk_ite(x_is_zero, nan, x_sgn_inf, v3); - - // (x is -oo) -> if (y is 0) then NaN else inf with -y's sign. + + // (x is -oo) -> if (y is 0) then NaN else inf with -y's sign. mk_is_ninf(x, c4); expr_ref neg_y_sgn_inf(m); mk_ite(y_is_pos, ninf, pinf, neg_y_sgn_inf); mk_ite(y_is_zero, nan, neg_y_sgn_inf, v4); - // (y is -oo) -> if (x is 0) then NaN else inf with -x's sign. + // (y is -oo) -> if (x is 0) then NaN else inf with -x's sign. mk_is_ninf(y, c5); expr_ref neg_x_sgn_inf(m); mk_ite(x_is_pos, ninf, pinf, neg_x_sgn_inf); @@ -714,9 +744,9 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref sign_xor(m); m_simp.mk_xor(x_is_pos, y_is_pos, sign_xor); mk_ite(sign_xor, nzero, pzero, v6); - - // else comes the actual multiplication. - unsigned sbits = m_util.get_sbits(f->get_range()); + + // else comes the actual multiplication. + unsigned sbits = m_util.get_sbits(f->get_range()); expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m); unpack(x, a_sgn, a_sig, a_exp, a_lz, true); @@ -732,7 +762,7 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz); dbg_decouple("fpa2bv_mul_lz_a", a_lz); - dbg_decouple("fpa2bv_mul_lz_b", b_lz); + dbg_decouple("fpa2bv_mul_lz_b", b_lz); expr_ref a_sig_ext(m), b_sig_ext(m); a_sig_ext = m_bv_util.mk_zero_extend(sbits, a_sig); @@ -762,21 +792,21 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref h_p(m), l_p(m), rbits(m); h_p = m_bv_util.mk_extract(2*sbits-1, sbits, product); l_p = m_bv_util.mk_extract(sbits-1, 0, product); - + if (sbits >= 4) { expr_ref sticky(m); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits-4, 0, product)); + sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits-4, 0, product)); rbits = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits-1, sbits-3, product), sticky); } else rbits = m_bv_util.mk_concat(l_p, m_bv_util.mk_numeral(0, 4 - sbits)); - + SASSERT(m_bv_util.get_bv_size(rbits) == 4); res_sig = m_bv_util.mk_concat(h_p, rbits); - round(f->get_range(), rm, res_sgn, res_sig, res_exp, v7); + round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, v7); - // And finally, we tie them together. + // And finally, we tie them together. mk_ite(c6, v6, v7, result); mk_ite(c5, v5, result, result); mk_ite(c4, v4, result, result); @@ -791,29 +821,30 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 3); - - expr_ref rm(m), x(m), y(m); - rm = args[0]; + SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM)); + + expr_ref bv_rm(m), x(m), y(m); + bv_rm = to_app(args[0])->get_arg(0); x = args[1]; y = args[2]; expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m); mk_nan(f, nan); - mk_nzero(f, nzero); + mk_nzero(f, nzero); mk_pzero(f, pzero); mk_ninf(f, ninf); - mk_pinf(f, pinf); + mk_pinf(f, pinf); expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m); expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m); mk_is_nan(x, x_is_nan); mk_is_zero(x, x_is_zero); mk_is_pos(x, x_is_pos); - mk_is_inf(x, x_is_inf); + mk_is_inf(x, x_is_inf); mk_is_nan(y, y_is_nan); mk_is_zero(y, y_is_zero); mk_is_pos(y, y_is_pos); - mk_is_inf(y, y_is_inf); + mk_is_inf(y, y_is_inf); dbg_decouple("fpa2bv_div_x_is_nan", x_is_nan); dbg_decouple("fpa2bv_div_x_is_zero", x_is_zero); @@ -822,7 +853,7 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_div_y_is_nan", y_is_nan); dbg_decouple("fpa2bv_div_y_is_zero", y_is_zero); dbg_decouple("fpa2bv_div_y_is_pos", y_is_pos); - dbg_decouple("fpa2bv_div_y_is_inf", y_is_inf); + dbg_decouple("fpa2bv_div_y_is_inf", y_is_inf); expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m), c7(m); expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m), v8(m); @@ -830,21 +861,21 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, // (x is NaN) || (y is NaN) -> NaN m_simp.mk_or(x_is_nan, y_is_nan, c1); v1 = nan; - + // (x is +oo) -> if (y is oo) then NaN else inf with y's sign. mk_is_pinf(x, c2); expr_ref y_sgn_inf(m); mk_ite(y_is_pos, pinf, ninf, y_sgn_inf); mk_ite(y_is_inf, nan, y_sgn_inf, v2); - + // (y is +oo) -> if (x is oo) then NaN else 0 with sign x.sgn ^ y.sgn mk_is_pinf(y, c3); expr_ref xy_zero(m), signs_xor(m); m_simp.mk_xor(x_is_pos, y_is_pos, signs_xor); mk_ite(signs_xor, nzero, pzero, xy_zero); mk_ite(x_is_inf, nan, xy_zero, v3); - - // (x is -oo) -> if (y is oo) then NaN else inf with -y's sign. + + // (x is -oo) -> if (y is oo) then NaN else inf with -y's sign. mk_is_ninf(x, c4); expr_ref neg_y_sgn_inf(m); mk_ite(y_is_pos, ninf, pinf, neg_y_sgn_inf); @@ -854,15 +885,15 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, mk_is_ninf(y, c5); mk_ite(x_is_inf, nan, xy_zero, v5); - // (y is 0) -> if (x is 0) then NaN else inf with xor sign. - c6 = y_is_zero; + // (y is 0) -> if (x is 0) then NaN else inf with xor sign. + c6 = y_is_zero; expr_ref sgn_inf(m); mk_ite(signs_xor, ninf, pinf, sgn_inf); mk_ite(x_is_zero, nan, sgn_inf, v6); // (x is 0) -> result is zero with sgn = x.sgn^y.sgn // This is a special case to avoid problems with the unpacking of zero. - c7 = x_is_zero; + c7 = x_is_zero; mk_ite(signs_xor, nzero, pzero, v7); // else comes the actual division. @@ -873,7 +904,7 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m); unpack(x, a_sgn, a_sig, a_exp, a_lz, true); unpack(y, b_sgn, b_sig, b_exp, b_lz, true); - + unsigned extra_bits = sbits+2; expr_ref a_sig_ext(m), b_sig_ext(m); a_sig_ext = m_bv_util.mk_concat(a_sig, m_bv_util.mk_numeral(0, sbits + extra_bits)); @@ -900,7 +931,7 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_div_quotient", quotient); - SASSERT(m_bv_util.get_bv_size(quotient) == (sbits + sbits + extra_bits)); + SASSERT(m_bv_util.get_bv_size(quotient) == (sbits + sbits + extra_bits)); expr_ref sticky(m); sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(extra_bits-2, 0, quotient)); @@ -910,7 +941,7 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref res_sig_lz(m); mk_leading_zeros(res_sig, sbits + 4, res_sig_lz); - dbg_decouple("fpa2bv_div_res_sig_lz", res_sig_lz); + dbg_decouple("fpa2bv_div_res_sig_lz", res_sig_lz); expr_ref res_sig_shift_amount(m); res_sig_shift_amount = m_bv_util.mk_bv_sub(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4)); dbg_decouple("fpa2bv_div_res_sig_shift_amount", res_sig_shift_amount); @@ -918,10 +949,10 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, shift_cond = m_bv_util.mk_ule(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4)); m_simp.mk_ite(shift_cond, res_sig, m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount), res_sig); m_simp.mk_ite(shift_cond, res_exp, m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits+1, 0, res_sig_shift_amount)), res_exp); - - round(f->get_range(), rm, res_sgn, res_sig, res_exp, v8); - // And finally, we tie them together. + round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, v8); + + // And finally, we tie them together. mk_ite(c7, v7, v8, result); mk_ite(c6, v6, result, result); mk_ite(c5, v5, result, result); @@ -937,7 +968,7 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); - + // Remainder is always exact, so there is no rounding mode. expr_ref x(m), y(m); x = args[0]; @@ -945,21 +976,21 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m); mk_nan(f, nan); - mk_nzero(f, nzero); + mk_nzero(f, nzero); mk_pzero(f, pzero); mk_ninf(f, ninf); - mk_pinf(f, pinf); + mk_pinf(f, pinf); expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m); expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m); mk_is_nan(x, x_is_nan); mk_is_zero(x, x_is_zero); mk_is_pos(x, x_is_pos); - mk_is_inf(x, x_is_inf); + mk_is_inf(x, x_is_inf); mk_is_nan(y, y_is_nan); mk_is_zero(y, y_is_zero); mk_is_pos(y, y_is_pos); - mk_is_inf(y, y_is_inf); + mk_is_inf(y, y_is_inf); dbg_decouple("fpa2bv_rem_x_is_nan", x_is_nan); dbg_decouple("fpa2bv_rem_x_is_zero", x_is_zero); @@ -968,7 +999,7 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_rem_y_is_nan", y_is_nan); dbg_decouple("fpa2bv_rem_y_is_zero", y_is_zero); dbg_decouple("fpa2bv_rem_y_is_pos", y_is_pos); - dbg_decouple("fpa2bv_rem_y_is_inf", y_is_inf); + dbg_decouple("fpa2bv_rem_y_is_inf", y_is_inf); expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m); expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m); @@ -980,7 +1011,7 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, // (x is +-oo) -> NaN c2 = x_is_inf; v2 = nan; - + // (y is +-oo) -> x c3 = y_is_inf; v3 = x; @@ -992,16 +1023,16 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, // (x is 0) -> x c5 = x_is_zero; v5 = pzero; - + // else the actual remainder. unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m); expr_ref b_sgn(m), b_sig(m), b_exp(m), b_lz(m); unpack(x, a_sgn, a_sig, a_exp, a_lz, true); unpack(y, b_sgn, b_sig, b_exp, b_lz, true); - + BVSLT(a_exp, b_exp, c6); v6 = x; @@ -1032,14 +1063,14 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, 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); - - // CMW: Actual rounding is not necessary here, this is - // just convenience to get rid of the extra bits. - expr_ref rm(m); - rm = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3); - round(f->get_range(), rm, res_sgn, res_sig, res_exp, v7); - // And finally, we tie them together. + // CMW: Actual rounding is not necessary here, this is + // just convenience to get rid of the extra bits. + expr_ref bv_rm(m); + bv_rm = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3); + round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, v7); + + // And finally, we tie them together. mk_ite(c6, v6, v7, result); mk_ite(c5, v5, result, result); mk_ite(c4, v4, result, result); @@ -1065,8 +1096,23 @@ void fpa2bv_converter::mk_abs(func_decl * f, unsigned num, expr * const * args, } void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + expr_ref x(m), y(m); + x = args[0]; + y = args[1]; + + expr_ref c(m), v(m); + c = m.mk_and(m.mk_and(m_util.mk_is_zero(x), m_util.mk_is_zero(y)), + m.mk_or(m.mk_and(m_util.mk_is_positive(x), m_util.mk_is_negative(y)), + m.mk_and(m_util.mk_is_negative(x), m_util.mk_is_positive(y)))); + v = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, x, y); + + // Note: This requires BR_REWRITE_FULL afterwards. + result = m.mk_ite(c, v, m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MIN_I, x, y)); +} + +void fpa2bv_converter::mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); - + expr * x = args[0], * y = args[1]; expr * x_sgn, * x_sig, * x_exp; @@ -1078,7 +1124,7 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, mk_is_zero(x, x_is_zero); mk_is_zero(y, y_is_zero); m_simp.mk_and(x_is_zero, y_is_zero, both_zero); - mk_is_nan(x, x_is_nan); + mk_is_nan(x, x_is_nan); mk_is_nan(y, y_is_nan); mk_pzero(f, pzero); @@ -1087,57 +1133,73 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref lt(m); mk_float_lt(f, num, args, lt); - - expr_ref zz(m); - zz = mk_min_unspecified(f, x, y); - TRACE("fpa2bv", tout << "min = " << mk_ismt2_pp(zz, m) << std::endl;); result = y; mk_ite(lt, x, result, result); mk_ite(both_zero, y, result, result); - mk_ite(m.mk_and(both_zero, sgn_diff), zz, result, result); mk_ite(y_is_nan, x, result, result); mk_ite(x_is_nan, y, result, result); SASSERT(is_well_sorted(m, result)); } -expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y) { +expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y) { unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); expr_ref res(m); // The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0. - + if (m_hi_fp_unspecified) // The hardware interpretation is -0.0. - mk_nzero(f, res); + mk_nzero(f, res); else { - app_ref pn_nondet(m), np_nondet(m); - pn_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - np_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_decls_to_hide.insert(pn_nondet->get_decl()); - m_decls_to_hide.insert(np_nondet->get_decl()); + if (m_min_pn_zeros == 0) { + m_min_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + m_decls_to_hide.insert_if_not_there(m_min_pn_zeros->get_decl()); + } + + if (m_min_np_zeros == 0) { + m_min_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + m_decls_to_hide.insert_if_not_there(m_min_np_zeros->get_decl()); + } expr_ref pn(m), np(m); - mk_fp(pn_nondet, + mk_fp(m_min_pn_zeros, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), pn); - mk_fp(np_nondet, + mk_fp(m_min_np_zeros, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), np); - expr_ref x_is_pzero(m), x_is_nzero(m); + + expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m); mk_is_pzero(x, x_is_pzero); mk_is_nzero(y, x_is_nzero); - mk_ite(m.mk_and(x_is_pzero, x_is_nzero), pn, np, res); + m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero); + mk_ite(xyzero, pn, np, res); } return res; } void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + expr_ref x(m), y(m); + x = args[0]; + y = args[1]; + + expr_ref c(m), v(m); + c = m.mk_and(m.mk_and(m_util.mk_is_zero(x), m_util.mk_is_zero(y)), + m.mk_or(m.mk_and(m_util.mk_is_positive(x), m_util.mk_is_negative(y)), + m.mk_and(m_util.mk_is_negative(x), m_util.mk_is_positive(y)))); + v = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, x, y); + + // Note: This requires BR_REWRITE_FULL afterwards. + result = m.mk_ite(c, v, m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MAX_I, x, y)); +} + +void fpa2bv_converter::mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); expr * x = args[0], *y = args[1]; @@ -1147,7 +1209,7 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, split_fp(x, x_sgn, x_exp, x_sig); split_fp(y, y_sgn, y_exp, y_sig); - expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m); + expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m); mk_is_zero(x, x_is_zero); mk_is_zero(y, y_is_zero); m_simp.mk_and(x_is_zero, y_is_zero, both_zero); @@ -1160,14 +1222,10 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref gt(m); mk_float_gt(f, num, args, gt); - - expr_ref zz(m); - zz = mk_max_unspecified(f, x, y); result = y; mk_ite(gt, x, result, result); - mk_ite(both_zero, y, result, result); - mk_ite(m.mk_and(both_zero, sgn_diff), zz, result, result); + mk_ite(both_zero, y, result, result); mk_ite(y_is_nan, x, result, result); mk_ite(x_is_nan, y, result, result); @@ -1182,46 +1240,53 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y) // The only cases in which max is unspecified for is when the arguments are +0.0 and -0.0. if (m_hi_fp_unspecified) - // The hardware interpretation is +0.0. + // The hardware interpretation is +0.0. mk_pzero(f, res); else { - app_ref pn_nondet(m), np_nondet(m); - pn_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - np_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_decls_to_hide.insert(pn_nondet->get_decl()); - m_decls_to_hide.insert(np_nondet->get_decl()); + if (m_max_pn_zeros == 0) { + m_max_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + m_decls_to_hide.insert_if_not_there(m_max_pn_zeros->get_decl()); + } + + if (m_max_np_zeros == 0) { + m_max_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + m_decls_to_hide.insert_if_not_there(m_max_np_zeros->get_decl()); + } expr_ref pn(m), np(m); - mk_fp(pn_nondet, + mk_fp(m_max_pn_zeros, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), pn); - mk_fp(np_nondet, + mk_fp(m_max_np_zeros, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), np); - expr_ref x_is_pzero(m), x_is_nzero(m); + + expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m); mk_is_pzero(x, x_is_pzero); mk_is_nzero(y, x_is_nzero); - mk_ite(m.mk_and(x_is_pzero, x_is_nzero), pn, np, res); + m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero); + mk_ite(xyzero, pn, np, res); } - + return res; } void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 4); - + SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM)); + // fusedma means (x * y) + z - expr_ref rm(m), x(m), y(m), z(m); - rm = args[0]; + expr_ref bv_rm(m), x(m), y(m), z(m); + bv_rm = to_app(args[0])->get_arg(0); x = args[1]; y = args[2]; z = args[3]; expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m); mk_nan(f, nan); - mk_nzero(f, nzero); + mk_nzero(f, nzero); mk_pzero(f, pzero); mk_ninf(f, ninf); mk_pinf(f, pinf); @@ -1246,7 +1311,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, mk_is_inf(z, z_is_inf); expr_ref rm_is_to_neg(m); - mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); + mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); dbg_decouple("fpa2bv_fma_x_is_nan", x_is_nan); dbg_decouple("fpa2bv_fma_x_is_zero", x_is_zero); @@ -1272,29 +1337,29 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, // (x is NaN) || (y is NaN) || (z is Nan) -> NaN m_simp.mk_or(x_is_nan, y_is_nan, z_is_nan, c1); v1 = nan; - + // (x is +oo) -> if (y is 0) then NaN else inf with y's sign. mk_is_pinf(x, c2); expr_ref y_sgn_inf(m), inf_or(m); mk_ite(y_is_pos, pinf, ninf, y_sgn_inf); m_simp.mk_or(y_is_zero, inf_cond, inf_or); mk_ite(inf_or, nan, y_sgn_inf, v2); - + // (y is +oo) -> if (x is 0) then NaN else inf with x's sign. mk_is_pinf(y, c3); expr_ref x_sgn_inf(m); mk_ite(x_is_pos, pinf, ninf, x_sgn_inf); m_simp.mk_or(x_is_zero, inf_cond, inf_or); mk_ite(inf_or, nan, x_sgn_inf, v3); - - // (x is -oo) -> if (y is 0) then NaN else inf with -y's sign. + + // (x is -oo) -> if (y is 0) then NaN else inf with -y's sign. mk_is_ninf(x, c4); expr_ref neg_y_sgn_inf(m); mk_ite(y_is_pos, ninf, pinf, neg_y_sgn_inf); m_simp.mk_or(y_is_zero, inf_cond, inf_or); mk_ite(inf_or, nan, neg_y_sgn_inf, v4); - // (y is -oo) -> if (x is 0) then NaN else inf with -x's sign. + // (y is -oo) -> if (x is 0) then NaN else inf with -x's sign. mk_is_ninf(y, c5); expr_ref neg_x_sgn_inf(m); mk_ite(x_is_pos, ninf, pinf, neg_x_sgn_inf); @@ -1310,7 +1375,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref ite_c(m); m_simp.mk_and(z_is_zero, m.mk_not(rm_is_to_neg), ite_c); mk_ite(ite_c, pzero, z, v7); - + // else comes the fused multiplication. unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); @@ -1320,7 +1385,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref c_sgn(m), c_sig(m), c_exp(m), c_lz(m); unpack(x, a_sgn, a_sig, a_exp, a_lz, true); unpack(y, b_sgn, b_sig, b_exp, b_lz, true); - unpack(z, c_sgn, c_sig, c_exp, c_lz, true); + unpack(z, c_sgn, c_sig, c_exp, c_lz, true); expr_ref a_lz_ext(m), b_lz_ext(m), c_lz_ext(m); a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz); @@ -1329,12 +1394,12 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref a_sig_ext(m), b_sig_ext(m); a_sig_ext = m_bv_util.mk_zero_extend(sbits, a_sig); - b_sig_ext = m_bv_util.mk_zero_extend(sbits, b_sig); + b_sig_ext = m_bv_util.mk_zero_extend(sbits, b_sig); expr_ref a_exp_ext(m), b_exp_ext(m), c_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); - c_exp_ext = m_bv_util.mk_sign_extend(2, c_exp); + c_exp_ext = m_bv_util.mk_sign_extend(2, c_exp); dbg_decouple("fpa2bv_fma_a_sig", a_sig_ext); dbg_decouple("fpa2bv_fma_b_sig", b_sig_ext); @@ -1355,7 +1420,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, mul_exp = m_bv_util.mk_bv_add(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_fma_mul_exp", mul_exp); - + mul_sig = m_bv_util.mk_bv_mul(a_sig_ext, b_sig_ext); dbg_decouple("fpa2bv_fma_mul_sig", mul_sig); @@ -1363,7 +1428,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, SASSERT(m_bv_util.get_bv_size(mul_exp) == ebits + 2); // The product has the form [-1][0].[2*sbits - 2]. - + // Extend c c_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits-1))); c_exp_ext = m_bv_util.mk_bv_sub(c_exp_ext, c_lz_ext); @@ -1382,7 +1447,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, m_simp.mk_ite(swap_cond, c_exp_ext, mul_exp, e_exp); // has ebits + 2 m_simp.mk_ite(swap_cond, mul_sgn, c_sgn, f_sgn); m_simp.mk_ite(swap_cond, mul_sig, c_sig, f_sig); // has 2 * sbits - m_simp.mk_ite(swap_cond, mul_exp, c_exp_ext, f_exp); // has ebits + 2 + m_simp.mk_ite(swap_cond, mul_exp, c_exp_ext, f_exp); // has ebits + 2 SASSERT(is_well_sorted(m, e_sgn)); SASSERT(is_well_sorted(m, e_sig)); @@ -1397,12 +1462,12 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, SASSERT(m_bv_util.get_bv_size(f_exp) == ebits + 2); expr_ref res_sgn(m), res_sig(m), res_exp(m); - + expr_ref exp_delta(m); exp_delta = m_bv_util.mk_bv_sub(e_exp, f_exp); dbg_decouple("fpa2bv_fma_add_exp_delta", exp_delta); - // cap the delta + // cap the delta expr_ref cap(m), cap_le_delta(m); cap = m_bv_util.mk_numeral(2*sbits, ebits+2); cap_le_delta = m_bv_util.mk_ule(cap, exp_delta); @@ -1410,23 +1475,23 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, SASSERT(m_bv_util.get_bv_size(exp_delta) == ebits+2); SASSERT(is_well_sorted(m, exp_delta)); dbg_decouple("fpa2bv_fma_add_exp_delta_capped", exp_delta); - + // Alignment shift with sticky bit computation. expr_ref shifted_big(m), shifted_f_sig(m), sticky_raw(m); shifted_big = m_bv_util.mk_bv_lshr( - m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits)), + m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits)), m_bv_util.mk_zero_extend((3*sbits)-(ebits+2), exp_delta)); shifted_f_sig = m_bv_util.mk_extract(3*sbits-1, sbits, shifted_big); - sticky_raw = m_bv_util.mk_extract(sbits-1, 0, shifted_big); + sticky_raw = m_bv_util.mk_extract(sbits-1, 0, shifted_big); SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2 * sbits); - SASSERT(is_well_sorted(m, shifted_f_sig)); - - expr_ref sticky(m); + SASSERT(is_well_sorted(m, shifted_f_sig)); + + expr_ref sticky(m); sticky = m_bv_util.mk_zero_extend(2*sbits-1, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_raw.get())); SASSERT(is_well_sorted(m, sticky)); dbg_decouple("fpa2bv_fma_f_sig_sticky_raw", sticky_raw); dbg_decouple("fpa2bv_fma_f_sig_sticky", sticky); - + expr * or_args[2] = { shifted_f_sig, sticky }; shifted_f_sig = m_bv_util.mk_bv_or(2, or_args); SASSERT(is_well_sorted(m, shifted_f_sig)); @@ -1446,9 +1511,9 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig); expr_ref sum(m); - m_simp.mk_ite(eq_sgn, + m_simp.mk_ite(eq_sgn, m_bv_util.mk_bv_add(e_sig, shifted_f_sig), - m_bv_util.mk_bv_sub(e_sig, shifted_f_sig), + m_bv_util.mk_bv_sub(e_sig, shifted_f_sig), sum); SASSERT(is_well_sorted(m, sum)); @@ -1456,19 +1521,19 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_fma_add_sum", sum); expr_ref sign_bv(m), n_sum(m); - sign_bv = m_bv_util.mk_extract(2*sbits+1, 2*sbits+1, sum); + sign_bv = m_bv_util.mk_extract(2*sbits+1, 2*sbits+1, sum); n_sum = m_bv_util.mk_bv_neg(sum); expr_ref res_sig_eq(m), sig_abs(m), one_1(m); one_1 = m_bv_util.mk_numeral(1, 1); m_simp.mk_eq(sign_bv, one_1, res_sig_eq); m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs); - dbg_decouple("fpa2bv_fma_add_sign_bv", sign_bv); - dbg_decouple("fpa2bv_fma_add_n_sum", n_sum); + dbg_decouple("fpa2bv_fma_add_sign_bv", sign_bv); + dbg_decouple("fpa2bv_fma_add_n_sum", n_sum); dbg_decouple("fpa2bv_fma_add_sig_abs", sig_abs); res_exp = e_exp; - + // Result could overflow into 4.xxx ... family_id bvfid = m_bv_util.get_fid(); @@ -1480,7 +1545,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_e_sgn, f_sgn, sign_bv); res_sgn_c2 = m.mk_app(bvfid, OP_BAND, e_sgn, not_f_sgn, not_sign_bv); res_sgn_c3 = m.mk_app(bvfid, OP_BAND, e_sgn, f_sgn); - expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 }; + expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 }; res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args); if (sbits > 5) { @@ -1503,12 +1568,12 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, SASSERT(is_well_sorted(m, is_zero_sig)); dbg_decouple("fpa2bv_fma_is_zero_sig", is_zero_sig); - + expr_ref zero_case(m); mk_ite(rm_is_to_neg, nzero, pzero, zero_case); expr_ref rounded(m); - round(f->get_range(), rm, res_sgn, res_sig, res_exp, rounded); + round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, rounded); mk_ite(is_zero_sig, zero_case, rounded, v8); @@ -1528,43 +1593,44 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); - - expr_ref rm(m), x(m); - rm = args[0]; - x = args[1]; + SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM)); + + expr_ref bv_rm(m), x(m); + bv_rm = to_app(args[0])->get_arg(0); + x = args[1]; expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m); mk_nan(f, nan); - mk_nzero(f, nzero); + mk_nzero(f, nzero); mk_pzero(f, pzero); mk_ninf(f, ninf); mk_pinf(f, pinf); - expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m); + expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m); mk_is_nan(x, x_is_nan); mk_is_zero(x, x_is_zero); mk_is_pos(x, x_is_pos); mk_is_inf(x, x_is_inf); - + expr_ref zero1(m), one1(m); zero1 = m_bv_util.mk_numeral(0, 1); one1 = m_bv_util.mk_numeral(1, 1); - + expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m); expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m); // (x is NaN) -> NaN c1 = x_is_nan; v1 = x; - + // (x is +oo) -> +oo mk_is_pinf(x, c2); v2 = x; - + // (x is +-0) -> +-0 mk_is_zero(x, c3); v3 = x; - + // (x < 0) -> NaN mk_is_neg(x, c4); v4 = nan; @@ -1596,11 +1662,11 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_sqrt_e_is_odd", e_is_odd); dbg_decouple("fpa2bv_sqrt_real_exp", real_exp); - expr_ref sig_prime(m); + expr_ref sig_prime(m); m_simp.mk_ite(e_is_odd, m_bv_util.mk_concat(a_sig, zero1), - m_bv_util.mk_concat(zero1, a_sig), + m_bv_util.mk_concat(zero1, a_sig), sig_prime); - SASSERT(m_bv_util.get_bv_size(sig_prime) == sbits+1); + SASSERT(m_bv_util.get_bv_size(sig_prime) == sbits+1); dbg_decouple("fpa2bv_sqrt_sig_prime", sig_prime); // This is algorithm 10.2 in the Handbook of Floating-Point Arithmetic @@ -1616,7 +1682,7 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_sqrt_R", R); S = m_bv_util.mk_concat(zero1, m_bv_util.mk_extract(sbits+4, 1, S)); - + expr_ref twoQ_plus_S(m); twoQ_plus_S = m_bv_util.mk_bv_add(m_bv_util.mk_concat(Q, zero1), m_bv_util.mk_concat(zero1, S)); T = m_bv_util.mk_bv_sub(m_bv_util.mk_concat(R, zero1), twoQ_plus_S); @@ -1629,21 +1695,21 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, SASSERT(m_bv_util.get_bv_size(T) == sbits + 6); expr_ref t_lt_0(m); - m_simp.mk_eq(m_bv_util.mk_extract(sbits+5, sbits+5, T), one1, t_lt_0); - + m_simp.mk_eq(m_bv_util.mk_extract(sbits+5, sbits+5, T), one1, t_lt_0); + expr * or_args[2] = { Q, S }; m_simp.mk_ite(t_lt_0, Q, m_bv_util.mk_bv_or(2, or_args), Q); - m_simp.mk_ite(t_lt_0, m_bv_util.mk_concat(m_bv_util.mk_extract(sbits+3, 0, R), zero1), - m_bv_util.mk_extract(sbits+4, 0, T), + m_simp.mk_ite(t_lt_0, m_bv_util.mk_concat(m_bv_util.mk_extract(sbits+3, 0, R), zero1), + m_bv_util.mk_extract(sbits+4, 0, T), R); } expr_ref is_exact(m); m_simp.mk_eq(R, m_bv_util.mk_numeral(0, sbits+5), is_exact); - dbg_decouple("fpa2bv_sqrt_is_exact", is_exact); + dbg_decouple("fpa2bv_sqrt_is_exact", is_exact); expr_ref rest(m), last(m), q_is_odd(m), rest_ext(m); last = m_bv_util.mk_extract(0, 0, Q); @@ -1661,7 +1727,7 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4); expr_ref rounded(m); - round(f->get_range(), rm, res_sgn, res_sig, res_exp, rounded); + round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, rounded); v5 = rounded; // And finally, we tie them together. @@ -1675,30 +1741,31 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); - - expr_ref rm(m), x(m); - rm = args[0]; + SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM)); + + expr_ref bv_rm(m), x(m); + bv_rm = to_app(args[0])->get_arg(0); x = args[1]; expr_ref rm_is_rta(m), rm_is_rte(m), rm_is_rtp(m), rm_is_rtn(m), rm_is_rtz(m); - mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_is_rta); - mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_is_rte); - mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_is_rtp); - mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_rtn); - mk_is_rm(rm, BV_RM_TO_ZERO, rm_is_rtz); + mk_is_rm(bv_rm, BV_RM_TIES_TO_AWAY, rm_is_rta); + mk_is_rm(bv_rm, BV_RM_TIES_TO_EVEN, rm_is_rte); + mk_is_rm(bv_rm, BV_RM_TO_POSITIVE, rm_is_rtp); + mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_is_rtn); + mk_is_rm(bv_rm, BV_RM_TO_ZERO, rm_is_rtz); expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m); mk_nan(f, nan); - mk_nzero(f, nzero); + mk_nzero(f, nzero); mk_pzero(f, pzero); expr_ref x_is_zero(m), x_is_pos(m), x_is_neg(m); mk_is_zero(x, x_is_zero); mk_is_pos(x, x_is_pos); mk_is_neg(x, x_is_neg); - + dbg_decouple("fpa2bv_r2i_x_is_zero", x_is_zero); - dbg_decouple("fpa2bv_r2i_x_is_pos", x_is_pos); + dbg_decouple("fpa2bv_r2i_x_is_pos", x_is_pos); expr_ref c1(m), c2(m), c3(m), c4(m), c5(m); expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m); @@ -1714,18 +1781,18 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * // (x is +-0) -> x ; -0.0 -> -0.0, says IEEE754, Sec 5.9. mk_is_zero(x, c3); v3 = x; - + expr_ref one_1(m), zero_1(m); one_1 = m_bv_util.mk_numeral(1, 1); zero_1 = m_bv_util.mk_numeral(0, 1); - + unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m); unpack(x, a_sgn, a_sig, a_exp, a_lz, true); - + dbg_decouple("fpa2bv_r2i_unpacked_sig", a_sig); dbg_decouple("fpa2bv_r2i_unpacked_exp", a_exp); @@ -1734,7 +1801,7 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * // exponent < 0 -> 0/1 expr_ref exp_lt_zero(m), exp_h(m); - exp_h = m_bv_util.mk_extract(ebits-1, ebits-1, a_exp); + exp_h = m_bv_util.mk_extract(ebits-1, ebits-1, a_exp); m_simp.mk_eq(exp_h, one_1, exp_lt_zero); dbg_decouple("fpa2bv_r2i_exp_lt_zero", exp_lt_zero); c4 = exp_lt_zero; @@ -1743,10 +1810,10 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * mk_one(f, zero_1, pone); mk_one(f, one_1, none); mk_ite(m.mk_eq(a_sgn, one_1), none, pone, xone); - + m_simp.mk_eq(a_sig, m_bv_util.mk_numeral(fu().fm().m_powers2(sbits-1), sbits), t1); m_simp.mk_eq(a_exp, m_bv_util.mk_numeral(-1, ebits), t2); - m_simp.mk_and(t1, t2, tie); + m_simp.mk_and(t1, t2, tie); dbg_decouple("fpa2bv_r2i_c42_tie", tie); m_simp.mk_and(tie, rm_is_rte, c421); @@ -1761,7 +1828,7 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * mk_ite(c423, xzero, v42, v42); mk_ite(c422, xone, v42, v42); mk_ite(c421, xzero, v42, v42); - + expr_ref v4_rtn(m), v4_rtp(m); mk_ite(x_is_neg, nzero, pone, v4_rtp); mk_ite(x_is_neg, none, pzero, v4_rtn); @@ -1771,7 +1838,7 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * mk_ite(rm_is_rtz, xzero, v4, v4); SASSERT(is_well_sorted(m, v4)); - + // exponent >= sbits-1 expr_ref exp_is_large(m); exp_is_large = m_bv_util.mk_sle(m_bv_util.mk_numeral(sbits-1, ebits), a_exp); @@ -1779,7 +1846,7 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * c5 = exp_is_large; v5 = x; - // Actual conversion with rounding. + // Actual conversion with rounding. // x.exponent >= 0 && x.exponent < x.sbits - 1 expr_ref res_sgn(m), res_sig(m), res_exp(m); @@ -1810,7 +1877,7 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * rem_shl = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits - 1, 0, rem), zero_1); m_simp.mk_eq(rem_shl, m_bv_util.mk_bv_shl(m_bv_util.mk_numeral(1, sbits+1), shift), - tie2); + tie2); div_last = m_bv_util.mk_extract(0, 0, div); tie2_c = m.mk_or(m.mk_and(tie2, m.mk_or(m.mk_and(rm_is_rte, m.mk_eq(div_last, one_1)), @@ -1841,13 +1908,13 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * c51 = m.mk_or(rm_is_rte, rm_is_rta); c52 = rm_is_rtp; c53 = rm_is_rtn; - + res_sig = div; m_simp.mk_ite(c53, v53, res_sig, res_sig); m_simp.mk_ite(c52, v52, res_sig, res_sig); m_simp.mk_ite(c51, v51, res_sig, res_sig); res_sig = m_bv_util.mk_concat(res_sig, m_bv_util.mk_numeral(0, 3)); // rounding bits are all 0. - + SASSERT(m_bv_util.get_bv_size(res_exp) == ebits); SASSERT(m_bv_util.get_bv_size(shift) == sbits + 1); @@ -1862,7 +1929,7 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * SASSERT(m_bv_util.get_bv_size(res_exp) == ebits + 2); // CMW: We use the rounder for normalization. - round(f->get_range(), rm, res_sgn, res_sig, res_exp, v6); + round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, v6); // And finally, we tie them together. mk_ite(c5, v5, v6, result); @@ -1881,7 +1948,7 @@ void fpa2bv_converter::mk_float_eq(func_decl * f, unsigned num, expr * const * a expr * x = args[0], * y = args[1]; - TRACE("fpa2bv_float_eq", tout << "X = " << mk_ismt2_pp(x, m) << std::endl; + TRACE("fpa2bv_float_eq", tout << "X = " << mk_ismt2_pp(x, m) << std::endl; tout << "Y = " << mk_ismt2_pp(y, m) << std::endl;); expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m); @@ -1896,7 +1963,7 @@ void fpa2bv_converter::mk_float_eq(func_decl * f, unsigned num, expr * const * a expr * y_sgn, * y_sig, * y_exp; split_fp(x, x_sgn, x_exp, x_sig); split_fp(y, y_sgn, y_exp, y_sig); - + expr_ref x_eq_y_sgn(m), x_eq_y_exp(m), x_eq_y_sig(m); m_simp.mk_eq(x_sgn, y_sgn, x_eq_y_sgn); m_simp.mk_eq(x_exp, y_exp, x_eq_y_exp); @@ -1919,7 +1986,7 @@ void fpa2bv_converter::mk_float_lt(func_decl * f, unsigned num, expr * const * a SASSERT(num == 2); expr * x = args[0], * y = args[1]; - + expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m); mk_is_nan(x, x_is_nan); mk_is_nan(y, y_is_nan); @@ -2054,14 +2121,14 @@ void fpa2bv_converter::mk_is_positive(func_decl * f, unsigned num, expr * const expr_ref t1(m), t2(m); mk_is_nan(args[0], t1); mk_is_pos(args[0], t2); - result = m.mk_and(m.mk_not(t1), t2); + result = m.mk_and(m.mk_not(t1), t2); } void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { TRACE("fpa2bv_to_fp", for (unsigned i=0; i < num; i++) tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl; ); - if (num == 1 && + if (num == 1 && m_bv_util.is_bv(args[0])) { sort * s = f->get_range(); unsigned to_sbits = m_util.get_sbits(s); @@ -2077,50 +2144,46 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args result); } else if (num == 2 && - m_bv_util.is_bv(args[0]) && - m_bv_util.get_bv_size(args[0]) == 3 && + m_util.is_rm(args[0]) && m_util.is_float(m.get_sort(args[1]))) { // rm + float -> float mk_to_fp_float(f, f->get_range(), args[0], args[1], result); } else if (num == 2 && - m_bv_util.is_bv(args[0]) && - m_bv_util.get_bv_size(args[0]) == 3 && - (m_arith_util.is_int(args[1]) || + m_util.is_rm(args[0]) && + (m_arith_util.is_int(args[1]) || m_arith_util.is_real(args[1]))) { // rm + real -> float mk_to_fp_real(f, f->get_range(), args[0], args[1], result); } else if (num == 2 && - m_bv_util.is_bv(args[0]) && - m_bv_util.get_bv_size(args[0]) == 3 && + m_util.is_rm(args[0]) && m_bv_util.is_bv(args[1])) { // rm + signed bv -> float mk_to_fp_signed(f, num, args, result); } - else if (num == 3 && - m_bv_util.is_bv(args[0]) && - m_bv_util.is_bv(args[1]) && - m_bv_util.is_bv(args[2])) { + else if (num == 3 && + m_bv_util.is_bv(args[0]) && + m_bv_util.is_bv(args[1]) && + m_bv_util.is_bv(args[2])) { // 3 BV -> float SASSERT(m_bv_util.get_bv_size(args[0]) == 1); SASSERT(m_util.get_ebits(f->get_range()) == m_bv_util.get_bv_size(args[1])); - SASSERT(m_util.get_sbits(f->get_range()) == m_bv_util.get_bv_size(args[2])+1); + SASSERT(m_util.get_sbits(f->get_range()) == m_bv_util.get_bv_size(args[2])+1); mk_fp(args[0], args[1], args[2], result); } else if (num == 3 && - m_bv_util.is_bv(args[0]) && - m_bv_util.get_bv_size(args[0]) == 3 && + m_util.is_rm(args[0]) && m_arith_util.is_numeral(args[1]) && m_arith_util.is_numeral(args[2])) { // rm + real + int -> float mk_to_fp_real_int(f, num, args, result); - } + } else UNREACHABLE(); - SASSERT(is_well_sorted(m, result)); + SASSERT(is_well_sorted(m, result)); } void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) { @@ -2129,6 +2192,9 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * unsigned to_sbits = m_util.get_sbits(s); unsigned to_ebits = m_util.get_ebits(s); + SASSERT(is_app_of(rm, m_util.get_family_id(), OP_FPA_INTERNAL_RM)); + expr * bv_rm = to_app(rm)->get_arg(0); + if (from_sbits == to_sbits && from_ebits == to_ebits) result = x; else { @@ -2161,7 +2227,7 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * mk_is_ninf(x, c5); v5 = ninf; - // otherwise: the actual conversion with rounding. + // otherwise: the actual conversion with rounding. expr_ref sgn(m), sig(m), exp(m), lz(m); unpack(x, sgn, sig, exp, lz, true); @@ -2188,11 +2254,11 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * expr_ref sticky(m), low(m), high(m); high = m_bv_util.mk_extract(from_sbits - 1, from_sbits - to_sbits - 2, sig); SASSERT(m_bv_util.get_bv_size(high) == to_sbits + 2); - low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig); + low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig); sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low.get()); SASSERT(m_bv_util.get_bv_size(sticky) == 1); dbg_decouple("fpa2bv_to_float_sticky", sticky); - res_sig = m_bv_util.mk_concat(high, sticky); + res_sig = m_bv_util.mk_concat(high, sticky); SASSERT(m_bv_util.get_bv_size(res_sig) == to_sbits + 3); } else @@ -2214,8 +2280,8 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * lz_ext = m_bv_util.mk_zero_extend(to_ebits - from_ebits + 2, lz); res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext); } - else if (from_ebits > (to_ebits + 2)) { - expr_ref lz_rest(m), lz_redor(m), lz_redor_bool(m); + else if (from_ebits > (to_ebits + 2)) { + expr_ref lz_rest(m), lz_redor(m), lz_redor_bool(m); lz_rest = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, lz); lz_redor = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lz_rest.get()); m_simp.mk_eq(lz_redor, one1, lz_redor_bool); @@ -2234,7 +2300,7 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * dbg_decouple("fpa2bv_to_float_exp_high", high); dbg_decouple("fpa2bv_to_float_exp_low", low); dbg_decouple("fpa2bv_to_float_exp_low_msb", low_msb); - + res_exp = low; expr_ref high_red_or(m), high_red_and(m); @@ -2251,19 +2317,19 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * dbg_decouple("fpa2bv_to_float_exp_h_or_eq_0", h_or_eq_0); dbg_decouple("fpa2bv_to_float_exp_s_is_zero", low_msb_is_zero); dbg_decouple("fpa2bv_to_float_exp_s_is_one", low_msb_is_one); - + m_simp.mk_and(h_or_eq_0, low_msb_is_one, exponent_underflow); m_simp.mk_and(h_and_eq_1, low_msb_is_zero, exponent_overflow); m_simp.mk_or(exponent_overflow, lz_redor_bool, exponent_overflow); dbg_decouple("fpa2bv_to_float_exp_ovf", exponent_overflow); dbg_decouple("fpa2bv_to_float_exp_udf", exponent_underflow); - // exponent underflow means that the result is the smallest - // representable float, rounded according to rm. - m_simp.mk_ite(exponent_underflow, + // exponent underflow means that the result is the smallest + // representable float, rounded according to rm. + m_simp.mk_ite(exponent_underflow, m_bv_util.mk_concat(m_bv_util.mk_numeral(1, 1), - m_bv_util.mk_numeral(1, to_ebits+1)), - res_exp, + m_bv_util.mk_numeral(1, to_ebits+1)), + res_exp, res_exp); m_simp.mk_ite(exponent_underflow, m_bv_util.mk_numeral(1, to_sbits+4), res_sig, res_sig); } @@ -2277,14 +2343,14 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * dbg_decouple("fpa2bv_to_float_res_exp", res_exp); expr_ref rounded(m); - expr_ref rm_e(rm, m); + expr_ref rm_e(bv_rm, m); round(s, rm_e, res_sgn, res_sig, res_exp, rounded); expr_ref is_neg(m), sig_inf(m); m_simp.mk_eq(sgn, one1, is_neg); mk_ite(is_neg, ninf, pinf, sig_inf); - mk_ite(exponent_overflow, sig_inf, rounded, v6); + mk_ite(exponent_overflow, sig_inf, rounded, v6); // And finally, we tie them together. mk_ite(c5, v5, v6, result); @@ -2298,23 +2364,24 @@ 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 << + TRACE("fpa2bv_to_fp_real", tout << "rm: " << mk_ismt2_pp(rm, 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)); + expr * bv_rm = to_app(rm)->get_arg(0); unsigned ebits = m_util.get_ebits(s); unsigned sbits = m_util.get_sbits(s); - if (m_bv_util.is_numeral(rm) && m_util.au().is_numeral(x)) { + if (m_bv_util.is_numeral(bv_rm) && m_util.au().is_numeral(x)) { rational tmp_rat; unsigned sz; - m_bv_util.is_numeral(to_expr(rm), tmp_rat, sz); + m_bv_util.is_numeral(to_expr(bv_rm), tmp_rat, sz); SASSERT(tmp_rat.is_int32()); SASSERT(sz == 3); - BV_RM_VAL bv_rm = (BV_RM_VAL)tmp_rat.get_unsigned(); mpf_rounding_mode mrm; - switch (bv_rm) { + switch ((BV_RM_VAL)tmp_rat.get_unsigned()) { case BV_RM_TIES_TO_AWAY: mrm = MPF_ROUND_NEAREST_TAWAY; break; case BV_RM_TIES_TO_EVEN: mrm = MPF_ROUND_NEAREST_TEVEN; break; case BV_RM_TO_NEGATIVE: mrm = MPF_ROUND_TOWARD_NEGATIVE; break; @@ -2351,11 +2418,11 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * mk_pzero(f, result); else { expr_ref rm_nta(m), rm_nte(m), rm_tp(m), rm_tn(m), rm_tz(m); - mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_nta); - mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_nte); - mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_tp); - mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_tn); - mk_is_rm(rm, BV_RM_TO_ZERO, rm_tz); + mk_is_rm(bv_rm, BV_RM_TIES_TO_AWAY, rm_nta); + mk_is_rm(bv_rm, BV_RM_TIES_TO_EVEN, rm_nte); + mk_is_rm(bv_rm, BV_RM_TO_POSITIVE, rm_tp); + mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_tn); + mk_is_rm(bv_rm, BV_RM_TO_ZERO, rm_tz); scoped_mpf v_nta(m_mpf_manager), v_nte(m_mpf_manager), v_tp(m_mpf_manager); scoped_mpf v_tn(m_mpf_manager), v_tz(m_mpf_manager); @@ -2416,13 +2483,13 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * two = au.mk_numeral(rational(2), false); expr_ref sgn(m), sig(m), exp(m); - sgn = mk_fresh_const("fpa2bv_to_fp_real_sgn", 1); + sgn = mk_fresh_const("fpa2bv_to_fp_real_sgn", 1); sig = mk_fresh_const("fpa2bv_to_fp_real_sig", sbits + 4); exp = mk_fresh_const("fpa2bv_to_fp_real_exp", ebits + 2); - expr_ref rme(rm, m); + expr_ref rme(bv_rm, m); round(s, rme, sgn, sig, exp, result); - + expr * e = m.mk_eq(m_util.mk_to_real(result), x); m_extra_assertions.push_back(e); } @@ -2436,7 +2503,8 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); - expr * rm = args[0]; + SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM)); + expr * bv_rm = to_app(args[0])->get_arg(0); rational q; if (!m_arith_util.is_numeral(args[1], q)) @@ -2474,10 +2542,10 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con mk_numeral(a_tz->get_decl(), 0, 0, bv_tz); expr_ref c1(m), c2(m), c3(m), c4(m); - c1 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)); - c2 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)); - c3 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)); - c4 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3)); + c1 = m.mk_eq(bv_rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)); + c2 = m.mk_eq(bv_rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)); + c3 = m.mk_eq(bv_rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)); + c4 = m.mk_eq(bv_rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3)); mk_ite(c1, bv_tn, bv_tz, result); mk_ite(c2, bv_tp, result, result); @@ -2576,19 +2644,20 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const // This is a conversion from signed bitvector to float: // ; from signed machine integer, represented as a 2's complement bit vector // ((_ to_fp eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb)) - // Semantics: + // Semantics: // Let b in[[(_ BitVec m)]] and let n be the signed integer represented by b (in 2's complement format). - // [[(_ to_fp eb sb)]](r, b) = +/ -infinity if n is too large / too small to be represented as a finite - // number of [[(_ FloatingPoint eb sb)]]; [[(_ to_fp eb sb)]](r, x) = y otherwise, where y is the finite - // number such that [[fp.to_real]](y) is closest to n according to rounding mode r. + // [[(_ to_fp eb sb)]](r, b) = +/ -infinity if n is too large / too small to be represented as a finite + // number of [[(_ FloatingPoint eb sb)]]; [[(_ to_fp eb sb)]](r, x) = y otherwise, where y is the finite + // number such that [[fp.to_real]](y) is closest to n according to rounding mode r. SASSERT(num == 2); SASSERT(m_util.is_float(f->get_range())); SASSERT(m_bv_util.is_bv(args[0])); SASSERT(m_bv_util.is_bv(args[1])); + SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM)); - expr_ref rm(m), x(m); - rm = args[0]; + expr_ref bv_rm(m), x(m); + bv_rm = to_app(args[0])->get_arg(0); x = args[1]; dbg_decouple("fpa2bv_to_fp_signed_x", x); @@ -2596,7 +2665,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); unsigned bv_sz = m_bv_util.get_bv_size(x); - SASSERT(m_bv_util.get_bv_size(rm) == 3); + SASSERT(m_bv_util.get_bv_size(bv_rm) == 3); expr_ref bv0_1(m), bv1_1(m), bv0_sz(m), bv1_sz(m); bv0_1 = m_bv_util.mk_numeral(0, 1); @@ -2613,7 +2682,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const // Special case: x == 0 -> p/n zero expr_ref c1(m), v1(m); - c1 = is_zero; + c1 = is_zero; v1 = pzero; // Special case: x != 0 @@ -2651,13 +2720,13 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const expr_ref extra_zeros(m); extra_zeros = m_bv_util.mk_numeral(0, extra_bits); sig_4 = m_bv_util.mk_concat(shifted_sig, extra_zeros); - lz = m_bv_util.mk_bv_add(m_bv_util.mk_concat(extra_zeros, lz), + lz = m_bv_util.mk_bv_add(m_bv_util.mk_concat(extra_zeros, lz), m_bv_util.mk_numeral(extra_bits, sig_sz)); bv_sz = bv_sz + extra_bits; SASSERT(is_well_sorted(m, lz)); } SASSERT(m_bv_util.get_bv_size(sig_4) == sig_sz); - + expr_ref s_exp(m), exp_rest(m); s_exp = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(bv_sz - 2, bv_sz), lz); // s_exp = (bv_sz-2) + (-lz) signed @@ -2665,13 +2734,13 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const unsigned exp_sz = ebits + 2; // (+2 for rounder) exp_2 = m_bv_util.mk_extract(exp_sz - 1, 0, s_exp); - // the remaining bits are 0 if ebits is large enough. + // the remaining bits are 0 if ebits is large enough. exp_too_large = m.mk_false(); // The exponent is at most bv_sz, i.e., we need ld(bv_sz)+1 ebits. - // exp < bv_sz (+sign bit which is [0]) + // exp < bv_sz (+sign bit which is [0]) unsigned exp_worst_case_sz = (unsigned)((log((double)bv_sz) / log((double)2)) + 1.0); - + TRACE("fpa2bv_to_fp_signed", tout << "exp worst case sz: " << exp_worst_case_sz << std::endl;); if (exp_sz < exp_worst_case_sz) { @@ -2683,13 +2752,13 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const max_exp_bvsz = m_bv_util.mk_zero_extend(bv_sz - exp_sz, max_exp); exp_too_large = m_bv_util.mk_ule(m_bv_util.mk_bv_add( - max_exp_bvsz, - m_bv_util.mk_numeral(1, bv_sz)), + max_exp_bvsz, + m_bv_util.mk_numeral(1, bv_sz)), s_exp); sig_4 = m.mk_ite(exp_too_large, m_bv_util.mk_numeral(0, sig_sz), sig_4); exp_2 = m.mk_ite(exp_too_large, max_exp, exp_2); } - dbg_decouple("fpa2bv_to_fp_signed_exp_too_large", exp_too_large); + dbg_decouple("fpa2bv_to_fp_signed_exp_too_large", exp_too_large); expr_ref sgn(m), sig(m), exp(m); sgn = is_neg_bit; @@ -2702,10 +2771,10 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const SASSERT(m_bv_util.get_bv_size(sig) == sbits + 4); SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2); - + expr_ref v2(m); - round(f->get_range(), rm, sgn, sig, exp, v2); - + round(f->get_range(), bv_rm, sgn, sig, exp, v2); + mk_ite(c1, v1, v2, result); } @@ -2724,11 +2793,11 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con SASSERT(num == 2); SASSERT(m_util.is_float(f->get_range())); - SASSERT(m_bv_util.is_bv(args[0])); + SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM)); SASSERT(m_bv_util.is_bv(args[1])); - expr_ref rm(m), x(m); - rm = args[0]; + expr_ref bv_rm(m), x(m); + bv_rm = to_app(args[0])->get_arg(0); x = args[1]; dbg_decouple("fpa2bv_to_fp_unsigned_x", x); @@ -2736,7 +2805,7 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); unsigned bv_sz = m_bv_util.get_bv_size(x); - SASSERT(m_bv_util.get_bv_size(rm) == 3); + SASSERT(m_bv_util.get_bv_size(bv_rm) == 3); expr_ref bv0_1(m), bv1_1(m), bv0_sz(m), bv1_sz(m); bv0_1 = m_bv_util.mk_numeral(0, 1); @@ -2757,7 +2826,7 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con v1 = pzero; // Special case: x != 0 - expr_ref exp_too_large(m), sig_4(m), exp_2(m); + expr_ref exp_too_large(m), sig_4(m), exp_2(m); // x is [bv_sz-1] . [bv_sz-2 ... 0] * 2^(bv_sz-1) // bv_sz-1 is the "1.0" bit for the rounder. @@ -2799,12 +2868,12 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con unsigned exp_sz = ebits + 2; // (+2 for rounder) exp_2 = m_bv_util.mk_extract(exp_sz - 1, 0, s_exp); - // the remaining bits are 0 if ebits is large enough. - exp_too_large = m.mk_false(); // This is always in range. + // the remaining bits are 0 if ebits is large enough. + exp_too_large = m.mk_false(); // This is always in range. // The exponent is at most bv_sz, i.e., we need ld(bv_sz)+1 ebits. - // exp < bv_sz (+sign bit which is [0]) - unsigned exp_worst_case_sz = (unsigned)((log((double)bv_sz) / log((double)2)) + 1.0); + // exp < bv_sz (+sign bit which is [0]) + unsigned exp_worst_case_sz = (unsigned)((log((double)bv_sz) / log((double)2)) + 1.0); if (exp_sz < exp_worst_case_sz) { // exp_sz < exp_worst_case_sz and exp >= 0. @@ -2836,7 +2905,7 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2); expr_ref v2(m); - round(f->get_range(), rm, sgn, sig, exp, v2); + round(f->get_range(), bv_rm, sgn, sig, exp, v2); mk_ite(c1, v1, v2, result); } @@ -2851,14 +2920,12 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) { TRACE("fpa2bv_to_bv", for (unsigned i = 0; i < num; i++) tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); - - SASSERT(f->get_num_parameters() == 1); - SASSERT(f->get_parameter(0).is_int()); + SASSERT(num == 2); - SASSERT(m_bv_util.get_bv_size(args[0]) == 3); + SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM)); SASSERT(m_util.is_float(args[1])); - expr * rm = args[0]; + expr * bv_rm = to_app(args[0])->get_arg(0); expr * x = args[1]; sort * xs = m.get_sort(x); sort * bv_srt = f->get_range(); @@ -2866,9 +2933,8 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args unsigned ebits = m_util.get_ebits(xs); unsigned sbits = m_util.get_sbits(xs); unsigned bv_sz = (unsigned)f->get_parameter(0).get_int(); - + expr_ref bv0(m), bv1(m); - bv0 = m_bv_util.mk_numeral(0, 1); bv1 = m_bv_util.mk_numeral(1, 1); expr_ref x_is_nan(m), x_is_inf(m), x_is_zero(m), x_is_neg(m), x_is_nzero(m); @@ -2906,7 +2972,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args SASSERT(m_bv_util.get_bv_size(sgn) == 1); SASSERT(m_bv_util.get_bv_size(sig) == sbits); SASSERT(m_bv_util.get_bv_size(exp) == ebits); - SASSERT(m_bv_util.get_bv_size(lz) == ebits); + SASSERT(m_bv_util.get_bv_size(lz) == ebits); unsigned sig_sz = m_bv_util.get_bv_size(sig); SASSERT(sig_sz == sbits); @@ -2916,10 +2982,10 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args SASSERT(sig_sz >= (bv_sz + 3)); expr_ref exp_m_lz(m), e_m_lz_m_bv_sz(m), shift(m), bv0_e2(m), shift_abs(m); - exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp), + exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp), m_bv_util.mk_zero_extend(2, lz)); e_m_lz_m_bv_sz = m_bv_util.mk_bv_sub(exp_m_lz, - m_bv_util.mk_numeral(bv_sz - 1, ebits + 2)); + m_bv_util.mk_numeral(bv_sz - 1, ebits + 2)); shift = m_bv_util.mk_bv_neg(e_m_lz_m_bv_sz); bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2); shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), e_m_lz_m_bv_sz, shift); @@ -2928,7 +2994,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args dbg_decouple("fpa2bv_to_bv_shift", shift); dbg_decouple("fpa2bv_to_bv_shift_abs", shift_abs); - // x is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long + // x is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long // [1][ ... sig ... ][r][g][ ... s ...] // [ ... ubv ... ][r][g][ ... s ... ] @@ -2957,11 +3023,11 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args round = m_bv_util.mk_extract(sig_sz - bv_sz - 1, sig_sz - bv_sz - 1, r_shifted_sig); sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, l_shifted_sig.get()); dbg_decouple("fpa2bv_to_bv_last", last); - dbg_decouple("fpa2bv_to_bv_round", round); + dbg_decouple("fpa2bv_to_bv_round", round); dbg_decouple("fpa2bv_to_bv_sticky", sticky); - + expr_ref rounding_decision(m); - rounding_decision = mk_rounding_decision(rm, sgn, last, round, sticky); + rounding_decision = mk_rounding_decision(bv_rm, sgn, last, round, sticky); SASSERT(m_bv_util.get_bv_size(rounding_decision) == 1); dbg_decouple("fpa2bv_to_bv_rounding_decision", rounding_decision); @@ -3024,6 +3090,11 @@ expr_ref fpa2bv_converter::mk_to_real_unspecified() { return expr_ref(m_util.mk_internal_to_real_unspecified(), m); } +void fpa2bv_converter::mk_rm(expr * bv3, expr_ref & result) { + SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3); + result = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_RM, 0, 0, 1, &bv3, m_util.mk_rm_sort()); +} + void fpa2bv_converter::mk_fp(expr * sign, expr * exponent, expr * significand, expr_ref & result) { SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1); SASSERT(m_bv_util.is_bv(significand)); @@ -3042,8 +3113,8 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e void fpa2bv_converter::split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const { SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_FP)); - SASSERT(to_app(e)->get_num_args() == 3); - sgn = to_app(e)->get_arg(0); + SASSERT(to_app(e)->get_num_args() == 3); + sgn = to_app(e)->get_arg(0); exp = to_app(e)->get_arg(1); sig = to_app(e)->get_arg(2); } @@ -3055,13 +3126,13 @@ void fpa2bv_converter::split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_r split_fp(e, e_sgn, e_exp, e_sig); sgn = e_sgn; exp = e_exp; - sig = e_sig; + sig = e_sig; } void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; split_fp(e, sgn, exp, sig); - + // exp == 1^n , sig != 0 expr_ref sig_is_zero(m), sig_is_not_zero(m), exp_is_top(m), top_exp(m), zero(m); mk_top_exp(m_bv_util.get_bv_size(exp), top_exp); @@ -3160,7 +3231,7 @@ void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) { m_simp.mk_and(n_is_zero, zexp, result); } -void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) { +void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; split_fp(e, sgn, exp, sig); @@ -3177,18 +3248,18 @@ void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) { m_simp.mk_not(or_ex, result); } -void fpa2bv_converter::mk_is_rm(expr * e, BV_RM_VAL rm, expr_ref & result) { - SASSERT(m_bv_util.is_bv(e) && m_bv_util.get_bv_size(e) == 3); +void fpa2bv_converter::mk_is_rm(expr * bv_rm, BV_RM_VAL rm, expr_ref & result) { expr_ref rm_num(m); rm_num = m_bv_util.mk_numeral(rm, 3); + switch(rm) { - case BV_RM_TIES_TO_AWAY: - case BV_RM_TIES_TO_EVEN: + case BV_RM_TIES_TO_AWAY: + case BV_RM_TIES_TO_EVEN: case BV_RM_TO_NEGATIVE: - case BV_RM_TO_POSITIVE: - case BV_RM_TO_ZERO: - return m_simp.mk_eq(e, rm_num, result); + case BV_RM_TO_POSITIVE: + case BV_RM_TO_ZERO: + return m_simp.mk_eq(bv_rm, rm_num, result); default: UNREACHABLE(); } @@ -3209,11 +3280,11 @@ void fpa2bv_converter::mk_min_exp(unsigned ebits, expr_ref & result) { } void fpa2bv_converter::mk_max_exp(unsigned ebits, expr_ref & result) { - SASSERT(ebits >= 2); - result = m_bv_util.mk_numeral(m_mpf_manager.m_powers2.m1(ebits-1, false), ebits); + SASSERT(ebits >= 2); + result = m_bv_util.mk_numeral(m_mpf_manager.m_powers2.m1(ebits-1, false), ebits); } -void fpa2bv_converter::mk_leading_zeros(expr * e, unsigned max_bits, expr_ref & result) { +void fpa2bv_converter::mk_leading_zeros(expr * e, unsigned max_bits, expr_ref & result) { SASSERT(m_bv_util.is_bv(e)); unsigned bv_sz = m_bv_util.get_bv_size(e); @@ -3241,18 +3312,18 @@ void fpa2bv_converter::mk_leading_zeros(expr * e, unsigned max_bits, expr_ref & expr_ref H_is_zero(m), nil_h(m); nil_h = m_bv_util.mk_numeral(0, H_size); - m_simp.mk_eq(H, nil_h, H_is_zero); + m_simp.mk_eq(H, nil_h, H_is_zero); expr_ref sum(m), h_m(m); h_m = m_bv_util.mk_numeral(H_size, max_bits); sum = m_bv_util.mk_bv_add(h_m, lzL); - m_simp.mk_ite(H_is_zero, sum, lzH, result); + m_simp.mk_ite(H_is_zero, sum, lzH, result); } SASSERT(is_well_sorted(m, result)); } -void fpa2bv_converter::mk_bias(expr * e, expr_ref & result) { +void fpa2bv_converter::mk_bias(expr * e, expr_ref & result) { unsigned ebits = m_bv_util.get_bv_size(e); SASSERT(ebits >= 2); @@ -3307,7 +3378,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref denormal_sig = m_bv_util.mk_zero_extend(1, sig); denormal_exp = m_bv_util.mk_numeral(1, ebits); mk_unbias(denormal_exp, denormal_exp); - dbg_decouple("fpa2bv_unpack_denormal_exp", denormal_exp); + dbg_decouple("fpa2bv_unpack_denormal_exp", denormal_exp); expr_ref zero_e(m); zero_e = m_bv_util.mk_numeral(0, ebits); @@ -3318,7 +3389,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref m_simp.mk_eq(zero_s, denormal_sig, is_sig_zero); expr_ref lz_d(m); - mk_leading_zeros(denormal_sig, ebits, lz_d); + mk_leading_zeros(denormal_sig, ebits, lz_d); m_simp.mk_ite(m.mk_or(is_normal, is_sig_zero), zero_e, lz_d, lz); dbg_decouple("fpa2bv_unpack_lz", lz); @@ -3328,24 +3399,24 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref SASSERT(is_well_sorted(m, is_sig_zero)); SASSERT(is_well_sorted(m, shift)); SASSERT(m_bv_util.get_bv_size(shift) == ebits); - if (ebits <= sbits) { + if (ebits <= sbits) { expr_ref q(m); q = m_bv_util.mk_zero_extend(sbits-ebits, shift); - denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, q); - } + denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, q); + } else { // the maximum shift is `sbits', because after that the mantissa // would be zero anyways. So we can safely cut the shift variable down, - // as long as we check the higher bits. + // as long as we check the higher bits. expr_ref sh(m), is_sh_zero(m), sl(m), sbits_s(m), short_shift(m); zero_s = m_bv_util.mk_numeral(0, sbits-1); sbits_s = m_bv_util.mk_numeral(sbits, sbits); - sh = m_bv_util.mk_extract(ebits-1, sbits, shift); + sh = m_bv_util.mk_extract(ebits-1, sbits, shift); m_simp.mk_eq(zero_s, sh, is_sh_zero); short_shift = m_bv_util.mk_extract(sbits-1, 0, shift); m_simp.mk_ite(is_sh_zero, short_shift, sbits_s, sl); denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, sl); - } + } } else lz = zero_e; @@ -3378,15 +3449,17 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result) switch(f->get_decl_kind()) { case OP_FPA_RM_NEAREST_TIES_TO_EVEN: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3); break; - case OP_FPA_RM_NEAREST_TIES_TO_AWAY: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3); break; + case OP_FPA_RM_NEAREST_TIES_TO_AWAY: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3); break; case OP_FPA_RM_TOWARD_POSITIVE: result = m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3); break; - case OP_FPA_RM_TOWARD_NEGATIVE: result = m_bv_util.mk_numeral(BV_RM_TO_NEGATIVE, 3); break; + case OP_FPA_RM_TOWARD_NEGATIVE: result = m_bv_util.mk_numeral(BV_RM_TO_NEGATIVE, 3); break; case OP_FPA_RM_TOWARD_ZERO: result = m_bv_util.mk_numeral(BV_RM_TO_ZERO, 3); break; default: UNREACHABLE(); } + + mk_rm(result, result); } -void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { +void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { #ifdef Z3DEBUG return; // CMW: This works only for quantifier-free formulas. @@ -3397,8 +3470,8 @@ void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { #endif } -expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * last, expr * round, expr * sticky) { - expr_ref rmr(rm, m); +expr_ref fpa2bv_converter::mk_rounding_decision(expr * bv_rm, expr * sgn, expr * last, expr * round, expr * sticky) { + expr_ref rmr(bv_rm, m); expr_ref sgnr(sgn, m); expr_ref lastr(last, m); expr_ref roundr(round, m); @@ -3420,7 +3493,7 @@ expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * la not_lors = m_bv_util.mk_bv_not(last_or_sticky); not_rors = m_bv_util.mk_bv_not(round_or_sticky); not_sgn = m_bv_util.mk_bv_not(sgn); - expr * nround_lors[2] = { not_round, not_lors }; + expr * nround_lors[2] = { not_round, not_lors }; expr * pos_args[2] = { sgn, not_rors }; expr * neg_args[2] = { not_sgn, not_rors }; expr * nl_r[2] = { last, not_round }; @@ -3437,32 +3510,32 @@ expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * la expr_ref res(m), inc_c2(m), inc_c3(m), inc_c4(m); expr_ref rm_is_to_neg(m), rm_is_to_pos(m), rm_is_away(m), rm_is_even(m), nil_1(m); nil_1 = m_bv_util.mk_numeral(0, 1); - mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); - mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_is_to_pos); - mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_is_away); - mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_is_even); + mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); + mk_is_rm(bv_rm, BV_RM_TO_POSITIVE, rm_is_to_pos); + mk_is_rm(bv_rm, BV_RM_TIES_TO_AWAY, rm_is_away); + mk_is_rm(bv_rm, BV_RM_TIES_TO_EVEN, rm_is_even); m_simp.mk_ite(rm_is_to_neg, inc_neg, nil_1, inc_c4); m_simp.mk_ite(rm_is_to_pos, inc_pos, inc_c4, inc_c3); m_simp.mk_ite(rm_is_away, inc_taway, inc_c3, inc_c2); m_simp.mk_ite(rm_is_even, inc_teven, inc_c2, res); - + dbg_decouple("fpa2bv_rnd_dec_res", res); return res; } -void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & result) { +void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & result) { unsigned ebits = m_util.get_ebits(s); unsigned sbits = m_util.get_sbits(s); - dbg_decouple("fpa2bv_rnd_rm", rm); + dbg_decouple("fpa2bv_rnd_rm", bv_rm); dbg_decouple("fpa2bv_rnd_sgn", sgn); dbg_decouple("fpa2bv_rnd_sig", sig); - dbg_decouple("fpa2bv_rnd_exp", exp); + dbg_decouple("fpa2bv_rnd_exp", exp); - SASSERT(is_well_sorted(m, rm)); + SASSERT(is_well_sorted(m, bv_rm)); SASSERT(is_well_sorted(m, sgn)); SASSERT(is_well_sorted(m, sig)); - SASSERT(is_well_sorted(m, exp)); + SASSERT(is_well_sorted(m, exp)); TRACE("fpa2bv_dbg", tout << "RND: " << std::endl << "ebits = " << ebits << std::endl << @@ -3471,11 +3544,11 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & "sig = " << mk_ismt2_pp(sig, m) << std::endl << "exp = " << mk_ismt2_pp(exp, m) << std::endl; ); - // Assumptions: sig is of the form f[-1:0] . f[1:sbits-1] [guard,round,sticky], + // Assumptions: sig is of the form f[-1:0] . f[1:sbits-1] [guard,round,sticky], // i.e., it has 2 + (sbits-1) + 3 = sbits + 4 bits, where the first one is in sgn. // Furthermore, note that sig is an unsigned bit-vector, while exp is signed. - - SASSERT(m_bv_util.is_bv(rm) && m_bv_util.get_bv_size(rm) == 3); + + SASSERT(m_bv_util.is_bv(bv_rm) && m_bv_util.get_bv_size(bv_rm) == 3); SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1); SASSERT(m_bv_util.is_bv(sig) && m_bv_util.get_bv_size(sig) >= 5); SASSERT(m_bv_util.is_bv(exp) && m_bv_util.get_bv_size(exp) >= 4); @@ -3491,7 +3564,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & mk_max_exp(ebits, e_max); TRACE("fpa2bv_dbg", tout << "e_min = " << mk_ismt2_pp(e_min, m) << std::endl << - "e_max = " << mk_ismt2_pp(e_max, m) << std::endl;); + "e_max = " << mk_ismt2_pp(e_max, m) << std::endl;); expr_ref OVF1(m), e_top_three(m), sigm1(m), e_eq_emax_and_sigm1(m), e_eq_emax(m); expr_ref e3(m), ne3(m), e2(m), e1(m), e21(m), one_1(m), h_exp(m), sh_exp(m), th_exp(m); @@ -3513,10 +3586,10 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & m_simp.mk_eq(t_sig, one_1, sigm1); m_simp.mk_and(e_eq_emax, sigm1, e_eq_emax_and_sigm1); m_simp.mk_or(e_top_three, e_eq_emax_and_sigm1, OVF1); - + dbg_decouple("fpa2bv_rnd_OVF1", OVF1); - TRACE("fpa2bv_dbg", tout << "OVF1 = " << mk_ismt2_pp(OVF1, m) << std::endl;); + TRACE("fpa2bv_dbg", tout << "OVF1 = " << mk_ismt2_pp(OVF1, m) << std::endl;); SASSERT(is_well_sorted(m, OVF1)); expr_ref lz(m); @@ -3528,19 +3601,19 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & expr_ref t(m); t = m_bv_util.mk_bv_add(exp, m_bv_util.mk_numeral(1, ebits+2)); - t = m_bv_util.mk_bv_sub(t, lz); + t = m_bv_util.mk_bv_sub(t, lz); t = m_bv_util.mk_bv_sub(t, m_bv_util.mk_sign_extend(2, e_min)); dbg_decouple("fpa2bv_rnd_t", t); - expr_ref TINY(m); + expr_ref TINY(m); TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral((unsigned)-1, ebits+2)); dbg_decouple("fpa2bv_rnd_TINY", TINY); TRACE("fpa2bv_dbg", tout << "TINY = " << mk_ismt2_pp(TINY, m) << std::endl;); - SASSERT(is_well_sorted(m, TINY)); + SASSERT(is_well_sorted(m, TINY)); - expr_ref beta(m); + expr_ref beta(m); beta = m_bv_util.mk_bv_add(m_bv_util.mk_bv_sub(exp, lz), m_bv_util.mk_numeral(1, ebits+2)); - TRACE("fpa2bv_dbg", tout << "beta = " << mk_ismt2_pp(beta, m)<< std::endl; ); + TRACE("fpa2bv_dbg", tout << "beta = " << mk_ismt2_pp(beta, m)<< std::endl; ); SASSERT(is_well_sorted(m, beta)); dbg_decouple("fpa2bv_rnd_beta", beta); @@ -3565,7 +3638,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & SASSERT(m_bv_util.get_bv_size(sigma) == ebits+2); unsigned sigma_size = ebits+2; - expr_ref sigma_neg(m), sigma_cap(m), sigma_neg_capped(m), sigma_lt_zero(m), sig_ext(m), + expr_ref sigma_neg(m), sigma_cap(m), sigma_neg_capped(m), sigma_lt_zero(m), sig_ext(m), rs_sig(m), ls_sig(m), big_sh_sig(m), sigma_le_cap(m); sigma_neg = m_bv_util.mk_bv_neg(sigma); sigma_cap = m_bv_util.mk_numeral(sbits+2, sigma_size); @@ -3577,7 +3650,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral((unsigned)-1, sigma_size)); dbg_decouple("fpa2bv_rnd_sigma_lt_zero", sigma_lt_zero); - sig_ext = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_size)); + sig_ext = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_size)); rs_sig = m_bv_util.mk_bv_lshr(sig_ext, m_bv_util.mk_zero_extend(2*sig_size - sigma_size, sigma_neg_capped)); ls_sig = m_bv_util.mk_bv_shl(sig_ext, m_bv_util.mk_zero_extend(2*sig_size - sigma_size, sigma)); m_simp.mk_ite(sigma_lt_zero, rs_sig, ls_sig, big_sh_sig); @@ -3602,8 +3675,8 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & expr * tmp[] = { sig, ext_sticky }; sig = m_bv_util.mk_bv_or(2, tmp); SASSERT(is_well_sorted(m, sig)); - SASSERT(m_bv_util.get_bv_size(sig) == sbits+2); - + SASSERT(m_bv_util.get_bv_size(sig) == sbits+2); + // CMW: The (OVF1 && OVFen) and (TINY && UNFen) cases are never taken. expr_ref ext_emin(m); ext_emin = m_bv_util.mk_zero_extend(2, e_min); @@ -3612,7 +3685,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & // Significand rounding expr_ref round(m), last(m); - sticky = m_bv_util.mk_extract(0, 0, sig); // new sticky bit! + sticky = m_bv_util.mk_extract(0, 0, sig); // new sticky bit! round = m_bv_util.mk_extract(1, 1, sig); last = m_bv_util.mk_extract(2, 2, sig); @@ -3625,22 +3698,22 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & sig = m_bv_util.mk_extract(sbits+1, 2, sig); expr_ref inc(m); - inc = mk_rounding_decision(rm, sgn, last, round, sticky); - + inc = mk_rounding_decision(bv_rm, sgn, last, round, sticky); + SASSERT(m_bv_util.get_bv_size(inc) == 1 && is_well_sorted(m, inc)); dbg_decouple("fpa2bv_rnd_inc", inc); - sig = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(1, sig), + sig = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(1, sig), m_bv_util.mk_zero_extend(sbits, inc)); SASSERT(is_well_sorted(m, sig)); dbg_decouple("fpa2bv_rnd_sig_plus_inc", sig); - // Post normalization + // Post normalization SASSERT(m_bv_util.get_bv_size(sig) == sbits + 1); expr_ref SIGovf(m); t_sig = m_bv_util.mk_extract(sbits, sbits, sig); m_simp.mk_eq(t_sig, one_1, SIGovf); - SASSERT(is_well_sorted(m, SIGovf)); + SASSERT(is_well_sorted(m, SIGovf)); dbg_decouple("fpa2bv_rnd_SIGovf", SIGovf); expr_ref hallbut1_sig(m), lallbut1_sig(m); @@ -3658,12 +3731,12 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & SASSERT(is_well_sorted(m, exp)); dbg_decouple("fpa2bv_rnd_sig_postnormalized", sig); dbg_decouple("fpa2bv_rnd_exp_postnormalized", exp); - + SASSERT(m_bv_util.get_bv_size(sig) == sbits); SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2); SASSERT(m_bv_util.get_bv_size(e_max) == ebits); - // Exponent adjustment and rounding + // Exponent adjustment and rounding expr_ref biased_exp(m); mk_bias(m_bv_util.mk_extract(ebits-1, 0, exp), biased_exp); dbg_decouple("fpa2bv_rnd_unbiased_exp", exp); @@ -3680,10 +3753,10 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & pem2m1 = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-2), ebits); m_simp.mk_ite(OVF2, pem2m1, biased_exp, biased_exp); m_simp.mk_or(OVF1, OVF2, OVF); - + SASSERT(is_well_sorted(m, OVF2)); SASSERT(is_well_sorted(m, OVF)); - + SASSERT(m.is_bool(OVF2)); SASSERT(m.is_bool(OVF)); dbg_decouple("fpa2bv_rnd_OVF2", OVF2); @@ -3692,15 +3765,15 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & // ExpRnd expr_ref top_exp(m), bot_exp(m); mk_top_exp(ebits, top_exp); - mk_bot_exp(ebits, bot_exp); + mk_bot_exp(ebits, bot_exp); expr_ref nil_1(m); nil_1 = m_bv_util.mk_numeral(0, 1); - expr_ref rm_is_to_zero(m), rm_is_to_neg(m), rm_is_to_pos(m), rm_zero_or_neg(m), rm_zero_or_pos(m); - mk_is_rm(rm, BV_RM_TO_ZERO, rm_is_to_zero); - mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); - mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_is_to_pos); + expr_ref rm_is_to_zero(m), rm_is_to_neg(m), rm_is_to_pos(m), rm_zero_or_neg(m), rm_zero_or_pos(m); + mk_is_rm(bv_rm, BV_RM_TO_ZERO, rm_is_to_zero); + mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); + mk_is_rm(bv_rm, BV_RM_TO_POSITIVE, rm_is_to_pos); m_simp.mk_or(rm_is_to_zero, rm_is_to_neg, rm_zero_or_neg); m_simp.mk_or(rm_is_to_zero, rm_is_to_pos, rm_zero_or_pos); dbg_decouple("fpa2bv_rnd_rm_is_to_zero", rm_is_to_zero); @@ -3724,7 +3797,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & dbg_decouple("fpa2bv_rnd_inf_sig", inf_sig); dbg_decouple("fpa2bv_rnd_inf_exp", inf_exp); - expr_ref ovfl_exp(m), max_inf_exp_neg(m), max_inf_exp_pos(m), n_d_check(m), n_d_exp(m); + expr_ref ovfl_exp(m), max_inf_exp_neg(m), max_inf_exp_pos(m), n_d_check(m), n_d_exp(m); m_simp.mk_ite(rm_zero_or_pos, max_exp, inf_exp, max_inf_exp_neg); m_simp.mk_ite(rm_zero_or_neg, max_exp, inf_exp, max_inf_exp_pos); m_simp.mk_ite(sgn_is_zero, max_inf_exp_pos, max_inf_exp_neg, ovfl_exp); @@ -3739,7 +3812,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & m_simp.mk_ite(sgn_is_zero, max_inf_sig_pos, max_inf_sig_neg, ovfl_sig); rest_sig = m_bv_util.mk_extract(sbits-2, 0, sig); m_simp.mk_ite(OVF, ovfl_sig, rest_sig, sig); - + dbg_decouple("fpa2bv_rnd_max_inf_sig_neg", max_inf_sig_neg); dbg_decouple("fpa2bv_rnd_max_inf_sig_pos", max_inf_sig_pos); dbg_decouple("fpa2bv_rnd_rm_zero_or_neg", rm_zero_or_neg); @@ -3753,7 +3826,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & res_sgn = sgn; res_sig = sig; res_exp = exp; - + SASSERT(m_bv_util.get_bv_size(res_sgn) == 1); SASSERT(is_well_sorted(m, res_sgn)); SASSERT(m_bv_util.get_bv_size(res_sig) == sbits-1); @@ -3771,6 +3844,9 @@ void fpa2bv_converter::reset(void) { dec_ref_map_key_values(m, m_const2bv); dec_ref_map_key_values(m, m_rm_const2bv); dec_ref_map_key_values(m, m_uf2bvuf); - + m_min_np_zeros = 0; + m_min_pn_zeros = 0; + m_max_np_zeros = 0; + m_max_pn_zeros = 0; m_extra_assertions.reset(); } diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 819216bd0..95f2ca057 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -26,8 +26,6 @@ Notes: #include"bv_decl_plugin.h" #include"basic_simplifier_plugin.h" -typedef enum { BV_RM_TIES_TO_EVEN, BV_RM_TIES_TO_AWAY, BV_RM_TO_POSITIVE, BV_RM_TO_NEGATIVE, BV_RM_TO_ZERO = 4 } BV_RM_VAL; - struct func_decl_triple { func_decl_triple () { f_sgn = 0; f_sig = 0; f_exp = 0; } func_decl_triple (func_decl * sgn, func_decl * sig, func_decl * exp) @@ -57,6 +55,11 @@ protected: obj_map m_rm_const2bv; obj_map m_uf2bvuf; obj_hashtable m_decls_to_hide; + + app_ref m_min_pn_zeros; + app_ref m_min_np_zeros; + app_ref m_max_pn_zeros; + app_ref m_max_np_zeros; public: fpa2bv_converter(ast_manager & m); @@ -68,17 +71,19 @@ public: bool is_float(sort * s) { return m_util.is_float(s); } bool is_float(expr * e) { return is_app(e) && m_util.is_float(to_app(e)->get_decl()->get_range()); } - bool is_rm(expr * e) { return m_util.is_rm(e); } + bool is_rm(expr * e) { return is_app(e) && m_util.is_rm(e); } bool is_rm(sort * s) { return m_util.is_rm(s); } bool is_float_family(func_decl * f) { return f->get_family_id() == m_util.get_family_id(); } + void mk_rm(expr * bv3, expr_ref & result); + void mk_fp(expr * sign, expr * exponent, expr * significand, expr_ref & result); void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const; void split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const; - void mk_eq(expr * a, expr * b, expr_ref & result); + void mk_eq(expr * a, expr * b, expr_ref & result); void mk_ite(expr * c, expr * t, expr * f, expr_ref & result); void mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -101,9 +106,7 @@ public: void mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -138,7 +141,12 @@ public: void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; } + void mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y); + + void mk_max(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); expr_ref mk_to_ubv_unspecified(unsigned width); @@ -186,7 +194,7 @@ protected: void round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & result); expr_ref mk_rounding_decision(expr * rm, expr * sgn, expr * last, expr * round, expr * sticky); - void add_core(unsigned sbits, unsigned ebits, expr_ref & rm, + void add_core(unsigned sbits, unsigned ebits, expr_ref & c_sgn, expr_ref & c_sig, expr_ref & c_exp, expr_ref & d_sgn, expr_ref & d_sig, expr_ref & d_exp, expr_ref & res_sgn, expr_ref & res_sig, expr_ref & res_exp); diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index 69c9a6290..c3720421c 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -123,7 +123,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { } if (m_conv.is_float_family(f)) { - switch (f->get_decl_kind()) { + switch (f->get_decl_kind()) { case OP_FPA_RM_NEAREST_TIES_TO_AWAY: case OP_FPA_RM_NEAREST_TIES_TO_EVEN: case OP_FPA_RM_TOWARD_NEGATIVE: @@ -141,9 +141,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FPA_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE; case OP_FPA_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE; case OP_FPA_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE; - case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE; - case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE; - case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE; + case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE; case OP_FPA_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE; case OP_FPA_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE; case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE; @@ -166,8 +164,16 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; + + case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL; + case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL; + case OP_FPA_INTERNAL_MIN_UNSPECIFIED: result = m_conv.mk_min_unspecified(f, args[0], args[1]); return BR_DONE; case OP_FPA_INTERNAL_MAX_UNSPECIFIED: result = m_conv.mk_max_unspecified(f, args[0], args[1]); return BR_DONE; + case OP_FPA_INTERNAL_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE; + case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE; + + case OP_FPA_INTERNAL_RM: case OP_FPA_INTERNAL_BVWRAP: case OP_FPA_INTERNAL_BVUNWRAP: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: @@ -179,21 +185,21 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { NOT_IMPLEMENTED_YET(); } } - - if (f->get_family_id() != 0 && f->get_family_id() != m_conv.fu().get_family_id()) - { + else { + SASSERT(!m_conv.is_float_family(f)); bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range()); - - for (unsigned i = 0; i < num; i++) - is_float_uf |= m_conv.is_float(f->get_domain()[i]) || m_conv.is_rm(f->get_domain()[i]); - if (is_float_uf) - { + for (unsigned i = 0; i < f->get_arity(); i++) { + sort * di = f->get_domain()[i]; + is_float_uf |= m_conv.is_float(di) || m_conv.is_rm(di); + } + + if (is_float_uf) { m_conv.mk_uninterpreted_function(f, num, args, result); return BR_DONE; } } - + return BR_FAILED; } diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index ec410fd18..d32aa5e6d 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -359,6 +359,10 @@ func_decl * fpa_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_parameters case OP_FPA_REM: name = "fp.rem"; break; case OP_FPA_MIN: name = "fp.min"; break; case OP_FPA_MAX: name = "fp.max"; break; + case OP_FPA_INTERNAL_MIN_I: name = "fp.min_i"; break; + case OP_FPA_INTERNAL_MAX_I: name = "fp.max_i"; break; + case OP_FPA_INTERNAL_MIN_UNSPECIFIED: name = "fp.min_unspecified"; break; + case OP_FPA_INTERNAL_MAX_UNSPECIFIED: name = "fp.max_unspecified"; break; default: UNREACHABLE(); break; @@ -643,7 +647,7 @@ func_decl * fpa_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, pa } func_decl * fpa_decl_plugin::mk_to_ieee_bv(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) m_manager->raise_exception("invalid number of arguments to to_ieee_bv"); if (!is_float_sort(domain[0])) @@ -656,6 +660,20 @@ func_decl * fpa_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters, return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); } +func_decl * fpa_decl_plugin::mk_internal_rm(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_rm"); + if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) || domain[0]->get_parameter(0).get_int() != 3) + m_manager->raise_exception("sort mismatch, expected argument of sort bitvector, size 3"); + if (!is_rm_sort(range)) + m_manager->raise_exception("sort mismatch, expected range of RoundingMode sort"); + + parameter ps[] = { parameter(3) }; + sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps); + return m_manager->mk_func_decl(symbol("rm"), 1, &bv_srt, range, func_decl_info(m_family_id, k, num_parameters, 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) @@ -684,37 +702,11 @@ func_decl * fpa_decl_plugin::mk_internal_bv_unwrap(decl_kind k, unsigned num_par 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)) - m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort"); + m_manager->raise_exception("sort mismatch, expected range of FloatingPoint or RoundingMode sort"); return m_manager->mk_func_decl(symbol("bv_unwrap"), 1, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters)); } -func_decl * fpa_decl_plugin::mk_internal_min_unspecified( - decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { - if (arity != 2) - m_manager->raise_exception("invalid number of arguments to fp.min_unspecified"); - if (domain[0] != domain[1] || !is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch, expected arguments of equal FloatingPoint sorts"); - if (!is_float_sort(range)) - m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort"); - - return m_manager->mk_func_decl(symbol("fp.min_unspecified"), 2, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters)); -} - -func_decl * fpa_decl_plugin::mk_internal_max_unspecified( - decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { - if (arity != 2) - m_manager->raise_exception("invalid number of arguments to fp.max_unspecified"); - if (domain[0] != domain[1] || !is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch, expected arguments of equal FloatingPoint sorts"); - if (!is_float_sort(range)) - m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort"); - - return m_manager->mk_func_decl(symbol("fp.max_unspecified"), 2, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters)); -} - func_decl * fpa_decl_plugin::mk_internal_to_ubv_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { @@ -818,14 +810,20 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return mk_to_fp_unsigned(k, num_parameters, parameters, arity, domain, range); case OP_FPA_TO_IEEE_BV: return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range); + + case OP_FPA_INTERNAL_RM: + return mk_internal_rm(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_BVWRAP: return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_BVUNWRAP: return mk_internal_bv_unwrap(k, num_parameters, parameters, arity, domain, range); + + case OP_FPA_INTERNAL_MIN_I: + case OP_FPA_INTERNAL_MAX_I: case OP_FPA_INTERNAL_MIN_UNSPECIFIED: - return mk_internal_min_unspecified(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_MAX_UNSPECIFIED: - return mk_internal_max_unspecified(k, num_parameters, parameters, arity, domain, range); + return mk_binary_decl(k, num_parameters, parameters, arity, domain, range); + case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: return mk_internal_to_ubv_unspecified(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: @@ -1031,18 +1029,6 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) { return mk_value(v); } -app * fpa_util::mk_internal_min_unspecified(expr * x, expr * y) { - SASSERT(m().get_sort(x) == m().get_sort(y)); - expr * args[] = { x, y }; - return m().mk_app(get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, 0, 0, 2, args, m().get_sort(x)); -} - -app * fpa_util::mk_internal_max_unspecified(expr * x, expr * y) { - SASSERT(m().get_sort(x) == m().get_sort(y)); - expr * args[] = { x, y }; - return m().mk_app(get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, 0, 0, 2, args, m().get_sort(x)); -} - app * fpa_util::mk_internal_to_ubv_unspecified(unsigned width) { parameter ps[] = { parameter(width) }; sort * range = m_bv_util.mk_sort(width); diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 50b388047..bf82aa487 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -34,6 +34,8 @@ enum fpa_sort_kind { FLOAT128_SORT }; +typedef enum { BV_RM_TIES_TO_EVEN, BV_RM_TIES_TO_AWAY, BV_RM_TO_POSITIVE, BV_RM_TO_NEGATIVE, BV_RM_TO_ZERO = 4 } BV_RM_VAL; + enum fpa_op_kind { OP_FPA_RM_NEAREST_TIES_TO_EVEN, OP_FPA_RM_NEAREST_TIES_TO_AWAY, @@ -85,8 +87,12 @@ enum fpa_op_kind { OP_FPA_TO_IEEE_BV, /* Internal use only */ + OP_FPA_INTERNAL_RM, // Internal conversion from (_ BitVec 3) to RoundingMode OP_FPA_INTERNAL_BVWRAP, - OP_FPA_INTERNAL_BVUNWRAP, + OP_FPA_INTERNAL_BVUNWRAP, + + OP_FPA_INTERNAL_MIN_I, + OP_FPA_INTERNAL_MAX_I, OP_FPA_INTERNAL_MIN_UNSPECIFIED, OP_FPA_INTERNAL_MAX_UNSPECIFIED, OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, @@ -125,6 +131,7 @@ class fpa_decl_plugin : public decl_plugin { sort * mk_float_sort(unsigned ebits, unsigned sbits); sort * mk_rm_sort(); + func_decl * mk_rm_const_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); func_decl * mk_float_const_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, @@ -158,14 +165,12 @@ class fpa_decl_plugin : public decl_plugin { func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); + func_decl * mk_internal_rm(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); func_decl * mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); func_decl * mk_internal_bv_unwrap(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - func_decl * mk_internal_min_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - func_decl * mk_internal_max_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); func_decl * mk_internal_to_ubv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); func_decl * mk_internal_to_sbv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, @@ -176,6 +181,7 @@ class fpa_decl_plugin : public decl_plugin { virtual void set_manager(ast_manager * m, family_id id); unsigned mk_id(mpf const & v); void recycled_id(unsigned id); + public: fpa_decl_plugin(); @@ -338,8 +344,6 @@ public: app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FPA_TO_IEEE_BV, arg1); } - app * mk_internal_min_unspecified(expr * x, expr * y); - app * mk_internal_max_unspecified(expr * x, expr * y); 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); diff --git a/src/ast/pattern/expr_pattern_match.h b/src/ast/pattern/expr_pattern_match.h index c3c0256fd..245edd877 100644 --- a/src/ast/pattern/expr_pattern_match.h +++ b/src/ast/pattern/expr_pattern_match.h @@ -37,7 +37,7 @@ class expr_pattern_match { CHECK_TERM, SET_BOUND, CHECK_BOUND, - YIELD, + YIELD }; struct instr { diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 1115663d2..fd7c60a57 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -1500,7 +1500,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r result = m_util.mk_bv_not(new_args[1]); return BR_DONE; } - __fallthrough; + Z3_fallthrough; default: if (m_bv_sort_ac) std::sort(new_args.begin(), new_args.end(), ast_to_lt()); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index d336c3a56..062703be0 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -93,10 +93,14 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(f, args[0], result); break; case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break; + 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_MAX_UNSPECIFIED: SASSERT(num_args == 2); st = BR_FAILED; break; + 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: @@ -434,19 +438,26 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_fm), v2(m_fm); if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) { - // Result could be +zero or -zero. - result = m_util.mk_internal_min_unspecified(arg1, arg2); + result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2); return BR_DONE; } - else { + else { scoped_mpf r(m_fm); m_fm.minimum(v1, v2, r); result = m_util.mk_value(r); return BR_DONE; } } + else { + expr_ref c(m()), v(m()); + c = m().mk_and(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), + m().mk_or(m().mk_and(m_util.mk_is_positive(arg1), m_util.mk_is_negative(arg2)), + m().mk_and(m_util.mk_is_negative(arg1), m_util.mk_is_positive(arg2)))); + v = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2); - return BR_FAILED; + result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_I, arg1, arg2)); + return BR_REWRITE_FULL; + } } br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { @@ -462,9 +473,8 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_fm), v2(m_fm); if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) { - // Result could be +zero or -zero. - result = m_util.mk_internal_max_unspecified(arg1, arg2); - return BR_REWRITE_FULL; + result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, arg1, arg2); + return BR_DONE; } else { scoped_mpf r(m_fm); @@ -473,8 +483,16 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { return BR_DONE; } } + else { + expr_ref c(m()), v(m()); + c = m().mk_and(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), + m().mk_or(m().mk_and(m_util.mk_is_positive(arg1), m_util.mk_is_negative(arg2)), + m().mk_and(m_util.mk_is_negative(arg1), m_util.mk_is_positive(arg2)))); + v = m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, arg1, arg2); - return BR_FAILED; + result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_I, arg1, arg2)); + return BR_REWRITE_FULL; + } } br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) { @@ -713,6 +731,27 @@ br_status fpa_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) return BR_FAILED; } +br_status fpa_rewriter::mk_rm(expr * arg, expr_ref & result) { + bv_util bu(m()); + rational bv_val; + unsigned sz = 0; + if (bu.is_numeral(arg, bv_val, sz)) { + SASSERT(bv_val.is_uint64()); + switch (bv_val.get_uint64()) { + case BV_RM_TIES_TO_AWAY: result = m_util.mk_round_nearest_ties_to_away(); break; + case BV_RM_TIES_TO_EVEN: result = m_util.mk_round_nearest_ties_to_even(); break; + case BV_RM_TO_NEGATIVE: result = m_util.mk_round_toward_negative(); break; + case BV_RM_TO_POSITIVE: result = m_util.mk_round_toward_positive(); break; + case BV_RM_TO_ZERO: + default: result = m_util.mk_round_toward_zero(); + } + + return BR_DONE; + } + + return BR_FAILED; +} + br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { unsynch_mpz_manager & mpzm = m_fm.mpz_manager(); bv_util bu(m()); diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index 41a929e4b..689ffad3c 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -77,6 +77,8 @@ public: br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); + + br_status mk_rm(expr * arg, expr_ref & result); br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result); br_status mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index add1b5b3d..30b5a7c4b 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -66,7 +66,7 @@ void context_params::set(char const * param, char const * value) { long val = strtol(value, 0, 10); m_timeout = static_cast(val); } - if (p == "rlimit") { + else if (p == "rlimit") { long val = strtol(value, 0, 10); m_rlimit = static_cast(val); } diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h index 76ed6e3e2..59cbf3a61 100755 --- a/src/interp/iz3base.h +++ b/src/interp/iz3base.h @@ -117,7 +117,7 @@ class iz3base : public iz3mgr, public scopes { /** Interpolator for clauses, to be implemented */ virtual void interpolate_clause(std::vector &lits, std::vector &itps){ - throw "no interpolator"; + throw iz3_exception("no interpolator"); } ast get_proof_check_assump(range &rng){ @@ -129,7 +129,7 @@ class iz3base : public iz3mgr, public scopes { int frame_of_assertion(const ast &ass){ stl_ext::hash_map::iterator it = frame_map.find(ass); if(it == frame_map.end()) - throw "unknown assertion"; + throw iz3_exception("unknown assertion"); return it->second; } diff --git a/src/interp/iz3exception.h b/src/interp/iz3exception.h new file mode 100644 index 000000000..134c049cf --- /dev/null +++ b/src/interp/iz3exception.h @@ -0,0 +1,28 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + iz3exception.h + +Abstract: + + Base class for exceptions raised by interpolation routines + +Author: + +Notes: + +--*/ +#ifndef _IZ3EXCEPTION_H_ +#define _IZ3EXCEPTION_H_ + +#include "z3_exception.h" +#include "error_codes.h" + +class iz3_exception: public default_exception { +public: + iz3_exception(const std::string &msg): default_exception(msg) {} +}; + +#endif diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 00bc5111a..58db2c3b5 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -218,7 +218,7 @@ public: iz3secondary *sp = iz3foci::create(this,num,(int *)(parents.empty()?0:&parents[0])); int res = sp->interpolate(cnsts, interps); if(res != 0) - throw "secondary failed"; + throw iz3_exception("secondary failed"); } void proof_to_interpolant(z3pf proof, diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h index 368c2c25e..601c8c3f5 100644 --- a/src/interp/iz3interp.h +++ b/src/interp/iz3interp.h @@ -21,6 +21,7 @@ #define IZ3_INTERP_H #include "iz3hash.h" +#include "iz3exception.h" #include "solver.h" class iz3base; @@ -35,12 +36,14 @@ public: }; /** This object is thrown if a tree interpolation problem is mal-formed */ -struct iz3_bad_tree { +struct iz3_bad_tree: public iz3_exception { + iz3_bad_tree(): iz3_exception("iz3_bad_tree") {} }; /** This object is thrown when iz3 fails due to an incompleteness in the secondary solver. */ -struct iz3_incompleteness { +struct iz3_incompleteness: public iz3_exception { + iz3_incompleteness(): iz3_exception("iz3_incompleteness") {} }; // This is thrown if there is some bug in the diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index 2f7fe1be2..2e55d7040 100755 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -515,7 +515,7 @@ bool iz3mgr::is_farkas_coefficient_negative(const ast &proof, int n){ symb s = sym(proof); bool ok = s->get_parameter(n+2).is_rational(r); if(!ok) - throw "Bad Farkas coefficient"; + throw iz3_exception("Bad Farkas coefficient"); return r.is_neg(); } @@ -532,7 +532,7 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector& rats){ rational r; bool ok = s->get_parameter(i).is_rational(r); if(!ok) - throw "Bad Farkas coefficient"; + throw iz3_exception("Bad Farkas coefficient"); #if 0 { ast con = conc(prem(proof,i-2)); @@ -591,7 +591,7 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector& r rational r; bool ok = s->get_parameter(i).is_rational(r); if(!ok) - throw "Bad Farkas coefficient"; + throw iz3_exception("Bad Farkas coefficient"); { ast con = arg(conc(proof),i-1); ast temp = make_real(r); // for debugging @@ -607,7 +607,7 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector& r if(rats[1].is_neg()){ // work around bug -- if all coeffs negative, negate them for(unsigned i = 1; i < rats.size(); i++){ if(!rats[i].is_neg()) - throw "Bad Farkas coefficients"; + throw iz3_exception("Bad Farkas coefficients"); rats[i] = -rats[i]; } } @@ -661,7 +661,7 @@ void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vectorget_parameter(i).is_rational(r); if(!ok) - throw "Bad Farkas coefficient"; + throw iz3_exception("Bad Farkas coefficient"); { ast con = conc(prem(proof,i-2)); ast temp = make_real(r); // for debugging @@ -677,7 +677,7 @@ void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector #include "iz3hash.h" +#include "iz3exception.h" #include"well_sorted.h" #include"arith_decl_plugin.h" diff --git a/src/interp/iz3pp.h b/src/interp/iz3pp.h index bbb10a785..c66b4a4fa 100644 --- a/src/interp/iz3pp.h +++ b/src/interp/iz3pp.h @@ -25,7 +25,8 @@ /** Exception thrown in case of mal-formed tree interpoloation specification */ -struct iz3pp_bad_tree { +struct iz3pp_bad_tree: public iz3_exception { + iz3pp_bad_tree(): iz3_exception("iz3pp_bad_tree") {} }; void iz3pp(ast_manager &m, diff --git a/src/interp/iz3proof.h b/src/interp/iz3proof.h index be85702a2..213afce5e 100755 --- a/src/interp/iz3proof.h +++ b/src/interp/iz3proof.h @@ -57,7 +57,9 @@ class iz3proof { typedef prover::ast ast; /** Object thrown in case of a proof error. */ - struct proof_error {}; + struct proof_error: public iz3_exception { + proof_error(): iz3_exception("proof_error") {} + }; /* Null proof node */ static const node null = -1; diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 046b0b7f1..c06aed36d 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -250,7 +250,7 @@ class iz3proof_itp_impl : public iz3proof_itp { #if 0 rational r; if(!is_integer(coeff,r)) - throw "ack!"; + throw iz3_exception("ack!"); ast n = make_int(r.numerator()); ast res = make(Times,n,t); if(!r.is_int()) { @@ -433,7 +433,7 @@ class iz3proof_itp_impl : public iz3proof_itp { if(op(foo) == Uninterpreted && sym(foo) == contra){ ast neg_lit = arg(foo,1); if(!is_false(neg_lit) && neg_lits.find(neg_lit) == neg_lits.end()) - throw "lost a literal"; + throw iz3_exception("lost a literal"); return; } else { @@ -506,7 +506,9 @@ class iz3proof_itp_impl : public iz3proof_itp { /* This is where the real work happens. Here, we simplify the proof obtained by cut elimination, obtaining an interpolant. */ - struct cannot_simplify {}; + struct cannot_simplify: public iz3_exception { + cannot_simplify(): iz3_exception("cannot_simplify") {} + }; hash_map simplify_memo; ast simplify(const ast &t){ @@ -582,7 +584,7 @@ class iz3proof_itp_impl : public iz3proof_itp { // if(g == symm) return simplify_rotate_symm(pl,args[0],pf); } if(op(pf) == Leq) - throw "foo!"; + throw iz3_exception("foo!"); throw cannot_simplify(); } @@ -831,7 +833,7 @@ class iz3proof_itp_impl : public iz3proof_itp { return my_implies(cond,ineqs); if(op(ineqs) != And) return my_and(Bconds,my_implies(cond,ineqs)); - throw "help!"; + throw iz3_exception("help!"); } ast add_mixed_eq2ineq(const ast &lhs, const ast &rhs, const ast &equa, const ast &itp){ @@ -871,7 +873,7 @@ class iz3proof_itp_impl : public iz3proof_itp { } } } - throw "help!"; + throw iz3_exception("help!"); } void reverse_modpon(std::vector &args){ @@ -980,7 +982,9 @@ class iz3proof_itp_impl : public iz3proof_itp { return chain; } - struct subterm_normals_failed {}; + struct subterm_normals_failed: public iz3_exception { + subterm_normals_failed(): iz3_exception("subterm_normals_failed") {} + }; void get_subterm_normals(const ast &ineq1, const ast &ineq2, const ast &chain, ast &normals, const ast &pos, hash_set &memo, ast &Aproves, ast &Bproves){ @@ -989,7 +993,7 @@ class iz3proof_itp_impl : public iz3proof_itp { if(o1 == Not || o1 == Leq || o1 == Lt || o1 == Geq || o1 == Gt || o1 == Plus || o1 == Times){ int n = num_args(ineq1); if(o2 != o1 || num_args(ineq2) != n) - throw "bad inequality rewriting"; + throw iz3_exception("bad inequality rewriting"); for(int i = 0; i < n; i++){ ast new_pos = add_pos_to_end(pos,i); get_subterm_normals(arg(ineq1,i), arg(ineq2,i), chain, normals, new_pos, memo, Aproves, Bproves); @@ -1000,7 +1004,7 @@ class iz3proof_itp_impl : public iz3proof_itp { memo.insert(ineq2); ast sub_chain = extract_rewrites(chain,pos); if(is_true(sub_chain)) - throw "bad inequality rewriting"; + throw iz3_exception("bad inequality rewriting"); ast new_normal = make_normal_step(ineq2,ineq1,reverse_chain(sub_chain)); normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves); } @@ -1149,7 +1153,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast interp = contra_chain(Q2,chain); return my_and(Aproves,my_implies(Bproves,interp)); } - throw "bad exmid"; + throw iz3_exception("bad exmid"); } ast simplify_cong(const std::vector &args){ @@ -1163,7 +1167,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast interp = contra_chain(Q2,chain); return my_and(Aproves,my_implies(Bproves,interp)); } - throw "bad cong"; + throw iz3_exception("bad cong"); } bool is_equivrel(const ast &p){ @@ -1171,7 +1175,9 @@ class iz3proof_itp_impl : public iz3proof_itp { return o == Equal || o == Iff; } - struct rewrites_failed{}; + struct rewrites_failed: public iz3_exception { + rewrites_failed(): iz3_exception("rewrites_failed") {} + }; /* Suppose p in Lang(B) and A |- p -> q and B |- q -> r. Return a z in Lang(B) such that B |- p -> z and A |- z -> q. Collect any side conditions in "rules". */ @@ -1414,7 +1420,7 @@ class iz3proof_itp_impl : public iz3proof_itp { rational r; if(is_numeral(arg(pos,0),r)) return r.get_unsigned(); - throw "bad position!"; + throw iz3_exception("bad position!"); } /* substitute y into position pos in x */ @@ -1429,7 +1435,7 @@ class iz3proof_itp_impl : public iz3proof_itp { args[i] = i == p ? subst_in_pos(arg(x,i),arg(pos,1),y) : arg(x,i); return clone(x,args); } - throw "bad term position!"; + throw iz3_exception("bad term position!"); } ast diff_chain(LitType t, const ast &pos, const ast &x, const ast &y, const ast &prefix){ @@ -1448,10 +1454,10 @@ class iz3proof_itp_impl : public iz3proof_itp { ast make_rewrite(LitType t, const ast &pos, const ast &cond, const ast &equality){ #if 0 if(pos == top_pos && op(equality) == Iff && !is_true(arg(equality,0))) - throw "bad rewrite"; + throw iz3_exception("bad rewrite"); #endif if(!is_equivrel(equality)) - throw "bad rewrite"; + throw iz3_exception("bad rewrite"); return make(t == LitA ? rewrite_A : rewrite_B, pos, cond, equality); } @@ -1662,25 +1668,25 @@ class iz3proof_itp_impl : public iz3proof_itp { if(is_true(rest)){ ast old = rewrite_rhs(last); if(!(op(old) == Not)) - throw "bad negative equality chain"; + throw iz3_exception("bad negative equality chain"); ast equ = arg(old,0); if(!is_equivrel(equ)) - throw "bad negative equality chain"; + throw iz3_exception("bad negative equality chain"); last = rewrite_update_rhs(last,top_pos,make(Not,make(op(equ),arg(equ,1),arg(equ,0))),make(True)); return chain_cons(rest,last); } ast pos = rewrite_pos(last); if(pos == top_pos) - throw "bad negative equality chain"; + throw iz3_exception("bad negative equality chain"); int idx = pos_arg(pos); if(idx != 0) - throw "bad negative equality chain"; + throw iz3_exception("bad negative equality chain"); pos = arg(pos,1); if(pos == top_pos){ ast lhs = rewrite_lhs(last); ast rhs = rewrite_rhs(last); if(op(lhs) != Equal || op(rhs) != Equal) - throw "bad negative equality chain"; + throw iz3_exception("bad negative equality chain"); last = make_rewrite(rewrite_side(last),rewrite_pos(last),rewrite_cond(last), make(Iff,make(Equal,arg(lhs,1),arg(lhs,0)),make(Equal,arg(rhs,1),arg(rhs,0)))); } @@ -1691,7 +1697,7 @@ class iz3proof_itp_impl : public iz3proof_itp { else if(idx == 1) idx = 0; else - throw "bad negative equality chain"; + throw iz3_exception("bad negative equality chain"); pos = pos_add(0,pos_add(idx,arg(pos,1))); last = make_rewrite(rewrite_side(last),pos,rewrite_cond(last),rewrite_equ(last)); } @@ -1708,7 +1714,7 @@ class iz3proof_itp_impl : public iz3proof_itp { return chain; } if(is_true(rest)) - throw "bad rewrite chain"; + throw iz3_exception("bad rewrite chain"); ast head = get_head_chain(rest,tail,is_not); tail = chain_cons(tail,last); return head; @@ -1766,7 +1772,9 @@ class iz3proof_itp_impl : public iz3proof_itp { } - struct cannot_split {}; + struct cannot_split: public iz3_exception { + cannot_split(): iz3_exception("cannot_split") {} + }; /** Split a chain of rewrites two chains, operating on positions 0 and 1. Fail if any rewrite in the chain operates on top position. */ @@ -1808,7 +1816,7 @@ class iz3proof_itp_impl : public iz3proof_itp { } case 1: if(rewrite_lhs(last) != rewrite_rhs(last)) - throw "bad rewrite chain"; + throw iz3_exception("bad rewrite chain"); break; default:; } @@ -1853,7 +1861,9 @@ class iz3proof_itp_impl : public iz3proof_itp { return rewrites_from_to(rest,lhs,mid); } - struct bad_ineq_inference {}; + struct bad_ineq_inference: public iz3_exception { + bad_ineq_inference(): iz3_exception("bad_ineq_inference") {} + }; ast chain_ineqs(opr comp_op, LitType t, const ast &chain, const ast &lhs, const ast &rhs){ if(is_true(chain)){ @@ -1907,7 +1917,7 @@ class iz3proof_itp_impl : public iz3proof_itp { rhs = arg(ineq,1); return; } - throw "bad ineq"; + throw iz3_exception("bad ineq"); } ast chain_pos_add(int arg, const ast &chain){ @@ -1974,7 +1984,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast make_normal(const ast &ineq, const ast &nrml){ if(!is_ineq(ineq)) - throw "what?"; + throw iz3_exception("what?"); return make(normal,ineq,nrml); } @@ -1985,7 +1995,7 @@ class iz3proof_itp_impl : public iz3proof_itp { return make_normal_step(lhs,rhs,proof); if(rhst == LitMixed && (lhst != LitMixed || ast_id(rhs) < ast_id(lhs))) return make_normal_step(rhs,lhs,reverse_chain(proof)); - throw "help!"; + throw iz3_exception("help!"); } ast chain_side_proves(LitType side, const ast &chain){ diff --git a/src/interp/iz3proof_itp.h b/src/interp/iz3proof_itp.h index e1e0de5cc..bd9eca441 100644 --- a/src/interp/iz3proof_itp.h +++ b/src/interp/iz3proof_itp.h @@ -50,7 +50,9 @@ class iz3proof_itp : public iz3mgr { typedef ast node; /** Object thrown in case of a proof error. */ - struct proof_error {}; + struct proof_error: public iz3_exception { + proof_error(): iz3_exception("proof_error") {} + }; /** Make a resolution node with given pivot literal and premises. diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 51084f809..1f7283b32 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -132,7 +132,7 @@ public: // if(range_is_empty(r)) range r = ast_scope(quanted); if(range_is_empty(r)) - throw "can't skolemize"; + throw iz3_exception("can't skolemize"); if(frame == INT_MAX || !in_range(frame,r)) frame = range_max(r); // this is desperation -- may fail if(frame >= frames) frame = frames - 1; @@ -1092,10 +1092,10 @@ public: rational xcoeff = get_first_coefficient(arg(x,0),xvar); rational ycoeff = get_first_coefficient(arg(y,0),yvar); if(xcoeff == rational(0) || ycoeff == rational(0) || xvar != yvar) - throw "bad assign-bounds lemma"; + throw iz3_exception("bad assign-bounds lemma"); rational ratio = xcoeff/ycoeff; if(denominator(ratio) != rational(1)) - throw "bad assign-bounds lemma"; + throw iz3_exception("bad assign-bounds lemma"); return make_int(ratio); // better be integer! } @@ -1104,7 +1104,7 @@ public: get_assign_bounds_coeffs(proof,farkas_coeffs); int nargs = num_args(con); if(nargs != (int)(farkas_coeffs.size())) - throw "bad assign-bounds theory lemma"; + throw iz3_exception("bad assign-bounds theory lemma"); #if 0 if(farkas_coeffs[0] != make_int(rational(1))) farkas_coeffs[0] = make_int(rational(1)); @@ -1145,7 +1145,7 @@ public: get_assign_bounds_rule_coeffs(proof,farkas_coeffs); int nargs = num_prems(proof)+1; if(nargs != (int)(farkas_coeffs.size())) - throw "bad assign-bounds theory lemma"; + throw iz3_exception("bad assign-bounds theory lemma"); #if 0 if(farkas_coeffs[0] != make_int(rational(1))) farkas_coeffs[0] = make_int(rational(1)); @@ -1447,7 +1447,7 @@ public: std::vector vals = cvec; if(!is_sat(cnstrs,new_proof,vals)) - throw "Proof error!"; + throw iz3_exception("Proof error!"); std::vector rat_farkas_coeffs; for(unsigned i = 0; i < cvec.size(); i++){ ast bar = vals[i]; @@ -1455,7 +1455,7 @@ public: if(is_numeral(bar,r)) rat_farkas_coeffs.push_back(r); else - throw "Proof error!"; + throw iz3_exception("Proof error!"); } rational the_lcd = lcd(rat_farkas_coeffs); std::vector farkas_coeffs; @@ -1503,7 +1503,7 @@ public: ast new_proof; std::vector dummy; if(is_sat(npcons,new_proof,dummy)) - throw "Proof error!"; + throw iz3_exception("Proof error!"); pfrule dk = pr(new_proof); int nnp = num_prems(new_proof); std::vector my_prems; @@ -1564,7 +1564,7 @@ public: ast new_proof; std::vector dummy; if(is_sat(npcons,new_proof,dummy)) - throw "Proof error!"; + throw iz3_exception("Proof error!"); pfrule dk = pr(new_proof); int nnp = num_prems(new_proof); std::vector my_prems; diff --git a/src/interp/iz3translate.h b/src/interp/iz3translate.h index 2fcf406db..86b0b3d2d 100755 --- a/src/interp/iz3translate.h +++ b/src/interp/iz3translate.h @@ -35,7 +35,8 @@ class iz3translation : public iz3base { virtual ~iz3translation(){} /** This is thrown when the proof cannot be translated. */ - struct unsupported { + struct unsupported: public iz3_exception { + unsupported(): iz3_exception("unsupported") {} }; static iz3translation *create(iz3mgr &mgr, diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index ec3af1ca3..f20f16a08 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -595,7 +595,9 @@ public: } - struct invalid_lemma {}; + struct invalid_lemma: public iz3_exception { + invalid_lemma(): iz3_exception("invalid_lemma") {} + }; @@ -846,7 +848,9 @@ public: return 1; } - struct non_lit_local_ante {}; + struct non_lit_local_ante: public iz3_exception { + non_lit_local_ante(): iz3_exception("non_lit_local_ante") {} + }; bool local_antes_simple; diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index bd5f53922..0caefd3fe 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -593,7 +593,7 @@ void asserted_formulas::propagate_values() { bool found = false; // Separate the formulas in two sets: C and R // C is a set which contains formulas of the form - // { x = n }, where x is a variable and n a numberal. + // { x = n }, where x is a variable and n a numeral. // R contains the rest. // // - new_exprs1 is the set C @@ -613,15 +613,18 @@ void asserted_formulas::propagate_values() { expr * lhs = to_app(n)->get_arg(0); expr * rhs = to_app(n)->get_arg(1); if (m_manager.is_value(lhs) || m_manager.is_value(rhs)) { - if (m_manager.is_value(lhs)) + if (m_manager.is_value(lhs)) { std::swap(lhs, rhs); + n = m_manager.mk_eq(lhs, rhs); + pr = m_manager.mk_symmetry(pr); + } if (!m_manager.is_value(lhs) && !m_simplifier.is_cached(lhs)) { if (i >= m_asserted_qhead) { new_exprs1.push_back(n); if (m_manager.proofs_enabled()) new_prs1.push_back(pr); } - TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n";); + TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\nproof: " << mk_pp(pr, m_manager) << "\n";); m_simplifier.cache_result(lhs, rhs, pr); found = true; continue; diff --git a/src/smt/params/dyn_ack_params.cpp b/src/smt/params/dyn_ack_params.cpp index c559e2b9b..15f48bad1 100644 --- a/src/smt/params/dyn_ack_params.cpp +++ b/src/smt/params/dyn_ack_params.cpp @@ -27,4 +27,4 @@ void dyn_ack_params::updt_params(params_ref const & _p) { m_dack_threshold = p.dack_threshold(); m_dack_gc = p.dack_gc(); m_dack_gc_inv_decay = p.dack_gc_inv_decay(); -} \ No newline at end of file +} diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 2c1ac13c5..8127b7eef 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -66,7 +66,7 @@ enum case_split_strategy { CS_ACTIVITY_WITH_CACHE, // case split based on activity and cache the activity CS_RELEVANCY, // case split based on relevancy CS_RELEVANCY_ACTIVITY, // case split based on relevancy and activity - CS_RELEVANCY_GOAL, // based on relevancy and the current goal + CS_RELEVANCY_GOAL // based on relevancy and the current goal }; struct smt_params : public preprocessor_params, diff --git a/src/smt/smt_almost_cg_table.cpp b/src/smt/smt_almost_cg_table.cpp index 93f136aad..66eb8c533 100644 --- a/src/smt/smt_almost_cg_table.cpp +++ b/src/smt/smt_almost_cg_table.cpp @@ -67,7 +67,7 @@ namespace smt { switch (num_args) { case 2: b += arg_hash(n, 1); - __fallthrough; + Z3_fallthrough; case 1: c += arg_hash(n, 0); } diff --git a/src/smt/smt_cg_table.cpp b/src/smt/smt_cg_table.cpp index ed36384c1..83d137ff0 100644 --- a/src/smt/smt_cg_table.cpp +++ b/src/smt/smt_cg_table.cpp @@ -127,7 +127,7 @@ namespace smt { switch (i) { case 2: b += n->get_arg(1)->get_root()->hash(); - __fallthrough; + Z3_fallthrough; case 1: c += n->get_arg(0)->get_root()->hash(); } diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index 679fd473f..68cd5703c 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -28,7 +28,7 @@ namespace smt { enum config_mode { CFG_BASIC, // install theories based on user options CFG_LOGIC, // install theories and configure Z3 based on the value of the parameter set-logic. - CFG_AUTO, // install theories based on static features of the input formula + CFG_AUTO // install theories based on static features of the input formula }; class context; diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 96133b88e..8713c4fdb 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1535,6 +1535,7 @@ namespace smt { while (best_efforts < max_efforts && !ctx.get_cancel_flag()) { theory_var x_j = null_theory_var; theory_var x_i = null_theory_var; + bool has_bound = false; max_gain.reset(); min_gain.reset(); ++round; @@ -1543,12 +1544,15 @@ namespace smt { typename vector::const_iterator it = r.begin_entries(); typename vector::const_iterator end = r.end_entries(); for (; it != end; ++it) { - if (it->is_dead()) continue; + if (it->is_dead()) continue; theory_var curr_x_j = it->m_var; theory_var curr_x_i = null_theory_var; SASSERT(is_non_base(curr_x_j)); curr_coeff = it->m_coeff; - bool curr_inc = curr_coeff.is_pos() ? max : !max; + bool curr_inc = curr_coeff.is_pos() ? max : !max; + if ((curr_inc && upper(curr_x_j)) || (!curr_inc && lower(curr_x_j))) { + has_bound = true; + } if ((curr_inc && at_upper(curr_x_j)) || (!curr_inc && at_lower(curr_x_j))) { // variable cannot be used for max/min. continue; @@ -1560,8 +1564,9 @@ namespace smt { SASSERT(!picked_var || safe_gain(curr_min_gain, curr_max_gain)); - if (!picked_var) { // && (r.size() > 1 || !safe_gain(curr_min_gain, curr_max_gain)) + if (!safe_gain(curr_min_gain, curr_max_gain)) { TRACE("opt", tout << "no variable picked\n";); + has_bound = true; best_efforts++; } else if (curr_x_i == null_theory_var) { @@ -1598,10 +1603,10 @@ namespace smt { TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << max_gain << "\n"; tout << "best efforts: " << best_efforts << " has shared: " << has_shared << "\n";); - if (x_j == null_theory_var && x_i == null_theory_var) { + if (!has_bound && x_i == null_theory_var && x_j == null_theory_var) { has_shared = false; best_efforts = 0; - result = UNBOUNDED; + result = UNBOUNDED; break; } diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index cb86e6679..ed96d050e 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -399,7 +399,6 @@ namespace smt { }; struct sidl_ext { - // TODO: It doesn't need to be a rational, but a bignum integer. static const bool m_int_theory = true; typedef s_integer numeral; typedef s_integer fin_numeral; @@ -415,13 +414,11 @@ namespace smt { rdl_ext() : m_epsilon(rational(), true) {} }; - struct srdl_ext { - static const bool m_int_theory = false; - typedef inf_s_integer numeral; - typedef s_integer fin_numeral; - numeral m_epsilon; - srdl_ext() : m_epsilon(s_integer(0),true) {} - }; + // + // there is no s_rational class, so + // instead we use multi-precision rationals. + // + struct srdl_ext : public rdl_ext {}; typedef theory_diff_logic theory_idl; typedef theory_diff_logic theory_fidl; diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 0fadc62ca..701efb2ba 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -74,7 +74,9 @@ namespace smt { } else { SASSERT(is_rm(f->get_range())); - result = m_th.wrap(m.mk_const(f)); + expr_ref bv(m); + bv = m_th.wrap(m.mk_const(f)); + mk_rm(bv, result); m_rm_const2bv.insert(f, result); m.inc_ref(f); m.inc_ref(result); @@ -83,7 +85,7 @@ namespace smt { void theory_fpa::fpa2bv_converter_wrapped::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { // TODO: This introduces temporary variables/func_decls that should be filtered in the end. - return fpa2bv_converter::mk_uninterpreted_function(f, num, args, result); + fpa2bv_converter::mk_uninterpreted_function(f, num, args, result); } expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) { @@ -106,7 +108,6 @@ namespace smt { expr_ref sc(m); m_th.m_converter.mk_is_zero(res, sc); m_extra_assertions.push_back(sc); - //m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, f->get_range()), a)); return res; } @@ -130,7 +131,6 @@ namespace smt { expr_ref sc(m); m_th.m_converter.mk_is_zero(res, sc); m_extra_assertions.push_back(sc); - //m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, f->get_range()), a)); return res; } @@ -314,6 +314,7 @@ namespace smt { expr_ref theory_fpa::convert_atom(expr * e) { ast_manager & m = get_manager(); + TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, get_manager()) << "\n";); expr_ref res(m); proof_ref pr(m); m_rw(e, res); @@ -331,15 +332,31 @@ namespace smt { proof_ref pr(m); m_rw(e, e_conv); - if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) { - m_th_rw(e_conv, res); + if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) { + if (!m_fpa_util.is_float(e_conv)) + m_th_rw(e_conv, res); + else { + expr_ref bv(m); + bv = wrap(e_conv); + unsigned bv_sz = m_bv_util.get_bv_size(bv); + unsigned ebits = m_fpa_util.get_ebits(m.get_sort(e_conv)); + unsigned sbits = m_fpa_util.get_sbits(m.get_sort(e_conv)); + SASSERT(bv_sz == ebits + sbits); + m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv), + m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv), + m_bv_util.mk_extract(sbits - 2, 0, bv), + res); + } } else if (m_fpa_util.is_rm(e)) { - SASSERT(is_sort_of(m.get_sort(e_conv), m_bv_util.get_family_id(), BV_SORT)); - SASSERT(m_bv_util.get_bv_size(e_conv) == 3); - m_th_rw(e_conv, res); + SASSERT(is_app_of(e_conv, get_family_id(), OP_FPA_INTERNAL_RM)); + expr_ref bv_rm(m); + bv_rm = to_app(e_conv)->get_arg(0); + m_th_rw(bv_rm); + m_converter.mk_rm(bv_rm, res); } - else if (m_fpa_util.is_float(e)) { + else if (m_fpa_util.is_float(e)) { + SASSERT(is_app_of(e_conv, get_family_id(), OP_FPA_FP)); expr_ref sgn(m), sig(m), exp(m); m_converter.split_fp(e_conv, sgn, exp, sig); m_th_rw(sgn); @@ -426,7 +443,7 @@ namespace smt { sort * srt = m.get_sort(e); expr_ref res(m); if (m_fpa_util.is_rm(srt)) { - res = to_app(e)->get_arg(0); + m_converter.mk_rm(to_app(e)->get_arg(0), res); } else { SASSERT(m_fpa_util.is_float(srt)); @@ -454,7 +471,6 @@ namespace smt { TRACE("t_fpa_detail", tout << "cached:" << std::endl; tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl << mk_ismt2_pp(res, m) << std::endl;); - return res; } else { if (m_fpa_util.is_unwrap(e)) @@ -464,7 +480,7 @@ namespace smt { else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e)) res = convert_term(e); else if (m_arith_util.is_real(e) || m_bv_util.is_bv(e)) - res = convert_conversion_term(e); + res = convert_conversion_term(e); else UNREACHABLE(); @@ -476,7 +492,7 @@ namespace smt { m.inc_ref(res); m_trail_stack.push(fpa2bv_conversion_trail_elem(m, m_conversions, e)); } - + return res; } @@ -643,19 +659,17 @@ namespace smt { expr_ref xc(m), yc(m); xc = convert(xe); yc = convert(ye); - TRACE("t_fpa_detail", tout << "xc = " << mk_ismt2_pp(xc, m) << std::endl << "yc = " << mk_ismt2_pp(yc, m) << std::endl;); expr_ref c(m); - - if (fu.is_float(xe) && fu.is_float(ye)) + + if ((fu.is_float(xe) && fu.is_float(ye)) || + (fu.is_rm(xe) && fu.is_rm(ye))) m_converter.mk_eq(xc, yc, c); - else if (fu.is_rm(xe) && fu.is_rm(ye)) + else c = m.mk_eq(xc, yc); - else - UNREACHABLE(); m_th_rw(c); assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c)); @@ -671,7 +685,7 @@ namespace smt { TRACE("t_fpa", tout << "new diseq: " << x << " != " << y << std::endl;); TRACE("t_fpa_detail", tout << mk_ismt2_pp(get_enode(x)->get_owner(), m) << " != " << - mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;); + mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;); fpa_util & fu = m_fpa_util; @@ -688,14 +702,13 @@ namespace smt { expr_ref c(m); - if (fu.is_float(xe) && fu.is_float(ye)) { + if ((fu.is_float(xe) && fu.is_float(ye))|| + (fu.is_rm(xe) && fu.is_rm(ye))) { m_converter.mk_eq(xc, yc, c); c = m.mk_not(c); } - else if (fu.is_rm(xe) && fu.is_rm(ye)) - c = m.mk_not(m.mk_eq(xc, yc)); else - UNREACHABLE(); + c = m.mk_not(m.mk_eq(xc, yc)); m_th_rw(c); assert_cnstr(m.mk_iff(m.mk_not(m.mk_eq(xe, ye)), c)); diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index f9d2eeed4..78c79dd11 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -45,11 +45,6 @@ void fpa2bv_model_converter::display(std::ostream & out) { unsigned indent = n.size() + 4; out << mk_ismt2_pp(it->m_value, m, indent) << ")"; } - for (obj_hashtable::iterator it = m_decls_to_hide.begin(); - it != m_decls_to_hide.end(); - it++) { - out << "\n to hide: " << mk_ismt2_pp(*it, m); - } out << ")" << std::endl; } @@ -130,16 +125,16 @@ expr_ref fpa2bv_model_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, res = fu.mk_value(fp_val); - TRACE("fpa2bv_mc", tout << "[" << mk_ismt2_pp(sgn, m) << - " " << mk_ismt2_pp(exp, m) << - " " << mk_ismt2_pp(sig, m) << "] == " << + TRACE("fpa2bv_mc", tout << "[" << mk_ismt2_pp(sgn, m) << + " " << mk_ismt2_pp(exp, m) << + " " << mk_ismt2_pp(sig, m) << "] == " << mk_ismt2_pp(res, m) << std::endl;); fu.fm().del(fp_val); return res; } -expr_ref fpa2bv_model_converter::convert_bv2fp(model * bv_mdl, sort * s, expr * bv) const { +expr_ref fpa2bv_model_converter::convert_bv2fp(model * bv_mdl, sort * s, expr * bv) const { fpa_util fu(m); bv_util bu(m); @@ -165,10 +160,11 @@ expr_ref fpa2bv_model_converter::convert_bv2fp(model * bv_mdl, sort * s, expr * expr_ref fpa2bv_model_converter::convert_bv2rm(expr * eval_v) const { fpa_util fu(m); bv_util bu(m); - expr_ref res(m); + expr_ref res(m); rational bv_val(0); unsigned sz = 0; + if (bu.is_numeral(eval_v, bv_val, sz)) { SASSERT(bv_val.is_uint64()); switch (bv_val.get_uint64()) { @@ -189,7 +185,7 @@ expr_ref fpa2bv_model_converter::convert_bv2rm(model * bv_mdl, func_decl * var, bv_util bu(m); expr_ref res(m); - expr_ref eval_v(m); + expr_ref eval_v(m); if (val && bv_mdl->eval(val, eval_v, true)) res = convert_bv2rm(eval_v); @@ -205,14 +201,26 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { for (unsigned i = 0; i < bv_mdl->get_num_constants(); i++) tout << bv_mdl->get_constant(i)->get_name() << " --> " << mk_ismt2_pp(bv_mdl->get_const_interp(bv_mdl->get_constant(i)), m) << std::endl; - ); + for (unsigned i = 0; i < bv_mdl->get_num_functions(); i++) { + func_decl * f = bv_mdl->get_function(i); + tout << f->get_name() << "(...) := " << std::endl; + func_interp * fi = bv_mdl->get_func_interp(f); + for (unsigned j = 0; j < fi->num_entries(); j++) { + func_entry const * fe = fi->get_entry(j); + for (unsigned k = 0; k < f->get_arity(); k++) { + tout << mk_ismt2_pp(fe->get_arg(k), m) << " "; + } + tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl; + } + tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl; + }); obj_hashtable seen; for (obj_hashtable::iterator it = m_decls_to_hide.begin(); it != m_decls_to_hide.end(); it++) - seen.insert(*it); + seen.insert(*it); for (obj_map::iterator it = m_const2bv.begin(); it != m_const2bv.end(); @@ -223,7 +231,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { SASSERT(fu.is_float(var->get_range())); SASSERT(var->get_range()->get_num_parameters() == 2); - expr_ref sgn(m), sig(m), exp(m); + expr_ref sgn(m), sig(m), exp(m); bv_mdl->eval(val->get_arg(0), sgn, true); bv_mdl->eval(val->get_arg(1), exp, true); bv_mdl->eval(val->get_arg(2), sig, true); @@ -237,7 +245,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { seen.insert(to_app(val->get_arg(0))->get_decl()); seen.insert(to_app(val->get_arg(1))->get_decl()); seen.insert(to_app(val->get_arg(2))->get_decl()); -#else +#else SASSERT(a->get_arg(0)->get_kind() == OP_EXTRACT); SASSERT(to_app(a->get_arg(0))->get_arg(0)->get_kind() == OP_EXTRACT); seen.insert(to_app(to_app(val->get_arg(0))->get_arg(0))->get_decl()); @@ -260,8 +268,10 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { func_decl * var = it->m_key; SASSERT(fu.is_rm(var->get_range())); expr * val = it->m_value; + SASSERT(is_app_of(val, fu.get_family_id(), OP_FPA_INTERNAL_RM)); + expr * bvval = to_app(val)->get_arg(0); expr_ref fv(m); - fv = convert_bv2rm(bv_mdl, var, val); + fv = convert_bv2rm(bv_mdl, var, bvval); TRACE("fpa2bv_mc", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << std::endl;); float_mdl->register_decl(var, fv); seen.insert(to_app(val)->get_decl()); @@ -298,7 +308,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { else new_args.push_back(aj); } - + expr_ref ret(m); ret = bv_fe->get_result(); if (fu.is_float(rng)) @@ -306,7 +316,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { else if (fu.is_rm(rng)) ret = convert_bv2rm(ret); - flt_fi->insert_new_entry(new_args.c_ptr(), ret); + flt_fi->insert_new_entry(new_args.c_ptr(), ret); } expr_ref els(m); @@ -318,7 +328,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { flt_fi->set_else(els); - float_mdl->register_decl(f, flt_fi); + float_mdl->register_decl(f, flt_fi); } // Keep all the non-float constants. diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 4cce4bfd1..a864f753a 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -35,7 +35,6 @@ public: obj_map const & uf2bvuf, obj_hashtable const & decls_to_hide) : m(m) { - // Just create a copy? for (obj_map::iterator it = const2bv.begin(); it != const2bv.end(); it++) @@ -62,7 +61,8 @@ public: } for (obj_hashtable::iterator it = decls_to_hide.begin(); it != decls_to_hide.end(); - it++) { + it++) + { m_decls_to_hide.insert(*it); m.inc_ref(*it); } @@ -106,6 +106,6 @@ model_converter * mk_fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv, obj_map const & rm_const2bv, obj_map const & uf2bvuf, - obj_hashtable const & m_decls_to_hide); + obj_hashtable const & decls_to_hide); #endif \ No newline at end of file diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 158bb935e..472f6b30c 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -56,8 +56,6 @@ class fpa2bv_tactic : public tactic { proof_converter_ref & pc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); - fail_if_proof_generation("fpa2bv", g); - fail_if_unsat_core_generation("fpa2bv", g); m_proofs_enabled = g->proofs_enabled(); m_produce_models = g->models_enabled(); m_produce_unsat_cores = g->unsat_core_enabled(); @@ -151,7 +149,12 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, pc, core); + try { + (*m_imp)(in, result, mc, pc, core); + } + catch (rewriter_exception & ex) { + throw tactic_exception(ex.msg()); + } } virtual void cleanup() { diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index 485e837ee..9c94d6cb2 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -71,21 +71,19 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { tactic * st = and_then(mk_simplify_tactic(m, simp_p), mk_propagate_values_tactic(m, p), - cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()), - mk_smt_tactic(), - and_then( - mk_fpa2bv_tactic(m, p), - mk_propagate_values_tactic(m, p), - using_params(mk_simplify_tactic(m, p), simp_p), - mk_bit_blaster_tactic(m, p), - using_params(mk_simplify_tactic(m, p), simp_p), - cond(mk_is_propositional_probe(), - mk_sat_tactic(m, p), - cond(mk_has_fp_to_real_probe(), - mk_qfnra_tactic(m, p), - mk_smt_tactic(p)) - ), - mk_fail_if_undecided_tactic()))); + mk_fpa2bv_tactic(m, p), + mk_propagate_values_tactic(m, p), + using_params(mk_simplify_tactic(m, p), simp_p), + mk_bit_blaster_tactic(m, p), + using_params(mk_simplify_tactic(m, p), simp_p), + cond(mk_is_propositional_probe(), + cond(mk_produce_proofs_probe(), + mk_smt_tactic(), // `sat' does not support proofs. + mk_sat_tactic(m, p)), + cond(mk_has_fp_to_real_probe(), + mk_qfnra_tactic(m, p), + mk_smt_tactic(p))), + mk_fail_if_undecided_tactic()); st->updt_params(p); return st; diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 33b6c15b9..59b9fd7a5 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -820,4 +820,4 @@ public: } }; -#endif \ No newline at end of file +#endif diff --git a/src/tactic/sls/sls_powers.h b/src/tactic/sls/sls_powers.h index c514fec00..b632e7100 100644 --- a/src/tactic/sls/sls_powers.h +++ b/src/tactic/sls/sls_powers.h @@ -46,4 +46,4 @@ public: } }; -#endif \ No newline at end of file +#endif diff --git a/src/test/hashtable.cpp b/src/test/hashtable.cpp index b01518985..47fae454a 100644 --- a/src/test/hashtable.cpp +++ b/src/test/hashtable.cpp @@ -18,7 +18,7 @@ Revision History: --*/ #ifdef _WINDOWS #include -#include +#include #include #include"hashtable.h" @@ -30,7 +30,7 @@ Revision History: struct int_hash_proc { unsigned operator()(int x) const { return x * 3; } }; typedef int_hashtable > int_set; -typedef stdext::hash_set > > safe_int_set; +typedef std::unordered_set > > safe_int_set; // typedef safe_int_set int_set; inline bool contains(int_set & h, int i) { diff --git a/src/util/hash.cpp b/src/util/hash.cpp index bb5ca0a41..42ba3f4da 100644 --- a/src/util/hash.cpp +++ b/src/util/hash.cpp @@ -52,38 +52,38 @@ unsigned string_hash(const char * str, unsigned length, unsigned init_value) { switch(len) { /* all the case statements fall through */ case 11: c+=((unsigned)str[10]<<24); - __fallthrough; + Z3_fallthrough; case 10: c+=((unsigned)str[9]<<16); - __fallthrough; + Z3_fallthrough; case 9 : c+=((unsigned)str[8]<<8); - __fallthrough; + Z3_fallthrough; /* the first byte of c is reserved for the length */ case 8 : b+=((unsigned)str[7]<<24); - __fallthrough; + Z3_fallthrough; case 7 : b+=((unsigned)str[6]<<16); - __fallthrough; + Z3_fallthrough; case 6 : b+=((unsigned)str[5]<<8); - __fallthrough; + Z3_fallthrough; case 5 : b+=str[4]; - __fallthrough; + Z3_fallthrough; case 4 : a+=((unsigned)str[3]<<24); - __fallthrough; + Z3_fallthrough; case 3 : a+=((unsigned)str[2]<<16); - __fallthrough; + Z3_fallthrough; case 2 : a+=((unsigned)str[1]<<8); - __fallthrough; + Z3_fallthrough; case 1 : a+=str[0]; - __fallthrough; + Z3_fallthrough; /* case 0: nothing left to add */ } mix(a,b,c); diff --git a/src/util/hash.h b/src/util/hash.h index 59bc2cc3b..82d343661 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -22,10 +22,6 @@ Revision History: #include #include"util.h" -#ifndef __fallthrough -#define __fallthrough -#endif - #define mix(a,b,c) \ { \ a -= b; a -= c; a ^= (c>>13); \ @@ -116,7 +112,7 @@ unsigned get_composite_hash(Composite app, unsigned n, GetKindHashProc const & k switch (n) { case 2: b += chasher(app, 1); - __fallthrough; + Z3_fallthrough; case 1: c += chasher(app, 0); } diff --git a/src/util/hwf.h b/src/util/hwf.h index d2055d56e..cf0c9b7ea 100644 --- a/src/util/hwf.h +++ b/src/util/hwf.h @@ -127,15 +127,15 @@ public: void to_rational(hwf const & x, scoped_mpq & o) { to_rational(x, o.m(), o); } - bool sgn(hwf const & x) const { + bool sgn(hwf const & x) const { return (x.get_raw() & 0x8000000000000000ull) != 0; } - uint64 sig(hwf const & x) const { + uint64 sig(hwf const & x) const { return x.get_raw() & 0x000FFFFFFFFFFFFFull; } - int exp(hwf const & x) const { + int exp(hwf const & x) const { return ((x.get_raw() & 0x7FF0000000000000ull) >> 52) - 1023; } diff --git a/src/util/util.h b/src/util/util.h index 2e7e860d7..f97f5c1f9 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -68,6 +68,18 @@ COMPILE_TIME_ASSERT(sizeof(int64) == 8); #define THREAD_LOCAL #endif +#ifdef __fallthrough +# define Z3_fallthrough __fallthrough +#elif defined(__has_cpp_attribute) +# if __has_cpp_attribute(clang::fallthrough) +# define Z3_fallthrough [[clang::fallthrough]] +# else +# define Z3_fallthrough +# endif +#else +# define Z3_fallthrough +#endif + inline bool is_power_of_two(unsigned v) { return !(v & (v - 1)) && v; } /** @@ -273,10 +285,6 @@ bool has_duplicates(const IT & begin, const IT & end) { return false; } -#ifndef __fallthrough -#define __fallthrough -#endif - #ifndef _WINDOWS #ifndef __declspec #define __declspec(X)