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

Find AND and XOR clauses.

Browse source
This commit is contained in:
Mathias Soeken 2020-02-27 19:04:19 +01:00 committed by Nikolaj Bjorner
parent 0713d1cdb1
commit 595fea7434
2 changed files with 81 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

75
src/sat/sat_npn3_finder.cpp
View file

@ -65,6 +65,8 @@ namespace sat {
find_mux(clauses);
find_maj(clauses);
find_orand(clauses);
find_and(clauses);
find_xor(clauses);
find_andxor(clauses);
find_xorand(clauses);
find_onehot(clauses);
@ -308,6 +310,79 @@ namespace sat {
find_npn3(clauses, m_on_orand, try_orand);
}
void npn3_finder::find_xor(clause_vector& clauses) {
if (!m_on_xor) return;
binary_hash_table_t binaries;
ternary_hash_table_t ternaries;
quaternary_hash_table_t quaternaries;
process_more_clauses(clauses, binaries, ternaries, quaternaries);
const auto try_xor = [&](literal w, literal x, literal y, literal z, clause &c) {
clause *c1, *c2, *c3, *c4, *c5, *c6, *c7;
if (!has_quaternary(quaternaries, ternaries, ~x, ~y, z, w, c1)) return false;
if (!has_quaternary(quaternaries, ternaries, ~x, y, ~z, w, c2)) return false;
if (!has_quaternary(quaternaries, ternaries, ~x, y, z, ~w, c3)) return false;
if (!has_quaternary(quaternaries, ternaries, ~x, ~y, ~z, ~w, c4)) return false;
if (!has_quaternary(quaternaries, ternaries, x, y, ~z, ~w, c5)) return false;
if (!has_quaternary(quaternaries, ternaries, x, ~y, z, ~w, c6)) return false;
if (!has_quaternary(quaternaries, ternaries, x, ~y, ~z, w, c7)) return false;
c.mark_used();
if (c1) c1->mark_used();
if (c2) c2->mark_used();
if (c3) c3->mark_used();
if (c4) c4->mark_used();
if (c5) c5->mark_used();
if (c6) c6->mark_used();
if (c7) c7->mark_used();
m_on_xor(w, ~x, y, z);
return true;
};
for (clause* cp : clauses) {
clause& c = *cp;
if (c.size() != 4 || c.was_used()) continue;
literal w = c[0], x = c[1], y = c[2], z = c[3];
if (try_xor(w, x, y, z, c)) continue;
}
filter(clauses);
}
void npn3_finder::find_and(clause_vector& clauses) {
if (!m_on_and) return;
binary_hash_table_t binaries;
ternary_hash_table_t ternaries;
quaternary_hash_table_t quaternaries;
process_more_clauses(clauses, binaries, ternaries, quaternaries);
const auto try_and = [&](literal w, literal x, literal y, literal z, clause &c) {
if (!implies(w, ~x)) return false;
if (!implies(w, ~y)) return false;
if (!implies(w, ~z)) return false;
c.mark_used();
m_on_and(w, ~x, ~y, ~z);
return true;
};
for (clause* cp : clauses) {
clause& c = *cp;
if (c.size() != 4 || c.was_used()) continue;
literal w = c[0], x = c[1], y = c[2], z = c[3];
if (try_and(w, x, y, z, c)) continue;
if (try_and(x, w, y, z, c)) continue;
if (try_and(y, w, x, z, c)) continue;
if (try_and(z, w, x, y, c)) continue;
}
filter(clauses);
}
void npn3_finder::find_andxor(clause_vector& clauses) {
if (!m_on_andxor) return;

6
src/sat/sat_npn3_finder.h
View file

@ -39,6 +39,8 @@ namespace sat {
on_function_t m_on_mux;
on_function_t m_on_maj;
on_function_t m_on_orand;
on_function_t m_on_and;
on_function_t m_on_xor;
on_function_t m_on_andxor;
on_function_t m_on_xorand;
on_function_t m_on_gamble;
@ -103,6 +105,8 @@ namespace sat {
void validate_if(literal x, literal c, literal t, literal e, clause const& c0, clause const* c1, clause const* c2, clause const* c3);
void find_maj(clause_vector& clauses);
void find_orand(clause_vector& clauses);
void find_and(clause_vector& clauses);
void find_xor(clause_vector& clauses);
void find_andxor(clause_vector& clauses);
void find_xorand(clause_vector& clauses);
void find_gamble(clause_vector& clauses);
@ -118,6 +122,8 @@ namespace sat {
void set_on_mux(std::function<void(literal head, literal cond, literal th, literal el)> const& f) { m_on_mux = f; }
void set_on_maj(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_maj = f; }
void set_on_orand(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_orand = f; }
void set_on_and(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_and = f; }
void set_on_xor(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_xor = f; }
void set_on_andxor(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_andxor = f; }
void set_on_xorand(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_xorand = f; }
void set_on_gamble(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_gamble = f; }