diff --git a/CMakeLists.txt b/CMakeLists.txt
index 28ff64568..cd9c14435 100644
--- a/CMakeLists.txt
+++ b/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
diff --git a/RELEASE_NOTES b/RELEASE_NOTES
index acdb627d8..dcb8fc093 100644
--- a/RELEASE_NOTES
+++ b/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
=============
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 18d57e729..5bd96c0fc 100644
--- a/scripts/mk_project.py
+++ b/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'])
diff --git a/src/api/api_context.h b/src/api/api_context.h
index b04768710..a6b8600d6 100644
--- a/src/api/api_context.h
+++ b/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; }
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 97541e31f..ac11022c1 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -532,6 +532,34 @@ namespace Microsoft.Z3
return new FuncDecl(this, MkSymbol(name), domain, range);
}
+ ///
+ /// Creates a new recursive function declaration.
+ ///
+ public FuncDecl MkRecFuncDecl(string name, Sort[] domain, Sort range)
+ {
+ Debug.Assert(range != null);
+ Debug.Assert(domain.All(d => d != null));
+
+ CheckContextMatch(domain);
+ CheckContextMatch(range);
+ return new FuncDecl(this, MkSymbol(name), domain, range, true);
+ }
+
+ ///
+ /// 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.
+ ///
+ public void AddRecDef(FuncDecl f, Expr[] args, Expr body)
+ {
+ CheckContextMatch(f);
+ CheckContextMatch(args);
+ CheckContextMatch(body);
+ IntPtr[] argsNative = AST.ArrayToNative(args);
+ Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
+ }
+
///
/// Creates a new function declaration.
///
diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs
index 24ae456d8..30ed790db 100644
--- a/src/api/dotnet/FuncDecl.cs
+++ b/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)
{
diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp
index 378710b36..a57ea6040 100644
--- a/src/ast/ast_pp_util.cpp
+++ b/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> 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) {
diff --git a/src/ast/ast_pp_util.h b/src/ast/ast_pp_util.h
index c3b8aa601..e70880672 100644
--- a/src/ast/ast_pp_util.h
+++ b/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);
diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 3a55bbb0b..5f2d36279 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/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> 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(m(), args, args+3, f2f(), ""));
+ process(e, r);
+ bodies.push_back(r);
+ unregister_var_names(f->get_arity());
+ }
+ r1 = mk_seq1(m(), decls.begin(), decls.end(), f2f(), "");
+ r2 = mk_seq1(m(), bodies.begin(), bodies.end(), f2f(), "");
+ format * args[2];
+ args[0] = r1;
+ args[1] = r2;
+ r = mk_seq1(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> 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),
diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
index 13093f138..dc306c6df 100644
--- a/src/ast/ast_smt2_pp.h
+++ b/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> const& funs, smt2_pp_environment & env, params_ref const & p = params_ref());
+
/**
\brief Internal wrapper (for debugging purposes only)
diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index 5e2828adf..227e00419 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/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) {
diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp
index bec60e61c..bc415c461 100644
--- a/src/ast/decl_collector.cpp
+++ b/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_preds.push_back(n);
- else
- m_decls.push_back(n);
+ 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();
diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h
index 07539dbd8..8945c0bec 100644
--- a/src/ast/decl_collector.h
+++ b/src/ast/decl_collector.h
@@ -26,10 +26,8 @@ Revision History:
class decl_collector {
ast_manager & m_manager;
- bool m_sep_preds;
ptr_vector m_sorts;
ptr_vector m_decls;
- ptr_vector 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, bool preds = true);
+ decl_collector(ast_manager & m);
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
diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index ca929a9d7..7fe7ae00b 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/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() {
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index 6bd338f54..347689a37 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -143,9 +143,8 @@ namespace recfun {
typedef obj_map case_def_map;
mutable scoped_ptr m_util;
- def_map m_defs; // function->def
- case_def_map m_case_defs; // case_pred->def
- svector m_def_block;
+ def_map m_defs; // function->def
+ case_def_map m_case_defs; // case_pred->def
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;
diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp
index f8abe81d8..7e121eb7f 100644
--- a/src/ast/reg_decl_plugins.cpp
+++ b/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));
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index a4b949280..db0164445 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/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 labels;
m_solver->get_labels(labels);
regular_stream() << "(labels";
- for (unsigned i = 0; i < labels.size(); i++) {
- regular_stream() << " " << labels[i];
+ for (symbol const& s : labels) {
+ regular_stream() << " " << s;
}
regular_stream() << "))" << std::endl;
}
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 5e21a1bca..b2ed1e5cb 100644
--- a/src/cmd_context/cmd_context.h
+++ b/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);
diff --git a/src/model/model_smt2_pp.cpp b/src/model/model_smt2_pp.cpp
index 807e2b4e7..b2a4f02aa 100644
--- a/src/model/model_smt2_pp.cpp
+++ b/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::const_iterator it = u.begin();
- ptr_vector::const_iterator end = u.end();
- for (; it != end; ++it) {
- SASSERT(is_app(*it));
- app * c = to_app(*it);
+ for (expr* e : u) {
+ SASSERT(is_app(e));
+ app * c = to_app(e);
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 (; it != end; ++it) {
- app * c = to_app(*it);
+ for (expr * e : u) {
+ app * c = to_app(e);
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 (; it != end; ++it) {
- app * c = to_app(*it);
+ for (expr* e : u) {
+ app * c = to_app(e);
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_bufferget_else(), deps);
- func_decl_set::iterator it2 = deps.begin();
- func_decl_set::iterator end2 = deps.end();
- for (; it2 != end2; ++it2) {
- func_decl * d = *it2;
+ for (func_decl * d : deps) {
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 var_names;
ptr_buffer f_var_names;
ptr_buffer 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));
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index 88354f1eb..c3e7c997e 100644
--- a/src/smt/theory_recfun.cpp
+++ b/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(m.get_plugin(get_family_id()))),
+ m_plugin(*reinterpret_cast(m.get_plugin(get_family_id()))),
m_util(m_plugin.u()),
m_preds(m),
m_max_depth(0),
diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h
index 56e738f21..46392c6d2 100644
--- a/src/smt/theory_recfun.h
+++ b/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 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 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 & args) :
+ body_expansion(app* pred, recfun::case_def const & d, ptr_vector & 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_util& m_util;
+ recfun::decl::plugin& m_plugin;
+ recfun::util& m_util;
stats m_stats;
// book-keeping for depth of predicates
@@ -104,7 +104,7 @@ namespace smt {
ptr_vector m_q_body_expand;
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); }