mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

only case expand for cases that contain defs. fixes #2601

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-01 18:41:11 -07:00
parent 88f0e4a64c
commit 6616b6a366
2 changed files with 25 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/ast/recfun_decl_plugin.cpp
View file

@ -64,17 +64,30 @@ namespace recfun {
m_decl = m.mk_func_decl(s, arity, domain, range, info);
}
bool def::contains_def(util& u, expr * e) {
struct def_find_p : public i_expr_pred {
util& u;
def_find_p(util& u): u(u) {}
bool operator()(expr* a) override { return is_app(a) && u.is_defined(to_app(a)->get_decl()); }
};
def_find_p p(u);
check_pred cp(p, m, false);
return cp(e);
}
// does `e` contain any `ite` construct?
bool def::contains_ite(expr * e) {
bool def::contains_ite(util& u, expr * e) {
struct ite_find_p : public i_expr_pred {
ast_manager & m;
ite_find_p(ast_manager & m) : m(m) {}
bool operator()(expr * e) override { return m.is_ite(e); }
def& d;
util& u;
ite_find_p(ast_manager & m, def& d, util& u) : m(m), d(d), u(u) {}
bool operator()(expr * e) override { return m.is_ite(e) && d.contains_def(u, e); }
};
// ignore ites under quantifiers.
// this is redundant as the code
// that unfolds ites uses quantifier-free portion.
ite_find_p p(m);
ite_find_p p(m, *this, u);
check_pred cp(p, m, false);
return cp(e);
}
@ -189,7 +202,8 @@ namespace recfun {
// Compute a set of cases, given the RHS
void def::compute_cases(replace& subst,
void def::compute_cases(util& u,
replace& subst,
is_immediate_pred & is_i,
unsigned n_vars, var *const * vars, expr* rhs)
{
@ -209,7 +223,7 @@ namespace recfun {
expr_ref_vector conditions(m);
// is the function a macro (unconditional body)?
if (n_vars == 0 || !contains_ite(rhs)) {
if (n_vars == 0 || !contains_ite(u, rhs)) {
// constant function or trivial control flow, only one (dummy) case
add_case(name, 0, conditions, rhs);
return;
@ -248,7 +262,7 @@ namespace recfun {
else if (is_app(e)) {
// explore arguments
for (expr * arg : *to_app(e)) {
if (contains_ite(arg)) {
if (contains_ite(u, arg)) {
stack.push_back(arg);
}
}
@ -361,7 +375,7 @@ namespace recfun {
SASSERT(n_vars == d->get_arity());
is_imm_pred is_i(*u);
d->compute_cases(r, is_i, n_vars, vars, rhs);
d->compute_cases(*u, r, is_i, n_vars, vars, rhs);
}
namespace decl {

5
src/ast/recfun_decl_plugin.h
View file

@ -111,10 +111,11 @@ namespace recfun {
def(ast_manager &m, family_id fid, symbol const & s, unsigned arity, sort *const * domain, sort* range, bool is_generated);
// compute cases for a function, given its RHS (possibly containing `ite`).
void compute_cases(replace& subst, is_immediate_pred &,
void compute_cases(util& u, replace& subst, is_immediate_pred &,
unsigned n_vars, var *const * vars, expr* rhs);
void add_case(std::string & name, unsigned case_index, expr_ref_vector const& conditions, expr* rhs, bool is_imm = false);
bool contains_ite(expr* e); // expression contains a test?
bool contains_ite(util& u, expr* e); // expression contains a test?
bool contains_def(util& u, expr* e); // expression contains a def
public:
symbol const & get_name() const { return m_name; }
vars const & get_vars() const { return m_vars; }