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

fix #4166

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-30 14:47:15 -07:00
parent e9119a6eb5
commit 893265ce94
3 changed files with 12 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_setup.cpp
View file

@ -877,7 +877,7 @@ namespace smt {
void setup::setup_datatypes() { void setup::setup_datatypes() {
TRACE("datatype", tout << "registering theory datatype...\n";); TRACE("datatype", tout << "registering theory datatype...\n";);
m_context.register_plugin(alloc(theory_datatype, m_manager, m_params)); m_context.register_plugin(alloc(theory_datatype, m_manager));
} }
void setup::setup_recfuns() { void setup::setup_recfuns() {

15
src/smt/theory_datatype.cpp
View file

@ -75,7 +75,7 @@ namespace smt {
theory* theory_datatype::mk_fresh(context* new_ctx) { theory* theory_datatype::mk_fresh(context* new_ctx) {
return alloc(theory_datatype, new_ctx->get_manager(), m_params); return alloc(theory_datatype, new_ctx->get_manager());
} }
/** /**
@ -286,7 +286,7 @@ namespace smt {
assert_is_constructor_axiom(n, c, null_literal); assert_is_constructor_axiom(n, c, null_literal);
} }
else { else {
if (m_params.m_dt_lazy_splits == 0 || (m_params.m_dt_lazy_splits == 1 && !s->is_infinite())) if (params().m_dt_lazy_splits == 0 || (params().m_dt_lazy_splits == 1 && !s->is_infinite()))
mk_split(r); mk_split(r);
} }
} }
@ -487,7 +487,7 @@ namespace smt {
// return... // return...
return FC_CONTINUE; return FC_CONTINUE;
} }
if (m_params.m_dt_lazy_splits > 0) { if (params().m_dt_lazy_splits > 0) {
// using lazy case splits... // using lazy case splits...
var_data * d = m_var_data[v]; var_data * d = m_var_data[v];
if (d->m_constructor == nullptr) { if (d->m_constructor == nullptr) {
@ -694,9 +694,12 @@ namespace smt {
return false; return false;
} }
theory_datatype::theory_datatype(ast_manager & m, theory_datatype_params & p): theory_datatype_params const& theory_datatype::params() const {
return get_context().get_fparams();
}
theory_datatype::theory_datatype(ast_manager & m):
theory(m.mk_family_id("datatype")), theory(m.mk_family_id("datatype")),
m_params(p),
m_util(m), m_util(m),
m_autil(m), m_autil(m),
m_find(*this), m_find(*this),
@ -932,7 +935,7 @@ namespace smt {
else { else {
// there are more than 2 unassigned recognizers... // there are more than 2 unassigned recognizers...
// if eager splits are enabled... create new case split // if eager splits are enabled... create new case split
if (m_params.m_dt_lazy_splits == 0 || (!dt->is_infinite() && m_params.m_dt_lazy_splits == 1)) if (params().m_dt_lazy_splits == 0 || (!dt->is_infinite() && params().m_dt_lazy_splits == 1))
mk_split(v); mk_split(v);
} }
} }

5
src/smt/theory_datatype.h
View file

@ -46,8 +46,6 @@ namespace smt {
stats() { reset(); } stats() { reset(); }
}; };
theory_datatype_params & m_params;
datatype_util m_util; datatype_util m_util;
array_util m_autil; array_util m_autil;
ptr_vector<var_data> m_var_data; ptr_vector<var_data> m_var_data;
@ -130,8 +128,9 @@ namespace smt {
void reset_eh() override; void reset_eh() override;
void restart_eh() override { m_util.reset(); } void restart_eh() override { m_util.reset(); }
bool is_shared(theory_var v) const override; bool is_shared(theory_var v) const override;
theory_datatype_params const& params() const;
public: public:
theory_datatype(ast_manager & m, theory_datatype_params & p); theory_datatype(ast_manager & m);
~theory_datatype() override; ~theory_datatype() override;
theory * mk_fresh(context * new_ctx) override; theory * mk_fresh(context * new_ctx) override;
void display(std::ostream & out) const override; void display(std::ostream & out) const override;