mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
615 lines
23 KiB
C++
615 lines
23 KiB
C++
/*++
|
|
Copyright (c) 2020 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
sat_npn3_finder.cpp
|
|
|
|
Author:
|
|
|
|
Mathias Soeken 2020-02-20
|
|
|
|
Notes:
|
|
|
|
NPN3 finder
|
|
|
|
--*/
|
|
|
|
#include "sat/sat_npn3_finder.h"
|
|
#include "sat/sat_solver.h"
|
|
|
|
namespace sat {
|
|
|
|
// binary
|
|
npn3_finder::binary::binary(literal _x, literal _y, use_list_t* u) : x(_x), y(_y), use_list(u) {
|
|
if (x.index() > y.index()) std::swap(x, y);
|
|
}
|
|
npn3_finder::binary::binary() : x(null_literal), y(null_literal), use_list(nullptr) {}
|
|
unsigned npn3_finder::binary::hash::operator()(binary const& t) const { return mk_mix(t.x.index(), t.y.index(), 3); }
|
|
bool npn3_finder::binary::eq::operator()(binary const& a, binary const& b) const {
|
|
return a.x == b.x && a.y == b.y;
|
|
}
|
|
|
|
// ternary
|
|
npn3_finder::ternary::ternary(literal _x, literal _y, literal _z, clause* c) :
|
|
x(_x), y(_y), z(_z), orig(c) {
|
|
if (x.index() > y.index()) std::swap(x, y);
|
|
if (y.index() > z.index()) std::swap(y, z);
|
|
if (x.index() > y.index()) std::swap(x, y);
|
|
}
|
|
npn3_finder::ternary::ternary() :x(null_literal), y(null_literal), z(null_literal), orig(nullptr) {}
|
|
unsigned npn3_finder::ternary::hash::operator()(ternary const& t) const { return mk_mix(t.x.hash(), t.y.hash(), t.z.hash()); }
|
|
bool npn3_finder::ternary::eq::operator()(ternary const& a, ternary const& b) const {
|
|
return a.x == b.x && a.y == b.y && a.z == b.z;
|
|
}
|
|
|
|
// quaternary
|
|
npn3_finder::quaternary::quaternary(literal _w, literal _x, literal _y, literal _z, clause* c) :
|
|
w(_w), x(_x), y(_y), z(_z), orig(c) {
|
|
if (w.index() > x.index()) std::swap(w, x);
|
|
if (y.index() > z.index()) std::swap(y, z);
|
|
if (w.index() > y.index()) std::swap(w, y);
|
|
if (x.index() > z.index()) std::swap(x, z);
|
|
if (x.index() > y.index()) std::swap(x, y);
|
|
}
|
|
npn3_finder::quaternary::quaternary() :w(null_literal), x(null_literal), y(null_literal), z(null_literal), orig(nullptr) {}
|
|
unsigned npn3_finder::quaternary::hash::operator()(quaternary const& t) const { return mk_mix(t.w.hash(), t.x.hash(), mk_mix(t.y.hash(), t.z.hash(), 3)); }
|
|
bool npn3_finder::quaternary::eq::operator()(quaternary const& a, quaternary const& b) const {
|
|
return a.w == b.w && a.x == b.x && a.y == b.y && a.z == b.z;
|
|
}
|
|
|
|
npn3_finder::npn3_finder(solver& s) : s(s), m_big(s.rand()) {}
|
|
|
|
void npn3_finder::operator()(clause_vector& clauses) {
|
|
m_big.init(s, true);
|
|
find_mux(clauses);
|
|
find_maj(clauses);
|
|
find_orand(clauses);
|
|
find_and(clauses);
|
|
find_xor(clauses);
|
|
find_andxor(clauses);
|
|
find_xorand(clauses);
|
|
find_onehot(clauses);
|
|
find_gamble(clauses);
|
|
find_dot(clauses);
|
|
}
|
|
|
|
bool npn3_finder::implies(literal a, literal b) const {
|
|
if (m_big.connected(a, b))
|
|
return true;
|
|
for (auto const& w : s.get_wlist(a)) {
|
|
if (w.is_binary_clause() && b == w.get_literal())
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
void npn3_finder::process_clauses(clause_vector& clauses, npn3_finder::binary_hash_table_t& binaries, npn3_finder::ternary_hash_table_t& ternaries)
|
|
{
|
|
for (clause* cp : clauses) cp->unmark_used();
|
|
|
|
auto insert_binary = [&](literal x, literal y, literal z, clause* c) {
|
|
binary b(x, y, nullptr);
|
|
auto* e = binaries.insert_if_not_there2(b);
|
|
if (e->get_data().use_list == nullptr) {
|
|
use_list_t* use_list = alloc(use_list_t);
|
|
m_use_lists.push_back(use_list);
|
|
e->get_data().use_list = use_list;
|
|
}
|
|
e->get_data().use_list->push_back(std::make_pair(z, c));
|
|
};
|
|
|
|
auto insert_ternary = [&](clause& c) {
|
|
if (c.size() == 3) {
|
|
ternaries.insert(ternary(c[0], c[1], c[2], &c));
|
|
insert_binary(c[0], c[1], c[2], &c);
|
|
insert_binary(c[0], c[2], c[1], &c);
|
|
insert_binary(c[2], c[1], c[0], &c);
|
|
}
|
|
};
|
|
for (clause* cp : s.learned()) {
|
|
insert_ternary(*cp);
|
|
}
|
|
for (clause* cp : s.clauses()) {
|
|
insert_ternary(*cp);
|
|
}
|
|
}
|
|
|
|
void npn3_finder::process_more_clauses(clause_vector& clauses, npn3_finder::binary_hash_table_t& binaries, npn3_finder::ternary_hash_table_t& ternaries, npn3_finder::quaternary_hash_table_t& quaternaries)
|
|
{
|
|
for (clause* cp : clauses) cp->unmark_used();
|
|
|
|
auto insert_binary = [&](literal x, literal y, literal z, clause* c) {
|
|
binary b(x, y, nullptr);
|
|
auto* e = binaries.insert_if_not_there2(b);
|
|
if (e->get_data().use_list == nullptr) {
|
|
use_list_t* use_list = alloc(use_list_t);
|
|
m_use_lists.push_back(use_list);
|
|
e->get_data().use_list = use_list;
|
|
}
|
|
e->get_data().use_list->push_back(std::make_pair(z, c));
|
|
};
|
|
|
|
auto insert = [&](clause& c) {
|
|
if (c.size() == 3) {
|
|
ternaries.insert(ternary(c[0], c[1], c[2], &c));
|
|
insert_binary(c[0], c[1], c[2], &c);
|
|
insert_binary(c[0], c[2], c[1], &c);
|
|
insert_binary(c[2], c[1], c[0], &c);
|
|
} else if (c.size() == 4) {
|
|
quaternaries.insert(quaternary(c[0], c[1], c[2], c[3], &c));
|
|
}
|
|
};
|
|
|
|
for (clause* cp : s.learned()) {
|
|
insert(*cp);
|
|
}
|
|
for (clause* cp : s.clauses()) {
|
|
insert(*cp);
|
|
}
|
|
}
|
|
|
|
bool npn3_finder::has_ternary(ternary_hash_table_t const& ternaries, literal x, literal y, literal z, clause*& c) const
|
|
{
|
|
ternary t(x, y, z, nullptr);
|
|
if (ternaries.find(t, t)) {
|
|
c = t.orig;
|
|
return true;
|
|
}
|
|
if (implies(~y, z) || implies(~x, y) || implies(~x, z)) {
|
|
c = nullptr;
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
bool npn3_finder::has_quaternary(quaternary_hash_table_t const& quaternaries, ternary_hash_table_t const& ternaries, literal w, literal x, literal y, literal z, clause*& c) const
|
|
{
|
|
quaternary q(w, x, y, z, nullptr);
|
|
if (quaternaries.find(q, q)) {
|
|
c = q.orig;
|
|
return true;
|
|
}
|
|
if (has_ternary(ternaries, w, x, y, c) || has_ternary(ternaries, w, x, z, c) || has_ternary(ternaries, w, y, z, c) || has_ternary(ternaries, x, y, z, c)) {
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
void npn3_finder::filter(clause_vector& clauses) const
|
|
{
|
|
//std::function<bool(clause*)> not_used = [](clause* cp) { return !cp->was_used(); };
|
|
//clauses.filter_update(not_used);
|
|
}
|
|
|
|
void npn3_finder::find_npn3(clause_vector& clauses, on_function_t const& on_function, std::function<bool(binary_hash_table_t const&, ternary_hash_table_t const&, literal, literal, literal, clause&)> const& checker)
|
|
{
|
|
if (!on_function) return;
|
|
|
|
binary_hash_table_t binaries;
|
|
ternary_hash_table_t ternaries;
|
|
process_clauses(clauses, binaries, ternaries);
|
|
|
|
for (clause* cp : clauses) {
|
|
clause& c = *cp;
|
|
if (c.size() != 3 || c.was_used()) continue;
|
|
literal x = c[0], y = c[1], z = c[2];
|
|
if (checker(binaries, ternaries, x, z, y, c)) continue;
|
|
if (checker(binaries, ternaries, x, y, z, c)) continue;
|
|
if (checker(binaries, ternaries, y, x, z, c)) continue;
|
|
if (checker(binaries, ternaries, z, x, y, c)) continue;
|
|
if (checker(binaries, ternaries, z, y, x, c)) continue;
|
|
if (checker(binaries, ternaries, y, z, x, c)) continue;
|
|
}
|
|
|
|
filter(clauses);
|
|
}
|
|
|
|
void npn3_finder::find_mux(clause_vector& clauses) {
|
|
auto try_ite = [&, this](binary_hash_table_t const& binaries, ternary_hash_table_t const& ternaries, literal x, literal y, literal z, clause& c) {
|
|
literal u;
|
|
clause* c1, * c2, * c3;
|
|
if (!has_ternary(ternaries, y, ~z, ~x, c1)) {
|
|
return false;
|
|
}
|
|
binary b(~y, x, nullptr);
|
|
if (!binaries.find(b, b)) {
|
|
return false;
|
|
}
|
|
for (auto p : *b.use_list) {
|
|
u = p.first;
|
|
c2 = p.second;
|
|
if (!has_ternary(ternaries, ~u, ~x, ~y, c3)) {
|
|
continue;
|
|
}
|
|
c.mark_used();
|
|
if (c1) c1->mark_used();
|
|
if (c2) c2->mark_used();
|
|
if (c3) c3->mark_used();
|
|
m_on_mux(~x, ~y, z, u);
|
|
return true;
|
|
}
|
|
return false;
|
|
};
|
|
|
|
find_npn3(clauses, m_on_mux, try_ite);
|
|
}
|
|
|
|
void npn3_finder::find_maj(clause_vector& clauses) {
|
|
// assume that x is head
|
|
auto try_maj = [&, this](binary_hash_table_t const& binaries, ternary_hash_table_t const& ternaries, literal x, literal y, literal z, clause& c) {
|
|
literal u;
|
|
clause *c1, *c2, *c3, *c4, *c5, *c6;
|
|
if (!has_ternary(ternaries, ~x, ~y, ~z, c1)) {
|
|
return false;
|
|
}
|
|
binary b(x, y, nullptr);
|
|
if (!binaries.find(b, b)) {
|
|
return false;
|
|
}
|
|
for (auto p : *b.use_list) {
|
|
u = p.first;
|
|
if (u == z) continue;
|
|
c2 = p.second;
|
|
if (!has_ternary(ternaries, x, y, u, c3)) {
|
|
continue;
|
|
}
|
|
if (!has_ternary(ternaries, ~x, ~y, ~u, c4)) {
|
|
continue;
|
|
}
|
|
if (!has_ternary(ternaries, x, z, u, c5)) {
|
|
continue;
|
|
}
|
|
if (!has_ternary(ternaries, ~x, ~z, ~u, c6)) {
|
|
continue;
|
|
}
|
|
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();
|
|
m_on_maj(~x, y, z, u);
|
|
return true;
|
|
}
|
|
return false;
|
|
};
|
|
|
|
find_npn3(clauses, m_on_maj, try_maj);
|
|
}
|
|
|
|
void npn3_finder::find_orand(clause_vector& clauses) {
|
|
// assume that x = head, y = x
|
|
auto try_orand = [&, this](binary_hash_table_t const& binaries, ternary_hash_table_t const& ternaries, literal x, literal y, literal z, clause& c) {
|
|
if (!implies(x, ~y)) return false;
|
|
|
|
literal u;
|
|
clause *c1, *c2;
|
|
binary b(x, y, nullptr);
|
|
if (!binaries.find(b, b)) return false;
|
|
|
|
for (auto p : *b.use_list) {
|
|
u = p.first;
|
|
if (u == z) continue;
|
|
c1 = p.second;
|
|
if (!has_ternary(ternaries, ~z, ~u, ~x, c2)) {
|
|
continue;
|
|
}
|
|
c.mark_used();
|
|
if (c1) c1->mark_used();
|
|
if (c2) c2->mark_used();
|
|
m_on_orand(x, ~y, ~z, ~u);
|
|
return true;
|
|
}
|
|
return false;
|
|
};
|
|
|
|
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;
|
|
process_clauses(clauses, binaries, ternaries);
|
|
|
|
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;
|
|
|
|
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_andxor = [&](literal w, literal x, literal y, literal z, clause &c) {
|
|
clause *c1, *c2, *c3, *c4, *c5;
|
|
if (!has_quaternary(quaternaries, ternaries, ~x, y, z, ~w, c1)) return false;
|
|
if (!has_ternary(ternaries, ~x, ~y, w, c2)) return false;
|
|
if (!has_ternary(ternaries, ~x, ~z, w, c3)) return false;
|
|
if (!has_ternary(ternaries, x, ~y, ~w, c4)) return false;
|
|
if (!has_ternary(ternaries, x, ~z, ~w, c5)) 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();
|
|
m_on_andxor(~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_andxor(w, x, y, z, c)) continue;
|
|
if (try_andxor(w, y, x, z, c)) continue;
|
|
if (try_andxor(w, z, x, y, c)) continue;
|
|
if (try_andxor(x, w, y, z, c)) continue;
|
|
if (try_andxor(x, y, w, z, c)) continue;
|
|
if (try_andxor(x, z, w, y, c)) continue;
|
|
if (try_andxor(y, w, x, z, c)) continue;
|
|
if (try_andxor(y, x, w, z, c)) continue;
|
|
if (try_andxor(y, z, w, x, c)) continue;
|
|
if (try_andxor(z, w, x, y, c)) continue;
|
|
if (try_andxor(z, x, w, y, c)) continue;
|
|
if (try_andxor(z, y, w, x, c)) continue;
|
|
}
|
|
|
|
filter(clauses);
|
|
}
|
|
|
|
void npn3_finder::find_xorand(clause_vector& clauses) {
|
|
if (!m_on_xorand) 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_xorand = [&](literal w, literal x, literal y, literal z, clause &c) {
|
|
clause *c1, *c2, *c3;
|
|
if (!has_quaternary(quaternaries, ternaries, x, ~y, ~z, w, c1)) return false;
|
|
if (!has_ternary(ternaries, ~y, z, ~w, c2)) return false;
|
|
if (!has_ternary(ternaries, y, ~z, ~w, c3)) return false;
|
|
if (!implies(w, ~x)) return false;
|
|
|
|
c.mark_used();
|
|
if (c1) c1->mark_used();
|
|
if (c2) c2->mark_used();
|
|
if (c3) c3->mark_used();
|
|
m_on_xorand(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_xorand(w, x, y, z, c)) continue;
|
|
if (try_xorand(w, y, x, z, c)) continue;
|
|
if (try_xorand(w, z, x, y, c)) continue;
|
|
if (try_xorand(x, w, y, z, c)) continue;
|
|
if (try_xorand(x, y, w, z, c)) continue;
|
|
if (try_xorand(x, z, w, y, c)) continue;
|
|
if (try_xorand(y, w, x, z, c)) continue;
|
|
if (try_xorand(y, x, w, z, c)) continue;
|
|
if (try_xorand(y, z, w, x, c)) continue;
|
|
if (try_xorand(z, w, x, y, c)) continue;
|
|
if (try_xorand(z, x, w, y, c)) continue;
|
|
if (try_xorand(z, y, w, x, c)) continue;
|
|
}
|
|
|
|
filter(clauses);
|
|
}
|
|
|
|
void npn3_finder::find_gamble(clause_vector& clauses) {
|
|
if (!m_on_gamble) 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_gamble = [&](literal w, literal x, literal y, literal z, clause &c) {
|
|
clause *c1, *c2, *c3, *c4;
|
|
if (!has_quaternary(quaternaries, ternaries, ~x, ~y, ~z, w, c1)) return false;
|
|
if (!has_ternary(ternaries, ~x, y, ~w, c2)) return false;
|
|
if (!has_ternary(ternaries, ~y, z, ~w, c3)) return false;
|
|
if (!has_ternary(ternaries, x, ~z, ~w, c4)) 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();
|
|
m_on_gamble(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_gamble(w, x, y, z, c)) continue;
|
|
if (try_gamble(x, w, y, z, c)) continue;
|
|
if (try_gamble(y, w, x, z, c)) continue;
|
|
if (try_gamble(z, w, x, y, c)) continue;
|
|
}
|
|
|
|
filter(clauses);
|
|
}
|
|
|
|
void npn3_finder::find_onehot(clause_vector& clauses) {
|
|
if (!m_on_onehot) 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_onehot = [&](literal w, literal x, literal y, literal z, clause &c) {
|
|
clause *c1, *c2, *c3, *c4, *c5, *c6;
|
|
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_ternary(ternaries, ~x, ~y, w, c4)) return false;
|
|
if (!has_ternary(ternaries, ~x, ~z, w, c5)) return false;
|
|
if (!has_ternary(ternaries, ~y, ~z, w, c6)) 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();
|
|
m_on_onehot(~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_onehot(w, x, y, z, c)) continue;
|
|
if (try_onehot(x, w, y, z, c)) continue;
|
|
if (try_onehot(y, w, x, z, c)) continue;
|
|
if (try_onehot(z, w, x, y, c)) continue;
|
|
}
|
|
|
|
filter(clauses);
|
|
}
|
|
|
|
void npn3_finder::find_dot(clause_vector& clauses) {
|
|
if (!m_on_dot) 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_dot = [&](literal w, literal x, literal y, literal z, clause &c) {
|
|
clause *c1, *c2, *c3, *c4;
|
|
if (!has_ternary(ternaries, ~x, z, ~w, c1)) return false;
|
|
if (!has_ternary(ternaries, x, ~y, ~w, c2)) return false;
|
|
if (!has_ternary(ternaries, x, ~z, ~w, c3)) return false;
|
|
if (!has_ternary(ternaries, ~x, ~z, w, c4)) 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();
|
|
m_on_dot(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_dot(w, x, y, z, c)) continue;
|
|
if (try_dot(w, x, z, y, c)) continue;
|
|
if (try_dot(w, y, x, z, c)) continue;
|
|
if (try_dot(w, y, z, x, c)) continue;
|
|
if (try_dot(w, z, x, y, c)) continue;
|
|
if (try_dot(w, z, y, x, c)) continue;
|
|
if (try_dot(x, w, y, z, c)) continue;
|
|
if (try_dot(x, w, z, y, c)) continue;
|
|
if (try_dot(x, y, w, z, c)) continue;
|
|
if (try_dot(x, y, z, w, c)) continue;
|
|
if (try_dot(x, z, w, y, c)) continue;
|
|
if (try_dot(x, z, y, w, c)) continue;
|
|
if (try_dot(y, w, x, z, c)) continue;
|
|
if (try_dot(y, w, z, x, c)) continue;
|
|
if (try_dot(y, x, w, z, c)) continue;
|
|
if (try_dot(y, x, z, w, c)) continue;
|
|
if (try_dot(y, z, w, x, c)) continue;
|
|
if (try_dot(y, z, x, w, c)) continue;
|
|
if (try_dot(z, w, x, y, c)) continue;
|
|
if (try_dot(z, w, y, x, c)) continue;
|
|
if (try_dot(z, x, w, y, c)) continue;
|
|
if (try_dot(z, x, y, w, c)) continue;
|
|
if (try_dot(z, y, w, x, c)) continue;
|
|
if (try_dot(z, y, x, w, c)) continue;
|
|
}
|
|
|
|
filter(clauses);
|
|
}
|
|
|
|
}
|