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

src/api/api_ast.cpp

@@ -24,6 +24,7 @@ Revision History:
 #include"bv_decl_plugin.h"
 #include"datatype_decl_plugin.h"
 #include"array_decl_plugin.h"
+#include"pb_decl_plugin.h"
 #include"ast_translation.h"
 #include"ast_pp.h"
 #include"ast_ll_pp.h"
@@ -1081,7 +1082,6 @@ extern "C" {
             case OP_BSREM_I:
             case OP_BUREM_I:
             case OP_BSMOD_I:
-
                 return Z3_OP_UNINTERPRETED;
             default:
                 UNREACHABLE();
@@ -1090,9 +1090,10 @@ extern "C" {
         }
         if (mk_c(c)->get_dt_fid() == _d->get_family_id()) {
             switch(_d->get_decl_kind()) {
-            case OP_DT_CONSTRUCTOR: return Z3_OP_DT_CONSTRUCTOR;
-            case OP_DT_RECOGNISER:  return Z3_OP_DT_RECOGNISER;
-            case OP_DT_ACCESSOR:    return Z3_OP_DT_ACCESSOR;
+            case OP_DT_CONSTRUCTOR:  return Z3_OP_DT_CONSTRUCTOR;
+            case OP_DT_RECOGNISER:   return Z3_OP_DT_RECOGNISER;
+            case OP_DT_ACCESSOR:     return Z3_OP_DT_ACCESSOR;
+            case OP_DT_UPDATE_FIELD: return Z3_OP_DT_UPDATE_FIELD;
             default:
                 UNREACHABLE();
                 return Z3_OP_UNINTERPRETED;
@@ -1186,6 +1187,15 @@ extern "C" {
             }
         }
 
+        if (mk_c(c)->get_pb_fid() == _d->get_family_id()) {
+            switch(_d->get_decl_kind()) {
+            case OP_PB_LE: return Z3_OP_PB_LE;
+            case OP_PB_GE: return Z3_OP_PB_GE;
+            case OP_AT_MOST_K: return Z3_OP_PB_AT_MOST;
+            default: UNREACHABLE();
+            }
+        }
+
         return Z3_OP_UNINTERPRETED;                
         Z3_CATCH_RETURN(Z3_OP_UNINTERPRETED);
     }

src/api/api_config_params.cpp

@@ -37,9 +37,7 @@ extern "C" {
         catch (z3_exception & ex) {
             // The error handler is only available for contexts
             // Just throw a warning.
-            std::ostringstream buffer;
-            buffer << "Error setting " << param_id << ", " << ex.msg();
-            warning_msg(buffer.str().c_str());
+            warning_msg(ex.msg());
         }
     }
 
@@ -64,9 +62,7 @@ extern "C" {
         catch (z3_exception & ex) {
             // The error handler is only available for contexts
             // Just throw a warning.
-            std::ostringstream buffer;
-            buffer << "Error setting " << param_id << ": " << ex.msg();
-            warning_msg(buffer.str().c_str());
+            warning_msg(ex.msg());
             return Z3_FALSE;
         }
     }
@@ -92,9 +88,7 @@ extern "C" {
         catch (z3_exception & ex) {
             // The error handler is only available for contexts
             // Just throw a warning.
-            std::ostringstream buffer;
-            buffer << "Error setting " << param_id << ": " << ex.msg();
-            warning_msg(buffer.str().c_str());
+            warning_msg(ex.msg());
         }
     }
 

src/api/api_context.cpp

@@ -89,7 +89,7 @@ namespace api {
         m_bv_util(m()),
         m_datalog_util(m()),
         m_fpa_util(m()),
-	m_dtutil(m()),
+        m_dtutil(m()),
         m_last_result(m()),
         m_ast_trail(m()),
         m_replay_stack() {
@@ -111,6 +111,7 @@ namespace api {
         m_basic_fid = m().get_basic_family_id();
         m_arith_fid = m().mk_family_id("arith");
         m_bv_fid    = m().mk_family_id("bv");
+        m_pb_fid    = m().mk_family_id("pb");
         m_array_fid = m().mk_family_id("array");
         m_dt_fid    = m().mk_family_id("datatype");
         m_datalog_fid = m().mk_family_id("datalog_relation");
@@ -515,6 +516,11 @@ extern "C" {
         memory::initialize(0);
     }
 
+    void Z3_API Z3_finalize_memory(void) {
+        LOG_Z3_finalize_memory();
+        memory::finalize();
+    }
+
     Z3_error_code Z3_API Z3_get_error_code(Z3_context c) {
         LOG_Z3_get_error_code(c);
         return mk_c(c)->get_error_code();

src/api/api_context.h

@@ -78,6 +78,7 @@ namespace api {
         family_id                  m_bv_fid;
         family_id                  m_dt_fid;
         family_id                  m_datalog_fid;
+        family_id                  m_pb_fid;
         family_id                  m_fpa_fid;
         datatype_decl_plugin *     m_dt_plugin;
         
@@ -127,6 +128,7 @@ namespace api {
         family_id get_bv_fid() const { return m_bv_fid; }
         family_id get_dt_fid() const { return m_dt_fid; }
         family_id get_datalog_fid() const { return m_datalog_fid; }
+        family_id get_pb_fid() const { return m_pb_fid; }
         family_id get_fpa_fid() const { return m_fpa_fid; }
         datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; }
 

src/api/api_datalog.cpp

@@ -125,7 +125,7 @@ namespace api {
                 return "unknown";
             }
         }
-        std::string to_string(unsigned num_queries, expr*const* queries) {
+        std::string to_string(unsigned num_queries, expr* const* queries) {
             std::stringstream str;
             m_context.display_smt2(num_queries, queries, str);
             return str.str();
@@ -466,13 +466,16 @@ extern "C" {
         ast_manager& m = mk_c(c)->m();
         Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
         mk_c(c)->save_object(v);
-        expr_ref_vector rules(m);
+        expr_ref_vector rules(m), queries(m);
         svector<symbol> names;
         
-        to_fixedpoint_ref(d)->ctx().get_rules_as_formulas(rules, names);
+        to_fixedpoint_ref(d)->ctx().get_rules_as_formulas(rules, queries, names);
         for (unsigned i = 0; i < rules.size(); ++i) {
             v->m_ast_vector.push_back(rules[i].get());
         }
+        for (unsigned i = 0; i < queries.size(); ++i) {
+            v->m_ast_vector.push_back(m.mk_not(queries[i].get()));
+        }
         RETURN_Z3(of_ast_vector(v));
         Z3_CATCH_RETURN(0);
     }

src/api/api_datatype.cpp

@@ -476,7 +476,7 @@ extern "C" {
             return 0;
         }
         ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
-        if (idx >= decls->size()) {
+        if (!decls || idx >= decls->size()) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
@@ -506,9 +506,9 @@ extern "C" {
             RETURN_Z3(0);
         }
         ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
-        if (idx >= decls->size()) {
+        if (!decls || idx >= decls->size()) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
-            return 0;
+            RETURN_Z3(0);
         }
         func_decl* decl = (*decls)[idx];
         decl = dt_util.get_constructor_recognizer(decl);
@@ -529,7 +529,7 @@ extern "C" {
             RETURN_Z3(0);            
         }
         ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
-        if (idx_c >= decls->size()) {
+        if (!decls || idx_c >= decls->size()) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
@@ -618,4 +618,25 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_ast Z3_datatype_update_field(
+        __in Z3_context c,  __in Z3_func_decl f, __in Z3_ast t, __in Z3_ast v) {        
+        Z3_TRY;
+        LOG_Z3_datatype_update_field(c, f, t, v);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        func_decl* _f      = to_func_decl(f);
+        expr* _t = to_expr(t);
+        expr* _v = to_expr(v);  
+        expr* args[2] = { _t, _v };
+        sort* domain[2] = { m.get_sort(_t), m.get_sort(_v) };
+        parameter param(_f);
+        func_decl * d = m.mk_func_decl(mk_c(c)->get_array_fid(), OP_DT_UPDATE_FIELD, 1, &param, 2, domain);
+        app* r = m.mk_app(d, 2, args);
+        mk_c(c)->save_ast_trail(r);
+        check_sorts(c, r);
+        RETURN_Z3(of_ast(r));
+        Z3_CATCH_RETURN(0);
+    }
+
+
 };

src/api/api_fpa.cpp

@@ -712,7 +712,7 @@ extern "C" {
 
     unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s) {
         Z3_TRY;
-        LOG_Z3_fpa_get_ebits(c, s);
+        LOG_Z3_fpa_get_sbits(c, s);
         RESET_ERROR_CODE();
         CHECK_NON_NULL(s, 0);
         return mk_c(c)->fpautil().get_sbits(to_sort(s));
@@ -765,7 +765,30 @@ extern "C" {
         mpqm.display_decimal(ss, q, sbits);
         return mk_c(c)->mk_external_string(ss.str());
         Z3_CATCH_RETURN("");
+    }
 
+    Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(__in Z3_context c, __in Z3_ast t, __out __uint64 * n) {
+        Z3_TRY;
+        LOG_Z3_fpa_get_numeral_significand_uint64(c, t, n);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();
+        unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
+        fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
+        scoped_mpf val(mpfm);
+        bool r = plugin->is_numeral(to_expr(t), val);
+        if (!r) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        const mpz & z = mpfm.sig(val);
+        if (!mpzm.is_uint64(z)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        *n = mpzm.get_uint64(z);
+        return 1;
+        Z3_CATCH_RETURN(0);
     }
 
     Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t) {
@@ -794,7 +817,7 @@ extern "C" {
 
     Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(__in Z3_context c, __in Z3_ast t, __out __int64 * n) {
         Z3_TRY;
-        LOG_Z3_fpa_get_numeral_exponent_string(c, t);
+        LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n);
         RESET_ERROR_CODE();
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();

src/api/api_interp.cpp

@@ -290,10 +290,10 @@ extern "C" {
             }
         }
         else {
-            model_ref _m;
-            m_solver.get()->get_model(_m);
+            model_ref mr;
+            m_solver.get()->get_model(mr);
             Z3_model_ref *tmp_val = alloc(Z3_model_ref);
-            tmp_val->m_model = _m.get();
+            tmp_val->m_model = mr.get();
             mk_c(c)->save_object(tmp_val);
             *model = of_model(tmp_val);
         }

src/api/api_model.cpp

@@ -65,6 +65,18 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a) {
+        Z3_TRY;
+        LOG_Z3_model_has_interp(c, m, a);
+        CHECK_NON_NULL(m, 0);
+        if (to_model_ref(m)->has_interpretation(to_func_decl(a))) {
+            return Z3_TRUE;
+        } else {
+            return Z3_FALSE;
+        }
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
     Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f) {
         Z3_TRY;
         LOG_Z3_model_get_func_interp(c, m, f);

src/api/api_opt.cpp

@@ -0,0 +1,243 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    api_opt.cpp
+
+Abstract:
+    API for optimization 
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-12-3.
+
+Revision History:
+
+--*/
+#include<iostream>
+#include"z3.h"
+#include"api_log_macros.h"
+#include"api_stats.h"
+#include"api_context.h"
+#include"api_util.h"
+#include"api_model.h"
+#include"opt_context.h"
+#include"cancel_eh.h"
+#include"scoped_timer.h"
+
+
+extern "C" {
+
+    struct Z3_optimize_ref : public api::object {
+        opt::context* m_opt;
+        Z3_optimize_ref():m_opt(0) {}
+        virtual ~Z3_optimize_ref() { dealloc(m_opt); }
+    };
+    inline Z3_optimize_ref * to_optimize(Z3_optimize o) { return reinterpret_cast<Z3_optimize_ref *>(o); }
+    inline Z3_optimize of_optimize(Z3_optimize_ref * o) { return reinterpret_cast<Z3_optimize>(o); }
+    inline opt::context* to_optimize_ptr(Z3_optimize o) { return to_optimize(o)->m_opt; }
+
+    Z3_optimize Z3_API Z3_mk_optimize(Z3_context c) {
+        Z3_TRY;
+        LOG_Z3_mk_optimize(c);
+        RESET_ERROR_CODE();
+        Z3_optimize_ref * o = alloc(Z3_optimize_ref);
+        o->m_opt = alloc(opt::context,mk_c(c)->m());
+        mk_c(c)->save_object(o);
+        RETURN_Z3(of_optimize(o));
+        Z3_CATCH_RETURN(0);
+    }
+
+    void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize o) {
+        Z3_TRY;
+        LOG_Z3_optimize_inc_ref(c, o);
+        RESET_ERROR_CODE();
+        to_optimize(o)->inc_ref();
+        Z3_CATCH;
+    }
+
+    void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize o) {
+        Z3_TRY;
+        LOG_Z3_optimize_dec_ref(c, o);
+        RESET_ERROR_CODE();
+        to_optimize(o)->dec_ref();
+        Z3_CATCH;
+    }
+    
+    void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_optimize_assert(c, o, a);
+        RESET_ERROR_CODE();
+        CHECK_FORMULA(a,);        
+        to_optimize_ptr(o)->add_hard_constraint(to_expr(a));
+        Z3_CATCH;
+    }
+
+    unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id) {
+        Z3_TRY;
+        LOG_Z3_optimize_assert_soft(c, o, a, weight, id);
+        RESET_ERROR_CODE();
+        CHECK_FORMULA(a,0);        
+        rational w(weight);
+        return to_optimize_ptr(o)->add_soft_constraint(to_expr(a), w, to_symbol(id));
+        Z3_CATCH_RETURN(0);
+    }
+
+    unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t) {
+        Z3_TRY;
+        LOG_Z3_optimize_maximize(c, o, t);
+        RESET_ERROR_CODE();
+        CHECK_VALID_AST(t,0);        
+        return to_optimize_ptr(o)->add_objective(to_app(t), true);
+        Z3_CATCH_RETURN(0);
+    }
+
+    unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t) {
+        Z3_TRY;
+        LOG_Z3_optimize_minimize(c, o, t);
+        RESET_ERROR_CODE();
+        CHECK_VALID_AST(t,0);        
+        return to_optimize_ptr(o)->add_objective(to_app(t), false);
+        Z3_CATCH_RETURN(0);
+    }
+
+    void Z3_API Z3_optimize_push(Z3_context c,Z3_optimize d) {
+        Z3_TRY;
+        LOG_Z3_optimize_push(c, d);
+        RESET_ERROR_CODE();
+        to_optimize_ptr(d)->push();
+        Z3_CATCH;
+    }
+
+    void Z3_API Z3_optimize_pop(Z3_context c,Z3_optimize d) {
+        Z3_TRY;
+        LOG_Z3_optimize_pop(c, d);
+        RESET_ERROR_CODE();
+        to_optimize_ptr(d)->pop(1);
+        Z3_CATCH;
+    }
+
+
+    Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o) {
+        Z3_TRY;
+        LOG_Z3_optimize_check(c, o);
+        RESET_ERROR_CODE();
+        lbool r = l_undef;
+        cancel_eh<opt::context> eh(*to_optimize_ptr(o));
+        unsigned timeout = to_optimize_ptr(o)->get_params().get_uint("timeout", mk_c(c)->get_timeout());
+        api::context::set_interruptable si(*(mk_c(c)), eh);        
+        {
+            scoped_timer timer(timeout, &eh);
+            try {
+                r = to_optimize_ptr(o)->optimize();
+            }
+            catch (z3_exception& ex) {
+                mk_c(c)->handle_exception(ex);
+                r = l_undef;
+            }
+            // to_optimize_ref(d).cleanup();
+        }
+        return of_lbool(r);
+        Z3_CATCH_RETURN(Z3_L_UNDEF);
+    }
+
+    Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o) {
+        Z3_TRY;
+        LOG_Z3_optimize_get_model(c, o);
+        RESET_ERROR_CODE();
+        model_ref _m;
+        to_optimize_ptr(o)->get_model(_m);
+        Z3_model_ref * m_ref = alloc(Z3_model_ref); 
+        if (_m) {
+            m_ref->m_model = _m;
+        }
+        else {
+            m_ref->m_model = alloc(model, mk_c(c)->m());
+        }
+        mk_c(c)->save_object(m_ref);
+        RETURN_Z3(of_model(m_ref));
+        Z3_CATCH_RETURN(0);
+    }
+
+    void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p) {
+        Z3_TRY;
+        LOG_Z3_optimize_set_params(c, o, p);
+        RESET_ERROR_CODE();
+        param_descrs descrs;
+        to_optimize_ptr(o)->collect_param_descrs(descrs);
+        to_params(p)->m_params.validate(descrs);
+        params_ref pr = to_param_ref(p);
+        to_optimize_ptr(o)->updt_params(pr);
+        Z3_CATCH;
+    }
+    
+    Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o) {
+        Z3_TRY;
+        LOG_Z3_optimize_get_param_descrs(c, o);
+        RESET_ERROR_CODE();
+        Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);
+        mk_c(c)->save_object(d);
+        to_optimize_ptr(o)->collect_param_descrs(d->m_descrs);
+        Z3_param_descrs r = of_param_descrs(d);
+        RETURN_Z3(r);
+        Z3_CATCH_RETURN(0);
+    }
+    
+    // get lower value or current approximation
+    Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx) {
+        Z3_TRY;
+        LOG_Z3_optimize_get_lower(c, o, idx);
+        RESET_ERROR_CODE();
+        expr_ref e = to_optimize_ptr(o)->get_lower(idx);
+        mk_c(c)->save_ast_trail(e);
+        RETURN_Z3(of_expr(e));
+        Z3_CATCH_RETURN(0);
+    }
+
+    // get upper or current approximation
+    Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx) {
+        Z3_TRY;
+        LOG_Z3_optimize_get_upper(c, o, idx);
+        RESET_ERROR_CODE();
+        expr_ref e = to_optimize_ptr(o)->get_upper(idx);
+        mk_c(c)->save_ast_trail(e);
+        RETURN_Z3(of_expr(e));
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o) {
+        Z3_TRY;
+        LOG_Z3_optimize_to_string(c, o);
+        RESET_ERROR_CODE();
+        return mk_c(c)->mk_external_string(to_optimize_ptr(o)->to_string());
+        Z3_CATCH_RETURN("");
+    }
+
+    Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize d) {
+        Z3_TRY;
+        LOG_Z3_optimize_get_help(c, d);
+        RESET_ERROR_CODE();
+        std::ostringstream buffer;
+        param_descrs descrs;
+        to_optimize_ptr(d)->collect_param_descrs(descrs);
+        descrs.display(buffer);
+        return mk_c(c)->mk_external_string(buffer.str());
+        Z3_CATCH_RETURN("");
+    }
+
+    Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c,Z3_optimize d) {
+        Z3_TRY;
+        LOG_Z3_optimize_get_statistics(c, d);
+        RESET_ERROR_CODE();
+        Z3_stats_ref * st = alloc(Z3_stats_ref);
+        to_optimize_ptr(d)->collect_statistics(st->m_stats);
+        mk_c(c)->save_object(st);
+        Z3_stats r = of_stats(st);
+        RETURN_Z3(r);
+        Z3_CATCH_RETURN(0);
+    }
+
+
+
+};

src/api/api_pb.cpp

@@ -0,0 +1,61 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    api_pb.cpp
+
+Abstract:
+    API for pb theory
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-11-13.
+
+Revision History:
+
+--*/
+#include<iostream>
+#include"z3.h"
+#include"api_log_macros.h"
+#include"api_context.h"
+#include"api_util.h"
+#include"pb_decl_plugin.h"
+
+extern "C" {
+    
+    Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, 
+                               Z3_ast const args[], unsigned k) {
+        Z3_TRY;
+        LOG_Z3_mk_atmost(c, num_args, args, k);
+        RESET_ERROR_CODE();
+        parameter param(k);
+        pb_util util(mk_c(c)->m());
+        ast* a = util.mk_at_most_k(num_args, to_exprs(args), k);
+        mk_c(c)->save_ast_trail(a);
+        check_sorts(c, a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(0);
+    }
+
+
+    Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, 
+                             Z3_ast const args[], int _coeffs[],
+                             int k) {
+        Z3_TRY;
+        LOG_Z3_mk_pble(c, num_args, args, _coeffs, k);
+        RESET_ERROR_CODE();
+        pb_util util(mk_c(c)->m());
+        vector<rational> coeffs;
+        for (unsigned i = 0; i < num_args; ++i) {
+            coeffs.push_back(rational(_coeffs[i]));
+        }
+        ast* a = util.mk_le(num_args, coeffs.c_ptr(), to_exprs(args), rational(k));
+        mk_c(c)->save_ast_trail(a);
+        check_sorts(c, a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(0);
+    }
+
+
+};

src/api/api_solver.cpp

@@ -355,6 +355,10 @@ extern "C" {
         init_solver(c, s);
         Z3_stats_ref * st = alloc(Z3_stats_ref);
         to_solver_ref(s)->collect_statistics(st->m_stats);
+        unsigned long long max_mem = memory::get_max_used_memory();
+        unsigned long long mem = memory::get_allocation_size();
+        st->m_stats.update("max memory", static_cast<double>(max_mem)/(1024.0*1024.0));
+        st->m_stats.update("memory", static_cast<double>(mem)/(1024.0*1024.0));
         mk_c(c)->save_object(st);
         Z3_stats r = of_stats(st);
         RETURN_Z3(r);

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

@@ -203,7 +203,12 @@ namespace z3 {
            and in \c ts the predicates for testing if terms of the enumeration sort correspond to an enumeration.
         */
         sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
-        
+        /**
+           \brief create an uninterpreted sort with the name given by the string or symbol.
+         */
+        sort uninterpreted_sort(char const* name);
+        sort uninterpreted_sort(symbol const& name);
+
         func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
         func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
         func_decl function(symbol const&  name, sort_vector const& domain, sort const& range);
@@ -655,6 +660,7 @@ namespace z3 {
         friend expr ite(expr const & c, expr const & t, expr const & e);
 
         friend expr distinct(expr_vector const& args);
+        friend expr concat(expr const& a, expr const& b);
 
         friend expr operator==(expr const & a, expr const & b) {
             check_context(a, b);
@@ -677,7 +683,7 @@ namespace z3 {
 
         friend expr operator+(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 Z3_ast args[2] = { a, b };
                 r = Z3_mk_add(a.ctx(), 2, args);
@@ -697,7 +703,7 @@ namespace z3 {
 
         friend expr operator*(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 Z3_ast args[2] = { a, b };
                 r = Z3_mk_mul(a.ctx(), 2, args);
@@ -724,7 +730,7 @@ namespace z3 {
 
         friend expr operator/(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 r = Z3_mk_div(a.ctx(), a, b);
             }
@@ -742,7 +748,7 @@ namespace z3 {
         friend expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
 
         friend expr operator-(expr const & a) {
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith()) {
                 r = Z3_mk_unary_minus(a.ctx(), a);
             }
@@ -759,7 +765,7 @@ namespace z3 {
 
         friend expr operator-(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 Z3_ast args[2] = { a, b };
                 r = Z3_mk_sub(a.ctx(), 2, args);
@@ -779,7 +785,7 @@ namespace z3 {
 
         friend expr operator<=(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 r = Z3_mk_le(a.ctx(), a, b);
             }
@@ -798,7 +804,7 @@ namespace z3 {
 
         friend expr operator>=(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 r = Z3_mk_ge(a.ctx(), a, b);
             }
@@ -817,7 +823,7 @@ namespace z3 {
 
         friend expr operator<(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 r = Z3_mk_lt(a.ctx(), a, b);
             }
@@ -836,7 +842,7 @@ namespace z3 {
         
         friend expr operator>(expr const & a, expr const & b) {
             check_context(a, b);
-            Z3_ast r;
+            Z3_ast r = 0;
             if (a.is_arith() && b.is_arith()) {
                 r = Z3_mk_gt(a.ctx(), a, b);
             }
@@ -1108,6 +1114,13 @@ namespace z3 {
         ctx.check_error();
         return expr(ctx, r);
     }
+
+    inline expr concat(expr const& a, expr const& b) {
+        check_context(a, b);
+        Z3_ast r = Z3_mk_concat(a.ctx(), a, b);
+        a.ctx().check_error();
+        return expr(a.ctx(), r);
+    }
     
     class func_entry : public object {
         Z3_func_entry m_entry;
@@ -1176,7 +1189,7 @@ namespace z3 {
         
         expr eval(expr const & n, bool model_completion=false) const {
             check_context(*this, n);
-            Z3_ast r;
+            Z3_ast r = 0;
             Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
             check_error();
             if (status == Z3_FALSE)
@@ -1536,6 +1549,62 @@ namespace z3 {
         }
     };
 
+    class optimize : public object {
+        Z3_optimize m_opt;
+    public:
+        class handle {
+            unsigned m_h;
+        public:
+            handle(unsigned h): m_h(h) {}
+            unsigned h() const { return m_h; }
+        };
+        optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
+        ~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); }
+        operator Z3_optimize() const { return m_opt; }
+        void add(expr const& e) {
+            assert(e.is_bool());
+            Z3_optimize_assert(ctx(), m_opt, e);
+        }
+        handle add(expr const& e, unsigned weight) {
+            assert(e.is_bool());
+            std::stringstream strm;
+            strm << weight; 
+            return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0)); 
+        }
+        handle add(expr const& e, char const* weight) {
+            assert(e.is_bool());
+            return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0)); 
+        }
+        handle maximize(expr const& e) {
+            return handle(Z3_optimize_maximize(ctx(), m_opt, e));
+        }
+        handle minimize(expr const& e) {
+            return handle(Z3_optimize_minimize(ctx(), m_opt, e));
+        }
+        void push() {
+            Z3_optimize_push(ctx(), m_opt);
+        }
+        void pop() {
+            Z3_optimize_pop(ctx(), m_opt);
+        }
+        check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt); check_error(); return to_check_result(r); }
+        model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
+        void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
+        expr lower(handle const& h) {
+            Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
+            check_error();
+            return expr(ctx(), r);
+        }
+        expr upper(handle const& h) {
+            Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
+            check_error();
+            return expr(ctx(), r);
+        }
+        stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }        
+        friend std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
+        std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error();  return r; }        
+    };
+
     inline tactic fail_if(probe const & p) {
         Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
         p.check_error();
@@ -1573,6 +1642,13 @@ namespace z3 {
         for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
         return s;
     }
+    inline sort context::uninterpreted_sort(char const* name) {
+        Z3_symbol _name = Z3_mk_string_symbol(*this, name);
+        return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
+    }
+    inline sort context::uninterpreted_sort(symbol const& name) {
+        return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
+    }
 
     inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
         array<Z3_sort> args(arity);

src/api/dll/dll.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #ifdef _WINDOWS
 
 #include<windows.h>

src/api/dotnet/ASTMap.cs

@@ -98,11 +98,12 @@ namespace Microsoft.Z3
         /// <summary>
         /// The keys stored in the map.
         /// </summary>
-        public ASTVector Keys
+        public AST[] Keys
         {
             get
             {
-                return new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject));
+                ASTVector res = new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject));
+                return res.ToArray();
             }
         }
 

src/api/dotnet/ASTVector.cs

@@ -99,6 +99,138 @@ namespace Microsoft.Z3
             return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject);
         }
 
+        /// <summary>
+        /// Translates an AST vector into an AST[]
+        /// </summary>    
+        public AST[] ToArray()
+        {
+            uint n = Size;
+            AST[] res = new AST[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = AST.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into an Expr[]
+        /// </summary>    
+        public Expr[] ToExprArray()
+        {
+            uint n = Size;
+            Expr[] res = new Expr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a BoolExpr[]
+        /// </summary>    
+        public BoolExpr[] ToBoolExprArray()
+        {
+            uint n = Size;
+            BoolExpr[] res = new BoolExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (BoolExpr) Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a BitVecExpr[]
+        /// </summary>    
+        public BitVecExpr[] ToBitVecExprArray()
+        {
+            uint n = Size;
+            BitVecExpr[] res = new BitVecExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (BitVecExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a ArithExpr[]
+        /// </summary>    
+        public ArithExpr[] ToArithExprArray()
+        {
+            uint n = Size;
+            ArithExpr[] res = new ArithExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (ArithExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a ArrayExpr[]
+        /// </summary>    
+        public ArrayExpr[] ToArrayExprArray()
+        {
+            uint n = Size;
+            ArrayExpr[] res = new ArrayExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (ArrayExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a DatatypeExpr[]
+        /// </summary>    
+        public DatatypeExpr[] ToDatatypeExprArray()
+        {
+            uint n = Size;
+            DatatypeExpr[] res = new DatatypeExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (DatatypeExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a FPExpr[]
+        /// </summary>    
+        public FPExpr[] ToFPExprArray()
+        {
+            uint n = Size;
+            FPExpr[] res = new FPExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (FPExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a FPRMExpr[]
+        /// </summary>    
+        public FPRMExpr[] ToFPRMExprArray()
+        {
+            uint n = Size;
+            FPRMExpr[] res = new FPRMExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (FPRMExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a IntExpr[]
+        /// </summary>    
+        public IntExpr[] ToIntExprArray()
+        {
+            uint n = Size;
+            IntExpr[] res = new IntExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (IntExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a RealExpr[]
+        /// </summary>    
+        public RealExpr[] ToRealExprArray()
+        {
+            uint n = Size;
+            RealExpr[] res = new RealExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (RealExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
         #region Internal
         internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
         internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Contract.Requires(ctx != null); }

src/api/dotnet/Context.cs

@@ -449,6 +449,19 @@ namespace Microsoft.Z3
             return MkDatatypeSorts(MkSymbols(names), c);
         }
 
+        /// <summary>
+        /// Update a datatype field at expression t with value v.
+	/// The function performs a record update at t. The field
+	/// that is passed in as argument is updated with value v,
+	/// the remainig fields of t are unchanged.	
+        /// </summary>
+	public Expr MkUpdateField(FuncDecl field, Expr t, Expr v) 
+	{
+	    return Expr.Create(this, Native.Z3_datatype_update_field(
+	                                  nCtx, field.NativeObject,
+                                          t.NativeObject, v.NativeObject));		
+	}
+
         #endregion
         #endregion
 
@@ -2251,6 +2264,36 @@ namespace Microsoft.Z3
         }
         #endregion
 
+        #region Pseudo-Boolean constraints
+
+        /// <summary>
+        /// Create an at-most-k constraint.
+        /// </summary>
+        public BoolExpr MkAtMost(BoolExpr[] args, uint k) 
+        {
+           Contract.Requires(args != null);
+           Contract.Requires(Contract.Result<BoolExpr[]>() != null);
+           CheckContextMatch(args);
+           return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Length, 
+                                                          AST.ArrayToNative(args), k));
+        }
+
+        /// <summary>
+        /// Create a pseudo-Boolean less-or-equal constraint.
+        /// </summary>
+        public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k) 
+        {
+           Contract.Requires(args != null);
+           Contract.Requires(coeffs != null);
+           Contract.Requires(args.Length == coeffs.Length);
+           Contract.Requires(Contract.Result<BoolExpr[]>() != null);
+           CheckContextMatch(args);
+           return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length, 
+                                                          AST.ArrayToNative(args), 
+                                                          coeffs, k));
+        }
+        #endregion
+
         #region Numerals
 
         #region General Numerals
@@ -3438,6 +3481,18 @@ namespace Microsoft.Z3
         }
         #endregion
 
+        #region Optimization
+        /// <summary>
+        /// Create an Optimization context.
+        /// </summary>
+        public Optimize MkOptimize()
+        {
+            Contract.Ensures(Contract.Result<Optimize>() != null);
+
+            return new Optimize(this);
+        }
+        #endregion
+
         #region Floating-Point Arithmetic
 
         #region Rounding Modes
@@ -4383,6 +4438,7 @@ namespace Microsoft.Z3
             Contract.Invariant(m_Statistics_DRQ != null);
             Contract.Invariant(m_Tactic_DRQ != null);
             Contract.Invariant(m_Fixedpoint_DRQ != null);
+            Contract.Invariant(m_Optimize_DRQ != null);
         }
 
         readonly private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue();
@@ -4400,6 +4456,7 @@ namespace Microsoft.Z3
         readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue(10);
         readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue(10);
         readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(10);
+	readonly private Optimize.DecRefQueue m_Optimize_DRQ = new Optimize.DecRefQueue(10);
 
         /// <summary>
         /// AST DRQ
@@ -4476,6 +4533,11 @@ namespace Microsoft.Z3
         /// </summary>
         public IDecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
 
+        /// <summary>
+        /// Optimize DRQ
+        /// </summary>
+        public IDecRefQueue Optimize_DRQ { get { Contract.Ensures(Contract.Result<Optimize.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
+
 
         internal long refCount = 0;
 
@@ -4518,6 +4580,7 @@ namespace Microsoft.Z3
             Statistics_DRQ.Clear(this);
             Tactic_DRQ.Clear(this);
             Fixedpoint_DRQ.Clear(this);
+            Optimize_DRQ.Clear(this);
 
             m_boolSort = null;
             m_intSort = null;

src/api/dotnet/Deprecated.cs

@@ -0,0 +1,111 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    Deprecated.cs
+
+Abstract:
+
+    Expose deprecated features for use from the managed API 
+    those who use them for experiments.
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+--*/
+using System;
+using System.Collections.Generic;
+using System.Runtime.InteropServices;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// The main interaction with Z3 happens via the Context.
+    /// </summary>
+    [ContractVerification(true)]
+    public class Deprecated 
+    {
+
+        /// <summary>
+        /// Creates a backtracking point.
+        /// </summary>
+        /// <seealso cref="Pop"/>
+         public static void Push(Context ctx) {
+             Native.Z3_push(ctx.nCtx);
+         }
+
+        /// <summary>
+        /// Backtracks <paramref name="n"/> backtracking points.
+        /// </summary>
+        /// <remarks>Note that an exception is thrown if <paramref name="n"/> is not smaller than <c>NumScopes</c></remarks>
+        /// <seealso cref="Push"/>
+         public static void Pop(Context ctx, uint n = 1) {
+             Native.Z3_pop(ctx.nCtx, n);
+         }
+
+        /// <summary>
+        /// Assert a constraint (or multiple) into the solver.
+        /// </summary>        
+         public static void Assert(Context ctx, params BoolExpr[] constraints) 
+         {
+            Contract.Requires(constraints != null);
+            Contract.Requires(Contract.ForAll(constraints, c => c != null));
+
+            ctx.CheckContextMatch(constraints);
+            foreach (BoolExpr a in constraints)
+            {
+                Native.Z3_assert_cnstr(ctx.nCtx, a.NativeObject);
+            }
+         }
+        /// <summary>
+        /// Checks whether the assertions in the context are consistent or not.
+        /// </summary>
+        public static Status Check(Context ctx, List<BoolExpr> core, ref Model model, ref Expr proof, params Expr[] assumptions)
+        {
+            Z3_lbool r;
+            model = null;
+            proof = null;
+            if (assumptions == null || assumptions.Length == 0)
+                r = (Z3_lbool)Native.Z3_check(ctx.nCtx);
+            else {
+                IntPtr mdl = IntPtr.Zero, prf = IntPtr.Zero;
+                uint core_size = 0;
+                IntPtr[] native_core = new IntPtr[assumptions.Length];
+                r = (Z3_lbool)Native.Z3_check_assumptions(ctx.nCtx, 
+                                   (uint)assumptions.Length, AST.ArrayToNative(assumptions),
+                                   ref mdl, ref prf, ref core_size, native_core);
+
+                for (uint i = 0; i < core_size; i++)
+                    core.Add((BoolExpr)Expr.Create(ctx, native_core[i]));
+                if (mdl != IntPtr.Zero) {
+                    model = new Model(ctx, mdl);
+                }
+                if (prf != IntPtr.Zero) {
+                    proof = Expr.Create(ctx, prf);
+                }
+
+            }
+            switch (r)
+            {
+                case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
+                case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
+                default: return Status.UNKNOWN;
+            }
+        }
+
+        /// <summary>
+        /// Retrieves an assignment to atomic propositions for a satisfiable context.
+        /// </summary>
+         public static BoolExpr GetAssignment(Context ctx) 
+         {
+             IntPtr x = Native.Z3_get_context_assignment(ctx.nCtx);
+             return (BoolExpr)Expr.Create(ctx, x);
+         }
+
+    }
+}

src/api/dotnet/FPNum.cs

@@ -59,6 +59,25 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// The significand value of a floating-point numeral as a UInt64
+        /// </summary>
+        /// <remarks>
+        /// This function extracts the significand bits, without the 
+        /// hidden bit or normalization. Throws an exception if the
+        /// significand does not fit into a UInt64.
+        /// </remarks>
+        public UInt64 SignificandUInt64
+        {
+            get
+            {
+                UInt64 result = 0;
+                if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0)
+                    throw new Z3Exception("Significand is not a 64 bit unsigned integer");                
+                return result;
+            }
+        }
+
         /// <summary>
         /// Return the exponent value of a floating-point numeral as a string
         /// </summary>

src/api/dotnet/Fixedpoint.cs

@@ -269,14 +269,6 @@ namespace Microsoft.Z3
                              AST.ArrayLength(queries), AST.ArrayToNative(queries));
         }
 
-        BoolExpr[] ToBoolExprs(ASTVector v) {
-            uint n = v.Size;
-            BoolExpr[] res = new BoolExpr[n];
-            for (uint i = 0; i < n; i++)
-                res[i] = new BoolExpr(Context, v[i].NativeObject);
-            return res;
-        }
-
         /// <summary>
         /// Retrieve set of rules added to fixedpoint context.
         /// </summary>                
@@ -286,7 +278,8 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
-                return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject)));
+                ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
+                return av.ToBoolExprArray();
             }
         }
 
@@ -299,7 +292,21 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
-                return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject)));
+                ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
+                return av.ToBoolExprArray();
+            }
+        }
+
+        /// <summary>
+        /// Fixedpoint statistics.
+        /// </summary>
+        public Statistics Statistics
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<Statistics>() != null);
+
+                return new Statistics(Context, Native.Z3_fixedpoint_get_statistics(Context.nCtx, NativeObject));
             }
         }
 
@@ -308,16 +315,19 @@ namespace Microsoft.Z3
         /// Add the rules to the current fixedpoint context. 
         /// Return the set of queries in the file.
         /// </summary>                
-	public BoolExpr[] ParseFile(string file) {
-            return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file)));
+        public BoolExpr[] ParseFile(string file)
+        {
+            ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file));
+            return av.ToBoolExprArray();
         }
 
         /// <summary>
         /// Similar to ParseFile. Instead it takes as argument a string.
-        /// </summary>                
-
-	public BoolExpr[] ParseString(string s) {
-            return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s)));
+        /// </summary>
+        public BoolExpr[] ParseString(string s)
+        {
+            ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s));
+            return av.ToBoolExprArray();
         }
 
 

src/api/dotnet/Goal.cs

@@ -208,6 +208,21 @@ namespace Microsoft.Z3
             return Native.Z3_goal_to_string(Context.nCtx, NativeObject);
         }
 
+        /// <summary>
+        /// Goal to BoolExpr conversion.
+        /// </summary>
+        /// <returns>A string representation of the Goal.</returns>
+        public BoolExpr AsBoolExpr() {
+            uint n = Size;
+            if (n == 0) 
+                return Context.MkTrue();
+            else if (n == 1)                
+                return Formulas[0];
+            else {
+                return Context.MkAnd(Formulas);
+            }
+        }
+
         #region Internal
         internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 

src/api/dotnet/InterpolationContext.cs

@@ -47,7 +47,7 @@ namespace Microsoft.Z3
         /// <remarks>For more information on interpolation please refer
         /// too the function Z3_get_interpolant in the C/C++ API, which is 
         /// well documented.</remarks>
-        public Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
+        public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
         {
             Contract.Requires(pf != null);
             Contract.Requires(pat != null);
@@ -59,11 +59,7 @@ namespace Microsoft.Z3
             CheckContextMatch(p);
 
             ASTVector seq = new ASTVector(this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject));
-            uint n = seq.Size;
-            Expr[] res = new Expr[n];
-            for (uint i = 0; i < n; i++)
-                res[i] = Expr.Create(this, seq[i].NativeObject);
-            return res;
+            return seq.ToBoolExprArray();
         }
 
         /// <summary> 
@@ -72,7 +68,7 @@ namespace Microsoft.Z3
         /// <remarks>For more information on interpolation please refer
         /// too the function Z3_compute_interpolant in the C/C++ API, which is 
         /// well documented.</remarks>
-        public Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model)
+        public Z3_lbool ComputeInterpolant(Expr pat, Params p, out BoolExpr[] interp, out Model model)
         {
             Contract.Requires(pat != null);
             Contract.Requires(p != null);
@@ -84,7 +80,7 @@ namespace Microsoft.Z3
 
             IntPtr i = IntPtr.Zero, m = IntPtr.Zero;
             int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m);
-            interp = new ASTVector(this, i);
+            interp = new ASTVector(this, i).ToBoolExprArray();
             model = new Model(this, m);
             return (Z3_lbool)r;
         }
@@ -106,7 +102,7 @@ namespace Microsoft.Z3
         /// <remarks>For more information on interpolation please refer
         /// too the function Z3_check_interpolant in the C/C++ API, which is 
         /// well documented.</remarks>
-        public int CheckInterpolant(Expr[] cnsts, uint[] parents, Expr[] interps, out string error, Expr[] theory)
+        public int CheckInterpolant(Expr[] cnsts, uint[] parents, BoolExpr[] interps, out string error, Expr[] theory)
         {
             Contract.Requires(cnsts.Length == parents.Length);
             Contract.Requires(cnsts.Length == interps.Length + 1);

src/api/dotnet/Microsoft.Z3.csproj

@@ -365,6 +365,7 @@
     <Compile Include="IntSymbol.cs" />
     <Compile Include="ListSort.cs" />
     <Compile Include="Model.cs" />
+    <Compile Include="Optimize.cs" />
     <Compile Include="Params.cs" />
     <Compile Include="ParamDescrs.cs" />
     <Compile Include="Pattern.cs" />

src/api/dotnet/Model.cs

@@ -265,12 +265,8 @@ namespace Microsoft.Z3
             Contract.Requires(s != null);
             Contract.Ensures(Contract.Result<Expr[]>() != null);
 
-            ASTVector nUniv = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject));
-            uint n = nUniv.Size;
-            Expr[] res = new Expr[n];
-            for (uint i = 0; i < n; i++)
-                res[i] = Expr.Create(Context, nUniv[i].NativeObject);
-            return res;
+            ASTVector av = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject));            
+            return av.ToExprArray();
         }
 
         /// <summary>

src/api/dotnet/Optimize.cs

@@ -0,0 +1,298 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    Optimize.cs
+
+Abstract:
+
+    Z3 Managed API: Optimizes
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-12-03
+
+Notes:
+    
+--*/
+
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Object for managing optimizization context
+    /// </summary>
+    [ContractVerification(true)]
+    public class Optimize : Z3Object
+    {
+        /// <summary>
+        /// A string that describes all available optimize solver parameters.
+        /// </summary>
+        public string Help
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<string>() != null);
+                return Native.Z3_optimize_get_help(Context.nCtx, NativeObject);
+            }
+        }
+
+        /// <summary>
+        /// Sets the optimize solver parameters.
+        /// </summary>
+        public Params Parameters
+        {
+            set
+            {
+                Contract.Requires(value != null);
+                Context.CheckContextMatch(value);
+                Native.Z3_optimize_set_params(Context.nCtx, NativeObject, value.NativeObject);
+            }
+        }
+
+        /// <summary>
+        /// Retrieves parameter descriptions for Optimize solver.
+        /// </summary>
+        public ParamDescrs ParameterDescriptions
+        {
+            get { return new ParamDescrs(Context, Native.Z3_optimize_get_param_descrs(Context.nCtx, NativeObject)); }
+        }
+
+        /// <summary>
+        /// Assert a constraint (or multiple) into the optimize solver.
+        /// </summary>        
+        public void Assert(params BoolExpr[] constraints)
+        {
+            Contract.Requires(constraints != null);
+            Contract.Requires(Contract.ForAll(constraints, c => c != null));
+
+            Context.CheckContextMatch(constraints);
+            foreach (BoolExpr a in constraints)
+            {
+                Native.Z3_optimize_assert(Context.nCtx, NativeObject, a.NativeObject);
+            }
+        }
+
+        /// <summary>
+        /// Alias for Assert.
+        /// </summary>        
+        public void Add(params BoolExpr[] constraints)
+        {
+            Assert(constraints);
+        }
+
+        /// <summary>
+        /// Handle to objectives returned by objective functions.
+        /// </summary>
+        public class Handle
+        {
+            Optimize opt;
+            uint handle;
+            internal Handle(Optimize opt, uint h)
+            {
+                this.opt = opt;
+                this.handle = h;
+            }
+
+            /// <summary>
+            /// Retrieve a lower bound for the objective handle.
+            /// </summary>        	   	
+            public ArithExpr Lower
+            {
+                get { return opt.GetLower(handle); }
+            }
+
+            /// <summary>
+            /// Retrieve an upper bound for the objective handle.
+            /// </summary>        	   	
+            public ArithExpr Upper
+            {
+                get { return opt.GetUpper(handle); }
+            }
+
+            /// <summary>
+            /// Retrieve the value of an objective.
+            /// </summary>        	   	
+            public ArithExpr Value
+            {
+                get { return Lower; }
+            }
+        }
+
+        /// <summary>
+        /// Assert soft constraint
+        /// </summary>        
+        /// <remarks>
+        /// Return an objective which associates with the group of constraints.
+        /// </remarks>
+        public Handle AssertSoft(BoolExpr constraint, uint weight, string group)
+        {
+            Context.CheckContextMatch(constraint);
+            Symbol s = Context.MkSymbol(group);
+            return new Handle(this, Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));
+        }
+
+
+        /// <summary>
+        /// Check satisfiability of asserted constraints.
+        /// Produce a model that (when the objectives are bounded and 
+        /// don't use strict inequalities) meets the objectives.
+        /// </summary>
+        ///
+        public Status Check()
+        {
+            Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject);
+            switch (r)
+            {
+                case Z3_lbool.Z3_L_TRUE:
+                    return Status.SATISFIABLE;
+                case Z3_lbool.Z3_L_FALSE:
+                    return Status.UNSATISFIABLE;
+                default:
+                    return Status.UNKNOWN;
+            }
+        }
+
+        /// <summary>
+        /// Creates a backtracking point.
+        /// </summary>
+        /// <seealso cref="Pop"/>
+        public void Push()
+        {
+            Native.Z3_optimize_push(Context.nCtx, NativeObject);
+        }
+
+        /// <summary>
+        /// Backtrack one backtracking point.
+        /// </summary>
+        /// <remarks>Note that an exception is thrown if Pop is called without a corresponding <c>Push</c></remarks>
+        /// <seealso cref="Push"/>
+        public void Pop()
+        {
+            Native.Z3_optimize_pop(Context.nCtx, NativeObject);
+        }
+
+
+        /// <summary>
+        /// The model of the last <c>Check</c>.
+        /// </summary>
+        /// <remarks>
+        /// The result is <c>null</c> if <c>Check</c> was not invoked before,
+        /// if its results was not <c>SATISFIABLE</c>, or if model production is not enabled.
+        /// </remarks>
+        public Model Model
+        {
+            get
+            {
+                IntPtr x = Native.Z3_optimize_get_model(Context.nCtx, NativeObject);
+                if (x == IntPtr.Zero)
+                    return null;
+                else
+                    return new Model(Context, x);
+            }
+        }
+
+        /// <summary>
+        /// Declare an arithmetical maximization objective.
+        /// Return a handle to the objective. The handle is used as
+        /// to retrieve the values of objectives after calling Check.
+        /// </summary>        	
+        public Handle MkMaximize(ArithExpr e)
+        {
+            return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
+        }
+
+        /// <summary>
+        /// Declare an arithmetical minimization objective. 
+        /// Similar to MkMaximize.
+        /// </summary>        	
+        public Handle MkMinimize(ArithExpr e)
+        {
+            return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
+        }
+
+        /// <summary>
+        /// Retrieve a lower bound for the objective handle.
+        /// </summary>        	
+        private ArithExpr GetLower(uint index)
+        {
+            return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
+        }
+
+
+        /// <summary>
+        /// Retrieve an upper bound for the objective handle.
+        /// </summary>        	
+        private ArithExpr GetUpper(uint index)
+        {
+            return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
+        }
+
+
+        /// <summary>
+        /// Print the context to a string (SMT-LIB parseable benchmark).
+        /// </summary>        	
+        public override string ToString()
+        {
+            return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
+        }
+
+        /// <summary>
+        /// Optimize statistics.
+        /// </summary>
+        public Statistics Statistics
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<Statistics>() != null);
+
+                return new Statistics(Context, Native.Z3_optimize_get_statistics(Context.nCtx, NativeObject));
+            }
+        }
+
+
+        #region Internal
+        internal Optimize(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal Optimize(Context ctx)
+            : base(ctx, Native.Z3_mk_optimize(ctx.nCtx))
+        {
+            Contract.Requires(ctx != null);
+        }
+
+        internal class DecRefQueue : IDecRefQueue
+        {
+            public DecRefQueue() : base() { }
+            public DecRefQueue(uint move_limit) : base(move_limit) { }
+            internal override void IncRef(Context ctx, IntPtr obj)
+            {
+                Native.Z3_optimize_inc_ref(ctx.nCtx, obj);
+            }
+
+            internal override void DecRef(Context ctx, IntPtr obj)
+            {
+                Native.Z3_optimize_dec_ref(ctx.nCtx, obj);
+            }
+        };
+
+        internal override void IncRef(IntPtr o)
+        {
+            Context.Optimize_DRQ.IncAndClear(Context, o);
+            base.IncRef(o);
+        }
+
+        internal override void DecRef(IntPtr o)
+        {
+            Context.Optimize_DRQ.Add(o);
+            base.DecRef(o);
+        }
+        #endregion
+    }
+}

src/api/dotnet/Params.cs

@@ -79,6 +79,7 @@ namespace Microsoft.Z3
             Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject);
         }
 
+
         /// <summary>
         /// Adds a parameter setting.
         /// </summary>
@@ -118,6 +119,7 @@ namespace Microsoft.Z3
         /// </summary>
         public void Add(string name, string value)
         {
+            Contract.Requires(name != null);
             Contract.Requires(value != null);
 
             Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, Context.MkSymbol(value).NativeObject);

src/api/dotnet/Solver.cs

@@ -178,8 +178,8 @@ namespace Microsoft.Z3
         {
             get
             {
-                ASTVector ass = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
-                return ass.Size;
+                ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
+                return assertions.Size;
             }
         }
 
@@ -192,12 +192,8 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
-                ASTVector ass = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
-                uint n = ass.Size;
-                BoolExpr[] res = new BoolExpr[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = new BoolExpr(Context, ass[i].NativeObject);
-                return res;
+                ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
+                return assertions.ToBoolExprArray();
             }
         }
 
@@ -270,18 +266,14 @@ namespace Microsoft.Z3
         /// The result is empty if <c>Check</c> was not invoked before,
         /// if its results was not <c>UNSATISFIABLE</c>, or if core production is disabled.
         /// </remarks>
-        public Expr[] UnsatCore
+        public BoolExpr[] UnsatCore
         {
             get
             {
                 Contract.Ensures(Contract.Result<Expr[]>() != null);
 
-                ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));
-                uint n = core.Size;
-                Expr[] res = new Expr[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = Expr.Create(Context, core[i].NativeObject);
-                return res;
+                ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));                
+                return core.ToBoolExprArray();
             }
         }
 

src/api/java/ASTMap.java

@@ -92,10 +92,10 @@ class ASTMap extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public ASTVector getKeys()
+    public AST[] getKeys()
     {
-        return new ASTVector(getContext(), Native.astMapKeys(getContext().nCtx(),
-                getNativeObject()));
+        ASTVector av = new ASTVector(getContext(), Native.astMapKeys(getContext().nCtx(), getNativeObject()));
+        return av.ToArray();
     }
 
     /**

src/api/java/ASTVector.java

@@ -119,4 +119,135 @@ public class ASTVector extends Z3Object
         getContext().getASTVectorDRQ().add(o);
         super.decRef(o);
     }
-}
+    
+    /**
+     * Translates the AST vector into an AST[]
+     * */
+    public AST[] ToArray()
+    {
+        int n = size();
+        AST[] res = new AST[n];
+        for (int i = 0; i < n; i++)
+            res[i] = AST.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+    
+    /**
+     * Translates the AST vector into an Expr[]
+     * */
+    public Expr[] ToExprArray() {
+        int n = size();
+        Expr[] res = new Expr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = Expr.create(getContext(), get(i).getNativeObject());
+        return res;	
+    }
+
+    /**
+     * Translates the AST vector into an BoolExpr[]
+     * */  
+    public BoolExpr[] ToBoolExprArray()
+    {
+        int n = size();
+        BoolExpr[] res = new BoolExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (BoolExpr) Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an BitVecExpr[]
+     * */    
+    public BitVecExpr[] ToBitVecExprArray()
+    {
+        int n = size();
+        BitVecExpr[] res = new BitVecExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (BitVecExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an ArithExpr[]
+     * */   
+    public ArithExpr[] ToArithExprExprArray()
+    {
+        int n = size();
+        ArithExpr[] res = new ArithExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (ArithExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an ArrayExpr[]
+     * */  
+    public ArrayExpr[] ToArrayExprArray()
+    {
+        int n = size();
+        ArrayExpr[] res = new ArrayExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (ArrayExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an DatatypeExpr[]
+     * */ 
+    public DatatypeExpr[] ToDatatypeExprArray()
+    {
+        int n = size();
+        DatatypeExpr[] res = new DatatypeExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (DatatypeExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an FPExpr[]
+     * */   
+    public FPExpr[] ToFPExprArray()
+    {
+        int n = size();
+        FPExpr[] res = new FPExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (FPExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an FPRMExpr[]
+     * */
+    public FPRMExpr[] ToFPRMExprArray()
+    {
+        int n = size();
+        FPRMExpr[] res = new FPRMExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (FPRMExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an IntExpr[]
+     * */ 
+    public IntExpr[] ToIntExprArray()
+    {
+        int n = size();
+        IntExpr[] res = new IntExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (IntExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an RealExpr[]
+     * */   
+    public RealExpr[] ToRealExprArray()
+    {
+        int n = size();
+        RealExpr[] res = new RealExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (RealExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+}

src/api/java/Context.java

@@ -361,6 +361,23 @@ public class Context extends IDisposable
         return mkDatatypeSorts(mkSymbols(names), c);
     }
 
+    /**
+     * Update a datatype field at expression t with value v.
+     * The function performs a record update at t. The field
+     * that is passed in as argument is updated with value v,
+     * the remainig fields of t are unchanged.	
+     **/
+    public Expr MkUpdateField(FuncDecl field, Expr t, Expr v) 
+            throws Z3Exception
+    {
+	return Expr.create
+	    (this, 
+	     Native.datatypeUpdateField
+	     (nCtx(), field.getNativeObject(),
+	      t.getNativeObject(), v.getNativeObject()));		
+    }
+
+
     /**
      * Creates a new function declaration.
      **/

src/api/java/FPNum.java

@@ -43,6 +43,21 @@ public class FPNum extends FPExpr
         return Native.fpaGetNumeralSignificandString(getContext().nCtx(), getNativeObject());
     }
 
+    /**
+     * The significand value of a floating-point numeral as a UInt64
+     * Remarks: This function extracts the significand bits, without the 
+     * hidden bit or normalization. Throws an exception if the
+     * significand does not fit into a UInt64.
+     * @throws Z3Exception
+     **/
+    public long getSignificandUInt64()
+    {
+        Native.LongPtr res = new Native.LongPtr();
+        if (Native.fpaGetNumeralSignificandUint64(getContext().nCtx(), getNativeObject(), res) ^ true)
+            throw new Z3Exception("Significand is not a 64 bit unsigned integer");
+        return res.value;
+    }
+    
     /**
      * Return the exponent value of a floating-point numeral as a string
      * @throws Z3Exception 

src/api/java/FPSort.java

@@ -43,7 +43,7 @@ public class FPSort extends Sort
      * The number of significand bits.
      */
     public int getSBits() {
-        return Native.fpaGetEbits(getContext().nCtx(), getNativeObject());        
+        return Native.fpaGetSbits(getContext().nCtx(), getNativeObject());        
     }
     
 }

src/api/java/Fixedpoint.java

@@ -295,14 +295,8 @@ public class Fixedpoint extends Z3Object
      **/
     public BoolExpr[] getRules()
     {
-
-        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(
-                getContext().nCtx(), getNativeObject()));
-        int n = v.size();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
-        return res;
+        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
+        return v.ToBoolExprArray();
     }
 
     /**
@@ -312,17 +306,45 @@ public class Fixedpoint extends Z3Object
      **/
     public BoolExpr[] getAssertions()
     {
-
-        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(
-                getContext().nCtx(), getNativeObject()));
-        int n = v.size();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
-        return res;
+        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
+        return v.ToBoolExprArray();
     }
 
-    Fixedpoint(Context ctx, long obj)
+    /**
+     * Fixedpoint statistics.
+     * 
+     * @throws Z3Exception
+     **/
+    public Statistics getStatistics()
+    {
+        return new Statistics(getContext(), Native.fixedpointGetStatistics(
+                getContext().nCtx(), getNativeObject()));
+    }
+
+    /** 
+     * Parse an SMT-LIB2 file with fixedpoint rules. 
+     * Add the rules to the current fixedpoint context. 
+     * Return the set of queries in the file.
+     **/        
+    public BoolExpr[] ParseFile(String file)
+    {
+        ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
+        return av.ToBoolExprArray();
+    }
+
+    /** 
+     * Parse an SMT-LIB2 string with fixedpoint rules. 
+     * Add the rules to the current fixedpoint context. 
+     * Return the set of queries in the file.
+     **/ 
+    public BoolExpr[] ParseString(String s)
+    {
+        ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
+        return av.ToBoolExprArray();
+    }
+    
+
+    Fixedpoint(Context ctx, long obj) throws Z3Exception
     {
         super(ctx, obj);
     }

src/api/java/Goal.java

@@ -221,6 +221,22 @@ public class Goal extends Z3Object
             return "Z3Exception: " + e.getMessage();
         }
     }
+    
+    /** 
+     * Goal to BoolExpr conversion.
+     *  
+     * Returns a string representation of the Goal.
+     **/
+    public BoolExpr AsBoolExpr() {
+        int n = size();
+        if (n == 0) 
+            return getContext().mkTrue();
+        else if (n == 1)                
+            return getFormulas()[0];
+        else {
+            return getContext().mkAnd(getFormulas());
+        }
+    }
 
     Goal(Context ctx, long obj)
     {

src/api/java/InterpolationContext.java

@@ -73,20 +73,23 @@ public class InterpolationContext extends Context
      * well documented.
      * @throws Z3Exception 
      **/
-    public Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
+    public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
     {
         checkContextMatch(pf);
         checkContextMatch(pat);
         checkContextMatch(p);
 
         ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
-        int n = seq.size();
-        Expr[] res = new Expr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = Expr.create(this, seq.get(i).getNativeObject());
-        return res;
+        return seq.ToBoolExprArray();
     }
 
+    public class ComputeInterpolantResult 
+    {
+        public Z3_lbool status = Z3_lbool.Z3_L_UNDEF;
+        public BoolExpr[] interp = null;
+        public Model model = null;
+    };
+    
     /**
      * Computes an interpolant.   
      * Remarks: For more information on interpolation please refer
@@ -94,17 +97,20 @@ public class InterpolationContext extends Context
      * well documented.
      * @throws Z3Exception 
      **/
-    public Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model)
+    public ComputeInterpolantResult ComputeInterpolant(Expr pat, Params p)
     {
         checkContextMatch(pat);
         checkContextMatch(p);
 
+        ComputeInterpolantResult res = new ComputeInterpolantResult();
         Native.LongPtr n_i = new Native.LongPtr();
         Native.LongPtr n_m = new Native.LongPtr();
-        int r = Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m);
-        interp = new ASTVector(this, n_i.value);
-        model = new Model(this, n_m.value);
-        return Z3_lbool.fromInt(r);
+        res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));        
+        if (res.status == Z3_lbool.Z3_L_FALSE)
+            res.interp = (new ASTVector(this, n_i.value)).ToBoolExprArray();
+        if (res.status == Z3_lbool.Z3_L_TRUE) 
+            res.model = new Model(this, n_m.value);
+        return res;
     }
 
     ///  
@@ -118,16 +124,23 @@ public class InterpolationContext extends Context
         return Native.interpolationProfile(nCtx());
     }
 
+    public class CheckInterpolantResult
+    {
+        public int return_value = 0;
+        public String error = null;
+    }
+    
     ///  
     /// Checks the correctness of an interpolant.
     ///    
     /// Remarks: For more information on interpolation please refer
     /// too the function Z3_check_interpolant in the C/C++ API, which is 
     /// well documented.
-    public int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory)
+    public CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, BoolExpr[] interps, String error, Expr[] theory)
     {
+        CheckInterpolantResult res = new CheckInterpolantResult();
         Native.StringPtr n_err_str = new Native.StringPtr();
-        int r = Native.checkInterpolant(nCtx(),
+        res.return_value = Native.checkInterpolant(nCtx(),
                                         cnsts.length,
                                         Expr.arrayToNative(cnsts),
                                         parents,
@@ -135,41 +148,52 @@ public class InterpolationContext extends Context
                                         n_err_str,
                                         theory.length,
                                         Expr.arrayToNative(theory));
-        error = n_err_str.value;
-        return r;
+        res.error = n_err_str.value;
+        return res;
     }
 
+    public class ReadInterpolationProblemResult 
+    {
+        public int return_value = 0;
+        public Expr[] cnsts;
+        public int[] parents;
+        public String error;
+        public Expr[] theory;
+    };
+    
     ///  
     /// Reads an interpolation problem from a file.
     ///    
     /// Remarks: For more information on interpolation please refer
     /// too the function Z3_read_interpolation_problem in the C/C++ API, which is 
     /// well documented.
-    public int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
+    public ReadInterpolationProblemResult ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
     {
+        ReadInterpolationProblemResult res = new ReadInterpolationProblemResult();
+        
         Native.IntPtr n_num = new Native.IntPtr();
         Native.IntPtr n_num_theory = new Native.IntPtr();
         Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr();
         Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
         Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr();
         Native.StringPtr n_err_str = new Native.StringPtr();
-        int r = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory);
+        res.return_value = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory);
         int num = n_num.value;
         int num_theory = n_num_theory.value;
-        error = n_err_str.value;
-        cnsts = new Expr[num];
-        parents = new int[num];
+        res.error = n_err_str.value;
+        res.cnsts = new Expr[num];
+        res.parents = new int[num];
         theory = new Expr[num_theory];
         for (int i = 0; i < num; i++)
         {
-            cnsts[i] = Expr.create(this, n_cnsts.value[i]);
-            parents[i] = n_parents.value[i];
+            res.cnsts[i] = Expr.create(this, n_cnsts.value[i]);
+            res.parents[i] = n_parents.value[i];
         }
         for (int i = 0; i < num_theory; i++)
-            theory[i] = Expr.create(this, n_theory.value[i]);
-        return r;
+            res.theory[i] = Expr.create(this, n_theory.value[i]);
+        return res;
     }
-
+    
     ///  
     /// Writes an interpolation problem to a file.
     ///    

src/api/java/Model.java

@@ -273,11 +273,7 @@ public class Model extends Z3Object
 
         ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
                 getContext().nCtx(), getNativeObject(), s.getNativeObject()));
-        int n = nUniv.size();
-        Expr[] res = new Expr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = Expr.create(getContext(), nUniv.get(i).getNativeObject());
-        return res;
+        return nUniv.ToExprArray();
     }
 
     /**

src/api/java/Solver.java

@@ -176,8 +176,7 @@ public class Solver extends Z3Object
      **/
     public int getNumAssertions()
     {
-        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
-                getContext().nCtx(), getNativeObject()));
+        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
         return assrts.size();
     }
 
@@ -188,13 +187,8 @@ public class Solver extends Z3Object
      **/
     public BoolExpr[] getAssertions()
     {
-        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
-                getContext().nCtx(), getNativeObject()));
-        int n = assrts.size();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), assrts.get(i).getNativeObject());
-        return res;
+        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
+        return assrts.ToBoolExprArray();
     }
 
     /**
@@ -282,16 +276,11 @@ public class Solver extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Expr[] getUnsatCore()
+    public BoolExpr[] getUnsatCore()
     {
 
-        ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(
-                getContext().nCtx(), getNativeObject()));
-        int n = core.size();
-        Expr[] res = new Expr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = Expr.create(getContext(), core.get(i).getNativeObject());
-        return res;
+        ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));        
+        return core.ToBoolExprArray();
     }
 
     /**

src/api/ml/z3.mli

@@ -123,7 +123,7 @@ sig
 end
 
 (** The abstract syntax tree (AST) module *)
-module AST :
+module rec AST :
 sig
   type ast 
 
@@ -156,6 +156,12 @@ sig
 		@return A new ASTVector *)
     val translate : ast_vector -> context -> ast_vector
 
+    (** Translates the ASTVector into an (Ast.ast list) *)
+    val to_list : ast_vector -> ast list
+
+    (** Translates the ASTVector into an (Expr.expr list) *)
+    val to_expr_list : ast_vector -> Expr.expr list
+
     (** Retrieves a string representation of the vector. *)
     val to_string : ast_vector -> string
   end
@@ -189,7 +195,7 @@ sig
     val get_size : ast_map -> int
 
     (** The keys stored in the map. *)
-    val get_keys : ast_map -> ast list
+    val get_keys : ast_map -> Expr.expr list
 
     (** Retrieves a string representation of the map.*)
     val to_string : ast_map -> string
@@ -260,7 +266,7 @@ sig
 end
 
 (** The Sort module implements type information for ASTs *)
-module Sort :
+and Sort :
 sig
   type sort = Sort of AST.ast
 
@@ -291,7 +297,7 @@ sig
 end
 
 (** Function declarations *)
-module rec FuncDecl :
+and FuncDecl :
 sig
   type func_decl = FuncDecl of AST.ast
 
@@ -2155,6 +2161,12 @@ sig
   (** Return the significand value of a floating-point numeral as a string. *)
   val get_numeral_significand_string : context -> Expr.expr -> string
 
+  (** Return the significand value of a floating-point numeral as a uint64. 
+	  Remark: This function extracts the significand bits, without the 
+      hidden bit or normalization. Throws an exception if the
+      significand does not fit into a uint64. *)
+  val get_numeral_significand_uint : context -> Expr.expr -> bool * int
+
   (** Return the exponent value of a floating-point numeral as a string *)
   val get_numeral_exponent_string : context -> Expr.expr -> string
 
@@ -2641,6 +2653,9 @@ sig
 
   (**  A string representation of the Goal. *)
   val to_string : goal -> string
+
+  (** Goal to BoolExpr conversion. *)
+  val as_expr : goal -> Expr.expr
 end
 
 (** Models
@@ -2751,7 +2766,7 @@ sig
   (** The finite set of distinct values that represent the interpretation of a sort. 
       {!get_sorts}
       @return A list of expressions, where each is an element of the universe of the sort *)
-  val sort_universe : model -> Sort.sort -> AST.ast list
+  val sort_universe : model -> Sort.sort -> Expr.expr list
     
   (** Conversion of models to strings. 
       @return A string representation of the model. *)
@@ -2938,6 +2953,55 @@ sig
   val interrupt : context -> unit
 end
 
+(** Objects that track statistical information. *)
+module Statistics :
+sig
+  type statistics 
+	
+  (** Statistical data is organized into pairs of \[Key, Entry\], where every
+	  Entry is either a floating point or integer value. *)
+  module Entry :
+  sig
+    type statistics_entry
+	  
+    (** The key of the entry. *)
+    val get_key : statistics_entry -> string
+	  
+    (** The int-value of the entry. *)
+    val get_int : statistics_entry -> int
+	  
+    (** The float-value of the entry. *)
+    val get_float : statistics_entry -> float
+	  
+    (** True if the entry is uint-valued. *)
+    val is_int : statistics_entry -> bool
+	  
+    (** True if the entry is float-valued. *)
+    val is_float : statistics_entry -> bool
+	  
+    (** The string representation of the the entry's value. *)
+    val to_string_value : statistics_entry -> string
+	  
+    (** The string representation of the entry (key and value) *)
+    val to_string : statistics_entry -> string
+  end
+
+  (** A string representation of the statistical data. *)    
+  val to_string : statistics -> string
+
+  (** The number of statistical data. *)
+  val get_size : statistics -> int
+
+  (** The data entries. *)
+  val get_entries : statistics -> Entry.statistics_entry list
+
+  (**   The statistical counters. *)
+  val get_keys : statistics -> string list
+
+  (** The value of a particular statistical counter. *)        
+  val get : statistics -> string -> Entry.statistics_entry option
+end
+
 (** Solvers *)
 module Solver :
 sig
@@ -2946,56 +3010,6 @@ sig
       
   val string_of_status : status -> string
 
-  (** Objects that track statistical information about solvers. *)
-  module Statistics :
-  sig
-    type statistics 
-
-    (**   Statistical data is organized into pairs of \[Key, Entry\], where every
-		  Entry is either a floating point or integer value.
-    *)
-    module Entry :
-    sig
-      type statistics_entry
-
-      (** The key of the entry. *)
-      val get_key : statistics_entry -> string
-
-      (** The int-value of the entry. *)
-      val get_int : statistics_entry -> int
-
-      (** The float-value of the entry. *)
-      val get_float : statistics_entry -> float
-		
-      (** True if the entry is uint-valued. *)
-      val is_int : statistics_entry -> bool
-		
-      (** True if the entry is float-valued. *)
-      val is_float : statistics_entry -> bool
-		
-      (** The string representation of the the entry's value. *)
-      val to_string_value : statistics_entry -> string
-		
-      (** The string representation of the entry (key and value) *)
-      val to_string : statistics_entry -> string
-    end
-
-    (** A string representation of the statistical data. *)    
-    val to_string : statistics -> string
-
-    (** The number of statistical data. *)
-    val get_size : statistics -> int
-
-    (** The data entries. *)
-    val get_entries : statistics -> Entry.statistics_entry list
-
-    (**   The statistical counters. *)
-    val get_keys : statistics -> string list
-
-    (** The value of a particular statistical counter. *)        
-    val get : statistics -> string -> Entry.statistics_entry option
-  end
-
   (** A string that describes all available solver parameters. *)
   val get_help : solver -> string
 
@@ -3081,7 +3095,7 @@ sig
       The unsat core is a subset of [Assertions]
       The result is empty if [Check] was not invoked before,
       if its results was not [UNSATISFIABLE], or if core production is disabled. *)
-  val get_unsat_core : solver -> AST.ast list
+  val get_unsat_core : solver -> Expr.expr list
 
   (** A brief justification of why the last call to [Check] returned [UNKNOWN]. *)
   val get_reason_unknown : solver -> string
@@ -3198,6 +3212,19 @@ sig
 
   (** Create a Fixedpoint context. *)
   val mk_fixedpoint : context -> fixedpoint
+
+  (** Retrieve statistics information from the last call to #Z3_fixedpoint_query. *)
+  val get_statistics : fixedpoint -> Statistics.statistics
+
+  (** Parse an SMT-LIB2 string with fixedpoint rules. 
+      Add the rules to the current fixedpoint context. 
+      Return the set of queries in the string. *)
+  val parse_string : fixedpoint -> string -> Expr.expr list
+
+  (** Parse an SMT-LIB2 file with fixedpoint rules. 
+      Add the rules to the current fixedpoint context. 
+      Return the set of queries in the file. *)
+  val parse_file : fixedpoint -> string -> Expr.expr list
 end
 
 (** Functions for handling SMT and SMT2 expressions and files *)
@@ -3272,12 +3299,12 @@ sig
   (** Gets an interpolant.
       For more information on interpolation please refer
       too the C/C++ API, which is well documented. *)
-  val get_interpolant : context -> Expr.expr -> Expr.expr -> Params.params -> AST.ASTVector.ast_vector
+  val get_interpolant : context -> Expr.expr -> Expr.expr -> Params.params -> Expr.expr list
 
   (** Computes an interpolant.
       For more information on interpolation please refer
       too the C/C++ API, which is well documented. *)
-  val compute_interpolant : context -> Expr.expr -> Params.params -> (AST.ASTVector.ast_vector * Model.model)
+  val compute_interpolant : context -> Expr.expr -> Params.params -> (Z3enums.lbool * Expr.expr list option * Model.model option)
 
   (** Retrieves an interpolation profile.
       For more information on interpolation please refer
@@ -3355,3 +3382,5 @@ val enable_trace : string -> unit
 *)
 val disable_trace : string -> unit
 
+
+

src/api/python/z3.py

@@ -32,7 +32,7 @@ sat
 Z3 exceptions:
 
 >>> try:
-...   x = Int('x')
+...   x = BitVec('x', 32)
 ...   y = Bool('y')
 ...   # the expression x + y is type incorrect
 ...   n = x + y
@@ -301,7 +301,6 @@ class AstRef(Z3PPObject):
         """Return unique identifier for object. It can be used for hash-tables and maps."""
         return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
 
-
     def ctx_ref(self):
         """Return a reference to the C context where this AST node is stored."""
         return self.ctx.ref()
@@ -455,7 +454,6 @@ class SortRef(AstRef):
     def get_id(self):
         return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
 
-
     def kind(self):
         """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.
         
@@ -555,6 +553,8 @@ def _to_sort_ref(s, ctx):
         return ArraySortRef(s, ctx)
     elif k == Z3_DATATYPE_SORT:
         return DatatypeSortRef(s, ctx)
+    elif k == Z3_FINITE_DOMAIN_SORT:
+        return FiniteDomainSortRef(s, ctx)
     elif k == Z3_FLOATING_POINT_SORT:
         return FPSortRef(s, ctx)
     elif k == Z3_ROUNDING_MODE_SORT:
@@ -1228,6 +1228,16 @@ class BoolSortRef(SortRef):
             _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
         return val
 
+    def subsort(self, other):
+        return isinstance(other, ArithSortRef)
+
+    def is_int(self):
+        return True
+
+    def is_bool(self):
+        return True
+
+
 class BoolRef(ExprRef):
     """All Boolean expressions are instances of this class."""
     def sort(self):
@@ -1900,6 +1910,10 @@ class ArithSortRef(SortRef):
                 return val
             if val_s.is_int() and self.is_real():
                 return ToReal(val)
+            if val_s.is_bool() and self.is_int():
+                return If(val, 1, 0)
+            if val_s.is_bool() and self.is_real():
+                return ToReal(If(val, 1, 0))
             if __debug__:
                 _z3_assert(False, "Z3 Integer/Real expression expected" )
         else:
@@ -5603,7 +5617,7 @@ class Statistics:
         sat
         >>> st = s.statistics()
         >>> len(st)
-        2
+        4
         """
         return int(Z3_stats_size(self.ctx.ref(), self.stats))
 
@@ -5617,7 +5631,7 @@ class Statistics:
         sat
         >>> st = s.statistics()
         >>> len(st)
-        2
+        4
         >>> st[0]
         ('nlsat propagations', 2)
         >>> st[1]
@@ -5641,7 +5655,7 @@ class Statistics:
         sat
         >>> st = s.statistics()
         >>> st.keys()
-        ['nlsat propagations', 'nlsat stages']
+        ['nlsat propagations', 'nlsat stages', 'max memory', 'memory']
         """
         return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
 
@@ -5678,7 +5692,7 @@ class Statistics:
         sat
         >>> st = s.statistics() 
         >>> st.keys()
-        ['nlsat propagations', 'nlsat stages']
+        ['nlsat propagations', 'nlsat stages', 'max memory', 'memory']
         >>> st.nlsat_propagations
         2
         >>> st.nlsat_stages
@@ -6071,8 +6085,6 @@ class Solver(Z3PPObject):
             e = BoolVal(True, self.ctx).as_ast()
         return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
 
-
-
 def SolverFor(logic, ctx=None):
     """Create a solver customized for the given logic. 
 
@@ -6333,6 +6345,166 @@ class Fixedpoint(Z3PPObject):
         else:
             return Exists(self.vars, fml)
 
+
+#########################################
+#
+# Finite domain sorts
+#
+#########################################
+
+class FiniteDomainSortRef(SortRef):
+    """Finite domain sort."""
+
+    def size(self):
+        """Return the size of the finite domain sort"""
+        r = (ctype.c_ulonglong * 1)()
+        if Z3_get_finite_domain_sort_size(self.ctx_ref(), self.ast(), r):
+            return r[0]
+        else:
+            raise Z3Exception("Failed to retrieve finite domain sort size")
+
+def FiniteDomainSort(name, sz, ctx=None):
+    """Create a named finite domain sort of a given size sz"""
+    ctx = _get_ctx(ctx)
+    return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx)
+
+#########################################
+#
+# Optimize
+#
+#########################################
+
+class OptimizeObjective:
+    def __init__(self, opt, value, is_max):
+        self._opt = opt
+        self._value = value
+        self._is_max = is_max
+
+    def lower(self):
+        opt = self._opt
+        return _to_expr_ref(Z3_optimize_get_lower(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
+    
+    def upper(self):
+        opt = self._opt
+        return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
+
+    def value(self):
+        if self._is_max:
+            return self.upper()
+        else:
+            return self.lower()
+
+class Optimize(Z3PPObject):
+    """Optimize API provides methods for solving using objective functions and weighted soft constraints"""
+     
+    def __init__(self, ctx=None):
+        self.ctx    = _get_ctx(ctx)
+        self.optimize = Z3_mk_optimize(self.ctx.ref())
+        Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
+
+    def __del__(self):
+        if self.optimize != None:
+            Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
+
+    def set(self, *args, **keys):
+        """Set a configuration option. The method `help()` return a string containing all available options.        
+        """
+        p = args2params(args, keys, self.ctx)
+        Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
+
+    def help(self):
+        """Display a string describing all available options."""
+        print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
+            
+    def param_descrs(self):
+        """Return the parameter description set."""
+        return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
+    
+    def assert_exprs(self, *args):
+        """Assert constraints as background axioms for the optimize solver."""
+        args = _get_args(args)
+        for arg in args:
+            if isinstance(arg, Goal) or isinstance(arg, AstVector):
+                for f in arg:
+                    Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
+            else:
+                Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
+
+    def add(self, *args):
+        """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
+        self.assert_exprs(*args)
+
+    def add_soft(self, arg, weight = "1", id = None):
+        """Add soft constraint with optional weight and optional identifier.
+           If no weight is supplied, then the penalty for violating the soft constraint
+           is 1.
+           Soft constraints are grouped by identifiers. Soft constraints that are
+           added without identifiers are grouped by default.
+        """
+        if _is_int(weight):
+            weight = "%d" % weight
+        if not isinstance(weight, str):
+            raise Z3Exception("weight should be a string or an integer")
+        if id == None:
+            id = ""
+        id = to_symbol(id, self.ctx)
+        v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
+        return OptimizeObjective(self, v, False)
+
+    def maximize(self, arg):
+        """Add objective function to maximize."""
+        return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), True)
+
+    def minimize(self, arg):
+        """Add objective function to minimize."""
+        return OptimizeObjective(self, Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()), False)
+
+    def push(self):
+        """create a backtracking point for added rules, facts and assertions"""
+        Z3_optimize_push(self.ctx.ref(), self.optimize)
+
+    def pop(self):
+        """restore to previously created backtracking point"""
+        Z3_optimize_pop(self.ctx.ref(), self.optimize)
+
+    def check(self):
+        """Check satisfiability while optimizing objective functions."""
+        return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize))
+
+    def model(self):
+        """Return a model for the last check()."""
+        try:
+            return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
+        except Z3Exception:
+            raise Z3Exception("model is not available")
+
+    def lower(self, obj):
+        if not isinstance(obj, OptimizeObjective):
+            raise Z3Exception("Expecting objective handle returned by maximize/minimize")
+        return obj.lower()
+
+    def upper(self, obj):
+        if not isinstance(obj, OptimizeObjective):
+            raise Z3Exception("Expecting objective handle returned by maximize/minimize")
+        return obj.upper()
+    
+    def __repr__(self):
+        """Return a formatted string with all added rules and constraints."""
+        return self.sexpr()
+
+    def sexpr(self):
+        """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.        
+        """
+        return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
+    
+    def statistics(self):
+        """Return statistics for the last `query()`.
+        """
+        return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
+
+
+        
+
 #########################################
 #
 # ApplyResult
@@ -8022,23 +8194,24 @@ def FP(name, fpsort, ctx=None):
     >>> eq(x, x2)
     True
     """ 
-    ctx = fpsort.ctx
+    if isinstance(fpsort, FPSortRef):
+        ctx = fpsort.ctx
+    else:
+        ctx = _get_ctx(ctx)
     return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
 
 def FPs(names, fpsort, ctx=None):
     """Return an array of floating-point constants.
     
-    >>> x, y, z = BitVecs('x y z', 16)
-    >>> x.size()
-    16
+    >>> x, y, z = FPs('x y z', FPSort(8, 24))
     >>> x.sort()
-    BitVec(16)
-    >>> Sum(x, y, z)
-    0 + x + y + z
-    >>> Product(x, y, z)
-    1*x*y*z
-    >>> simplify(Product(x, y, z))
-    x*y*z
+    FPSort(8, 24)
+    >>> x.sbits()
+    24
+    >>> x.ebits()
+    8
+    >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
+    fpMul(RNE(), fpAdd(RNE(), x, y), z)
     """
     ctx = z3._get_ctx(ctx)
     if isinstance(names, str):

src/api/python/z3printer.py

@@ -1017,6 +1017,8 @@ class Formatter:
             return self.pp_seq(a.assertions(), 0, [])
         elif isinstance(a, z3.Fixedpoint):
             return a.sexpr()
+        elif isinstance(a, z3.Optimize):
+            return a.sexpr()
         elif isinstance(a, z3.ApplyResult):
             return self.pp_seq_seq(a, 0, [])
         elif isinstance(a, z3.ModelRef):

src/api/python/z3types.py

@@ -78,6 +78,10 @@ class FixedpointObj(ctypes.c_void_p):
   def __init__(self, fixedpoint): self._as_parameter_ = fixedpoint
   def from_param(obj): return obj
 
+class OptimizeObj(ctypes.c_void_p):
+  def __init__(self, optimize): self._as_parameter_ = optimize
+  def from_param(obj): return obj
+
 class ModelObj(ctypes.c_void_p):
   def __init__(self, model): self._as_parameter_ = model
   def from_param(obj): return obj

src/api/python/z3util.py

@@ -0,0 +1,468 @@
+"""
+Usage:  
+import common_z3 as CM_Z3
+"""
+
+import common as CM
+from z3 import *
+
+def get_z3_version(as_str=False):
+    major = ctypes.c_uint(0)
+    minor = ctypes.c_uint(0)
+    build = ctypes.c_uint(0)
+    rev   = ctypes.c_uint(0)
+    Z3_get_version(major,minor,build,rev)
+    rs = map(int,(major.value,minor.value,build.value,rev.value))
+    if as_str:
+        return "{}.{}.{}.{}".format(*rs)
+    else:
+        return rs
+        
+    
+
+
+
+def ehash(v):
+    """
+    Returns a 'stronger' hash value than the default hash() method.
+    The result from hash() is not enough to distinguish between 2 
+    z3 expressions in some cases.
+    
+    >>> x1 = Bool('x'); x2 = Bool('x'); x3 = Int('x')
+    >>> print x1.hash(),x2.hash(),x3.hash() #BAD: all same hash values
+    783810685 783810685 783810685
+    >>> print ehash(x1), ehash(x2), ehash(x3)
+    x_783810685_1 x_783810685_1 x_783810685_2
+    
+    """
+    if __debug__:
+        assert is_expr(v)
+
+    return "{}_{}_{}".format(str(v),v.hash(),v.sort_kind())
+
+
+"""
+In Z3, variables are caleld *uninterpreted* consts and 
+variables are *interpreted* consts.
+"""
+
+def is_expr_var(v):
+    """
+    EXAMPLES:
+
+    >>> is_expr_var(Int('7'))
+    True
+    >>> is_expr_var(IntVal('7'))
+    False
+    >>> is_expr_var(Bool('y'))
+    True
+    >>> is_expr_var(Int('x') + 7 == Int('y'))
+    False
+    >>> LOnOff, (On,Off) = EnumSort("LOnOff",['On','Off'])
+    >>> Block,Reset,SafetyInjection=Consts("Block Reset SafetyInjection",LOnOff)
+    >>> is_expr_var(LOnOff)
+    False
+    >>> is_expr_var(On)
+    False
+    >>> is_expr_var(Block)
+    True
+    >>> is_expr_var(SafetyInjection)
+    True
+    """
+
+    return is_const(v) and v.decl().kind()==Z3_OP_UNINTERPRETED
+
+def is_expr_val(v):
+    """
+    EXAMPLES:
+
+    >>> is_expr_val(Int('7'))
+    False
+    >>> is_expr_val(IntVal('7'))
+    True
+    >>> is_expr_val(Bool('y'))
+    False
+    >>> is_expr_val(Int('x') + 7 == Int('y'))
+    False
+    >>> LOnOff, (On,Off) = EnumSort("LOnOff",['On','Off'])
+    >>> Block,Reset,SafetyInjection=Consts("Block Reset SafetyInjection",LOnOff)
+    >>> is_expr_val(LOnOff)
+    False
+    >>> is_expr_val(On)
+    True
+    >>> is_expr_val(Block)
+    False
+    >>> is_expr_val(SafetyInjection)
+    False
+    """        
+    return is_const(v) and v.decl().kind()!=Z3_OP_UNINTERPRETED
+
+
+
+
+def get_vars(f,rs=[]):
+    """
+    >>> x,y = Ints('x y')
+    >>> a,b = Bools('a b')
+    >>> get_vars(Implies(And(x+y==0,x*2==10),Or(a,Implies(a,b==False))))
+    [x, y, a, b]
+
+    """
+    if __debug__:
+        assert is_expr(f)
+
+    if is_const(f):
+        if is_expr_val(f):
+            return rs
+        else:  #variable
+            return CM.vset(rs + [f],str)
+
+    else:
+        for f_ in f.children():
+            rs = get_vars(f_,rs)
+
+        return CM.vset(rs,str)
+
+
+
+def mk_var(name,vsort):
+    if vsort.kind() == Z3_INT_SORT:
+        v = Int(name)
+    elif vsort.kind() == Z3_REAL_SORT:
+        v = Real(name)
+    elif vsort.kind() == Z3_BOOL_SORT:
+        v = Bool(name)
+    elif vsort.kind() == Z3_DATATYPE_SORT:
+        v = Const(name,vsort)
+
+    else:
+        assert False, 'Cannot handle this sort (s: %sid: %d)'\
+            %(vsort,vsort.kind())
+
+    return v
+
+
+
+def prove(claim,assume=None,verbose=0):
+    """
+    >>> r,m = prove(BoolVal(True),verbose=0); r,model_str(m,as_str=False)
+    (True, None)
+
+    #infinite counter example when proving contradiction
+    >>> r,m = prove(BoolVal(False)); r,model_str(m,as_str=False)
+    (False, [])
+
+    >>> x,y,z=Bools('x y z')
+    >>> r,m = prove(And(x,Not(x))); r,model_str(m,as_str=True)
+    (False, '[]')
+
+    >>> r,m = prove(True,assume=And(x,Not(x)),verbose=0)
+    Traceback (most recent call last):
+    ...
+    AssertionError: Assumption is alway False!
+
+    >>> r,m = prove(Implies(x,x),assume=y,verbose=2); r,model_str(m,as_str=False)
+    assume: 
+    y
+    claim: 
+    Implies(x, x)
+    to_prove: 
+    Implies(y, Implies(x, x))
+    (True, None)
+
+    >>> r,m = prove(And(x,True),assume=y,verbose=0); r,model_str(m,as_str=False)
+    (False, [(x, False), (y, True)])
+
+    >>> r,m = prove(And(x,y),assume=y,verbose=0)
+    >>> print r
+    False
+    >>> print model_str(m,as_str=True)
+    x = False
+    y = True
+
+    >>> a,b = Ints('a b')
+    >>> r,m = prove(a**b == b**a,assume=None,verbose=0)
+    E: cannot solve !
+    >>> r is None and m is None
+    True
+
+    """
+
+    if __debug__:
+        assert not assume or is_expr(assume)
+
+
+    to_prove = claim
+    if assume:
+        if __debug__:
+            is_proved,_ = prove(Not(assume))
+
+            def _f():
+                emsg = "Assumption is alway False!"
+                if verbose >= 2:
+                    emsg = "{}\n{}".format(assume,emsg)
+                return emsg
+
+            assert is_proved==False, _f()
+
+        to_prove = Implies(assume,to_prove)
+
+
+
+    if verbose >= 2:
+        print('assume: ')
+        print(assume)
+        print('claim: ')
+        print(claim)
+        print('to_prove: ')
+        print(to_prove)
+
+    f = Not(to_prove)
+
+    models = get_models(f,k=1)
+    if models is None: #unknown
+        print('E: cannot solve !')
+        return None, None
+    elif models == False: #unsat
+        return True,None   
+    else: #sat
+        if __debug__:
+            assert isinstance(models,list)
+
+        if models:
+            return False, models[0] #the first counterexample
+        else:
+            return False, []  #infinite counterexample,models
+        
+
+def get_models(f,k):
+    """
+    Returns the first k models satisfiying f.
+    If f is not satisfiable, returns False.
+    If f cannot be solved, returns None
+    If f is satisfiable, returns the first k models
+    Note that if f is a tautology, e.g.\ True, then the result is []
+    
+    Based on http://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation
+
+    EXAMPLES:
+    >>> x, y = Ints('x y')
+    >>> len(get_models(And(0<=x,x <= 4),k=11))
+    5
+    >>> get_models(And(0<=x**y,x <= 1),k=2) is None
+    True
+    >>> get_models(And(0<=x,x <= -1),k=2)
+    False
+    >>> len(get_models(x+y==7,5))
+    5
+    >>> len(get_models(And(x<=5,x>=1),7))
+    5
+    >>> get_models(And(x<=0,x>=5),7)
+    False
+
+    >>> x = Bool('x')
+    >>> get_models(And(x,Not(x)),k=1)
+    False
+    >>> get_models(Implies(x,x),k=1)
+    []
+    >>> get_models(BoolVal(True),k=1)
+    []
+
+
+
+    """
+
+    if __debug__:
+        assert is_expr(f)
+        assert k>=1
+    
+
+
+    s = Solver()
+    s.add(f)
+
+    models = []
+    i = 0
+    while s.check() == sat and i < k:
+        i = i + 1
+
+        m = s.model()
+
+        if not m: #if m == []
+            break
+
+        models.append(m)
+
+
+        #create new constraint to block the current model
+        block = Not(And([v() == m[v] for v in m]))
+        s.add(block)
+
+    
+    if s.check() == unknown:
+        return None
+    elif s.check() == unsat and i==0:
+        return False
+    else:
+        return models
+
+def is_tautology(claim,verbose=0):
+    """
+    >>> is_tautology(Implies(Bool('x'),Bool('x')))
+    True
+
+    >>> is_tautology(Implies(Bool('x'),Bool('y')))
+    False
+
+    >>> is_tautology(BoolVal(True))
+    True
+
+    >>> is_tautology(BoolVal(False))
+    False
+
+    """
+    return prove(claim=claim,assume=None,verbose=verbose)[0]
+
+
+def is_contradiction(claim,verbose=0):
+    """
+    >>> x,y=Bools('x y')
+    >>> is_contradiction(BoolVal(False))
+    True
+    
+    >>> is_contradiction(BoolVal(True))
+    False
+    
+    >>> is_contradiction(x)
+    False
+    
+    >>> is_contradiction(Implies(x,y))
+    False
+    
+    >>> is_contradiction(Implies(x,x))
+    False
+    
+    >>> is_contradiction(And(x,Not(x)))
+    True
+    """
+
+    return prove(claim=Not(claim),assume=None,verbose=verbose)[0]
+
+
+def exact_one_model(f):
+    """
+    return True if f has exactly 1 model, False otherwise.
+    
+    EXAMPLES:
+
+    >>> x, y = Ints('x y')
+    >>> exact_one_model(And(0<=x**y,x <= 0))
+    False
+
+    >>> exact_one_model(And(0<=x,x <= 0))
+    True
+
+    >>> exact_one_model(And(0<=x,x <= 1))
+    False
+
+    >>> exact_one_model(And(0<=x,x <= -1))
+    False
+    """
+
+    models = get_models(f,k=2)
+    if isinstance(models,list):
+        return len(models)==1
+    else:
+        return False
+        
+    
+
+def myBinOp(op,*L):
+    """
+    >>> myAnd(*[Bool('x'),Bool('y')])
+    And(x, y)
+    
+    >>> myAnd(*[Bool('x'),None])
+    x
+    
+    >>> myAnd(*[Bool('x')])
+    x
+    
+    >>> myAnd(*[])
+    
+    >>> myAnd(Bool('x'),Bool('y'))
+    And(x, y)
+    
+    >>> myAnd(*[Bool('x'),Bool('y')])
+    And(x, y)
+
+    >>> myAnd([Bool('x'),Bool('y')])
+    And(x, y)
+
+    >>> myAnd((Bool('x'),Bool('y')))
+    And(x, y)
+    
+    >>> myAnd(*[Bool('x'),Bool('y'),True])
+    Traceback (most recent call last):
+    ...
+    AssertionError
+    """
+
+    if __debug__:
+        assert op == Z3_OP_OR or op == Z3_OP_AND or op == Z3_OP_IMPLIES
+    
+    if len(L)==1 and (isinstance(L[0],list) or isinstance(L[0],tuple)):
+        L = L[0]
+
+    if __debug__:
+        assert all(not isinstance(l,bool) for l in L)
+
+    L = [l for l in L if is_expr(l)]
+    if L:
+        if len(L)==1:
+            return L[0]
+        else:
+            if op ==  Z3_OP_OR:
+                return Or(L)
+            elif op == Z3_OP_AND:
+                return And(L)
+            else:   #IMPLIES
+                return Implies(L[0],L[1])
+    else:
+        return None
+
+
+def myAnd(*L): return myBinOp(Z3_OP_AND,*L)
+def myOr(*L): return myBinOp(Z3_OP_OR,*L)
+def myImplies(a,b):return myBinOp(Z3_OP_IMPLIES,[a,b])
+    
+
+
+Iff = lambda f,g: And(Implies(f,g),Implies(g,f))
+
+
+
+def model_str(m,as_str=True):
+    """
+    Returned a 'sorted' model (so that it's easier to see)
+    The model is sorted by its key, 
+    e.g. if the model is y = 3 , x = 10, then the result is 
+    x = 10, y = 3
+
+    EXAMPLES:
+    see doctest exampels from function prove() 
+
+    """
+    if __debug__:
+        assert m is None or m == [] or isinstance(m,ModelRef)
+
+    if m :
+        vs = [(v,m[v]) for v in m]
+        vs = sorted(vs,key=lambda a,_: str(a))
+        if as_str:
+            return '\n'.join(['{} = {}'.format(k,v) for (k,v) in vs])
+        else:
+            return vs
+    else:
+        return str(m) if as_str else m
+

src/api/z3_api.h

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #ifndef _Z3_API_H_
 #define _Z3_API_H_
 
@@ -47,6 +53,7 @@ DEFINE_TYPE(Z3_func_interp);
 #define Z3_func_interp_opt Z3_func_interp
 DEFINE_TYPE(Z3_func_entry);
 DEFINE_TYPE(Z3_fixedpoint);
+DEFINE_TYPE(Z3_optimize);
 DEFINE_TYPE(Z3_rcf_num);
 DEFINE_VOID(Z3_theory_data);
 #endif
@@ -85,6 +92,7 @@ DEFINE_VOID(Z3_theory_data);
    - \c Z3_func_interp: interpretation of a function in a model.
    - \c Z3_func_entry: representation of the value of a \c Z3_func_interp at a particular point.
    - \c Z3_fixedpoint: context for the recursive predicate solver.
+   - \c Z3_optimize: context for solving optimization queries.
    - \c Z3_ast_vector: vector of \c Z3_ast objects.
    - \c Z3_ast_map: mapping from \c Z3_ast to \c Z3_ast objects.
    - \c Z3_goal: set of formulas that can be solved and/or transformed using tactics and solvers.
@@ -592,7 +600,10 @@ typedef enum
           }
           This proof object has one antecedent: a hypothetical proof for false.
           It converts the proof in a proof for (or (not l_1) ... (not l_n)),
-          when T1 contains the hypotheses: l_1, ..., l_n.
+          when T1 contains the open hypotheses: l_1, ..., l_n.
+          The hypotheses are closed after an application of a lemma.
+          Furthermore, there are no other open hypotheses in the subtree covered by
+          the lemma.
 
    - Z3_OP_PR_UNIT_RESOLUTION: 
        \nicebox{
@@ -877,6 +888,17 @@ typedef enum
 
       - Z3_OP_DT_ACCESSOR: datatype accessor.
 
+      - Z3_OP_DT_UPDATE_FIELD: datatype field update.
+
+      - Z3_OP_PB_AT_MOST: Cardinality constraint. 
+              E.g., x + y + z <= 2
+      
+      - Z3_OP_PB_LE: Generalized Pseudo-Boolean cardinality constraint.
+              Example  2*x + 3*y <= 4
+
+      - Z3_OP_PB_GE: Generalized Pseudo-Boolean cardinality constraint.
+              Example  2*x + 3*y + 2*z >= 4
+
       - Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: Floating-point rounding mode RNE
       
       - Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: Floating-point rounding mode RNA
@@ -1141,6 +1163,12 @@ typedef enum {
     Z3_OP_DT_CONSTRUCTOR=0x800,
     Z3_OP_DT_RECOGNISER,
     Z3_OP_DT_ACCESSOR,
+    Z3_OP_DT_UPDATE_FIELD,
+
+    // Pseudo Booleans
+    Z3_OP_PB_AT_MOST=0x900,
+    Z3_OP_PB_LE,
+    Z3_OP_PB_GE,
 
     // Floating-Point Arithmetic
     Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN,
@@ -1327,6 +1355,7 @@ typedef enum
   def_Type('FUNC_INTERP',      'Z3_func_interp',      'FuncInterpObj')
   def_Type('FUNC_ENTRY',       'Z3_func_entry',       'FuncEntryObj')
   def_Type('FIXEDPOINT',       'Z3_fixedpoint',       'FixedpointObj')
+  def_Type('OPTIMIZE',         'Z3_optimize',         'OptimizeObj')
   def_Type('PARAM_DESCRS',     'Z3_param_descrs',     'ParamDescrs')
   def_Type('RCF_NUM',          'Z3_rcf_num',          'RCFNumObj')
 */
@@ -3868,6 +3897,28 @@ END_MLAPI_EXCLUDE
     Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(
         __in Z3_context c, __in Z3_sort t, unsigned idx_c, unsigned idx_a);
 
+    /**
+       \brief Update record field with a value.
+
+       This corresponds to the 'with' construct in OCaml. 
+       It has the effect of updating a record field with a given value.
+       The remaining fields are left unchanged. It is the record
+       equivalent of an array store (see \sa Z3_mk_store).
+       If the datatype has more than one constructor, then the update function
+       behaves as identity if there is a miss-match between the accessor and
+       constructor. For example ((_ update-field car) nil 1) is nil, 
+       while ((_ update-field car) (cons 2 nil) 1) is (cons 1 nil).
+
+
+       \pre Z3_get_sort_kind(Z3_get_sort(c, t)) == Z3_get_domain(c, field_access, 1) == Z3_DATATYPE_SORT
+       \pre Z3_get_sort(c, value) == Z3_get_range(c, field_access)
+
+
+       def_API('Z3_datatype_update_field', AST, (_in(CONTEXT), _in(FUNC_DECL), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_datatype_update_field(
+        __in Z3_context c,  __in Z3_func_decl field_access, 
+        __in Z3_ast t, __in Z3_ast value);
 
     /**
         \brief Return arity of relation.
@@ -3893,6 +3944,29 @@ END_MLAPI_EXCLUDE
     Z3_sort Z3_API Z3_get_relation_column(__in Z3_context c, __in Z3_sort s, unsigned col);
 
 
+    /**
+       \brief Pseudo-Boolean relations.
+
+       Encode p1 + p2 + ... + pn <= k
+
+       def_API('Z3_mk_atmost', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in(UINT)))
+    */
+
+    Z3_ast Z3_API Z3_mk_atmost(__in Z3_context c, __in unsigned num_args, 
+                               __in_ecount(num_args) Z3_ast const args[], __in unsigned k);
+
+    /**
+       \brief Pseudo-Boolean relations.
+
+       Encode k1*p1 + k2*p2 + ... + kn*pn <= k
+
+       def_API('Z3_mk_pble', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in_array(1,INT), _in(INT)))
+    */
+
+    Z3_ast Z3_API Z3_mk_pble(__in Z3_context c, __in unsigned num_args, 
+                             __in_ecount(num_args) Z3_ast const args[], __in_ecount(num_args) int coeffs[],
+                             __in int k);
+
     /**
        \mlonly {3 {L Function Declarations}} \endmlonly
     */
@@ -4659,6 +4733,13 @@ END_MLAPI_EXCLUDE
     */
     Z3_ast_opt Z3_API Z3_model_get_const_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl a);
 
+    /**
+       \brief Test if there exists an interpretation (i.e., assignment) for \c a in the model \c m.
+
+       def_API('Z3_model_has_interp', BOOL, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL)))
+    */
+    Z3_bool Z3_API Z3_model_has_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl a);
+
     /**
        \brief Return the interpretation of the function \c f in the model \c m.
        Return \mlonly [None], \endmlonly \conly \c NULL,
@@ -5290,7 +5371,19 @@ END_MLAPI_EXCLUDE
     */
     void Z3_API Z3_reset_memory(void);
 #endif
-    
+
+#ifdef CorML3
+    /**
+       \brief Destroy all allocated resources.
+
+       Any pointers previously returned by the API become invalid.
+       Can be used for memory leak detection.
+
+       def_API('Z3_finalize_memory', VOID, ())
+    */
+    void Z3_API Z3_finalize_memory(void);
+#endif
+
     /*@}*/
 
 #ifdef CorML3
@@ -5947,7 +6040,7 @@ END_MLAPI_EXCLUDE
     /**
        \brief Parse an SMT-LIB2 string with fixedpoint rules. 
        Add the rules to the current fixedpoint context. 
-       Return the set of queries in the file.
+       Return the set of queries in the string.
 
        \param c - context.
        \param f - fixedpoint context.
@@ -6039,6 +6132,197 @@ END_MLAPI_EXCLUDE
 #endif
 #endif
 
+
+
+#ifdef CorML4
+    /**
+        @name Optimize facilities
+    */
+    /*@{*/
+
+    /**
+       \brief Create a new optimize context. 
+       
+       \conly \remark User must use #Z3_optimize_inc_ref and #Z3_optimize_dec_ref to manage optimize objects.
+       \conly Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
+
+       def_API('Z3_mk_optimize', OPTIMIZE, (_in(CONTEXT), ))
+    */
+    Z3_optimize Z3_API Z3_mk_optimize(__in Z3_context c);
+
+#ifdef Conly
+    /**
+       \brief Increment the reference counter of the given optimize context
+       
+       def_API('Z3_optimize_inc_ref', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    void Z3_API Z3_optimize_inc_ref(__in Z3_context c,__in Z3_optimize d);
+
+    /**
+       \brief Decrement the reference counter of the given optimize context.
+
+       def_API('Z3_optimize_dec_ref', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    void Z3_API Z3_optimize_dec_ref(__in Z3_context c,__in Z3_optimize d);
+#endif
+
+    /**
+       \brief Assert hard constraint to the optimization context.
+       
+       def_API('Z3_optimize_assert', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
+    */
+    void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a);
+
+
+    /**
+       \brief Assert soft constraint to the optimization context.
+       \param c - context
+       \param o - optimization context
+       \param a - formula
+       \param weight - a positive weight, penalty for violating soft constraint
+       \param id - optional identifier to group soft constraints
+
+       def_API('Z3_optimize_assert_soft', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(STRING), _in(SYMBOL)))
+    */
+    unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id);
+
+
+    /**
+       \brief Add a maximization constraint.
+       \param c - context
+       \param o - optimization context
+       \param a - arithmetical term       
+       def_API('Z3_optimize_maximize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
+    */
+    unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t);
+
+    /**
+       \brief Add a minimization constraint.
+       \param c - context
+       \param o - optimization context
+       \param a - arithmetical term   
+    
+       def_API('Z3_optimize_minimize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
+    */
+    unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t);
+
+
+    /**
+       \brief Create a backtracking point.
+       
+       The optimize solver contains a set of rules, added facts and assertions.
+       The set of rules, facts and assertions are restored upon calling #Z3_optimize_pop.
+
+       \sa Z3_optimize_pop
+
+       def_API('Z3_optimize_push', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    void Z3_API Z3_optimize_push(Z3_context c,Z3_optimize d);
+
+    /**
+       \brief Backtrack one level.
+       
+       \sa Z3_optimize_push
+
+       \pre The number of calls to pop cannot exceed calls to push.
+
+       def_API('Z3_optimize_pop', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    void Z3_API Z3_optimize_pop(Z3_context c,Z3_optimize d);
+
+    /**
+       \brief Check consistency and produce optimal values.
+       \param c - context
+       \param o - optimization context
+       
+       def_API('Z3_optimize_check', INT, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o);
+
+
+    /**
+       \brief Retrieve the model for the last #Z3_optimize_check
+
+       The error handler is invoked if a model is not available because 
+       the commands above were not invoked for the given optimization 
+       solver, or if the result was \c Z3_L_FALSE.
+       
+       def_API('Z3_optimize_get_model', MODEL, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o);
+
+    /**
+       \brief Set parameters on optimization context.       
+
+       \param c - context
+       \param o - optimization context
+       \param p - parameters
+
+       def_API('Z3_optimize_set_params', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(PARAMS)))
+    */
+    void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p);
+
+    /**
+       \brief Return the parameter description set for the given optimize object.
+
+       \param c - context
+       \param o - optimization context
+
+       def_API('Z3_optimize_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT), _in(OPTIMIZE)))
+    */    
+    Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o);
+
+    /**
+       \brief Retrieve lower bound value or approximation for the i'th optimization objective.
+
+       \param c - context
+       \param o - optimization context
+       \param idx - index of optimization objective
+
+       def_API('Z3_optimize_get_lower', AST, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT)))
+    */
+    Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx);
+
+    /**
+       \brief Retrieve upper bound value or approximation for the i'th optimization objective.
+
+       \param c - context
+       \param o - optimization context
+       \param idx - index of optimization objective
+
+       def_API('Z3_optimize_get_upper', AST, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT)))
+    */
+    Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx);
+
+    /**
+       \brief Print the current context as a string.
+       \param c - context.
+       \param o - optimization context.
+
+       def_API('Z3_optimize_to_string', STRING, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    Z3_string Z3_API Z3_optimize_to_string(
+        __in Z3_context c, 
+        __in Z3_optimize o);
+
+
+    /**
+       \brief Return a string containing a description of parameters accepted by optimize.
+
+       def_API('Z3_optimize_get_help', STRING, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    Z3_string Z3_API Z3_optimize_get_help(__in Z3_context c, __in Z3_optimize t);
+
+    /**
+       \brief Retrieve statistics information from the last call to #Z3_optimize_check
+
+       def_API('Z3_optimize_get_statistics', STATS, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    Z3_stats Z3_API Z3_optimize_get_statistics(__in Z3_context c,__in Z3_optimize d);
+
+
+#endif
+
 #ifdef CorML4
     /*@}*/
     
@@ -6667,7 +6951,7 @@ END_MLAPI_EXCLUDE
 
        def_API('Z3_tactic_apply_ex', APPLY_RESULT, (_in(CONTEXT), _in(TACTIC), _in(GOAL), _in(PARAMS)))
     */
-    Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p);
+    Z3_apply_result Z3_API Z3_tactic_apply_ex(__in Z3_context c, __in Z3_tactic t, __in Z3_goal g, __in Z3_params p);
 
 #ifdef CorML3
     /**

src/api/z3_fpa.h

@@ -858,6 +858,20 @@ extern "C" {
     */
     Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t);
 
+    /**
+        \brief Return the significand value of a floating-point numeral as a uint64.
+
+        \param c logical context
+        \param t a floating-point numeral
+
+        Remarks: This function extracts the significand bits in `t`, without the 
+        hidden bit or normalization. Sets the Z3_INVALID_ARG error code if the 
+        significand does not fit into a uint64.
+
+        def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64)))
+    */
+    Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(__in Z3_context c, __in Z3_ast t, __out __uint64 * n);
+
     /**
         \brief Return the exponent value of a floating-point numeral as a string
 

src/api/z3_macros.h

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #ifndef __in
 #define __in
 #endif

src/api/z3_replayer.cpp

@@ -22,12 +22,14 @@ Notes:
 #include"stream_buffer.h"
 #include"symbol.h"
 #include"trace.h"
+#include<sstream>
 
 void register_z3_replayer_cmds(z3_replayer & in);
 
+
 void throw_invalid_reference() {
     TRACE("z3_replayer", tout << "invalid argument reference\n";);
-    throw z3_replayer_exception("invalid argument reference");
+    throw z3_replayer_exception("invalid argument reference1");
 }
 
 struct z3_replayer::imp {
@@ -45,7 +47,38 @@ struct z3_replayer::imp {
     size_t_map<void *>       m_heap;
     svector<z3_replayer_cmd> m_cmds;
 
-    enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY, FLOAT };
+    enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, INT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY, FLOAT };
+
+    char const* kind2string(value_kind k) const {
+        switch (k) {
+        case INT64: return "int64";
+        case UINT64: return "uint64";
+        case DOUBLE: return "double";
+        case STRING: return "string";
+        case SYMBOL: return "symbol";
+        case OBJECT: return "object";
+        case UINT_ARRAY: return "uint_array";
+        case INT_ARRAY: return "int_array";
+        case SYMBOL_ARRAY: return "symbol_array";
+        case OBJECT_ARRAY: return "object_array";
+        case FLOAT: return "float";
+        default: UNREACHABLE(); return "unknown";
+        }
+    }
+
+
+    void check_arg(unsigned pos, value_kind k) const {
+        if (pos >= m_args.size()) {
+            TRACE("z3_replayer", tout << "too few arguments " << m_args.size() << " expecting " << kind2string(k) << "\n";);
+            throw z3_replayer_exception("invalid argument reference2");
+        }
+        if (m_args[pos].m_kind != k) {
+            std::stringstream strm;
+            strm << "expecting " << kind2string(k) << " at position " 
+                 << pos << " but got " << kind2string(m_args[pos].m_kind);
+            throw z3_replayer_exception(strm.str().c_str());
+        }
+    }
 
     struct value { 
         value_kind m_kind;
@@ -71,6 +104,7 @@ struct z3_replayer::imp {
     vector<ptr_vector<void> >   m_obj_arrays;
     vector<svector<Z3_symbol> > m_sym_arrays;
     vector<unsigned_vector>     m_unsigned_arrays;
+    vector<svector<int> >       m_int_arrays;
 
     imp(z3_replayer & o, std::istream & in):
         m_owner(o),
@@ -321,6 +355,15 @@ struct z3_replayer::imp {
                 v.push_back(static_cast<unsigned>(m_args[i].m_uint));
             }
         }
+        if (k == INT64) {
+            aidx = m_int_arrays.size();
+            nk   = INT_ARRAY;
+            m_int_arrays.push_back(svector<int>());
+            svector<int> & v = m_int_arrays.back();
+            for (unsigned i = asz - sz; i < asz; i++) {
+                v.push_back(static_cast<int>(m_args[i].m_int));
+            }
+        }
         else if (k == SYMBOL) {
             aidx = m_sym_arrays.size();
             nk   = SYMBOL_ARRAY;
@@ -489,8 +532,7 @@ struct z3_replayer::imp {
                 next(); skip_blank(); read_ptr(); skip_blank(); read_uint64();
                 unsigned pos = static_cast<unsigned>(m_uint64);
                 TRACE("z3_replayer", tout << "[" << m_line << "] " << "* " << m_ptr << " " << pos << "\n";);
-                if (pos >= m_args.size() || m_args[pos].m_kind != OBJECT)
-                    throw_invalid_reference();
+                check_arg(pos, OBJECT);
                 m_heap.insert(m_ptr, m_args[pos].m_obj);
                 break;
             }
@@ -499,8 +541,7 @@ struct z3_replayer::imp {
                 // @ obj_id array_pos idx
                 next(); skip_blank(); read_ptr(); skip_blank(); read_uint64();
                 unsigned pos = static_cast<unsigned>(m_uint64);
-                if (pos >= m_args.size() || m_args[pos].m_kind != OBJECT_ARRAY)
-                    throw_invalid_reference();
+                check_arg(pos, OBJECT_ARRAY);
                 unsigned aidx = static_cast<unsigned>(m_args[pos].m_uint);
                 ptr_vector<void> & v = m_obj_arrays[aidx];
                 skip_blank(); read_uint64();
@@ -525,26 +566,22 @@ struct z3_replayer::imp {
     }
 
     int get_int(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != INT64)
-            throw_invalid_reference();
+        check_arg(pos, INT64);
         return static_cast<int>(m_args[pos].m_int);
     }
 
     __int64 get_int64(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != INT64)
-            throw_invalid_reference();
+        check_arg(pos, INT64);
         return m_args[pos].m_int;
     }
 
     unsigned get_uint(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != UINT64)
-            throw_invalid_reference();
+        check_arg(pos, UINT64);
         return static_cast<unsigned>(m_args[pos].m_uint);
     }
 
     __uint64 get_uint64(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != UINT64)
-            throw_invalid_reference();
+        check_arg(pos, UINT64);
         return m_args[pos].m_uint;
     }
 
@@ -555,46 +592,45 @@ struct z3_replayer::imp {
     }
 
     double get_double(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != DOUBLE)
-            throw_invalid_reference();
+        check_arg(pos, DOUBLE);
         return m_args[pos].m_double;
     }
 
     Z3_string get_str(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != STRING)
-            throw_invalid_reference();
+        check_arg(pos, STRING);
         return m_args[pos].m_str;
     }
 
     Z3_symbol get_symbol(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != SYMBOL)
-            throw_invalid_reference();
+        check_arg(pos, SYMBOL);
         return reinterpret_cast<Z3_symbol>(const_cast<char*>(m_args[pos].m_str));
     }
 
     void * get_obj(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != OBJECT)
-            throw_invalid_reference();
+        check_arg(pos, OBJECT);
         return m_args[pos].m_obj;
     }
 
     unsigned * get_uint_array(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != UINT_ARRAY)
-            throw_invalid_reference();
+        check_arg(pos, UINT_ARRAY);
         unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
         return m_unsigned_arrays[idx].c_ptr();
     }
 
+    int * get_int_array(unsigned pos) const {
+        check_arg(pos, INT_ARRAY);
+        unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
+        return m_int_arrays[idx].c_ptr();
+    }
+
     Z3_symbol * get_symbol_array(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != SYMBOL_ARRAY)
-            throw_invalid_reference();
+        check_arg(pos, SYMBOL_ARRAY);
         unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
         return m_sym_arrays[idx].c_ptr();
     }
 
     void ** get_obj_array(unsigned pos) const {
-        if (pos >= m_args.size() || m_args[pos].m_kind != OBJECT_ARRAY)
-            throw_invalid_reference();
+        check_arg(pos, OBJECT_ARRAY);
         unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
         ptr_vector<void> const & v = m_obj_arrays[idx];
         TRACE("z3_replayer_bug", tout << "pos: " << pos << ", idx: " << idx << " size(): " << v.size() << "\n";
@@ -603,38 +639,32 @@ struct z3_replayer::imp {
     }
 
     int * get_int_addr(unsigned pos) {
-        if (pos >= m_args.size() || m_args[pos].m_kind != INT64)
-            throw_invalid_reference();
+        check_arg(pos, INT64);
         return reinterpret_cast<int*>(&(m_args[pos].m_int));
     }
 
     __int64 * get_int64_addr(unsigned pos) {
-        if (pos >= m_args.size() || m_args[pos].m_kind != INT64)
-            throw_invalid_reference();
+        check_arg(pos, INT64);
         return &(m_args[pos].m_int);
     }
 
     unsigned * get_uint_addr(unsigned pos) {
-        if (pos >= m_args.size() || m_args[pos].m_kind != UINT64)
-            throw_invalid_reference();
+        check_arg(pos, UINT64);
         return reinterpret_cast<unsigned*>(&(m_args[pos].m_uint));
     }
 
     __uint64 * get_uint64_addr(unsigned pos) {
-        if (pos >= m_args.size() || m_args[pos].m_kind != UINT64)
-            throw_invalid_reference();
+        check_arg(pos, UINT64);
         return &(m_args[pos].m_uint);
     }
 
     Z3_string * get_str_addr(unsigned pos) {
-        if (pos >= m_args.size() || m_args[pos].m_kind != STRING)
-            throw_invalid_reference();
+        check_arg(pos, STRING);
         return &(m_args[pos].m_str);
     }
 
     void ** get_obj_addr(unsigned pos) {
-        if (pos >= m_args.size() || m_args[pos].m_kind != OBJECT)
-            throw_invalid_reference();
+        check_arg(pos, OBJECT);
         return &(m_args[pos].m_obj);
     }
 
@@ -653,6 +683,7 @@ struct z3_replayer::imp {
         m_obj_arrays.reset();
         m_sym_arrays.reset();
         m_unsigned_arrays.reset();
+        m_int_arrays.reset();
     }
     
   
@@ -715,6 +746,10 @@ unsigned * z3_replayer::get_uint_array(unsigned pos) const {
     return m_imp->get_uint_array(pos);
 }
 
+int * z3_replayer::get_int_array(unsigned pos) const {
+    return m_imp->get_int_array(pos);
+}
+
 Z3_symbol * z3_replayer::get_symbol_array(unsigned pos) const {
     return m_imp->get_symbol_array(pos);
 }

src/api/z3_replayer.h

@@ -50,6 +50,7 @@ public:
     void * get_obj(unsigned pos) const;
 
     unsigned * get_uint_array(unsigned pos) const;
+    int * get_int_array(unsigned pos) const;
     Z3_symbol * get_symbol_array(unsigned pos) const;
     void ** get_obj_array(unsigned pos) const;
 

src/ast/ast.cpp

@@ -316,7 +316,8 @@ func_decl::func_decl(symbol const & name, unsigned arity, sort * const * domain,
     decl(AST_FUNC_DECL, name, info),
     m_arity(arity),
     m_range(range) {
-    memcpy(const_cast<sort **>(get_domain()), domain, sizeof(sort *) * arity);
+    if (arity != 0)
+        memcpy(const_cast<sort **>(get_domain()), domain, sizeof(sort *) * arity);
 }
 
 // -----------------------------------
@@ -378,8 +379,10 @@ quantifier::quantifier(bool forall, unsigned num_decls, sort * const * decl_sort
 
     memcpy(const_cast<sort **>(get_decl_sorts()), decl_sorts, sizeof(sort *) * num_decls);
     memcpy(const_cast<symbol*>(get_decl_names()), decl_names, sizeof(symbol) * num_decls);
-    memcpy(const_cast<expr **>(get_patterns()), patterns, sizeof(expr *) * num_patterns);
-    memcpy(const_cast<expr **>(get_no_patterns()), no_patterns, sizeof(expr *) * num_no_patterns);
+    if (num_patterns != 0)
+        memcpy(const_cast<expr **>(get_patterns()), patterns, sizeof(expr *) * num_patterns);
+    if (num_no_patterns != 0)
+        memcpy(const_cast<expr **>(get_no_patterns()), no_patterns, sizeof(expr *) * num_no_patterns);
 }
 
 // -----------------------------------
@@ -1043,6 +1046,13 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
     case OP_DISTINCT: {
         func_decl_info info(m_family_id, OP_DISTINCT);
         info.set_pairwise();
+        for (unsigned i = 1; i < arity; i++) {        
+            if (domain[i] != domain[0]) {
+                std::ostringstream buffer;
+                buffer << "Sort mismatch between first argument and argument " << (i+1);
+                throw ast_exception(buffer.str().c_str());
+            }
+        }
         return m_manager->mk_func_decl(symbol("distinct"), arity, domain, m_bool_sort, info);
     }
     default:
@@ -2036,7 +2046,13 @@ inline app * ast_manager::mk_app_core(func_decl * decl, expr * arg1, expr * arg2
 }
 
 app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * args) {
-    SASSERT(decl->get_arity() == num_args || decl->is_right_associative() || decl->is_left_associative() || decl->is_chainable());
+    if (decl->get_arity() != num_args && !decl->is_right_associative() && 
+        !decl->is_left_associative() && !decl->is_chainable()) {
+        std::ostringstream buffer;
+        buffer << "Wrong number of arguments (" << num_args 
+               << ") passed to function " << mk_pp(decl, *this);        
+        throw ast_exception(buffer.str().c_str());
+    }
     app * r = 0;
     if (num_args > 2 && !decl->is_flat_associative()) {
         if (decl->is_right_associative()) {
@@ -2071,6 +2087,8 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar
     return r;
 }
 
+
+
 func_decl * ast_manager::mk_fresh_func_decl(symbol const & prefix, symbol const & suffix, unsigned arity, 
                                             sort * const * domain, sort * range) {
     func_decl_info info(null_family_id, null_decl_kind);
@@ -2338,6 +2356,10 @@ quantifier * ast_manager::update_quantifier(quantifier * q, bool is_forall, unsi
                          num_patterns == 0 ? q->get_no_patterns() : 0);
 }
 
+app * ast_manager::mk_distinct(unsigned num_args, expr * const * args) {
+    return mk_app(m_basic_family_id, OP_DISTINCT, num_args, args);
+}
+
 app * ast_manager::mk_distinct_expanded(unsigned num_args, expr * const * args) {
     if (num_args < 2)
         return mk_true();

src/ast/ast.h

@@ -2000,12 +2000,13 @@ public:
     app * mk_and(expr * arg1, expr * arg2, expr * arg3) { return mk_app(m_basic_family_id, OP_AND, arg1, arg2, arg3); }
     app * mk_implies(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_IMPLIES, arg1, arg2); }
     app * mk_not(expr * n) { return mk_app(m_basic_family_id, OP_NOT, n); }
-    app * mk_distinct(unsigned num_args, expr * const * args) { return mk_app(m_basic_family_id, OP_DISTINCT, num_args, args); }
+    app * mk_distinct(unsigned num_args, expr * const * args);
     app * mk_distinct_expanded(unsigned num_args, expr * const * args);
     app * mk_true() { return m_true; }
     app * mk_false() { return m_false; }
     app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); }
 
+
     func_decl* mk_and_decl() { 
         sort* domain[2] = { m_bool_sort, m_bool_sort };
         return mk_func_decl(m_basic_family_id, OP_AND, 0, 0, 2, domain); 

src/ast/ast_smt2_pp.cpp

@@ -77,6 +77,8 @@ bool smt2_pp_environment::is_indexed_fdecl(func_decl * f) const {
     for (i = 0; i < num; i++) {
         if (f->get_parameter(i).is_int())
             continue;
+        if (f->get_parameter(i).is_rational())
+            continue;
         if (f->get_parameter(i).is_ast() && is_func_decl(f->get_parameter(i).get_ast()))
             continue;
         break;
@@ -105,9 +107,13 @@ format * smt2_pp_environment::pp_fdecl_params(format * fname, func_decl * f) {
     ptr_buffer<format> fs;
     fs.push_back(fname);
     for (unsigned i = 0; i < num; i++) {
-        SASSERT(f->get_parameter(i).is_int() || (f->get_parameter(i).is_ast() && is_func_decl(f->get_parameter(i).get_ast())));
+        SASSERT(f->get_parameter(i).is_int() || 
+                f->get_parameter(i).is_rational() || 
+                (f->get_parameter(i).is_ast() && is_func_decl(f->get_parameter(i).get_ast())));
         if (f->get_parameter(i).is_int())
             fs.push_back(mk_int(get_manager(), f->get_parameter(i).get_int()));
+        else if (f->get_parameter(i).is_rational())
+            fs.push_back(mk_string(get_manager(), f->get_parameter(i).get_rational().to_string().c_str()));
         else
             fs.push_back(pp_fdecl_ref(to_func_decl(f->get_parameter(i).get_ast())));
     }
@@ -335,22 +341,22 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d
     }
     else {
         SASSERT(u.is_irrational_algebraic_numeral(t));
-        anum const & val = u.to_irrational_algebraic_numeral(t);
+        anum const & val2 = u.to_irrational_algebraic_numeral(t);
         algebraic_numbers::manager & am = u.am();
         format * vf;
         std::ostringstream buffer;
         bool is_neg = false;
         if (decimal) {
             scoped_anum abs_val(am);
-            am.set(abs_val, val);
-            if (am.is_neg(val)) {
+            am.set(abs_val, val2);
+            if (am.is_neg(val2)) {
                 is_neg = true;
                 am.neg(abs_val);
             }
             am.display_decimal(buffer, abs_val, decimal_prec);
         }
         else {
-            am.display_root_smt2(buffer, val); 
+            am.display_root_smt2(buffer, val2); 
         }
         vf = mk_string(get_manager(), buffer.str().c_str());
         return is_neg ? mk_neg(vf) : vf;
@@ -1159,6 +1165,26 @@ std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p) {
     return out;
 }
 
+std::ostream& operator<<(std::ostream& out, expr_ref const&  e) {
+    return out << mk_ismt2_pp(e.get(), e.get_manager());
+}
+
+std::ostream& operator<<(std::ostream& out, app_ref const&  e) {
+    return out << mk_ismt2_pp(e.get(), e.get_manager());
+}
+
+std::ostream& operator<<(std::ostream& out, expr_ref_vector const&  e) {
+    for (unsigned i = 0; i < e.size(); ++i) 
+        out << mk_ismt2_pp(e[i], e.get_manager()) << "\n";
+    return out;
+}
+
+std::ostream& operator<<(std::ostream& out, app_ref_vector const&  e) {
+    for (unsigned i = 0; i < e.size(); ++i) 
+        out << mk_ismt2_pp(e[i], e.get_manager()) << "\n";
+    return out;
+}
+
 #ifdef Z3DEBUG
 void pp(expr const * n, ast_manager & m) {
     std::cout << mk_ismt2_pp(const_cast<expr*>(n), m) << std::endl;

src/ast/ast_smt2_pp.h

@@ -110,4 +110,10 @@ struct mk_ismt2_pp {
 
 std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p);
 
+std::ostream& operator<<(std::ostream& out, expr_ref const& e);
+std::ostream& operator<<(std::ostream& out, app_ref const& e);
+
+std::ostream& operator<<(std::ostream& out, expr_ref_vector const& e);
+std::ostream& operator<<(std::ostream& out, app_ref_vector const& e);
+
 #endif

src/ast/ast_smt_pp.cpp

@@ -1058,7 +1058,8 @@ void ast_smt_pp::display_ast_smt2(std::ostream& strm, ast* a, unsigned indent, u
 
 void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     ptr_vector<quantifier> ql;
-    decl_collector decls(m_manager);
+    ast_manager& m = m_manager;
+    decl_collector decls(m);
     smt_renaming rn;    
 
     for (unsigned i = 0; i < m_assumptions.size(); ++i) {
@@ -1069,7 +1070,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     }
     decls.visit(n);    
 
-    if (m_manager.is_proof(n)) {
+    if (m.is_proof(n)) {
         strm << "(";
     }
     if (m_benchmark_name != symbol::null) {
@@ -1078,7 +1079,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     if (m_source_info != symbol::null && m_source_info != symbol("")) {
         strm << "; :source { " << m_source_info << " }\n";
     }    
-    if (m_manager.is_bool(n)) {
+    if (m.is_bool(n)) {
         strm << "(set-info :status " << m_status << ")\n";
     }
     if (m_category != symbol::null && m_category != symbol("")) {
@@ -1095,7 +1096,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     for (unsigned i = 0; i < decls.get_num_sorts(); ++i) {
         sort* s = decls.get_sorts()[i];
         if (!(*m_is_declared)(s)) {
-            smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
+            smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
             p.pp_sort_decl(sort_mark, s);
         }        
     }
@@ -1103,7 +1104,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     for (unsigned i = 0; i < decls.get_num_decls(); ++i) {
         func_decl* d = decls.get_func_decls()[i];
         if (!(*m_is_declared)(d)) {
-            smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
+            smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
             p(d);
             strm << "\n";
         }
@@ -1112,34 +1113,36 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     for (unsigned i = 0; i < decls.get_num_preds(); ++i) {
         func_decl* d = decls.get_pred_decls()[i];
         if (!(*m_is_declared)(d)) {
-            smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
+            smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
             p(d);
             strm << "\n";
         }
     }
 
     for (unsigned i = 0; i < m_assumptions.size(); ++i) {
-        strm << "(assert\n";
-        smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0);
-        p(m_assumptions[i].get());   
-        strm << ")\n";     
+        smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
+        strm << "(assert\n ";
+        p(m_assumptions[i].get());
+        strm << ")\n";
     }
 
     for (unsigned i = 0; i < m_assumptions_star.size(); ++i) {        
-        strm << "(assert\n";
-        smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0);
-        p(m_assumptions_star[i].get());        
+        smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
+        strm << "(assert\n ";
+        p(m_assumptions_star[i].get());
         strm << ")\n";
     }
 
-    smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0);
-    if (m_manager.is_bool(n)) {
-        strm << "(assert\n";
-        p(n);
-        strm << ")\n";
+    smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 0);
+    if (m.is_bool(n)) {
+        if (!m.is_true(n)) {
+            strm << "(assert\n ";
+            p(n);
+            strm << ")\n";
+        }
         strm << "(check-sat)\n";
     }
-    else if (m_manager.is_proof(n)) {
+    else if (m.is_proof(n)) {
         strm << "(proof\n";
         p(n);
         strm << "))\n";

src/ast/ast_trail.h

@@ -0,0 +1,76 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    ast_trail.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-06-02.
+
+Revision History:
+
+    Extracted AST specific features from trail.h
+    nbjorner 2014-9-28
+
+--*/
+#ifndef _AST_TRAIL_H_
+#define _AST_TRAIL_H_
+
+#include"ast.h"
+#include"trail.h"
+
+
+template<typename S, typename T>
+class ast2ast_trailmap {
+    ref_vector<S, ast_manager> m_domain;
+    ref_vector<T, ast_manager> m_range;
+    obj_map<S, T*>             m_map;
+public:
+    ast2ast_trailmap(ast_manager& m):
+        m_domain(m),
+        m_range(m), 
+        m_map()
+    {}
+
+    bool find(S* s, T*& t) {
+        return m_map.find(s,t);
+    }
+    
+    void insert(S* s, T* t) {
+        SASSERT(!m_map.contains(s));
+        m_domain.push_back(s);
+        m_range.push_back(t);
+        m_map.insert(s,t);
+    }
+    
+    void pop() {
+        SASSERT(!m_domain.empty());
+        m_map.remove(m_domain.back());
+        m_domain.pop_back();
+        m_range.pop_back();
+    }
+};
+
+template<typename Ctx, typename S, typename T>
+class ast2ast_trail : public trail<Ctx> {
+    ast2ast_trailmap<S,T>& m_map;
+public:
+    ast2ast_trail(ast2ast_trailmap<S,T>& m, S* s, T* t) : 
+        m_map(m) {
+        m.insert(s,t);
+    }
+
+    virtual void undo(Ctx& ctx) {
+        m_map.pop();
+    }    
+};
+
+
+#endif /* _AST_TRAIL_H_ */
+

src/ast/ast_util.cpp

@@ -44,12 +44,12 @@ app * mk_list_assoc_app(ast_manager & m, family_id fid, decl_kind k, unsigned nu
     return mk_list_assoc_app(m, decl, num_args, args);
 }
 
-bool is_well_formed_vars(ptr_vector<sort>& bound, expr* e) {
+bool is_well_formed_vars(ptr_vector<sort>& bound, expr * top) {
     ptr_vector<expr> todo;
     ast_mark mark;
-    todo.push_back(e);
+    todo.push_back(top);
     while (!todo.empty()) {
-        expr* e = todo.back();
+        expr * e = todo.back();
         todo.pop_back();
         if (mark.is_marked(e)) {
             continue;

src/ast/bv_decl_plugin.cpp

@@ -501,13 +501,17 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
     func_decl * r = mk_func_decl(k, bv_size);
     if (r != 0) {
         if (arity != r->get_arity()) {
-            m_manager->raise_exception("declared arity mismatches supplied arity");
-            return 0;            
+            if (r->get_info()->is_associative())
+                arity = r->get_arity();
+            else {
+                m_manager->raise_exception("declared arity mismatches supplied arity");
+                return 0;
+            }
         }
         for (unsigned i = 0; i < arity; ++i) {
             if (domain[i] != r->get_domain(i)) {
                 m_manager->raise_exception("declared sorts do not match supplied sorts");
-                return 0;            
+                return 0;
             }
         }
         return r;
@@ -566,6 +570,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
 
 func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                          unsigned num_args, expr * const * args, sort * range) {
+    ast_manager& m = *m_manager;
     int bv_size;
     if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) {
         // bv_size is filled in.
@@ -589,11 +594,35 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
         return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range);
     }
     else if (num_args == 0 || !get_bv_size(args[0], bv_size)) {
-        m_manager->raise_exception("operator is applied to arguments of the wrong sort");
+        m.raise_exception("operator is applied to arguments of the wrong sort");
         return 0;
     }
     func_decl * r = mk_func_decl(k, bv_size);
     if (r != 0) {
+        if (num_args != r->get_arity()) {
+            if (r->get_info()->is_associative()) {
+                sort * fs = r->get_domain(0);
+                for (unsigned i = 0; i < num_args; ++i) {
+                    if (m.get_sort(args[i]) != fs) {
+                        m_manager->raise_exception("declared sorts do not match supplied sorts");
+                        return 0;
+                    }
+                }
+                return r;
+            }
+            else {
+                m.raise_exception("declared arity mismatches supplied arity");
+                return 0;
+            }
+        }
+        for (unsigned i = 0; i < num_args; ++i) {
+            if (m.get_sort(args[i]) != r->get_domain(i)) {
+                std::ostringstream buffer;
+                buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " does not match declaration " << mk_pp(r, m);
+                m.raise_exception(buffer.str().c_str());
+                return 0;
+            }
+        }
         return r;
     }
     return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range);

src/ast/datatype_decl_plugin.cpp

@@ -149,10 +149,10 @@ enum status {
 */
 static bool is_recursive_datatype(parameter const * parameters) {
     unsigned num_types          = parameters[0].get_int();
-    unsigned tid                = parameters[1].get_int();
+    unsigned top_tid            = parameters[1].get_int();
     buffer<status>    already_found(num_types, WHITE);
     buffer<unsigned>  todo;
-    todo.push_back(tid);
+    todo.push_back(top_tid);
     while (!todo.empty()) {
         unsigned tid = todo.back();
         if (already_found[tid] == BLACK) {
@@ -198,11 +198,11 @@ static bool is_recursive_datatype(parameter const * parameters) {
 */
 static sort_size get_datatype_size(parameter const * parameters) {
     unsigned num_types          = parameters[0].get_int();
-    unsigned tid                = parameters[1].get_int();
+    unsigned top_tid            = parameters[1].get_int();
     buffer<sort_size> szs(num_types, sort_size());
     buffer<status>    already_found(num_types, WHITE);
     buffer<unsigned>  todo;
-    todo.push_back(tid);
+    todo.push_back(top_tid);
     while (!todo.empty()) {
         unsigned tid  = todo.back();
         if (already_found[tid] == BLACK) {
@@ -280,7 +280,7 @@ static sort_size get_datatype_size(parameter const * parameters) {
             }
         }
     }
-    return szs[tid];
+    return szs[top_tid];
 }
 
 /**
@@ -422,8 +422,55 @@ static sort * get_type(ast_manager & m, family_id datatype_fid, sort * source_da
     }
 }
 
+func_decl * datatype_decl_plugin::mk_update_field(
+    unsigned num_parameters, parameter const * parameters, 
+    unsigned arity, sort * const * domain, sort * range) {
+    decl_kind k = OP_DT_UPDATE_FIELD;
+    ast_manager& m = *m_manager;
+
+    if (num_parameters != 1 || !parameters[0].is_ast()) {
+        m.raise_exception("invalid parameters for datatype field update");
+        return 0;
+    }
+    if (arity != 2) {
+        m.raise_exception("invalid number of arguments for datatype field update");
+        return 0;
+    }
+    func_decl* acc = 0;
+    if (is_func_decl(parameters[0].get_ast())) {
+        acc = to_func_decl(parameters[0].get_ast());
+    }
+    if (acc && !get_util().is_accessor(acc)) {
+        acc = 0;
+    }
+    if (!acc) {
+        m.raise_exception("datatype field update requires a datatype accessor as the second argument");
+        return 0;
+    }
+    sort* dom = acc->get_domain(0);
+    sort* rng = acc->get_range();
+    if (dom != domain[0]) {
+        m.raise_exception("first argument to field update should be a data-type");
+        return 0;
+    }
+    if (rng != domain[1]) {
+        std::ostringstream buffer;
+        buffer << "second argument to field update should be " << mk_ismt2_pp(rng, m) 
+               << " instead of " << mk_ismt2_pp(domain[1], m);
+        m.raise_exception(buffer.str().c_str());
+        return 0;
+    }
+    range = domain[0];
+    func_decl_info info(m_family_id, k, num_parameters, parameters);
+    return m.mk_func_decl(symbol("update_field"), arity, domain, range, info);
+}
+
 func_decl * datatype_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                              unsigned arity, sort * const * domain, sort * range) {
+
+    if (k == OP_DT_UPDATE_FIELD) {
+        return mk_update_field(num_parameters, parameters, arity, domain, range);
+    }
     if (num_parameters < 2 || !parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) {
         m_manager->raise_exception("invalid parameters for datatype operator");
         return 0;
@@ -521,6 +568,9 @@ func_decl * datatype_decl_plugin::mk_func_decl(decl_kind k, unsigned num_paramet
             return m_manager->mk_func_decl(a_name, arity, domain, a_type, info);
         }
         break;
+    case OP_DT_UPDATE_FIELD: 
+        UNREACHABLE();
+        return 0;
     default:
         m_manager->raise_exception("invalid datatype operator kind");
         return 0;
@@ -607,8 +657,8 @@ bool datatype_decl_plugin::is_fully_interp(sort const * s) const {
     for (unsigned tid = 0; tid < num_types; tid++) {
         unsigned o                 = parameters[2 + 2*tid + 1].get_int(); // constructor offset
         unsigned num_constructors  = parameters[o].get_int();
-        for (unsigned s = 1; s <= num_constructors; s++) {
-            unsigned k_i           = parameters[o + s].get_int();
+        for (unsigned si = 1; si <= num_constructors; si++) {
+            unsigned k_i           = parameters[o + si].get_int();
             unsigned num_accessors = parameters[k_i + 2].get_int();
             unsigned r = 0;
             for (; r < num_accessors; r++) {
@@ -672,6 +722,13 @@ bool datatype_decl_plugin::is_value(app * e) const {
     return true;
 }
 
+void datatype_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
+    if (logic == symbol::null) {
+        op_names.push_back(builtin_name("update-field", OP_DT_UPDATE_FIELD));
+    }
+}
+
+
 datatype_util::datatype_util(ast_manager & m):
     m_manager(m),
     m_family_id(m.mk_family_id("datatype")),

src/ast/datatype_decl_plugin.h

@@ -32,6 +32,7 @@ enum datatype_op_kind {
     OP_DT_CONSTRUCTOR,
     OP_DT_RECOGNISER,
     OP_DT_ACCESSOR,
+    OP_DT_UPDATE_FIELD,
     LAST_DT_OP
 };
 
@@ -149,8 +150,14 @@ public:
 
     virtual bool is_unique_value(app * e) const { return is_value(e); }
 
+    virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
+
 private:
     bool is_value_visit(expr * arg, ptr_buffer<app> & todo) const;
+
+    func_decl * mk_update_field(
+        unsigned num_parameters, parameter const * parameters, 
+        unsigned arity, sort * const * domain, sort * range);
 };
 
 class datatype_util {
@@ -181,9 +188,11 @@ public:
     bool is_constructor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_CONSTRUCTOR); }
     bool is_recognizer(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_RECOGNISER); }
     bool is_accessor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_ACCESSOR); }
+    bool is_update_field(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_UPDATE_FIELD); }
     bool is_constructor(app * f) const { return is_app_of(f, m_family_id, OP_DT_CONSTRUCTOR); }
     bool is_recognizer(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER); }
     bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); }
+    bool is_update_field(app * f) const { return is_app_of(f, m_family_id, OP_DT_UPDATE_FIELD); }
     ptr_vector<func_decl> const * get_datatype_constructors(sort * ty);
     unsigned get_datatype_num_constructors(sort * ty) { 
         SASSERT(is_datatype(ty));

src/ast/dl_decl_plugin.cpp

@@ -44,7 +44,8 @@ namespace datalog {
         m_num_sym("N"),
         m_lt_sym("<"),
         m_le_sym("<="),
-        m_rule_sym("R")
+        m_rule_sym("R"),
+        m_min_sym("min")
     {
     }
 
@@ -490,6 +491,66 @@ namespace datalog {
         return m_manager->mk_func_decl(m_clone_sym, 1, &s, s, info);
     }
 
+    /**
+      In SMT2 syntax, we can write \c ((_ min R N) v_0 v_1 ... v_k)) where 0 <= N <= k,
+      R is a relation of sort V_0 x V_1 x ... x V_k and each v_i is a zero-arity function
+      (also known as a "constant" in SMT2 parlance) whose range is of sort V_i.
+
+      Example:
+
+        (define-sort number_t () (_ BitVec 2))
+        (declare-rel numbers (number_t number_t))
+        (declare-rel is_min (number_t number_t))
+
+        (declare-var x number_t)
+        (declare-var y number_t)
+
+        (rule (numbers #b00 #b11))
+        (rule (numbers #b00 #b01))
+
+        (rule (=> (and (numbers x y) ((_ min numbers 1) x y)) (is_min x y)))
+
+      This says that we want to find the mininum y grouped by x.
+    */
+    func_decl * dl_decl_plugin::mk_min(decl_kind k, unsigned num_parameters, parameter const * parameters) {
+        if (num_parameters < 2) {
+            m_manager->raise_exception("invalid min aggregate definition due to missing parameters");
+            return 0;
+        }
+
+        parameter const & relation_parameter = parameters[0];
+        if (!relation_parameter.is_ast() || !is_func_decl(relation_parameter.get_ast())) {
+            m_manager->raise_exception("invalid min aggregate definition, first parameter is not a function declaration");
+            return 0;
+        }
+
+        func_decl* f = to_func_decl(relation_parameter.get_ast());
+        if (!m_manager->is_bool(f->get_range())) {
+            m_manager->raise_exception("invalid min aggregate definition, first paramater must be a predicate");
+            return 0;
+        }
+
+        parameter const & min_col_parameter = parameters[1];
+        if (!min_col_parameter.is_int()) {
+            m_manager->raise_exception("invalid min aggregate definition, second parameter must be an integer");
+            return 0;
+        }
+
+        if (min_col_parameter.get_int() < 0) {
+            m_manager->raise_exception("invalid min aggregate definition, second parameter must be non-negative");
+            return 0;
+        }
+
+        if ((unsigned)min_col_parameter.get_int() >= f->get_arity()) {
+            m_manager->raise_exception("invalid min aggregate definition, second parameter exceeds the arity of the relation");
+            return 0;
+        }
+
+        func_decl_info info(m_family_id, k, num_parameters, parameters);
+        SASSERT(f->get_info() == 0);
+        return m_manager->mk_func_decl(m_min_sym, f->get_arity(), f->get_domain(), f->get_range(), info);
+    }
+
     func_decl * dl_decl_plugin::mk_func_decl(
         decl_kind k, unsigned num_parameters, parameter const * parameters, 
         unsigned arity, sort * const * domain, sort * range) {
@@ -617,6 +678,9 @@ namespace datalog {
                 break;
             }
 
+            case OP_DL_MIN:
+                return mk_min(k, num_parameters, parameters);
+
             default:
                 m_manager->raise_exception("operator not recognized");
                 return 0;
@@ -627,7 +691,7 @@ namespace datalog {
     }
 
     void dl_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
-
+        op_names.push_back(builtin_name(m_min_sym.bare_str(), OP_DL_MIN));
     }
 
     void dl_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {

src/ast/dl_decl_plugin.h

@@ -50,6 +50,7 @@ namespace datalog {
         OP_DL_LT,
         OP_DL_REP,
         OP_DL_ABS,
+        OP_DL_MIN,
         LAST_RA_OP
     };
     
@@ -71,6 +72,7 @@ namespace datalog {
         symbol m_lt_sym;
         symbol m_le_sym;
         symbol m_rule_sym;
+        symbol m_min_sym;
 
         bool check_bounds(char const* msg, unsigned low, unsigned up, unsigned val) const;
         bool check_domain(unsigned low, unsigned up, unsigned val) const;
@@ -94,12 +96,69 @@ namespace datalog {
         func_decl * mk_compare(decl_kind k, symbol const& sym, sort*const* domain);
         func_decl * mk_clone(sort* r);
         func_decl * mk_rule(unsigned arity);
+        func_decl * mk_min(decl_kind k, unsigned num_parameters, parameter const * parameters);
                                 
         sort * mk_finite_sort(unsigned num_params, parameter const* params);
         sort * mk_relation_sort(unsigned num_params, parameter const* params);
         sort * mk_rule_sort();
 
     public:
+        /**
+        Is \c decl a min aggregation function?
+        */
+        static bool is_aggregate(const func_decl* const decl)
+        {
+            return decl->get_decl_kind() == OP_DL_MIN;
+        }
+
+        /**
+        \pre: is_aggregate(aggregate)
+
+        \returns function declaration of predicate which is subject to min aggregation function
+        */
+        static func_decl * min_func_decl(const func_decl* const aggregate)
+        {
+            SASSERT(is_aggregate(aggregate));
+            parameter const & relation_parameter = aggregate->get_parameter(0);
+            return to_func_decl(relation_parameter.get_ast());
+        }
+
+        /**
+        \pre: is_aggregate(aggregate)
+
+        \returns column identifier (starting at zero) which is minimized by aggregation function
+        */
+        static unsigned min_col(const func_decl* const aggregate)
+        {
+            SASSERT(is_aggregate(aggregate));
+            return (unsigned)aggregate->get_parameter(1).get_int();
+        }
+
+        /**
+        \pre: is_aggregate(aggregate)
+
+        \returns column identifiers for the "group by" in the given min aggregation function
+        */
+        static unsigned_vector group_by_cols(const func_decl* const aggregate)
+        {
+            SASSERT(is_aggregate(aggregate));
+            unsigned _min_col = min_col(aggregate);
+            if (aggregate->get_arity() == 0U)
+                return unsigned_vector();
+
+            unsigned col_num = 0;
+            unsigned_vector cols(aggregate->get_arity() - 1U);
+            for (unsigned i = 0; i < cols.size(); ++i, ++col_num)
+            {
+                if (col_num == _min_col)
+                    ++col_num;
+
+                cols[i] = col_num;
+            }
+
+            return cols;
+        }
+
         dl_decl_plugin();
         virtual ~dl_decl_plugin() {}
 

src/ast/expr2polynomial.cpp

@@ -367,16 +367,16 @@ struct expr2polynomial::imp {
             begin_loop:
                 checkpoint();
                 frame & fr = m_frame_stack.back();
-                app * t = fr.m_curr;
-                TRACE("expr2polynomial", tout << "processing: " << fr.m_idx << "\n" << mk_ismt2_pp(t, m()) << "\n";);
-                unsigned num_args = t->get_num_args();
+                app * a = fr.m_curr;
+                TRACE("expr2polynomial", tout << "processing: " << fr.m_idx << "\n" << mk_ismt2_pp(a, m()) << "\n";);
+                unsigned num_args = a->get_num_args();
                 while (fr.m_idx < num_args) {
-                    expr * arg = t->get_arg(fr.m_idx);
+                    expr * arg = a->get_arg(fr.m_idx);
                     fr.m_idx++;
                     if (!visit(arg)) 
                         goto begin_loop;
                 }
-                process_app(t);
+                process_app(a);
                 m_frame_stack.pop_back();
             }
         }

src/ast/expr_map.h

@@ -44,6 +44,10 @@ public:
     void erase(expr * k);
     void reset();
     void flush();
+    void set_store_proofs(bool f) { 
+        if (m_store_proofs != f) flush();
+        m_store_proofs = f; 
+    }
 };
 
 #endif

src/ast/fpa/fpa2bv_converter.h

@@ -80,6 +80,7 @@ public:
 
     void mk_eq(expr * a, expr * b, expr_ref & result);
     void mk_ite(expr * c, expr * t, expr * f, expr_ref & result);
+    void mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
 
     void mk_rounding_mode(func_decl * f, expr_ref & result);
     void mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
@@ -92,7 +93,7 @@ public:
     void mk_ninf(func_decl * f, expr_ref & result);
     void mk_nan(func_decl * f, expr_ref & result);
     void mk_nzero(func_decl *f, expr_ref & result);
-    void mk_pzero(func_decl *f, expr_ref & result);
+    void mk_pzero(func_decl *f, expr_ref & result);    
 
     void mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
@@ -151,6 +152,8 @@ public:
     expr_ref_vector m_extra_assertions;
 
 protected:
+    void mk_one(func_decl *f, expr_ref sign, expr_ref & result);
+
     void mk_is_nan(expr * e, expr_ref & result);
     void mk_is_inf(expr * e, expr_ref & result);
     void mk_is_pinf(expr * e, expr_ref & result);

src/ast/fpa/fpa2bv_rewriter.h

@@ -103,8 +103,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
             }
             return BR_FAILED;
         }
-
-        if (m().is_ite(f)) {
+        else if (m().is_ite(f)) {
             SASSERT(num == 3);
             if (m_conv.is_float(args[1])) {
                 m_conv.mk_ite(args[0], args[1], args[2], result);
@@ -112,6 +111,14 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
             }
             return BR_FAILED;
         }
+        else if (m().is_distinct(f)) {
+            sort * ds = f->get_domain()[0];
+            if (m_conv.is_float(ds) || m_conv.is_rm(ds)) {
+                m_conv.mk_distinct(f, num, args, result);
+                return BR_DONE;
+            }
+            return BR_FAILED;
+        }
         
         if (m_conv.is_float_family(f)) {
             switch (f->get_decl_kind()) {            

src/ast/fpa_decl_plugin.cpp

@@ -289,7 +289,7 @@ func_decl * fpa_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_param
 
 func_decl * fpa_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                                unsigned arity, sort * const * domain, sort * range) {
-    if (arity != 2)
+    if (arity < 2)
         m_manager->raise_exception("invalid number of arguments to floating point relation");
     if (domain[0] != domain[1] || !is_float_sort(domain[0]))
         m_manager->raise_exception("sort mismatch, expected equal FloatingPoint sorts as arguments");
@@ -306,7 +306,7 @@ func_decl * fpa_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_parameter
     }
     func_decl_info finfo(m_family_id, k);
     finfo.set_chainable(true);
-    return m_manager->mk_func_decl(name, arity, domain, m_manager->mk_bool_sort(), finfo);
+    return m_manager->mk_func_decl(name, domain[0], domain[1], m_manager->mk_bool_sort(), finfo);
 }
 
 func_decl * fpa_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
@@ -879,12 +879,20 @@ void fpa_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
 }
 
 expr * fpa_decl_plugin::get_some_value(sort * s) {
-    SASSERT(s->is_sort_of(m_family_id, FLOATING_POINT_SORT));    
-    mpf tmp;
-    m_fm.mk_nan(s->get_parameter(0).get_int(), s->get_parameter(1).get_int(), tmp);
-    expr * res = this->mk_numeral(tmp);
-    m_fm.del(tmp);
-    return res;
+    if (s->is_sort_of(m_family_id, FLOATING_POINT_SORT)) {
+        mpf tmp;
+        m_fm.mk_nan(s->get_parameter(0).get_int(), s->get_parameter(1).get_int(), tmp);
+        expr * res = mk_numeral(tmp);
+        m_fm.del(tmp);
+        return res;
+    }
+    else if (s->is_sort_of(m_family_id, ROUNDING_MODE_SORT)) {
+        func_decl * f = mk_rm_const_decl(OP_FPA_RM_TOWARD_ZERO, 0, 0, 0, 0, s);
+        return m_manager->mk_const(f);
+    }
+    
+    UNREACHABLE();
+    return 0;
 }
 
 bool fpa_decl_plugin::is_value(app * e) const {

src/ast/func_decl_dependencies.cpp

@@ -145,24 +145,24 @@ class func_decl_dependencies::top_sort {
             return false;
         m_todo.push_back(f);
         while (!m_todo.empty()) {
-            func_decl * f = m_todo.back();
+            func_decl * cf = m_todo.back();
             
-            switch (get_color(f)) {
+            switch (get_color(cf)) {
             case CLOSED:                
                 m_todo.pop_back();
                 break;
             case OPEN:
-                set_color(f, IN_PROGRESS);
-                if (visit_children(f)) {
-                    SASSERT(m_todo.back() == f);
+                set_color(cf, IN_PROGRESS);
+                if (visit_children(cf)) {
+                    SASSERT(m_todo.back() == cf);
                     m_todo.pop_back();
-                    set_color(f, CLOSED);
+                    set_color(cf, CLOSED);
                 }
                 break;
             case IN_PROGRESS: 
-                if (all_children_closed(f)) {
-                    SASSERT(m_todo.back() == f);
-                    set_color(f, CLOSED);
+                if (all_children_closed(cf)) {
+                    SASSERT(m_todo.back() == cf);
+                    set_color(cf, CLOSED);
                 } else {
                     m_todo.reset();
                     return true;

src/ast/macros/macro_manager.cpp

@@ -255,9 +255,9 @@ bool macro_manager::macro_expander::get_subst(expr * _n, expr_ref & r, proof_ref
     app * n = to_app(_n);
     quantifier * q = 0;
     func_decl * d  = n->get_decl(); 
-    TRACE("macro_manager_bug", tout << "trying to expand:\n" << mk_pp(n, m_manager) << "\nd:\n" << d->get_name() << "\n";);
+    TRACE("macro_manager_bug", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";);
     if (m_macro_manager.m_decl2macro.find(d, q)) {
-        TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m_manager) << "\n";);
+        TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n";);
         app * head = 0;
         expr * def = 0;
         m_macro_manager.get_head_def(q, d, head, def);
@@ -272,17 +272,17 @@ bool macro_manager::macro_expander::get_subst(expr * _n, expr_ref & r, proof_ref
             SASSERT(subst_args[nidx] == 0);
             subst_args[nidx] = n->get_arg(i);
         }
-        var_subst s(m_manager);
+        var_subst s(m);
         s(def, num, subst_args.c_ptr(), r);
-        if (m_manager.proofs_enabled()) {
-            expr_ref instance(m_manager);
+        if (m.proofs_enabled()) {
+            expr_ref instance(m);
             s(q->get_expr(), num, subst_args.c_ptr(), instance);
-            proof * qi_pr = m_manager.mk_quant_inst(m_manager.mk_or(m_manager.mk_not(q), instance), num, subst_args.c_ptr());
+            proof * qi_pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), instance), num, subst_args.c_ptr());
             proof * q_pr  = 0;
             m_macro_manager.m_decl2macro_pr.find(d, q_pr);
             SASSERT(q_pr != 0);
             proof * prs[2] = { qi_pr, q_pr };
-            p = m_manager.mk_unit_resolution(2, prs);
+            p = m.mk_unit_resolution(2, prs);
         }
         else {
             p = 0;

src/ast/macros/macro_util.cpp

@@ -489,7 +489,6 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const {
                   tout << "#" << i << " -> " << mk_pp(var_mapping[i], m_manager) << "\n";
               });
         subst(t, var_mapping.size(), var_mapping.c_ptr(), norm_t);
-        SASSERT(is_well_sorted(m_manager, norm_t));
     }
     else {
         norm_t = t;

src/ast/normal_forms/nnf.cpp

@@ -137,7 +137,6 @@ class skolemizer {
             }
         }
         s(body, substitution.size(), substitution.c_ptr(), r);
-        SASSERT(is_well_sorted(m(), r));
         p = 0;
         if (m().proofs_enabled()) {
             if (q->is_forall()) 

src/ast/pattern/pattern_inference.cpp

@@ -116,7 +116,7 @@ void pattern_inference::collect::operator()(expr * n, unsigned num_bindings) {
         n              = e.m_node;
         unsigned delta = e.m_delta;
         TRACE("collect", tout << "processing: " << n->get_id() << " " << delta << " kind: " << n->get_kind() << "\n";);
-        TRACE("collect_info", tout << mk_pp(n, m_manager) << "\n";);
+        TRACE("collect_info", tout << mk_pp(n, m) << "\n";);
         if (visit_children(n, delta)) {
             m_todo.pop_back();
             save_candidate(n, delta);
@@ -170,9 +170,9 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
                 free_vars.insert(idx);
             info * i = 0;
             if (delta == 0)
-                i = alloc(info, m_manager, n, free_vars, 1);
+                i = alloc(info, m, n, free_vars, 1);
             else
-                i = alloc(info, m_manager, m_manager.mk_var(idx, to_var(n)->get_sort()), free_vars, 1);
+                i = alloc(info, m, m.mk_var(idx, to_var(n)->get_sort()), free_vars, 1);
             save(n, delta, i);
         }
         else {
@@ -189,7 +189,7 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
         }
         
         if (c->get_num_args() == 0) {
-            save(n, delta, alloc(info, m_manager, n, uint_set(), 1));
+            save(n, delta, alloc(info, m, n, uint_set(), 1));
             return;
         }
 
@@ -219,10 +219,10 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
             
         app * new_node = 0;
         if (changed)
-            new_node = m_manager.mk_app(decl, buffer.size(), buffer.c_ptr());
+            new_node = m.mk_app(decl, buffer.size(), buffer.c_ptr());
         else
             new_node = to_app(n);
-        save(n, delta, alloc(info, m_manager, new_node, free_vars, size));
+        save(n, delta, alloc(info, m, new_node, free_vars, size));
         // Remark: arithmetic patterns are only used if they are nested inside other terms.
         // That is, we never consider x + 1 as pattern. On the other hand, f(x+1) can be a pattern
         // if arithmetic is not in the forbidden list.
@@ -235,7 +235,7 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
         decl_kind k   = c->get_decl_kind();
         if (!free_vars.empty() && 
             (fid != m_afid || (fid == m_afid && !m_owner.m_nested_arith_only && (k == OP_DIV || k == OP_IDIV || k == OP_MOD || k == OP_REM || k == OP_MUL)))) {
-            TRACE("pattern_inference", tout << "potential candidate: \n" << mk_pp(new_node, m_manager) << "\n";);
+            TRACE("pattern_inference", tout << "potential candidate: \n" << mk_pp(new_node, m) << "\n";);
             m_owner.add_candidate(new_node, free_vars, size);
         }
         return;
@@ -338,7 +338,7 @@ bool pattern_inference::contains_subpattern::operator()(expr * n) {
                     uint_set const & s2 = e->get_data().m_value.m_free_vars;
                     SASSERT(s2.subset_of(s1));
                     if (s1 == s2) {
-                        TRACE("pattern_inference", tout << mk_pp(n, m_owner.m_manager) << "\nis bigger than\n" << mk_pp(to_app(curr), m_owner.m_manager) << "\n";);
+                        TRACE("pattern_inference", tout << mk_pp(n, m_owner.m) << "\nis bigger than\n" << mk_pp(to_app(curr), m_owner.m) << "\n";);
                         return true;
                     }
                 }
@@ -411,7 +411,7 @@ void pattern_inference::candidates2unary_patterns(ptr_vector<app> const & candid
         expr2info::obj_map_entry * e = m_candidates_info.find_core(candidate);
         info const & i = e->get_data().m_value;
         if (i.m_free_vars.num_elems() == m_num_bindings) {
-            app * new_pattern = m_manager.mk_pattern(candidate);
+            app * new_pattern = m.mk_pattern(candidate);
             result.push_back(new_pattern);
         }
         else {
@@ -435,7 +435,7 @@ void pattern_inference::candidates2multi_patterns(unsigned max_num_patterns,
     for (unsigned j = 0; j < m_pre_patterns.size(); j++) {
         pre_pattern * curr = m_pre_patterns[j];
         if (curr->m_free_vars.num_elems() == m_num_bindings) {
-            app * new_pattern = m_manager.mk_pattern(curr->m_exprs.size(), curr->m_exprs.c_ptr());
+            app * new_pattern = m.mk_pattern(curr->m_exprs.size(), curr->m_exprs.c_ptr());
             result.push_back(new_pattern);
             if (result.size() >= max_num_patterns)
                 return;
@@ -489,7 +489,7 @@ bool pattern_inference::is_forbidden(app * n) const {
     // occur outside of the quantifier. That is, Z3 will never match this kind of 
     // pattern.
     if (m_params.m_pi_avoid_skolems && decl->is_skolem()) {
-        CTRACE("pattern_inference_skolem", decl->is_skolem(), tout << "ignoring: " << mk_pp(n, m_manager) << "\n";);
+        CTRACE("pattern_inference_skolem", decl->is_skolem(), tout << "ignoring: " << mk_pp(n, m) << "\n";);
         return true;
     }
     if (is_forbidden(decl))
@@ -509,8 +509,8 @@ bool pattern_inference::has_preferred_patterns(ptr_vector<app> & candidate_patte
             expr2info::obj_map_entry * e = m_candidates_info.find_core(candidate);
             info const & i = e->get_data().m_value;
             if (i.m_free_vars.num_elems() == m_num_bindings) {
-                TRACE("pattern_inference", tout << "found preferred pattern:\n" << mk_pp(candidate, m_manager) << "\n";);
-                app * p = m_manager.mk_pattern(candidate);
+                TRACE("pattern_inference", tout << "found preferred pattern:\n" << mk_pp(candidate, m) << "\n";);
+                app * p = m.mk_pattern(candidate);
                 result.push_back(p);
                 found = true;
             }
@@ -531,11 +531,11 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
     m_collect(n, num_bindings);
 
     TRACE("pattern_inference", 
-          tout << mk_pp(n, m_manager);
+          tout << mk_pp(n, m);
           tout << "\ncandidates:\n";
           unsigned num = m_candidates.size();
           for (unsigned i = 0; i < num; i++) {
-              tout << mk_pp(m_candidates.get(i), m_manager) << "\n";
+              tout << mk_pp(m_candidates.get(i), m) << "\n";
           });
 
     if (!m_candidates.empty()) {
@@ -543,7 +543,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
         filter_looping_patterns(m_tmp1);
         TRACE("pattern_inference",
               tout << "candidates after removing looping-patterns:\n";
-              dump_app_vector(tout, m_tmp1, m_manager););
+              dump_app_vector(tout, m_tmp1, m););
         SASSERT(!m_tmp1.empty());
         if (!has_preferred_patterns(m_tmp1, result)) {
             // continue if there are no preferred patterns
@@ -552,7 +552,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
             SASSERT(!m_tmp2.empty());
             TRACE("pattern_inference",
                   tout << "candidates after removing bigger patterns:\n";
-                  dump_app_vector(tout, m_tmp2, m_manager););
+                  dump_app_vector(tout, m_tmp2, m););
             m_tmp1.reset();
             candidates2unary_patterns(m_tmp2, m_tmp1, result);
             unsigned num_extra_multi_patterns = m_params.m_pi_max_multi_patterns;
@@ -563,7 +563,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
                 std::stable_sort(m_tmp1.begin(), m_tmp1.end(), m_pattern_weight_lt);
                 TRACE("pattern_inference",
                       tout << "candidates after sorting:\n";
-                      dump_app_vector(tout, m_tmp1, m_manager););
+                      dump_app_vector(tout, m_tmp1, m););
                 candidates2multi_patterns(num_extra_multi_patterns, m_tmp1, result);
             }
         }
@@ -577,7 +577,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
 #include"database.h" // defines g_pattern_database
 
 void pattern_inference::reduce1_quantifier(quantifier * q) {
-    TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m_manager) << "\n";);
+    TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m) << "\n";);
     if (!q->is_forall()) {
         simplifier::reduce1_quantifier(q);
         return;
@@ -587,27 +587,27 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
 
     if (m_params.m_pi_use_database) {
         m_database.initialize(g_pattern_database);
-        app_ref_vector new_patterns(m_manager);
+        app_ref_vector new_patterns(m);
         unsigned new_weight;
         if (m_database.match_quantifier(q, new_patterns, new_weight)) {
 #ifdef Z3DEBUG
-            for (unsigned i = 0; i < new_patterns.size(); i++) { SASSERT(is_well_sorted(m_manager, new_patterns.get(i))); }
+            for (unsigned i = 0; i < new_patterns.size(); i++) { SASSERT(is_well_sorted(m, new_patterns.get(i))); }
 #endif
-            quantifier_ref new_q(m_manager);
+            quantifier_ref new_q(m);
             if (q->get_num_patterns() > 0) {
                 // just update the weight...
-                TRACE("pattern_inference", tout << "updating weight to: " << new_weight << "\n" << mk_pp(q, m_manager) << "\n";);
-                new_q = m_manager.update_quantifier_weight(q, new_weight);
+                TRACE("pattern_inference", tout << "updating weight to: " << new_weight << "\n" << mk_pp(q, m) << "\n";);
+                new_q = m.update_quantifier_weight(q, new_weight);
             }
             else {
-                quantifier_ref tmp(m_manager);
-                tmp   = m_manager.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), q->get_expr());
-                new_q = m_manager.update_quantifier_weight(tmp, new_weight); 
-                TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(new_q, m_manager) << "\n";);
+                quantifier_ref tmp(m);
+                tmp   = m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), q->get_expr());
+                new_q = m.update_quantifier_weight(tmp, new_weight); 
+                TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(new_q, m) << "\n";);
             }
             proof * pr = 0;
-            if (m_manager.fine_grain_proofs())
-                pr = m_manager.mk_rewrite(q, new_q);
+            if (m.fine_grain_proofs())
+                pr = m.mk_rewrite(q, new_q);
             cache_result(q, new_q, pr);
             return;
         }
@@ -635,7 +635,7 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
         new_no_patterns.push_back(new_pattern);
     } 
     
-    app_ref_buffer new_patterns(m_manager);
+    app_ref_buffer new_patterns(m);
     
     if (m_params.m_pi_arith == AP_CONSERVATIVE)
         m_forbidden.push_back(m_afid);
@@ -677,26 +677,26 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
                     warning_msg("using non nested arith. pattern (quantifier id: %s), the weight was increased to %d (this value can be modified using PI_NON_NESTED_ARITH_WEIGHT=<val>).", 
                                 q->get_qid().str().c_str(), weight);         
                 }
-                // verbose_stream() << mk_pp(q, m_manager) << "\n";
+                // verbose_stream() << mk_pp(q, m) << "\n";
             }
         }
     }
 
-    quantifier_ref new_q(m_manager);
-    new_q = m_manager.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_body);
+    quantifier_ref new_q(m);
+    new_q = m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_body);
     if (weight != q->get_weight())
-        new_q = m_manager.update_quantifier_weight(new_q, weight);
-    proof_ref pr(m_manager);
-    if (m_manager.fine_grain_proofs()) {  
+        new_q = m.update_quantifier_weight(new_q, weight);
+    proof_ref pr(m);
+    if (m.fine_grain_proofs()) {  
         if (new_body_pr == 0)
-            new_body_pr = m_manager.mk_reflexivity(new_body);
-        pr = m_manager.mk_quant_intro(q, new_q, new_body_pr);
+            new_body_pr = m.mk_reflexivity(new_body);
+        pr = m.mk_quant_intro(q, new_q, new_body_pr);
     }
     
     if (new_patterns.empty() && m_params.m_pi_pull_quantifiers) {
-        pull_quant pull(m_manager);
-        expr_ref   new_expr(m_manager);
-        proof_ref  new_pr(m_manager);
+        pull_quant pull(m);
+        expr_ref   new_expr(m);
+        proof_ref  new_pr(m);
         pull(new_q, new_expr, new_pr);
         quantifier * new_new_q = to_quantifier(new_expr);
         if (new_new_q != new_q) {
@@ -705,12 +705,12 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
                 if (m_params.m_pi_warnings) {
                     warning_msg("pulled nested quantifier to be able to find an useable pattern (quantifier id: %s)", q->get_qid().str().c_str());
                 }
-                new_q = m_manager.update_quantifier(new_new_q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_new_q->get_expr());
-                if (m_manager.fine_grain_proofs()) {
-                    pr = m_manager.mk_transitivity(pr, new_pr);
-                    pr = m_manager.mk_transitivity(pr, m_manager.mk_quant_intro(new_new_q, new_q, m_manager.mk_reflexivity(new_q->get_expr())));
+                new_q = m.update_quantifier(new_new_q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_new_q->get_expr());
+                if (m.fine_grain_proofs()) {
+                    pr = m.mk_transitivity(pr, new_pr);
+                    pr = m.mk_transitivity(pr, m.mk_quant_intro(new_new_q, new_q, m.mk_reflexivity(new_q->get_expr())));
                 }
-                TRACE("pattern_inference", tout << "pulled quantifier:\n" << mk_pp(new_q, m_manager) << "\n";);
+                TRACE("pattern_inference", tout << "pulled quantifier:\n" << mk_pp(new_q, m) << "\n";);
             }
         }
     }
@@ -719,7 +719,7 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
         if (m_params.m_pi_warnings) {
             warning_msg("failed to find a pattern for quantifier (quantifier id: %s)", q->get_qid().str().c_str());
         }
-        TRACE("pi_failed", tout << mk_pp(q, m_manager) << "\n";);
+        TRACE("pi_failed", tout << mk_pp(q, m) << "\n";);
     }
 
     if (new_patterns.empty() && new_body == q->get_expr()) {

src/ast/pattern/pattern_inference.h

@@ -38,7 +38,7 @@ Revision History:
    every instance of f(g(X)) is also an instance of f(X).
 */
 class smaller_pattern {
-    ast_manager &    m_manager;
+    ast_manager &    m;
     ptr_vector<expr> m_bindings;
 
     typedef std::pair<expr *, expr *> expr_pair;
@@ -54,7 +54,7 @@ class smaller_pattern {
 public:
 
     smaller_pattern(ast_manager & m):
-        m_manager(m) {
+        m(m) {
     }
 
     bool operator()(unsigned num_bindings, expr * p1, expr * p2);
@@ -135,7 +135,7 @@ class pattern_inference : public simplifier {
                 m_node(n, m), m_free_vars(vars), m_size(sz) {}
         };
         
-        ast_manager &            m_manager;
+        ast_manager &            m;
         pattern_inference &      m_owner;
         family_id                m_afid;
         unsigned                 m_num_bindings;
@@ -150,7 +150,7 @@ class pattern_inference : public simplifier {
         void save_candidate(expr * n, unsigned delta);
         void reset();
     public:
-        collect(ast_manager & m, pattern_inference & o):m_manager(m), m_owner(o), m_afid(m.mk_family_id("arith")) {}
+        collect(ast_manager & m, pattern_inference & o):m(m), m_owner(o), m_afid(m.mk_family_id("arith")) {}
         void operator()(expr * n, unsigned num_bindings);
     };
 

src/ast/pb_decl_plugin.cpp

@@ -0,0 +1,282 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    pb_decl_plugin.cpp
+
+Abstract:
+
+    Cardinality Constraints plugin
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-05-11
+
+Revision History:
+
+--*/
+
+#include "pb_decl_plugin.h"
+
+pb_decl_plugin::pb_decl_plugin():
+    m_at_most_sym("at-most"),
+    m_at_least_sym("at-least"),
+    m_pble_sym("pble"),
+    m_pbge_sym("pbge"),
+    m_pbeq_sym("pbeq")
+{}
+
+func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
+                                         unsigned arity, sort * const * domain, sort * range) {
+    SASSERT(m_manager);
+    ast_manager& m = *m_manager;
+    for (unsigned i = 0; i < arity; ++i) {
+        if (!m.is_bool(domain[i])) {
+            m.raise_exception("invalid non-Boolean sort applied to 'at-most'");
+        }
+    }
+    symbol sym;
+    switch(k) {
+    case OP_AT_LEAST_K: sym = m_at_least_sym; break;
+    case OP_AT_MOST_K: sym = m_at_most_sym; break;
+    case OP_PB_LE: sym = m_pble_sym; break;
+    case OP_PB_GE: sym = m_pbge_sym; break;
+    case OP_PB_EQ: sym = m_pbeq_sym; break;
+    default: break;
+    }
+    switch(k) {
+    case OP_AT_LEAST_K:
+    case OP_AT_MOST_K: {
+        if (num_parameters != 1 || !parameters[0].is_int() || parameters[0].get_int() < 0) {
+            m.raise_exception("function expects one non-negative integer parameter");
+        }
+        func_decl_info info(m_family_id, k, 1, parameters);
+        return m.mk_func_decl(sym, arity, domain, m.mk_bool_sort(), info);
+    }
+    case OP_PB_GE:
+    case OP_PB_LE: 
+    case OP_PB_EQ: {
+        if (num_parameters != 1 + arity) {
+            m.raise_exception("function expects arity+1 rational parameters");
+        }
+        vector<parameter> params;
+        for (unsigned i = 0; i < num_parameters; ++i) {
+            parameter const& p = parameters[i];
+            if (p.is_int()) {
+                params.push_back(p);
+            }
+            else if (p.is_rational()) {
+                // HACK: ast pretty printer does not work with rationals.
+                rational r = p.get_rational();
+                if (r.is_int32()) {
+                    params.push_back(parameter(r.get_int32()));
+                }
+                else {
+                    params.push_back(p);
+                }
+            }
+            else {
+                m.raise_exception("functions 'pble/pbge/pbeq' expect arity+1 integer parameters");
+            }
+        }
+        func_decl_info info(m_family_id, k, num_parameters, params.c_ptr());
+        return m.mk_func_decl(sym, arity, domain, m.mk_bool_sort(), info);
+    }
+    default:
+        UNREACHABLE();
+        return 0;
+    }
+}
+
+void pb_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
+    if (logic == symbol::null) {
+        op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K));
+        op_names.push_back(builtin_name(m_at_least_sym.bare_str(), OP_AT_LEAST_K));
+        op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE));
+        op_names.push_back(builtin_name(m_pbge_sym.bare_str(), OP_PB_GE));
+        op_names.push_back(builtin_name(m_pbeq_sym.bare_str(), OP_PB_EQ));
+    }
+}
+
+app * pb_util::mk_le(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k) {
+    vector<parameter> params;
+    params.push_back(parameter(k));
+    for (unsigned i = 0; i < num_args; ++i) {
+        params.push_back(parameter(coeffs[i]));
+    }
+    return m.mk_app(m_fid, OP_PB_LE, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
+}
+
+app * pb_util::mk_ge(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k) {
+    vector<parameter> params;
+    params.push_back(parameter(k));
+    for (unsigned i = 0; i < num_args; ++i) {
+        params.push_back(parameter(coeffs[i]));
+    }
+    return m.mk_app(m_fid, OP_PB_GE, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
+}
+
+app * pb_util::mk_eq(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k) {
+    vector<parameter> params;
+    params.push_back(parameter(k));
+    for (unsigned i = 0; i < num_args; ++i) {
+        params.push_back(parameter(coeffs[i]));
+    }
+    return m.mk_app(m_fid, OP_PB_EQ, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
+}
+
+// ax + by < k
+// <=>
+// -ax - by >= -k + 1
+// <=>
+// a(1-x) + b(1-y) >= -k + a + b + 1
+app * pb_util::mk_lt(unsigned num_args, rational const * _coeffs, expr * const * _args, rational const& _k) {
+    vector<rational> coeffs;
+    rational k(_k);
+    expr_ref_vector args(m);
+    expr* f;
+    rational d(denominator(k));
+    for (unsigned i = 0; i < num_args; ++i) {
+        coeffs.push_back(_coeffs[i]);
+        d = lcm(d, denominator(coeffs[i]));
+        if (m.is_not(_args[i], f)) {
+            args.push_back(f);
+        }
+        else {
+            args.push_back(m.mk_not(_args[i]));
+        }
+    }
+    if (!d.is_one()) {
+        k *= d;
+        for (unsigned i = 0; i < num_args; ++i) {
+            coeffs[i] *= d;        
+        }
+    }
+    k.neg();
+    k += rational::one();
+    for (unsigned i = 0; i < num_args; ++i) {
+        k += coeffs[i];
+    }
+    return mk_ge(num_args, coeffs.c_ptr(), args.c_ptr(), k);
+}
+
+
+app * pb_util::mk_at_most_k(unsigned num_args, expr * const * args, unsigned k) {
+    parameter param(k);
+    return m.mk_app(m_fid, OP_AT_MOST_K, 1, &param, num_args, args, m.mk_bool_sort());
+}
+
+bool pb_util::is_at_most_k(func_decl *a) const {
+    return is_decl_of(a, m_fid, OP_AT_MOST_K);
+}
+
+bool pb_util::is_at_most_k(expr *a, rational& k) const {
+    if (is_at_most_k(a)) {
+        k = get_k(a);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
+app * pb_util::mk_at_least_k(unsigned num_args, expr * const * args, unsigned k) {
+    parameter param(k);
+    return m.mk_app(m_fid, OP_AT_LEAST_K, 1, &param, num_args, args, m.mk_bool_sort());
+}
+
+bool pb_util::is_at_least_k(func_decl *a) const {
+    return is_decl_of(a, m_fid, OP_AT_LEAST_K);
+}
+
+bool pb_util::is_at_least_k(expr *a, rational& k) const {
+    if (is_at_least_k(a)) {
+        k = get_k(a);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
+rational pb_util::get_k(func_decl *a) const {
+    parameter const& p = a->get_parameter(0);
+    if (is_at_most_k(a) || is_at_least_k(a)) {
+        return to_rational(p);
+    }
+    else {
+        SASSERT(is_le(a) || is_ge(a) || is_eq(a));
+        return to_rational(p);
+    }
+}
+
+
+bool pb_util::is_le(func_decl *a) const {
+    return is_decl_of(a, m_fid, OP_PB_LE);
+}
+
+bool pb_util::is_le(expr* a, rational& k) const {
+    if (is_le(a)) {
+        k = get_k(a);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
+bool pb_util::is_ge(func_decl *a) const {
+    return is_decl_of(a, m_fid, OP_PB_GE);
+}
+
+bool pb_util::is_ge(expr* a, rational& k) const {
+    if (is_ge(a)) {
+        k = get_k(a);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
+
+bool pb_util::is_eq(func_decl *a) const {
+    return is_decl_of(a, m_fid, OP_PB_EQ);
+}
+
+bool pb_util::is_eq(expr* a, rational& k) const {
+    if (is_eq(a)) {
+        k = get_k(a);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
+rational pb_util::get_coeff(func_decl* a, unsigned index) const {
+    if (is_at_most_k(a) || is_at_least_k(a)) {
+        return rational::one();
+    }
+    SASSERT(is_le(a) || is_ge(a) || is_eq(a));
+    SASSERT(1 + index < a->get_num_parameters());
+    return to_rational(a->get_parameter(index + 1));
+}
+
+rational pb_util::to_rational(parameter const& p) const {
+    if (p.is_int()) {
+        return rational(p.get_int());
+    }
+    SASSERT(p.is_rational());
+    return p.get_rational();
+}
+
+bool pb_util::has_unit_coefficients(func_decl* f) const {
+    if (is_at_most_k(f) || is_at_least_k(f)) return true;
+    unsigned sz = f->get_arity();
+    for (unsigned i = 0; i < sz; ++i) {
+        if (!get_coeff(f, i).is_one()) return false;
+    }
+    return true;
+}

src/ast/pb_decl_plugin.h

@@ -0,0 +1,123 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    pb_decl_plugin.h
+
+Abstract:
+
+    Pseudo-Boolean and Cardinality Constraints plugin
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-05-11
+
+Notes:
+
+
+  (at-most-k x1 .... x_n) means x1 + ... + x_n <= k
+ 
+hence:
+
+  (not (at-most-k x1 .... x_n)) means x1 + ... + x_n >= k + 1
+
+
+--*/
+#ifndef _PB_DECL_PLUGIN_H_
+#define _PB_DECL_PLUGIN_H_
+
+#include"ast.h"
+ 
+enum pb_op_kind {
+    OP_AT_MOST_K,  // at most K Booleans are true.
+    OP_AT_LEAST_K, // at least K Booleans are true.
+    OP_PB_LE,      // pseudo-Boolean <= (generalizes at_most_k)
+    OP_PB_GE,      // pseudo-Boolean >= 
+    OP_PB_EQ,      // equality
+    LAST_PB_OP
+};
+
+
+class pb_decl_plugin : public decl_plugin {
+    symbol m_at_most_sym;
+    symbol m_at_least_sym;
+    symbol m_pble_sym;
+    symbol m_pbge_sym;
+    symbol m_pbeq_sym;
+    func_decl * mk_at_most(unsigned arity, unsigned k);
+    func_decl * mk_at_least(unsigned arity, unsigned k);
+    func_decl * mk_le(unsigned arity, rational const* coeffs, int k);
+    func_decl * mk_ge(unsigned arity, rational const* coeffs, int k);
+    func_decl * mk_eq(unsigned arity, rational const* coeffs, int k);
+public:
+    pb_decl_plugin();
+    virtual ~pb_decl_plugin() {}
+
+    virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
+        UNREACHABLE();
+        return 0;
+    }
+
+    virtual decl_plugin * mk_fresh() {
+        return alloc(pb_decl_plugin);
+    }
+    
+    //
+    // Contract for func_decl:
+    //   parameters[0] - integer (at most k elements)
+    //      all sorts are Booleans
+    //    parameters[1] .. parameters[arity] - coefficients
+    virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
+                                     unsigned arity, sort * const * domain, sort * range);
+    virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
+};
+
+
+class pb_util {
+    ast_manager & m;
+    family_id     m_fid;
+public:
+    pb_util(ast_manager& m):m(m), m_fid(m.mk_family_id("pb")) {}
+    ast_manager & get_manager() const { return m; }
+    family_id get_family_id() const { return m_fid; }
+    app * mk_at_most_k(unsigned num_args, expr * const * args, unsigned k);
+    app * mk_at_least_k(unsigned num_args, expr * const * args, unsigned k);
+    app * mk_le(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
+    app * mk_ge(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
+    app * mk_eq(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
+    app * mk_lt(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
+    bool is_at_most_k(func_decl *a) const;
+    bool is_at_most_k(expr *a) const { return is_app(a) && is_at_most_k(to_app(a)->get_decl()); }
+    bool is_at_most_k(expr *a, rational& k) const;
+    bool is_at_least_k(func_decl *a) const;
+    bool is_at_least_k(expr *a) const { return is_app(a) && is_at_least_k(to_app(a)->get_decl()); }
+    bool is_at_least_k(expr *a, rational& k) const;
+    rational get_k(func_decl *a) const;
+    rational get_k(expr *a) const { return get_k(to_app(a)->get_decl()); }
+    bool is_le(func_decl *a) const;
+    bool is_le(expr *a) const { return is_app(a) && is_le(to_app(a)->get_decl()); }
+    bool is_le(expr* a, rational& k) const;
+    bool is_ge(func_decl* a) const;
+    bool is_ge(expr* a) const { return is_app(a) && is_ge(to_app(a)->get_decl()); }
+    bool is_ge(expr* a, rational& k) const;
+    rational get_coeff(expr* a, unsigned index) const { return get_coeff(to_app(a)->get_decl(), index); }
+    rational get_coeff(func_decl* a, unsigned index) const; 
+    bool has_unit_coefficients(func_decl* f) const;
+    bool has_unit_coefficients(expr* f) const { return is_app(f) && has_unit_coefficients(to_app(f)->get_decl()); }
+
+
+    bool is_eq(func_decl* f) const;
+    bool is_eq(expr* e) const { return is_app(e) && is_eq(to_app(e)->get_decl()); }
+    bool is_eq(expr* e, rational& k) const;
+
+
+private:
+    rational to_rational(parameter const& p) const;
+};
+
+
+
+
+#endif /* _PB_DECL_PLUGIN_H_ */
+

src/ast/pp_params.pyg

@@ -10,7 +10,7 @@ def_module_params('pp',
                           ('decimal', BOOL, False, 'pretty print real numbers using decimal notation (the output may be truncated). Z3 adds a ? if the value is not precise'),
                           ('decimal_precision', UINT, 10, 'maximum number of decimal places to be used when pp.decimal=true'),
                           ('bv_literals', BOOL, True, 'use Bit-Vector literals (e.g, #x0F and #b0101) during pretty printing'),
-						  ('fp_real_literals', BOOL, False, 'use real-numbered floating point literals (e.g, +1.0p-1) during pretty printing'),
+                          ('fp_real_literals', BOOL, False, 'use real-numbered floating point literals (e.g, +1.0p-1) during pretty printing'),
                           ('bv_neg', BOOL, False, 'use bvneg when displaying Bit-Vector literals where the most significant bit is 1'),
                           ('flat_assoc', BOOL, True, 'flat associative operators (when pretty printing SMT2 terms/formulas)'),
                           ('fixed_indent', BOOL, False, 'use a fixed indentation for applications'),

src/ast/proof_checker/proof_checker.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "proof_checker.h"
 #include "ast_ll_pp.h"
 #include "ast_pp.h"

src/ast/reg_decl_plugins.cpp

@@ -24,6 +24,7 @@ Revision History:
 #include"datatype_decl_plugin.h"
 #include"dl_decl_plugin.h"
 #include"seq_decl_plugin.h"
+#include"pb_decl_plugin.h"
 #include"fpa_decl_plugin.h"
 
 void reg_decl_plugins(ast_manager & m) {
@@ -48,4 +49,7 @@ void reg_decl_plugins(ast_manager & m) {
     if (!m.get_plugin(m.mk_family_id(symbol("fpa")))) {
         m.register_plugin(symbol("fpa"), alloc(fpa_decl_plugin));
     }
+    if (!m.get_plugin(m.mk_family_id(symbol("pb")))) {
+        m.register_plugin(symbol("pb"), alloc(pb_decl_plugin));
+    }
 }

src/ast/rewriter/ast_counter.cpp

@@ -18,12 +18,9 @@ Revision History:
 --*/
 
 #include "ast_counter.h"
-#include "var_subst.h"
 
 void counter::update(unsigned el, int delta) {
     int & counter = get(el);
-    SASSERT(!m_stay_non_negative || counter>=0);
-    SASSERT(!m_stay_non_negative || static_cast<int>(counter)>=-delta);
     counter += delta;
 }
 
@@ -89,19 +86,17 @@ int counter::get_max_counter_value() const {
     return res;
 }
 
-void var_counter::count_vars(ast_manager & m, const app * pred, int coef) {
+void var_counter::count_vars(const app * pred, int coef) {
     unsigned n = pred->get_num_args();
     for (unsigned i = 0; i < n; i++) {
-        m_sorts.reset();
-        m_todo.reset();
-        m_mark.reset();
-        ::get_free_vars(m_mark, m_todo, pred->get_arg(i), m_sorts);
-        for (unsigned j = 0; j < m_sorts.size(); ++j) {
-            if (m_sorts[j]) {
+        m_fv(pred->get_arg(i));
+        for (unsigned j = 0; j < m_fv.size(); ++j) {
+            if (m_fv[j]) {
                 update(j, coef);
             }
         }
     }
+    m_fv.reset();
 }
 
 

src/ast/rewriter/ast_counter.h

@@ -27,16 +27,16 @@ Revision History:
 #include "ast.h"
 #include "map.h"
 #include "uint_set.h"
+#include "var_subst.h"
 
 class counter {
 protected:
     typedef u_map<int> map_impl;
     map_impl m_data;
-    const bool m_stay_non_negative;
 public:
     typedef map_impl::iterator iterator;
     
-    counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
+    counter() {}
     
     void reset() { m_data.reset(); }
     iterator begin() const { return m_data.begin(); }
@@ -69,15 +69,14 @@ public:
 
 class var_counter : public counter {
 protected:
-    ptr_vector<sort> m_sorts;
     expr_fast_mark1  m_visited;
+    expr_free_vars   m_fv;
     ptr_vector<expr> m_todo;
-    ast_mark         m_mark;
     unsigned_vector  m_scopes;
     unsigned get_max_var(bool & has_var);    
 public:
-    var_counter(bool stay_non_negative = true): counter(stay_non_negative) {}
-    void count_vars(ast_manager & m, const app * t, int coef = 1);
+    var_counter() {}
+    void count_vars(const app * t, int coef = 1);
     unsigned get_max_var(expr* e);
     unsigned get_next_var(expr* e);
 };
@@ -85,11 +84,10 @@ public:
 class ast_counter {
     typedef obj_map<ast, int> map_impl;
     map_impl m_data;
-    bool     m_stay_non_negative;
  public:
     typedef map_impl::iterator iterator;
     
-    ast_counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
+    ast_counter() {}
     
     iterator begin() const { return m_data.begin(); }
     iterator end() const { return m_data.end(); }
@@ -99,7 +97,6 @@ class ast_counter {
     }
     void update(ast * el, int delta){
         get(el) += delta;
-        SASSERT(!m_stay_non_negative || get(el) >= 0);
     }
     
     void inc(ast * el) { update(el, 1); }

src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h

@@ -464,18 +464,18 @@ void bit_blaster_tpl<Cfg>::mk_udiv_urem(unsigned sz, expr * const * a_bits, expr
         // update p
         if (i < sz - 1) {
             for (unsigned j = sz - 1; j > 0; j--) {
-                expr_ref i(m());
-                mk_ite(q, t.get(j-1), p.get(j-1), i); 
-                p.set(j, i);
+                expr_ref ie(m());
+                mk_ite(q, t.get(j-1), p.get(j-1), ie); 
+                p.set(j, ie);
             }
             p.set(0, a_bits[sz - i - 2]);
         }
         else {
             // last step: p contains the remainder
             for (unsigned j = 0; j < sz; j++) {
-                expr_ref i(m());
-                mk_ite(q, t.get(j), p.get(j), i);
-                p.set(j, i);
+                expr_ref ie(m());
+                mk_ite(q, t.get(j), p.get(j), ie);
+                p.set(j, ie);
             }
         }
     }
@@ -1041,6 +1041,11 @@ void bit_blaster_tpl<Cfg>::mk_ext_rotate_left_right(unsigned sz, expr * const *
             mk_rotate_right(sz, a_bits, static_cast<unsigned>(k.get_uint64()), out_bits);
     }
     else {
+        //
+        // Review: a better tuned implementation is possible by using shifts by power of two.
+        // e.g., looping over the bits of b_bits, then rotate by a power of two depending
+        // on the bit-position. This would get rid of the mk_urem.
+        //
         expr_ref_vector sz_bits(m());
         expr_ref_vector masked_b_bits(m());
         expr_ref_vector eqs(m());

src/ast/rewriter/datatype_rewriter.cpp

@@ -60,6 +60,32 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr
         UNREACHABLE();
         break;
     }
+    case OP_DT_UPDATE_FIELD: {
+        SASSERT(num_args == 2);
+        if (!is_app(args[0]) || !m_util.is_constructor(to_app(args[0])))
+            return BR_FAILED;
+        app * a = to_app(args[0]);
+        func_decl * c_decl = a->get_decl();
+        if (c_decl != m_util.get_accessor_constructor(f)) {
+            result = a;
+            return BR_DONE;
+        }
+        ptr_vector<func_decl> const * acc = m_util.get_constructor_accessors(c_decl);
+        SASSERT(acc && acc->size() == a->get_num_args());
+        unsigned num = acc->size();
+        ptr_buffer<expr> new_args;
+        for (unsigned i = 0; i < num; ++i) {
+            
+            if (f == (*acc)[i]) {
+                new_args.push_back(args[1]);
+            }
+            else {
+                new_args.push_back(a->get_arg(i));
+            }
+        }
+        result = m().mk_app(c_decl, num, new_args.c_ptr());
+        return BR_DONE;        
+    }
     default:
         UNREACHABLE();
     }

src/ast/rewriter/expr_safe_replace.cpp

@@ -29,43 +29,45 @@ void expr_safe_replace::insert(expr* src, expr* dst) {
 }
 
 void expr_safe_replace::operator()(expr* e, expr_ref& res) {
-    obj_map<expr,expr*> cache;
-    ptr_vector<expr> todo, args;
-    expr_ref_vector refs(m);
-    todo.push_back(e);
+    m_todo.push_back(e);
     expr* a, *b, *d;
-    todo.push_back(e);
     
-    while (!todo.empty()) {
-        a = todo.back();
-        if (cache.contains(a)) {
-            todo.pop_back();
+    while (!m_todo.empty()) {
+        a = m_todo.back();
+        if (m_cache.contains(a)) {
+            m_todo.pop_back();
         }
         else if (m_subst.find(a, b)) {
-            cache.insert(a, b);
-            todo.pop_back();
+            m_cache.insert(a, b);
+            m_todo.pop_back();
         }
         else if (is_var(a)) {
-            cache.insert(a, a);
-            todo.pop_back();
+            m_cache.insert(a, a);
+            m_todo.pop_back();
         }
         else if (is_app(a)) {
             app* c = to_app(a);
             unsigned n = c->get_num_args();
-            args.reset();
+            m_args.reset();
+            bool arg_differs = false;
             for (unsigned i = 0; i < n; ++i) {
-                if (cache.find(c->get_arg(i), d)) {
-                    args.push_back(d);
+                if (m_cache.find(c->get_arg(i), d)) {
+                    m_args.push_back(d);
+                    arg_differs |= c->get_arg(i) != d;
                 }
                 else {
-                    todo.push_back(c->get_arg(i));
+                    m_todo.push_back(c->get_arg(i));
                 }
             }
-            if (args.size() == n) {
-                b = m.mk_app(c->get_decl(), args.size(), args.c_ptr());
-                refs.push_back(b);
-                cache.insert(a, b);
-                todo.pop_back();
+            if (m_args.size() == n) {
+                if (arg_differs) {
+                    b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr());
+                    m_refs.push_back(b);
+                } else {
+                    b = a;
+                }
+                m_cache.insert(a, b);
+                m_todo.pop_back();
             }
         }
         else {
@@ -93,12 +95,16 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
             }
             replace(q->get_expr(), new_body);
             b = m.update_quantifier(q, pats.size(), pats.c_ptr(), nopats.size(), nopats.c_ptr(), new_body);
-            refs.push_back(b);
-            cache.insert(a, b);
-            todo.pop_back();
+            m_refs.push_back(b);
+            m_cache.insert(a, b);
+            m_todo.pop_back();
         }        
     }
-    res = cache.find(e);
+    res = m_cache.find(e);
+    m_cache.reset();
+    m_todo.reset();
+    m_args.reset();
+    m_refs.reset();    
 }
 
 void expr_safe_replace::reset() {

src/ast/rewriter/expr_safe_replace.h

@@ -29,9 +29,12 @@ class expr_safe_replace {
     expr_ref_vector m_src;
     expr_ref_vector m_dst;
     obj_map<expr, expr*> m_subst;
+    obj_map<expr,expr*> m_cache;
+    ptr_vector<expr> m_todo, m_args;
+    expr_ref_vector m_refs;
 
 public:
-    expr_safe_replace(ast_manager& m): m(m), m_src(m), m_dst(m) {}
+    expr_safe_replace(ast_manager& m): m(m), m_src(m), m_dst(m), m_refs(m) {}
 
     void insert(expr* src, expr* dst);
 
@@ -42,6 +45,8 @@ public:
     void apply_substitution(expr* s, expr* def, expr_ref& t);
 
     void reset();
+
+    bool empty() const { return m_subst.empty(); }
 };
 
 #endif /* __EXPR_SAFE_REPLACE_H__ */

src/ast/rewriter/fpa_rewriter.cpp

@@ -70,7 +70,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_FPA_MAX:       SASSERT(num_args == 2); st = mk_max(args[0], args[1], result); break;
     case OP_FPA_FMA:       SASSERT(num_args == 4); st = mk_fma(args[0], args[1], args[2], args[3], result); break;
     case OP_FPA_SQRT:      SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break;
-    case OP_FPA_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round(args[0], args[1], result); break;
+    case OP_FPA_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round_to_integral(args[0], args[1], result); break;
 
     case OP_FPA_EQ:        SASSERT(num_args == 2); st = mk_float_eq(args[0], args[1], result); break; 
     case OP_FPA_LT:        SASSERT(num_args == 2); st = mk_lt(args[0], args[1], result); break;
@@ -143,9 +143,9 @@ br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result)
 
 br_status fpa_rewriter::mk_to_real_unspecified(expr_ref & result) {
     if (m_hi_fp_unspecified)
-        result = m_util.au().mk_numeral(0, false);
-    else
         // The "hardware interpretation" is 0.
+        result = m_util.au().mk_numeral(rational(0), false);
+    else
         result = m_util.mk_internal_to_real_unspecified();
 
     return BR_DONE;    
@@ -243,7 +243,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
                 !m_util.au().is_numeral(args[2], r2))
                 return BR_FAILED;
 
-            TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);            
+            TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);
             m_fm.set(v, ebits, sbits, rmv, r1.to_mpq(), r2.to_mpq().numerator());
             result = m_util.mk_value(v);
             return BR_DONE;
@@ -411,14 +411,24 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
         result = arg1;
         return BR_DONE;
     }
-    // expand as using ite's
-    result = m().mk_ite(m().mk_or(mk_eq_nan(arg1), m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2))),
+    if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) {
+        result = arg2;
+        return BR_DONE;
+    }
+
+    result = m().mk_ite(mk_eq_nan(arg1),
                         arg2,
-                        m().mk_ite(mk_eq_nan(arg2), 
-                                   arg1,
-                                   m().mk_ite(m_util.mk_lt(arg1, arg2),
-                                           arg1,
-                                           arg2)));
+                        m().mk_ite(mk_eq_nan(arg2),
+                        arg1,
+                        // min(-0.0, +0.0) = min(+0.0, -0.0) = +0.0
+                        m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2),
+                                              m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))),
+                        m_util.mk_pzero(m().get_sort(arg1)),
+                        m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
+                        arg2,
+                        m().mk_ite(m_util.mk_lt(arg1, arg2),
+                        arg1,
+                        arg2)))));
     return BR_REWRITE_FULL;
 }
 
@@ -431,14 +441,24 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
         result = arg1;
         return BR_DONE;
     }
-    // expand as using ite's
-    result = m().mk_ite(m().mk_or(mk_eq_nan(arg1), m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2))),
+    if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) {
+        result = arg2;
+        return BR_DONE;
+    }
+
+    result = m().mk_ite(mk_eq_nan(arg1),
                         arg2,
-                        m().mk_ite(mk_eq_nan(arg2), 
-                                   arg1,
-                                   m().mk_ite(m_util.mk_gt(arg1, arg2),
-                                              arg1,
-                                              arg2)));
+                        m().mk_ite(mk_eq_nan(arg2),
+                        arg1,                        
+                        // max(-0.0, +0.0) = max(+0.0, -0.0) = +0.0
+                        m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2), 
+                                              m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))),
+                        m_util.mk_pzero(m().get_sort(arg1)),
+                        m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
+                        arg2,
+                        m().mk_ite(m_util.mk_gt(arg1, arg2),
+                        arg1,
+                        arg2)))));
     return BR_REWRITE_FULL;
 }
 
@@ -472,7 +492,7 @@ br_status fpa_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
     return BR_FAILED;
 }
 
-br_status fpa_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) {
+br_status fpa_rewriter::mk_round_to_integral(expr * arg1, expr * arg2, expr_ref & result) {
     mpf_rounding_mode rm;
     if (m_util.is_rm_numeral(arg1, rm)) {
         scoped_mpf v2(m_fm);
@@ -571,6 +591,7 @@ br_status fpa_rewriter::mk_ge(expr * arg1, expr * arg2, expr_ref & result) {
 
 br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) {
     scoped_mpf v(m_fm);
+
     if (m_util.is_numeral(arg1, v)) {
         result = (m_fm.is_zero(v)) ? m().mk_true() : m().mk_false();
         return BR_DONE;
@@ -581,6 +602,7 @@ br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) {
 
 br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) {
     scoped_mpf v(m_fm);
+
     if (m_util.is_numeral(arg1, v)) {
         result = (m_fm.is_nzero(v)) ? m().mk_true() : m().mk_false();
         return BR_DONE;
@@ -591,6 +613,7 @@ br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) {
 
 br_status fpa_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) {
     scoped_mpf v(m_fm);
+
     if (m_util.is_numeral(arg1, v)) {
         result = (m_fm.is_pzero(v)) ? m().mk_true() : m().mk_false();
         return BR_DONE;

src/ast/rewriter/fpa_rewriter.h

@@ -57,7 +57,7 @@ public:
     br_status mk_max(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result);
     br_status mk_sqrt(expr * arg1, expr * arg2, expr_ref & result);
-    br_status mk_round(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_round_to_integral(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_float_eq(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_lt(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_gt(expr * arg1, expr * arg2, expr_ref & result);

src/ast/rewriter/pb_rewriter.cpp

@@ -0,0 +1,275 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    pb_rewriter.cpp
+
+Abstract:
+
+    Basic rewriting rules for PB constraints.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-14-12
+
+Notes:
+
+--*/
+
+#include "pb_rewriter.h"
+#include "pb_rewriter_def.h"
+#include "ast_pp.h"
+#include "ast_smt_pp.h"
+
+
+class pb_ast_rewriter_util {
+    ast_manager& m;
+    expr_ref_vector m_refs;
+public:
+
+    typedef std::pair<expr*, rational> arg_t;
+    typedef vector<arg_t> args_t;
+    typedef rational numeral;
+
+    pb_ast_rewriter_util(ast_manager& m): m(m), m_refs(m) {}
+
+    expr* negate(expr* e) {
+        if (m.is_true(e)) {
+            return m.mk_false();
+        }
+        if (m.is_false(e)) {
+            return m.mk_true();
+        }
+        if (m.is_not(e, e)) {
+            return e;
+        }
+        m_refs.push_back(m.mk_not(e));
+        return m_refs.back();
+    }
+
+    void display(std::ostream& out, expr* e) {
+        out << mk_pp(e, m);
+    }
+
+    bool is_negated(expr* e) const {
+        return m.is_not(e);
+    }
+
+    bool is_true(expr* e) const {
+        return m.is_true(e);
+    }
+
+    bool is_false(expr* e) const {
+        return m.is_false(e);
+    }
+
+    struct compare {
+        bool operator()(std::pair<expr*,rational> const& a,
+                        std::pair<expr*,rational> const& b) {
+            return a.first->get_id() < b.first->get_id();
+        }
+
+    };
+};
+
+expr_ref pb_rewriter::translate_pb2lia(obj_map<expr,expr*>& vars, expr* fml) {
+    pb_util util(m());
+    arith_util a(m());
+    expr_ref result(m()), tmp(m());
+    expr_ref_vector es(m());
+    expr*const* args = to_app(fml)->get_args();
+    unsigned sz = to_app(fml)->get_num_args();
+    for (unsigned i = 0; i < sz; ++i) {
+        expr* e = args[i];
+        if (m().is_not(e, e)) {
+            es.push_back(a.mk_sub(a.mk_numeral(rational(1),true),vars.find(e)));
+        }
+        else {
+            es.push_back(vars.find(e));
+        }
+    }
+
+    if (util.is_at_most_k(fml) || util.is_at_least_k(fml)) {
+        if (es.empty()) {
+            tmp = a.mk_numeral(rational(0), true);
+        }
+        else {
+            tmp = a.mk_add(es.size(), es.c_ptr());
+        }
+        if (util.is_at_most_k(fml)) {
+            result = a.mk_le(tmp, a.mk_numeral(util.get_k(fml), false));
+        }
+        else {
+            result = a.mk_ge(tmp, a.mk_numeral(util.get_k(fml), false));
+        }
+    }
+    else if (util.is_le(fml) || util.is_ge(fml) || util.is_eq(fml)) {
+        for (unsigned i = 0; i < sz; ++i) {
+            es[i] = a.mk_mul(a.mk_numeral(util.get_coeff(fml, i),false), es[i].get());
+        }
+        if (es.empty()) {
+            tmp = a.mk_numeral(rational(0), true);
+        }
+        else {
+            tmp = a.mk_add(es.size(), es.c_ptr());
+        }
+        if (util.is_le(fml)) {
+            result = a.mk_le(tmp, a.mk_numeral(util.get_k(fml), false));
+        }
+        else if (util.is_ge(fml)) {
+            result = a.mk_ge(tmp, a.mk_numeral(util.get_k(fml), false));
+        }
+        else {
+            result = m().mk_eq(tmp, a.mk_numeral(util.get_k(fml), false));
+        }
+    }
+    else {
+        result = fml;
+    }
+    return result;
+}
+
+expr_ref pb_rewriter::mk_validate_rewrite(app_ref& e1, app_ref& e2) {
+    ast_manager& m = e1.get_manager();
+    arith_util a(m);
+    symbol name;
+    obj_map<expr,expr*> vars;
+    expr_ref_vector trail(m), fmls(m);    
+    unsigned sz = to_app(e1)->get_num_args();
+    expr*const*args = to_app(e1)->get_args();
+    for (unsigned i = 0; i < sz; ++i) {
+        expr* e = args[i];
+        if (m.is_true(e)) {
+            if (!vars.contains(e)) {
+                trail.push_back(a.mk_numeral(rational(1), true));
+                vars.insert(e, trail.back());            
+            }
+            continue;
+        }
+        if (m.is_false(e)) {
+            if (!vars.contains(e)) {
+                trail.push_back(a.mk_numeral(rational(0), true));
+                vars.insert(e, trail.back());            
+            }
+            continue;
+        }
+
+        std::ostringstream strm;
+        strm << "x" << i;
+        name = symbol(strm.str().c_str());
+        trail.push_back(m.mk_const(name, a.mk_int()));
+        expr* x = trail.back();
+        m.is_not(e,e);
+        vars.insert(e, x);
+        fmls.push_back(a.mk_le(a.mk_numeral(rational(0), true), x));
+        fmls.push_back(a.mk_le(x, a.mk_numeral(rational(1), true)));
+    }
+    expr_ref tmp(m);
+    expr_ref fml1 = translate_pb2lia(vars, e1);
+    expr_ref fml2 = translate_pb2lia(vars, e2);    
+    tmp = m.mk_not(m.mk_eq(fml1, fml2));
+    fmls.push_back(tmp);
+    tmp = m.mk_and(fmls.size(), fmls.c_ptr());
+    return tmp;
+}
+
+static unsigned s_lemma = 0;
+
+void pb_rewriter::validate_rewrite(func_decl* f, unsigned sz, expr*const* args, expr_ref& fml) {
+    ast_manager& m = fml.get_manager();
+    app_ref tmp1(m), tmp2(m);
+    tmp1 = m.mk_app(f, sz, args);
+    tmp2 = to_app(fml);
+    expr_ref tmp = mk_validate_rewrite(tmp1, tmp2);
+    dump_pb_rewrite(tmp);
+}
+
+void pb_rewriter::dump_pb_rewrite(expr* fml) {
+    std::ostringstream strm;
+    strm << "pb_rewrite_" << (s_lemma++) << ".smt2";
+    std::ofstream out(strm.str().c_str());    
+    ast_smt_pp pp(m());
+    pp.display_smt2(out, fml);    
+    out.close();
+}
+
+br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    ast_manager& m = result.get_manager();
+    rational sum(0), maxsum(0);
+    for (unsigned i = 0; i < num_args; ++i) {
+        if (m.is_true(args[i])) {
+            sum += m_util.get_coeff(f, i);
+            maxsum += m_util.get_coeff(f, i);
+        }
+        else if (!m.is_false(args[i])) {
+            maxsum += m_util.get_coeff(f, i);            
+        }
+    }
+    rational k = m_util.get_k(f);
+
+    vector<std::pair<expr*,rational> > vec;
+    for (unsigned i = 0; i < num_args; ++i) {
+        vec.push_back(std::make_pair(args[i], m_util.get_coeff(f, i)));
+    }
+    
+    switch(f->get_decl_kind()) {
+    case OP_AT_MOST_K:
+    case OP_PB_LE:
+        for (unsigned i = 0; i < num_args; ++i) {
+            vec[i].second.neg();
+        }
+        k.neg();
+        break;
+    case OP_AT_LEAST_K:
+    case OP_PB_GE:
+    case OP_PB_EQ:
+        break;
+    default:
+        UNREACHABLE();
+        return BR_FAILED;
+    }    
+
+    bool is_eq = f->get_decl_kind() == OP_PB_EQ;
+    
+    pb_ast_rewriter_util pbu(m);
+    pb_rewriter_util<pb_ast_rewriter_util> util(pbu);
+
+    util.unique(vec, k, is_eq);
+    lbool is_sat = util.normalize(vec, k, is_eq);
+    util.prune(vec, k, is_eq);
+    switch (is_sat) {
+    case l_true:
+        result = m.mk_true();
+        break;
+    case l_false:
+        result = m.mk_false();
+        break;
+    default:
+        m_args.reset();
+        m_coeffs.reset();
+        for (unsigned i = 0; i < vec.size(); ++i) {
+            m_args.push_back(vec[i].first);
+            m_coeffs.push_back(vec[i].second);
+        }
+        if (is_eq) {
+            result = m_util.mk_eq(vec.size(), m_coeffs.c_ptr(), m_args.c_ptr(), k);
+        }
+        else {
+            result = m_util.mk_ge(vec.size(), m_coeffs.c_ptr(), m_args.c_ptr(), k);
+        }
+        break;
+    }
+    TRACE("pb",
+          expr_ref tmp(m);
+          tmp = m.mk_app(f, num_args, args);
+          tout << tmp << "\n";
+          tout << result << "\n";
+          );
+    TRACE("pb_validate",
+          validate_rewrite(f, num_args, args, result););
+          
+    return BR_DONE;
+}
+
+

src/ast/rewriter/pb_rewriter.h

@@ -0,0 +1,65 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    pb_rewriter.h
+
+Abstract:
+
+    Basic rewriting rules for PB constraints.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-14-12
+
+Notes:
+
+--*/
+#ifndef _PB_REWRITER_H_
+#define _PB_REWRITER_H_
+
+#include"pb_decl_plugin.h"
+#include"rewriter_types.h"
+#include"params.h"
+#include"lbool.h"
+
+
+template<typename PBU>
+class pb_rewriter_util {    
+    PBU& m_util;
+    void display(std::ostream& out, typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq);
+public:
+    pb_rewriter_util(PBU& u) : m_util(u) {}
+    void unique(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq);
+    lbool normalize(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq);
+    void prune(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq);
+};
+
+/**
+   \brief Cheap rewrite rules for PB constraints
+*/
+class pb_rewriter {
+    pb_util       m_util;
+    vector<rational> m_coeffs;
+    ptr_vector<expr> m_args;
+
+    void validate_rewrite(func_decl* f, unsigned sz, expr*const* args, expr_ref& fml);
+public:    
+    pb_rewriter(ast_manager & m, params_ref const & p = params_ref()):
+        m_util(m) {
+    }
+    ast_manager & m() const { return m_util.get_manager(); }
+    family_id get_fid() const { return m_util.get_family_id(); }
+
+    void updt_params(params_ref const & p) {}
+    static void get_param_descrs(param_descrs & r) {}
+
+    br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+
+    expr_ref translate_pb2lia(obj_map<expr,expr*>& vars, expr* fml);
+    expr_ref mk_validate_rewrite(app_ref& e1, app_ref& e2);
+    void dump_pb_rewrite(expr* fml);
+};
+
+#endif

src/ast/rewriter/pb_rewriter_def.h

@@ -0,0 +1,298 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    pb_rewriter_def.h
+
+Abstract:
+
+    Basic rewriting rules for PB constraints.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-14-12
+
+Notes:
+
+--*/
+#ifndef _PB_REWRITER_DEF_H_
+#define _PB_REWRITER_DEF_H_
+
+#include"pb_rewriter.h"
+
+
+template<typename PBU>
+void pb_rewriter_util<PBU>::display(std::ostream& out, typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
+    for (unsigned i = 0; i < args.size(); ++i) {
+        out << args[i].second << " * ";
+        m_util.display(out, args[i].first);
+        out << " ";
+        if (i+1 < args.size()) out << "+ ";
+    }
+    out << (is_eq?" = ":" >= ") << k << "\n";
+}
+
+template<typename PBU>
+void pb_rewriter_util<PBU>::unique(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
+    
+    TRACE("pb_verbose", display(tout << "pre-unique:", args, k, is_eq););
+    for (unsigned i = 0; i < args.size(); ++i) {
+        if (m_util.is_negated(args[i].first)) {
+            args[i].first = m_util.negate(args[i].first);
+            k -= args[i].second;
+            args[i].second = -args[i].second;
+        }
+    }
+    // remove constants
+    for (unsigned i = 0; i < args.size(); ++i) {
+        if (m_util.is_true(args[i].first)) {
+            k -= args[i].second;
+            std::swap(args[i], args[args.size()-1]);
+            args.pop_back();
+            --i;
+        }
+        else if (m_util.is_false(args[i].first)) {
+            std::swap(args[i], args[args.size()-1]);
+            args.pop_back();                
+            --i;
+        }
+    }
+    // sort and coalesce arguments:
+    typename PBU::compare cmp;
+    std::sort(args.begin(), args.end(), cmp);
+
+    // coallesce
+    unsigned i, j;
+    for (i = 0, j = 1; j < args.size(); ++j) {
+        if (args[i].first == args[j].first) {
+            args[i].second += args[j].second;
+        }
+        else {
+            ++i;
+            args[i] = args[j];
+        }
+    }
+    args.resize(i+1);
+
+    // remove 0s.
+    for (i = 0, j = 0; j < args.size(); ++j) {
+        if (!args[j].second.is_zero()) {
+            if (i != j) {
+                args[i] = args[j];
+            }
+            ++i;
+        }
+    }
+    args.resize(i);
+    TRACE("pb_verbose", display(tout << "post-unique:", args, k, is_eq););
+}
+
+template<typename PBU>
+lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
+    TRACE("pb_verbose", display(tout << "pre-normalize:", args, k, is_eq););
+
+    DEBUG_CODE(
+        bool found = false;
+        for (unsigned i = 0; !found && i < args.size(); ++i) {
+            found = args[i].second.is_zero();
+        }
+        if (found) display(verbose_stream(), args, k, is_eq);
+        SASSERT(!found););
+
+    // 
+    // Ensure all coefficients are positive:
+    //    c*l + y >= k 
+    // <=> 
+    //    c*(1-~l) + y >= k
+    // <=>
+    //    c - c*~l + y >= k
+    // <=> 
+    //    -c*~l + y >= k - c
+    // 
+    typename PBU::numeral sum(0);
+    for (unsigned i = 0; i < args.size(); ++i) {
+        typename PBU::numeral c = args[i].second;
+        if (c.is_neg()) {
+            args[i].second = -c;
+            args[i].first = m_util.negate(args[i].first);
+            k -= c;
+        }
+        sum += args[i].second;
+    }
+    // detect tautologies:
+    if (!is_eq && k <= PBU::numeral::zero()) {
+        args.reset();
+        k = PBU::numeral::zero();
+        return l_true;
+    }
+    if (is_eq && k.is_zero() && args.empty()) {
+        return l_true;
+    }
+
+    // detect infeasible constraints:
+    if (sum < k) {
+        args.reset();
+        k = PBU::numeral::one();
+        return l_false;
+    }
+
+    if (is_eq && k == sum) {
+        for (unsigned i = 0; i < args.size(); ++i) {
+            args[i].second = PBU::numeral::one();
+        }
+        typename PBU::numeral num(args.size()); 
+        k = num;
+        return l_undef;
+    }
+    
+    bool all_int = true;
+    for (unsigned i = 0; all_int && i < args.size(); ++i) {
+        all_int = args[i].second.is_int();
+    }
+    
+    if (!all_int) {
+        // normalize to integers.
+        typename PBU::numeral d(denominator(k));
+        for (unsigned i = 0; i < args.size(); ++i) {
+            d = lcm(d, denominator(args[i].second));
+        }
+        SASSERT(!d.is_one());
+        k *= d;
+        for (unsigned i = 0; i < args.size(); ++i) {
+            args[i].second *= d;
+        }            
+    }
+
+    if (is_eq) {
+        TRACE("pb_verbose", display(tout << "post-normalize:", args, k, is_eq););
+        return l_undef;
+    }
+    
+    // Ensure the largest coefficient is not larger than k:
+    sum = PBU::numeral::zero();
+    for (unsigned i = 0; i < args.size(); ++i) {
+        typename PBU::numeral c = args[i].second;
+        if (c > k) {
+            args[i].second = k;
+        }
+        sum += args[i].second;
+    }
+    SASSERT(!args.empty());
+    
+    // normalize tight inequalities to unit coefficients.
+    if (sum == k) {
+        for (unsigned i = 0; i < args.size(); ++i) {
+            args[i].second = PBU::numeral::one();
+        }
+        typename PBU::numeral num(args.size()); 
+        k = num;
+    }
+    
+    // apply cutting plane reduction:
+    typename PBU::numeral g(0);
+    for (unsigned i = 0; !g.is_one() && i < args.size(); ++i) {
+        typename PBU::numeral c = args[i].second;
+        if (c != k) {
+            if (g.is_zero()) {
+                g = c;
+            }
+            else {
+                g = gcd(g, c);
+            }
+        }
+    }
+    if (g.is_zero()) {
+        // all coefficients are equal to k.
+        for (unsigned i = 0; i < args.size(); ++i) {
+            SASSERT(args[i].second == k);
+            args[i].second = PBU::numeral::one();
+        }
+        k = PBU::numeral::one();
+    }
+    else if (g > PBU::numeral::one()) {
+        
+        //
+        // Example 5x + 5y + 2z + 2u >= 5
+        // becomes 3x + 3y + z + u >= 3
+        // 
+        typename PBU::numeral k_new = div(k, g);    
+        if (!(k % g).is_zero()) {     // k_new is the ceiling of k / g.
+            k_new++;
+        }
+        for (unsigned i = 0; i < args.size(); ++i) {
+            SASSERT(args[i].second.is_pos());
+            typename PBU::numeral c = args[i].second;
+            if (c == k) {
+                c = k_new;
+            }
+            else {
+                c = div(c, g);
+            }
+            args[i].second = c;
+            SASSERT(args[i].second.is_pos());
+        }
+        k = k_new;            
+    }
+    //
+    // normalize coefficients that fall within a range
+    // k/n <= ... < k/(n-1) for some n = 1,2,...
+    //
+    // e.g, k/n <= min <= max < k/(n-1)
+    //      k/min <= n, n-1 < k/max
+    // .    floor(k/max) = ceil(k/min) - 1  
+    // .    floor(k/max) < k/max
+    //
+    // example: k = 5, min = 3, max = 4: 5/3 -> 2   5/4 -> 1, n = 2
+    // replace all coefficients by 1, and k by 2.
+    //
+    if (!k.is_one()) {
+        typename PBU::numeral min = args[0].second, max = args[0].second;
+        for (unsigned i = 1; i < args.size(); ++i) {
+            if (args[i].second < min) min = args[i].second;
+            if (args[i].second > max) max = args[i].second;
+        }            
+        SASSERT(min.is_pos());
+        typename PBU::numeral n0 = k/max;
+        typename PBU::numeral n1 = floor(n0);
+        typename PBU::numeral n2 = ceil(k/min) - PBU::numeral::one();
+        if (n1 == n2 && !n0.is_int()) {
+            IF_VERBOSE(3, display(verbose_stream() << "set cardinality\n", args, k, is_eq););
+            
+            for (unsigned i = 0; i < args.size(); ++i) {
+                args[i].second = PBU::numeral::one();
+            }
+            k = n1 + PBU::numeral::one();
+        }
+    }
+    TRACE("pb_verbose", display(tout << "post-normalize:", args, k, is_eq););
+    return l_undef;
+}
+
+template<typename PBU>
+void pb_rewriter_util<PBU>::prune(typename PBU::args_t& args, typename PBU::numeral& k, bool is_eq) {
+    if (is_eq) {
+        return;
+    }
+    typename PBU::numeral nlt(0);
+    unsigned occ = 0;
+    for (unsigned i = 0; nlt < k && i < args.size(); ++i) {
+        if (args[i].second < k) {
+            nlt += args[i].second;
+            ++occ;
+        }
+    }
+    if (0 < occ && nlt < k) {        
+        for (unsigned i = 0; i < args.size(); ++i) {
+            if (args[i].second < k) {
+                args[i] = args.back();
+                args.pop_back();
+                --i;
+            }
+        }
+        unique(args, k, is_eq);
+        normalize(args, k, is_eq);
+    }    
+}
+
+#endif

src/ast/rewriter/poly_rewriter_def.h

@@ -31,6 +31,8 @@ void poly_rewriter<Config>::updt_params(params_ref const & _p) {
     m_hoist_mul = p.hoist_mul();
     m_hoist_cmul = p.hoist_cmul();
     m_som_blowup = p.som_blowup();
+    if (!m_flat) m_som = false;
+    if (m_som) m_hoist_mul = false;
 }
 
 template<typename Config>

src/ast/rewriter/rewriter_def.h

@@ -324,7 +324,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
                     }
                     result_stack().push_back(def);
                     TRACE("get_macro", tout << "bindings:\n";
-                          for (unsigned i = 0; i < m_bindings.size(); i++) tout << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";);
+                          for (unsigned j = 0; j < m_bindings.size(); j++) tout << j << ": " << mk_ismt2_pp(m_bindings[j], m()) << "\n";);
                     begin_scope();
                     m_num_qvars = 0;
                     m_root      = def;

src/ast/rewriter/th_rewriter.cpp

@@ -25,6 +25,7 @@ Notes:
 #include"array_rewriter.h"
 #include"fpa_rewriter.h"
 #include"dl_rewriter.h"
+#include"pb_rewriter.h"
 #include"rewriter_def.h"
 #include"expr_substitution.h"
 #include"ast_smt2_pp.h"
@@ -41,6 +42,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     datatype_rewriter   m_dt_rw;
     fpa_rewriter        m_f_rw;
     dl_rewriter         m_dl_rw;
+    pb_rewriter         m_pb_rw;
     arith_util          m_a_util;
     bv_util             m_bv_util;
     unsigned long long  m_max_memory; // in bytes
@@ -196,6 +198,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             return m_f_rw.mk_app_core(f, num, args, result);
         if (fid == m_dl_rw.get_fid())
             return m_dl_rw.mk_app_core(f, num, args, result);
+        if (fid == m_pb_rw.get_fid())
+            return m_pb_rw.mk_app_core(f, num, args, result);
         return BR_FAILED;
     }
 
@@ -645,6 +649,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_dt_rw(m),
         m_f_rw(m, p),
         m_dl_rw(m),
+        m_pb_rw(m),
         m_a_util(m),
         m_bv_util(m),
         m_used_dependencies(m),

src/ast/rewriter/var_subst.cpp

@@ -164,7 +164,7 @@ void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref
           tout << "\n----->\n" << mk_ismt2_pp(result, m) << "\n";);
 }
 
-static void get_free_vars_offset(ast_mark& mark, ptr_vector<expr>& todo, unsigned offset, expr* e, ptr_vector<sort>& sorts) {
+static void get_free_vars_offset(expr_sparse_mark& mark, ptr_vector<expr>& todo, unsigned offset, expr* e, ptr_vector<sort>& sorts) {
     todo.push_back(e);
     while (!todo.empty()) {
         e = todo.back();
@@ -176,7 +176,7 @@ static void get_free_vars_offset(ast_mark& mark, ptr_vector<expr>& todo, unsigne
         switch(e->get_kind()) {
         case AST_QUANTIFIER: {
             quantifier* q = to_quantifier(e);
-            ast_mark mark1;
+            expr_sparse_mark mark1;
             ptr_vector<expr> todo1;
             get_free_vars_offset(mark1, todo1, offset+q->get_num_decls(), q->get_expr(), sorts);
             break;
@@ -210,11 +210,33 @@ static void get_free_vars_offset(ast_mark& mark, ptr_vector<expr>& todo, unsigne
 
 
 void get_free_vars(expr* e, ptr_vector<sort>& sorts) {
-    ast_mark mark;
+    expr_sparse_mark mark;
     ptr_vector<expr> todo;
     get_free_vars_offset(mark, todo, 0, e, sorts);
 }
 
-void get_free_vars(ast_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts) {
+void get_free_vars(expr_sparse_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts) {
     get_free_vars_offset(mark, todo, 0, e, sorts);
 }
+
+void expr_free_vars::reset() {
+    m_mark.reset();
+    m_sorts.reset();
+    SASSERT(m_todo.empty());
+}
+
+void expr_free_vars::set_default_sort(sort *s) {
+    for (unsigned i = 0; i < m_sorts.size(); ++i) {
+        if (!m_sorts[i]) m_sorts[i] = s;
+    }
+}
+
+void expr_free_vars::operator()(expr* e) {
+    reset();
+    get_free_vars_offset(m_mark, m_todo, 0, e, m_sorts);
+}
+
+void expr_free_vars::accumulate(expr* e) {
+    SASSERT(m_todo.empty());
+    get_free_vars_offset(m_mark, m_todo, 0, e, m_sorts);
+}

src/ast/rewriter/var_subst.h

@@ -81,9 +81,23 @@ void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref
 
    Return the sorts of the free variables.
 */
-void get_free_vars(expr* e, ptr_vector<sort>& sorts);
 
-void get_free_vars(ast_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts);
+class expr_free_vars {
+    expr_sparse_mark m_mark;
+    ptr_vector<sort> m_sorts;
+    ptr_vector<expr> m_todo;
+public:    
+    void reset();
+    void operator()(expr* e);
+    void accumulate(expr* e);
+    bool empty() const { return m_sorts.empty(); }
+    unsigned size() const { return m_sorts.size(); }
+    sort* operator[](unsigned idx) const { return m_sorts[idx]; }
+    bool contains(unsigned idx) const { return idx < m_sorts.size() && m_sorts[idx] != 0; }
+    void set_default_sort(sort* s);
+    void reverse() { m_sorts.reverse(); }
+    sort*const* c_ptr() const { return m_sorts.c_ptr(); }  
+};
 
 #endif
 

src/ast/shared_occs.h

@@ -75,7 +75,7 @@ public:
     iterator end_shared() const { return m_shared.end(); }
     void reset();
     void cleanup();
-    void display(std::ostream & out, ast_manager & m) const;
+    void display(std::ostream & out, ast_manager & mgr) const;
 };
 
 #endif

src/ast/simplifier/array_simplifier_plugin.cpp

@@ -332,6 +332,7 @@ lbool array_simplifier_plugin::eq_default(expr* def, unsigned arity, unsigned nu
     for (unsigned i = 0; i < num_st; ++i) {
         all_eq  &= (st[i][arity] == def);
         all_diseq &= m_manager.is_unique_value(st[i][arity]) && (st[i][arity] != def);
+        TRACE("array_simplifier", tout << m_manager.is_unique_value(st[i][arity]) << " " << mk_pp(st[i][arity], m_manager) << "\n";);
     }
     if (all_eq) {
         return l_true;
@@ -350,6 +351,12 @@ bool array_simplifier_plugin::insert_table(expr* def, unsigned arity, unsigned n
                 return false;
             }
         }
+        TRACE("array_simplifier", tout << "inserting: ";
+              for (unsigned j = 0; j < arity; ++j) {
+                  tout << mk_pp(st[i][j], m_manager) << " ";              
+              }
+            tout << " |-> " << mk_pp(def, m_manager) << "\n";
+            );
         args_entry e(arity, st[i]);
         table.insert_if_not_there(e);
     }
@@ -424,7 +431,8 @@ bool array_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & resul
             lbool eq = eq_stores(c1, arity2, st1.size(), st1.c_ptr(), st2.size(), st2.c_ptr());
             TRACE("array_simplifier", 
                   tout << mk_pp(lhs, m_manager) << " = " 
-                  << mk_pp(rhs, m_manager) << " := " << eq << "\n";);
+                  << mk_pp(rhs, m_manager) << " := " << eq << "\n";
+                  tout << "arity: " << arity1 << "\n";);
             switch(eq) {
             case l_false: 
                 result = m_manager.mk_false(); 

src/ast/simplifier/base_simplifier.h

@@ -20,21 +20,32 @@ Notes:
 #define _BASE_SIMPLIFIER_H_
 
 #include"expr_map.h"
+#include"ast_pp.h"
 
 /**
    \brief Implements basic functionality used by expression simplifiers.
 */
 class base_simplifier {
 protected:
-    ast_manager &                  m_manager;
+    ast_manager &                  m;
     expr_map                       m_cache;
     ptr_vector<expr>               m_todo;
 
-    void cache_result(expr * n, expr * r, proof * p) { m_cache.insert(n, r, p); }
+    void cache_result(expr * n, expr * r, proof * p) { 
+        m_cache.insert(n, r, p); 
+        CTRACE("simplifier", !is_rewrite_proof(n, r, p),
+               tout << mk_pp(n, m) << "\n";
+               tout << mk_pp(r, m) << "\n";
+               tout << mk_pp(p, m) << "\n";);
+        SASSERT(is_rewrite_proof(n, r, p));
+    }
     void reset_cache() { m_cache.reset(); }
     void flush_cache() { m_cache.flush(); }
     void get_cached(expr * n, expr * & r, proof * & p) const { m_cache.get(n, r, p); }
 
+    void reinitialize() { m_cache.set_store_proofs(m.fine_grain_proofs()); }
+
+
     void visit(expr * n, bool & visited) {
         if (!is_cached(n)) {
             m_todo.push_back(n);
@@ -44,11 +55,22 @@ protected:
 
 public:
     base_simplifier(ast_manager & m):
-        m_manager(m),
+        m(m),
         m_cache(m, m.fine_grain_proofs()) {
     }
     bool is_cached(expr * n) const {  return m_cache.contains(n); }
-    ast_manager & get_manager() { return m_manager; }
+    ast_manager & get_manager() { return m; }
+
+    bool is_rewrite_proof(expr* n, expr* r, proof* p) {
+        if (p && 
+            !m.is_undef_proof(p) && 
+            !(m.has_fact(p) && 
+              (m.is_eq(m.get_fact(p)) || m.is_oeq(m.get_fact(p)) || m.is_iff(m.get_fact(p))) && 
+              to_app(m.get_fact(p))->get_arg(0) == n && 
+              to_app(m.get_fact(p))->get_arg(1) == r)) return false;
+        
+        return (!m.fine_grain_proofs() || p || (n == r));
+    }
 };
 
 #endif /* _BASE_SIMPLIFIER_H_ */

src/ast/simplifier/bv_elim.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "bv_elim.h"
 #include "bv_decl_plugin.h"
 #include "var_subst.h"
@@ -100,11 +106,11 @@ bool bv_elim_star::visit_quantifier(quantifier* q) {
 }
 
 void bv_elim_star::reduce1_quantifier(quantifier* q) {
-    quantifier_ref r(m_manager);
-    proof_ref pr(m_manager);
+    quantifier_ref r(m);
+    proof_ref pr(m);
     m_bv_elim.elim(q, r);
-    if (m_manager.fine_grain_proofs()) {
-        pr = m_manager.mk_rewrite(q, r.get());
+    if (m.fine_grain_proofs()) {
+        pr = m.mk_rewrite(q, r.get());
     }
     else {
         pr = 0;

src/ast/simplifier/datatype_simplifier_plugin.cpp

@@ -81,6 +81,8 @@ bool datatype_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr *
         }
         UNREACHABLE();
     }
+    case OP_DT_UPDATE_FIELD:
+        return false;
     default:
         UNREACHABLE();
     }

src/ast/simplifier/elim_bounds.cpp

@@ -203,20 +203,20 @@ void elim_bounds_star::reduce1_quantifier(quantifier * q) {
         cache_result(q, q, 0); 
         return;
     }
-    quantifier_ref new_q(m_manager);
+    quantifier_ref new_q(m);
     expr * new_body = 0;
     proof * new_pr;
     get_cached(q->get_expr(), new_body, new_pr);
-    new_q = m_manager.update_quantifier(q, new_body);
-    expr_ref r(m_manager);
+    new_q = m.update_quantifier(q, new_body);
+    expr_ref r(m);
     m_elim(new_q, r);
     if (q == r.get()) {
         cache_result(q, q, 0);
         return;
     }
-    proof_ref pr(m_manager);
-    if (m_manager.fine_grain_proofs())
-        pr = m_manager.mk_rewrite(q, r); // TODO: improve justification
+    proof_ref pr(m);
+    if (m.fine_grain_proofs())
+        pr = m.mk_rewrite(q, r); // TODO: improve justification
     cache_result(q, r, pr);
 }