mirror of
https://github.com/Z3Prover/z3
synced 2025-06-04 21:31:22 +00:00
injectivity: Cleanup whitespace
This commit is contained in:
Nicolas Braud-Santoni
parent
27fd879b8c
commit
ae9ace2321
1 changed files with 170 additions and 170 deletions
|
|
@ -29,120 +29,120 @@ Notes:
|
||||||
|
|
||||||
class injectivity_tactic : public tactic {
|
class injectivity_tactic : public tactic {
|
||||||
|
|
||||||
struct InjHelper : public obj_map<func_decl, obj_hashtable<func_decl>*> {
|
struct InjHelper : public obj_map<func_decl, obj_hashtable<func_decl>*> {
|
||||||
ast_manager & m_manager;
|
ast_manager & m_manager;
|
||||||
|
|
||||||
void insert(func_decl* const f, func_decl* const g) {
|
void insert(func_decl* const f, func_decl* const g) {
|
||||||
obj_hashtable<func_decl> *m;
|
obj_hashtable<func_decl> *m;
|
||||||
if (! obj_map::find(f, m)) {
|
if (! obj_map::find(f, m)) {
|
||||||
m_manager.inc_ref(f);
|
m_manager.inc_ref(f);
|
||||||
m = alloc(obj_hashtable<func_decl>); // TODO: Check we don't leak memory
|
m = alloc(obj_hashtable<func_decl>); // TODO: Check we don't leak memory
|
||||||
obj_map::insert(f, m);
|
obj_map::insert(f, m);
|
||||||
}
|
}
|
||||||
if (!m->contains(g)) {
|
if (!m->contains(g)) {
|
||||||
m_manager.inc_ref(g);
|
m_manager.inc_ref(g);
|
||||||
m->insert(g);
|
m->insert(g);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
bool find(func_decl* const f, func_decl* const g) const {
|
bool find(func_decl* const f, func_decl* const g) const {
|
||||||
obj_hashtable<func_decl> *m;
|
obj_hashtable<func_decl> *m;
|
||||||
if(! obj_map::find(f, m))
|
if(! obj_map::find(f, m))
|
||||||
return false;
|
return false;
|
||||||
|
|
||||||
return m->contains(g);
|
return m->contains(g);
|
||||||
}
|
}
|
||||||
|
|
||||||
InjHelper(ast_manager& m) : obj_map<func_decl, obj_hashtable<func_decl>*>(), m_manager(m) {}
|
InjHelper(ast_manager& m) : obj_map<func_decl, obj_hashtable<func_decl>*>(), m_manager(m) {}
|
||||||
~InjHelper() {
|
~InjHelper() {
|
||||||
for(auto m : *this) {
|
for(auto m : *this) {
|
||||||
for (func_decl* f : *m.get_value())
|
for (func_decl* f : *m.get_value())
|
||||||
m_manager.dec_ref(f);
|
m_manager.dec_ref(f);
|
||||||
|
|
||||||
m_manager.dec_ref(m.m_key);
|
m_manager.dec_ref(m.m_key);
|
||||||
dealloc(m.m_value);
|
dealloc(m.m_value);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
};
|
};
|
||||||
|
|
||||||
struct finder {
|
struct finder {
|
||||||
ast_manager & m_manager;
|
ast_manager & m_manager;
|
||||||
InjHelper & inj_map;
|
InjHelper & inj_map;
|
||||||
|
|
||||||
finder(ast_manager & m, InjHelper & map, params_ref const & p) :
|
finder(ast_manager & m, InjHelper & map, params_ref const & p) :
|
||||||
m_manager(m),
|
m_manager(m),
|
||||||
inj_map(map) {
|
inj_map(map) {
|
||||||
updt_params(p);
|
updt_params(p);
|
||||||
}
|
}
|
||||||
|
|
||||||
ast_manager & m() const { return m_manager; }
|
ast_manager & m() const { return m_manager; }
|
||||||
|
|
||||||
bool is_axiom(expr* n, func_decl* &f, func_decl* &g) {
|
bool is_axiom(expr* n, func_decl* &f, func_decl* &g) {
|
||||||
if (!is_quantifier(n))
|
if (!is_quantifier(n))
|
||||||
return false;
|
return false;
|
||||||
|
|
||||||
quantifier* const q = to_quantifier(n);
|
quantifier* const q = to_quantifier(n);
|
||||||
if (!q->is_forall() || q->get_num_decls() != 1)
|
if (!q->is_forall() || q->get_num_decls() != 1)
|
||||||
return false;
|
return false;
|
||||||
|
|
||||||
const expr * const body = q->get_expr();
|
const expr * const body = q->get_expr();
|
||||||
|
|
||||||
// n ~= forall x. body
|
// n ~= forall x. body
|
||||||
|
|
||||||
if (!m().is_eq(body))
|
if (!m().is_eq(body))
|
||||||
return false;
|
return false;
|
||||||
|
|
||||||
const app * const body_a = to_app(body);
|
const app * const body_a = to_app(body);
|
||||||
if (body_a->get_num_args() != 2)
|
if (body_a->get_num_args() != 2)
|
||||||
return false;
|
return false;
|
||||||
|
|
||||||
const expr* a = body_a->get_arg(0);
|
const expr* a = body_a->get_arg(0);
|
||||||
const expr* b = body_a->get_arg(1);
|
const expr* b = body_a->get_arg(1);
|
||||||
|
|
||||||
// n ~= forall x. (= a b)
|
// n ~= forall x. (= a b)
|
||||||
|
|
||||||
if (is_app(a) && is_var(b)) {
|
if (is_app(a) && is_var(b)) {
|
||||||
// Do nothing
|
// Do nothing
|
||||||
}
|
}
|
||||||
else if (is_app(b) && is_var(a)) {
|
else if (is_app(b) && is_var(a)) {
|
||||||
std::swap(a, b);
|
std::swap(a, b);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
return false;
|
return false;
|
||||||
|
|
||||||
const app* const a_app = to_app(a);
|
const app* const a_app = to_app(a);
|
||||||
const var* const b_var = to_var(b);
|
const var* const b_var = to_var(b);
|
||||||
|
|
||||||
if (b_var->get_idx() != 0) // idx is the De Bruijn's index
|
if (b_var->get_idx() != 0) // idx is the De Bruijn's index
|
||||||
return false;
|
return false;
|
||||||
|
|
||||||
if (a_app->get_num_args() != 1)
|
if (a_app->get_num_args() != 1)
|
||||||
return false;
|
return false;
|
||||||
|
|
||||||
g = a_app->get_decl();
|
g = a_app->get_decl();
|
||||||
const expr* const a_body = a_app->get_arg(0);
|
const expr* const a_body = a_app->get_arg(0);
|
||||||
|
|
||||||
// n ~= forall x. (= (g a_body) x)
|
// n ~= forall x. (= (g a_body) x)
|
||||||
|
|
||||||
if (!is_app(a_body))
|
if (!is_app(a_body))
|
||||||
return false;
|
return false;
|
||||||
const app* const a_body_app = to_app(a_body);
|
const app* const a_body_app = to_app(a_body);
|
||||||
if (a_body_app->get_num_args() != 1) // Maybe TODO: support multi-argument functions
|
if (a_body_app->get_num_args() != 1) // Maybe TODO: support multi-argument functions
|
||||||
return false;
|
return false;
|
||||||
|
|
||||||
f = a_body_app->get_decl();
|
f = a_body_app->get_decl();
|
||||||
const expr* const a_body_body = a_body_app->get_arg(0);
|
const expr* const a_body_body = a_body_app->get_arg(0);
|
||||||
|
|
||||||
// n ~= forall x. (= (g (f a_body_body)) x)
|
|
||||||
if (a_body_body != b_var)
|
|
||||||
return false;
|
|
||||||
|
|
||||||
// n ~= forall x. (= (g (f x)) x)
|
// n ~= forall x. (= (g (f a_body_body)) x)
|
||||||
|
if (a_body_body != b_var)
|
||||||
|
return false;
|
||||||
|
|
||||||
|
// n ~= forall x. (= (g (f x)) x)
|
||||||
|
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
void operator()(goal_ref const & goal,
|
void operator()(goal_ref const & goal,
|
||||||
goal_ref_buffer & result,
|
goal_ref_buffer & result,
|
||||||
model_converter_ref & mc,
|
model_converter_ref & mc,
|
||||||
|
|
@ -152,112 +152,112 @@ class injectivity_tactic : public tactic {
|
||||||
mc = 0; pc = 0; core = 0;
|
mc = 0; pc = 0; core = 0;
|
||||||
tactic_report report("injectivity", *goal);
|
tactic_report report("injectivity", *goal);
|
||||||
fail_if_unsat_core_generation("injectivity", goal); // TODO: Support UNSAT cores
|
fail_if_unsat_core_generation("injectivity", goal); // TODO: Support UNSAT cores
|
||||||
fail_if_proof_generation("injectivity", goal);
|
fail_if_proof_generation("injectivity", goal);
|
||||||
|
|
||||||
for (unsigned i = 0; i < goal->size(); ++i) {
|
for (unsigned i = 0; i < goal->size(); ++i) {
|
||||||
func_decl *f, *g;
|
func_decl *f, *g;
|
||||||
if (!is_axiom(goal->form(i), f, g)) continue;
|
if (!is_axiom(goal->form(i), f, g)) continue;
|
||||||
TRACE("injectivity", tout << "Marking " << f->get_name() << " as injective" << std::endl;);
|
TRACE("injectivity", tout << "Marking " << f->get_name() << " as injective" << std::endl;);
|
||||||
inj_map.insert(f, g);
|
inj_map.insert(f, g);
|
||||||
// TODO: Record that g is f's pseudoinverse
|
// TODO: Record that g is f's pseudoinverse
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
void updt_params(params_ref const & p) {}
|
void updt_params(params_ref const & p) {}
|
||||||
};
|
};
|
||||||
|
|
||||||
struct rewriter_eq_cfg : public default_rewriter_cfg {
|
struct rewriter_eq_cfg : public default_rewriter_cfg {
|
||||||
ast_manager & m_manager;
|
ast_manager & m_manager;
|
||||||
InjHelper & inj_map;
|
InjHelper & inj_map;
|
||||||
// expr_ref_vector m_out;
|
// expr_ref_vector m_out;
|
||||||
// sort_ref_vector m_bindings;
|
// sort_ref_vector m_bindings;
|
||||||
|
|
||||||
ast_manager & m() const { return m_manager; }
|
ast_manager & m() const { return m_manager; }
|
||||||
|
|
||||||
rewriter_eq_cfg(ast_manager & m, InjHelper & map, params_ref const & p) : m_manager(m), inj_map(map) {
|
rewriter_eq_cfg(ast_manager & m, InjHelper & map, params_ref const & p) : m_manager(m), inj_map(map) {
|
||||||
}
|
}
|
||||||
|
|
||||||
~rewriter_eq_cfg() {
|
~rewriter_eq_cfg() {
|
||||||
}
|
}
|
||||||
|
|
||||||
void cleanup_buffers() {
|
void cleanup_buffers() {
|
||||||
// m_out.finalize();
|
// m_out.finalize();
|
||||||
}
|
}
|
||||||
|
|
||||||
void reset() {
|
void reset() {
|
||||||
}
|
}
|
||||||
|
|
||||||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
||||||
if(num != 2)
|
if(num != 2)
|
||||||
return BR_FAILED;
|
return BR_FAILED;
|
||||||
|
|
||||||
if (!m().is_eq(f))
|
if (!m().is_eq(f))
|
||||||
return BR_FAILED;
|
return BR_FAILED;
|
||||||
|
|
||||||
// We are rewriting (= a b)
|
// We are rewriting (= a b)
|
||||||
if (!is_app(args[0]) || !is_app(args[1]))
|
if (!is_app(args[0]) || !is_app(args[1]))
|
||||||
return BR_FAILED;
|
return BR_FAILED;
|
||||||
|
|
||||||
const app* const a = to_app(args[0]);
|
const app* const a = to_app(args[0]);
|
||||||
const app* const b = to_app(args[1]);
|
const app* const b = to_app(args[1]);
|
||||||
|
|
||||||
// a and b are applications of the same function
|
// a and b are applications of the same function
|
||||||
if (a->get_decl() != b->get_decl())
|
if (a->get_decl() != b->get_decl())
|
||||||
return BR_FAILED;
|
return BR_FAILED;
|
||||||
|
|
||||||
// Maybe TODO: Generalize to multi-parameter functions ?
|
// Maybe TODO: Generalize to multi-parameter functions ?
|
||||||
if (a->get_num_args() != 1 || b->get_num_args() != 1)
|
if (a->get_num_args() != 1 || b->get_num_args() != 1)
|
||||||
return BR_FAILED;
|
return BR_FAILED;
|
||||||
|
|
||||||
if (!inj_map.contains(a->get_decl()))
|
if (!inj_map.contains(a->get_decl()))
|
||||||
return BR_FAILED;
|
return BR_FAILED;
|
||||||
|
|
||||||
SASSERT(m().get_sort(a->get_arg(0)) == m().get_sort(b->get_arg(0)));
|
SASSERT(m().get_sort(a->get_arg(0)) == m().get_sort(b->get_arg(0)));
|
||||||
TRACE("injectivity", tout << "Rewriting (= " << mk_ismt2_pp(args[0], m()) <<
|
TRACE("injectivity", tout << "Rewriting (= " << mk_ismt2_pp(args[0], m()) <<
|
||||||
" " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;);
|
" " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;);
|
||||||
result = m().mk_eq(a->get_arg(0), b->get_arg(0));
|
result = m().mk_eq(a->get_arg(0), b->get_arg(0));
|
||||||
result_pr = nullptr;
|
result_pr = nullptr;
|
||||||
return BR_DONE;
|
return BR_DONE;
|
||||||
}
|
}
|
||||||
|
|
||||||
};
|
};
|
||||||
|
|
||||||
struct rewriter_eq : public rewriter_tpl<rewriter_eq_cfg> {
|
struct rewriter_eq : public rewriter_tpl<rewriter_eq_cfg> {
|
||||||
rewriter_eq_cfg m_cfg;
|
rewriter_eq_cfg m_cfg;
|
||||||
rewriter_eq(ast_manager & m, InjHelper & map, params_ref const & p) :
|
rewriter_eq(ast_manager & m, InjHelper & map, params_ref const & p) :
|
||||||
rewriter_tpl<rewriter_eq_cfg>(m, m.proofs_enabled(), m_cfg),
|
rewriter_tpl<rewriter_eq_cfg>(m, m.proofs_enabled(), m_cfg),
|
||||||
m_cfg(m, map, p) {
|
m_cfg(m, map, p) {
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
struct rewriter_inverse { };
|
struct rewriter_inverse { };
|
||||||
|
|
||||||
finder * m_finder;
|
finder * m_finder;
|
||||||
rewriter_eq * m_eq;
|
rewriter_eq * m_eq;
|
||||||
InjHelper * m_map;
|
InjHelper * m_map;
|
||||||
// rewriter_inverse * m_inverse;
|
// rewriter_inverse * m_inverse;
|
||||||
|
|
||||||
params_ref m_params;
|
params_ref m_params;
|
||||||
ast_manager & m_manager;
|
ast_manager & m_manager;
|
||||||
|
|
||||||
public:
|
public:
|
||||||
injectivity_tactic(ast_manager & m, params_ref const & p):
|
injectivity_tactic(ast_manager & m, params_ref const & p):
|
||||||
m_params(p),
|
m_params(p),
|
||||||
m_manager(m) {
|
m_manager(m) {
|
||||||
TRACE("injectivity", tout << "constructed new tactic" << std::endl;);
|
TRACE("injectivity", tout << "constructed new tactic" << std::endl;);
|
||||||
m_map = alloc(InjHelper, m);
|
m_map = alloc(InjHelper, m);
|
||||||
m_finder = alloc(finder, m, *m_map, p);
|
m_finder = alloc(finder, m, *m_map, p);
|
||||||
m_eq = alloc(rewriter_eq, m, *m_map, p);
|
m_eq = alloc(rewriter_eq, m, *m_map, p);
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual tactic * translate(ast_manager & m) {
|
virtual tactic * translate(ast_manager & m) {
|
||||||
return alloc(injectivity_tactic, m, m_params);
|
return alloc(injectivity_tactic, m, m_params);
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual ~injectivity_tactic() {
|
virtual ~injectivity_tactic() {
|
||||||
dealloc(m_finder);
|
dealloc(m_finder);
|
||||||
dealloc(m_eq);
|
dealloc(m_eq);
|
||||||
dealloc(m_map);
|
dealloc(m_map);
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual void updt_params(params_ref const & p) {
|
virtual void updt_params(params_ref const & p) {
|
||||||
|
|
@ -269,30 +269,30 @@ public:
|
||||||
insert_max_memory(r);
|
insert_max_memory(r);
|
||||||
insert_produce_models(r);
|
insert_produce_models(r);
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual void operator()(goal_ref const & g,
|
virtual void operator()(goal_ref const & g,
|
||||||
goal_ref_buffer & result,
|
goal_ref_buffer & result,
|
||||||
model_converter_ref & mc,
|
model_converter_ref & mc,
|
||||||
proof_converter_ref & pc,
|
proof_converter_ref & pc,
|
||||||
expr_dependency_ref & core) {
|
expr_dependency_ref & core) {
|
||||||
(*m_finder)(g, result, mc, pc, core);
|
(*m_finder)(g, result, mc, pc, core);
|
||||||
|
|
||||||
for (unsigned i = 0; i < g->size(); ++i) {
|
for (unsigned i = 0; i < g->size(); ++i) {
|
||||||
expr* curr = g->form(i);
|
expr* curr = g->form(i);
|
||||||
expr_ref rw(m_manager);
|
expr_ref rw(m_manager);
|
||||||
proof_ref pr(m_manager);
|
proof_ref pr(m_manager);
|
||||||
(*m_eq)(curr, rw, pr);
|
(*m_eq)(curr, rw, pr);
|
||||||
g->update(i, rw, pr, g->dep(i));
|
g->update(i, rw, pr, g->dep(i));
|
||||||
}
|
}
|
||||||
result.push_back(g.get());
|
result.push_back(g.get());
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual void cleanup() {
|
virtual void cleanup() {
|
||||||
InjHelper * m = alloc(InjHelper, m_manager);
|
InjHelper * m = alloc(InjHelper, m_manager);
|
||||||
finder * f = alloc(finder, m_manager, *m, m_params);
|
finder * f = alloc(finder, m_manager, *m, m_params);
|
||||||
rewriter_eq * r = alloc(rewriter_eq, m_manager, *m, m_params);
|
rewriter_eq * r = alloc(rewriter_eq, m_manager, *m, m_params);
|
||||||
std::swap(m, m_map), std::swap(f, m_finder), std::swap(r, m_eq);
|
std::swap(m, m_map), std::swap(f, m_finder), std::swap(r, m_eq);
|
||||||
dealloc(m), dealloc(f), dealloc(r);
|
dealloc(m), dealloc(f), dealloc(r);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue