mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

delay load specrels

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-10 12:18:56 -08:00
parent 541658fe02
commit e2f5c1f7c8
4 changed files with 19 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/poly_rewriter.h
View file

@ -108,7 +108,6 @@ public:
updt_params(p); updt_params(p);
SASSERT(!m_som || m_flat); // som of monomials form requires flattening to be enabled. 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. SASSERT(!m_som || !m_hoist_mul); // som is mutually exclusive with hoisting multiplication.
updt_params(p);
} }
ast_manager & m() const { return Config::m(); } ast_manager & m() const { return Config::m(); }

30
src/ast/special_relations_decl_plugin.h
View file

@ -72,15 +72,19 @@ enum sr_property {
class special_relations_util { class special_relations_util {
ast_manager& m; ast_manager& m;
family_id m_fid; mutable family_id m_fid;
func_decl* mk_rel_decl(func_decl* f, decl_kind k) { func_decl* mk_rel_decl(func_decl* f, decl_kind k) {
parameter p(f); SASSERT(f->get_arity() == 2); 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: 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()); } 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(func_decl* f) const;
sr_property get_property(app* e) const { return get_property(e->get_decl()); } 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_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); } 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_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, m_fid, OP_SPECIAL_RELATION_PO); } 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, m_fid, OP_SPECIAL_RELATION_PLO); } 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, m_fid, OP_SPECIAL_RELATION_TO); } 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, m_fid, OP_SPECIAL_RELATION_TC); } 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_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( m_fid, OP_SPECIAL_RELATION_PO, 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( m_fid, OP_SPECIAL_RELATION_PLO, 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( m_fid, OP_SPECIAL_RELATION_TO, arg1, arg2); } app * mk_to (expr * arg1, expr * arg2) { return m.mk_app( fid(), OP_SPECIAL_RELATION_TO, arg1, arg2); }
}; };

2
src/ast/static_features.cpp
View file

@ -30,7 +30,7 @@ static_features::static_features(ast_manager & m):
m_afid(m.mk_family_id("arith")), m_afid(m.mk_family_id("arith")),
m_lfid(m.mk_family_id("label")), m_lfid(m.mk_family_id("label")),
m_arrfid(m.mk_family_id("array")), 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_label_sym("label"),
m_pattern_sym("pattern"), m_pattern_sym("pattern"),
m_expr_list_sym("expr-list") { m_expr_list_sym("expr-list") {

2
src/cmd_context/cmd_context.cpp
View file

@ -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("fpa"), alloc(fpa_decl_plugin), logic_has_fpa());
register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic()); 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("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 { else {
// the manager was created by an external module // the manager was created by an external module