mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +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 13:50:05 -08:00
parent cc5971ceaf
commit 283aa04d68
1 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

12
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) {
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
@ -130,24 +130,24 @@ namespace sat {
m_lits.append(sz, lits);
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_stats.m_num_ands++;
// m_stats.m_num_ands++;
}
void aig_simplifier::add_xor(literal head, unsigned sz, literal const* 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) {
literal lits[3] = { c, t, e };
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) {
literal lits[2] = { l1, ~l2 };
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) {
@ -228,7 +228,7 @@ namespace sat {
xf.set(on_xor);
xf(clauses);
#if 0
#if 1
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) {
m_stats.m_num_luts++;