From 3afe081f62b4e89a3022a0a29e5865c19c8fb765 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Mar 2019 11:42:40 -0700 Subject: [PATCH] fixup compiled patterns Signed-off-by: Nikolaj Bjorner --- src/ast/ast_util.h | 15 ++++++++ src/ast/pattern/expr_pattern_match.cpp | 12 ++----- src/ast/pattern/expr_pattern_match.h | 21 +++--------- src/tactic/core/special_relations_tactic.cpp | 36 ++++++++++++++++---- src/tactic/core/special_relations_tactic.h | 14 +++----- 5 files changed, 54 insertions(+), 44 deletions(-) diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h index a45c65d82..a8c9131c7 100644 --- a/src/ast/ast_util.h +++ b/src/ast/ast_util.h @@ -111,6 +111,17 @@ app * mk_and(ast_manager & m, unsigned num_args, app * const * args); inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); } inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); } +inline app_ref operator&(expr_ref& a, expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); } +inline app_ref operator&(app_ref& a, expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); } +inline app_ref operator&(var_ref& a, expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); } +inline app_ref operator&(quantifier_ref& a, expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); } + +inline app_ref operator|(expr_ref& a, expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); } +inline app_ref operator|(app_ref& a, expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); } +inline app_ref operator|(var_ref& a, expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); } +inline app_ref operator|(quantifier_ref& a, expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); } + + /** Return (or args[0] ... args[num_args-1]) if num_args >= 2 Return args[0] if num_args == 1 @@ -129,6 +140,10 @@ expr * mk_not(ast_manager & m, expr * arg); expr_ref mk_not(const expr_ref& e); +inline expr_ref not(const expr_ref& e) { return mk_not(e); } +inline app_ref not(const app_ref& e) { return app_ref(e.m().mk_not(e), e.m()); } + + /** Negate and push over conjunction or disjunction. */ diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp index 5a1f20c3b..8ae0dcbf2 100644 --- a/src/ast/pattern/expr_pattern_match.cpp +++ b/src/ast/pattern/expr_pattern_match.cpp @@ -102,7 +102,7 @@ expr_pattern_match::instantiate(expr* a, unsigned num_bound, subst& s, expr_ref& for (unsigned i = 0; i < num_bound; ++i) { b.insert(m_bound_dom[i], m_bound_rng[i]); } - + TRACE("expr_pattern_match", tout << mk_pp(a, m_manager) << " " << num_bound << "\n";); inst_proc proc(m_manager, s, b, m_regs); for_each_ast(proc, a); expr* v = nullptr; @@ -273,11 +273,7 @@ expr_pattern_match::match(expr* a, unsigned init, subst& s) break; } case CHECK_BOUND: - TRACE("expr_pattern_match", - tout - << "check bound " - << pc.m_num_bound << " " << pc.m_reg; - ); + TRACE("expr_pattern_match", tout << "check bound " << pc.m_num_bound << " " << pc.m_reg << "\n";); ok = m_bound_rng[pc.m_num_bound] == m_regs[pc.m_reg]; break; case BIND: @@ -418,7 +414,6 @@ expr_pattern_match::initialize(char const * spec_string) { for (expr * e : ctx.assertions()) { compile(e); } - TRACE("expr_pattern_match", display(tout); ); } unsigned expr_pattern_match::initialize(quantifier* q) { @@ -444,7 +439,6 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const { break; case BIND: out << "bind "; - out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " "; out << mk_pp(pc.m_pat, m_manager) << "\n"; out << "next: " << pc.m_next << "\n"; out << "offset: " << pc.m_offset << "\n"; @@ -452,7 +446,6 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const { break; case BIND_AC: out << "bind_ac "; - out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " "; out << mk_pp(pc.m_pat, m_manager) << "\n"; out << "next: " << pc.m_next << "\n"; out << "offset: " << pc.m_offset << "\n"; @@ -460,7 +453,6 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const { break; case BIND_C: out << "bind_c "; - out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " "; out << mk_pp(pc.m_pat, m_manager) << "\n"; out << "next: " << pc.m_next << "\n"; out << "offset: " << pc.m_offset << "\n"; diff --git a/src/ast/pattern/expr_pattern_match.h b/src/ast/pattern/expr_pattern_match.h index 679d69fbb..6c472d708 100644 --- a/src/ast/pattern/expr_pattern_match.h +++ b/src/ast/pattern/expr_pattern_match.h @@ -80,13 +80,7 @@ class expr_pattern_match { } void operator()(var* v) { - var* b = nullptr; - if (m_bound.find(v, b)) { - m_memoize.insert(v, b); - } - else { - UNREACHABLE(); - } + m_memoize.insert(v, m_bound[v]); } void operator()(app * n) { @@ -98,15 +92,9 @@ class expr_pattern_match { if (m_subst.find(decl, r)) { decl = to_app(m_regs[r])->get_decl(); } - for (unsigned i = 0; i < num_args; ++i) { - expr* arg = nullptr; - if (m_memoize.find(n->get_arg(i), arg)) { - SASSERT(arg); - args.push_back(arg); - } - else { - UNREACHABLE(); - } + for (expr* arg : *n) { + arg = m_memoize[arg]; + args.push_back(arg); } if (m_manager.is_pattern(n)) { result = m_manager.mk_pattern(num_args, reinterpret_cast(args.c_ptr())); @@ -116,7 +104,6 @@ class expr_pattern_match { } m_pinned.push_back(result); m_memoize.insert(n, result); - return; } }; diff --git a/src/tactic/core/special_relations_tactic.cpp b/src/tactic/core/special_relations_tactic.cpp index be0706c5c..75f8e270c 100644 --- a/src/tactic/core/special_relations_tactic.cpp +++ b/src/tactic/core/special_relations_tactic.cpp @@ -19,6 +19,8 @@ Notes: --*/ #include "tactic/core/special_relations_tactic.h" #include "ast/rewriter/func_decl_replace.h" +#include "ast/ast_util.h" +#include "ast/ast_pp.h" void special_relations_tactic::collect_feature(goal const& g, unsigned idx, obj_map& goal_features) { @@ -27,7 +29,10 @@ void special_relations_tactic::collect_feature(goal const& g, unsigned idx, if (!is_quantifier(f)) return; unsigned index = 0; app_ref_vector patterns(m); - if (m_pm.match_quantifier_index(to_quantifier(f), patterns, index)) { + bool is_match = m_pm.match_quantifier_index(to_quantifier(f), patterns, index); + TRACE("special_relations", tout << "check " << is_match << " " << mk_pp(f, m) << "\n"; + if (is_match) tout << patterns << " " << index << "\n";); + if (is_match) { p = to_app(patterns.get(0)->get_arg(0))->get_decl(); insert(goal_features, p, idx, m_properties[index]); } @@ -44,8 +49,8 @@ void special_relations_tactic::insert(obj_map& goal_featur void special_relations_tactic::initialize() { if (!m_properties.empty()) return; - sort_ref A(m); - func_decl_ref R(m.mk_func_decl(symbol("R"), A, A, m.mk_bool_sort()), m); + sort_ref A(m.mk_uninterpreted_sort(symbol("A")), m); + func_decl_ref R(m.mk_func_decl(symbol("?R"), A, A, m.mk_bool_sort()), m); var_ref x(m.mk_var(0, A), m); var_ref y(m.mk_var(1, A), m); var_ref z(m.mk_var(2, A), m); @@ -68,34 +73,51 @@ void special_relations_tactic::initialize() { expr_ref fml(m); quantifier_ref q(m); expr_ref pat(m.mk_pattern(to_app(Rxy)), m); + expr_ref pat0(m.mk_pattern(to_app(Rxx)), m); expr* pats[1] = { pat }; + expr* pats0[1] = { pat0 }; + fml = m.mk_or(m.mk_not(Rxy), m.mk_not(Ryz), Rxz); q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); register_pattern(m_pm.initialize(q), sr_transitive); - + fml = m.mk_or(not(Rxy & Ryz), Rxz); + q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); + register_pattern(m_pm.initialize(q), sr_transitive); + fml = Rxx; - q = m.mk_forall(1, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); + q = m.mk_forall(1, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats0); register_pattern(m_pm.initialize(q), sr_reflexive); fml = m.mk_or(nRxy, nRyx, m.mk_eq(x, y)); q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); register_pattern(m_pm.initialize(q), sr_antisymmetric); + fml = m.mk_or(not(Rxy & Ryx), m.mk_eq(x, y)); + q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); + register_pattern(m_pm.initialize(q), sr_antisymmetric); fml = m.mk_or(nRyx, nRzx, Ryz, Rzy); q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); register_pattern(m_pm.initialize(q), sr_lefttree); + fml = m.mk_or(not (Ryx & Rzx), Ryz, Rzy); + q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); + register_pattern(m_pm.initialize(q), sr_lefttree); - fml = m.mk_or(nRxy, nRxz, Ryx, Rzy); + fml = m.mk_or(nRxy, nRxz, Ryz, Rzy); + q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); + register_pattern(m_pm.initialize(q), sr_righttree); + fml = m.mk_or(not(Rxy & Rxz), Ryz, Rzy); q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); register_pattern(m_pm.initialize(q), sr_righttree); fml = m.mk_or(Rxy, Ryx); q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); register_pattern(m_pm.initialize(q), sr_total); + + TRACE("special_relations", m_pm.display(tout);); } void special_relations_tactic::register_pattern(unsigned index, sr_property p) { - SASSERT(index == m_properties.size() + 1); + SASSERT(index == m_properties.size()); m_properties.push_back(p); } diff --git a/src/tactic/core/special_relations_tactic.h b/src/tactic/core/special_relations_tactic.h index 58da2efbc..c706c78e8 100644 --- a/src/tactic/core/special_relations_tactic.h +++ b/src/tactic/core/special_relations_tactic.h @@ -43,17 +43,10 @@ class special_relations_tactic : public tactic { void initialize(); void register_pattern(unsigned index, sr_property); - 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_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()): m(m), m_params(ref), m_pm(m) {} + special_relations_tactic(ast_manager & m, params_ref const & ref = params_ref()): + m(m), m_params(ref), m_pm(m) {} ~special_relations_tactic() override {} @@ -71,8 +64,9 @@ public: tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p = params_ref()); + /* - ADD_TACTIC("special_relations", "detect and replace by special relations.", "mk_special_relations_tactic(m, p)") + ADD_TACTIC("special-relations", "detect and replace by special relations.", "mk_special_relations_tactic(m, p)") */ #endif