1 /*++ 2 Copyright (c) 2020 Microsoft Corporation 3 4 Module Name: 5 6 sat_npn3_finder.h 7 8 Abstract: 9 10 extracts clauses for 3-input Boolean functions 11 12 Author: 13 14 Mathias Soeken 2020-02-20 15 16 Notes: 17 18 NPN3 finder 19 --*/ 20 21 #pragma once 22 23 #include "util/params.h" 24 #include "util/scoped_ptr_vector.h" 25 #include "util/statistics.h" 26 #include "sat/sat_clause.h" 27 #include "sat/sat_types.h" 28 #include "sat/sat_big.h" 29 30 namespace sat { 31 32 class solver; 33 34 class npn3_finder { 35 solver& s; 36 big m_big; 37 38 typedef std::function<void(literal, literal, literal, literal)> on_function_t; 39 on_function_t m_on_mux; 40 on_function_t m_on_maj; 41 on_function_t m_on_orand; 42 on_function_t m_on_and; 43 on_function_t m_on_xor; 44 on_function_t m_on_andxor; 45 on_function_t m_on_xorand; 46 on_function_t m_on_gamble; 47 on_function_t m_on_onehot; 48 on_function_t m_on_dot; 49 50 typedef svector<std::pair<literal, clause*>> use_list_t; 51 scoped_ptr_vector<use_list_t> m_use_lists; 52 53 struct binary { 54 literal x, y; 55 use_list_t* use_list; 56 binary(literal _x, literal _y, use_list_t* u); 57 binary(); 58 struct hash { 59 unsigned operator()(binary const& t) const; 60 }; 61 struct eq { 62 bool operator()(binary const& a, binary const& b) const; 63 }; 64 }; 65 66 struct ternary { 67 literal x, y, z; 68 clause* orig; 69 ternary(literal _x, literal _y, literal _z, clause* c); 70 ternary(); 71 struct hash { 72 unsigned operator()(ternary const& t) const; 73 }; 74 struct eq { 75 bool operator()(ternary const& a, ternary const& b) const; 76 }; 77 }; 78 79 struct quaternary { 80 literal w, x, y, z; 81 clause* orig; 82 quaternary(literal _w, literal _x, literal _y, literal _z, clause* c); 83 quaternary(); 84 struct hash { 85 unsigned operator()(quaternary const& q) const; 86 }; 87 struct eq { 88 bool operator()(quaternary const& a, quaternary const& b) const; 89 }; 90 }; 91 92 typedef hashtable<binary, binary::hash, binary::eq> binary_hash_table_t; 93 typedef hashtable<ternary, ternary::hash, ternary::eq> ternary_hash_table_t; 94 typedef hashtable<quaternary, quaternary::hash, quaternary::eq> quaternary_hash_table_t; 95 96 void process_clauses(clause_vector& clauses, binary_hash_table_t& binaries, ternary_hash_table_t& ternaries); 97 void process_more_clauses(clause_vector& clauses, binary_hash_table_t& binaries, ternary_hash_table_t& ternaries, quaternary_hash_table_t& quaternaries); 98 bool has_ternary(ternary_hash_table_t const& ternaries, literal x, literal y, literal z, clause*& c) const; 99 bool 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; 100 101 bool implies(literal a, literal b) const; 102 void filter(clause_vector& clauses) const; 103 void 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); 104 void find_mux(clause_vector& clauses); 105 void find_maj(clause_vector& clauses); 106 void find_orand(clause_vector& clauses); 107 void find_and(clause_vector& clauses); 108 void find_xor(clause_vector& clauses); 109 void find_andxor(clause_vector& clauses); 110 void find_xorand(clause_vector& clauses); 111 void find_gamble(clause_vector& clauses); 112 void find_onehot(clause_vector& clauses); 113 void find_dot(clause_vector& clauses); 114 115 116 public: 117 npn3_finder(solver& s); ~npn3_finder()118 ~npn3_finder() {} set_on_mux(std::function<void (literal head,literal cond,literal th,literal el)> const & f)119 void set_on_mux(std::function<void(literal head, literal cond, literal th, literal el)> const& f) { m_on_mux = f; } set_on_maj(std::function<void (literal head,literal a,literal b,literal c)> const & f)120 void set_on_maj(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_maj = f; } set_on_orand(std::function<void (literal head,literal a,literal b,literal c)> const & f)121 void set_on_orand(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_orand = f; } set_on_and(std::function<void (literal head,literal a,literal b,literal c)> const & f)122 void set_on_and(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_and = f; } set_on_xor(std::function<void (literal head,literal a,literal b,literal c)> const & f)123 void set_on_xor(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_xor = f; } set_on_andxor(std::function<void (literal head,literal a,literal b,literal c)> const & f)124 void set_on_andxor(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_andxor = f; } set_on_xorand(std::function<void (literal head,literal a,literal b,literal c)> const & f)125 void set_on_xorand(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_xorand = f; } set_on_gamble(std::function<void (literal head,literal a,literal b,literal c)> const & f)126 void set_on_gamble(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_gamble = f; } set_on_onehot(std::function<void (literal head,literal a,literal b,literal c)> const & f)127 void set_on_onehot(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_onehot = f; } set_on_dot(std::function<void (literal head,literal a,literal b,literal c)> const & f)128 void set_on_dot(std::function<void(literal head, literal a, literal b, literal c)> const& f) { m_on_dot = f; } 129 void operator()(clause_vector& clauses); 130 }; 131 } 132