mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

n/a

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-18 18:07:04 -07:00
parent c0556b2f64
commit 2d4a5e0a5e
4 changed files with 17 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/ast/recfun_decl_plugin.h
View file

@ -201,6 +201,7 @@ namespace recfun {
def* mk_def(symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs);
bool has_def(const symbol& s) const { return m_defs.contains(s); }
bool has_def() const { return !m_defs.empty(); }
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]); }
@ -241,6 +242,8 @@ namespace recfun {
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 has_def() const { return m_plugin->has_def(); }
//<! add a function declaration
def * decl_fun(symbol const & s, unsigned n_args, sort *const * args, sort * range);

1
src/smt/smt_setup.cpp
View file

@ -884,7 +884,6 @@ namespace smt {
TRACE("recfun", tout << "registering theory recfun...\n";);
theory_recfun * th = alloc(theory_recfun, m_manager);
m_context.register_plugin(th);
th->setup_params();
}
void setup::setup_dl() {

25
src/smt/theory_recfun.cpp
View file

@ -45,7 +45,7 @@ namespace smt {
char const * theory_recfun::get_name() const { return "recfun"; }
void theory_recfun::setup_params() {
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());
@ -330,28 +330,15 @@ namespace smt {
}
final_check_status theory_recfun::final_check_eh() {
if (m_guards.size() > get_max_depth()) {
#if 1
return FC_GIVEUP;
#else
for (unsigned i = get_max_depth(); i < m_guards.size(); ++i) {
app* a = m_guards.get(i);
body_expansion b_e(u(), a);
push_body_expand(std::move(b_e));
}
unsigned new_depth = m_guards.size() + 1;
IF_VERBOSE(2, verbose_stream() << "(smt.recfun :new-depth " << new_depth << ")\n");
set_max_depth(new_depth);
return FC_CONTINUE;
#endif
}
return FC_DONE;
}
void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) {
app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth());
TRACEFN("add_theory_assumption " << mk_pp(dlimit.get(), m));
assumptions.push_back(dlimit);
if (u().has_def()) {
app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth());
TRACEFN("add_theory_assumption " << mk_pp(dlimit.get(), m));
assumptions.push_back(dlimit);
}
}
// if `dlimit` occurs in unsat core, return 'true'

16
src/smt/theory_recfun.h
View file

@ -138,16 +138,16 @@ namespace smt {
void new_diseq_eh(theory_var v1, theory_var v2) override {}
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; }
public:
theory_recfun(ast_manager & m);
virtual ~theory_recfun() override;
void setup_params(); // read parameters
virtual theory * mk_fresh(context * new_ctx) override;
virtual void display(std::ostream & out) const override;
virtual void collect_statistics(::statistics & st) const override;
unsigned get_max_depth() const { return m_max_depth; }
void set_max_depth(unsigned n) { SASSERT(n>0); m_max_depth = n; }
void inc_max_depth() { ++m_max_depth; }
~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;
};
}