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

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.

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'])

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<omp.h>\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')
+    try:
-    rmf('hello.cmo')
+        rmf('hello.cmi')
-    rmf('hello.cmx')
+        rmf('hello.cmo')
-    rmf('a.out')
+        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())            

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("mk_win_dist.py: Z3 Windows distribution generator\n")
-    print "This script generates the zip files containing executables, dlls, header files for Windows."
+    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("It must be executed from the Z3 root directory.")
-    print "\nOptions:"
+    print("\nOptions:")
-    print "  -h, --help                    display this message."
+    print("  -h, --help                    display this message.")
-    print "  -s, --silent                  do not print verbose messages."
+    print("  -s, --silent                  do not print verbose messages.")
-    print "  -b <sudir>, --build=<subdir>  subdirectory where x86 and x64 Z3 versions will be built (default: build-dist)."
+    print("  -b <sudir>, --build=<subdir>  subdirectory where x86 and x64 Z3 versions will be built (default: build-dist).")
-    print "  -f, --force                   force script to regenerate Makefiles."
+    print("  -f, --force                   force script to regenerate Makefiles.")
-    print "  --nojava                      do not include Java bindings in the binary distribution files."
+    print("  --nojava                      do not include Java bindings in the binary distribution files.")
-    print "  --githash                     include git hash in the Zip file."
+    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)

src/api/dotnet/Context.cs

@@ -2516,7 +2516,7 @@ namespace Microsoft.Z3
         /// Create a bit-vector numeral.
         /// </summary>
         /// <param name="v">value of the numeral.</param>
-        /// /// <param name="size">the size of the bit-vector</param>
+        /// <param name="size">the size of the bit-vector</param>
         public BitVecNum MkBV(long v, uint size)
         {
             Contract.Ensures(Contract.Result<BitVecNum>() != null);

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();

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; }

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);
+    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);    
-    m_simp.mk_or(x_is_nan, c1_and, c1);
-
     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);
+    result = y;
-    mk_float_lt(f, num, args, c3);
+    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);
+    SASSERT(is_well_sorted(m, result));
-    
-    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);
 }
 
 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 * x = args[0], *y = args[1];
-    expr * y_sgn, * y_sig, * y_exp;
+
+    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);
+    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(y, y_is_zero);
     mk_is_zero(x, x_is_zero);
-    m_simp.mk_and(y_is_zero, x_is_zero, c1_and);
+    mk_is_zero(y, y_is_zero);
-    mk_is_nan(x, x_is_nan);    
+    m_simp.mk_and(x_is_zero, y_is_zero, both_zero);
-    m_simp.mk_or(x_is_nan, c1_and, c1);
+    mk_is_nan(x, x_is_nan);
-        
     mk_is_nan(y, y_is_nan);
-    c2 = y_is_nan;
+    mk_pzero(f, pzero);
-    
-    expr_ref c3(m);
-    mk_float_gt(f, num, args, c3);
 
-    expr_ref r_sgn(m), r_sig(m), r_exp(m);
+    expr_ref gt(m);
-    
+    mk_float_gt(f, num, args, gt);
-    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 c3xy_sig(m), c2c3_sig(m);
+    result = y;
-    m_simp.mk_ite(c3, x_sig, y_sig, c3xy_sig);
+    mk_ite(gt, x, result, result);
-    m_simp.mk_ite(c2, x_sig, c3xy_sig, c2c3_sig);
+    mk_ite(both_zero, pzero, result, result);
-    m_simp.mk_ite(c1, y_sig, c2c3_sig, r_sig);
+    mk_ite(y_is_nan, x, result, result);
+    mk_ite(x_is_nan, y, result, result);
 
-    expr_ref c3xy_exp(m), c2c3_exp(m);
+    SASSERT(is_well_sorted(m, result));
-    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);
 }
 
 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);
+        if (q.is_zero())
-        m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
+            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);
+        if (m_util.au().is_zero(x))
-        mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_nta);
+            mk_pzero(f, result);
-        mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_nte);
+        else {
-        mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_tp);
+            expr_ref rm_nta(m), rm_nte(m), rm_tp(m), rm_tn(m), rm_tz(m);
-        mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_tn);
+            mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_nta);
-        mk_is_rm(rm, BV_RM_TO_ZERO, rm_tz);        
+            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_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);
+            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_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_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_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_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());
+            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);
+            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);
+            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);
+            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);
+            unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nta), ebits);
-        mk_bias(unbiased_exp, e);
+            mk_bias(unbiased_exp, e);
-        mk_fp(sgn, e, s, v1);
+            mk_fp(sgn, e, s, v1);
 
-        sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nte)) ? 1 : 0, 1);
+            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);
+            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);
+            unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nte), ebits);
-        mk_bias(unbiased_exp, e);
+            mk_bias(unbiased_exp, e);
-        mk_fp(sgn, e, s, v2);
+            mk_fp(sgn, e, s, v2);
 
-        sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
+            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);
+            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);
+            unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
-        mk_bias(unbiased_exp, e);
+            mk_bias(unbiased_exp, e);
-        mk_fp(sgn, e, s, v3);
+            mk_fp(sgn, e, s, v3);
 
-        sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1);
+            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);
+            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);
+            unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits);
-        mk_bias(unbiased_exp, e);
+            mk_bias(unbiased_exp, e);
-        mk_fp(sgn, e, s, v4);
+            mk_fp(sgn, e, s, v4);
 
-        sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
+            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);
+            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);
+            unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
-        mk_bias(unbiased_exp, e);
+            mk_bias(unbiased_exp, e);
-        
+
-        mk_fp(sgn, e, s, result);        
+            mk_fp(sgn, e, s, result);
-        mk_ite(rm_tn, v4, result, result);
+            mk_ite(rm_tn, v4, result, result);
-        mk_ite(rm_tp, v3, result, result);
+            mk_ite(rm_tp, v3, result, result);
-        mk_ite(rm_nte, v2, result, result);
+            mk_ite(rm_nte, v2, result, result);
-        mk_ite(rm_nta, v1, 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);
+    if (q.is_zero())
-    m_mpf_manager.set(nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq(), e.to_mpq().numerator());
+        return mk_pzero(f, result);
-    m_mpf_manager.set(nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq(), e.to_mpq().numerator());
+    else {
-    m_mpf_manager.set(tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq(), e.to_mpq().numerator());
+        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(tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq(), e.to_mpq().numerator());
+        m_mpf_manager.set(nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, 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());
+        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);
+        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_nte = m_plugin->mk_numeral(nte);
-    a_nta = m_plugin->mk_numeral(nta);
+        a_nta = m_plugin->mk_numeral(nta);
-    a_tp = m_plugin->mk_numeral(tp);
+        a_tp = m_plugin->mk_numeral(tp);
-    a_tn = m_plugin->mk_numeral(tn);
+        a_tn = m_plugin->mk_numeral(tn);
-    a_tz = m_plugin->mk_numeral(tz);
+        a_tz = m_plugin->mk_numeral(tz);
 
-    expr_ref bv_nte(m), bv_nta(m), bv_tp(m), bv_tn(m), bv_tz(m);
+        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_nte->get_decl(), 0, 0, bv_nte);
-    mk_numeral(a_nta->get_decl(), 0, 0, bv_nta);
+        mk_numeral(a_nta->get_decl(), 0, 0, bv_nta);
-    mk_numeral(a_tp->get_decl(), 0, 0, bv_tp);
+        mk_numeral(a_tp->get_decl(), 0, 0, bv_tp);
-    mk_numeral(a_tn->get_decl(), 0, 0, bv_tn);
+        mk_numeral(a_tn->get_decl(), 0, 0, bv_tn);
-    mk_numeral(a_tz->get_decl(), 0, 0, bv_tz);
+        mk_numeral(a_tz->get_decl(), 0, 0, bv_tz);
 
-    expr_ref c1(m), c2(m), c3(m), c4(m);
+        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));
+        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));
+        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));
+        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));
+        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(c1, bv_tn, bv_tz, result);
-    mk_ite(c2, bv_tp, result, result);
+        mk_ite(c2, bv_tp, result, result);
-    mk_ite(c3, bv_nta, result, result);
+        mk_ite(c3, bv_nta, result, result);
-    mk_ite(c4, bv_nte, 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);
+    expr_ref c1(m), v1(m);
-    c1 = is_zero;
+    c1 = is_zero;    
-    mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
+    v1 = pzero;
-    mk_ite(rm_is_to_neg, nzero, pzero, v1);
 
     // 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);
+    v1 = pzero;
-    mk_ite(rm_is_to_neg, nzero, pzero, v1);
 
     // 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));

src/ast/fpa_decl_plugin.cpp

@@ -879,12 +879,20 @@ void fpa_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
 }
 
 expr * fpa_decl_plugin::get_some_value(sort * s) {
-    SASSERT(s->is_sort_of(m_family_id, FLOATING_POINT_SORT));    
+    if (s->is_sort_of(m_family_id, FLOATING_POINT_SORT)) {
-    mpf tmp;
+        mpf tmp;
-    m_fm.mk_nan(s->get_parameter(0).get_int(), s->get_parameter(1).get_int(), tmp);
+        m_fm.mk_nan(s->get_parameter(0).get_int(), s->get_parameter(1).get_int(), tmp);
-    expr * res = this->mk_numeral(tmp);
+        expr * res = mk_numeral(tmp);
-    m_fm.del(tmp);
+        m_fm.del(tmp);
-    return res;
+        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 {

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
+    if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) {
-    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))),
+        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), 
+                        m().mk_ite(mk_eq_nan(arg2),
-                                   arg1,
+                        arg1,
-                                   m().mk_ite(m_util.mk_lt(arg1, arg2),
+                        m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
-                                           arg1,
+                        m_util.mk_pzero(m().get_sort(arg1)),
-                                           arg2)));
+                        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
+    if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) {
-    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))),
+        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), 
+                        m().mk_ite(mk_eq_nan(arg2),
-                                   arg1,
+                        arg1,
-                                   m().mk_ite(m_util.mk_gt(arg1, arg2),
+                        m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
-                                              arg1,
+                        m_util.mk_pzero(m().get_sort(arg1)),
-                                              arg2)));
+                        m().mk_ite(m_util.mk_gt(arg1, arg2),
+                        arg1,
+                        arg2))));
     return BR_REWRITE_FULL;
 }
 

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<ast> &cnsts, hash_set<ast> &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<ast> &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<iz3mgr::ast> 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++)

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,

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

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 {