From 7a6823aef1f2ad9266fdc7fd2930c7bf3c683096 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Mar 2019 10:07:50 -0700 Subject: [PATCH] add special relations tactic Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 1 - src/ast/rewriter/CMakeLists.txt | 1 + src/ast/rewriter/func_decl_replace.cpp | 2 +- src/ast/special_relations_decl_plugin.h | 15 ++-- src/tactic/core/CMakeLists.txt | 2 + src/tactic/core/special_relations_tactic.cpp | 81 +++++++++++++++++--- src/tactic/core/special_relations_tactic.h | 11 ++- 7 files changed, 92 insertions(+), 21 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 7ba33a61d..e1fe76175 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1104,7 +1104,6 @@ typedef enum { // Special relations Z3_OP_SPECIAL_RELATION_LO, Z3_OP_SPECIAL_RELATION_PO, - Z3_OP_SPECIAL_RELATION_PO_AO, Z3_OP_SPECIAL_RELATION_PLO, Z3_OP_SPECIAL_RELATION_TO, diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index 9f98ff0ed..d506c75b3 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -19,6 +19,7 @@ z3_add_component(rewriter factor_equivs.cpp factor_rewriter.cpp fpa_rewriter.cpp + func_decl_replace.cpp hoist_rewriter.cpp inj_axiom.cpp label_rewriter.cpp diff --git a/src/ast/rewriter/func_decl_replace.cpp b/src/ast/rewriter/func_decl_replace.cpp index 6e64dd568..dcde9044f 100644 --- a/src/ast/rewriter/func_decl_replace.cpp +++ b/src/ast/rewriter/func_decl_replace.cpp @@ -86,7 +86,7 @@ expr_ref func_decl_replace::operator()(expr* e) { } } } - return expr_ref(cache.find(e), m); + return expr_ref(m_cache.find(e), m); } void func_decl_replace::reset() { diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h index e8260e154..5926057f5 100644 --- a/src/ast/special_relations_decl_plugin.h +++ b/src/ast/special_relations_decl_plugin.h @@ -26,7 +26,6 @@ Revision History: enum special_relations_op_kind { OP_SPECIAL_RELATION_LO, OP_SPECIAL_RELATION_PO, - OP_SPECIAL_RELATION_PO_AO, OP_SPECIAL_RELATION_PLO, OP_SPECIAL_RELATION_TO, LAST_SPECIAL_RELATIONS_OP @@ -35,7 +34,6 @@ enum special_relations_op_kind { class special_relations_decl_plugin : public decl_plugin { symbol m_lo; symbol m_po; - symbol m_po_ao; symbol m_plo; symbol m_to; public: @@ -56,15 +54,17 @@ public: }; enum sr_property { + sr_none = 0x00, sr_transitive = 0x01, // Rxy & Ryz -> Rxz sr_reflexive = 0x02, // Rxx sr_antisymmetric = 0x04, // Rxy & Ryx -> x = y sr_lefttree = 0x08, // Ryx & Rzx -> Ryz | Rzy sr_righttree = 0x10, // Rxy & Rxz -> Ryx | Rzy + sr_total = 0x20, // Rxy | Ryx sr_po = 0x01 | 0x02 | 0x04, // partial order - sr_lo = 0x01 | 0x02 | 0x04 | 0x08 | 0x10, // linear order - sr_plo = 0x01 | 0x02 | 0x04 | 0x20, // piecewise linear order sr_to = 0x01 | 0x02 | 0x04 | 0x10, // right-tree + sr_plo = 0x01 | 0x02 | 0x04 | 0x08 | 0x10, // piecewise linear order + sr_lo = 0x01 | 0x02 | 0x04 | 0x20, // linear order }; class special_relations_util { @@ -78,15 +78,18 @@ public: sr_property get_property(func_decl* f) const; sr_property get_property(app* e) const { return get_property(e->get_decl()); } + func_decl* mk_to_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_TO, 1, &p, 2, f->get_domain(), f->get_range()); } + func_decl* mk_po_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_PO, 1, &p, 2, f->get_domain(), f->get_range()); } + func_decl* mk_plo_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_PLO, 1, &p, 2, f->get_domain(), f->get_range()); } + func_decl* mk_lo_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_LO, 1, &p, 2, f->get_domain(), f->get_range()); } + bool is_lo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_LO); } bool is_po(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO); } - bool is_po_ao(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO_AO); } bool is_plo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PLO); } bool is_to(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TO); } app * mk_lo (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_LO, arg1, arg2); } app * mk_po (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO, arg1, arg2); } - app * mk_po_ao (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO_AO, arg1, arg2); } app * mk_plo(expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PLO, arg1, arg2); } app * mk_to (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_TO, arg1, arg2); } diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index 44284b625..a247c7b20 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -19,6 +19,7 @@ z3_add_component(core_tactics reduce_invertible_tactic.cpp simplify_tactic.cpp solve_eqs_tactic.cpp + special_relations_tactic.cpp split_clause_tactic.cpp symmetry_reduce_tactic.cpp tseitin_cnf_tactic.cpp @@ -46,6 +47,7 @@ z3_add_component(core_tactics reduce_invertible_tactic.h simplify_tactic.h solve_eqs_tactic.h + special_relations_tactic.h split_clause_tactic.h symmetry_reduce_tactic.h tseitin_cnf_tactic.h diff --git a/src/tactic/core/special_relations_tactic.cpp b/src/tactic/core/special_relations_tactic.cpp index cb0533e81..f256bdbef 100644 --- a/src/tactic/core/special_relations_tactic.cpp +++ b/src/tactic/core/special_relations_tactic.cpp @@ -17,7 +17,8 @@ Author: Notes: --*/ -#include "tactic/core/special_relations.h" +#include "tactic/core/special_relations_tactic.h" +#include "ast/rewriter/func_decl_replace.h" void special_relations_tactic::collect_feature(goal const& g, unsigned idx, obj_map& goal_features) { @@ -26,14 +27,34 @@ void special_relations_tactic::collect_feature(goal const& g, unsigned idx, if (is_transitivity(f, p)) { insert(goal_features, p, idx, sr_transitive); } + else if (is_anti_symmetry(f, p)) { + insert(goal_features, p, idx, sr_antisymmetric); + } + else if (is_left_tree(f, p)) { + insert(goal_features, p, idx, sr_lefttree); + } + else if (is_right_tree(f, p)) { + insert(goal_features, p, idx, sr_righttree); + } + else if (is_reflexive(f, p)) { + insert(goal_features, p, idx, sr_reflexive); + } + else if (is_total(f, p)) { + insert(goal_features, p, idx, sr_total); + } } -void specia_relations_tactic::insert(obj_map& goal_features, func_decl* p, unsigned idx, sr_property p) { - +void special_relations_tactic::insert(obj_map& goal_features, func_decl* f, unsigned idx, sr_property p) { + sp_axioms ax; + goal_features.find(f, ax); + ax.m_goal_indices.push_back(idx); + ax.m_sp_features = (sr_property)(p | ax.m_sp_features); + goal_features.insert(f, ax); } bool special_relations_tactic::is_transitivity(expr* fml, func_decl_ref& p) { + // match Forall x, y, z . p(x,y) & p(y,z) -> p(x,z) return false; } bool special_relations_tactic::is_anti_symmetry(expr* fml, func_decl_ref& p) { @@ -45,7 +66,7 @@ bool special_relations_tactic::is_left_tree(expr* fml, func_decl_ref& p) { bool special_relations_tactic::is_right_tree(expr* fml, func_decl_ref& p) { return false; } -bool special_relations_tactic::is_reflexivity(expr* fml, func_decl_ref& p) { +bool special_relations_tactic::is_reflexive(expr* fml, func_decl_ref& p) { return false; } bool special_relations_tactic::is_total(expr* fml, func_decl_ref& p) { @@ -57,16 +78,58 @@ bool special_relations_tactic::is_symmetric(expr* fml, func_decl_ref& p) { void special_relations_tactic::operator()(goal_ref const & g, goal_ref_buffer & result) { - tactic_report report("special_relations", g); + tactic_report report("special_relations", *g); obj_map goal_features; - unsigned size = g.size(); + unsigned size = g->size(); for (unsigned idx = 0; idx < size; idx++) { - collect_feature(g, idx, goal_features); + collect_feature(*g, idx, goal_features); } - if (!goal_features.empty()) { - + special_relations_util u(m); + func_decl_replace replace(m); + unsigned_vector to_delete; + for(auto const& kv : goal_features) { + func_decl* sp = nullptr; + sr_property feature = kv.m_value.m_sp_features; + switch (feature) { + case sr_po: + replace.insert(kv.m_key, u.mk_po_decl(kv.m_key)); + to_delete.append(kv.m_value.m_goal_indices); + break; + case sr_to: + replace.insert(kv.m_key, u.mk_to_decl(kv.m_key)); + to_delete.append(kv.m_value.m_goal_indices); + break; + case sr_plo: + replace.insert(kv.m_key, u.mk_plo_decl(kv.m_key)); + to_delete.append(kv.m_value.m_goal_indices); + break; + case sr_lo: + replace.insert(kv.m_key, u.mk_lo_decl(kv.m_key)); + to_delete.append(kv.m_value.m_goal_indices); + break; + default: + TRACE("special_relations", tout << "unprocessed feature " << feature << "\n";); + break; + } } + if (!replace.empty()) { + for (unsigned idx = 0; idx < size; idx++) { + if (to_delete.contains(idx)) { + g->update(idx, m.mk_true()); + } + else { + expr_ref new_f = replace(g->form(idx)); + g->update(idx, new_f); + } + } + g->elim_true(); + } + g->inc_depth(); result.push_back(g.get()); } +tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p) { + return alloc(special_relations_tactic, m, p); +} + diff --git a/src/tactic/core/special_relations_tactic.h b/src/tactic/core/special_relations_tactic.h index 88bd94843..9d7be3717 100644 --- a/src/tactic/core/special_relations_tactic.h +++ b/src/tactic/core/special_relations_tactic.h @@ -22,29 +22,32 @@ Notes: #include "tactic/tactic.h" #include "tactic/tactical.h" +#include "ast/special_relations_decl_plugin.h" class special_relations_tactic : public tactic { + ast_manager& m; params_ref m_params; struct sp_axioms { unsigned_vector m_goal_indices; - unsigned m_sp_features; + sr_property m_sp_features; + sp_axioms():m_sp_features(sr_none) {} }; void collect_feature(goal const& g, unsigned idx, obj_map& goal_features); - void insert(obj_map& goal_features, func_decl* p, unsigned idx, sr_property p); + void insert(obj_map& goal_features, func_decl* f, unsigned idx, sr_property p); bool is_transitivity(expr* fml, func_decl_ref& p); bool is_anti_symmetry(expr* fml, func_decl_ref& p); bool is_left_tree(expr* fml, func_decl_ref& p); bool is_right_tree(expr* fml, func_decl_ref& p); - bool is_reflexivity(expr* fml, func_decl_ref& p); + bool is_reflexive(expr* fml, func_decl_ref& p); bool is_total(expr* fml, func_decl_ref& p); bool is_symmetric(expr* fml, func_decl_ref& p); public: - special_relations_tactic(ast_manager & m, params_ref const & ref = params_ref()) {} + special_relations_tactic(ast_manager & m, params_ref const & ref = params_ref()): m(m), m_params(ref) {} ~special_relations_tactic() override {}