mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-04 14:10:16 -08:00
parent 876bd80bea
commit fd808dd98b
2 changed files with 21 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/sat/sat_aig_simplifier.cpp
View file

@ -119,7 +119,7 @@ namespace sat {
void aig_simplifier::add_and(literal head, unsigned sz, literal const* lits) { void aig_simplifier::add_and(literal head, unsigned sz, literal const* lits) {
m_aig_cuts.add_node(head, and_op, sz, lits); m_aig_cuts.add_node(head, and_op, sz, lits);
// m_stats.m_num_ands++; m_stats.m_num_ands++;
} }
// head == l1 or l2 or l3 // head == l1 or l2 or l3
@ -130,24 +130,24 @@ namespace sat {
m_lits.append(sz, lits); m_lits.append(sz, lits);
for (unsigned i = 0; i < sz; ++i) m_lits[i].neg(); for (unsigned i = 0; i < sz; ++i) m_lits[i].neg();
m_aig_cuts.add_node(~head, and_op, sz, m_lits.c_ptr()); m_aig_cuts.add_node(~head, and_op, sz, m_lits.c_ptr());
// m_stats.m_num_ands++; m_stats.m_num_ands++;
} }
void aig_simplifier::add_xor(literal head, unsigned sz, literal const* lits) { void aig_simplifier::add_xor(literal head, unsigned sz, literal const* lits) {
m_aig_cuts.add_node(head, xor_op, sz, lits); m_aig_cuts.add_node(head, xor_op, sz, lits);
// m_stats.m_num_xors++; m_stats.m_num_xors++;
} }
void aig_simplifier::add_ite(literal head, literal c, literal t, literal e) { void aig_simplifier::add_ite(literal head, literal c, literal t, literal e) {
literal lits[3] = { c, t, e }; literal lits[3] = { c, t, e };
m_aig_cuts.add_node(head, ite_op, 3, lits); m_aig_cuts.add_node(head, ite_op, 3, lits);
// m_stats.m_num_ites++; m_stats.m_num_ites++;
} }
void aig_simplifier::add_iff(literal head, literal l1, literal l2) { void aig_simplifier::add_iff(literal head, literal l1, literal l2) {
literal lits[2] = { l1, ~l2 }; literal lits[2] = { l1, ~l2 };
m_aig_cuts.add_node(head, xor_op, 2, lits); m_aig_cuts.add_node(head, xor_op, 2, lits);
// m_stats.m_num_xors++; m_stats.m_num_xors++;
} }
void aig_simplifier::set_root(bool_var v, literal r) { void aig_simplifier::set_root(bool_var v, literal r) {
@ -184,13 +184,13 @@ namespace sat {
std::function<void (literal head, literal_vector const& ands)> on_and = std::function<void (literal head, literal_vector const& ands)> on_and =
[&,this](literal head, literal_vector const& ands) { [&,this](literal head, literal_vector const& ands) {
m_aig_cuts.add_node(head, and_op, ands.size(), ands.c_ptr()); m_aig_cuts.add_node(head, and_op, ands.size(), ands.c_ptr());
m_stats.m_num_ands++; m_stats.m_xands++;
}; };
std::function<void (literal head, literal c, literal t, literal e)> on_ite = std::function<void (literal head, literal c, literal t, literal e)> on_ite =
[&,this](literal head, literal c, literal t, literal e) { [&,this](literal head, literal c, literal t, literal e) {
literal args[3] = { c, t, e }; literal args[3] = { c, t, e };
m_aig_cuts.add_node(head, ite_op, 3, args); m_aig_cuts.add_node(head, ite_op, 3, args);
m_stats.m_num_ites++; m_stats.m_xites++;
}; };
aig_finder af(s); aig_finder af(s);
af.set(on_and); af.set(on_and);
@ -222,16 +222,16 @@ namespace sat {
} }
m_aig_cuts.add_node(head, xor_op, sz, m_lits.c_ptr()); m_aig_cuts.add_node(head, xor_op, sz, m_lits.c_ptr());
m_lits.reset(); m_lits.reset();
m_stats.m_num_xors++; m_stats.m_xxors++;
}; };
xor_finder xf(s); xor_finder xf(s);
xf.set(on_xor); xf.set(on_xor);
xf(clauses); xf(clauses);
#if 1 #if 0
std::function<void(uint64_t, bool_var_vector const&, bool_var)> on_lut = std::function<void(uint64_t, bool_var_vector const&, bool_var)> on_lut =
[&,this](uint64_t l, bool_var_vector const& vars, bool_var v) { [&,this](uint64_t l, bool_var_vector const& vars, bool_var v) {
m_stats.m_num_luts++; m_stats.m_xluts++;
}; };
lut_finder lf(s); lut_finder lf(s);
lf.set(on_lut); lf.set(on_lut);
@ -687,12 +687,15 @@ namespace sat {
} }
void aig_simplifier::collect_statistics(statistics& st) const { void aig_simplifier::collect_statistics(statistics& st) const {
st.update("sat-aig.eqs", m_stats.m_num_eqs); st.update("sat-aig.eqs", m_stats.m_num_eqs);
st.update("sat-aig.cuts", m_stats.m_num_cuts); st.update("sat-aig.cuts", m_stats.m_num_cuts);
st.update("sat-aig.ands", m_stats.m_num_ands); st.update("sat-aig.ands", m_stats.m_num_ands);
st.update("sat-aig.ites", m_stats.m_num_ites); st.update("sat-aig.ites", m_stats.m_num_ites);
st.update("sat-aig.xors", m_stats.m_num_xors); st.update("sat-aig.xors", m_stats.m_num_xors);
st.update("sat-aig.luts", m_stats.m_num_luts); 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-aig.dc-reduce", m_stats.m_num_dont_care_reductions);
} }

3
src/sat/sat_aig_simplifier.h
View file

@ -27,7 +27,8 @@ namespace sat {
class aig_simplifier { class aig_simplifier {
public: public:
struct stats { struct stats {
unsigned m_num_eqs, m_num_units, m_num_cuts, m_num_xors, m_num_ands, m_num_ites, m_num_luts; unsigned m_num_eqs, m_num_units, m_num_cuts, m_num_xors, m_num_ands, m_num_ites;
unsigned m_xxors, m_xands, m_xites, m_xluts; // extrated gates
unsigned m_num_calls, m_num_dont_care_reductions, m_num_learned_implies; unsigned m_num_calls, m_num_dont_care_reductions, m_num_learned_implies;
stats() { reset(); } stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); } void reset() { memset(this, 0, sizeof(*this)); }