From cb87d47f08281f3e2cefac07d4e4ea80e97e21e9 Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Tue, 22 Aug 2017 17:03:20 +0000 Subject: [PATCH 1/7] obj_hashtable: Constify --- src/util/obj_hashtable.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 9c3473e3d..189d1e1a0 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -134,7 +134,7 @@ public: return m_table.end(); } - void insert(Key * k, Value const & v) { + void insert(Key * const k, Value const & v) { m_table.insert(key_data(k, v)); } @@ -150,7 +150,7 @@ public: return m_table.find_core(key_data(k)); } - bool find(Key * k, Value & v) const { + bool find(Key * const k, Value & v) const { obj_map_entry * e = find_core(k); if (e) { v = e->get_data().m_value; From 4cb7f72509b6a590b1f706f0f7be09e76ac6e1a5 Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Thu, 17 Aug 2017 16:43:25 +0000 Subject: [PATCH 2/7] First version of the inj. tactic --- scripts/mk_project.py | 10 +- src/tactic/core/injectivity_tactic.cpp | 305 +++++++++++++++++++++++++ src/tactic/core/injectivity_tactic.h | 32 +++ 3 files changed, 342 insertions(+), 5 deletions(-) create mode 100644 src/tactic/core/injectivity_tactic.cpp create mode 100644 src/tactic/core/injectivity_tactic.h diff --git a/scripts/mk_project.py b/scripts/mk_project.py index b40205445..64dd93faa 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -23,6 +23,10 @@ def init_project_def(): add_lib('subpaving', ['interval'], 'math/subpaving') add_lib('ast', ['util', 'polynomial']) add_lib('rewriter', ['ast', 'polynomial', 'automata'], 'ast/rewriter') + # Simplifier module will be deleted in the future. + # It has been replaced with rewriter module. + add_lib('simplifier', ['rewriter'], 'ast/simplifier') + add_lib('macros', ['simplifier'], 'ast/macros') add_lib('normal_forms', ['rewriter'], 'ast/normal_forms') add_lib('model', ['rewriter']) add_lib('tactic', ['ast', 'model']) @@ -30,7 +34,7 @@ def init_project_def(): add_lib('parser_util', ['ast'], 'parsers/util') add_lib('grobner', ['ast'], 'math/grobner') add_lib('euclid', ['util'], 'math/euclid') - add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core') + add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter'], 'tactic/core') add_lib('sat_tactic', ['tactic', 'sat'], 'sat/tactic') add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith') add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic') @@ -43,11 +47,7 @@ def init_project_def(): add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds') add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2') add_lib('proof_checker', ['rewriter'], 'ast/proof_checker') - # Simplifier module will be deleted in the future. - # It has been replaced with rewriter module. - add_lib('simplifier', ['rewriter'], 'ast/simplifier') add_lib('fpa', ['ast', 'util', 'simplifier', 'model'], 'ast/fpa') - add_lib('macros', ['simplifier'], 'ast/macros') add_lib('pattern', ['normal_forms', 'smt2parser', 'simplifier'], 'ast/pattern') add_lib('bit_blaster', ['rewriter', 'simplifier'], 'ast/rewriter/bit_blaster') add_lib('smt_params', ['ast', 'simplifier', 'pattern', 'bit_blaster'], 'smt/params') diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp new file mode 100644 index 000000000..d8b5e6acf --- /dev/null +++ b/src/tactic/core/injectivity_tactic.cpp @@ -0,0 +1,305 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + injectivity_tactic.cpp + +Abstract: + + Injectivity tactics + - Discover axioms of the form `forall x. (= (g (f x)) x` + Mark `f` as injective + - Rewrite (sub)terms of the form `(= (f x) (f y))` to `(= x y)` whenever `f` is injective. + +Author: + + Nicolas Braud-Santoni (t-nibrau) 2017-08-10 + +Notes: + +--*/ +#include +#include +#include "tactic/tactical.h" +#include "ast/rewriter/rewriter_def.h" +#include "tactic/core/injectivity_tactic.h" +#include "util/dec_ref_util.h" + + +class injectivity_tactic : public tactic { + + struct InjHelper : public obj_map*> { + ast_manager & m_manager; + + void insert(func_decl* const f, func_decl* const g) { + obj_hashtable *m; + if (! obj_map::find(f, m)) { + m_manager.inc_ref(f); + m = alloc(obj_hashtable); // TODO: Check we don't leak memory + obj_map::insert(f, m); + } + if (!m->contains(g)) { + m_manager.inc_ref(g); + m->insert(g); + } + } + + bool find(func_decl* const f, func_decl* const g) const { + obj_hashtable *m; + if(! obj_map::find(f, m)) + return false; + + return m->contains(g); + } + + InjHelper(ast_manager& m) : obj_map*>(), m_manager(m) {} + ~InjHelper() { + for(auto m : *this) { + for (func_decl* f : *m.get_value()) + m_manager.dec_ref(f); + + m_manager.dec_ref(m.m_key); + dealloc(m.m_value); + } + } + + }; + + struct finder { + ast_manager & m_manager; + InjHelper & inj_map; + + finder(ast_manager & m, InjHelper & map, params_ref const & p) : + m_manager(m), + inj_map(map) { + updt_params(p); + } + + ast_manager & m() const { return m_manager; } + + bool is_axiom(expr* n, func_decl* &f, func_decl* &g) { + if (!is_quantifier(n)) + return false; + + quantifier* const q = to_quantifier(n); + if (!q->is_forall() || q->get_num_decls() != 1) + return false; + + const expr * const body = q->get_expr(); + + // n ~= forall x. body + + if (!m().is_eq(body)) + return false; + + const app * const body_a = to_app(body); + if (body_a->get_num_args() != 2) + return false; + + const expr* a = body_a->get_arg(0); + const expr* b = body_a->get_arg(1); + + // n ~= forall x. (= a b) + + if (is_app(a) && is_var(b)) { + // Do nothing + } + else if (is_app(b) && is_var(a)) { + std::swap(a, b); + } + else + return false; + + const app* const a_app = to_app(a); + const var* const b_var = to_var(b); + + if (b_var->get_idx() != 0) // idx is the De Bruijn's index + return false; + + if (a_app->get_num_args() != 1) + return false; + + g = a_app->get_decl(); + const expr* const a_body = a_app->get_arg(0); + + // n ~= forall x. (= (g a_body) x) + + if (!is_app(a_body)) + return false; + const app* const a_body_app = to_app(a_body); + if (a_body_app->get_num_args() != 1) // Maybe TODO: support multi-argument functions + return false; + + f = a_body_app->get_decl(); + 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) + + return true; + } + + void operator()(goal_ref const & goal, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + SASSERT(goal->is_well_sorted()); + mc = 0; pc = 0; core = 0; + tactic_report report("injectivity", *goal); + fail_if_unsat_core_generation("injectivity", goal); // TODO: Support UNSAT cores + fail_if_proof_generation("injectivity", goal); + + for (unsigned i = 0; i < goal->size(); ++i) { + func_decl *f, *g; + if (!is_axiom(goal->form(i), f, g)) continue; + TRACE("injectivity_finder", tout << "Marking " << f->get_name() << " as injective" << std::endl;); + inj_map.insert(f, g); + // TODO: Record that g is f's pseudoinverse + } + } + + void updt_params(params_ref const & p) {} + }; + + struct rewriter_eq_cfg : public default_rewriter_cfg { + ast_manager & m_manager; + InjHelper & inj_map; +// expr_ref_vector m_out; +// sort_ref_vector m_bindings; + + 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() { + } + + void cleanup_buffers() { +// m_out.finalize(); + } + + void reset() { + } + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + if(num != 2) + return BR_FAILED; + + if (!m().is_eq(f)) + return BR_FAILED; + + // We are rewriting (= a b) + if (!is_app(args[0]) || !is_app(args[1])) + return BR_FAILED; + + const app* const a = to_app(args[0]); + const app* const b = to_app(args[1]); + + // a and b are applications of the same function + if (a->get_decl() != b->get_decl()) + return BR_FAILED; + + // Maybe TODO: Generalize to multi-parameter functions ? + if (a->get_num_args() != 1 || b->get_num_args() != 1) + return BR_FAILED; + + if (!inj_map.contains(a->get_decl())) + return BR_FAILED; + + SASSERT(m().get_sort(a->get_arg(0)) == m().get_sort(b->get_arg(0))); + TRACE("injectivity_eq", tout << "Rewriting (= " << mk_ismt2_pp(args[0], m()) << + " " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;); + result = m().mk_eq(a->get_arg(0), b->get_arg(0)); + result_pr = nullptr; + return BR_DONE; + } + + }; + + struct rewriter_eq : public rewriter_tpl { + rewriter_eq_cfg m_cfg; + rewriter_eq(ast_manager & m, InjHelper & map, params_ref const & p) : + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, map, p) { + } + }; + + struct rewriter_inverse { }; + + finder * m_finder; + rewriter_eq * m_eq; + InjHelper * m_map; +// rewriter_inverse * m_inverse; + + params_ref m_params; + ast_manager & m_manager; + +public: + injectivity_tactic(ast_manager & m, params_ref const & p): + m_params(p), + m_manager(m) { + TRACE("injectivity", tout << "constructed new tactic" << std::endl;); + m_map = alloc(InjHelper, m); + m_finder = alloc(finder, m, *m_map, p); + m_eq = alloc(rewriter_eq, m, *m_map, p); + } + + virtual tactic * translate(ast_manager & m) { + return alloc(injectivity_tactic, m, m_params); + } + + virtual ~injectivity_tactic() { + dealloc(m_finder); + dealloc(m_eq); + dealloc(m_map); + } + + virtual void updt_params(params_ref const & p) { + m_params = p; + m_finder->updt_params(p); + } + + virtual void collect_param_descrs(param_descrs & r) { + insert_max_memory(r); + insert_produce_models(r); + r.insert("elim_and", CPK_BOOL, "(default: false) eliminate conjunctions during (internal) calls to the simplifier."); + } + + virtual void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + std::cerr << "injectivity finder: " << m_finder << std::endl; + (*m_finder)(g, result, mc, pc, core); + + for (unsigned i = 0; i < g->size(); ++i) { + std::cerr << "injectivity rewrite " << i << std::endl; + expr* curr = g->form(i); + expr_ref rw(m_manager); + proof_ref pr(m_manager); + (*m_eq)(curr, rw, pr); + g->update(i, rw, pr, g->dep(i)); + } + } + + virtual void cleanup() { + InjHelper * m = alloc(InjHelper, m_manager); + finder * f = alloc(finder, 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); + dealloc(m), dealloc(f), dealloc(r); + } + + +}; + +tactic * mk_injectivity_tactic(ast_manager & m, params_ref const & p) { + return alloc(injectivity_tactic, m, p); +} diff --git a/src/tactic/core/injectivity_tactic.h b/src/tactic/core/injectivity_tactic.h new file mode 100644 index 000000000..447357912 --- /dev/null +++ b/src/tactic/core/injectivity_tactic.h @@ -0,0 +1,32 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + injectivity_tactic.h + +Abstract: + + Injectivity tactics + +Author: + + Nicolas Braud-Santoni (t-nibrau) 2017-08-10 + +Notes: + +--*/ +#ifndef INJECTIVITY_TACTIC_H_ +#define INJECTIVITY_TACTIC_H_ + +#include "util/params.h" +class ast_manager; +class tactic; + +tactic * mk_injectivity_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("injectivity", "Identifies and applies injectivity axioms.", "mk_injectivity_tactic(m, p)") +*/ + +#endif From c0b6d00e8aa9a19d2cca474aaad9d0fd37af408e Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Tue, 22 Aug 2017 18:09:38 +0000 Subject: [PATCH 3/7] Update debug output --- src/tactic/core/injectivity_tactic.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp index d8b5e6acf..75685c891 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -157,7 +157,7 @@ class injectivity_tactic : public tactic { for (unsigned i = 0; i < goal->size(); ++i) { func_decl *f, *g; if (!is_axiom(goal->form(i), f, g)) continue; - TRACE("injectivity_finder", 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); // TODO: Record that g is f's pseudoinverse } @@ -213,7 +213,7 @@ class injectivity_tactic : public tactic { return BR_FAILED; SASSERT(m().get_sort(a->get_arg(0)) == m().get_sort(b->get_arg(0))); - TRACE("injectivity_eq", 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;); result = m().mk_eq(a->get_arg(0), b->get_arg(0)); result_pr = nullptr; @@ -276,11 +276,9 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - std::cerr << "injectivity finder: " << m_finder << std::endl; (*m_finder)(g, result, mc, pc, core); for (unsigned i = 0; i < g->size(); ++i) { - std::cerr << "injectivity rewrite " << i << std::endl; expr* curr = g->form(i); expr_ref rw(m_manager); proof_ref pr(m_manager); From 33dd168195cf561786163adce7e471f82f011aeb Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Tue, 22 Aug 2017 18:09:57 +0000 Subject: [PATCH 4/7] Remove unnecessary parameter --- src/tactic/core/injectivity_tactic.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp index 75685c891..4dc3fe5d5 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -268,7 +268,6 @@ public: virtual void collect_param_descrs(param_descrs & r) { insert_max_memory(r); insert_produce_models(r); - r.insert("elim_and", CPK_BOOL, "(default: false) eliminate conjunctions during (internal) calls to the simplifier."); } virtual void operator()(goal_ref const & g, From 27fd879b8ceb5aee860ae1c7ffa3e1afe2727159 Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Tue, 22 Aug 2017 18:44:34 +0000 Subject: [PATCH 5/7] injectivity: Fixup rewriter --- src/tactic/core/injectivity_tactic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp index 4dc3fe5d5..95e380982 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -284,7 +284,8 @@ public: (*m_eq)(curr, rw, pr); g->update(i, rw, pr, g->dep(i)); } - } + result.push_back(g.get()); + } virtual void cleanup() { InjHelper * m = alloc(InjHelper, m_manager); From ae9ace232143af631af831a23d48c9f7fbd471c1 Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Wed, 23 Aug 2017 10:25:33 +0000 Subject: [PATCH 6/7] injectivity: Cleanup whitespace --- src/tactic/core/injectivity_tactic.cpp | 340 ++++++++++++------------- 1 file changed, 170 insertions(+), 170 deletions(-) diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp index 95e380982..7d90a2155 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -29,120 +29,120 @@ Notes: class injectivity_tactic : public tactic { - struct InjHelper : public obj_map*> { - ast_manager & m_manager; + struct InjHelper : public obj_map*> { + ast_manager & m_manager; - void insert(func_decl* const f, func_decl* const g) { - obj_hashtable *m; - if (! obj_map::find(f, m)) { - m_manager.inc_ref(f); - m = alloc(obj_hashtable); // TODO: Check we don't leak memory - obj_map::insert(f, m); - } - if (!m->contains(g)) { - m_manager.inc_ref(g); - m->insert(g); - } - } + void insert(func_decl* const f, func_decl* const g) { + obj_hashtable *m; + if (! obj_map::find(f, m)) { + m_manager.inc_ref(f); + m = alloc(obj_hashtable); // TODO: Check we don't leak memory + obj_map::insert(f, m); + } + if (!m->contains(g)) { + m_manager.inc_ref(g); + m->insert(g); + } + } - bool find(func_decl* const f, func_decl* const g) const { - obj_hashtable *m; - if(! obj_map::find(f, m)) - return false; + bool find(func_decl* const f, func_decl* const g) const { + obj_hashtable *m; + if(! obj_map::find(f, m)) + return false; - return m->contains(g); - } + return m->contains(g); + } - InjHelper(ast_manager& m) : obj_map*>(), m_manager(m) {} - ~InjHelper() { - for(auto m : *this) { - for (func_decl* f : *m.get_value()) - m_manager.dec_ref(f); + InjHelper(ast_manager& m) : obj_map*>(), m_manager(m) {} + ~InjHelper() { + for(auto m : *this) { + for (func_decl* f : *m.get_value()) + m_manager.dec_ref(f); - m_manager.dec_ref(m.m_key); - dealloc(m.m_value); - } - } + m_manager.dec_ref(m.m_key); + dealloc(m.m_value); + } + } - }; + }; struct finder { 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), - inj_map(map) { + inj_map(map) { updt_params(p); } - + ast_manager & m() const { return m_manager; } - bool is_axiom(expr* n, func_decl* &f, func_decl* &g) { - if (!is_quantifier(n)) - return false; + bool is_axiom(expr* n, func_decl* &f, func_decl* &g) { + if (!is_quantifier(n)) + return false; - quantifier* const q = to_quantifier(n); - if (!q->is_forall() || q->get_num_decls() != 1) - return false; + quantifier* const q = to_quantifier(n); + if (!q->is_forall() || q->get_num_decls() != 1) + 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)) - return false; + if (!m().is_eq(body)) + return false; - const app * const body_a = to_app(body); - if (body_a->get_num_args() != 2) - return false; + const app * const body_a = to_app(body); + if (body_a->get_num_args() != 2) + return false; - const expr* a = body_a->get_arg(0); - const expr* b = body_a->get_arg(1); + const expr* a = body_a->get_arg(0); + 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)) { - // Do nothing - } - else if (is_app(b) && is_var(a)) { - std::swap(a, b); - } - else - return false; + if (is_app(a) && is_var(b)) { + // Do nothing + } + else if (is_app(b) && is_var(a)) { + std::swap(a, b); + } + else + return false; - const app* const a_app = to_app(a); - const var* const b_var = to_var(b); + const app* const a_app = to_app(a); + const var* const b_var = to_var(b); - if (b_var->get_idx() != 0) // idx is the De Bruijn's index - return false; + if (b_var->get_idx() != 0) // idx is the De Bruijn's index + return false; - if (a_app->get_num_args() != 1) - return false; + if (a_app->get_num_args() != 1) + return false; - g = a_app->get_decl(); - const expr* const a_body = a_app->get_arg(0); + g = a_app->get_decl(); + 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)) - return false; - const app* const a_body_app = to_app(a_body); - if (a_body_app->get_num_args() != 1) // Maybe TODO: support multi-argument functions - return false; + if (!is_app(a_body)) + return false; + const app* const a_body_app = to_app(a_body); + if (a_body_app->get_num_args() != 1) // Maybe TODO: support multi-argument functions + return false; - f = a_body_app->get_decl(); - 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; + f = a_body_app->get_decl(); + const expr* const a_body_body = a_body_app->get_arg(0); - // 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, goal_ref_buffer & result, model_converter_ref & mc, @@ -152,112 +152,112 @@ class injectivity_tactic : public tactic { mc = 0; pc = 0; core = 0; tactic_report report("injectivity", *goal); 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) { - func_decl *f, *g; - if (!is_axiom(goal->form(i), f, g)) continue; - TRACE("injectivity", tout << "Marking " << f->get_name() << " as injective" << std::endl;); - inj_map.insert(f, g); - // TODO: Record that g is f's pseudoinverse - } + for (unsigned i = 0; i < goal->size(); ++i) { + func_decl *f, *g; + if (!is_axiom(goal->form(i), f, g)) continue; + TRACE("injectivity", tout << "Marking " << f->get_name() << " as injective" << std::endl;); + inj_map.insert(f, g); + // TODO: Record that g is f's pseudoinverse + } } void updt_params(params_ref const & p) {} }; - struct rewriter_eq_cfg : public default_rewriter_cfg { - ast_manager & m_manager; - InjHelper & inj_map; -// expr_ref_vector m_out; -// sort_ref_vector m_bindings; + struct rewriter_eq_cfg : public default_rewriter_cfg { + ast_manager & m_manager; + InjHelper & inj_map; +// expr_ref_vector m_out; +// 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() { -// m_out.finalize(); - } + void cleanup_buffers() { +// 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) { - if(num != 2) - return BR_FAILED; + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + if(num != 2) + return BR_FAILED; - if (!m().is_eq(f)) - return BR_FAILED; + if (!m().is_eq(f)) + return BR_FAILED; - // We are rewriting (= a b) - if (!is_app(args[0]) || !is_app(args[1])) - return BR_FAILED; + // We are rewriting (= a b) + if (!is_app(args[0]) || !is_app(args[1])) + return BR_FAILED; - const app* const a = to_app(args[0]); - const app* const b = to_app(args[1]); + const app* const a = to_app(args[0]); + const app* const b = to_app(args[1]); - // a and b are applications of the same function - if (a->get_decl() != b->get_decl()) - return BR_FAILED; + // a and b are applications of the same function + if (a->get_decl() != b->get_decl()) + return BR_FAILED; - // Maybe TODO: Generalize to multi-parameter functions ? - if (a->get_num_args() != 1 || b->get_num_args() != 1) - return BR_FAILED; + // Maybe TODO: Generalize to multi-parameter functions ? + if (a->get_num_args() != 1 || b->get_num_args() != 1) + return BR_FAILED; - if (!inj_map.contains(a->get_decl())) - return BR_FAILED; + if (!inj_map.contains(a->get_decl())) + return BR_FAILED; - 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()) << - " " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;); - result = m().mk_eq(a->get_arg(0), b->get_arg(0)); - result_pr = nullptr; - return BR_DONE; - } + 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()) << + " " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;); + result = m().mk_eq(a->get_arg(0), b->get_arg(0)); + result_pr = nullptr; + return BR_DONE; + } - }; + }; - struct rewriter_eq : public rewriter_tpl { - rewriter_eq_cfg m_cfg; - rewriter_eq(ast_manager & m, InjHelper & map, params_ref const & p) : - rewriter_tpl(m, m.proofs_enabled(), m_cfg), - m_cfg(m, map, p) { - } - }; + struct rewriter_eq : public rewriter_tpl { + rewriter_eq_cfg m_cfg; + rewriter_eq(ast_manager & m, InjHelper & map, params_ref const & p) : + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, map, p) { + } + }; - struct rewriter_inverse { }; + struct rewriter_inverse { }; finder * m_finder; - rewriter_eq * m_eq; - InjHelper * m_map; -// rewriter_inverse * m_inverse; + rewriter_eq * m_eq; + InjHelper * m_map; +// rewriter_inverse * m_inverse; params_ref m_params; - ast_manager & m_manager; + ast_manager & m_manager; public: injectivity_tactic(ast_manager & m, params_ref const & p): m_params(p), - m_manager(m) { - TRACE("injectivity", tout << "constructed new tactic" << std::endl;); - m_map = alloc(InjHelper, m); + m_manager(m) { + TRACE("injectivity", tout << "constructed new tactic" << std::endl;); + m_map = alloc(InjHelper, m); 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) { return alloc(injectivity_tactic, m, m_params); } - + virtual ~injectivity_tactic() { dealloc(m_finder); - dealloc(m_eq); - dealloc(m_map); + dealloc(m_eq); + dealloc(m_map); } virtual void updt_params(params_ref const & p) { @@ -269,30 +269,30 @@ public: insert_max_memory(r); insert_produce_models(r); } - - virtual void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, + + virtual void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { (*m_finder)(g, result, mc, pc, core); - - for (unsigned i = 0; i < g->size(); ++i) { - expr* curr = g->form(i); - expr_ref rw(m_manager); - proof_ref pr(m_manager); - (*m_eq)(curr, rw, pr); - g->update(i, rw, pr, g->dep(i)); - } - result.push_back(g.get()); - } - + + for (unsigned i = 0; i < g->size(); ++i) { + expr* curr = g->form(i); + expr_ref rw(m_manager); + proof_ref pr(m_manager); + (*m_eq)(curr, rw, pr); + g->update(i, rw, pr, g->dep(i)); + } + result.push_back(g.get()); + } + virtual void cleanup() { - InjHelper * m = alloc(InjHelper, m_manager); - finder * f = alloc(finder, 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); - dealloc(m), dealloc(f), dealloc(r); + InjHelper * m = alloc(InjHelper, m_manager); + finder * f = alloc(finder, 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); + dealloc(m), dealloc(f), dealloc(r); } From b877c962caa73ae29be01a4dd28c7a82ac7600d3 Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Wed, 23 Aug 2017 10:27:55 +0000 Subject: [PATCH 7/7] injectivity: Add tactic to CMake-based builds --- src/tactic/core/CMakeLists.txt | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index 1f766bd47..f192b4fa6 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -9,6 +9,7 @@ z3_add_component(core_tactics distribute_forall_tactic.cpp elim_term_ite_tactic.cpp elim_uncnstr_tactic.cpp + injectivity_tactic.cpp nnf_tactic.cpp occf_tactic.cpp pb_preprocess_tactic.cpp @@ -22,6 +23,7 @@ z3_add_component(core_tactics collect_occs.cpp COMPONENT_DEPENDENCIES normal_forms + rewriter tactic TACTIC_HEADERS blast_term_ite_tactic.h @@ -32,6 +34,7 @@ z3_add_component(core_tactics distribute_forall_tactic.h elim_term_ite_tactic.h elim_uncnstr_tactic.h + injectivity_tactic.h nnf_tactic.h occf_tactic.h pb_preprocess_tactic.h