mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
disable unsound simplify, rename stats, delay region allocation for cutsets
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
963f8240c2
commit
39061d7388
|
@ -576,7 +576,7 @@ namespace sat {
|
|||
cuts2bins(cuts);
|
||||
bins2dont_cares();
|
||||
dont_cares2cuts(cuts);
|
||||
m_aig_cuts.simplify();
|
||||
// m_aig_cuts.simplify();
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -698,16 +698,16 @@ namespace sat {
|
|||
}
|
||||
|
||||
void cut_simplifier::collect_statistics(statistics& st) const {
|
||||
st.update("sat-aig.eqs", m_stats.m_num_eqs);
|
||||
st.update("sat-aig.cuts", m_stats.m_num_cuts);
|
||||
st.update("sat-aig.ands", m_stats.m_num_ands);
|
||||
st.update("sat-aig.ites", m_stats.m_num_ites);
|
||||
st.update("sat-aig.xors", m_stats.m_num_xors);
|
||||
st.update("sat-aig.xands", m_stats.m_xands);
|
||||
st.update("sat-aig.xites", m_stats.m_xites);
|
||||
st.update("sat-aig.xxors", m_stats.m_xxors);
|
||||
st.update("sat-aig.xluts", m_stats.m_xluts);
|
||||
st.update("sat-aig.dc-reduce", m_stats.m_num_dont_care_reductions);
|
||||
st.update("sat-cut.eqs", m_stats.m_num_eqs);
|
||||
st.update("sat-cut.cuts", m_stats.m_num_cuts);
|
||||
st.update("sat-cut.ands", m_stats.m_num_ands);
|
||||
st.update("sat-cut.ites", m_stats.m_num_ites);
|
||||
st.update("sat-cut.xors", m_stats.m_num_xors);
|
||||
st.update("sat-cut.xands", m_stats.m_xands);
|
||||
st.update("sat-cut.xites", m_stats.m_xites);
|
||||
st.update("sat-cut.xxors", m_stats.m_xxors);
|
||||
st.update("sat-cut.xluts", m_stats.m_xluts);
|
||||
st.update("sat-cut.dc-reduce", m_stats.m_num_dont_care_reductions);
|
||||
}
|
||||
|
||||
void cut_simplifier::validate_unit(literal lit) {
|
||||
|
|
|
@ -92,7 +92,7 @@ namespace sat {
|
|||
|
||||
struct hash {
|
||||
unsigned operator()(bin_rel const& p) const {
|
||||
return mk_mix(p.u, p.v, 1);
|
||||
return p.u + 65599*p.v; // Weinberger's should be a bit cheaper mk_mix(p.u, p.v, 1);
|
||||
}
|
||||
};
|
||||
struct eq {
|
||||
|
|
|
@ -79,6 +79,9 @@ namespace sat {
|
|||
|
||||
void cut_set::push_back(on_update_t& on_add, cut const& c) {
|
||||
SASSERT(m_max_size > 0);
|
||||
if (!m_cuts) {
|
||||
m_cuts = new (*m_region) cut[m_max_size];
|
||||
}
|
||||
if (m_size == m_max_size) {
|
||||
m_max_size *= 2;
|
||||
cut* new_cuts = new (*m_region) cut[m_max_size];
|
||||
|
@ -109,9 +112,9 @@ namespace sat {
|
|||
SASSERT(!m_region || m_cuts);
|
||||
VERIFY(!m_region || m_max_size > 0);
|
||||
if (!m_region) {
|
||||
m_max_size = max_sz;
|
||||
m_max_size = 2; // max_sz;
|
||||
m_region = &r;
|
||||
m_cuts = new (r) cut[max_sz];
|
||||
m_cuts = nullptr;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue