From bce1ee6d393954e04228a7cd4fa94689e500c6c2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Mar 2019 09:21:34 -0700 Subject: [PATCH] new files Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/func_decl_replace.cpp | 96 ++++++++++++++++++++ src/ast/rewriter/func_decl_replace.h | 45 +++++++++ src/tactic/core/special_relations_tactic.cpp | 72 +++++++++++++++ src/tactic/core/special_relations_tactic.h | 69 ++++++++++++++ 4 files changed, 282 insertions(+) create mode 100644 src/ast/rewriter/func_decl_replace.cpp create mode 100644 src/ast/rewriter/func_decl_replace.h create mode 100644 src/tactic/core/special_relations_tactic.cpp create mode 100644 src/tactic/core/special_relations_tactic.h diff --git a/src/ast/rewriter/func_decl_replace.cpp b/src/ast/rewriter/func_decl_replace.cpp new file mode 100644 index 000000000..6e64dd568 --- /dev/null +++ b/src/ast/rewriter/func_decl_replace.cpp @@ -0,0 +1,96 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + func_decl_replace.cpp + +Abstract: + + Replace functions in expressions. + +Author: + + Nikolaj Bjorner (nbjorner) 2019-03-28 + +Revision History: + + +--*/ + + +#include "ast/rewriter/func_decl_replace.h" + +expr_ref func_decl_replace::operator()(expr* e) { + m_todo.push_back(e); + + while (!m_todo.empty()) { + expr* a = m_todo.back(), *b; + if (m_cache.contains(a)) { + m_todo.pop_back(); + } + else if (is_var(a)) { + m_cache.insert(a, a); + m_todo.pop_back(); + } + else if (is_app(a)) { + app* c = to_app(a); + unsigned n = c->get_num_args(); + m_args.reset(); + bool arg_differs = false; + for (unsigned i = 0; i < n; ++i) { + expr* d = nullptr, *arg = c->get_arg(i); + if (m_cache.find(arg, d)) { + m_args.push_back(d); + arg_differs |= arg != d; + SASSERT(m.get_sort(arg) == m.get_sort(d)); + } + else { + m_todo.push_back(arg); + } + } + if (m_args.size() == n) { + if (arg_differs) { + b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr()); + m_refs.push_back(b); + SASSERT(m.get_sort(a) == m.get_sort(b)); + } else { + b = a; + } + func_decl* f = nullptr; + if (m_subst.find(c->get_decl(), f)) { + b = m.mk_app(f, m_args.size(), m_args.c_ptr()); + m_refs.push_back(b); + } + m_cache.insert(a, b); + m_todo.pop_back(); + } + } + else { + quantifier* q = to_quantifier(a); + SASSERT(is_quantifier(a)); + expr* body = q->get_expr(), *new_body; + if (m_cache.find(body, new_body)) { + if (new_body == body) { + b = a; + } + else { + b = m.update_quantifier(q, new_body); + m_refs.push_back(b); + } + m_cache.insert(a, b); + m_todo.pop_back(); + } + else { + m_todo.push_back(body); + } + } + } + return expr_ref(cache.find(e), m); +} + +void func_decl_replace::reset() { + m_cache.reset(); + m_subst.reset(); + m_refs.reset(); +} diff --git a/src/ast/rewriter/func_decl_replace.h b/src/ast/rewriter/func_decl_replace.h new file mode 100644 index 000000000..a553ed999 --- /dev/null +++ b/src/ast/rewriter/func_decl_replace.h @@ -0,0 +1,45 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + func_decl_replace.h + +Abstract: + + Replace functions in expressions. + +Author: + + Nikolaj Bjorner (nbjorner) 2019-03-28 + +Revision History: + + +--*/ + +#ifndef FUNC_DECL_REPLACE_H_ +#define FUNC_DECL_REPLACE_H_ + +#include "ast/ast.h" + +class func_decl_replace { + ast_manager& m; + obj_map m_subst; + obj_map m_cache; + ptr_vector m_todo, m_args; + expr_ref_vector m_refs; + +public: + func_decl_replace(ast_manager& m): m(m), m_refs(m) {} + + void insert(func_decl* src, func_decl* dst) { m_subst.insert(src, dst); } + + expr_ref operator()(expr* e); + + void reset(); + + bool empty() const { return m_subst.empty(); } +}; + +#endif /* FUNC_DECL_REPLACE_H_ */ diff --git a/src/tactic/core/special_relations_tactic.cpp b/src/tactic/core/special_relations_tactic.cpp new file mode 100644 index 000000000..cb0533e81 --- /dev/null +++ b/src/tactic/core/special_relations_tactic.cpp @@ -0,0 +1,72 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + special_relations_tactic.cpp + +Abstract: + + Detect special relations in an axiomatization, + rewrite goal using special relations. + +Author: + + Nikolaj Bjorner (nbjorner) 2019-03-28 + +Notes: + +--*/ +#include "tactic/core/special_relations.h" + +void special_relations_tactic::collect_feature(goal const& g, unsigned idx, + obj_map& goal_features) { + expr* f = g.form(idx); + func_decl_ref p(m); + if (is_transitivity(f, p)) { + insert(goal_features, p, idx, sr_transitive); + } +} + +void specia_relations_tactic::insert(obj_map& goal_features, func_decl* p, unsigned idx, sr_property p) { + +} + + +bool special_relations_tactic::is_transitivity(expr* fml, func_decl_ref& p) { + return false; +} +bool special_relations_tactic::is_anti_symmetry(expr* fml, func_decl_ref& p) { + return false; +} +bool special_relations_tactic::is_left_tree(expr* fml, func_decl_ref& p) { + return false; +} +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) { + return false; +} +bool special_relations_tactic::is_total(expr* fml, func_decl_ref& p) { + return false; +} +bool special_relations_tactic::is_symmetric(expr* fml, func_decl_ref& p) { + return false; +} + + +void special_relations_tactic::operator()(goal_ref const & g, goal_ref_buffer & result) { + tactic_report report("special_relations", g); + obj_map goal_features; + unsigned size = g.size(); + for (unsigned idx = 0; idx < size; idx++) { + collect_feature(g, idx, goal_features); + } + if (!goal_features.empty()) { + + } + g->inc_depth(); + result.push_back(g.get()); +} + diff --git a/src/tactic/core/special_relations_tactic.h b/src/tactic/core/special_relations_tactic.h new file mode 100644 index 000000000..88bd94843 --- /dev/null +++ b/src/tactic/core/special_relations_tactic.h @@ -0,0 +1,69 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + special_relations_tactic.h + +Abstract: + + Detect special relations in an axiomatization, + rewrite goal using special relations. + +Author: + + Nikolaj Bjorner (nbjorner) 2019-03-28 + +Notes: + +--*/ +#ifndef SPECIAL_RELATIONS_TACTIC_H_ +#define SPECIAL_RELATIONS_TACTIC_H_ + +#include "tactic/tactic.h" +#include "tactic/tactical.h" + +class special_relations_tactic : public tactic { + params_ref m_params; + + struct sp_axioms { + unsigned_vector m_goal_indices; + unsigned m_sp_features; + }; + + 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); + + 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_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() override {} + + void updt_params(params_ref const & p) override { m_params = p; } + + void collect_param_descrs(param_descrs & r) override { } + + void operator()(goal_ref const & in, goal_ref_buffer & result) override; + + void cleanup() override {} + + tactic * translate(ast_manager & m) override { return alloc(special_relations_tactic, m, m_params); } + +}; + +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)") +*/ + +#endif