prepare release notes

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

CMakeLists.txt

@@ -34,7 +34,7 @@ endif()
 ################################################################################
 set(Z3_VERSION_MAJOR 4)
 set(Z3_VERSION_MINOR 8)
-set(Z3_VERSION_PATCH 2)
+set(Z3_VERSION_PATCH 3)
 set(Z3_VERSION_TWEAK 0)
 set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
 set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified

RELEASE_NOTES

@@ -1,5 +1,19 @@
 RELEASE NOTES
 
+Version 4.8.3
+=============
+- New features
+  - native handling of recursive function definitions
+  - PB rounding based option for conflict resolution when reasoning about PB constraints.
+
+Version 4.8.2
+=============
+- Post-Release. 
+
+Version 4.8.1
+=============
+- Release. Bug-fix for 4.8.0
+
 Version 4.8.0
 =============
 

scripts/mk_project.py

@@ -9,7 +9,7 @@ from mk_util import *
 
 # Z3 Project definition
 def init_project_def():
-    set_version(4, 8, 2, 0)
+    set_version(4, 8, 3, 0)
     add_lib('util', [], includes2install = ['z3_version.h'])
     add_lib('polynomial', ['util'], 'math/polynomial')
     add_lib('sat', ['util'])

src/api/api_context.h

@@ -63,7 +63,7 @@ namespace api {
         datalog::dl_decl_util      m_datalog_util;
         fpa_util                   m_fpa_util;
         seq_util                   m_sutil;
-        recfun_util                m_recfun;
+        recfun::util               m_recfun;
 
         // Support for old solver API
         smt_params                 m_fparams;
@@ -130,7 +130,7 @@ namespace api {
         fpa_util & fpautil() { return m_fpa_util; }
         datatype_util& dtutil() { return m_dt_plugin->u(); }
         seq_util& sutil() { return m_sutil; }
-        recfun_util& recfun() { return m_recfun; }
+        recfun::util& recfun() { return m_recfun; }
         family_id get_basic_fid() const { return m_basic_fid; }
         family_id get_array_fid() const { return m_array_fid; }
         family_id get_arith_fid() const { return m_arith_fid; }

src/api/dotnet/Context.cs

@@ -532,6 +532,34 @@ namespace Microsoft.Z3
             return new FuncDecl(this, MkSymbol(name), domain, range);
         }
 
+        /// <summary>
+        /// Creates a new recursive function declaration.
+        /// </summary>
+        public FuncDecl MkRecFuncDecl(string name, Sort[] domain, Sort range)
+        {
+            Debug.Assert(range != null);
+            Debug.Assert(domain.All(d => d != null));
+
+            CheckContextMatch<Sort>(domain);
+            CheckContextMatch(range);
+            return new FuncDecl(this, MkSymbol(name), domain, range, true);
+        }
+
+        /// <summary>
+        /// Bind a definition to a recursive function declaration.
+	/// The function must have previously been created using
+	/// MkRecFuncDecl. The body may contain recursive uses of the function or
+	/// other mutually recursive functions. 
+        /// </summary>
+	public void AddRecDef(FuncDecl f, Expr[] args, Expr body) 
+	{
+	    CheckContextMatch(f);
+	    CheckContextMatch<Expr>(args);
+	    CheckContextMatch(body);
+            IntPtr[] argsNative = AST.ArrayToNative(args);
+	    Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
+	}	
+
         /// <summary>
         /// Creates a new function declaration.
         /// </summary>

src/api/dotnet/FuncDecl.cs

@@ -302,6 +302,15 @@ namespace Microsoft.Z3
             Debug.Assert(range != null);
         }
 
+        internal FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range, bool is_rec)
+            : base(ctx, Native.Z3_mk_rec_func_decl(ctx.nCtx, name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject))
+        {
+            Debug.Assert(ctx != null);
+            Debug.Assert(name != null);
+            Debug.Assert(range != null);
+        }
+
+
 #if DEBUG
         internal override void CheckNativeObject(IntPtr obj)
         {

src/ast/ast_pp_util.cpp

@@ -20,6 +20,7 @@ Revision History:
 #include "ast/ast_pp_util.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/ast_smt_pp.h"
+#include "ast/recfun_decl_plugin.h"
 
 void ast_pp_util::collect(expr* e) {
     coll.visit(e);
@@ -49,7 +50,14 @@ void ast_pp_util::display_decls(std::ostream& out) {
             ast_smt2_pp(out, f, m_env) << "\n";
         }
     }
-    SASSERT(coll.get_num_preds() == 0);
+    vector<std::pair<func_decl*, expr*>> recfuns;
+    recfun::util u(m);
+    func_decl_ref_vector funs = u.get_rec_funs();
+    if (funs.empty()) return;
+    for (func_decl * f : funs) {
+        recfuns.push_back(std::make_pair(f, u.get_def(f).get_rhs()));
+    }
+    ast_smt2_pp_recdefs(out, recfuns, m_env);
 }
 
 void ast_pp_util::remove_decl(func_decl* f) {

src/ast/ast_pp_util.h

@@ -31,7 +31,7 @@ class ast_pp_util {
 
     decl_collector      coll;
 
-    ast_pp_util(ast_manager& m): m(m), m_env(m), coll(m, false) {}
+    ast_pp_util(ast_manager& m): m(m), m_env(m), coll(m) {}
 
     void collect(expr* e);
 

src/ast/ast_smt2_pp.cpp

@@ -1163,6 +1163,33 @@ public:
         unregister_var_names(f->get_arity());
     }
 
+    // format set of mutually recursive definitions
+    void operator()(vector<std::pair<func_decl*, expr*>> const& funs, format_ref & r) {
+        format_ref_vector decls(m()), bodies(m());
+        format_ref r1(m()), r2(m());
+
+        for (auto const& p : funs) {
+            unsigned len;
+            func_decl* f = p.first;
+            expr* e = p.second;
+            format * fname = m_env.pp_fdecl_name(f, len);
+            register_var_names(f->get_arity());        
+            format * args[3];
+            args[0] = fname;
+            args[1] = pp_var_args(f->get_arity(), f->get_domain());
+            args[2] = m_env.pp_sort(f->get_range());
+            decls.push_back(mk_seq1<format**, f2f>(m(), args, args+3, f2f(), ""));                             
+            process(e, r);
+            bodies.push_back(r);
+            unregister_var_names(f->get_arity());
+        }
+        r1 = mk_seq1<format*const*, f2f>(m(), decls.begin(), decls.end(), f2f(), "");
+        r2 = mk_seq1<format*const*, f2f>(m(), bodies.begin(), bodies.end(), f2f(), "");
+        format * args[2];
+        args[0] = r1;
+        args[1] = r2;
+        r = mk_seq1<format**, f2f>(m(), args, args+2, f2f(), "define-rec-funs");
+    }
 
 
 };
@@ -1275,6 +1302,16 @@ std::ostream & ast_smt2_pp(std::ostream & out, symbol const& s, bool is_skolem,
     return out;
 }
 
+std::ostream & ast_smt2_pp_recdefs(std::ostream & out, vector<std::pair<func_decl*, expr*>> const& funs, smt2_pp_environment & env, params_ref const & p) {
+    ast_manager & m = env.get_manager();
+    format_ref r(fm(m));
+    smt2_printer pr(env, p);
+    pr(funs, r);
+    pp(out, r.get(), m, p);
+    return out;
+}
+
+
 mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent, unsigned num_vars, char const * var_prefix):
     m_ast(t),
     m_manager(m),

src/ast/ast_smt2_pp.h

@@ -105,6 +105,8 @@ std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & e
 std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "declare-fun");
 std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "define-fun");
 std::ostream & ast_smt2_pp(std::ostream & out, symbol const& s, bool is_skolem, smt2_pp_environment & env, params_ref const& p = params_ref());
+std::ostream & ast_smt2_pp_recdefs(std::ostream & out, vector<std::pair<func_decl*, expr*>> const& funs, smt2_pp_environment & env, params_ref const & p = params_ref());
+
 
 /**
    \brief Internal wrapper (for debugging purposes only)

src/ast/ast_smt_pp.cpp

@@ -980,14 +980,6 @@ 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, ql, rn, m_logic, true, true, m_simplify_implies, 0);
-            p(d);
-            strm << "\n";
-        }
-    }
 #endif
 
     for (expr* a : m_assumptions) {

src/ast/decl_collector.cpp

@@ -50,18 +50,14 @@ void decl_collector::visit_func(func_decl * n) {
     if (!m_visited.is_marked(n)) {
         family_id fid = n->get_family_id();
         if (fid == null_family_id) {
-            if (m_sep_preds && is_bool(n->get_range()))
+            m_decls.push_back(n);
-                m_preds.push_back(n);
-            else
-                m_decls.push_back(n);
         }
         m_visited.mark(n, true);
     }
 }
 
-decl_collector::decl_collector(ast_manager & m, bool preds):
+decl_collector::decl_collector(ast_manager & m):
     m_manager(m),
-    m_sep_preds(preds),
     m_dt_util(m) {
     m_basic_fid = m_manager.get_basic_family_id();
     m_dt_fid = m_dt_util.get_family_id();

src/ast/decl_collector.h

@@ -26,10 +26,8 @@ Revision History:
 
 class decl_collector {
     ast_manager &         m_manager;
-    bool                  m_sep_preds;
     ptr_vector<sort>      m_sorts;
     ptr_vector<func_decl> m_decls;
-    ptr_vector<func_decl> m_preds;
     ast_mark              m_visited;
     family_id             m_basic_fid;
     family_id             m_dt_fid;
@@ -46,8 +44,7 @@ class decl_collector {
 
 
 public:
-    // if preds == true, then predicates are stored in a separate collection.
+    decl_collector(ast_manager & m);
-    decl_collector(ast_manager & m, bool preds = true);
     ast_manager & m() { return m_manager; }
 
     void visit_func(func_decl* n);
@@ -59,11 +56,9 @@ public:
 
     unsigned get_num_sorts() const { return m_sorts.size(); }
     unsigned get_num_decls() const { return m_decls.size(); }
-    unsigned get_num_preds() const { return m_preds.size(); }
     
     sort * const * get_sorts() const { return m_sorts.c_ptr(); }
     func_decl * const * get_func_decls() const { return m_decls.c_ptr(); }
-    func_decl * const * get_pred_decls() const { return m_preds.c_ptr(); }
 };
 
 #endif

src/ast/recfun_decl_plugin.cpp

@@ -369,7 +369,7 @@ namespace recfun {
     }
 
     namespace decl {
-        plugin::plugin() : decl_plugin(), m_defs(), m_case_defs(), m_def_block() {}
+        plugin::plugin() : decl_plugin(), m_defs(), m_case_defs() {}
         plugin::~plugin() { finalize(); }
 
         void plugin::finalize() {

src/ast/recfun_decl_plugin.h

@@ -143,9 +143,8 @@ namespace recfun {
             typedef obj_map<func_decl, case_def*> case_def_map;
 
             mutable scoped_ptr<util> m_util;
-            def_map                 m_defs; // function->def
+            def_map                  m_defs;       // function->def
-            case_def_map            m_case_defs; // case_pred->def
+            case_def_map             m_case_defs;  // case_pred->def
-            svector<symbol>         m_def_block;
             
             ast_manager & m() { return *m_manager; }
         public:
@@ -206,8 +205,11 @@ namespace recfun {
 
         ast_manager & m() { return m_manager; }
         th_rewriter & get_th_rewriter() { return m_th_rw; }
+        decl::plugin& get_plugin() { return *m_plugin; }
+
         bool is_case_pred(expr * e) const { return is_app_of(e, m_fid, OP_FUN_CASE_PRED); }
         bool is_defined(expr * e) const { return is_app_of(e, m_fid, OP_FUN_DEFINED); }
+        bool is_defined(func_decl* f) const { return is_decl_of(f, m_fid, OP_FUN_DEFINED); }
         bool is_depth_limit(expr * e) const { return is_app_of(e, m_fid, OP_DEPTH_LIMIT); }
         bool owns_app(app * e) const { return e->get_family_id() == m_fid; }
 
@@ -242,11 +244,6 @@ namespace recfun {
 
         app_ref mk_depth_limit_pred(unsigned d);
 
-        decl::plugin& get_plugin() { return *m_plugin; }
     };
 }
 
-typedef recfun::def recfun_def;
-typedef recfun::case_def recfun_case_def;
-typedef recfun::decl::plugin recfun_decl_plugin;
-typedef recfun::util recfun_util;

src/ast/reg_decl_plugins.cpp

@@ -42,7 +42,7 @@ void reg_decl_plugins(ast_manager & m) {
         m.register_plugin(symbol("datatype"), alloc(datatype_decl_plugin));    
     }
     if (!m.get_plugin(m.mk_family_id(symbol("recfun")))) {
-        m.register_plugin(symbol("recfun"), alloc(recfun_decl_plugin));    
+        m.register_plugin(symbol("recfun"), alloc(recfun::decl::plugin));    
     }
     if (!m.get_plugin(m.mk_family_id(symbol("datalog_relation")))) {
         m.register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin));

src/cmd_context/cmd_context.cpp

@@ -693,7 +693,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         register_plugin(symbol("bv"),       alloc(bv_decl_plugin), logic_has_bv());
         register_plugin(symbol("array"),    alloc(array_decl_plugin), logic_has_array());
         register_plugin(symbol("datatype"), alloc(datatype_decl_plugin), logic_has_datatype());
-        register_plugin(symbol("recfun"),   alloc(recfun_decl_plugin), logic_has_recfun());
+        register_plugin(symbol("recfun"),   alloc(recfun::decl::plugin), logic_has_recfun());
         register_plugin(symbol("seq"),      alloc(seq_decl_plugin), logic_has_seq());
         register_plugin(symbol("pb"),       alloc(pb_decl_plugin), logic_has_pb());
         register_plugin(symbol("fpa"),      alloc(fpa_decl_plugin), logic_has_fpa());
@@ -899,7 +899,7 @@ void cmd_context::model_del(func_decl* f) {
 }
 
 
-recfun_decl_plugin& cmd_context::get_recfun_plugin() {
+recfun::decl::plugin& cmd_context::get_recfun_plugin() {
     recfun::util u(get_ast_manager());
     return u.get_plugin();
 }
@@ -944,7 +944,7 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
 
     TRACE("recfun", tout<< "define recfun " << f->get_name()  << " = " << mk_pp(rhs, m()) << "\n";);
 
-    recfun_decl_plugin& p = get_recfun_plugin();
+    recfun::decl::plugin& p = get_recfun_plugin();
 
     var_ref_vector vars(m());
     for (expr* b : binding) {
@@ -2040,7 +2040,7 @@ void cmd_context::display_smt2_benchmark(std::ostream & out, unsigned num, expr
     if (logic != symbol::null)
         out << "(set-logic " << logic << ")" << std::endl;
     // collect uninterpreted function declarations
-    decl_collector decls(m(), false);
+    decl_collector decls(m());
     for (unsigned i = 0; i < num; i++) {
         decls.visit(assertions[i]);
     }
@@ -2071,8 +2071,8 @@ void cmd_context::slow_progress_sample() {
     svector<symbol> labels;
     m_solver->get_labels(labels);
     regular_stream() << "(labels";
-    for (unsigned i = 0; i < labels.size(); i++) {
+    for (symbol const& s : labels) {
-        regular_stream() << " " << labels[i];
+        regular_stream() << " " << s;
     }
     regular_stream() << "))" << std::endl;
 }

src/cmd_context/cmd_context.h

@@ -307,7 +307,7 @@ protected:
     void erase_macro(symbol const& s);
     bool macros_find(symbol const& s, unsigned n, expr*const* args, expr*& t) const;
 
-    recfun_decl_plugin& get_recfun_plugin();
+    recfun::decl::plugin& get_recfun_plugin();
 
 public:
     cmd_context(bool main_ctx = true, ast_manager * m = nullptr, symbol const & l = symbol::null);

src/model/model_smt2_pp.cpp

@@ -21,6 +21,7 @@ Revision History:
 #include "model/model_smt2_pp.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/func_decl_dependencies.h"
+#include "ast/recfun_decl_plugin.h"
 #include "ast/pp.h"
 using namespace format_ns;
 
@@ -60,11 +61,9 @@ static void pp_uninterp_sorts(std::ostream & out, ast_printer_context & ctx, mod
         ctx.display(buffer, s, 13);
         buffer << ":\n";
         pp_indent(buffer, TAB_SZ);
-        ptr_vector<expr>::const_iterator it  = u.begin();
+        for (expr* e : u) {
-        ptr_vector<expr>::const_iterator end = u.end();
+            SASSERT(is_app(e));
-        for (; it != end; ++it) {
+            app * c = to_app(e);
-            SASSERT(is_app(*it));
-            app * c = to_app(*it);
             pp_symbol(buffer, c->get_decl()->get_name());
             buffer << " ";
         }
@@ -87,9 +86,8 @@ static void pp_uninterp_sorts(std::ostream & out, ast_printer_context & ctx, mod
         out << "\n";
         pp_indent(out, indent);
         out << ";; definitions for universe elements:\n";
-        it  = u.begin();
+        for (expr * e : u) {
-        for (; it != end; ++it) {
+            app * c = to_app(e);
-            app * c = to_app(*it);
             pp_indent(out, indent);
             out << "(declare-fun ";
             unsigned len  = pp_symbol(out, c->get_decl()->get_name());
@@ -101,9 +99,8 @@ static void pp_uninterp_sorts(std::ostream & out, ast_printer_context & ctx, mod
         out << ";; cardinality constraint:\n";
         f_conds.reset();
         format * var = mk_string(m, "x");
-        it  = u.begin();
+        for (expr* e : u) {
-        for (; it != end; ++it) {
+            app * c = to_app(e);
-            app * c = to_app(*it);
             symbol csym = c->get_decl()->get_name();
             std::string cname;
             if (is_smt2_quoted_symbol(csym))
@@ -170,10 +167,7 @@ void sort_fun_decls(ast_manager & m, model_core const & md, ptr_buffer<func_decl
                 func_decl_set deps;
                 bool all_visited = true;
                 collect_func_decls(m, curr_i->get_else(), deps);
-                func_decl_set::iterator it2  = deps.begin();
+                for (func_decl * d : deps) {
-                func_decl_set::iterator end2 = deps.end();
-                for (; it2 != end2; ++it2) {
-                    func_decl * d = *it2;
                     if (d->get_arity() > 0 && md.has_interpretation(d) && !visited.contains(d)) {
                         todo.push_back(d);
                         visited.insert(d);
@@ -189,8 +183,10 @@ void sort_fun_decls(ast_manager & m, model_core const & md, ptr_buffer<func_decl
     }
 }
 
+
 static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core const & md, unsigned indent) {
     ast_manager & m = ctx.get_ast_manager();
+    recfun::util recfun_util(m);
     sbuffer<symbol>    var_names;
     ptr_buffer<format> f_var_names;
     ptr_buffer<format> f_arg_decls;
@@ -200,6 +196,9 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co
     sort_fun_decls(m, md, func_decls);
     for (unsigned i = 0; i < func_decls.size(); i++) {
         func_decl * f     = func_decls[i]; 
+        if (recfun_util.is_defined(f)) {
+            continue;
+        }
         func_interp * f_i = md.get_func_interp(f);
         SASSERT(f->get_arity() == f_i->get_arity());
         format_ref body(fm(m));

src/smt/theory_recfun.cpp

@@ -31,7 +31,7 @@ namespace smt {
     theory_recfun::theory_recfun(ast_manager & m)
         : theory(m.mk_family_id("recfun")), 
           m(m),
-          m_plugin(*reinterpret_cast<recfun_decl_plugin*>(m.get_plugin(get_family_id()))),
+          m_plugin(*reinterpret_cast<recfun::decl::plugin*>(m.get_plugin(get_family_id()))),
           m_util(m_plugin.u()), 
           m_preds(m),
           m_max_depth(0),

src/smt/theory_recfun.h

@@ -36,9 +36,9 @@ namespace smt {
         // one case-expansion of `f(t1...tn)`
         struct case_expansion {
             app *              m_lhs; // the term to expand
-            recfun_def *        m_def;
+            recfun::def *       m_def;
             ptr_vector<expr>    m_args;
-            case_expansion(recfun_util& u, app * n) : 
+            case_expansion(recfun::util& u, app * n) : 
             m_lhs(n), m_def(nullptr), m_args()  {
                 SASSERT(u.is_defined(n));
                 func_decl * d = n->get_decl();
@@ -66,14 +66,14 @@ namespace smt {
         // one body-expansion of `f(t1...tn)` using a `C_f_i(t1...tn)`
         struct body_expansion {
             app*                    m_pred;
-            recfun_case_def const * m_cdef;
+            recfun::case_def const * m_cdef;
             ptr_vector<expr>        m_args;
 
-            body_expansion(recfun_util& u, app * n) : m_pred(n), m_cdef(0), m_args() {
+            body_expansion(recfun::util& u, app * n) : m_pred(n), m_cdef(0), m_args() {
                 m_cdef = &u.get_case_def(n);
                 m_args.append(n->get_num_args(), n->get_args());
             }
-            body_expansion(app* pred, recfun_case_def const & d, ptr_vector<expr> & args) : 
+            body_expansion(app* pred, recfun::case_def const & d, ptr_vector<expr> & args) : 
                 m_pred(pred), m_cdef(&d), m_args(args) {}
             body_expansion(body_expansion const & from): 
                 m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(from.m_args) {}
@@ -90,8 +90,8 @@ namespace smt {
         friend std::ostream& operator<<(std::ostream&, pp_body_expansion const &);
         
         ast_manager&            m;
-        recfun_decl_plugin&     m_plugin;
+        recfun::decl::plugin&   m_plugin;
-        recfun_util&            m_util;
+        recfun::util&           m_util;
         stats                   m_stats;
 
         // book-keeping for depth of predicates
@@ -104,7 +104,7 @@ namespace smt {
         ptr_vector<body_expansion> m_q_body_expand;
         vector<literal_vector> m_q_clauses;
 
-        recfun_util & u() const { return m_util; }
+        recfun::util & u() const { return m_util; }
         bool is_defined(app * f) const { return u().is_defined(f); }
         bool is_case_pred(app * f) const { return u().is_case_pred(f); }