mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

No need to hash quaternaries for AND.

Browse source
This commit is contained in:
Mathias Soeken 2020-03-01 12:55:36 +01:00 • committed by Nikolaj Bjorner
parent e8f7a08289
commit 20c3f75740
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/sat_npn3_finder.cpp
View file

@ -354,8 +354,7 @@ namespace sat {
binary_hash_table_t binaries; binary_hash_table_t binaries;
ternary_hash_table_t ternaries; ternary_hash_table_t ternaries;
quaternary_hash_table_t quaternaries; process_clauses(clauses, binaries, ternaries);
process_more_clauses(clauses, binaries, ternaries, quaternaries);
const auto try_and = [&](literal w, literal x, literal y, literal z, clause &c) { const auto try_and = [&](literal w, literal x, literal y, literal z, clause &c) {
if (!implies(w, ~x)) return false; if (!implies(w, ~x)) return false;