From e2f5c1f7c835680a8184d055575a5c3b1012116f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 10 Jan 2020 12:18:56 -0800 Subject: [PATCH] delay load specrels Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/poly_rewriter.h | 1 - src/ast/special_relations_decl_plugin.h | 30 ++++++++++++++----------- src/ast/static_features.cpp | 2 +- src/cmd_context/cmd_context.cpp | 2 +- 4 files changed, 19 insertions(+), 16 deletions(-) diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h index f49980a57..9a83ac729 100644 --- a/src/ast/rewriter/poly_rewriter.h +++ b/src/ast/rewriter/poly_rewriter.h @@ -108,7 +108,6 @@ public: updt_params(p); SASSERT(!m_som || m_flat); // som of monomials form requires flattening to be enabled. SASSERT(!m_som || !m_hoist_mul); // som is mutually exclusive with hoisting multiplication. - updt_params(p); } ast_manager & m() const { return Config::m(); } diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h index 339fdc82e..e43f22cd5 100644 --- a/src/ast/special_relations_decl_plugin.h +++ b/src/ast/special_relations_decl_plugin.h @@ -72,15 +72,19 @@ enum sr_property { class special_relations_util { ast_manager& m; - family_id m_fid; + mutable family_id m_fid; func_decl* mk_rel_decl(func_decl* f, decl_kind k) { parameter p(f); SASSERT(f->get_arity() == 2); - return m.mk_func_decl(m_fid, k, 1, &p, 2, f->get_domain(), f->get_range()); + return m.mk_func_decl(fid(), k, 1, &p, 2, f->get_domain(), f->get_range()); } + family_id fid() const { + if (null_family_id == m_fid) m_fid = m.get_family_id("specrels"); + return m_fid; + } public: - special_relations_util(ast_manager& m) : m(m), m_fid(m.get_family_id("special_relations")) {} + special_relations_util(ast_manager& m) : m(m), m_fid(null_family_id) { } - bool is_special_relation(func_decl* f) const { return f->get_family_id() == m_fid; } + bool is_special_relation(func_decl* f) const { return f->get_family_id() == fid(); } bool is_special_relation(app* e) const { return is_special_relation(e->get_decl()); } sr_property get_property(func_decl* f) const; sr_property get_property(app* e) const { return get_property(e->get_decl()); } @@ -91,16 +95,16 @@ public: func_decl* mk_lo_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_LO); } func_decl* mk_tc_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TC); } - 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_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); } - bool is_tc(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TC); } + bool is_lo(expr const * e) const { return is_app_of(e, fid(), OP_SPECIAL_RELATION_LO); } + bool is_po(expr const * e) const { return is_app_of(e, fid(), OP_SPECIAL_RELATION_PO); } + bool is_plo(expr const * e) const { return is_app_of(e, fid(), OP_SPECIAL_RELATION_PLO); } + bool is_to(expr const * e) const { return is_app_of(e, fid(), OP_SPECIAL_RELATION_TO); } + bool is_tc(expr const * e) const { return is_app_of(e, fid(), OP_SPECIAL_RELATION_TC); } - 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_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); } + app * mk_lo (expr * arg1, expr * arg2) { return m.mk_app( fid(), OP_SPECIAL_RELATION_LO, arg1, arg2); } + app * mk_po (expr * arg1, expr * arg2) { return m.mk_app( fid(), OP_SPECIAL_RELATION_PO, arg1, arg2); } + app * mk_plo(expr * arg1, expr * arg2) { return m.mk_app( fid(), OP_SPECIAL_RELATION_PLO, arg1, arg2); } + app * mk_to (expr * arg1, expr * arg2) { return m.mk_app( fid(), OP_SPECIAL_RELATION_TO, arg1, arg2); } }; diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index e5135347c..d3d9ec294 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -30,7 +30,7 @@ static_features::static_features(ast_manager & m): m_afid(m.mk_family_id("arith")), m_lfid(m.mk_family_id("label")), m_arrfid(m.mk_family_id("array")), - m_srfid(m.mk_family_id("special_relations")), + m_srfid(m.mk_family_id("specrels")), m_label_sym("label"), m_pattern_sym("pattern"), m_expr_list_sym("expr-list") { diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 61a0296c2..b3d14c8da 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -689,7 +689,7 @@ void cmd_context::init_manager_core(bool new_manager) { register_plugin(symbol("fpa"), alloc(fpa_decl_plugin), logic_has_fpa()); register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic()); register_plugin(symbol("csp"), alloc(csp_decl_plugin), smt_logics::logic_is_csp(m_logic)); - register_plugin(symbol("special_relations"), alloc(special_relations_decl_plugin), !has_logic()); + register_plugin(symbol("specrels"), alloc(special_relations_decl_plugin), !has_logic()); } else { // the manager was created by an external module