diff --git a/RELEASE_NOTES b/RELEASE_NOTES index afa613f57..2c7e2e0fb 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -1,6 +1,6 @@ RELEASE NOTES -Version 4.4 +Version 4.4.0 ============= - New feature: Support for the theory of floating-point numbers. This comes in the form of logics (QF_FP and QF_FPBV), tactics (qffp and qffpbv), as well as a theory plugin that allows theory combinations. Z3 supports the official SMT theory definition of FP (see http://smtlib.cs.uiowa.edu/theories/FloatingPoint.smt2) in SMT2 files, as well as all APIs. diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 1e21ff810..556b06098 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -9,7 +9,7 @@ from mk_util import * # Z3 Project definition def init_project_def(): - set_version(4, 4, 0, 0) + set_version(4, 4, 1, 0) add_lib('util', []) add_lib('polynomial', ['util'], 'math/polynomial') add_lib('sat', ['util']) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 547379aec..72d432eab 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -86,6 +86,9 @@ VS_PAR_NUM=8 GPROF=False GIT_HASH=False +FPMATH="Default" +FPMATH_FLAGS="-mfpmath=sse -msse -msse2" + def check_output(cmd): return str(subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).rstrip('\r\n') @@ -227,10 +230,37 @@ def test_openmp(cc): t.add('#include\nint main() { return omp_in_parallel() ? 1 : 0; }\n') t.commit() if IS_WINDOWS: - return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '/openmp']) == 0 + r = exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '/openmp']) == 0 + try: + rmf('tstomp.obj') + rmf('tstomp.exe') + except: + pass + return r else: return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '-fopenmp']) == 0 +def test_fpmath(cc): + global FPMATH_FLAGS + if is_verbose(): + print("Testing floating point support...") + t = TempFile('tstsse.cpp') + t.add('int main() { return 42; }\n') + t.commit() + if exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-mfpmath=sse -msse -msse2']) == 0: + FPMATH_FLAGS="-mfpmath=sse -msse -msse2" + return "SSE2-GCC" + elif exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-msse -msse2']) == 0: + FPMATH_FLAGS="-msse -msse2" + return "SSE2-CLANG" + elif exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-mfpu=vfp -mfloat-abi=hard']) == 0: + FPMATH_FLAGS="-mfpu=vfp -mfloat-abi=hard" + return "ARM-VFP" + else: + FPMATH_FLAGS="" + return "UNKNOWN" + + def find_jni_h(path): for root, dirs, files in os.walk(path): for f in files: @@ -357,10 +387,14 @@ def check_ml(): r = exec_cmd([OCAMLOPT, '-o', 'a.out', 'hello.ml']) if r != 0: raise MKException('Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler. Note that ocamlopt may require flexlink to be in your path.') - rmf('hello.cmi') - rmf('hello.cmo') - rmf('hello.cmx') - rmf('a.out') + try: + rmf('hello.cmi') + rmf('hello.cmo') + rmf('hello.cmx') + rmf('a.out') + rmf('hello.o') + except: + pass find_ml_lib() find_ocaml_find() @@ -1777,7 +1811,7 @@ def mk_config(): print('OCaml Native: %s' % OCAMLOPT) print('OCaml Library: %s' % OCAML_LIB) else: - global CXX, CC, GMP, FOCI2, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG + global CXX, CC, GMP, FOCI2, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS OS_DEFINES = "" ARITH = "internal" check_ar() @@ -1806,9 +1840,11 @@ def mk_config(): if GIT_HASH: CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH) CXXFLAGS = '%s -fvisibility=hidden -c' % CXXFLAGS + FPMATH = test_fpmath(CXX) + CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS) HAS_OMP = test_openmp(CXX) if HAS_OMP: - CXXFLAGS = '%s -fopenmp -mfpmath=sse' % CXXFLAGS + CXXFLAGS = '%s -fopenmp' % CXXFLAGS LDFLAGS = '%s -fopenmp' % LDFLAGS SLIBEXTRAFLAGS = '%s -fopenmp' % SLIBEXTRAFLAGS else: @@ -1861,7 +1897,6 @@ def mk_config(): CPPFLAGS = '%s -DZ3DEBUG' % CPPFLAGS if TRACE or DEBUG_MODE: CPPFLAGS = '%s -D_TRACE' % CPPFLAGS - CXXFLAGS = '%s -msse -msse2' % CXXFLAGS config.write('PREFIX=%s\n' % PREFIX) config.write('CC=%s\n' % CC) config.write('CXX=%s\n' % CXX) @@ -1892,6 +1927,7 @@ def mk_config(): print('OpenMP: %s' % HAS_OMP) print('Prefix: %s' % PREFIX) print('64-bit: %s' % is64()) + print('FP math: %s' % FPMATH) if GPROF: print('gprof: enabled') print('Python version: %s' % distutils.sysconfig.get_python_version()) diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 33d7a3eab..db4cc48e3 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -47,16 +47,16 @@ def set_build_dir(path): mk_dir(BUILD_X64_DIR) def display_help(): - print "mk_win_dist.py: Z3 Windows distribution generator\n" - print "This script generates the zip files containing executables, dlls, header files for Windows." - print "It must be executed from the Z3 root directory." - print "\nOptions:" - print " -h, --help display this message." - print " -s, --silent do not print verbose messages." - print " -b , --build= subdirectory where x86 and x64 Z3 versions will be built (default: build-dist)." - print " -f, --force force script to regenerate Makefiles." - print " --nojava do not include Java bindings in the binary distribution files." - print " --githash include git hash in the Zip file." + print("mk_win_dist.py: Z3 Windows distribution generator\n") + print("This script generates the zip files containing executables, dlls, header files for Windows.") + print("It must be executed from the Z3 root directory.") + print("\nOptions:") + print(" -h, --help display this message.") + print(" -s, --silent do not print verbose messages.") + print(" -b , --build= subdirectory where x86 and x64 Z3 versions will be built (default: build-dist).") + print(" -f, --force force script to regenerate Makefiles.") + print(" --nojava do not include Java bindings in the binary distribution files.") + print(" --githash include git hash in the Zip file.") exit(0) # Parse configuration option for mk_make script @@ -180,7 +180,7 @@ def mk_dist_dir_core(x64): mk_util.JAVA_ENABLED = JAVA_ENABLED mk_win_dist(build_path, dist_path) if is_verbose(): - print "Generated %s distribution folder at '%s'" % (platform, dist_path) + print("Generated %s distribution folder at '%s'") % (platform, dist_path) def mk_dist_dir(): mk_dist_dir_core(False) @@ -208,7 +208,7 @@ def mk_zip_core(x64): ZIPOUT = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED) os.path.walk(dist_path, mk_zip_visitor, '*') if is_verbose(): - print "Generated '%s'" % zfname + print("Generated '%s'") % zfname except: pass ZIPOUT = None @@ -253,7 +253,7 @@ def cp_vs_runtime_core(x64): for f in VS_RUNTIME_FILES: shutil.copy(f, bin_dist_path) if is_verbose(): - print "Copied '%s' to '%s'" % (f, bin_dist_path) + print("Copied '%s' to '%s'") % (f, bin_dist_path) def cp_vs_runtime(): cp_vs_runtime_core(True) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 917b0a954..b4fb954b8 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2516,7 +2516,7 @@ namespace Microsoft.Z3 /// Create a bit-vector numeral. /// /// value of the numeral. - /// /// the size of the bit-vector + /// the size of the bit-vector public BitVecNum MkBV(long v, uint size) { Contract.Ensures(Contract.Result() != null); diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 6780145d9..3a6275e33 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1043,6 +1043,13 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters case OP_DISTINCT: { func_decl_info info(m_family_id, OP_DISTINCT); info.set_pairwise(); + for (unsigned i = 1; i < arity; i++) { + if (domain[i] != domain[0]) { + std::ostringstream buffer; + buffer << "Sort mismatch between first argument and argument " << (i+1); + throw ast_exception(buffer.str().c_str()); + } + } return m_manager->mk_func_decl(symbol("distinct"), arity, domain, m_bool_sort, info); } default: @@ -2338,6 +2345,10 @@ quantifier * ast_manager::update_quantifier(quantifier * q, bool is_forall, unsi num_patterns == 0 ? q->get_no_patterns() : 0); } +app * ast_manager::mk_distinct(unsigned num_args, expr * const * args) { + return mk_app(m_basic_family_id, OP_DISTINCT, num_args, args); +} + app * ast_manager::mk_distinct_expanded(unsigned num_args, expr * const * args) { if (num_args < 2) return mk_true(); diff --git a/src/ast/ast.h b/src/ast/ast.h index 93f456965..a5f5c286f 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2000,7 +2000,7 @@ public: app * mk_and(expr * arg1, expr * arg2, expr * arg3) { return mk_app(m_basic_family_id, OP_AND, arg1, arg2, arg3); } app * mk_implies(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_IMPLIES, arg1, arg2); } app * mk_not(expr * n) { return mk_app(m_basic_family_id, OP_NOT, n); } - app * mk_distinct(unsigned num_args, expr * const * args) { return mk_app(m_basic_family_id, OP_DISTINCT, num_args, args); } + app * mk_distinct(unsigned num_args, expr * const * args); app * mk_distinct_expanded(unsigned num_args, expr * const * args); app * mk_true() { return m_true; } app * mk_false() { return m_false; } diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 69b661589..60120bea2 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1041,80 +1041,54 @@ void fpa2bv_converter::mk_min(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 c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), c1_and(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, c1_and); - mk_is_nan(x, x_is_nan); - m_simp.mk_or(x_is_nan, c1_and, c1); - + m_simp.mk_and(x_is_zero, y_is_zero, both_zero); + mk_is_nan(x, x_is_nan); mk_is_nan(y, y_is_nan); - c2 = y_is_nan; + mk_pzero(f, pzero); + + expr_ref lt(m); + mk_float_lt(f, num, args, lt); - expr_ref c3(m); - mk_float_lt(f, num, args, c3); + result = y; + mk_ite(lt, x, result, result); + mk_ite(both_zero, pzero, result, result); + mk_ite(y_is_nan, x, result, result); + mk_ite(x_is_nan, y, result, result); - expr_ref r_sgn(m), r_sig(m), r_exp(m); - - expr_ref c3xy(m), c2c3(m); - m_simp.mk_ite(c3, x_sgn, y_sgn, c3xy); - m_simp.mk_ite(c2, x_sgn, c3xy, c2c3); - m_simp.mk_ite(c1, y_sgn, c2c3, r_sgn); - - expr_ref c3xy_sig(m), c2c3_sig(m); - m_simp.mk_ite(c3, x_sig, y_sig, c3xy_sig); - m_simp.mk_ite(c2, x_sig, c3xy_sig, c2c3_sig); - m_simp.mk_ite(c1, y_sig, c2c3_sig, r_sig); - - expr_ref c3xy_exp(m), c2c3_exp(m); - m_simp.mk_ite(c3, x_exp, y_exp, c3xy_exp); - m_simp.mk_ite(c2, x_exp, c3xy_exp, c2c3_exp); - m_simp.mk_ite(c1, y_exp, c2c3_exp, r_exp); - - mk_fp(r_sgn, r_exp, r_sig, result); + SASSERT(is_well_sorted(m, result)); } void fpa2bv_converter::mk_max(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; - expr * y_sgn, * y_sig, * y_exp; + expr * x = args[0], *y = args[1]; + + expr * x_sgn, *x_sig, *x_exp; + 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 c1(m), c2(m), x_is_nan(m), y_is_nan(m), y_is_zero(m), x_is_zero(m), c1_and(m); - mk_is_zero(y, y_is_zero); + 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); - m_simp.mk_and(y_is_zero, x_is_zero, c1_and); - mk_is_nan(x, x_is_nan); - m_simp.mk_or(x_is_nan, c1_and, c1); - + 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(y, y_is_nan); - c2 = y_is_nan; - - expr_ref c3(m); - mk_float_gt(f, num, args, c3); + mk_pzero(f, pzero); - expr_ref r_sgn(m), r_sig(m), r_exp(m); - - expr_ref c3xy_sgn(m), c2c3_sgn(m); - m_simp.mk_ite(c3, x_sgn, y_sgn, c3xy_sgn); - m_simp.mk_ite(c2, x_sgn, c3xy_sgn, c2c3_sgn); - m_simp.mk_ite(c1, y_sgn, c2c3_sgn, r_sgn); + expr_ref gt(m); + mk_float_gt(f, num, args, gt); - expr_ref c3xy_sig(m), c2c3_sig(m); - m_simp.mk_ite(c3, x_sig, y_sig, c3xy_sig); - m_simp.mk_ite(c2, x_sig, c3xy_sig, c2c3_sig); - m_simp.mk_ite(c1, y_sig, c2c3_sig, r_sig); + result = y; + mk_ite(gt, x, result, result); + mk_ite(both_zero, pzero, result, result); + mk_ite(y_is_nan, x, result, result); + mk_ite(x_is_nan, y, result, result); - expr_ref c3xy_exp(m), c2c3_exp(m); - m_simp.mk_ite(c3, x_exp, y_exp, c3xy_exp); - m_simp.mk_ite(c2, x_exp, c3xy_exp, c2c3_exp); - m_simp.mk_ite(c1, y_exp, c2c3_exp, r_exp); - - mk_fp(r_sgn, r_exp, r_sig, result); + SASSERT(is_well_sorted(m, result)); } void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { @@ -2096,79 +2070,89 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * bool is_int; m_util.au().is_numeral(x, q, is_int); - scoped_mpf v(m_mpf_manager); - m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); + if (q.is_zero()) + return mk_pzero(f, result); + else { + scoped_mpf v(m_mpf_manager); + m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); - expr_ref sgn(m), s(m), e(m), unbiased_exp(m); - sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1); - unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits); - mk_bias(unbiased_exp, e); - mk_fp(sgn, e, s, result); + + expr_ref sgn(m), s(m), e(m), unbiased_exp(m); + sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v)) ? 1 : 0, 1); + s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1); + unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits); + mk_bias(unbiased_exp, e); + + mk_fp(sgn, e, s, result); + } } else if (m_util.au().is_numeral(x)) { rational q; bool is_int; m_util.au().is_numeral(x, q, is_int); - 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); + if (m_util.au().is_zero(x)) + 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); - 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); - m_util.fm().set(v_nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq()); - m_util.fm().set(v_nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq()); - m_util.fm().set(v_tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq()); - m_util.fm().set(v_tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq()); - m_util.fm().set(v_tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq()); + 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); + m_util.fm().set(v_nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq()); + m_util.fm().set(v_nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq()); + m_util.fm().set(v_tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq()); + m_util.fm().set(v_tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq()); + m_util.fm().set(v_tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq()); - expr_ref v1(m), v2(m), v3(m), v4(m); + expr_ref v1(m), v2(m), v3(m), v4(m); - expr_ref sgn(m), s(m), e(m), unbiased_exp(m); - sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nta)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1); - unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nta), ebits); - mk_bias(unbiased_exp, e); - mk_fp(sgn, e, s, v1); + expr_ref sgn(m), s(m), e(m), unbiased_exp(m); + sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nta)) ? 1 : 0, 1); + s = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1); + unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nta), ebits); + mk_bias(unbiased_exp, e); + mk_fp(sgn, e, s, v1); - sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nte)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1); - unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nte), ebits); - mk_bias(unbiased_exp, e); - mk_fp(sgn, e, s, v2); + sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nte)) ? 1 : 0, 1); + s = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1); + unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nte), ebits); + mk_bias(unbiased_exp, e); + mk_fp(sgn, e, s, v2); - sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1); - unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits); - mk_bias(unbiased_exp, e); - mk_fp(sgn, e, s, v3); + sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1); + s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1); + unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits); + mk_bias(unbiased_exp, e); + mk_fp(sgn, e, s, v3); - sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1); - unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits); - mk_bias(unbiased_exp, e); - mk_fp(sgn, e, s, v4); + sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1); + s = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1); + unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits); + mk_bias(unbiased_exp, e); + mk_fp(sgn, e, s, v4); - sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1); - unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits); - mk_bias(unbiased_exp, e); - - mk_fp(sgn, e, s, result); - mk_ite(rm_tn, v4, result, result); - mk_ite(rm_tp, v3, result, result); - mk_ite(rm_nte, v2, result, result); - mk_ite(rm_nta, v1, result, result); + sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1); + s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1); + unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits); + mk_bias(unbiased_exp, e); + + mk_fp(sgn, e, s, result); + mk_ite(rm_tn, v4, result, result); + mk_ite(rm_tp, v3, result, result); + mk_ite(rm_nte, v2, result, result); + mk_ite(rm_nta, v1, result, result); + } } else { bv_util & bu = m_bv_util; arith_util & au = m_arith_util; - + expr_ref bv0(m), bv1(m), zero(m), two(m); bv0 = bu.mk_numeral(0, 1); bv1 = bu.mk_numeral(1, 1); @@ -2182,6 +2166,10 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * expr_ref rme(rm, m); round(s, rme, sgn, sig, exp, result); + + expr_ref c0(m); + mk_is_zero(x, c0); + mk_ite(c0, x, result, result); expr * e = m.mk_eq(m_util.mk_to_real(result), x); m_extra_assertions.push_back(e); @@ -2209,38 +2197,43 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con SASSERT(e.is_int64()); SASSERT(m_mpz_manager.eq(e.to_mpq().denominator(), 1)); - scoped_mpf nte(m_mpf_manager), nta(m_mpf_manager), tp(m_mpf_manager), tn(m_mpf_manager), tz(m_mpf_manager); - m_mpf_manager.set(nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq(), e.to_mpq().numerator()); - m_mpf_manager.set(nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq(), e.to_mpq().numerator()); - m_mpf_manager.set(tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq(), e.to_mpq().numerator()); - m_mpf_manager.set(tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq(), e.to_mpq().numerator()); - m_mpf_manager.set(tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq(), e.to_mpq().numerator()); + if (q.is_zero()) + return mk_pzero(f, result); + else { + scoped_mpf nte(m_mpf_manager), nta(m_mpf_manager), tp(m_mpf_manager), tn(m_mpf_manager), tz(m_mpf_manager); + m_mpf_manager.set(nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq(), e.to_mpq().numerator()); + m_mpf_manager.set(nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq(), e.to_mpq().numerator()); + m_mpf_manager.set(tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq(), e.to_mpq().numerator()); + m_mpf_manager.set(tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq(), e.to_mpq().numerator()); + m_mpf_manager.set(tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq(), e.to_mpq().numerator()); - app_ref a_nte(m), a_nta(m), a_tp(m), a_tn(m), a_tz(m); - a_nte = m_plugin->mk_numeral(nte); - a_nta = m_plugin->mk_numeral(nta); - a_tp = m_plugin->mk_numeral(tp); - a_tn = m_plugin->mk_numeral(tn); - a_tz = m_plugin->mk_numeral(tz); + app_ref a_nte(m), a_nta(m), a_tp(m), a_tn(m), a_tz(m); + a_nte = m_plugin->mk_numeral(nte); + a_nta = m_plugin->mk_numeral(nta); + a_tp = m_plugin->mk_numeral(tp); + a_tn = m_plugin->mk_numeral(tn); + a_tz = m_plugin->mk_numeral(tz); - expr_ref bv_nte(m), bv_nta(m), bv_tp(m), bv_tn(m), bv_tz(m); - mk_numeral(a_nte->get_decl(), 0, 0, bv_nte); - mk_numeral(a_nta->get_decl(), 0, 0, bv_nta); - mk_numeral(a_tp->get_decl(), 0, 0, bv_tp); - mk_numeral(a_tn->get_decl(), 0, 0, bv_tn); - mk_numeral(a_tz->get_decl(), 0, 0, bv_tz); + expr_ref bv_nte(m), bv_nta(m), bv_tp(m), bv_tn(m), bv_tz(m); + mk_numeral(a_nte->get_decl(), 0, 0, bv_nte); + mk_numeral(a_nta->get_decl(), 0, 0, bv_nta); + mk_numeral(a_tp->get_decl(), 0, 0, bv_tp); + mk_numeral(a_tn->get_decl(), 0, 0, bv_tn); + 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)); + 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)); - mk_ite(c1, bv_tn, bv_tz, result); - mk_ite(c2, bv_tp, result, result); - mk_ite(c3, bv_nta, result, result); - mk_ite(c4, bv_nte, result, result); + mk_ite(c1, bv_tn, bv_tz, result); + mk_ite(c2, bv_tp, result, result); + mk_ite(c3, bv_nta, result, result); + mk_ite(c4, bv_nte, result, result); + } } + void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { TRACE("fpa2bv_to_real", for (unsigned i = 0; i < num; i++) tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); @@ -2367,10 +2360,9 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const mk_pinf(f, pinf); // Special case: x == 0 -> p/n zero - expr_ref c1(m), v1(m), rm_is_to_neg(m); - c1 = is_zero; - mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); - mk_ite(rm_is_to_neg, nzero, pzero, v1); + expr_ref c1(m), v1(m); + c1 = is_zero; + v1 = pzero; // Special case: x != 0 expr_ref is_neg_bit(m), exp_too_large(m), sig_4(m), exp_2(m); @@ -2508,10 +2500,9 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con mk_pinf(f, pinf); // Special case: x == 0 -> p/n zero - expr_ref c1(m), v1(m), rm_is_to_neg(m); + expr_ref c1(m), v1(m); c1 = is_zero; - mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); - mk_ite(rm_is_to_neg, nzero, pzero, v1); + v1 = pzero; // Special case: x != 0 expr_ref exp_too_large(m), sig_4(m), exp_2(m); @@ -3182,7 +3173,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref m_simp.mk_ite(m.mk_or(is_normal, is_sig_zero), zero_e, lz_d, lz); dbg_decouple("fpa2bv_unpack_lz", lz); - expr_ref shift(m); + expr_ref shift(m); m_simp.mk_ite(is_sig_zero, zero_e, lz, shift); dbg_decouple("fpa2bv_unpack_shift", shift); SASSERT(is_well_sorted(m, is_sig_zero)); diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 48b7adb8b..e559ee179 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -879,12 +879,20 @@ void fpa_decl_plugin::get_sort_names(svector & sort_names, symbol } expr * fpa_decl_plugin::get_some_value(sort * s) { - SASSERT(s->is_sort_of(m_family_id, FLOATING_POINT_SORT)); - mpf tmp; - m_fm.mk_nan(s->get_parameter(0).get_int(), s->get_parameter(1).get_int(), tmp); - expr * res = this->mk_numeral(tmp); - m_fm.del(tmp); - return res; + if (s->is_sort_of(m_family_id, FLOATING_POINT_SORT)) { + mpf tmp; + m_fm.mk_nan(s->get_parameter(0).get_int(), s->get_parameter(1).get_int(), tmp); + expr * res = mk_numeral(tmp); + m_fm.del(tmp); + return res; + } + else if (s->is_sort_of(m_family_id, ROUNDING_MODE_SORT)) { + func_decl * f = mk_rm_const_decl(OP_FPA_RM_TOWARD_ZERO, 0, 0, 0, 0, s); + return m_manager->mk_const(f); + } + + UNREACHABLE(); + return 0; } bool fpa_decl_plugin::is_value(app * e) const { diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 6aee683ff..5fb9dfd37 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -411,14 +411,20 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { result = arg1; return BR_DONE; } - // expand as using ite's - result = m().mk_ite(m().mk_or(mk_eq_nan(arg1), m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2))), + if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) { + result = m_util.mk_pzero(m().get_sort(arg1)); + return BR_DONE; + } + + result = m().mk_ite(mk_eq_nan(arg1), arg2, - m().mk_ite(mk_eq_nan(arg2), - arg1, - m().mk_ite(m_util.mk_lt(arg1, arg2), - arg1, - arg2))); + m().mk_ite(mk_eq_nan(arg2), + arg1, + m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), + m_util.mk_pzero(m().get_sort(arg1)), + m().mk_ite(m_util.mk_lt(arg1, arg2), + arg1, + arg2)))); return BR_REWRITE_FULL; } @@ -431,14 +437,20 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { result = arg1; return BR_DONE; } - // expand as using ite's - result = m().mk_ite(m().mk_or(mk_eq_nan(arg1), m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2))), + if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) { + result = m_util.mk_pzero(m().get_sort(arg1)); + return BR_DONE; + } + + result = m().mk_ite(mk_eq_nan(arg1), arg2, - m().mk_ite(mk_eq_nan(arg2), - arg1, - m().mk_ite(m_util.mk_gt(arg1, arg2), - arg1, - arg2))); + m().mk_ite(mk_eq_nan(arg2), + arg1, + m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), + m_util.mk_pzero(m().get_sort(arg1)), + m().mk_ite(m_util.mk_gt(arg1, arg2), + arg1, + arg2)))); return BR_REWRITE_FULL; } diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 9d90a05c7..c9b5e7920 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -398,10 +398,27 @@ public: s.assert_expr(to_expr(cnsts[i].raw())); } + void get_proof_assumptions(z3pf proof, std::vector &cnsts, hash_set &memo){ + if(memo.find(proof) != memo.end())return; + memo.insert(proof); + pfrule dk = pr(proof); + if(dk == PR_ASSERTED) + cnsts.push_back(conc(proof)); + else { + unsigned nprems = num_prems(proof); + for(unsigned i = 0; i < nprems; i++){ + z3pf arg = prem(proof,i); + get_proof_assumptions(arg,cnsts,memo); + } + } + } + iz3interp(ast_manager &_m_manager) : iz3base(_m_manager) {} }; + + void iz3interpolate(ast_manager &_m_manager, ast *proof, const ptr_vector &cnsts, @@ -475,6 +492,13 @@ void iz3interpolate(ast_manager &_m_manager, _cnsts[i] = itp.cook(cnsts[i]); iz3mgr::ast _proof = itp.cook(proof); iz3mgr::ast _tree = itp.cook(tree); + + // if consts isn't provided, we can reconstruct it + if(_cnsts.empty()){ + hash_set memo; + itp.get_proof_assumptions(_proof,_cnsts,memo); + } + itp.proof_to_interpolant(_proof,_cnsts,_tree,_interps,options); interps.resize(_interps.size()); for(unsigned i = 0; i < interps.size(); i++) diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h index 2b1926994..c2668eb56 100644 --- a/src/interp/iz3interp.h +++ b/src/interp/iz3interp.h @@ -67,7 +67,11 @@ void iz3interpolate(ast_manager &_m_manager, interpolation_options_struct * options = 0); /* Compute an interpolant from a proof. This version uses the ast - representation, for compatibility with the new API. */ + representation, for compatibility with the new API. Here, cnsts is + a vector of all the assertions in the proof. This can be + over-approximated by the set of all assertions in the + solver. However, if it is empty it will be reconstructed from the + proof, so it can be considered a hint. */ void iz3interpolate(ast_manager &_m_manager, ast *proof, diff --git a/src/test/api.cpp b/src/test/api.cpp index a09371f01..234d1192c 100644 --- a/src/test/api.cpp +++ b/src/test/api.cpp @@ -447,9 +447,28 @@ void test_bvneg() { Z3_del_context(ctx); } +static bool cb_called = false; +static void my_cb(Z3_context, Z3_error_code) { + cb_called = true; +} + +static void test_mk_distinct() { + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = Z3_mk_context(cfg); + Z3_set_error_handler(ctx, my_cb); + + Z3_sort bv8 = Z3_mk_bv_sort(ctx, 8); + Z3_sort bv32 = Z3_mk_bv_sort(ctx, 32); + Z3_ast args[] = { Z3_mk_int64(ctx, 0, bv8), Z3_mk_int64(ctx, 0, bv32) }; + Z3_ast d = Z3_mk_distinct(ctx, 2, args); + SASSERT(cb_called); + +} + void tst_api() { test_apps(); test_bvneg(); + test_mk_distinct(); // bv_invariant(); } #else diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index c96ba594e..9de56773a 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1475,6 +1475,9 @@ void mpf_manager::mk_ninf(unsigned ebits, unsigned sbits, mpf & o) { void mpf_manager::unpack(mpf & o, bool normalize) { // Insert the hidden bit or adjust the exponent of denormal numbers. + if (is_zero(o)) + return; + if (is_normal(o)) m_mpz_manager.add(o.significand, m_powers2(o.sbits-1), o.significand); else {