mirror of
https://github.com/Z3Prover/z3
synced 2026-05-08 19:35:25 +00:00
disable elim-uncnstr under quantifiers #9293
This commit is contained in:
Nikolaj Bjorner
parent
101a9233bc
commit
844e248b1e
3 changed files with 76 additions and 11 deletions
|
|
@ -121,7 +121,7 @@ eliminate:
|
|||
elim_unconstrained::elim_unconstrained(ast_manager& m, dependent_expr_state& fmls) :
|
||||
dependent_expr_simplifier(m, fmls), m_inverter(m), m_lt(*this), m_heap(1024, m_lt), m_trail(m), m_args(m) {
|
||||
std::function<bool(expr*)> is_var = [&](expr* e) {
|
||||
return is_uninterp_const(e) && !m_fmls.frozen(e) && get_node(e).is_root() && get_node(e).num_parents() <= 1;
|
||||
return is_uninterp_const(e) && !m_fmls.frozen(e) && !m_disabled.is_marked(e) && get_node(e).is_root() && get_node(e).num_parents() <= 1;
|
||||
};
|
||||
m_inverter.set_is_var(is_var);
|
||||
}
|
||||
|
|
@ -247,10 +247,12 @@ elim_unconstrained::node& elim_unconstrained::get_node(expr* t) {
|
|||
m_heap.increased(arg->get_id());
|
||||
}
|
||||
}
|
||||
else if (is_quantifier(t)) {
|
||||
node& ch = get_node(to_quantifier(t)->get_expr());
|
||||
else if (is_quantifier(t)) {
|
||||
auto body = to_quantifier(t)->get_expr();
|
||||
node& ch = get_node(body);
|
||||
SASSERT(ch.is_root());
|
||||
ch.add_parent(*n);
|
||||
disable(body);
|
||||
}
|
||||
}
|
||||
return *n;
|
||||
|
|
@ -436,6 +438,7 @@ void elim_unconstrained::reduce() {
|
|||
assert_normalized(old_fmls);
|
||||
update_model_trail(*mc, old_fmls);
|
||||
mc->reset();
|
||||
m_disabled.reset();
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -443,3 +446,21 @@ void elim_unconstrained::updt_params(params_ref const& p) {
|
|||
smt_params_helper sp(p);
|
||||
m_config.m_enabled = sp.elim_unconstrained();
|
||||
}
|
||||
|
||||
void elim_unconstrained::disable(expr* e) {
|
||||
if (m_disabled.is_marked(e))
|
||||
return;
|
||||
|
||||
ptr_buffer<expr> todo;
|
||||
todo.push_back(e);
|
||||
while (!todo.empty()) {
|
||||
e = todo.back();
|
||||
todo.pop_back();
|
||||
if (m_disabled.is_marked(e))
|
||||
continue;
|
||||
m_disabled.mark(e);
|
||||
if (is_app(e))
|
||||
for (auto arg : *to_app(e))
|
||||
todo.push_back(arg);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -92,6 +92,7 @@ class elim_unconstrained : public dependent_expr_simplifier {
|
|||
stats m_stats;
|
||||
config m_config;
|
||||
bool m_created_compound = false;
|
||||
expr_mark m_disabled;
|
||||
|
||||
bool is_var_lt(int v1, int v2) const;
|
||||
node& get_node(unsigned n) const { return *m_nodes[n]; }
|
||||
|
|
@ -108,6 +109,7 @@ class elim_unconstrained : public dependent_expr_simplifier {
|
|||
expr* reconstruct_term(node& n);
|
||||
void assert_normalized(vector<dependent_expr>& old_fmls);
|
||||
void update_model_trail(generic_model_converter& mc, vector<dependent_expr> const& old_fmls);
|
||||
void disable(expr *e);
|
||||
|
||||
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -25,6 +25,7 @@ Notes:
|
|||
#include "ast/array_decl_plugin.h"
|
||||
#include "ast/datatype_decl_plugin.h"
|
||||
#include "ast/seq_decl_plugin.h"
|
||||
#include "ast/for_each_expr.h"
|
||||
#include "tactic/core/collect_occs.h"
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
|
|
@ -39,7 +40,8 @@ class elim_uncnstr_tactic : public tactic {
|
|||
struct rw_cfg : public default_rewriter_cfg {
|
||||
bool m_produce_proofs;
|
||||
obj_hashtable<expr> & m_vars;
|
||||
obj_hashtable<expr>& m_nonvars;
|
||||
obj_hashtable<expr>& m_nonvars;
|
||||
expr_mark & m_disabled;
|
||||
ref<mc> m_mc;
|
||||
arith_util m_a_util;
|
||||
bv_util m_bv_util;
|
||||
|
|
@ -52,11 +54,14 @@ class elim_uncnstr_tactic : public tactic {
|
|||
unsigned long long m_max_memory;
|
||||
unsigned m_max_steps;
|
||||
|
||||
rw_cfg(ast_manager & m, bool produce_proofs, obj_hashtable<expr> & vars, obj_hashtable<expr> & nonvars, mc * _m,
|
||||
rw_cfg(ast_manager & m, bool produce_proofs, obj_hashtable<expr> & vars,
|
||||
obj_hashtable<expr> & nonvars, expr_mark& disabled,
|
||||
mc * _m,
|
||||
unsigned long long max_memory, unsigned max_steps):
|
||||
m_produce_proofs(produce_proofs),
|
||||
m_vars(vars),
|
||||
m_nonvars(nonvars),
|
||||
m_nonvars(nonvars),
|
||||
m_disabled(disabled),
|
||||
m_mc(_m),
|
||||
m_a_util(m),
|
||||
m_bv_util(m),
|
||||
|
|
@ -78,7 +83,7 @@ class elim_uncnstr_tactic : public tactic {
|
|||
}
|
||||
|
||||
bool uncnstr(expr * arg) const {
|
||||
return m_vars.contains(arg) && !m_nonvars.contains(arg);
|
||||
return m_vars.contains(arg) && !m_nonvars.contains(arg) && !m_disabled.is_marked(arg);
|
||||
}
|
||||
|
||||
bool uncnstr(unsigned num, expr * const * args) const {
|
||||
|
|
@ -878,10 +883,11 @@ class elim_uncnstr_tactic : public tactic {
|
|||
class rw : public rewriter_tpl<rw_cfg> {
|
||||
rw_cfg m_cfg;
|
||||
public:
|
||||
rw(ast_manager & m, bool produce_proofs, obj_hashtable<expr> & vars, obj_hashtable<expr>& nonvars, mc * _m,
|
||||
rw(ast_manager & m, bool produce_proofs, obj_hashtable<expr> & vars, obj_hashtable<expr>& nonvars,
|
||||
expr_mark& disabled, mc * _m,
|
||||
unsigned long long max_memory, unsigned max_steps):
|
||||
rewriter_tpl<rw_cfg>(m, produce_proofs, m_cfg),
|
||||
m_cfg(m, produce_proofs, vars, nonvars, _m, max_memory, max_steps) {
|
||||
m_cfg(m, produce_proofs, vars, nonvars, disabled, _m, max_memory, max_steps) {
|
||||
}
|
||||
};
|
||||
|
||||
|
|
@ -889,6 +895,8 @@ class elim_uncnstr_tactic : public tactic {
|
|||
ref<mc> m_mc;
|
||||
obj_hashtable<expr> m_vars;
|
||||
obj_hashtable<expr> m_nonvars;
|
||||
expr_mark m_disabled;
|
||||
expr_ref_vector m_pinned;
|
||||
scoped_ptr<rw> m_rw;
|
||||
unsigned m_num_elim_apps = 0;
|
||||
unsigned long long m_max_memory;
|
||||
|
|
@ -903,7 +911,7 @@ class elim_uncnstr_tactic : public tactic {
|
|||
}
|
||||
|
||||
void init_rw(bool produce_proofs) {
|
||||
m_rw = alloc(rw, m(), produce_proofs, m_vars, m_nonvars, m_mc.get(), m_max_memory, m_max_steps);
|
||||
m_rw = alloc(rw, m(), produce_proofs, m_vars, m_nonvars, m_disabled, m_mc.get(), m_max_memory, m_max_steps);
|
||||
}
|
||||
|
||||
void run(goal_ref const & g, goal_ref_buffer & result) {
|
||||
|
|
@ -914,6 +922,7 @@ class elim_uncnstr_tactic : public tactic {
|
|||
m_vars.reset();
|
||||
collect_occs p;
|
||||
p(*g, m_vars);
|
||||
disable_quantified(g);
|
||||
if (m_vars.empty() || recfun::util(m()).has_rec_defs()) {
|
||||
result.push_back(g.get());
|
||||
// did not increase depth since it didn't do anything.
|
||||
|
|
@ -931,6 +940,7 @@ class elim_uncnstr_tactic : public tactic {
|
|||
unsigned round = 0;
|
||||
unsigned size = g->size();
|
||||
unsigned idx = 0;
|
||||
|
||||
while (true) {
|
||||
for (; idx < size; ++idx) {
|
||||
expr * f = g->form(idx);
|
||||
|
|
@ -964,6 +974,7 @@ class elim_uncnstr_tactic : public tactic {
|
|||
size = g->size();
|
||||
m_rw->reset(); // reset cache
|
||||
m_vars.reset();
|
||||
disable_quantified(g);
|
||||
{
|
||||
collect_occs p;
|
||||
p(*g, m_vars);
|
||||
|
|
@ -974,11 +985,42 @@ class elim_uncnstr_tactic : public tactic {
|
|||
idx = 0;
|
||||
}
|
||||
}
|
||||
|
||||
void disable(expr* e) {
|
||||
if (m_disabled.is_marked(e))
|
||||
return;
|
||||
m_pinned.push_back(e);
|
||||
|
||||
ptr_buffer<expr> todo;
|
||||
todo.push_back(e);
|
||||
while (!todo.empty()) {
|
||||
e = todo.back();
|
||||
todo.pop_back();
|
||||
if (m_disabled.is_marked(e))
|
||||
continue;
|
||||
m_disabled.mark(e);
|
||||
if (is_app(e))
|
||||
for (auto arg : *to_app(e))
|
||||
todo.push_back(arg);
|
||||
}
|
||||
}
|
||||
|
||||
void disable_quantified(goal_ref const &g) {
|
||||
m_disabled.reset();
|
||||
m_pinned.reset();
|
||||
|
||||
for (unsigned idx = 0; idx < g->size(); ++idx) {
|
||||
expr *f = g->form(idx);
|
||||
for (expr *e : subterms::all(expr_ref(f, m())))
|
||||
if (is_quantifier(e))
|
||||
disable(to_quantifier(e)->get_expr());
|
||||
}
|
||||
}
|
||||
|
||||
params_ref m_params;
|
||||
public:
|
||||
elim_uncnstr_tactic(ast_manager & m, params_ref const & p):
|
||||
m_manager(m), m_params(p) {
|
||||
m_manager(m), m_pinned(m), m_params(p) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue