Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/api/dotnet/Solver.cs

@@ -210,7 +210,7 @@ namespace Microsoft.Z3
         public Status Check(params Expr[] assumptions)
         {
             Z3_lbool r;
-            if (assumptions == null)
+            if (assumptions == null || assumptions.Length == 0)
                 r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
             else
                 r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));

src/ast/float_decl_plugin.cpp

@@ -255,7 +255,11 @@ func_decl * float_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_param
     case OP_FLOAT_IS_ZERO: name = "isZero";  break;
     case OP_FLOAT_IS_NZERO: name = "isNZero";   break;
     case OP_FLOAT_IS_PZERO: name = "isPZero";   break;        
-    case OP_FLOAT_IS_SIGN_MINUS: name = "isSignMinus";  break;        
+    case OP_FLOAT_IS_SIGN_MINUS: name = "isSignMinus";  break;
+    case OP_FLOAT_IS_NAN: name = "isNaN";  break;
+    case OP_FLOAT_IS_INF: name = "isInfinite";  break;
+    case OP_FLOAT_IS_NORMAL: name = "isNormal";  break;
+    case OP_FLOAT_IS_SUBNORMAL: name = "isSubnormal";  break;
     default:
         UNREACHABLE();
         break;
@@ -415,6 +419,10 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
     case OP_FLOAT_IS_NZERO:
     case OP_FLOAT_IS_PZERO:
     case OP_FLOAT_IS_SIGN_MINUS: 
+    case OP_FLOAT_IS_NAN:
+    case OP_FLOAT_IS_INF:
+    case OP_FLOAT_IS_NORMAL:
+    case OP_FLOAT_IS_SUBNORMAL:
         return mk_unary_rel_decl(k, num_parameters, parameters, arity, domain, range);
     case OP_FLOAT_ABS: 
     case OP_FLOAT_UMINUS:
@@ -473,9 +481,13 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
     op_names.push_back(builtin_name("<=", OP_FLOAT_LE));
     op_names.push_back(builtin_name(">=", OP_FLOAT_GE));
 
+    op_names.push_back(builtin_name("isNaN", OP_FLOAT_IS_NAN));
+    op_names.push_back(builtin_name("isInfinite", OP_FLOAT_IS_INF));
     op_names.push_back(builtin_name("isZero", OP_FLOAT_IS_ZERO));
     op_names.push_back(builtin_name("isNZero", OP_FLOAT_IS_NZERO));
     op_names.push_back(builtin_name("isPZero", OP_FLOAT_IS_PZERO));
+    op_names.push_back(builtin_name("isNormal", OP_FLOAT_IS_NORMAL));
+    op_names.push_back(builtin_name("isSubnormal", OP_FLOAT_IS_SUBNORMAL));
     op_names.push_back(builtin_name("isSignMinus", OP_FLOAT_IS_SIGN_MINUS));
 
     op_names.push_back(builtin_name("min", OP_FLOAT_MIN));

src/ast/float_decl_plugin.h

@@ -61,9 +61,13 @@ enum float_op_kind {
     OP_FLOAT_GT,
     OP_FLOAT_LE,
     OP_FLOAT_GE,
+    OP_FLOAT_IS_NAN,
+    OP_FLOAT_IS_INF,
     OP_FLOAT_IS_ZERO,
-    OP_FLOAT_IS_NZERO,
+    OP_FLOAT_IS_NORMAL,
+    OP_FLOAT_IS_SUBNORMAL,    
     OP_FLOAT_IS_PZERO,
+    OP_FLOAT_IS_NZERO,
     OP_FLOAT_IS_SIGN_MINUS,
 
     OP_TO_FLOAT,
@@ -223,7 +227,7 @@ public:
     app * mk_rem(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_REM, arg1, arg2); }
     app * mk_max(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MAX, arg1, arg2); }
     app * mk_min(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MIN, arg1, arg2); }
-    app * mk_abs(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_ABS, arg1, arg2); }
+    app * mk_abs(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_ABS, arg1); }
     app * mk_sqrt(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_SQRT, arg1, arg2); }
     app * mk_round(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_ROUND_TO_INTEGRAL, arg1, arg2); }
     app * mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4) {
@@ -237,7 +241,11 @@ public:
     app * mk_le(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_LE, arg1, arg2); }
     app * mk_ge(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_GE, arg1, arg2); }
 
+    app * mk_is_nan(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NAN, arg1); }
+    app * mk_is_inf(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_INF, arg1); }
     app * mk_is_zero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_ZERO, arg1); }
+    app * mk_is_normal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NORMAL, arg1); }
+    app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SUBNORMAL, arg1); }
     app * mk_is_nzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NZERO, arg1); }
     app * mk_is_pzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_PZERO, arg1); }
     app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SIGN_MINUS, arg1); }

src/ast/rewriter/float_rewriter.cpp

@@ -58,6 +58,10 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
     case OP_FLOAT_IS_ZERO:   SASSERT(num_args == 1); st = mk_is_zero(args[0], result); break;
     case OP_FLOAT_IS_NZERO:  SASSERT(num_args == 1); st = mk_is_nzero(args[0], result); break;
     case OP_FLOAT_IS_PZERO:  SASSERT(num_args == 1); st = mk_is_pzero(args[0], result); break;
+    case OP_FLOAT_IS_NAN:    SASSERT(num_args == 1); st = mk_is_nan(args[0], result); break;
+    case OP_FLOAT_IS_INF:    SASSERT(num_args == 1); st = mk_is_inf(args[0], result); break;
+    case OP_FLOAT_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break;
+    case OP_FLOAT_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break;
     case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break;
     case OP_TO_IEEE_BV:      SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break;
     }
@@ -79,17 +83,21 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
         rational q;
         mpf q_mpf;
         if (m_util.au().is_numeral(args[1], q)) {        
+            TRACE("fp_rewriter", tout << "q: " << q << std::endl; );
             mpf v;
             m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
             result = m_util.mk_value(v);
-            m_util.fm().del(v);            
+            m_util.fm().del(v);
+            TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
             return BR_DONE;
         }
-        else if (m_util.is_value(args[1], q_mpf)) {            
+        else if (m_util.is_value(args[1], q_mpf)) {
+            TRACE("fp_rewriter", tout << "q: " << m_util.fm().to_string(q_mpf) << std::endl; );
             mpf v;
             m_util.fm().set(v, ebits, sbits, rm, q_mpf);
             result = m_util.mk_value(v);
             m_util.fm().del(v);
+            TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
             return BR_DONE;
         }
         else 
@@ -113,11 +121,11 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
             return BR_FAILED;
 
         TRACE("fp_rewriter", tout << "q: " << q << ", e: " << e << "\n";);
-
         mpf v;
 	    m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator());
         result = m_util.mk_value(v);
-        m_util.fm().del(v);
+        m_util.fm().del(v);        
+        TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
         return BR_DONE;
     }
     else {
@@ -428,6 +436,46 @@ br_status float_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) {
     return BR_FAILED;
 }
 
+br_status float_rewriter::mk_is_nan(expr * arg1, expr_ref & result) {
+    scoped_mpf v(m_util.fm());
+    if (m_util.is_value(arg1, v)) {
+        result = (m_util.fm().is_nan(v)) ? m().mk_true() : m().mk_false();
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_is_inf(expr * arg1, expr_ref & result) {
+    scoped_mpf v(m_util.fm());
+    if (m_util.is_value(arg1, v)) {
+        result = (m_util.fm().is_inf(v)) ? m().mk_true() : m().mk_false();
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_is_normal(expr * arg1, expr_ref & result) {
+    scoped_mpf v(m_util.fm());
+    if (m_util.is_value(arg1, v)) {
+        result = (m_util.fm().is_normal(v)) ? m().mk_true() : m().mk_false();
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) {
+    scoped_mpf v(m_util.fm());
+    if (m_util.is_value(arg1, v)) {
+        result = (m_util.fm().is_denormal(v)) ? m().mk_true() : m().mk_false();
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
 br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) {
     scoped_mpf v(m_util.fm());
     if (m_util.is_value(arg1, v)) {

src/ast/rewriter/float_rewriter.h

@@ -66,6 +66,10 @@ public:
     br_status mk_is_zero(expr * arg1, expr_ref & result);
     br_status mk_is_nzero(expr * arg1, expr_ref & result);
     br_status mk_is_pzero(expr * arg1, expr_ref & result);
+    br_status mk_is_nan(expr * arg1, expr_ref & result);
+    br_status mk_is_inf(expr * arg1, expr_ref & result);
+    br_status mk_is_normal(expr * arg1, expr_ref & result);
+    br_status mk_is_subnormal(expr * arg1, expr_ref & result);
     br_status mk_is_sign_minus(expr * arg1, expr_ref & result);
 
     br_status mk_to_ieee_bv(expr * arg1, expr_ref & result);

src/muz_qe/dl_instruction.cpp

@@ -528,9 +528,9 @@ namespace datalog {
 
     class instr_filter_interpreted_and_project : public instruction {
         reg_idx m_src;
-        reg_idx m_res;
         app_ref m_cond;
         unsigned_vector m_cols;
+        reg_idx m_res;
     public:
         instr_filter_interpreted_and_project(reg_idx src, app_ref & condition,
             unsigned col_cnt, const unsigned * removed_cols, reg_idx result)

src/muz_qe/fixedpoint_params.pyg

@@ -48,6 +48,7 @@ def_module_params('fixedpoint',
                           ('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"),
                           ('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"),
                           ('use_arith_inductive_generalizer', BOOL, False, "PDR: generalize lemmas using arithmetic heuristics for induction strengthening"),
+	                  ('use_convex_hull_generalizer', BOOL, False, "PDR: generalize using convex hulls of lemmas"),
                           ('cache_mode', UINT, 0, "PDR: use no (0), symbolic (1) or explicit cache (2) for model search"),
                           ('inductive_reachability_check', BOOL, False, "PDR: assume negation of the cube on the previous level when "
                                                                         "checking for reachability (not only during cube weakening)"),

src/muz_qe/pdr_context.cpp

@@ -1572,6 +1572,9 @@ namespace pdr {
             }
 
         }
+        if (m_params.use_convex_hull_generalizer()) {
+            m_core_generalizers.push_back(alloc(core_convex_hull_generalizer, *this));
+        }
         if (!use_mc && m_params.use_inductive_generalizer()) {
             m_core_generalizers.push_back(alloc(core_bool_inductive_generalizer, *this, 0));
         }

src/muz_qe/pdr_generalizers.cpp

@@ -147,6 +147,177 @@ namespace pdr {
     }
 
 
+    core_convex_hull_generalizer::core_convex_hull_generalizer(context& ctx):
+        core_generalizer(ctx),
+        m(ctx.get_manager()),
+        a(m),
+        m_sigma(m),
+        m_trail(m) {
+        m_sigma.push_back(m.mk_fresh_const("sigma", a.mk_real()));
+        m_sigma.push_back(m.mk_fresh_const("sigma", a.mk_real()));
+    }
+    
+    void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) {
+        manager& pm = n.pt().get_pdr_manager();
+        expr_ref_vector conv1(m), conv2(m), core1(m), core2(m), eqs(m);
+        if (core.empty()) {
+            return;
+        }        
+        if (!m_left.contains(n.pt().head())) {
+            expr_ref left(m), right(m);
+            m_left.insert(n.pt().head(), 0);
+            unsigned sz = n.pt().sig_size();        
+            for (unsigned i = 0; i < sz; ++i) {
+                func_decl* fn0 = n.pt().sig(i);
+                sort* srt = fn0->get_range();
+                if (a.is_int_real(srt)) {
+                    func_decl* fn1 = pm.o2n(fn0, 0);
+                    left  = m.mk_fresh_const(fn1->get_name().str().c_str(), srt);
+                    right = m.mk_fresh_const(fn1->get_name().str().c_str(), srt);
+                    m_left.insert(fn1, left);
+                    m_right.insert(fn1, right);
+                    m_trail.push_back(left);
+                    m_trail.push_back(right);
+                }
+            }
+        }
+        unsigned sz = n.pt().sig_size();        
+        for (unsigned i = 0; i < sz; ++i) {
+            expr* left, *right;
+            func_decl* fn0 = n.pt().sig(i);
+            func_decl* fn1 = pm.o2n(fn0, 0);
+            if (m_left.find(fn1, left) && m_right.find(fn1, right)) {
+                eqs.push_back(m.mk_eq(m.mk_const(fn1), a.mk_add(left, right)));
+            }
+        }
+        if (!mk_convex(core, 0, conv1)) {
+            IF_VERBOSE(0, verbose_stream() << "Non-convex: " << mk_pp(pm.mk_and(core), m) << "\n";);
+            return;
+        }
+        conv1.append(eqs);
+        conv1.push_back(a.mk_gt(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real())));
+        conv1.push_back(a.mk_gt(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real())));
+        conv1.push_back(m.mk_eq(a.mk_numeral(rational(1), a.mk_real()), a.mk_add(m_sigma[0].get(), m_sigma[1].get())));
+        expr_ref fml = n.pt().get_formulas(n.level(), false);
+        expr_ref_vector fmls(m);
+        datalog::flatten_and(fml, fmls);
+        for (unsigned i = 0; i < fmls.size(); ++i) {
+            fml = m.mk_not(fmls[i].get());
+            core2.reset();
+            datalog::flatten_and(fml, core2);
+            if (!mk_convex(core2, 1, conv2)) {
+                IF_VERBOSE(0, verbose_stream() << "Non-convex: " << mk_pp(pm.mk_and(core2), m) << "\n";);
+                continue;
+            }
+            conv2.append(conv1);
+            expr_ref state = pm.mk_and(conv2);
+            TRACE("pdr", tout << "Check:\n" << mk_pp(state, m) << "\n";
+                  tout << "New formula:\n" << mk_pp(pm.mk_and(core), m) << "\n";
+                  tout << "Old formula:\n" << mk_pp(fml, m) << "\n";
+
+                  );
+            model_node nd(0, state, n.pt(), n.level());
+            if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) {
+                TRACE("pdr", 
+                      tout << mk_pp(state, m) << "\n";
+                      tout << "Generalized to:\n" << mk_pp(pm.mk_and(conv2), m) << "\n";);
+                IF_VERBOSE(0,
+                           verbose_stream() << mk_pp(state, m) << "\n";
+                           verbose_stream() << "Generalized to:\n" << mk_pp(pm.mk_and(conv2), m) << "\n";);
+                core.reset();
+                core.append(conv2);
+            }            
+        }
+    }
+
+    bool core_convex_hull_generalizer::mk_convex(expr_ref_vector const& core, unsigned index, expr_ref_vector& conv) {
+        conv.reset();
+        for (unsigned i = 0; i < core.size(); ++i) {
+            mk_convex(core[i], index, conv);
+        }
+        return !conv.empty();
+    }
+
+    void core_convex_hull_generalizer::mk_convex(expr* fml, unsigned index, expr_ref_vector& conv) {
+        expr_ref result(m), r1(m), r2(m);
+        expr* e1, *e2;        
+        bool is_not = m.is_not(fml, fml);
+        if (a.is_le(fml, e1, e2) && mk_convex(e1, index, false, r1) && mk_convex(e2, index, false, r2)) {
+            result = a.mk_le(r1, r2);
+        }
+        else if (a.is_ge(fml, e1, e2) && mk_convex(e1, index, false, r1) && mk_convex(e2, index, false, r2)) {
+            result = a.mk_ge(r1, r2);
+        }
+        else if (a.is_gt(fml, e1, e2) && mk_convex(e1, index, false, r1) && mk_convex(e2, index, false, r2)) {
+            result = a.mk_gt(r1, r2);
+        }
+        else if (a.is_lt(fml, e1, e2) && mk_convex(e1, index, false, r1) && mk_convex(e2, index, false, r2)) {
+            result = a.mk_lt(r1, r2);
+        }
+        else if (m.is_eq(fml, e1, e2) && a.is_int_real(e1) && mk_convex(e1, index, false, r1) && mk_convex(e2, index, false, r2)) {
+            result = m.mk_eq(r1, r2);
+        }
+        else {
+            TRACE("pdr", tout << "Did not handle " << mk_pp(fml, m) << "\n";);
+            return;
+        }
+        if (is_not) {
+            result = m.mk_not(result);
+        }
+        conv.push_back(result);
+    }
+
+    
+    bool core_convex_hull_generalizer::translate(func_decl* f, unsigned index, expr_ref& result) {
+        expr* tmp;
+        if (index == 0 && m_left.find(f, tmp)) {
+            result = tmp;
+            return true;
+        }
+        if (index == 1 && m_right.find(f, tmp)) {
+            result = tmp;
+            return true;
+        }
+        return false;
+    }
+
+
+    bool core_convex_hull_generalizer::mk_convex(expr* term, unsigned index, bool is_mul, expr_ref& result) {
+        if (!is_app(term)) {
+            return false;
+        }
+        app* app = to_app(term);
+        expr* e1, *e2;
+        expr_ref r1(m), r2(m);
+        if (translate(app->get_decl(), index, result)) {
+            return true;
+        }
+        if (a.is_add(term, e1, e2) && mk_convex(e1, index, is_mul, r1) && mk_convex(e2, index, is_mul, r2)) {
+            result = a.mk_add(r1, r2);
+            return true;
+        }
+        if (a.is_sub(term, e1, e2) && mk_convex(e1, index, is_mul, r1) && mk_convex(e2, index, is_mul, r2)) {
+            result = a.mk_sub(r1, r2);
+            return true;
+        }
+        if (a.is_mul(term, e1, e2) && mk_convex(e1, index, true, r1) && mk_convex(e2, index, true, r2)) {
+            result = a.mk_mul(r1, r2);
+            return true;
+        }
+        if (a.is_numeral(term)) {
+            if (is_mul) {
+                result = term;
+            }
+            else {
+                result = a.mk_mul(m_sigma[index].get(), term);
+            }
+            return true;
+        }
+        IF_VERBOSE(0, verbose_stream() << "Not handled: " << mk_pp(term, m) << "\n";);
+        return false;
+    }
+
+
     // ---------------------------------
     // core_arith_inductive_generalizer 
     // NB. this is trying out some ideas for generalization in

src/muz_qe/pdr_generalizers.h

@@ -73,6 +73,23 @@ namespace pdr {
         virtual void collect_statistics(statistics& st) const;
     };
 
+    class core_convex_hull_generalizer : public core_generalizer {
+        ast_manager&    m;
+        arith_util      a;
+        expr_ref_vector m_sigma;
+        expr_ref_vector m_trail;
+        obj_map<func_decl, expr*> m_left;
+        obj_map<func_decl, expr*> m_right;
+        bool mk_convex(expr_ref_vector const& core, unsigned index, expr_ref_vector& conv);
+        void mk_convex(expr* fml, unsigned index, expr_ref_vector& conv);
+        bool mk_convex(expr* term, unsigned index, bool is_mul, expr_ref& result);
+        bool translate(func_decl* fn, unsigned index, expr_ref& result);
+    public:
+        core_convex_hull_generalizer(context& ctx);
+        virtual ~core_convex_hull_generalizer() {}
+        virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);
+    };	
+
     class core_multi_generalizer : public core_generalizer {
         core_bool_inductive_generalizer m_gen;
     public:

src/sat/sat_asymm_branch.cpp

@@ -72,11 +72,14 @@ namespace sat {
         int limit  = -static_cast<int>(m_asymm_branch_limit);
         std::stable_sort(s.m_clauses.begin(), s.m_clauses.end(), clause_size_lt());
         m_counter -= s.m_clauses.size();
+        SASSERT(s.m_qhead == s.m_trail.size());
         clause_vector::iterator it  = s.m_clauses.begin();
         clause_vector::iterator it2 = it;
         clause_vector::iterator end = s.m_clauses.end();
         try {
             for (; it != end; ++it) {
+                if (s.inconsistent())
+                    break;
                 SASSERT(s.m_qhead == s.m_trail.size());
                 if (m_counter < limit || s.inconsistent()) {
                     *it2 = *it;
@@ -111,6 +114,7 @@ namespace sat {
     bool asymm_branch::process(clause & c) {
         TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";);
         SASSERT(s.scope_lvl() == 0);
+        SASSERT(s.m_qhead == s.m_trail.size());
 #ifdef Z3DEBUG
         unsigned trail_sz = s.m_trail.size();
 #endif
@@ -143,6 +147,7 @@ namespace sat {
         SASSERT(!s.inconsistent());
         SASSERT(s.scope_lvl() == 0);
         SASSERT(trail_sz == s.m_trail.size());
+        SASSERT(s.m_qhead == s.m_trail.size());
         if (i == sz - 1) {
             // clause size can't be reduced.
             s.attach_clause(c);
@@ -181,15 +186,18 @@ namespace sat {
             s.assign(c[0], justification());
             s.del_clause(c);
             s.propagate_core(false); 
+            SASSERT(s.inconsistent() || s.m_qhead == s.m_trail.size());
             return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state.
         case 2:
             SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
             s.mk_bin_clause(c[0], c[1], false);
             s.del_clause(c);
+            SASSERT(s.m_qhead == s.m_trail.size());
             return false;
         default:
             c.shrink(new_sz);
             s.attach_clause(c);
+            SASSERT(s.m_qhead == s.m_trail.size());
             return true;
         }
     }

src/sat/sat_simplifier.cpp

@@ -632,7 +632,8 @@ namespace sat {
         case 1:
             TRACE("elim_lit", tout << "clause became unit: " << c[0] << "\n";);
             propagate_unit(c[0]);
-            remove_clause(c);
+            // propagate_unit will delete c.
+            // remove_clause(c);
             return;
         case 2:
             TRACE("elim_lit", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
@@ -823,7 +824,8 @@ namespace sat {
                 }
                 if (sz == 1) {
                     propagate_unit(c[0]);
-                    remove_clause(c);
+                    // propagate_unit will delete c.
+                    // remove_clause(c);
                     continue;
                 }
                 if (sz == 2) {

src/tactic/fpa/fpa2bv_converter.cpp

@@ -1022,13 +1022,15 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
     split(x, x_sgn, x_sig, x_exp);
     split(y, y_sgn, y_sig, y_exp);
 
-    expr_ref c1(m), c2(m), y_is_nan(m), x_is_nzero(m), y_is_zero(m), c2_and(m);
+    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);
-    mk_is_nan(x, c1);
+    mk_is_zero(x, x_is_zero);
-    mk_is_nan(y, y_is_nan);
-    mk_is_nzero(x, x_is_nzero);
     mk_is_zero(y, y_is_zero);
-    m_simp.mk_and(x_is_nzero, y_is_zero, c2_and);
+    m_simp.mk_and(x_is_zero, y_is_zero, c1_and);
-    m_simp.mk_or(y_is_nan, c2_and, c2);
+    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;       
     
     expr_ref c3(m);
     mk_float_lt(f, num, args, c3);
@@ -1063,13 +1065,15 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
     split(x, x_sgn, x_sig, x_exp);
     split(y, y_sgn, y_sig, y_exp);
 
-    expr_ref c1(m), c2(m), y_is_nan(m), y_is_nzero(m), x_is_zero(m), xy_is_zero(m);
+    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_nan(x, c1);
+    mk_is_zero(y, y_is_zero);
-    mk_is_nan(y, y_is_nan);
-    mk_is_nzero(y, y_is_nzero);
     mk_is_zero(x, x_is_zero);
-    m_simp.mk_and(y_is_nzero, x_is_zero, xy_is_zero);
+    m_simp.mk_and(y_is_zero, x_is_zero, c1_and);
-    m_simp.mk_or(y_is_nan, xy_is_zero, c2);
+    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;
     
     expr_ref c3(m);
     mk_float_gt(f, num, args, c3);
@@ -1111,20 +1115,23 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     mk_minus_inf(f, ninf);
     mk_plus_inf(f, pinf);        
 
-    expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m);
+    expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_neg(m), x_is_inf(m);
-    expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m);
+    expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_neg(m), y_is_inf(m);
-    expr_ref z_is_nan(m), z_is_zero(m), z_is_pos(m), z_is_inf(m);
+    expr_ref z_is_nan(m), z_is_zero(m), z_is_pos(m), z_is_neg(m), z_is_inf(m);
     mk_is_nan(x, x_is_nan);
     mk_is_zero(x, x_is_zero);
     mk_is_pos(x, x_is_pos);
+    mk_is_neg(x, x_is_neg);
     mk_is_inf(x, x_is_inf);
     mk_is_nan(y, y_is_nan);
     mk_is_zero(y, y_is_zero);
     mk_is_pos(y, y_is_pos);
+    mk_is_neg(y, y_is_neg);
     mk_is_inf(y, y_is_inf);
     mk_is_nan(z, z_is_nan);
     mk_is_zero(z, z_is_zero);
     mk_is_pos(z, z_is_pos);
+    mk_is_neg(z, z_is_neg);
     mk_is_inf(z, z_is_inf);
 
     dbg_decouple("fpa2bv_fma_x_is_nan", x_is_nan);
@@ -1140,42 +1147,56 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     dbg_decouple("fpa2bv_fma_z_is_pos", z_is_pos);
     dbg_decouple("fpa2bv_fma_z_is_inf", z_is_inf);
 
-    expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m);
+    expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m), c7(m);
-    expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m);
+    expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m), v8(m);
 
-    // (x is NaN) || (y is NaN) -> NaN
+    expr_ref inf_xor(m), inf_cond(m);
-    m_simp.mk_or(x_is_nan, y_is_nan, c1);
+    m_simp.mk_xor(x_is_neg, y_is_neg, inf_xor);
+    m_simp.mk_xor(inf_xor, z_is_neg, inf_xor);
+    m_simp.mk_and(z_is_inf, inf_xor, inf_cond);
+
+    // (x is NaN) || (y is NaN) || (z is Nan) -> NaN
+    m_simp.mk_or(x_is_nan, y_is_nan, z_is_nan, c1);
     v1 = nan;
     
     // (x is +oo) -> if (y is 0) then NaN else inf with y's sign.
     mk_is_pinf(x, c2);
-    expr_ref y_sgn_inf(m);
+    expr_ref y_sgn_inf(m), inf_or(m);
     mk_ite(y_is_pos, pinf, ninf, y_sgn_inf);
-    mk_ite(y_is_zero, nan, y_sgn_inf, v2);
+    m_simp.mk_or(y_is_zero, inf_cond, inf_or);
+    mk_ite(inf_or, nan, y_sgn_inf, v2);
                 
     // (y is +oo) -> if (x is 0) then NaN else inf with x's sign.
     mk_is_pinf(y, c3);
     expr_ref x_sgn_inf(m);
     mk_ite(x_is_pos, pinf, ninf, x_sgn_inf);
-    mk_ite(x_is_zero, nan, x_sgn_inf, v3);
+    m_simp.mk_or(x_is_zero, inf_cond, inf_or);
+    mk_ite(inf_or, nan, x_sgn_inf, v3);
     
     // (x is -oo) -> if (y is 0) then NaN else inf with -y's sign.    
     mk_is_ninf(x, c4);
     expr_ref neg_y_sgn_inf(m);
     mk_ite(y_is_pos, ninf, pinf, neg_y_sgn_inf);
-    mk_ite(y_is_zero, nan, neg_y_sgn_inf, v4);
+    m_simp.mk_or(y_is_zero, inf_cond, inf_or);
+    mk_ite(inf_or, nan, neg_y_sgn_inf, v4);
 
     // (y is -oo) -> if (x is 0) then NaN else inf with -x's sign.    
     mk_is_ninf(y, c5);
     expr_ref neg_x_sgn_inf(m);
     mk_ite(x_is_pos, ninf, pinf, neg_x_sgn_inf);
-    mk_ite(x_is_zero, nan, neg_x_sgn_inf, v5);
+    m_simp.mk_or(x_is_zero, inf_cond, inf_or);
+    mk_ite(inf_or, nan, neg_x_sgn_inf, v5);
+
+    // z is +-INF -> Z.
+    mk_is_inf(z, c6);
+    v6 = z;
 
     // (x is 0) || (y is 0) -> x but with sign = x.sign ^ y.sign
-    m_simp.mk_or(x_is_zero, y_is_zero, c6);
+    m_simp.mk_or(x_is_zero, y_is_zero, c7);
     expr_ref sign_xor(m);
     m_simp.mk_xor(x_is_pos, y_is_pos, sign_xor);
-    mk_ite(sign_xor, nzero, pzero, v6);
+    mk_ite(sign_xor, nzero, pzero, v7);    
+    
         
     // else comes the fused multiplication.
     unsigned ebits = m_util.get_ebits(f->get_range());
@@ -1190,54 +1211,57 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     expr_ref c_sgn(m), c_sig(m), c_exp(m), c_lz(m);
     unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
     unpack(y, b_sgn, b_sig, b_exp, b_lz, true);
-    unpack(z, c_sgn, c_sig, c_exp, c_lz, false);
+    unpack(z, c_sgn, c_sig, c_exp, c_lz, true);
 
-    expr_ref a_lz_ext(m), b_lz_ext(m);
+    expr_ref a_lz_ext(m), b_lz_ext(m), c_lz_ext(m);
     a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz);
     b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz);
+    c_lz_ext = m_bv_util.mk_zero_extend(2, c_lz);
 
     expr_ref a_sig_ext(m), b_sig_ext(m);
     a_sig_ext = m_bv_util.mk_zero_extend(sbits, a_sig);
     b_sig_ext = m_bv_util.mk_zero_extend(sbits, b_sig);
 
-    expr_ref a_exp_ext(m), b_exp_ext(m);
+    expr_ref a_exp_ext(m), b_exp_ext(m), c_exp_ext(m);
     a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp);
     b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp);
+    c_exp_ext = m_bv_util.mk_sign_extend(2, c_exp);
 
     expr_ref mul_sgn(m), mul_sig(m), mul_exp(m);
     expr * signs[2] = { a_sgn, b_sgn };
-    mul_sgn = m_bv_util.mk_bv_xor(2, signs);
 
+    mul_sgn = m_bv_util.mk_bv_xor(2, signs);
     dbg_decouple("fpa2bv_fma_mul_sgn", mul_sgn);
 
-    mul_exp = m_bv_util.mk_bv_sub(
+    mul_exp = m_bv_util.mk_bv_add(m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext),
-                m_bv_util.mk_bv_add(a_exp_ext, b_exp_ext),
+                                  m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext));
-                m_bv_util.mk_bv_add(a_lz_ext, b_lz_ext));
+    dbg_decouple("fpa2bv_fma_mul_exp", mul_exp);
     
     mul_sig = m_bv_util.mk_bv_mul(a_sig_ext, b_sig_ext);
-
     dbg_decouple("fpa2bv_fma_mul_sig", mul_sig);
 
     SASSERT(m_bv_util.get_bv_size(mul_sig) == 2*sbits);
+    SASSERT(m_bv_util.get_bv_size(mul_exp) == ebits + 2);
 
-    // The result in `product' represents a number of the form 1.*** (unpacked)
+    // The product has the form [-1][0].[2*sbits - 2].
-    // (product = mul_sgn/mul_sig/mul_exp and c_sgn/c_sig/c_exp is unpacked w/o normalization).
+    
+    // Extend c
+    c_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits-1)));
 
-    // extend c.
+    SASSERT(m_bv_util.get_bv_size(mul_sig) == 2 * sbits);
-    c_sig = m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits));
+    SASSERT(m_bv_util.get_bv_size(c_sig) == 2 * sbits);
-    c_exp = m_bv_util.mk_sign_extend(2, c_exp);
 
     expr_ref swap_cond(m);
-    swap_cond = m_bv_util.mk_sle(mul_exp, c_exp);
+    swap_cond = m_bv_util.mk_sle(mul_exp, c_exp_ext);
     SASSERT(is_well_sorted(m, swap_cond));
 
     expr_ref e_sgn(m), e_sig(m), e_exp(m), f_sgn(m), f_sig(m), f_exp(m);
     m_simp.mk_ite(swap_cond, c_sgn, mul_sgn, e_sgn);
     m_simp.mk_ite(swap_cond, c_sig, mul_sig, e_sig); // has 2 * sbits
-    m_simp.mk_ite(swap_cond, c_exp, mul_exp, e_exp); // has ebits + 2
+    m_simp.mk_ite(swap_cond, c_exp_ext, mul_exp, e_exp); // has ebits + 2
     m_simp.mk_ite(swap_cond, mul_sgn, c_sgn, f_sgn);
     m_simp.mk_ite(swap_cond, mul_sig, c_sig, f_sig); // has 2 * sbits
-    m_simp.mk_ite(swap_cond, mul_exp, c_exp, f_exp); // has ebits + 2
+    m_simp.mk_ite(swap_cond, mul_exp, c_exp_ext, f_exp); // has ebits + 2
 
     SASSERT(is_well_sorted(m, e_sgn));
     SASSERT(is_well_sorted(m, e_sig));
@@ -1247,26 +1271,94 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     SASSERT(is_well_sorted(m, f_exp));
 
     expr_ref res_sgn(m), res_sig(m), res_exp(m);
-    add_core(2 * sbits, ebits + 2, rm,
+    
-             e_sgn, e_sig, e_exp, f_sgn, f_sig, f_exp, 
+    expr_ref exp_delta(m);
-             res_sgn, res_sig, res_exp);
+    exp_delta = m_bv_util.mk_bv_sub(e_exp, f_exp);
+    dbg_decouple("fpa2bv_fma_add_exp_delta", exp_delta);
 
-    // Note: res_sig is now 2 * sbits + 4, i.e., `sbits' too much, which should go into a sticky bit.
+    // cap the delta    
-    unsigned sig_size = m_bv_util.get_bv_size(res_sig);
+    expr_ref cap(m), cap_le_delta(m);
-    SASSERT(sig_size == (2*sbits+4));
+    cap = m_bv_util.mk_numeral(sbits+3, ebits+2);
+    cap_le_delta = m_bv_util.mk_ule(exp_delta, cap);
+    m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta);
+    SASSERT(m_bv_util.get_bv_size(exp_delta) == ebits+2);
+    dbg_decouple("fpa2bv_fma_add_exp_delta_capped", exp_delta);
+    
+    // Alignment shift with sticky bit computation.    
+    expr_ref big_f_sig(m);
+    big_f_sig = m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits+4));    
+    SASSERT(is_well_sorted(m, big_f_sig));
 
-    // Note: res_exp is 2 bits too wide.
+    expr_ref shifted_big(m), shifted_f_sig(m), sticky_raw(m);
-    unsigned exp_size = m_bv_util.get_bv_size(res_exp);
+    shifted_big = m_bv_util.mk_bv_lshr(big_f_sig, m_bv_util.mk_concat(m_bv_util.mk_numeral(0, (2*(sbits+4))-(ebits+2)), exp_delta));
-    SASSERT(exp_size == ebits+4);
+    shifted_f_sig = m_bv_util.mk_extract((2*(sbits+4)-1), (sbits+4), shifted_big);
-    res_exp = m_bv_util.mk_extract(ebits+1, 0, res_exp);
+    SASSERT(is_well_sorted(m, shifted_f_sig));
 
-    expr_ref sticky(m);
+    sticky_raw = m_bv_util.mk_extract(sbits+3, 0, shifted_big);    
-    sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits, 0, res_sig));    
+    expr_ref sticky(m), sticky_eq(m), nil_sbit4(m), one_sbit4(m); 
-    res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(2*sbits+3, sbits+1, res_sig), sticky);        
+    nil_sbit4 = m_bv_util.mk_numeral(0, sbits+4);
+    one_sbit4 = m_bv_util.mk_numeral(1, sbits+4);
+    m_simp.mk_eq(sticky_raw, nil_sbit4, sticky_eq);
+    m_simp.mk_ite(sticky_eq, nil_sbit4, one_sbit4, sticky);
+    SASSERT(is_well_sorted(m, sticky));
+    
+    expr * or_args[2] = { shifted_f_sig, sticky };
+    shifted_f_sig = m_bv_util.mk_bv_or(2, or_args);
+    SASSERT(is_well_sorted(m, shifted_f_sig));
 
-    sig_size = m_bv_util.get_bv_size(res_sig);    
+    expr_ref eq_sgn(m);
-    SASSERT(sig_size == sbits+4);    
+    m_simp.mk_eq(e_sgn, f_sgn, eq_sgn);
+    
+    // two extra bits for catching the overflow.
+    e_sig = m_bv_util.mk_zero_extend(2, e_sig);
+    shifted_f_sig = m_bv_util.mk_zero_extend(2, shifted_f_sig);
 
+    SASSERT(m_bv_util.get_bv_size(e_sig) == sbits+6);
+    SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == sbits+6);
+
+    dbg_decouple("fpa2bv_fma_add_e_sig", e_sig);
+    dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig);
+
+    expr_ref sum(m);
+    m_simp.mk_ite(eq_sgn, 
+                  m_bv_util.mk_bv_add(e_sig, shifted_f_sig), // ADD LZ
+                  m_bv_util.mk_bv_sub(e_sig, shifted_f_sig),                  
+                  sum);
+
+    SASSERT(is_well_sorted(m, sum));
+
+    dbg_decouple("fpa2bv_fma_add_sum", sum);
+
+    expr_ref sign_bv(m), n_sum(m);
+    sign_bv = m_bv_util.mk_extract(sbits+4, sbits+4, sum);        
+    n_sum = m_bv_util.mk_bv_neg(sum);
+
+    dbg_decouple("fpa2bv_fma_add_sign_bv", sign_bv);    
+    dbg_decouple("fpa2bv_fma_add_n_sum", n_sum);         
+    
+    family_id bvfid = m_bv_util.get_fid();
+
+    expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m);
+    expr_ref not_e_sgn(m), not_f_sgn(m), not_sign_bv(m);
+    not_e_sgn = m_bv_util.mk_bv_not(e_sgn);
+    not_f_sgn = m_bv_util.mk_bv_not(f_sgn);
+    not_sign_bv = m_bv_util.mk_bv_not(sign_bv);
+    res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_e_sgn, e_sgn, sign_bv);
+    res_sgn_c2 = m.mk_app(bvfid, OP_BAND, e_sgn, not_f_sgn, not_sign_bv);
+    res_sgn_c3 = m.mk_app(bvfid, OP_BAND, e_sgn, f_sgn);
+    expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };   
+    res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args);
+
+    expr_ref res_sig_eq(m), sig_abs(m), one_1(m);
+    one_1 = m_bv_util.mk_numeral(1, 1);
+    m_simp.mk_eq(sign_bv, one_1, res_sig_eq);
+    m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs);
+
+    dbg_decouple("fpa2bv_fma_add_sig_abs", sig_abs);
+
+    res_sig = m_bv_util.mk_extract(sbits+3, 0, sig_abs);
+    res_exp = m_bv_util.mk_bv_sub(e_exp, c_lz_ext);
+    
     expr_ref is_zero_sig(m), nil_sbits4(m);
     nil_sbits4 = m_bv_util.mk_numeral(0, sbits+4);
     m_simp.mk_eq(res_sig, nil_sbits4, is_zero_sig);
@@ -1281,10 +1373,11 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     expr_ref rounded(m);
     round(f->get_range(), rm, res_sgn, res_sig, res_exp, rounded);
 
-    mk_ite(is_zero_sig, zero_case, rounded, v7);
+    mk_ite(is_zero_sig, zero_case, rounded, v8);
 
     // And finally, we tie them together.
-    mk_ite(c6, v6, v7, result);
+    mk_ite(c7, v7, v8, result);
+    mk_ite(c6, v6, result, result);
     mk_ite(c5, v5, result, result);
     mk_ite(c4, v4, result, result);
     mk_ite(c3, v3, result, result);
@@ -1293,7 +1386,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
 
     SASSERT(is_well_sorted(m, result));
 
-    TRACE("fpa2bv_mul", tout << "MUL = " << mk_ismt2_pp(result, m) << std::endl; );
+    TRACE("fpa2bv_fma_", tout << "FMA = " << mk_ismt2_pp(result, m) << std::endl; );
 }
 
 void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@@ -1528,6 +1621,26 @@ void fpa2bv_converter::mk_is_pzero(func_decl * f, unsigned num, expr * const * a
     m_simp.mk_and(a0_is_pos, a0_is_zero, result);
 }
 
+void fpa2bv_converter::mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 1);
+    mk_is_nan(args[0], result);
+}
+
+void fpa2bv_converter::mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 1);
+    mk_is_inf(args[0], result);
+}
+
+void fpa2bv_converter::mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 1);
+    mk_is_normal(args[0], result);
+}
+
+void fpa2bv_converter::mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 1);
+    mk_is_denormal(args[0], result);
+}
+
 void fpa2bv_converter::mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 1);
     mk_is_neg(args[0], result);
@@ -1585,6 +1698,10 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
         expr_ref sgn(m), sig(m), exp(m), lz(m);
         unpack(x, sgn, sig, exp, lz, true);
 
+        dbg_decouple("fpa2bv_to_float_x_sig", sig);
+        dbg_decouple("fpa2bv_to_float_x_exp", exp);
+        dbg_decouple("fpa2bv_to_float_lz", lz);
+
         expr_ref res_sgn(m), res_sig(m), res_exp(m);
 
         res_sgn = sgn;
@@ -1597,10 +1714,13 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
         SASSERT(m_bv_util.get_bv_size(sgn) == 1);
         SASSERT(m_bv_util.get_bv_size(sig) == from_sbits);
         SASSERT(m_bv_util.get_bv_size(exp) == from_ebits);
+        SASSERT(m_bv_util.get_bv_size(lz) == from_ebits);
 
-        if (from_sbits < (to_sbits + 3))
+        if (from_sbits < (to_sbits + 3)) 
+        {
             // make sure that sig has at least to_sbits + 3
             res_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, to_sbits+3-from_sbits));
+        } 
         else if (from_sbits > (to_sbits + 3))
         {
             // collapse the extra bits into a sticky bit.
@@ -1621,7 +1741,9 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
         exponent_overflow = m.mk_false();
 
         if (from_ebits < (to_ebits + 2))
-            res_exp = m_bv_util.mk_sign_extend(to_ebits+2-from_ebits, exp);
+        {                        
+            res_exp = m_bv_util.mk_sign_extend(to_ebits-from_ebits+2, exp);            
+        }
         else if (from_ebits > (to_ebits + 2))
         {
             expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), h_or_eq(m), h_and_eq(m);
@@ -1634,7 +1756,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
             high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get());
 
             zero1 = m_bv_util.mk_numeral(0, 1);
-            m_simp.mk_eq(high_red_and, one1, h_and_eq);            
+            m_simp.mk_eq(high_red_and, one1, h_and_eq);
             m_simp.mk_eq(high_red_or, zero1, h_or_eq);
             m_simp.mk_eq(lows, zero1, s_is_zero);
             m_simp.mk_eq(lows, one1, s_is_one);
@@ -1650,10 +1772,18 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
         else
             res_exp = exp;
 
+        // subtract lz for subnormal numbers.
+        expr_ref lz_ext(m);
+        lz_ext = m_bv_util.mk_zero_extend(to_ebits-from_ebits+2, lz);
+        res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext);
         SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits+2);
 
+        dbg_decouple("fpa2bv_to_float_res_sig", res_sig);
+        dbg_decouple("fpa2bv_to_float_res_exp", res_exp);
+
         expr_ref rounded(m);
         round(s, rm, res_sgn, res_sig, res_exp, rounded);
+        
 
         expr_ref is_neg(m), sig_inf(m);
         m_simp.mk_eq(sgn, one1, is_neg);
@@ -1668,7 +1798,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
         mk_ite(c4, v4, result, result);
         mk_ite(c3, v3, result, result);
         mk_ite(c2, v2, result, result);
-        mk_ite(c1, v1, result, result);
+        mk_ite(c1, v1, result, result);        
     }
     else {
         // .. other than that, we only support rationals for asFloat
@@ -1713,7 +1843,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
         m_util.fm().del(v);
     }
 
-    SASSERT(is_well_sorted(m, result));
+    SASSERT(is_well_sorted(m, result));    
 }
 
 void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@@ -2571,9 +2701,13 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
     sz = bv_mdl->get_num_functions();
     for (unsigned i = 0; i < sz; i++)
     {
-        func_decl * c = bv_mdl->get_function(i);
+        func_decl * f = bv_mdl->get_function(i);
-        if (!seen.contains(c))
+        if (!seen.contains(f))
-            float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
+        {
+            TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl; );
+            func_interp * val = bv_mdl->get_func_interp(f);
+            float_mdl->register_decl(f, val);
+        }
     }
 
     sz = bv_mdl->get_num_uninterpreted_sorts();

src/tactic/fpa/fpa2bv_converter.h

@@ -116,6 +116,10 @@ public:
     void mk_is_nzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_is_pzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
 
     void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);    

src/tactic/fpa/fpa2bv_rewriter.h

@@ -29,9 +29,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
     ast_manager              & m_manager;    
     expr_ref_vector            m_out;    
     fpa2bv_converter         & m_conv;
-    sort_ref_vector            m_bindings;    
+    sort_ref_vector            m_bindings;
-    expr_ref_vector            m_mappings;    
-
 
     unsigned long long         m_max_memory;
     unsigned                   m_max_steps;
@@ -42,8 +40,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
         m_manager(m),
         m_out(m),
         m_conv(c),
-        m_bindings(m),
+        m_bindings(m) {
-        m_mappings(m) {
         updt_params(p);
         // We need to make sure that the mananger has the BV plugin loaded.
         symbol s_bv("bv");
@@ -135,6 +132,10 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
             case OP_FLOAT_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
             case OP_FLOAT_IS_NZERO: m_conv.mk_is_nzero(f, num, args, result); return BR_DONE;
             case OP_FLOAT_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE;
             case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE;
             case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE;
             case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
@@ -177,7 +178,6 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
                 new_bindings.push_back(q->get_decl_sort(i));
             SASSERT(new_bindings.size() == q->get_num_decls());
             m_bindings.append(new_bindings);
-            m_mappings.resize(m_bindings.size(), 0);
         }
         return true;
     }
@@ -215,8 +215,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
                                    new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(),
                                    old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns);
         result_pr = 0;
-        m_bindings.shrink(old_sz);
+        m_bindings.shrink(old_sz);        
-        m_mappings.shrink(old_sz);
         TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " << 
                 mk_ismt2_pp(old_q->get_expr(), m()) << std::endl <<
                 " new body: " << mk_ismt2_pp(new_body, m()) << std::endl;
@@ -243,10 +242,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
                                 new_exp);
         }
         else
-            new_exp = m().mk_var(t->get_idx(), s);
+            new_exp = m().mk_var(t->get_idx(), s);        
-        m_mappings[inx] = new_exp;
 
-        result = m_mappings[inx].get();
+        result = new_exp;
         result_pr = 0;        
         TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;);
         return true;

src/tactic/sls/sls_tactic.cpp

@@ -1370,7 +1370,7 @@ class sls_tactic : public tactic {
 
         void updt_params(params_ref const & p) {        
             m_produce_models = p.get_bool("produce_models", false);        
-            m_max_restarts = p.get_uint("sls_restarts", -1);
+            m_max_restarts = p.get_uint("sls_restarts", (unsigned)-1);
             m_tracker.set_random_seed(p.get_uint("random_seed", 0));
             m_plateau_limit = p.get_uint("plateau_limit", 100);
         }
@@ -1612,7 +1612,7 @@ class sls_tactic : public tactic {
         lbool search(goal_ref const & g) {        
             lbool res = l_undef;
             double score = 0.0, old_score = 0.0;
-            unsigned new_const = -1, new_bit = 0;        
+            unsigned new_const = (unsigned)-1, new_bit = 0;        
             mpz new_value;
             move_type move;
             
@@ -1631,7 +1631,7 @@ class sls_tactic : public tactic {
                     checkpoint();
             
                     old_score = score;
-                    new_const = -1;
+                    new_const = (unsigned)-1;
                         
                     ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(g);
 

src/util/mpf.cpp

@@ -367,7 +367,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
         o.ebits = ebits;
         o.sbits = sbits;    
 
-        signed ds = sbits - x.sbits + 4;  // plus rounding bits
+        signed ds = sbits - x.sbits + 3;  // plus rounding bits
         if (ds > 0)
         {
             m_mpz_manager.mul2k(o.significand, ds);