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

scripts/mk_unix_dist.py

@@ -58,7 +58,7 @@ def display_help():
 
 # Parse configuration option for mk_make script
 def parse_options():
-    global FORCE_MK, JAVA_ENABLED, GIT_HASH
+    global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED
     path = BUILD_DIR
     options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 
                                                                    'help',

scripts/mk_win_dist.py

@@ -63,7 +63,7 @@ def display_help():
 
 # Parse configuration option for mk_make script
 def parse_options():
-    global FORCE_MK, JAVA_ENABLED, GIT_HASH
+    global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED
     path = BUILD_DIR
     options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 
                                                                    'help',

src/ackermannization/ackermannize_bv_tactic.cpp

@@ -74,6 +74,10 @@ public:
         m_lemma_limit = p.div0_ackermann_limit();
     }
 
+    virtual void collect_param_descrs(param_descrs & r) {
+        ackermannize_bv_tactic_params::collect_param_descrs(r);
+    }
+
     virtual void collect_statistics(statistics & st) const {
         st.update("ackr-constraints", m_st.m_ackrs_sz);
     }

src/api/api_ast.cpp

@@ -1066,15 +1066,14 @@ extern "C" {
             case OP_BV2INT:    return Z3_OP_BV2INT;
             case OP_CARRY:     return Z3_OP_CARRY;
             case OP_XOR3:      return Z3_OP_XOR3;
-            case OP_BSMUL_NO_OVFL:
+            case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL;
-            case OP_BUMUL_NO_OVFL:
+            case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL;
-            case OP_BSMUL_NO_UDFL:
+            case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;
-            case OP_BSDIV_I:
+            case OP_BSDIV_I: return Z3_OP_BSDIV_I;
-            case OP_BUDIV_I:
+            case OP_BUDIV_I: return Z3_OP_BUDIV_I;
-            case OP_BSREM_I:
+            case OP_BSREM_I: return Z3_OP_BSREM_I;
-            case OP_BUREM_I:
+            case OP_BUREM_I: return Z3_OP_BUREM_I;
-            case OP_BSMOD_I:
+            case OP_BSMOD_I: return Z3_OP_BSMOD_I;
-                return Z3_OP_UNINTERPRETED;
             default:
                 UNREACHABLE();
                 return Z3_OP_UNINTERPRETED;

src/api/api_model.cpp

@@ -50,14 +50,13 @@ extern "C" {
         Z3_CATCH;
     }
 
-    Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a) {
+    Z3_ast_opt Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a) {
         Z3_TRY;
         LOG_Z3_model_get_const_interp(c, m, a);
         RESET_ERROR_CODE();
         CHECK_NON_NULL(m, 0);
         expr * r = to_model_ref(m)->get_const_interp(to_func_decl(a));
         if (!r) {
-            SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
         mk_c(c)->save_ast_trail(r);

src/api/c++/z3++.h

@@ -1582,6 +1582,9 @@ namespace z3 {
 	    return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
 	}
 
+        // returns interpretation of constant declaration c.
+        // If c is not assigned any value in the model it returns 
+        // an expression with a null ast reference.
         expr get_const_interp(func_decl c) const {
             check_context(*this, c);
             Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);

src/api/python/z3.py

@@ -3468,7 +3468,7 @@ def is_bv_value(a):
     """
     return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
 
-def BV2Int(a):
+def BV2Int(a, is_signed=False):
     """Return the Z3 expression BV2Int(a).
 
     >>> b = BitVec('b', 3)
@@ -3477,6 +3477,10 @@ def BV2Int(a):
     >>> x = Int('x')
     >>> x > BV2Int(b)
     x > BV2Int(b)
+    >>> x > BV2Int(b, is_signed=False)
+    x > BV2Int(b)
+    >>> x > BV2Int(b, is_signed=True)
+    x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
     >>> solve(x > BV2Int(b), b == 1, x < 3)
     [b = 1, x = 2]
     """
@@ -3484,7 +3488,7 @@ def BV2Int(a):
         _z3_assert(is_bv(a), "Z3 bit-vector expression expected")
     ctx = a.ctx
     ## investigate problem with bv2int
-    return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), 0), ctx)
+    return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)
 
 def BitVecSort(sz, ctx=None):
     """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
@@ -5516,7 +5520,10 @@ class ModelRef(Z3PPObject):
             decl = decl.decl()
         try:
             if decl.arity() == 0:
-                r = _to_expr_ref(Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast), self.ctx)
+                _r = Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast)
+                if _r.value is None:
+                    return None
+                r = _to_expr_ref(_r, self.ctx)
                 if is_as_array(r):
                     return self.get_interp(get_as_array_func(r))
                 else:

src/api/z3_api.h

@@ -1060,6 +1060,15 @@ typedef enum {
     Z3_OP_CARRY,
     Z3_OP_XOR3,
 
+    Z3_OP_BSMUL_NO_OVFL,
+    Z3_OP_BUMUL_NO_OVFL,
+    Z3_OP_BSMUL_NO_UDFL,
+    Z3_OP_BSDIV_I,
+    Z3_OP_BUDIV_I,
+    Z3_OP_BSREM_I,
+    Z3_OP_BUREM_I,
+    Z3_OP_BSMOD_I,
+
     // Proofs
     Z3_OP_PR_UNDEF = 0x500,
     Z3_OP_PR_TRUE,

src/ast/fpa/fpa2bv_converter.cpp

@@ -1928,8 +1928,7 @@ void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref &
     tie_pttrn = m_bv_util.mk_concat(one_1, m_bv_util.mk_numeral(0, sbits-1));
     m_simp.mk_eq(rem, tie_pttrn, tie2);
     div_last = m_bv_util.mk_extract(0, 0, div);
-    tie2_c = m.mk_ite(tie2, m.mk_or(m.mk_and(rm_is_rte, m.mk_eq(div_last, one_1)),
+    tie2_c = m.mk_ite(tie2, m.mk_or(m.mk_and(rm_is_rte, m.mk_eq(div_last, one_1)), rm_is_rta),
-                                    m.mk_and(rm_is_rta, m.mk_eq(div_last, zero_1))),
                             m_bv_util.mk_ule(tie_pttrn, rem));
     m_simp.mk_ite(tie2_c, div_p1, div, v51);
 
@@ -2235,14 +2234,17 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
     SASSERT(is_well_sorted(m, result));
 }
 
+
 void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) {
+    SASSERT(is_app_of(rm, m_util.get_family_id(), OP_FPA_INTERNAL_RM));
+    mk_to_fp_float(s, to_app(rm)->get_arg(0), x, result);
+}
+
+void fpa2bv_converter::mk_to_fp_float(sort * to_srt, expr * rm, expr * x, expr_ref & result) {
     unsigned from_sbits = m_util.get_sbits(m.get_sort(x));
     unsigned from_ebits = m_util.get_ebits(m.get_sort(x));
-    unsigned to_sbits = m_util.get_sbits(s);
+    unsigned to_sbits = m_util.get_sbits(to_srt);
-    unsigned to_ebits = m_util.get_ebits(s);
+    unsigned to_ebits = m_util.get_ebits(to_srt);
-
-    SASSERT(is_app_of(rm, m_util.get_family_id(), OP_FPA_INTERNAL_RM));
-    expr * bv_rm = to_app(rm)->get_arg(0);
 
     if (from_sbits == to_sbits && from_ebits == to_ebits)
         result = x;
@@ -2253,20 +2255,20 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
 
         one1 = m_bv_util.mk_numeral(1, 1);
         expr_ref ninf(m), pinf(m);
-        mk_pinf(f, pinf);
+        mk_pinf(to_srt, pinf);
-        mk_ninf(f, ninf);
+        mk_ninf(to_srt, ninf);
 
         // NaN -> NaN
         mk_is_nan(x, c1);
-        mk_nan(f, v1);
+        mk_nan(to_srt, v1);
 
         // +0 -> +0
         mk_is_pzero(x, c2);
-        mk_pzero(f, v2);
+        mk_pzero(to_srt, v2);
 
         // -0 -> -0
         mk_is_nzero(x, c3);
-        mk_nzero(f, v3);
+        mk_nzero(to_srt, v3);
 
         // +oo -> +oo
         mk_is_pinf(x, c4);
@@ -2380,8 +2382,8 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
         dbg_decouple("fpa2bv_to_float_res_exp", res_exp);
 
         expr_ref rounded(m);
-        expr_ref rm_e(bv_rm, m);
+        expr_ref rm_e(rm, m);
-        round(s, rm_e, res_sgn, res_sig, res_exp, rounded);
+        round(to_srt, rm_e, res_sgn, res_sig, res_exp, rounded);
 
         expr_ref is_neg(m), sig_inf(m);
         m_simp.mk_eq(sgn, one1, is_neg);

src/ast/fpa/fpa2bv_converter.h

@@ -144,6 +144,9 @@ public:
     void dbg_decouple(const char * prefix, expr_ref & e);
     expr_ref_vector m_extra_assertions;
 
+    bool is_special(func_decl * f) { return m_specials.contains(f); }
+    bool is_uf2bvuf(func_decl * f) { return m_uf2bvuf.contains(f); }
+
 protected:
     void mk_one(func_decl *f, expr_ref & sign, expr_ref & result);
 
@@ -201,6 +204,8 @@ private:
     void mk_div(sort * s, expr_ref & bv_rm, expr_ref & x, expr_ref & y, expr_ref & result);
     void mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & result);
     void mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & x, expr_ref & result);
+
+    void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result);
 };
 
 #endif

src/ast/rewriter/th_rewriter.cpp

@@ -212,14 +212,11 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
 
     // auxiliary function for pull_ite_core
     expr * mk_eq_value(expr * lhs, expr * value) {
-        SASSERT(m().is_value(value));
+        if (m().are_equal(lhs, value)) {
-        if (m().is_value(lhs)) {
+            return m().mk_true();
-            if (m().are_equal(lhs, value)) {
+        }
-                return m().mk_true();
+        else if (m().are_distinct(lhs, value)) {
-            }
+            return m().mk_false();
-            else if (m().are_distinct(lhs, value)) {
-                return m().mk_false();
-            }
         }
         return m().mk_eq(lhs, value);
     }

src/math/grobner/grobner.cpp

@@ -670,7 +670,7 @@ grobner::equation * grobner::simplify(equation const * source, equation * target
             simplify(target);
         }
     }
-    while (simplified);
+    while (simplified && !m_manager.canceled());
     TRACE("grobner", tout << "result: "; display_equation(tout, *target););
     return result ? target : 0;
 }
@@ -697,7 +697,10 @@ grobner::equation * grobner::simplify_using_processed(equation * eq) {
                 simplified = true;
                 eq         = new_eq;
             }
-        }
+            if (m_manager.canceled()) {
+                return 0;
+            }
+        }        
     }
     while (simplified);
     TRACE("grobner", tout << "simplification result: "; display_equation(tout, *eq););
@@ -749,13 +752,13 @@ grobner::equation * grobner::pick_next() {
 /**
    \brief Use the given equation to simplify processed terms.
 */
-void grobner::simplify_processed(equation * eq) {
+bool grobner::simplify_processed(equation * eq) {
     ptr_buffer<equation> to_insert;
     ptr_buffer<equation> to_remove;
     ptr_buffer<equation> to_delete;
     equation_set::iterator it  = m_processed.begin();
     equation_set::iterator end = m_processed.end();
-    for (; it != end; ++it) {
+    for (; it != end && !m_manager.canceled(); ++it) {
         equation * curr        = *it;
         m_changed_leading_term = false;
         // if the leading term is simplified, then the equation has to be moved to m_to_process
@@ -795,6 +798,7 @@ void grobner::simplify_processed(equation * eq) {
     end1 = to_delete.end();
     for (; it1 != end1; ++it1)
         del_equation(*it1);
+    return !m_manager.canceled();
 }
 
 /**
@@ -944,7 +948,8 @@ bool grobner::compute_basis_step() {
         m_equations_to_unfreeze.push_back(eq);
         eq = new_eq;
     }
-    simplify_processed(eq);
+    if (m_manager.canceled()) return false;
+    if (!simplify_processed(eq)) return false;
     superpose(eq);
     m_processed.insert(eq);
     simplify_to_process(eq);
@@ -954,7 +959,7 @@ bool grobner::compute_basis_step() {
 
 bool grobner::compute_basis(unsigned threshold) {
     compute_basis_init();
-    while (m_num_new_equations < threshold) {
+    while (m_num_new_equations < threshold && !m_manager.canceled()) {
         if (compute_basis_step()) return true;
     }
     return false;

src/math/grobner/grobner.h

@@ -175,7 +175,7 @@ protected:
 
     equation * pick_next();
 
-    void simplify_processed(equation * eq);
+    bool simplify_processed(equation * eq);
 
     void simplify_to_process(equation * eq);
 

src/model/model_evaluator.cpp

@@ -114,7 +114,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         result_pr = 0;
         family_id fid = f->get_family_id();
-        if (num == 0 && (fid == null_family_id || m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f))) {
+        bool is_uninterp = fid != null_family_id && m().get_plugin(fid)->is_considered_uninterpreted(f);
+        if (num == 0 && (fid == null_family_id || is_uninterp)) {
             expr * val = m_model.get_const_interp(f);
             if (val != 0) {
                 result = val;
@@ -150,7 +151,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
                     st = m_f_rw.mk_eq_core(args[0], args[1], result);
                 else if (s_fid == m_seq_rw.get_fid())
                     st = m_seq_rw.mk_eq_core(args[0], args[1], result);
-                else if (fid == m_ar_rw.get_fid())
+                else if (s_fid == m_ar_rw.get_fid())
                     st = mk_array_eq(args[0], args[1], result);
                 if (st != BR_FAILED)
                     return st;

src/muz/fp/dl_cmds.cpp

@@ -219,9 +219,17 @@ public:
 
     virtual void set_next_arg(cmd_context & ctx, func_decl* t) {
         m_target = t;
+        if (t->get_family_id() != null_family_id) {
+            throw cmd_exception("Invalid query argument, expected uinterpreted function name, but argument is interpreted");
+        }
+        datalog::context& dlctx = m_dl_ctx->dlctx();
+        if (!dlctx.get_predicates().contains(t)) {
+            throw cmd_exception("Invalid query argument, expected a predicate registered as a relation");
+        }
     }
 
     virtual void prepare(cmd_context & ctx) { 
+        ctx.m(); // ensure manager is initialized.
         parametric_cmd::prepare(ctx);
         m_target   = 0; 
     }
@@ -383,6 +391,7 @@ public:
     virtual unsigned get_arity() const { return VAR_ARITY; }
 
     virtual void prepare(cmd_context & ctx) {
+        ctx.m(); // ensure manager is initialized.
         m_arg_idx = 0; 
         m_query_arg_idx = 0; 
         m_domain = 0;
@@ -443,6 +452,7 @@ public:
     virtual unsigned get_arity() const { return 2; }
 
     virtual void prepare(cmd_context & ctx) {
+        ctx.m(); // ensure manager is initialized.
         m_arg_idx = 0; 
     }
     virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { 

src/opt/opt_cmds.cpp

@@ -141,6 +141,13 @@ class alternate_min_max_cmd : public cmd {
     app_ref_vector*      m_vars;
     svector<bool>        m_is_max;
     unsigned             m_position;
+
+    app_ref_vector& vars(cmd_context& ctx) {
+        if (!m_vars) {
+            m_vars = alloc(app_ref_vector, ctx.m());
+        }
+        return *m_vars;
+    }
 public:
     alternate_min_max_cmd():
         cmd("min-max"),
@@ -150,6 +157,7 @@ public:
     
     virtual void reset(cmd_context & ctx) { 
         dealloc(m_vars);
+        m_vars = 0;
         m_is_max.reset();
         m_position = 0;
     }
@@ -176,8 +184,7 @@ public:
             }
             else {
                 m_is_max.push_back(is_max);
-                if (!m_vars) m_vars = alloc(app_ref_vector, ctx.m());
+                vars(ctx).push_back(ctx.m().mk_const(ctx.find_func_decl(slist[i])));
-                m_vars->push_back(ctx.m().mk_const(ctx.find_func_decl(slist[i])));
             }
         }
         ++m_position;
@@ -188,8 +195,8 @@ public:
             throw cmd_exception("malformed objective term: it cannot be a quantifier or bound variable");
         }
         ++m_position;
-        if (!m_vars) m_vars = alloc(app_ref_vector, ctx.m());
+        get_opt(ctx).min_max(to_app(t), vars(ctx), m_is_max);
-        get_opt(ctx).min_max(to_app(t), *m_vars, m_is_max);
+        reset(ctx);
     }
 
     virtual void failure_cleanup(cmd_context & ctx) {

src/opt/opt_context.cpp

@@ -218,11 +218,9 @@ namespace opt {
         import_scoped_state(); 
         normalize();
         internalize();
-        update_solver();
+        qe::max_min_opt max_min(m, m_params);
-        solver& s = get_solver();
+        max_min.add(m_hard_constraints);
-        s.assert_expr(m_hard_constraints);
+        return max_min.check(is_max, vars, t);
-        std::cout << "min-max is TBD\n";
-        return l_undef;
     }
 
 

src/qe/qe_arith.cpp

@@ -51,13 +51,6 @@ namespace qe {
         }
         return is_divides(a, e1, e2, k, t) || is_divides(a, e2, e1, k, t);
     }
-
-
-#if 0
-        obj_map<expr, unsigned> m_expr2var;
-        ptr_vector<expr>        m_var2expr;
-
-#endif
     
     struct arith_project_plugin::imp {
 
@@ -88,18 +81,23 @@ namespace qe {
             }            
         }
 
-        void insert_mul(expr* x, rational const& v, obj_map<expr, rational>& ts)
+        void insert_mul(expr* x, rational const& v, obj_map<expr, rational>& ts) {
-        {
             rational w;
             if (ts.find(x, w)) {
                 ts.insert(x, w + v);
             }
             else {
+                TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << "\n";);
                 ts.insert(x, v); 
             }
         }
 
-        void linearize(model& model, opt::model_based_opt& mbo, expr* lit, obj_map<expr, unsigned>& tids) {
+        //
+        // extract linear inequalities from literal 'lit' into the model-based optimization manager 'mbo'.
+        // It uses the current model to choose values for conditionals and it primes mbo with the current
+        // interpretation of sub-expressions that are treated as variables for mbo.
+        // 
+        void linearize(opt::model_based_opt& mbo, model& model, expr* lit, obj_map<expr, unsigned>& tids) {
             obj_map<expr, rational> ts;
             rational c(0), mul(1);
             expr_ref t(m);
@@ -112,19 +110,19 @@ namespace qe {
             SASSERT(!m.is_not(lit));
             if (a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) {
                 if (is_not) mul.neg();
-                linearize(model, mul, e1, c, ts);
+                linearize(mbo, model, mul, e1, c, ts, tids);
-                linearize(model, -mul, e2, c, ts);
+                linearize(mbo, model, -mul, e2, c, ts, tids);
                 ty = is_not ? opt::t_lt : opt::t_le;
             }
             else if (a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1)) {
                 if (is_not) mul.neg();
-                linearize(model,  mul, e1, c, ts);
+                linearize(mbo, model,  mul, e1, c, ts, tids);
-                linearize(model, -mul, e2, c, ts);
+                linearize(mbo, model, -mul, e2, c, ts, tids);
                 ty = is_not ? opt::t_le: opt::t_lt;
             }
             else if (m.is_eq(lit, e1, e2) && !is_not && is_arith(e1)) {
-                linearize(model,  mul, e1, c, ts);
+                linearize(mbo, model,  mul, e1, c, ts, tids);
-                linearize(model, -mul, e2, c, ts);
+                linearize(mbo, model, -mul, e2, c, ts, tids);
                 ty = opt::t_eq;
             }  
             else if (m.is_distinct(lit) && !is_not && is_arith(to_app(lit)->get_arg(0))) {
@@ -137,55 +135,63 @@ namespace qe {
                 UNREACHABLE();
             }            
             else {
+                TRACE("qe", tout << "Skipping " << mk_pp(lit, m) << "\n";);
                 return;
             }
-            if (ty == opt::t_lt && is_int()) {
+#if 0
+            TBD for integers
+            if (ty == opt::t_lt && false) {
                 c += rational(1);
                 ty = opt::t_le;
             }            
+#endif
             vars coeffs;
-            extract_coefficients(ts, tids, coeffs);
+            extract_coefficients(mbo, model, ts, tids, coeffs);
             mbo.add_constraint(coeffs, c, ty);
         }
 
-        void linearize(model& model, rational const& mul, expr* t, rational& c, obj_map<expr, rational>& ts) {
+        //
+        // convert linear arithmetic term into an inequality for mbo.
+        // 
+        void linearize(opt::model_based_opt& mbo, model& model, rational const& mul, expr* t, rational& c, 
+                       obj_map<expr, rational>& ts, obj_map<expr, unsigned>& tids) {
             expr* t1, *t2, *t3;
             rational mul1;
             expr_ref val(m);
             if (a.is_mul(t, t1, t2) && is_numeral(model, t1, mul1)) {
-                linearize(model, mul* mul1, t2, c, ts);
+                linearize(mbo, model, mul* mul1, t2, c, ts, tids);
             }
             else if (a.is_mul(t, t1, t2) && is_numeral(model, t2, mul1)) {
-                linearize(model, mul* mul1, t1, c, ts);
+                linearize(mbo, model, mul* mul1, t1, c, ts, tids);
             }
             else if (a.is_add(t)) {
                 app* ap = to_app(t);
                 for (unsigned i = 0; i < ap->get_num_args(); ++i) {
-                    linearize(model, mul, ap->get_arg(i), c, ts);
+                    linearize(mbo, model, mul, ap->get_arg(i), c, ts, tids);
                 }
             }
             else if (a.is_sub(t, t1, t2)) {
-                linearize(model, mul, t1, c, ts);
+                linearize(mbo, model, mul, t1, c, ts, tids);
-                linearize(model, -mul, t2, c, ts);
+                linearize(mbo, model, -mul, t2, c, ts, tids);
             }
             else if (a.is_uminus(t, t1)) {
-                linearize(model, -mul, t1, c, ts);
+                linearize(mbo, model, -mul, t1, c, ts, tids);
             }
             else if (a.is_numeral(t, mul1)) {
                 c += mul*mul1;
             }
-            else if (extract_mod(model, t, val)) {
-                insert_mul(val, mul, ts);
-            }
             else if (m.is_ite(t, t1, t2, t3)) {
                 VERIFY(model.eval(t1, val));
                 SASSERT(m.is_true(val) || m.is_false(val));
                 TRACE("qe", tout << mk_pp(t1, m) << " := " << val << "\n";);
                 if (m.is_true(val)) {
-                    linearize(model, mul, t2, c, ts);
+                    linearize(mbo, model, mul, t2, c, ts, tids);
+                    linearize(mbo, model, t1, tids);
                 }
                 else {
-                    linearize(model, mul, t3, c, ts);
+                    expr_ref not_t1(mk_not(m, t1), m);
+                    linearize(mbo, model, mul, t3, c, ts, tids);
+                    linearize(mbo, model, not_t1, tids);
                 }
             }
             else {
@@ -193,6 +199,9 @@ namespace qe {
             }
         }
 
+        //
+        // extract linear terms from t into c and ts.
+        // 
         void is_linear(model& model, rational const& mul, expr* t, rational& c, expr_ref_vector& ts) {
             expr* t1, *t2, *t3;
             rational mul1;
@@ -245,7 +254,9 @@ namespace qe {
             }
         }
 
-
+        // 
+        // extract linear inequalities from literal lit.
+        // 
         bool is_linear(model& model, expr* lit, bool& found_eq) {
             rational c(0), mul(1);
             expr_ref t(m);
@@ -977,13 +988,13 @@ namespace qe {
             // extract objective function.
             vars coeffs;
             rational c(0), mul(1);
-            linearize(mdl, mul, t, c, ts);
+            linearize(mbo, mdl, mul, t, c, ts, tids);
-            extract_coefficients(ts, tids, coeffs);
+            extract_coefficients(mbo, mdl, ts, tids, coeffs);
             mbo.set_objective(coeffs, c);
 
             // extract linear constraints
             for (unsigned i = 0; i < fmls.size(); ++i) {
-                linearize(mdl, mbo, fmls[i], tids);
+                linearize(mbo, mdl, fmls[i], tids);
             }
             
             // find optimal value
@@ -1021,13 +1032,21 @@ namespace qe {
             return value;
         }
 
-        void extract_coefficients(obj_map<expr, rational> const& ts, obj_map<expr, unsigned>& tids, vars& coeffs) {
+        void extract_coefficients(opt::model_based_opt& mbo, model& model, obj_map<expr, rational> const& ts, obj_map<expr, unsigned>& tids, vars& coeffs) {
             coeffs.reset();
             obj_map<expr, rational>::iterator it = ts.begin(), end = ts.end();
             for (; it != end; ++it) {
                 unsigned id;
                 if (!tids.find(it->m_key, id)) {
-                    id = tids.size();
+                    rational r;
+                    expr_ref val(m);
+                    if (model.eval(it->m_key, val) && a.is_numeral(val, r)) {
+                        id = mbo.add_var(r);
+                    }
+                    else {
+                        TRACE("qe", tout << "extraction of coefficients cancelled\n";);
+                        return;
+                    }
                     tids.insert(it->m_key, id);
                 }
                 coeffs.push_back(var(id, it->m_value));                

src/qe/qsat.cpp

@@ -548,8 +548,7 @@ namespace qe {
             unsigned m_num_rounds;        
             stats() { reset(); }
             void reset() { memset(this, 0, sizeof(*this)); }
-        };
+        };        
-        
         
         ast_manager&               m;
         params_ref                 m_params;
@@ -619,7 +618,7 @@ namespace qe {
         }
 
         kernel& get_kernel(unsigned j) {        
-            if (is_exists(j)) {
+            if (m_kernel_ex || is_exists(j)) {
                 return m_ex; 
             }
             else {
@@ -704,96 +703,7 @@ namespace qe {
             for (unsigned i = 0; i < vars.size(); ++i) {
                 m_pred_abs.fmc()->insert(vars[i]->get_decl());
             }
-        }
+        }        
-
-#if 0
-        void hoist_ite(expr_ref& fml) {
-            app* ite;
-            scoped_ptr<expr_replacer> replace = mk_default_expr_replacer(m);
-            th_rewriter rewriter(m);
-            while (find_ite(fml, ite)) {
-                expr* cond, *th, *el;
-                VERIFY(m.is_ite(ite, cond, th, el));
-                expr_ref tmp1(fml, m), tmp2(fml, m);
-                replace->apply_substitution(cond, m.mk_true(), tmp1);
-                replace->apply_substitution(cond, m.mk_false(), tmp2);
-                fml = m.mk_ite(cond, tmp1, tmp2);
-                rewriter(fml);
-            }
-        }
-
-        bool find_ite(expr* e, app*& ite) {
-            ptr_vector<expr> todo;
-            todo.push_back(e);
-            ast_mark visited;
-            while(!todo.empty()) {
-                e = todo.back();
-                todo.pop_back();
-                if (visited.is_marked(e)) {
-                    continue;
-                }        
-                visited.mark(e, true);
-                if (m.is_ite(e) && !m.is_bool(e)) {
-                    ite = to_app(e);
-                    return true;
-                }
-                if (is_app(e)) {
-                    app* a = to_app(e);
-                    todo.append(a->get_num_args(), a->get_args());
-                }
-            }
-            return false;
-        }
-
-        // slower
-        void hoist_ite2(expr_ref& fml) {
-            obj_map<expr,expr*> result;
-            expr_ref_vector trail(m);
-            ptr_vector<expr> todo, args;
-            todo.push_back(fml);
-            
-            while (!todo.empty()) {
-                expr* e = todo.back();
-                if (result.contains(e)) {
-                    todo.pop_back();
-                    continue;
-                }
-                if (!is_app(e)) {
-                    todo.pop_back();
-                    result.insert(e, e);
-                    continue;
-                }
-                app* a = to_app(e);
-                expr* r;
-                unsigned sz = a->get_num_args();
-                args.reset();
-                for (unsigned i = 0; i < sz; ++i) {
-                    if (result.find(a->get_arg(i), r)) {
-                        args.push_back(r);
-                    }
-                    else {
-                        todo.push_back(a->get_arg(i));
-                    }
-                }
-                if (sz == args.size()) {
-                    r = m.mk_app(a->get_decl(), args.size(), args.c_ptr());
-                    trail.push_back(r);
-                    if (m.is_bool(e) && m.get_basic_family_id() != a->get_family_id()) {
-                        expr_ref fml(r, m);
-                        hoist_ite(fml);
-                        trail.push_back(fml);
-                        r = fml;
-                    }
-                    result.insert(e, r);
-                    todo.pop_back();
-                }                               
-            }
-            fml = result.find(fml);
-        }
-#endif
-
-
-        
 
         void initialize_levels() {
             // initialize levels.
@@ -1160,7 +1070,8 @@ namespace qe {
             m_level(0),
             m_mode(mode),
             m_avars(m),
-            m_free_vars(m)
+            m_free_vars(m),
+            m_kernel_ex(false)
         {
             reset();
         }
@@ -1326,6 +1237,92 @@ namespace qe {
             m_ex.assert_expr(bound);            
         }
 
+
+        bool         m_kernel_ex;
+
+        lbool max_min(expr_ref_vector const& fmls, svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
+            m_kernel_ex = true;
+            // Assume this is the only call to check.
+            expr_ref_vector defs(m);
+            app_ref_vector free_vars(m), vars1(m);
+            expr_ref fml = mk_and(fmls);
+            m_pred_abs.get_free_vars(fml, free_vars);
+            m_pred_abs.abstract_atoms(fml, defs);
+            fml = m_pred_abs.mk_abstract(fml);
+            get_kernel(0).k().assert_expr(mk_and(defs));
+            get_kernel(0).k().assert_expr(fml);
+            obj_hashtable<app> var_set;
+            for (unsigned i = 0; i < vars.size(); ++i) {
+                var_set.insert(vars[i]);
+            }
+            for (unsigned i = 0; i < free_vars.size(); ++i) {
+                app* v = free_vars[i].get();
+                if (!var_set.contains(v)) {
+                    vars1.push_back(v);
+                }
+            }
+            // 
+            // Insert all variables in alternating list of max/min objectives.
+            // By convention, the outer-most level is max.
+            //
+            bool is_m = true;
+            for (unsigned i = 0; i < vars.size(); ++i) {
+                if (is_m != is_max[i]) {
+                    m_vars.push_back(vars1);
+                    vars1.reset();       
+                    is_m = is_max[i];
+                }
+                vars1.push_back(vars[i]);
+            }
+            m_vars.push_back(vars1);
+            
+            return max_min();
+        }
+
+        lbool max_min() {
+            while (true) {
+                ++m_stats.m_num_rounds;
+                check_cancel();
+                expr_ref_vector asms(m_asms);
+                m_pred_abs.get_assumptions(m_model.get(), asms);
+                //
+                // TBD: add bound to asms.
+                // 
+                smt::kernel& k = get_kernel(m_level).k();
+                lbool res = k.check(asms);
+                switch (res) {
+                case l_true:
+                    k.get_model(m_model);
+                    SASSERT(validate_model(asms));
+                    TRACE("qe", k.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); );
+                    // 
+                    // TBD: compute new bound on objective.
+                    // 
+                    push();
+                    break;
+                case l_false:
+                    switch (m_level) {
+                    case 0: return l_false;
+                    case 1:
+                        // TBD
+                        break;
+                    default:
+                        if (m_model.get()) {
+                            project(asms); 
+                        }
+                        else {
+                            pop(1);
+                        }
+                        break; 
+                    }
+                    break;
+                case l_undef:
+                    return res;
+                }
+            }
+            return l_undef;
+        }
+
     };
 
     lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl, params_ref const& p) {
@@ -1333,6 +1330,50 @@ namespace qe {
         qsat qs(m, p, qsat_maximize);
         return qs.maximize(fmls, t, mdl, value);
     }    
+
+
+    struct max_min_opt::imp {
+
+        expr_ref_vector m_fmls;
+        qsat            m_qsat;
+
+        imp(ast_manager& m, params_ref const& p): 
+            m_fmls(m), 
+            m_qsat(m, p, qsat_maximize)
+        {}
+
+        void add(expr* e) {
+            m_fmls.push_back(e);
+        }
+
+        lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
+            return m_qsat.max_min(m_fmls, is_max, vars, t);
+        }
+
+    };
+
+    max_min_opt::max_min_opt(ast_manager& m, params_ref const& p) {
+        m_imp = alloc(imp, m, p);
+    }
+
+    max_min_opt::~max_min_opt() {
+        dealloc(m_imp);
+    }
+
+    void max_min_opt::add(expr* e) {
+        m_imp->add(e);
+    }
+
+    void max_min_opt::add(expr_ref_vector const& fmls) {
+        for (unsigned i = 0; i < fmls.size(); ++i) {
+            add(fmls[i]);
+        }
+    }
+
+    lbool max_min_opt::check(svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
+        return m_imp->check(is_max, vars, t);
+    }
+
 };
 
 tactic * mk_qsat_tactic(ast_manager& m, params_ref const& p) {
@@ -1350,94 +1391,3 @@ tactic * mk_qe_rec_tactic(ast_manager& m, params_ref const& p) {
 
 
 
-#if 0
-
-    class min_max_opt {
-        struct imp;
-        imp* m_imp;
-    public:
-        min_max_opt(ast_manager& m);
-        ~min_max_opt();
-        void add(expr* e);
-        void add(expr_ref_vector const& fmls);
-        lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t);
-    };
-
-    struct min_max_opt::imp {
-        ast_manager&    m;
-        expr_ref_vector m_fmls;
-        pred_abs        m_pred_abs;
-        qe::mbp         m_mbp;
-        kernel          m_kernel;
-        vector<app_ref_vector> m_vars;
-
-        imp(ast_manager& m): 
-            m(m), 
-            m_fmls(m), 
-            m_pred_abs(m), 
-            m_mbp(m),
-            m_kernel(m) {}
-
-        void add(expr* e) {
-            m_fmls.push_back(e);
-        }
-
-        lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
-            // Assume this is the only call to check.
-            expr_ref_vector defs(m);
-            app_ref_vector free_vars(m), vars1(m);
-            expr_ref fml = mk_and(m_fmls);
-            m_pred_abs.get_free_vars(fml, free_vars);
-            m_pred_abs.abstract_atoms(fml, defs);
-            fml = m_pred_abs.mk_abstract(fml);
-            m_kernel.assert_expr(mk_and(defs));
-            m_kernel.assert_expr(fml);
-            obj_hashtable<app> var_set;
-            for (unsigned i = 0; i < vars.size(); ++i) {
-                var_set.insert(vars[i]);
-            }
-            for (unsigned i = 0; i < free_vars.size(); ++i) {
-                app* v = free_vars[i].get();
-                if (!var_set.contains(v)) {
-                    vars1.push_back(v);
-                }
-            }
-            bool is_m = is_max[0];
-            for (unsigned i = 0; i < vars.size(); ++i) {
-                if (is_m != is_max[i]) {
-                    m_vars.push_back(vars1);
-                    vars1.reset();       
-                    is_m = is_max[i];
-                }
-                vars1.push_back(vars[i]);
-            }
-
-            // TBD
-            
-            return l_undef;
-        }
-    };
-
-    min_max_opt::min_max_opt(ast_manager& m) {
-        m_imp = alloc(imp, m);
-    }
-
-    min_max_opt::~min_max_opt() {
-        dealloc(m_imp);
-    }
-
-    void min_max_opt::add(expr* e) {
-        m_imp->add(e);
-    }
-
-    void min_max_opt::add(expr_ref_vector const& fmls) {
-        for (unsigned i = 0; i < fmls.size(); ++i) {
-            add(fmls[i]);
-        }
-    }
-
-    lbool min_max_opt::check(svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
-        return m_imp->check(is_max, vars, t);
-    }
-
-#endif

src/qe/qsat.h

@@ -114,6 +114,17 @@ namespace qe {
         void collect_statistics(statistics& st) const;
     };
 
+    class max_min_opt {
+        struct imp;
+        imp* m_imp;
+    public:
+        max_min_opt(ast_manager& m, params_ref const& p = params_ref());
+        ~max_min_opt();
+        void add(expr* e);
+        void add(expr_ref_vector const& fmls);
+        lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t);
+    };
+
     lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl, params_ref const& p);
 
 }

src/smt/theory_fpa.cpp

@@ -85,8 +85,63 @@ namespace smt {
     }
 
     void theory_fpa::fpa2bv_converter_wrapped::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
-        // TODO: This introduces temporary variables/func_decls that should be filtered in the end.
+        // TODO: This introduces temporary func_decls that should be filtered in the end.
-        fpa2bv_converter::mk_uninterpreted_function(f, num, args, result);
+
+        TRACE("t_fpa", tout << "UF: " << mk_ismt2_pp(f, m) << std::endl; );
+        SASSERT(f->get_arity() == num);
+        
+        expr_ref_buffer new_args(m);
+
+        for (unsigned i = 0; i < num; i++) {
+            if (is_float(args[i]) || is_rm(args[i])) {
+                expr_ref ai(m), wrapped(m);
+                ai = args[i];                
+                wrapped = m_th.wrap(ai);
+                new_args.push_back(wrapped);
+                m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, m.get_sort(ai)), ai));
+            }
+            else
+                new_args.push_back(args[i]);
+        }
+
+        func_decl * fd;
+        if (m_uf2bvuf.find(f, fd))
+            mk_uninterpreted_output(f->get_range(), fd, new_args, result);
+        else {
+            sort_ref_buffer new_domain(m);
+
+            for (unsigned i = 0; i < f->get_arity(); i++) {
+                sort * di = f->get_domain()[i];
+                if (is_float(di))
+                    new_domain.push_back(m_bv_util.mk_sort(m_util.get_sbits(di) + m_util.get_ebits(di)));
+                else if (is_rm(di))
+                    new_domain.push_back(m_bv_util.mk_sort(3));
+                else
+                    new_domain.push_back(di);
+            }
+
+            sort * frng = f->get_range();
+            sort_ref rng(frng, m);
+            if (m_util.is_float(frng))
+                rng = m_bv_util.mk_sort(m_util.get_ebits(frng) + m_util.get_sbits(frng));
+            else if (m_util.is_rm(frng))
+                rng = m_bv_util.mk_sort(3);
+
+            func_decl_ref fbv(m);
+            fbv = m.mk_fresh_func_decl(new_domain.size(), new_domain.c_ptr(), rng);            
+            TRACE("t_fpa", tout << "New UF func_decl : " << mk_ismt2_pp(fbv, m) << std::endl;);
+
+            m_uf2bvuf.insert(f, fbv);
+            m.inc_ref(f);
+            m.inc_ref(fbv);
+
+            mk_uninterpreted_output(frng, fbv, new_args, result);
+        }
+
+        expr_ref fapp(m);
+        fapp = m.mk_app(f, num, args);
+        m_extra_assertions.push_back(m.mk_eq(fapp, result));        
+        TRACE("t_fpa", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; );
     }
 
     expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) {
@@ -284,30 +339,40 @@ namespace smt {
     app_ref theory_fpa::wrap(expr * e) {
         SASSERT(!m_fpa_util.is_wrap(e));
         ast_manager & m = get_manager();
-        sort * e_srt = m.get_sort(e);
+        app_ref res(m);
 
-        func_decl *w;
+        if (is_app(e) &&
+            to_app(e)->get_family_id() == get_family_id() &&
+            to_app(e)->get_decl_kind() == OP_FPA_FP) {
+            expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };            
+            res = m_bv_util.mk_concat(3, cargs);
+            m_th_rw((expr_ref&)res);
+        }
+        else {
+            sort * e_srt = m.get_sort(e);
+            func_decl * w;
 
-        if (!m_wraps.find(e_srt, w)) {
+            if (!m_wraps.find(e_srt, w)) {
-            SASSERT(!m_wraps.contains(e_srt));
+                SASSERT(!m_wraps.contains(e_srt));
 
-            sort * bv_srt;
+                sort * bv_srt;
-            if (m_converter.is_rm(e_srt))
+                if (m_converter.is_rm(e_srt))
-                bv_srt = m_bv_util.mk_sort(3);
+                    bv_srt = m_bv_util.mk_sort(3);
-            else {
+                else {
-                SASSERT(m_converter.is_float(e_srt));
+                    SASSERT(m_converter.is_float(e_srt));
-                unsigned ebits = m_fpa_util.get_ebits(e_srt);
+                    unsigned ebits = m_fpa_util.get_ebits(e_srt);
-                unsigned sbits = m_fpa_util.get_sbits(e_srt);
+                    unsigned sbits = m_fpa_util.get_sbits(e_srt);
-                bv_srt = m_bv_util.mk_sort(ebits + sbits);
+                    bv_srt = m_bv_util.mk_sort(ebits + sbits);
+                }
+
+                w = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt);
+                m_wraps.insert(e_srt, w);
+                m.inc_ref(w);
             }
 
-            w = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt);
+            res = m.mk_app(w, e);
-            m_wraps.insert(e_srt, w);
-            m.inc_ref(w);
         }
-
+        
-        app_ref res(m);
-        res = m.mk_app(w, e);
         return res;
     }
 
@@ -389,59 +454,6 @@ namespace smt {
         return res;
     }
 
-#if 0
-    expr_ref theory_fpa::convert_uf(expr * e) {
-        SASSERT(is_app(e));
-        ast_manager & m = get_manager();
-        expr_ref res(m);
-
-        app * a = to_app(e);
-        func_decl * f = a->get_decl();
-        sort * const * domain = f->get_domain();
-        unsigned arity = f->get_arity();
-
-        expr_ref_buffer new_args(m);
-        expr_ref unwrapped(m);
-
-        for (unsigned i = 0; i < arity; i++) {
-            expr * ai = a->get_arg(i);
-            if (m_fpa_util.is_float(ai) || m_fpa_util.is_rm(ai)) {
-                if (m_fpa_util.is_unwrap(ai))
-                    unwrapped = ai;
-                else {
-                    // unwrapped = unwrap(wrap(ai), domain[i]);
-                    // assert_cnstr(m.mk_eq(unwrapped, ai));
-                    // assert_cnstr();
-                    unwrapped = convert_term(ai);
-                }
-
-                new_args.push_back(unwrapped);
-                TRACE("t_fpa_detail", tout << "UF arg(" << i << ") = " << mk_ismt2_pp(unwrapped, get_manager()) << "\n";);
-            }
-            else
-                new_args.push_back(ai);
-        }
-
-        sort * rng = f->get_range();
-        if (m_fpa_util.is_float(rng)) {
-            unsigned sbits = m_fpa_util.get_sbits(rng);
-            unsigned bv_sz = m_fpa_util.get_ebits(rng) + sbits;
-            expr_ref wrapped(m);
-            wrapped = wrap(m.mk_app(f, new_args.size(), new_args.c_ptr()));
-
-            m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped),
-                              m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped),
-                              m_bv_util.mk_extract(sbits - 2, 0, wrapped),
-                              res);
-        }
-        else
-            res = m.mk_app(f, new_args.size(), new_args.c_ptr());
-
-        TRACE("t_fpa_detail", tout << "UF call = " << mk_ismt2_pp(res, get_manager()) << "\n";);
-        return res;
-    }
-#endif
-
     expr_ref theory_fpa::convert_conversion_term(expr * e) {
         /* This is for the conversion functions fp.to_* */
         ast_manager & m = get_manager();
@@ -606,6 +618,7 @@ namespace smt {
         // Therefore, we translate and assert them here.
         fpa_op_kind k = (fpa_op_kind)term->get_decl_kind();
         switch (k) {
+        case OP_FPA_TO_FP:
         case OP_FPA_TO_UBV:
         case OP_FPA_TO_SBV:
         case OP_FPA_TO_REAL:
@@ -966,4 +979,16 @@ namespace smt {
             out << r->get_id() << " --> " << mk_ismt2_pp(n, m) << std::endl;
         }
     }
+
+    bool theory_fpa::include_func_interp(func_decl * f) {
+        TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;);
+        func_decl * wt;
+
+        if (m_wraps.find(f->get_range(), wt) || m_unwraps.find(f->get_range(), wt))
+            return wt == f;
+        else if (m_converter.is_uf2bvuf(f) || m_converter.is_special(f))
+            return false;
+        else
+            return true;
+    }
 };

src/smt/theory_fpa.h

@@ -83,7 +83,7 @@ namespace smt {
             virtual ~fpa2bv_converter_wrapped() {}
             virtual void mk_const(func_decl * f, expr_ref & result);
             virtual void mk_rm_const(func_decl * f, expr_ref & result);
-            virtual void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+            virtual void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result);            
 
             virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y);
             virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y);
@@ -112,7 +112,7 @@ namespace smt {
                 result.append(m_deps);
             }
 
-            virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values);
+            virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values);            
         };
 
         class fpa_rm_value_proc : public model_value_proc {
@@ -163,6 +163,7 @@ namespace smt {
         virtual char const * get_name() const { return "fpa"; }
 
         virtual model_value_proc * mk_value(enode * n, model_generator & mg);
+        virtual bool include_func_interp(func_decl * f);
 
         void assign_eh(bool_var v, bool is_true);
         virtual void relevant_eh(app * n);

src/smt/theory_seq.cpp

@@ -2823,6 +2823,7 @@ void theory_seq::add_elim_string_axiom(expr* n) {
     - len(unit(u)) = 1              if x = unit(u)
     - len(str) = str.length()       if x = str
     - len(empty) = 0                if x = empty
+    - len(int.to.str(i)) >= 1       if x = int.to.str(i) and more generally if i = 0 then 1 else 1+floor(log(|i|))
     - len(x) >= 0                   otherwise
  */
 void theory_seq::add_length_axiom(expr* n) {
@@ -2837,16 +2838,17 @@ void theory_seq::add_length_axiom(expr* n) {
         m_rewrite(len);
         SASSERT(n != len);
         add_axiom(mk_eq(len, n, false));
-        if (!ctx.at_base_level()) {
+    }
-            m_trail_stack.push(push_replay(alloc(replay_axiom, m, n)));
+    else if (m_util.str.is_itos(x)) {
-        }
+        add_axiom(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(1))));
     }
     else {
         add_axiom(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));
-        if (!ctx.at_base_level()) {
-            m_trail_stack.push(push_replay(alloc(replay_axiom, m, n)));
-        }
     }
+    if (!ctx.at_base_level()) {
+        m_trail_stack.push(push_replay(alloc(replay_axiom, m, n)));
+    }
+
 }
 
 

src/tactic/bv/bvarray2uf_rewriter.cpp

@@ -163,6 +163,59 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
         result = m_manager.mk_distinct_expanded(num, args);
         res = BR_REWRITE1;
     }
+    else if (m_manager.is_term_ite(f) && is_bv_array(f->get_range())) {
+        expr_ref c(args[0], m_manager);
+        func_decl_ref f_t(mk_uf_for_array(args[1]), m_manager);
+        func_decl_ref f_f(mk_uf_for_array(args[2]), m_manager);
+
+        TRACE("bvarray2uf_rw", tout << "(ite " << c << ", " << f_t->get_name()
+            << ", " << f_f->get_name() << ")" << std::endl;);
+
+        sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[1])) };
+        symbol names[1] = { symbol("x") };
+        var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
+
+        app_ref f_a(m_manager), f_ta(m_manager), f_fa(m_manager);
+        f_a = m_manager.mk_app(f, num, args);
+        f_ta = m_manager.mk_app(f_t, x.get());
+        f_fa = m_manager.mk_app(f_f, x.get());
+
+        app_ref e(m_manager);
+        func_decl_ref itefd(m_manager);
+        e = m_manager.mk_ite(c, f_ta, f_fa);
+
+        func_decl * bv_f = 0;
+        if (!m_arrays_fs.find(f_a, bv_f)) {
+            sort * domain = get_index_sort(args[1]);
+            sort * range = get_value_sort(args[1]);
+            bv_f = m_manager.mk_fresh_func_decl("f_t", "", 1, &domain, range);
+            TRACE("bvarray2uf_rw", tout << mk_ismt2_pp(e, m_manager) << " -> " << bv_f->get_name() << std::endl; );
+            if (is_uninterp_const(e)) {
+                if (m_emc)
+                    m_emc->insert(e->get_decl(),
+                        m_array_util.mk_as_array(m_manager.get_sort(e), bv_f));
+            }
+            else if (m_fmc)
+                m_fmc->insert(bv_f);
+            m_arrays_fs.insert(e, bv_f);
+            m_manager.inc_ref(e);
+            m_manager.inc_ref(bv_f);
+        }
+
+        expr_ref q(m_manager), body(m_manager);
+        body = m_manager.mk_eq(m_manager.mk_app(bv_f, x), e);
+        q = m_manager.mk_forall(1, sorts, names, body);
+        extra_assertions.push_back(q);
+
+        result = m_array_util.mk_as_array(f->get_range(), bv_f);
+
+        TRACE("bvarray2uf_rw", tout << "result: " << mk_ismt2_pp(result, m_manager) << ")" << std::endl;);
+        res = BR_DONE;
+        
+    }
+    else if (f->get_family_id() == m_manager.get_basic_family_id() && is_bv_array(f->get_range())) {
+        NOT_IMPLEMENTED_YET();
+    }
     else if (f->get_family_id() == null_family_id) {
         TRACE("bvarray2uf_rw", tout << "UF APP: " << f->get_name() << std::endl; );
 

src/test/qe_arith.cpp

@@ -280,12 +280,170 @@ static void test2(char const *ex) {
     ctx.assert_expr(pr1);
     ctx.assert_expr(npr2);
     VERIFY(l_false == ctx.check());
-    ctx.pop(1);
+    ctx.pop(1);       
-    
-    
 }
 
+typedef opt::model_based_opt::var var_t;
+
+static void mk_var(unsigned x, app_ref& v) {
+    ast_manager& m = v.get_manager();
+    arith_util a(m);
+    std::ostringstream strm;
+    strm << "v" << x;
+    v = m.mk_const(symbol(strm.str().c_str()), a.mk_real());
+}
+
+static void mk_term(vector<var_t> const& vars, rational const& coeff, app_ref& term) {
+    ast_manager& m = term.get_manager();
+    expr_ref_vector ts(m);
+    arith_util a(m);
+
+    for (unsigned i = 0; i < vars.size(); ++i) {
+        app_ref var(m);
+        mk_var(vars[i].m_id, var);
+        rational coeff = vars[i].m_coeff;
+        ts.push_back(a.mk_mul(a.mk_numeral(coeff, false), var));
+    }
+    ts.push_back(a.mk_numeral(coeff, a.mk_real()));
+    term = a.mk_add(ts.size(), ts.c_ptr());    
+}
+
+static void add_random_ineq(
+    expr_ref_vector& fmls, 
+    opt::model_based_opt& mbo,
+    random_gen& r,
+    svector<int>  const& values,
+    unsigned max_vars,
+    unsigned max_coeff) 
+{
+    ast_manager& m = fmls.get_manager();
+    arith_util a(m);
+
+    unsigned num_vars = values.size();
+    uint_set used_vars;
+    vector<var_t> vars;
+    int value = 0;
+    for (unsigned i = 0; i < max_vars; ++i) {
+        unsigned x = r(num_vars);
+        if (used_vars.contains(x)) {
+            continue;
+        }
+        used_vars.insert(x);
+        int coeff = r(max_coeff + 1);
+        if (coeff == 0) {
+            continue;
+        }
+        unsigned sign = r(2);
+        coeff = sign == 0 ? coeff : -coeff;
+        vars.push_back(var_t(x, rational(coeff)));
+        value += coeff*values[x];
+    }
+    unsigned abs_value = value < 0 ? - value : value;
+    // value + k <= 0
+    // k <= - value
+    // range for k is 2*|value|
+    // k <= - value - range
+    opt::ineq_type rel = opt::t_le;
+
+    int coeff = 0;
+    if (r(4) == 0) {
+        rel = opt::t_eq;
+        coeff = -value;
+    }
+    else {
+        if (abs_value > 0) {
+            coeff = -value - r(2*abs_value);
+        }
+        else {
+            coeff = 0;
+        }
+        if (coeff != -value && r(3) == 0) {
+            rel = opt::t_lt;
+        }   
+    }
+    expr_ref fml(m);
+    app_ref t1(m);
+    app_ref t2(a.mk_numeral(rational(0), a.mk_real()), m);
+    mk_term(vars, rational(coeff), t1);
+    switch (rel) {
+    case opt::t_eq:
+        fml = m.mk_eq(t1, t2);
+        break;
+    case opt::t_lt:
+        fml = a.mk_lt(t1, t2);
+        break;
+    case opt::t_le:
+        fml = a.mk_le(t1, t2);
+        break;
+    }
+    fmls.push_back(fml);
+    mbo.add_constraint(vars, rational(coeff), rel);
+}
+
+static void test_maximize(opt::model_based_opt& mbo, ast_manager& m, unsigned num_vars, expr_ref_vector const& fmls, app* t) {
+    qe::arith_project_plugin plugin(m);
+    model mdl(m);
+    expr_ref bound(m);
+    arith_util a(m);
+    for (unsigned i = 0; i < num_vars; ++i) {
+        app_ref var(m);
+        mk_var(i, var);
+        rational val = mbo.get_value(i);
+        mdl.register_decl(var->get_decl(), a.mk_numeral(val, false));
+    }
+    opt::inf_eps value1 = plugin.maximize(fmls, mdl, t, bound);
+    opt::inf_eps value2 = mbo.maximize();    
+    std::cout << "optimal: " << value1 << " " << value2 << "\n";
+    mbo.display(std::cout);
+}
+                        
+static void check_random_ineqs(random_gen& r, ast_manager& m, unsigned num_vars, unsigned max_value, unsigned num_ineqs, unsigned max_vars, unsigned max_coeff) {
+    opt::model_based_opt mbo;
+    expr_ref_vector fmls(m);
+
+    svector<int> values;
+    for (unsigned i = 0; i < num_vars; ++i) {
+        values.push_back(r(max_value + 1));
+        mbo.add_var(rational(values.back()));
+    }
+    for (unsigned i = 0; i < num_ineqs; ++i) {
+        add_random_ineq(fmls, mbo, r, values, max_vars, max_coeff);
+    }
+
+    vector<var_t> vars;
+    vars.reset();
+    vars.push_back(var_t(0, rational(2)));
+    vars.push_back(var_t(1, rational(-2)));
+    mbo.set_objective(vars, rational(0));
+       
+
+    mbo.display(std::cout);
+    app_ref t(m);
+    mk_term(vars, rational(0), t);
+    
+    test_maximize(mbo, m, num_vars, fmls, t);
+    
+    for (unsigned i = 0; i < values.size(); ++i) {
+        std::cout << i << ": " << values[i] << " -> " << mbo.get_value(i) << "\n";
+    }
+}
+
+static void check_random_ineqs() {
+    random_gen r(1);
+    ast_manager m;
+    reg_decl_plugins(m);    
+
+    for (unsigned i = 0; i < 100; ++i) {
+        check_random_ineqs(r, m, 4, 5, 5, 3, 6);
+    }
+}
+
+
+
+
 void tst_qe_arith() {
+    check_random_ineqs();
+    return;
 //    enable_trace("qe");
     testI(example8);    
     testR(example7);

src/util/mpf.cpp

@@ -1095,7 +1095,7 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o
             TRACE("mpf_dbg", tout << "tie= " << tie << "; <tie = " << less_than_tie << "; >tie = " << more_than_tie << std::endl;);
             if (tie) {
                 if ((rm == MPF_ROUND_NEAREST_TEVEN && m_mpz_manager.is_odd(div)) ||
-                    (rm == MPF_ROUND_NEAREST_TAWAY && m_mpz_manager.is_even(div))) {
+                    (rm == MPF_ROUND_NEAREST_TAWAY)) {
                     TRACE("mpf_dbg", tout << "div++ (1)" << std::endl;);
                     m_mpz_manager.inc(div);
                 }
@@ -1214,11 +1214,194 @@ void mpf_manager::to_ieee_bv_mpz(const mpf & x, scoped_mpz & o) {
     }
 }
 
+void mpf_manager::renormalize(unsigned ebits, unsigned sbits, mpf_exp_t & exp, mpz & sig) {
+    if (m_mpz_manager.is_zero(sig))
+        return;
+
+    const mpz & pg = m_powers2(sbits);
+    while (m_mpz_manager.ge(sig, pg)) {
+        m_mpz_manager.machine_div2k(sig, 1);
+        exp++;
+    }
+    
+    const mpz & pl = m_powers2(sbits-1);
+    while (m_mpz_manager.lt(sig, pl)) {
+        m_mpz_manager.mul2k(sig, 1);
+        exp--;
+    }
+}
+
+void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & exp_diff, bool partial) {
+    unsigned ebits = x.ebits;
+    unsigned sbits = x.sbits;
+    
+    SASSERT(-1 <= exp_diff && exp_diff < INT64_MAX);
+    SASSERT(exp_diff < ebits+sbits || partial);
+
+    signed int D = (signed int)(exp_diff);
+    mpf_exp_t N = sbits-1;
+
+    TRACE("mpf_dbg_rem", tout << "x=" << to_string(x) << std::endl;
+                         tout << "y=" << to_string(y) << std::endl;
+                         tout << "d=" << D << std::endl;
+                         tout << "partial=" << partial << std::endl;);
+
+    SASSERT(m_mpz_manager.lt(x.significand, m_powers2(sbits)));
+    SASSERT(m_mpz_manager.ge(x.significand, m_powers2(sbits - 1)));
+    SASSERT(m_mpz_manager.lt(y.significand, m_powers2(sbits)));
+    SASSERT(m_mpz_manager.ge(y.significand, m_powers2(sbits - 1)));
+
+    // 1. Compute a/b        
+    bool x_div_y_sgn = x.sign != y.sign;
+    mpf_exp_t x_div_y_exp = D;
+    scoped_mpz x_sig_shifted(m_mpz_manager), x_div_y_sig_lrg(m_mpz_manager), x_div_y_rem(m_mpz_manager);
+    scoped_mpz x_rem_y_sig(m_mpz_manager);
+    m_mpz_manager.mul2k(x.significand, 2*sbits + 2, x_sig_shifted);
+    m_mpz_manager.machine_div_rem(x_sig_shifted, y.significand, x_div_y_sig_lrg, x_div_y_rem); // rem useful?
+    // x/y is in x_diuv_y_sig_lrg and has sbits+3 extra bits.
+
+    TRACE("mpf_dbg_rem", tout << "X/Y_exp=" << x_div_y_exp << std::endl;
+                         tout << "X/Y_sig_lrg=" << m_mpz_manager.to_string(x_div_y_sig_lrg) << std::endl;
+                         tout << "X/Y_rem=" << m_mpz_manager.to_string(x_div_y_rem) << std::endl;
+                         tout << "X/Y~=" << to_string_hexfloat(x_div_y_sgn, x_div_y_exp, x_div_y_sig_lrg, ebits, sbits, sbits+3) << std::endl;);
+
+    // 2. Round a/b to integer Q/QQ
+    bool Q_sgn = x_div_y_sgn;
+    mpf_exp_t Q_exp = x_div_y_exp;
+    scoped_mpz Q_sig(m_mpz_manager), Q_rem(m_mpz_manager);
+    unsigned Q_shft = (sbits-1) + (sbits+3) -  (unsigned) (partial ? N :Q_exp);
+    if (partial) {        
+        // Round according to MPF_ROUND_TOWARD_ZERO
+        SASSERT(0 < N && N < Q_exp && Q_exp < INT_MAX);
+        m_mpz_manager.machine_div2k(x_div_y_sig_lrg, Q_shft, Q_sig);
+    }
+    else {
+        // Round according to MPF_ROUND_NEAREST_TEVEN
+        m_mpz_manager.machine_div_rem(x_div_y_sig_lrg, m_powers2(Q_shft), Q_sig, Q_rem);
+        const mpz & shiftm1_p = m_powers2(Q_shft-1);
+        bool tie = m_mpz_manager.eq(Q_rem, shiftm1_p);
+        bool more_than_tie = m_mpz_manager.gt(Q_rem, shiftm1_p);
+        TRACE("mpf_dbg_rem", tout << "tie= " << tie << "; >tie= " << more_than_tie << std::endl;);
+        if ((tie && m_mpz_manager.is_odd(Q_sig)) || more_than_tie)
+            m_mpz_manager.inc(Q_sig);
+    }
+    m_mpz_manager.mul2k(Q_sig, Q_shft);
+    m_mpz_manager.machine_div2k(Q_sig, sbits+3);
+    renormalize(ebits, sbits, Q_exp, Q_sig);
+
+    TRACE("mpf_dbg_rem", tout << "Q_exp=" << Q_exp << std::endl;
+                         tout << "Q_sig=" << m_mpz_manager.to_string(Q_sig) << std::endl;
+                         tout << "Q=" << to_string_hexfloat(Q_sgn, Q_exp, Q_sig, ebits, sbits, 0) << std::endl;);
+        
+    if ((D == -1 || partial) && m_mpz_manager.is_zero(Q_sig))
+        return; // This means x % y = x.
+
+    // no extra bits in Q_sig.
+    SASSERT(!m_mpz_manager.is_zero(Q_sig));
+    SASSERT(m_mpz_manager.lt(Q_sig, m_powers2(sbits)));
+    SASSERT(m_mpz_manager.ge(Q_sig, m_powers2(sbits - 1)));
+
+
+    // 3. Compute Y*Q / Y*QQ*2^{D-N}
+    bool YQ_sgn = y.sign ^ Q_sgn;
+    scoped_mpz YQ_sig(m_mpz_manager);
+    mpf_exp_t YQ_exp = Q_exp + y.exponent;
+    m_mpz_manager.mul(y.significand, Q_sig, YQ_sig);    
+    renormalize(ebits, 2*sbits-1, YQ_exp, YQ_sig); // YQ_sig has `sbits-1' extra bits.
+
+    TRACE("mpf_dbg_rem", tout << "YQ_sgn=" << YQ_sgn << std::endl;
+                         tout << "YQ_exp=" << YQ_exp << std::endl;
+                         tout << "YQ_sig=" << m_mpz_manager.to_string(YQ_sig) << std::endl;
+                         tout << "YQ=" << to_string_hexfloat(YQ_sgn, YQ_exp, YQ_sig, ebits, sbits, sbits-1) << std::endl;);
+
+    // `sbits-1' extra bits in YQ_sig.    
+    SASSERT(m_mpz_manager.lt(YQ_sig, m_powers2(2*sbits-1)));
+    SASSERT(m_mpz_manager.ge(YQ_sig, m_powers2(2*sbits-2)) || YQ_exp <= mk_bot_exp(ebits));
+
+    // 4. Compute X-Y*Q    
+    mpf_exp_t X_YQ_exp = x.exponent;
+    scoped_mpz X_YQ_sig(m_mpz_manager);
+    mpf_exp_t exp_delta = exp(x) - YQ_exp;
+    TRACE("mpf_dbg_rem", tout << "exp_delta=" << exp_delta << std::endl;);
+    SASSERT(INT_MIN < exp_delta && exp_delta <= INT_MAX);
+    scoped_mpz minuend(m_mpz_manager), subtrahend(m_mpz_manager);
+
+    scoped_mpz x_sig_lrg(m_mpz_manager);
+    m_mpz_manager.mul2k(x.significand, sbits-1, x_sig_lrg); // sbits-1 extra bits into x
+
+    m_mpz_manager.set(minuend, x_sig_lrg);
+    m_mpz_manager.set(subtrahend, YQ_sig);
+
+    SASSERT(m_mpz_manager.lt(minuend, m_powers2(2*sbits-1)));
+    SASSERT(m_mpz_manager.ge(minuend, m_powers2(2*sbits-2)));
+    SASSERT(m_mpz_manager.lt(subtrahend, m_powers2(2*sbits-1)));
+    SASSERT(m_mpz_manager.ge(subtrahend, m_powers2(2*sbits-2)));
+    
+    if (exp_delta != 0) {
+        scoped_mpz sticky_rem(m_mpz_manager);
+        m_mpz_manager.set(sticky_rem, 0);
+        if (exp_delta > sbits+5)
+            sticky_rem.swap(subtrahend);        
+        else if (exp_delta > 0)
+            m_mpz_manager.machine_div_rem(subtrahend, m_powers2((unsigned)exp_delta), subtrahend, sticky_rem);        
+        else {
+            SASSERT(exp_delta < 0);
+            exp_delta = -exp_delta;
+            m_mpz_manager.mul2k(subtrahend, (int)exp_delta);
+        }
+        if (!m_mpz_manager.is_zero(sticky_rem) && m_mpz_manager.is_even(subtrahend))
+            m_mpz_manager.inc(subtrahend);
+        TRACE("mpf_dbg_rem", tout << "aligned subtrahend=" << m_mpz_manager.to_string(subtrahend) << std::endl;);
+    }
+           
+    m_mpz_manager.sub(minuend, subtrahend, X_YQ_sig);
+    TRACE("mpf_dbg_rem", tout << "X_YQ_sig'=" << m_mpz_manager.to_string(X_YQ_sig) << std::endl;);
+
+    bool neg = m_mpz_manager.is_neg(X_YQ_sig);
+    if (neg) m_mpz_manager.neg(X_YQ_sig);
+    bool X_YQ_sgn = ((!x.sign && !YQ_sgn && neg) ||
+                      (x.sign &&  YQ_sgn && !neg) ||
+                      (x.sign && !YQ_sgn));
+
+    // 5. Rounding
+    if (m_mpz_manager.is_zero(X_YQ_sig))
+        mk_zero(ebits, sbits, x.sign, x);
+    else {
+        renormalize(ebits, 2*sbits-1, X_YQ_exp, X_YQ_sig);
+
+        TRACE("mpf_dbg_rem", tout << "minuend=" << m_mpz_manager.to_string(minuend) << std::endl;
+                             tout << "subtrahend=" << m_mpz_manager.to_string(subtrahend) << std::endl;
+                             tout << "X_YQ_sgn=" << X_YQ_sgn << std::endl;
+                             tout << "X_YQ_exp=" << X_YQ_exp << std::endl;
+                             tout << "X_YQ_sig=" << m_mpz_manager.to_string(X_YQ_sig) << std::endl;        
+                             tout << "X-YQ=" << to_string_hexfloat(X_YQ_sgn, X_YQ_exp, X_YQ_sig, ebits, sbits, sbits-1) << std::endl;);
+
+        // `sbits-1' extra bits in X_YQ_sig
+        SASSERT(m_mpz_manager.lt(X_YQ_sig, m_powers2(2*sbits-1)));
+        scoped_mpz rnd_bits(m_mpz_manager);
+        m_mpz_manager.machine_div_rem(X_YQ_sig, m_powers2(sbits-1), X_YQ_sig, rnd_bits);
+        TRACE("mpf_dbg_rem", tout << "final sticky=" << m_mpz_manager.to_string(rnd_bits) << std::endl; );
+
+        // Round to nearest, ties to even.
+        if (m_mpz_manager.eq(rnd_bits, mpz(32))) { // tie. 
+            if (m_mpz_manager.is_odd(X_YQ_sig)) {
+                m_mpz_manager.inc(X_YQ_sig);
+            }
+        }
+        else if (m_mpz_manager.gt(rnd_bits, mpz(32)))
+            m_mpz_manager.inc(X_YQ_sig);
+
+        set(x, ebits, sbits, X_YQ_sgn, X_YQ_exp, X_YQ_sig);
+    }
+
+    TRACE("mpf_dbg_rem", tout << "partial remainder = " << to_string_hexfloat(x) << std::endl;);
+}
+
 void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
     SASSERT(x.sbits == y.sbits && x.ebits == y.ebits);
 
-    TRACE("mpf_dbg", tout << "X = " << to_string(x) << std::endl;);
+    TRACE("mpf_dbg_rem", tout << "X = " << to_string(x) << "=" << to_string_hexfloat(x) << std::endl;
-    TRACE("mpf_dbg", tout << "Y = " << to_string(y) << std::endl;);
+                         tout << "Y = " << to_string(y) << "=" << to_string_hexfloat(y) << std::endl;);
 
     if (is_nan(x) || is_nan(y))
         mk_nan(x.ebits, x.sbits, o);
@@ -1231,58 +1414,35 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
     else if (is_zero(x))
         set(o, x);
     else {
-        // This is a generalized version of the algorithm for FPREM1 in the Intel
+        SASSERT(is_regular(x) && is_regular(y));
+
+        // This is a generalized version of the algorithm for FPREM1 in the `Intel
         // 64 and IA-32 Architectures Software Developer's Manual',
-        // Section 3-402 Vol. 2A FPREM1-Partial Remainder'.
+        // Section 3-402 Vol. 2A `FPREM1-Partial Remainder'.
         scoped_mpf ST0(*this), ST1(*this);
         set(ST0, x);
         set(ST1, y);
+        unpack(ST0, true);
+        unpack(ST1, true);
 
-        const mpf_exp_t B = x.sbits-1; // max bits per iteration.
+        const mpf_exp_t B = x.sbits;
         mpf_exp_t D;
         do {
-            D = ST0.exponent() - ST1.exponent();
+            if (ST0.exponent() < ST1.exponent() - 1) {
-            TRACE("mpf_dbg_rem", tout << "st0=" << to_string_hexfloat(ST0) << std::endl;
+                D = 0;                    
-                                 tout << "st1=" << to_string_hexfloat(ST1) << std::endl;
-                                 tout << "D=" << D << std::endl;);
-
-            if (D < B) {
-                scoped_mpf ST0_DIV_ST1(*this), Q(*this), ST1_MUL_Q(*this), ST0p(*this);
-                div(MPF_ROUND_NEAREST_TEVEN, ST0, ST1, ST0_DIV_ST1);
-                round_to_integral(MPF_ROUND_NEAREST_TEVEN, ST0_DIV_ST1, Q);
-                mul(MPF_ROUND_NEAREST_TEVEN, ST1, Q, ST1_MUL_Q);
-                sub(MPF_ROUND_NEAREST_TEVEN, ST0, ST1_MUL_Q, ST0p);
-                TRACE("mpf_dbg_rem", tout << "ST0/ST1=" << to_string_hexfloat(ST0_DIV_ST1) << std::endl;
-                                     tout << "Q=" << to_string_hexfloat(Q) << std::endl;
-                                     tout << "ST1*Q=" << to_string_hexfloat(ST1_MUL_Q) << std::endl;
-                                     tout << "ST0'=" << to_string_hexfloat(ST0p) << std::endl;);
-                set(ST0, ST0p);
             }
             else {
-                const mpf_exp_t N = B;
+                D = ST0.exponent() - ST1.exponent();
-                scoped_mpf ST0_DIV_ST1(*this), QQ(*this), ST1_MUL_QQ(*this), ST0p(*this);
+                partial_remainder(ST0.get(), ST1.get(), D, (D >= B));
-                div(MPF_ROUND_TOWARD_ZERO, ST0, ST1, ST0_DIV_ST1);
-                ST0_DIV_ST1.get().exponent -= D - N;
-                round_to_integral(MPF_ROUND_TOWARD_ZERO, ST0_DIV_ST1, QQ);
-                mul(MPF_ROUND_NEAREST_TEVEN, ST1, QQ, ST1_MUL_QQ);
-                ST1_MUL_QQ.get().exponent += D - N;
-                sub(MPF_ROUND_NEAREST_TEVEN, ST0, ST1_MUL_QQ, ST0p);
-                TRACE("mpf_dbg_rem", tout << "ST0/ST1/2^{D-N}=" << to_string_hexfloat(ST0_DIV_ST1) << std::endl;
-                                     tout << "QQ=" << to_string_hexfloat(QQ) << std::endl;
-                                     tout << "ST1*QQ*2^{D-N}=" << to_string_hexfloat(ST1_MUL_QQ) << std::endl;
-                                     tout << "ST0'=" << to_string_hexfloat(ST0p) << std::endl;);
-                SASSERT(!eq(ST0, ST0p));
-                set(ST0, ST0p);
             }
+        } while (D >= B && !ST0.is_zero());
 
-            SASSERT(ST0.exponent() - ST1.exponent() <= D);
+        m_mpz_manager.mul2k(ST0.significand(), 3);
-        } while (D >= B);
+        set(o, x.ebits, x.sbits, MPF_ROUND_TOWARD_ZERO, ST0);
-
+        round(MPF_ROUND_NEAREST_TEVEN, o);
-        set(o, ST0);
-        if (is_zero(o))
-            o.sign = x.sign;
     }
 
+    TRACE("mpf_dbg_rem", tout << "R = " << to_string(o) << "=" << to_string_hexfloat(o) << std::endl; );
     TRACE("mpf_dbg", tout << "REMAINDER = " << to_string(o) << std::endl;);
 }
 
@@ -1365,7 +1525,7 @@ std::string mpf_manager::to_string(mpf const & x) {
     }
 
     //DEBUG_CODE(
-    //   res += " " + to_string_hexfloat(x);
+    //   res += " " + to_string_raw(x);
     //);
 
     return res;
@@ -1407,6 +1567,19 @@ std::string mpf_manager::to_string_raw(mpf const & x) {
     return res;
 }
 
+std::string mpf_manager::to_string_hexfloat(bool sgn, mpf_exp_t exp, scoped_mpz const & sig, unsigned ebits, unsigned sbits, unsigned rbits) {
+    scoped_mpf q(*this);
+    scoped_mpz q_sig(m_mpz_manager);
+    m_mpz_manager.set(q_sig, sig);
+    if (rbits != 0) m_mpz_manager.div(q_sig, m_powers2(rbits), q_sig); // restore scale
+    if (m_mpz_manager.ge(q_sig, m_powers2(sbits-1)))
+        m_mpz_manager.sub(q_sig, m_powers2(sbits-1), q_sig); // strip hidden bit
+    else if (exp == mk_min_exp(ebits))
+        exp = mk_bot_exp(ebits);
+    set(q, ebits, sbits, sgn, exp, q_sig);
+    return to_string(q.get());
+}
+
 std::string mpf_manager::to_string_hexfloat(mpf const & x) {
     std::stringstream ss("");
     std::ios::fmtflags ff = ss.setf(std::ios_base::hex | std::ios_base::uppercase |

src/util/mpf.h

@@ -185,9 +185,6 @@ public:
     void mk_pinf(unsigned ebits, unsigned sbits, mpf & o);
     void mk_ninf(unsigned ebits, unsigned sbits, mpf & o);
 
-    std::string to_string_raw(mpf const & a);
-    std::string to_string_hexfloat(mpf const & a);
-
     unsynch_mpz_manager & mpz_manager(void) { return m_mpz_manager; }
     unsynch_mpq_manager & mpq_manager(void) { return m_mpq_manager; }
 
@@ -226,6 +223,9 @@ protected:
     void round(mpf_rounding_mode rm, mpf & o);
     void round_sqrt(mpf_rounding_mode rm, mpf & o);
 
+    void renormalize(unsigned ebits, unsigned sbits, mpf_exp_t & exp, mpz & sig);
+    void partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & exp_diff, bool partial);
+
     void mk_round_inf(mpf_rounding_mode rm, mpf & o);
 
     // Convert x into a mpz numeral. zm is the manager that owns o.
@@ -284,6 +284,9 @@ protected:
         }
     };
 
+    std::string to_string_raw(mpf const & a);
+    std::string to_string_hexfloat(mpf const & a);    
+    std::string to_string_hexfloat(bool sgn, mpf_exp_t exp, scoped_mpz const & sig, unsigned ebits, unsigned sbits, unsigned rbits);
 public:
     powers2 m_powers2;
 };
@@ -291,6 +294,7 @@ public:
 class scoped_mpf : public _scoped_numeral<mpf_manager> {
     friend class mpf_manager;
     mpz & significand() { return get().significand; }
+    const mpz & significand() const { return get().significand; }
     bool sign() const { return get().sign; }
     mpf_exp_t exponent() const { return get().exponent; }
     unsigned sbits() const { return get().sbits; }