mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

recfun

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-21 18:25:27 -07:00
parent 918a5b9e8c
commit b5676413e4
7 changed files with 75 additions and 73 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/api/python/z3/z3.py
View file

@ -1,4 +1,5 @@
############################################
# Copyright (c) 2012 Microsoft Corporation
#

60
src/ast/recfun_decl_plugin.cpp
View file

@ -15,6 +15,7 @@ Revision History:
--*/
#include <functional>
#include <sstream>
#include "ast/expr_functors.h"
@ -29,14 +30,15 @@ Revision History:
namespace recfun {
case_def::case_def(ast_manager &m,
family_id fid,
def * d,
std::string & name,
unsigned case_index,
sort_ref_vector const & arg_sorts,
expr_ref_vector const& guards,
expr* rhs)
case_def::case_def(
ast_manager &m,
family_id fid,
def * d,
std::string & name,
unsigned case_index,
sort_ref_vector const & arg_sorts,
expr_ref_vector const& guards,
expr* rhs)
: m_pred(m),
m_guards(guards),
m_rhs(expr_ref(rhs,m)),
@ -52,11 +54,9 @@ namespace recfun {
m_domain(m, arity, domain),
m_range(range, m), m_vars(m), m_cases(),
m_decl(m),
m_fid(fid),
m_macro(false)
m_fid(fid)
{
SASSERT(arity == get_arity());
SASSERT(arity == get_arity());
func_decl_info info(fid, OP_FUN_DEFINED);
m_decl = m.mk_func_decl(s, arity, domain, range, info);
}
@ -124,7 +124,6 @@ namespace recfun {
case_state() : m_reg(), m_branches() {}
bool empty() const { return m_branches.empty(); }
region & reg() { return m_reg; }
branch pop_branch() {
branch res = m_branches.back();
@ -135,7 +134,7 @@ namespace recfun {
void push_branch(branch const & b) { m_branches.push_back(b); }
unfold_lst const * cons_unfold(expr * e, unfold_lst const * next) {
return new (reg()) unfold_lst{e, next};
return new (m_reg) unfold_lst{e, next};
}
unfold_lst const * cons_unfold(expr * e1, expr * e2, unfold_lst const * next) {
return cons_unfold(e1, cons_unfold(e2, next));
@ -145,11 +144,11 @@ namespace recfun {
}
ite_lst const * cons_ite(app * ite, ite_lst const * next) {
return new (reg()) ite_lst{ite, next};
return new (m_reg) ite_lst{ite, next};
}
choice_lst const * cons_choice(app * ite, bool sign, choice_lst const * next) {
return new (reg()) choice_lst{ite, sign, next};
return new (m_reg) choice_lst{ite, sign, next};
}
};
@ -203,21 +202,17 @@ namespace recfun {
unsigned case_idx = 0;
std::string name;
name.append("case_");
std::string name("case-");
name.append(m_name.bare_str());
name.append("_");
m_vars.append(n_vars, vars);
// is the function a macro (unconditional body)?
m_macro = n_vars == 0 || !contains_ite(rhs);
expr_ref_vector conditions(m);
if (m_macro) {
// is the function a macro (unconditional body)?
if (n_vars == 0 || !contains_ite(rhs)) {
// constant function or trivial control flow, only one (dummy) case
name.append("dummy");
add_case(name, 0, conditions, rhs);
return;
}
@ -311,15 +306,15 @@ namespace recfun {
*/
util::util(ast_manager & m, family_id id)
: m_manager(m), m_family_id(id), m_th_rw(m), m_plugin(0) {
m_plugin = dynamic_cast<decl::plugin*>(m.get_plugin(m_family_id));
: m_manager(m), m_fid(id), m_th_rw(m),
m_plugin(dynamic_cast<decl::plugin*>(m.get_plugin(m_fid))) {
}
util::~util() {
}
def * util::decl_fun(symbol const& name, unsigned n, sort *const * domain, sort * range) {
return alloc(def, m(), m_family_id, name, n, domain, range);
return alloc(def, m(), m_fid, name, n, domain, range);
}
void util::set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
@ -328,7 +323,7 @@ namespace recfun {
app_ref util::mk_depth_limit_pred(unsigned d) {
parameter p(d);
func_decl_info info(m_family_id, OP_DEPTH_LIMIT, 1, &p);
func_decl_info info(m_fid, OP_DEPTH_LIMIT, 1, &p);
func_decl* decl = m().mk_const_decl(symbol("recfun-depth-limit"), m().mk_bool_sort(), info);
return app_ref(m().mk_const(decl), m());
}
@ -376,13 +371,13 @@ namespace recfun {
m_defs.reset();
// m_case_defs does not own its data, no need to deallocate
m_case_defs.reset();
m_util = 0; // force deletion
m_util = nullptr; // force deletion
}
util & plugin::u() const {
SASSERT(m_manager);
SASSERT(m_family_id != null_family_id);
if (m_util.get() == 0) {
if (!m_util.get()) {
m_util = alloc(util, *m_manager, m_family_id);
}
return *(m_util.get());
@ -398,7 +393,7 @@ namespace recfun {
void plugin::set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
u().set_definition(d, n_vars, vars, rhs);
for (case_def & c : d.get_def()->get_cases()) {
m_case_defs.insert(c.get_name(), &c);
m_case_defs.insert(c.get_decl(), &c);
}
}
@ -434,7 +429,10 @@ namespace recfun {
func_decl * plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range)
{
switch(k) {
UNREACHABLE();
// TBD: parameter usage seems inconsistent with other uses.
IF_VERBOSE(0, verbose_stream() << "mk-func-decl " << k << "\n");
switch (k) {
case OP_FUN_CASE_PRED:
return mk_fun_pred_decl(num_parameters, parameters, arity, domain, range);
case OP_FUN_DEFINED:

31
src/ast/recfun_decl_plugin.h
View file

@ -19,6 +19,7 @@ Revision History:
#include "ast/ast.h"
#include "ast/rewriter/th_rewriter.h"
#include "util/obj_hashtable.h"
namespace recfun {
class case_def; //<! one possible control path of a function
@ -62,7 +63,7 @@ namespace recfun {
void add_guard(expr_ref && e) { m_guards.push_back(e); }
public:
symbol const& get_name() const { return m_pred->get_name(); }
func_decl* get_decl() const { return m_pred; }
app_ref apply_case_predicate(ptr_vector<expr> const & args) const {
ast_manager& m = m_pred.get_manager();
@ -97,7 +98,6 @@ namespace recfun {
cases m_cases; //!< possible cases
func_decl_ref m_decl; //!< generic declaration
family_id m_fid;
bool m_macro;
def(ast_manager &m, family_id fid, symbol const & s, unsigned arity, sort *const * domain, sort* range);
@ -115,11 +115,10 @@ namespace recfun {
sort_ref const & get_range() const { return m_range; }
func_decl * get_decl() const { return m_decl.get(); }
bool is_fun_macro() const { return m_macro; }
bool is_fun_macro() const { return m_cases.size() == 1; }
bool is_fun_defined() const { return !is_fun_macro(); }
expr * get_macro_rhs() const {
SASSERT(is_fun_macro());
return m_cases[0].get_rhs();
}
};
@ -140,7 +139,7 @@ namespace recfun {
class plugin : public decl_plugin {
typedef map<symbol, def*, symbol_hash_proc, symbol_eq_proc> def_map;
typedef map<symbol, case_def*, symbol_hash_proc, symbol_eq_proc> case_def_map;
typedef obj_map<func_decl, case_def*> case_def_map;
mutable scoped_ptr<util> m_util;
def_map m_defs; // function->def
@ -175,8 +174,8 @@ namespace recfun {
def const& get_def(const symbol& s) const { return *(m_defs[s]); }
promise_def get_promise_def(const symbol &s) const { return promise_def(&u(), m_defs[s]); }
def& get_def(symbol const& s) { return *(m_defs[s]); }
bool has_case_def(const symbol& s) const { return m_case_defs.contains(s); }
case_def& get_case_def(symbol const& s) { SASSERT(has_case_def(s)); return *(m_case_defs[s]); }
bool has_case_def(func_decl* f) const { return m_case_defs.contains(f); }
case_def& get_case_def(func_decl* f) { SASSERT(has_case_def(f)); return *(m_case_defs[f]); }
bool is_declared(symbol const& s) const { return m_defs.contains(s); }
private:
func_decl * mk_fun_pred_decl(unsigned num_parameters, parameter const * parameters,
@ -192,7 +191,7 @@ namespace recfun {
friend class decl::plugin;
ast_manager & m_manager;
family_id m_family_id;
family_id m_fid;
th_rewriter m_th_rw;
decl::plugin * m_plugin;
@ -205,10 +204,10 @@ namespace recfun {
ast_manager & m() { return m_manager; }
th_rewriter & get_th_rewriter() { return m_th_rw; }
bool is_case_pred(expr * e) const { return is_app_of(e, m_family_id, OP_FUN_CASE_PRED); }
bool is_defined(expr * e) const { return is_app_of(e, m_family_id, OP_FUN_DEFINED); }
bool is_depth_limit(expr * e) const { return is_app_of(e, m_family_id, OP_DEPTH_LIMIT); }
bool owns_app(app * e) const { return e->get_family_id() == m_family_id; }
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_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; }
bool has_def() const { return m_plugin->has_def(); }
@ -222,17 +221,13 @@ namespace recfun {
case_def& get_case_def(expr* e) {
SASSERT(is_case_pred(e));
return get_case_def(to_app(e)->get_name());
}
case_def& get_case_def(symbol const & s) {
SASSERT(m_plugin->has_case_def(s));
return m_plugin->get_case_def(s);
return m_plugin->get_case_def(to_app(e)->get_decl());
}
app* mk_fun_defined(def const & d, unsigned n_args, expr * const * args) {
return m().mk_app(d.get_decl(), n_args, args);
}
app* mk_fun_defined(def const & d, ptr_vector<expr> const & args) {
return mk_fun_defined(d, args.size(), args.c_ptr());
}

2
src/smt/params/smt_params_helper.pyg
View file

@ -97,5 +97,5 @@ def_module_params(module_name='smt',
('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none'),
('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy'),
('recfun.native', BOOL, False, 'use native rec-fun solver'),
('recfun.max_depth', UINT, 50, 'maximum depth of unrolling for recursive functions')
('recfun.max_depth', UINT, 2, 'maximum depth of unrolling for recursive functions')
))

5
src/smt/smt_context.h
View file

@ -1639,13 +1639,14 @@ namespace smt {
};
inline std::ostream & operator<<(std::ostream & out, pp_lits const & pp) {
out << "clause{";
out << "{";
bool first = true;
for (unsigned i = 0; i < pp.len; ++i) {
if (first) { first = false; } else { out << " ∨ "; }
if (first) { first = false; } else { out << " or\n"; }
pp.ctx.display_detailed_literal(out, pp.lits[i]);
}
return out << "}";
}
};

44
src/smt/theory_recfun.cpp
View file

@ -33,7 +33,7 @@ namespace smt {
m_plugin(*reinterpret_cast<recfun_decl_plugin*>(m.get_plugin(get_family_id()))),
m_util(m_plugin.u()),
m_guard_preds(m),
m_max_depth(0),
m_max_depth(UINT_MAX),
m_q_case_expand(),
m_q_body_expand()
{
@ -45,10 +45,12 @@ namespace smt {
char const * theory_recfun::get_name() const { return "recfun"; }
void theory_recfun::init_search_eh() {
// obtain max depth via parameters
smt_params_helper p(ctx().get_params());
set_max_depth(p.recfun_max_depth());
unsigned theory_recfun::get_max_depth() {
if (m_max_depth == UINT_MAX) {
smt_params_helper p(ctx().get_params());
set_max_depth(p.recfun_max_depth());
}
return m_max_depth;
}
theory* theory_recfun::mk_fresh(context* new_ctx) {
@ -121,7 +123,7 @@ namespace smt {
unsigned new_lim = m_guard_preds_lim.size()-num_scopes;
unsigned start = m_guard_preds_lim[new_lim];
for (unsigned i = start; i < m_guard_preds.size(); ++i) {
m_guards[m_guard_preds.get(i)->get_decl()].pop_back();
m_guards[m_guard_preds.get(i)].pop_back();
}
m_guard_preds.resize(start);
m_guard_preds_lim.shrink(new_lim);
@ -177,7 +179,6 @@ namespace smt {
c.push_back(~mk_literal(dlimit));
enable_trace("recfun");
TRACE("recfun", ctx().display(tout << c.back() << " " << dlimit << "\n"););
SASSERT(ctx().get_assignment(c.back()) == l_false);
for (expr * g : guards) {
c.push_back(mk_literal(g));
@ -194,17 +195,17 @@ namespace smt {
expr* e = ctx().bool_var2expr(v);
if (is_true && u().is_case_pred(e)) {
TRACEFN("assign_case_pred_true " << mk_pp(e, m));
app* a = to_app(e);
// body-expand
body_expansion b_e(u(), a);
body_expansion b_e(u(), to_app(e));
push_body_expand(std::move(b_e));
}
}
// replace `vars` by `args` in `e`
expr_ref theory_recfun::apply_args(recfun::vars const & vars,
ptr_vector<expr> const & args,
expr * e) {
expr_ref theory_recfun::apply_args(
recfun::vars const & vars,
ptr_vector<expr> const & args,
expr * e) {
SASSERT(is_standard_order(vars));
var_subst subst(m, true);
expr_ref new_body(m);
@ -245,14 +246,14 @@ namespace smt {
* 2. add unit clause `f(args) = rhs`
*/
void theory_recfun::assert_macro_axiom(case_expansion & e) {
TRACEFN("case expansion " << pp_case_expansion(e, m) << "\n");
TRACEFN("case expansion " << pp_case_expansion(e, m) << "\n");
SASSERT(e.m_def->is_fun_macro());
auto & vars = e.m_def->get_vars();
expr_ref lhs(e.m_lhs, m);
expr_ref rhs(apply_args(vars, e.m_args, e.m_def->get_macro_rhs()), m);
literal lit = mk_eq_lit(lhs, rhs);
ctx().mk_th_axiom(get_id(), 1, &lit);
TRACEFN("macro expansion yields " << mk_pp(rhs,m) << "\n" <<
TRACEFN("macro expansion yields " << mk_pp(rhs, m) << "\n" <<
"literal " << pp_lit(ctx(), lit));
}
@ -291,9 +292,10 @@ namespace smt {
assert_body_axiom(be);
// add to set of local assumptions, for depth-limit purpose
func_decl* d = pred_applied->get_decl();
// func_decl* d = pred_applied->get_decl();
m_guard_preds.push_back(pred_applied);
auto& vec = m_guards.insert_if_not_there2(d, ptr_vector<expr>())->get_data().m_value;
auto& vec = m_guards.insert_if_not_there2(e.m_lhs, ptr_vector<expr>())->get_data().m_value;
vec.push_back(pred_applied);
if (vec.size() == get_max_depth()) {
max_depth_limit(vec);
@ -322,11 +324,17 @@ namespace smt {
for (auto & g : e.m_cdef->get_guards()) {
expr_ref guard = apply_args(vars, args, g);
clause.push_back(~mk_literal(guard));
if (clause.back() == true_literal) {
return;
}
if (clause.back() == false_literal) {
clause.pop_back();
}
}
clause.push_back(mk_eq_lit(lhs, rhs));
ctx().mk_th_axiom(get_id(), clause);
TRACEFN("body " << pp_body_expansion(e,m));
TRACEFN("clause " << pp_lits(ctx(), clause));
TRACEFN(pp_lits(ctx(), clause));
}
final_check_status theory_recfun::final_check_eh() {
@ -373,7 +381,7 @@ namespace smt {
}
std::ostream& operator<<(std::ostream & out, theory_recfun::pp_body_expansion const & e) {
out << "body_exp(" << e.e.m_cdef->get_name();
out << "body_exp(" << e.e.m_cdef->get_decl()->get_name();
for (auto* t : e.e.m_args) {
out << " " << mk_pp(t,e.m);
}

5
src/smt/theory_recfun.h
View file

@ -90,7 +90,7 @@ namespace smt {
recfun_decl_plugin& m_plugin;
recfun_util& m_util;
stats m_stats;
obj_map<func_decl, ptr_vector<expr> > m_guards;
obj_map<expr, ptr_vector<expr> > m_guards;
app_ref_vector m_guard_preds;
unsigned_vector m_guard_preds_lim;
unsigned m_max_depth; // for fairness and termination
@ -138,12 +138,11 @@ namespace smt {
void add_theory_assumptions(expr_ref_vector & assumptions) override;
void set_max_depth(unsigned n) { SASSERT(n>0); m_max_depth = n; }
unsigned get_max_depth() const { return m_max_depth; }
unsigned get_max_depth();
public:
theory_recfun(ast_manager & m);
~theory_recfun() override;
void init_search_eh() override;
theory * mk_fresh(context * new_ctx) override;
void display(std::ostream & out) const override;
void collect_statistics(::statistics & st) const override;