merge with master

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

scripts/mk_util.py

@@ -643,7 +643,7 @@ def display_help(exit_code):
 def parse_options():
     global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
     global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
-    global LINUX_X64, SLOW_OPTIMIZE, USE_OMP, PYTHON_INSTALL_ENABLED
+    global LINUX_X64, SLOW_OPTIMIZE, USE_OMP
     try:
         options, remainder = getopt.gnu_getopt(sys.argv[1:],
                                                'b:df:sxhmcvtnp:gj',
@@ -711,29 +711,7 @@ def parse_options():
         else:
             print("ERROR: Invalid command line option '%s'" % opt)
             display_help(1)
-    # Handle the Python package directory
+
-    if IS_WINDOWS:
-        # Installing under Windows doesn't make sense as the install prefix is used
-        # but that doesn't make sense under Windows
-        # CMW: It makes perfectly good sense; the prefix is Python's sys.prefix,
-        # i.e., something along the lines of C:\Python\... At the moment we are not
-        # sure whether we would want to install libz3.dll into that directory though.
-        PYTHON_INSTALL_ENABLED = False
-    else:
-        if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
-            print(("Warning: The detected Python package directory (%s)"
-                   " does not live under the installation prefix (%s)"
-                   ". This would lead to a broken Python installation. "
-                   "Use --pypkgdir= to change the Python package directory") %
-                  (PYTHON_PACKAGE_DIR, PREFIX))
-            if IS_OSX and PYTHON_PACKAGE_DIR.startswith('/Library/'):
-                print("Using hack to install Python bindings, this might lead to a broken system")
-                PYTHON_INSTALL_ENABLED = True
-            else:
-                print("Disabling install of Python bindings")
-                PYTHON_INSTALL_ENABLED = False
-        else:
-            PYTHON_INSTALL_ENABLED = True
 
 # Return a list containing a file names included using '#include' in
 # the given C/C++ file named fname.
@@ -1039,6 +1017,11 @@ class Component:
     def mk_unix_dist(self, build_path, dist_path):
         return
 
+    # Used to print warnings or errors after mk_make.py is done, so that they
+    # are not quite as easy to miss.
+    def final_info(self):
+        pass
+
 class LibComponent(Component):
     def __init__(self, name, path, deps, includes2install):
         Component.__init__(self, name, path, deps)
@@ -1065,8 +1048,8 @@ class LibComponent(Component):
         out.write('\n')
         out.write('%s: %s\n\n' % (self.name, libfile))
 
-    def mk_install_dep(self, out):
+    def mk_install_deps(self, out):
-        out.write('%s' % libfile)
+        return
 
     def mk_install(self, out):
         for include in self.includes2install:
@@ -1154,8 +1137,10 @@ class ExeComponent(Component):
     def main_component(self):
         return self.install
 
-    def mk_install_dep(self, out):
+    def mk_install_deps(self, out):
-        out.write('%s' % exefile)
+        if self.install:
+            exefile = '%s$(EXE_EXT)' % self.exe_name
+            out.write('%s' % exefile)
 
     def mk_install(self, out):
         if self.install:
@@ -1311,7 +1296,7 @@ class DLLComponent(Component):
     def require_def_file(self):
         return IS_WINDOWS and self.export_files
 
-    def mk_install_dep(self, out):
+    def mk_install_deps(self, out):
         out.write('%s$(SO_EXT)' % self.dll_name)
         if self.static:
             out.write(' %s$(LIB_EXT)' % self.dll_name)
@@ -1353,21 +1338,38 @@ class PythonInstallComponent(Component):
         self.pythonPkgDir = None
         self.in_prefix_install = True
         self.libz3Component = libz3Component
-        if not PYTHON_INSTALL_ENABLED:
+
+        if IS_WINDOWS:
+            # Installing under Windows doesn't make sense as the install prefix is used
+            # but that doesn't make sense under Windows
+            # CMW: It makes perfectly good sense; the prefix is Python's sys.prefix,
+            # i.e., something along the lines of C:\Python\... At the moment we are not
+            # sure whether we would want to install libz3.dll into that directory though.
+            PYTHON_INSTALL_ENABLED = False
             return
+        else:
+            PYTHON_INSTALL_ENABLED = True
 
         if IS_WINDOWS or IS_OSX:
             # Use full path that is possibly outside of install prefix
-            self.pythonPkgDir = PYTHON_PACKAGE_DIR
             self.in_prefix_install = PYTHON_PACKAGE_DIR.startswith(PREFIX)
-            assert os.path.isabs(self.pythonPkgDir)
+            self.pythonPkgDir = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
         else:
             # Use path inside the prefix (should be the normal case on Linux)
             # CMW: Also normal on *BSD?
             assert PYTHON_PACKAGE_DIR.startswith(PREFIX)
             self.pythonPkgDir = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
+            self.in_prefix_install = True
+
+        if self.in_prefix_install:
             assert not os.path.isabs(self.pythonPkgDir)
-            assert self.in_prefix_install
+
+    def final_info(self):
+        if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
+            print("Warning: The detected Python package directory (%s) is not "
+                  "in the installation prefix (%s). This can lead to a broken "
+                  "Python API installation. Use --pypkgdir= to change the "
+                  "Python package directory." % (PYTHON_PACKAGE_DIR, PREFIX))
 
     def main_component(self):
         return False    
@@ -2339,12 +2341,12 @@ def mk_makefile():
             out.write(' %s' % c.name)
     out.write('\n\t@echo Z3 was successfully built.\n')
     out.write("\t@echo \"Z3Py scripts can already be executed in the \'%s\' directory.\"\n" % BUILD_DIR)
-    out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be also executed if \'%s\' directory is added to the PYTHONPATH environment variable.\"\n" % BUILD_DIR)
+    out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be executed if the \'%s\' directory is added to the PYTHONPATH environment variable.\"\n" % BUILD_DIR)
     if not IS_WINDOWS:
         out.write("\t@echo Use the following command to install Z3 at prefix $(PREFIX).\n")
         out.write('\t@echo "    sudo make install"\n\n')
-        out.write("\t@echo If you are doing a staged install you can use DESTDIR.\n")
+        # out.write("\t@echo If you are doing a staged install you can use DESTDIR.\n")
-        out.write('\t@echo "    make DESTDIR=/some/temp/directory install"\n')
+        # out.write('\t@echo "    make DESTDIR=/some/temp/directory install"\n')
     # Generate :examples rule
     out.write('examples:')
     for c in get_components():
@@ -2358,6 +2360,8 @@ def mk_makefile():
     if not IS_WINDOWS:
         mk_install(out)
         mk_uninstall(out)
+    for c in get_components():
+        c.final_info()
     out.close()
     # Finalize
     if VERBOSE:
@@ -3473,22 +3477,17 @@ class MakeRuleCmd(object):
 
     @classmethod
     def _install_root(cls, path, in_prefix, out, is_install=True):
-        if in_prefix:
+        if not in_prefix:
-            assert not os.path.isabs(path)
+            # The Python bindings on OSX are sometimes not installed inside the prefix. 
-            install_root = cls.install_root()
-        else:
-            # This hack only exists for the Python bindings on OSX
-            # which are sometimes not installed inside the prefix.
-            # In all other cases installing outside the prefix is
-            # misleading and dangerous!
-            assert IS_OSX
-            assert os.path.isabs(path)
             install_root = "$(DESTDIR)"
             action_string = 'install' if is_install else 'uninstall'
             cls.write_cmd(out, 'echo "WARNING: {}ing files/directories ({}) that are not in the install prefix ($(PREFIX))."'.format(
-                action_string, path))
+                    action_string, path))
-            print("WARNING: Generating makefile rule that {}s {} '{}' which is outside the installation prefix '{}'.".format(
+            #print("WARNING: Generating makefile rule that {}s {} '{}' which is outside the installation prefix '{}'.".format(
-                action_string, 'to' if is_install else 'from', path, PREFIX))
+            #        action_string, 'to' if is_install else 'from', path, PREFIX))
+        else:
+            assert not os.path.isabs(path)
+            install_root = cls.install_root()
         return install_root
 
     @classmethod
@@ -3608,14 +3607,15 @@ class MakeRuleCmd(object):
         out.write("\t@{}\n".format(line))
 
 def strip_path_prefix(path, prefix):
-    assert path.startswith(prefix)
+    if path.startswith(prefix):
-    stripped_path = path[len(prefix):]
+        stripped_path = path[len(prefix):]
-    stripped_path.replace('//','/')
+        stripped_path.replace('//','/')
-    if stripped_path[0] == '/':
+        if stripped_path[0] == '/':
-        stripped_path = stripped_path[1:]
+            stripped_path = stripped_path[1:]
-
+        assert not os.path.isabs(stripped_path)
-    assert not os.path.isabs(stripped_path)
+        return stripped_path
-    return stripped_path
+    else:
+        return path
 
 def configure_file(template_file_path, output_file_path, substitutions):
     """

src/api/api_fpa.cpp

@@ -931,13 +931,21 @@ extern "C" {
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();
         unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
         unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
-        fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
+        family_id fid = mk_c(c)->get_fpa_fid();
-        scoped_mpf val(mpfm);
+        fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
-        if (!plugin->is_numeral(to_expr(t), val)) {
+        SASSERT(plugin != 0);
+        expr * e = to_expr(t);
+        if (!is_app(e) ||
+            is_app_of(e, fid, OP_FPA_NAN) ||
+            is_app_of(e, fid, OP_FPA_PLUS_INF) ||
+            is_app_of(e, fid, OP_FPA_MINUS_INF)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return "";
         }
-        else if (!mpfm.is_regular(val)) {
+        scoped_mpf val(mpfm);
+        app * a = to_app(e);
+        bool r = plugin->is_numeral(e, val);
+        if (!r || !mpfm.is_regular(val)) {
             SET_ERROR_CODE(Z3_INVALID_ARG)
             return "";
         }
@@ -960,16 +968,25 @@ extern "C" {
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();
         unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
-        fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
+        family_id fid = mk_c(c)->get_fpa_fid();
-        scoped_mpf val(mpfm);
+        fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
-        bool r = plugin->is_numeral(to_expr(t), val);
+        SASSERT(plugin != 0);
-        if (!r) {
+        expr * e = to_expr(t);
+        if (!is_app(e) ||
+            is_app_of(e, fid, OP_FPA_NAN) ||
+            is_app_of(e, fid, OP_FPA_PLUS_INF) ||
+            is_app_of(e, fid, OP_FPA_MINUS_INF)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
+            *n = 0;
             return 0;
         }
+        scoped_mpf val(mpfm);
+        app * a = to_app(e);
+        bool r = plugin->is_numeral(e, val);
         const mpz & z = mpfm.sig(val);
-        if (!mpzm.is_uint64(z)) {
+        if (!r || mpfm.is_regular(val)|| !mpzm.is_uint64(z)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
+            *n = 0;
             return 0;
         }
         *n = mpzm.get_uint64(z);
@@ -983,15 +1000,22 @@ extern "C" {
         RESET_ERROR_CODE();
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();
+        family_id fid = mk_c(c)->get_fpa_fid();
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
-        scoped_mpf val(mpfm);
+        SASSERT(plugin != 0);
-        bool r = plugin->is_numeral(to_expr(t), val);
+        expr * e = to_expr(t);
-        if (!r) {
+        if (!is_app(e) ||
+            is_app_of(e, fid, OP_FPA_NAN) ||
+            is_app_of(e, fid, OP_FPA_PLUS_INF) ||
+            is_app_of(e, fid, OP_FPA_MINUS_INF)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return "";
         }
-        else if (!mpfm.is_normal(val) && !mpfm.is_denormal(val)) {
+        scoped_mpf val(mpfm);
-            SET_ERROR_CODE(Z3_INVALID_ARG)
+        app * a = to_app(e);
+        bool r = plugin->is_numeral(e, val);
+        if (!r || !mpfm.is_regular(val)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
             return "";
         }
         mpf_exp_t exp = mpfm.exp_normalized(val);
@@ -1007,11 +1031,24 @@ extern "C" {
         RESET_ERROR_CODE();
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();
+        family_id fid = mk_c(c)->get_fpa_fid();
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
-        scoped_mpf val(mpfm);
+        SASSERT(plugin != 0);
-        bool r = plugin->is_numeral(to_expr(t), val);
+        expr * e = to_expr(t);
-        if (!r) {
+        if (!is_app(e) ||
+            is_app_of(e, fid, OP_FPA_NAN) ||
+            is_app_of(e, fid, OP_FPA_PLUS_INF) ||
+            is_app_of(e, fid, OP_FPA_MINUS_INF)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
+            *n = 0;
+            return 0;
+        }
+        scoped_mpf val(mpfm);
+        app * a = to_app(e);
+        bool r = plugin->is_numeral(e, val);
+        if (!r || !mpfm.is_regular(val)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            *n = 0;
             return 0;
         }
         *n = mpfm.exp(val);

src/api/python/z3.py

@@ -8352,20 +8352,36 @@ def FPSort(ebits, sbits, ctx=None):
     ctx = z3._get_ctx(ctx)
     return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)
 
-def _to_float_str(val):
+def _to_float_str(val, exp=0):
     if isinstance(val, float):
-        return str(val)
+        v = val.as_integer_ratio()
+        num = v[0]
+        den = v[1]
+        rvs = str(num) + '/' + str(den)
+        res = rvs + 'p' + _to_int_str(exp)
     elif isinstance(val, bool):
         if val:
-            return "1.0"
+            res = "1.0"
         else:
-            return "0.0"
+            res = "0.0"
     elif _is_int(val):
-        return str(val)
+        res = str(val)
     elif isinstance(val, str):
-        return val
+        inx = val.find('*(2**')
-    if __debug__:
+        if inx == -1:
-        _z3_assert(False, "Python value cannot be used as a double")
+            res = val
+        elif val[-1] == ')':
+            res = val[0:inx]
+            exp = str(int(val[inx+5:-1]) + int(exp))
+        else:
+            _z3_assert(False, "String does not have floating-point numeral form.")
+    elif __debug__:
+        _z3_assert(False, "Python value cannot be used to create floating-point numerals.")
+    if exp == 0:
+        return res
+    else:
+        return res + 'p' + exp
+
 
 def fpNaN(s):
     _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
@@ -8422,8 +8438,6 @@ def FPVal(sig, exp=None, fps=None, ctx=None):
     if exp == None:
         exp = 0    
     val = _to_float_str(sig)
-    val = val + 'p'
-    val = val + _to_int_str(exp)
     return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
 
 def FP(name, fpsort, ctx=None):

src/ast/expr_abstract.cpp

@@ -49,6 +49,7 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const*
         case AST_APP: {
             app* a = to_app(curr);
             bool all_visited = true;
+            bool changed = false;
             m_args.reset();
             for (unsigned i = 0; i < a->get_num_args(); ++i) {
                 if (!m_map.find(a->get_arg(i), b)) {
@@ -56,12 +57,17 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const*
                     all_visited = false;
                 }
                 else {
+                    changed |= b != a->get_arg(i);
                     m_args.push_back(b);
                 }
             }
             if (all_visited) {
-                b = m.mk_app(a->get_decl(), m_args.size(), m_args.c_ptr());
+                if (changed) {
-                m_pinned.push_back(b);
+                    b = m.mk_app(a->get_decl(), m_args.size(), m_args.c_ptr());
+                    m_pinned.push_back(b);
+                } else {
+                    b = curr;
+                }
                 m_map.insert(curr, b);
                 m_stack.pop_back();
             }

src/ast/fpa_decl_plugin.cpp

@@ -39,7 +39,7 @@ void fpa_decl_plugin::set_manager(ast_manager * m, family_id id) {
     m_int_sort = m_manager->mk_sort(m_arith_fid, INT_SORT);
     SASSERT(m_int_sort != 0); // arith_decl_plugin must be installed before fpa_decl_plugin.
     m_manager->inc_ref(m_int_sort);
-    
+
     // BV is not optional anymore.
     SASSERT(m_manager->has_plugin(symbol("bv")));
     m_bv_fid = m_manager->mk_family_id("bv");
@@ -69,28 +69,30 @@ void fpa_decl_plugin::recycled_id(unsigned id) {
 }
 
 func_decl * fpa_decl_plugin::mk_numeral_decl(mpf const & v) {
-    parameter p(mk_id(v), true);
-    SASSERT(p.is_external());
     sort * s = mk_float_sort(v.get_ebits(), v.get_sbits());
-    return m_manager->mk_const_decl(symbol("fp.numeral"),  s, func_decl_info(m_family_id, OP_FPA_NUM, 1, &p));
+    func_decl * r = 0;
+    if (m_fm.is_nan(v))
+        r = m_manager->mk_const_decl(symbol("NaN"), s, func_decl_info(m_family_id, OP_FPA_NAN));
+    else if (m_fm.is_pinf(v))
+        r = m_manager->mk_const_decl(symbol("+oo"), s, func_decl_info(m_family_id, OP_FPA_PLUS_INF));
+    else if (m_fm.is_ninf(v))
+        r = m_manager->mk_const_decl(symbol("-oo"), s, func_decl_info(m_family_id, OP_FPA_MINUS_INF));
+    else if (m_fm.is_pzero(v))
+        r = m_manager->mk_const_decl(symbol("+zero"), s, func_decl_info(m_family_id, OP_FPA_PLUS_ZERO));
+    else if (m_fm.is_nzero(v))
+        r = m_manager->mk_const_decl(symbol("-zero"), s, func_decl_info(m_family_id, OP_FPA_MINUS_ZERO));
+    else {
+        SASSERT(m_fm.is_regular(v));
+        parameter p(mk_id(v), true);
+        SASSERT(p.is_external());
+        sort * s = mk_float_sort(v.get_ebits(), v.get_sbits());
+        r = m_manager->mk_const_decl(symbol("fp.numeral"), s, func_decl_info(m_family_id, OP_FPA_NUM, 1, &p));
+    }
+    return r;
 }
 
 app * fpa_decl_plugin::mk_numeral(mpf const & v) {
-    sort * s = mk_float_sort(v.get_ebits(), v.get_sbits());
+    return m_manager->mk_const(mk_numeral_decl(v));
-    func_decl * d;
-    if (m_fm.is_nan(v))
-        d = m_manager->mk_const_decl(symbol("NaN"), s, func_decl_info(m_family_id, OP_FPA_NAN));
-    else if (m_fm.is_pinf(v))
-        d = m_manager->mk_const_decl(symbol("+oo"), s, func_decl_info(m_family_id, OP_FPA_PLUS_INF));
-    else if (m_fm.is_ninf(v))
-        d = m_manager->mk_const_decl(symbol("-oo"), s, func_decl_info(m_family_id, OP_FPA_MINUS_INF));
-    else if (m_fm.is_pzero(v))
-        d = m_manager->mk_const_decl(symbol("+zero"), s, func_decl_info(m_family_id, OP_FPA_PLUS_ZERO));
-    else if (m_fm.is_nzero(v))
-        d = m_manager->mk_const_decl(symbol("-zero"), s, func_decl_info(m_family_id, OP_FPA_MINUS_ZERO));
-    else
-        d = mk_numeral_decl(v);
-    return m_manager->mk_const(d);
 }
 
 bool fpa_decl_plugin::is_numeral(expr * n, mpf & val) {
@@ -161,9 +163,9 @@ bool fpa_decl_plugin::is_rm_numeral(expr * n, mpf_rounding_mode & val) {
     return 0;
 }
 
-bool fpa_decl_plugin::is_rm_numeral(expr * n) { 
+bool fpa_decl_plugin::is_rm_numeral(expr * n) {
-    mpf_rounding_mode t; 
+    mpf_rounding_mode t;
-    return is_rm_numeral(n, t); 
+    return is_rm_numeral(n, t);
 }
 
 void fpa_decl_plugin::del(parameter const & p) {
@@ -182,8 +184,8 @@ void fpa_decl_plugin::finalize() {
     if (m_int_sort)  { m_manager->dec_ref(m_int_sort); }
 }
 
-decl_plugin * fpa_decl_plugin::mk_fresh() { 
+decl_plugin * fpa_decl_plugin::mk_fresh() {
-    return alloc(fpa_decl_plugin); 
+    return alloc(fpa_decl_plugin);
 }
 
 sort * fpa_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) {
@@ -268,7 +270,7 @@ func_decl * fpa_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_param
     }
 
     SASSERT(is_sort_of(s, m_family_id, FLOATING_POINT_SORT));
-    
+
     unsigned ebits = s->get_parameter(0).get_int();
     unsigned sbits = s->get_parameter(1).get_int();
     scoped_mpf val(m_fm);
@@ -297,9 +299,9 @@ func_decl * fpa_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_parameter
     switch (k) {
     case OP_FPA_EQ: name = "fp.eq";  break;
     case OP_FPA_LT: name = "fp.lt";   break;
-    case OP_FPA_GT: name = "fp.gt";   break;        
+    case OP_FPA_GT: name = "fp.gt";   break;
-    case OP_FPA_LE: name = "fp.leq";  break;        
+    case OP_FPA_LE: name = "fp.leq";  break;
-    case OP_FPA_GE: name = "fp.geq";  break;        
+    case OP_FPA_GE: name = "fp.geq";  break;
     default:
         UNREACHABLE();
         break;
@@ -336,7 +338,7 @@ func_decl * fpa_decl_plugin::mk_unary_decl(decl_kind k, unsigned num_parameters,
     if (arity != 1)
         m_manager->raise_exception("invalid number of arguments to floating point operator");
     if (!is_float_sort(domain[0]))
-        m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort"); 
+        m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort");
     symbol name;
     switch (k) {
     case OP_FPA_ABS: name = "fp.abs"; break;
@@ -353,7 +355,7 @@ func_decl * fpa_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_parameters
     if (arity != 2)
         m_manager->raise_exception("invalid number of arguments to floating point operator");
     if (domain[0] != domain[1] || !is_float_sort(domain[0]))
-        m_manager->raise_exception("sort mismatch, expected arguments of equal FloatingPoint sorts"); 
+        m_manager->raise_exception("sort mismatch, expected arguments of equal FloatingPoint sorts");
     symbol name;
     switch (k) {
     case OP_FPA_REM: name = "fp.rem"; break;
@@ -377,7 +379,7 @@ func_decl * fpa_decl_plugin::mk_rm_binary_decl(decl_kind k, unsigned num_paramet
     if (!is_rm_sort(domain[0]))
         m_manager->raise_exception("sort mismatch, expected first argument of RoundingMode sort");
     if (domain[1] != domain[2] || !is_float_sort(domain[1]))
-        m_manager->raise_exception("sort mismatch, expected arguments 1 and 2 of equal FloatingPoint sorts"); 
+        m_manager->raise_exception("sort mismatch, expected arguments 1 and 2 of equal FloatingPoint sorts");
     symbol name;
     switch (k) {
     case OP_FPA_ADD: name = "fp.add";   break;
@@ -398,7 +400,7 @@ func_decl * fpa_decl_plugin::mk_rm_unary_decl(decl_kind k, unsigned num_paramete
     if (!is_rm_sort(domain[0]))
         m_manager->raise_exception("sort mismatch, expected RoundingMode as first argument");
     if (!is_float_sort(domain[1]))
-        m_manager->raise_exception("sort mismatch, expected FloatingPoint as second argument"); 
+        m_manager->raise_exception("sort mismatch, expected FloatingPoint as second argument");
     symbol name;
     switch (k) {
     case OP_FPA_SQRT: name = "fp.sqrt";   break;
@@ -423,8 +425,8 @@ func_decl * fpa_decl_plugin::mk_fma(decl_kind k, unsigned num_parameters, parame
 }
 
 func_decl * fpa_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, parameter const * parameters,
-                                        unsigned arity, sort * const * domain, sort * range) {    
+                                        unsigned arity, sort * const * domain, sort * range) {
-    if (m_bv_plugin && arity == 3 && 
+    if (m_bv_plugin && arity == 3 &&
         is_sort_of(domain[0], m_bv_fid, BV_SORT) &&
         is_sort_of(domain[1], m_bv_fid, BV_SORT) &&
         is_sort_of(domain[2], m_bv_fid, BV_SORT)) {
@@ -445,7 +447,7 @@ func_decl * fpa_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, para
 
         int ebits = parameters[0].get_int();
         int sbits = parameters[1].get_int();
-        
+
         if (domain[0]->get_parameter(0).get_int() != (ebits + sbits))
             m_manager->raise_exception("sort mismatch; invalid bit-vector size, expected bitvector of size (ebits+sbits)");
 
@@ -453,7 +455,7 @@ func_decl * fpa_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, para
         symbol name("to_fp");
         return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
     }
-    else if (m_bv_plugin && arity == 2 && 
+    else if (m_bv_plugin && arity == 2 &&
              is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
              is_sort_of(domain[1], m_bv_fid, BV_SORT)) {
         // RoundingMode + 1 BV -> 1 FP
@@ -477,16 +479,16 @@ func_decl * fpa_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, para
         if (!parameters[0].is_int() || !parameters[1].is_int())
             m_manager->raise_exception("invalid parameter type to to_fp");
         int ebits = parameters[0].get_int();
-        int sbits = parameters[1].get_int();        
+        int sbits = parameters[1].get_int();
         if (!is_rm_sort(domain[0]))
             m_manager->raise_exception("sort mismatch, expected first argument of RoundingMode sort");
         if (!is_sort_of(domain[1], m_family_id, FLOATING_POINT_SORT))
             m_manager->raise_exception("sort mismatch, expected second argument of FloatingPoint sort");
-        
+
         sort * fp = mk_float_sort(ebits, sbits);
         symbol name("to_fp");
         return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
-    }    
+    }
     else if (arity == 3 &&
              is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
              is_sort_of(domain[1], m_arith_fid, REAL_SORT) &&
@@ -494,7 +496,7 @@ func_decl * fpa_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, para
     {
         // Rounding + 1 Real + 1 Int -> 1 FP
         if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
-            m_manager->raise_exception("expecting two integer parameters to to_fp");                
+            m_manager->raise_exception("expecting two integer parameters to to_fp");
 
         sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
         symbol name("to_fp");
@@ -561,13 +563,13 @@ func_decl * fpa_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_paramet
         m_manager->raise_exception("sort mismatch, expected first argument of RoundingMode sort");
     if (!is_sort_of(domain[1], m_bv_fid, BV_SORT))
         m_manager->raise_exception("sort mismatch, expected second argument of bit-vector sort");
-    
+
     // RoundingMode + 1 BV -> 1 FP
     if (num_parameters != 2)
         m_manager->raise_exception("invalid number of parameters to to_fp_unsigned");
     if (!parameters[0].is_int() || !parameters[1].is_int())
         m_manager->raise_exception("invalid parameter type to to_fp_unsigned");
-    
+
     int ebits = parameters[0].get_int();
     int sbits = parameters[1].get_int();
 
@@ -579,16 +581,16 @@ func_decl * fpa_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_paramet
 func_decl * fpa_decl_plugin::mk_fp(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                      unsigned arity, sort * const * domain, sort * range) {
     if (arity != 3)
-        m_manager->raise_exception("invalid number of arguments to fp");    
+        m_manager->raise_exception("invalid number of arguments to fp");
-    if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) || 
+    if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) ||
         (domain[0]->get_parameter(0).get_int() != 1) ||
         !is_sort_of(domain[1], m_bv_fid, BV_SORT) ||
         !is_sort_of(domain[2], m_bv_fid, BV_SORT))
         m_manager->raise_exception("sort mismatch, expected three bit-vectors, the first one of size 1.");
-    
+
     int eb = (domain[1])->get_parameter(0).get_int();
     int sb = (domain[2])->get_parameter(0).get_int() + 1;
-    symbol name("fp");    
+    symbol name("fp");
     sort * fp = mk_float_sort(eb, sb);
     return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k));
 }
@@ -636,12 +638,12 @@ func_decl * fpa_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, par
 }
 
 func_decl * fpa_decl_plugin::mk_to_real(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 fp.to_real");
     if (!is_float_sort(domain[0]))
         m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort");
-    
+
     symbol name("fp.to_real");
     return m_manager->mk_func_decl(name, 1, domain, m_real_sort, func_decl_info(m_family_id, k));
 }
@@ -668,7 +670,7 @@ func_decl * fpa_decl_plugin::mk_internal_rm(decl_kind k, unsigned num_parameters
         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));
@@ -688,7 +690,7 @@ func_decl * fpa_decl_plugin::mk_internal_bv_wrap(decl_kind k, unsigned num_param
         sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps);
         return m_manager->mk_func_decl(symbol("bv_wrap"), 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
     }
-    else {        
+    else {
         parameter ps[] = { parameter(3) };
         sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps);
         return m_manager->mk_func_decl(symbol("bv_wrap"), 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
@@ -698,12 +700,12 @@ func_decl * fpa_decl_plugin::mk_internal_bv_wrap(decl_kind k, unsigned num_param
 func_decl * fpa_decl_plugin::mk_internal_bv_unwrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                                      unsigned arity, sort * const * domain, sort * range) {
     if (arity != 1)
-        m_manager->raise_exception("invalid number of arguments to internal_bv_unwrap");    
+        m_manager->raise_exception("invalid number of arguments to internal_bv_unwrap");
     if (!is_sort_of(domain[0], m_bv_fid, BV_SORT))
         m_manager->raise_exception("sort mismatch, expected argument of bitvector sort");
     if (!is_float_sort(range) && !is_rm_sort(range))
         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));
 }
 
@@ -716,7 +718,7 @@ func_decl * fpa_decl_plugin::mk_internal_to_ubv_unspecified(
         m_manager->raise_exception("invalid number of parameters to fp.to_ubv_unspecified; expecting 1");
     if (!parameters[0].is_int())
         m_manager->raise_exception("invalid parameters type provided to fp.to_ubv_unspecified; expecting an integer");
-        
+
     sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, parameters);
     return m_manager->mk_func_decl(symbol("fp.to_ubv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
 }
@@ -748,7 +750,7 @@ func_decl * fpa_decl_plugin::mk_internal_to_real_unspecified(
 
 func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                             unsigned arity, sort * const * domain, sort * range) {
-    switch (k) {    
+    switch (k) {
     case OP_FPA_MINUS_INF:
     case OP_FPA_PLUS_INF:
     case OP_FPA_NAN:
@@ -768,14 +770,14 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_FPA_GE:
         return mk_bin_rel_decl(k, num_parameters, parameters, arity, domain, range);
     case OP_FPA_IS_ZERO:
-    case OP_FPA_IS_NEGATIVE: 
+    case OP_FPA_IS_NEGATIVE:
     case OP_FPA_IS_POSITIVE:
     case OP_FPA_IS_NAN:
     case OP_FPA_IS_INF:
     case OP_FPA_IS_NORMAL:
     case OP_FPA_IS_SUBNORMAL:
         return mk_unary_rel_decl(k, num_parameters, parameters, arity, domain, range);
-    case OP_FPA_ABS: 
+    case OP_FPA_ABS:
     case OP_FPA_NEG:
         return mk_unary_decl(k, num_parameters, parameters, arity, domain, range);
     case OP_FPA_REM:
@@ -787,7 +789,7 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_FPA_DIV:
         return mk_rm_binary_decl(k, num_parameters, parameters, arity, domain, range);
     case OP_FPA_SUB:
-        if (arity == 1) 
+        if (arity == 1)
             return mk_unary_decl(OP_FPA_NEG, num_parameters, parameters, arity, domain, range);
         else
             return mk_rm_binary_decl(k, num_parameters, parameters, arity, domain, range);
@@ -797,7 +799,7 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_FPA_FMA:
         return mk_fma(k, num_parameters, parameters, arity, domain, range);
     case OP_FPA_FP:
-        return mk_fp(k, num_parameters, parameters, arity, domain, range);    
+        return mk_fp(k, num_parameters, parameters, arity, domain, range);
     case OP_FPA_TO_UBV:
         return mk_to_ubv(k, num_parameters, parameters, arity, domain, range);
     case OP_FPA_TO_SBV:
@@ -817,13 +819,13 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         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:
     case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
         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:
@@ -857,19 +859,19 @@ void fpa_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
     op_names.push_back(builtin_name("RTZ", OP_FPA_RM_TOWARD_ZERO));
 
     op_names.push_back(builtin_name("fp.abs", OP_FPA_ABS));
-    op_names.push_back(builtin_name("fp.neg", OP_FPA_NEG)); 
+    op_names.push_back(builtin_name("fp.neg", OP_FPA_NEG));
-    op_names.push_back(builtin_name("fp.add", OP_FPA_ADD)); 
+    op_names.push_back(builtin_name("fp.add", OP_FPA_ADD));
-    op_names.push_back(builtin_name("fp.sub", OP_FPA_SUB));     
+    op_names.push_back(builtin_name("fp.sub", OP_FPA_SUB));
-    op_names.push_back(builtin_name("fp.mul", OP_FPA_MUL)); 
+    op_names.push_back(builtin_name("fp.mul", OP_FPA_MUL));
     op_names.push_back(builtin_name("fp.div", OP_FPA_DIV));
-    op_names.push_back(builtin_name("fp.fma", OP_FPA_FMA)); 
+    op_names.push_back(builtin_name("fp.fma", OP_FPA_FMA));
-    op_names.push_back(builtin_name("fp.sqrt", OP_FPA_SQRT)); 
+    op_names.push_back(builtin_name("fp.sqrt", OP_FPA_SQRT));
     op_names.push_back(builtin_name("fp.rem", OP_FPA_REM));
     op_names.push_back(builtin_name("fp.roundToIntegral", OP_FPA_ROUND_TO_INTEGRAL));
     op_names.push_back(builtin_name("fp.min", OP_FPA_MIN));
-    op_names.push_back(builtin_name("fp.max", OP_FPA_MAX));      
+    op_names.push_back(builtin_name("fp.max", OP_FPA_MAX));
     op_names.push_back(builtin_name("fp.leq", OP_FPA_LE));
-    op_names.push_back(builtin_name("fp.lt",  OP_FPA_LT));    
+    op_names.push_back(builtin_name("fp.lt",  OP_FPA_LT));
     op_names.push_back(builtin_name("fp.geq", OP_FPA_GE));
     op_names.push_back(builtin_name("fp.gt",  OP_FPA_GT));
     op_names.push_back(builtin_name("fp.eq", OP_FPA_EQ));
@@ -880,13 +882,13 @@ void fpa_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
     op_names.push_back(builtin_name("fp.isInfinite", OP_FPA_IS_INF));
     op_names.push_back(builtin_name("fp.isNaN", OP_FPA_IS_NAN));
     op_names.push_back(builtin_name("fp.isNegative", OP_FPA_IS_NEGATIVE));
-    op_names.push_back(builtin_name("fp.isPositive", OP_FPA_IS_POSITIVE));    
+    op_names.push_back(builtin_name("fp.isPositive", OP_FPA_IS_POSITIVE));
 
     op_names.push_back(builtin_name("fp", OP_FPA_FP));
     op_names.push_back(builtin_name("fp.to_ubv", OP_FPA_TO_UBV));
     op_names.push_back(builtin_name("fp.to_sbv", OP_FPA_TO_SBV));
     op_names.push_back(builtin_name("fp.to_real", OP_FPA_TO_REAL));
-   
+
     op_names.push_back(builtin_name("to_fp", OP_FPA_TO_FP));
     op_names.push_back(builtin_name("to_fp_unsigned", OP_FPA_TO_FP_UNSIGNED));
 
@@ -917,13 +919,13 @@ expr * fpa_decl_plugin::get_some_value(sort * s) {
         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 {
-    if (e->get_family_id() != m_family_id) 
+    if (e->get_family_id() != m_family_id)
         return false;
     switch (e->get_decl_kind()) {
     case OP_FPA_RM_NEAREST_TIES_TO_EVEN:
@@ -956,7 +958,7 @@ bool fpa_decl_plugin::is_unique_value(app* e) const {
     case OP_FPA_RM_TOWARD_POSITIVE:
     case OP_FPA_RM_TOWARD_NEGATIVE:
     case OP_FPA_RM_TOWARD_ZERO:
-        return true;    
+        return true;
     case OP_FPA_PLUS_INF:  /* No; +oo == fp(#b0 #b11 #b00) */
     case OP_FPA_MINUS_INF: /* No; -oo == fp #b1 #b11 #b00) */
     case OP_FPA_PLUS_ZERO: /* No; +zero == fp #b0 #b00 #b000) */
@@ -1029,7 +1031,7 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) {
     return mk_value(v);
 }
 
-app * fpa_util::mk_internal_to_ubv_unspecified(unsigned width) {    
+app * fpa_util::mk_internal_to_ubv_unspecified(unsigned width) {
     parameter ps[] = { parameter(width) };
     sort * range = m_bv_util.mk_sort(width);
     return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, 1, ps, 0, 0, range);

src/ast/rewriter/fpa_rewriter.cpp

@@ -764,7 +764,6 @@ br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref &
         bu.is_numeral(arg3, r3, bvs3)) {
         SASSERT(mpzm.is_one(r2.to_mpq().denominator()));
         SASSERT(mpzm.is_one(r3.to_mpq().denominator()));
-        SASSERT(mpzm.is_int64(r3.to_mpq().numerator()));
         scoped_mpf v(m_fm);
         mpf_exp_t biased_exp = mpzm.get_int64(r2.to_mpq().numerator());
         m_fm.set(v, bvs2, bvs3 + 1,

src/interp/iz3interp.cpp

@@ -26,7 +26,6 @@
 #pragma warning(disable:4101)
 #endif
 
-#include <assert.h>
 #include <algorithm>
 #include <stdio.h>
 #include <fstream>

src/interp/iz3translate.cpp

@@ -2023,8 +2023,8 @@ public:
                 break;
             }
             default:
-                pfgoto(proof);
+                pfgoto(proof);                
-                assert(0 && "translate_main: unsupported proof rule");
+                SASSERT(0 && "translate_main: unsupported proof rule");
                 throw unsupported();
             }
         }

src/muz/rel/dl_mk_simple_joins.cpp

@@ -11,7 +11,7 @@ Abstract:
 
 Author:
 
-    Leonardo de Moura (leonardo) 2010-05-20.
+    Krystof Hoder 2010-05-20.
 
 Revision History:
 
@@ -302,14 +302,10 @@ namespace datalog {
 
         }
 
-        pair_info & get_pair(app_pair key) const {
-            return *m_costs.find(key);
-        }
-
         void remove_rule_from_pair(app_pair key, rule * r, unsigned original_len) {
-            std::cout << "remove: " << mk_pp(key.first, m) << " - " << mk_pp(key.second, m) << "\n";
+            pair_info * ptr = 0;
-            pair_info * ptr = &get_pair(key);
+            if (m_costs.find(key, ptr) && ptr &&
-            if (ptr->remove_rule(r, original_len)) {
+                ptr->remove_rule(r, original_len)) {
                 SASSERT(ptr->m_rules.empty());
                 m_costs.remove(key);
                 dealloc(ptr);
@@ -364,7 +360,12 @@ namespace datalog {
         void join_pair(app_pair pair_key) {
             app * t1 = pair_key.first;
             app * t2 = pair_key.second;
-            pair_info & inf = get_pair(pair_key);
+            pair_info* infp = 0;
+            if (!m_costs.find(pair_key, infp) || !infp) {
+                UNREACHABLE();
+                return;
+            }            
+            pair_info & inf = *infp;
             SASSERT(!inf.m_rules.empty());
             var_idx_set & output_vars = inf.m_all_nonlocal_vars;
             expr_ref_vector args(m);

src/shell/smtlib_frontend.cpp

@@ -33,7 +33,6 @@ Revision History:
 #include"smt_solver.h"
 
 extern bool g_display_statistics;
-extern void display_config();
 static clock_t             g_start_time;
 static smtlib::solver*     g_solver      = 0;
 static cmd_context *       g_cmd_context = 0;