1 /*++ 2 Copyright (c) 2020 Microsoft Corporation 3 4 Module Name: 5 6 sat_lut_finder.h 7 8 Abstract: 9 10 lut finder 11 12 Author: 13 14 Nikolaj Bjorner 2020-02-03 15 16 Notes: 17 18 Find LUT with small input fan-ins 19 20 --*/ 21 22 #pragma once 23 24 #include "util/params.h" 25 #include "util/statistics.h" 26 #include "sat/sat_clause.h" 27 #include "sat/sat_types.h" 28 #include "sat/sat_solver.h" 29 30 namespace sat { 31 32 class lut_finder { 33 solver& s; 34 struct clause_filter { 35 unsigned m_filter; 36 clause* m_clause; clause_filterclause_filter37 clause_filter(unsigned f, clause* cp): 38 m_filter(f), m_clause(cp) {} 39 }; 40 unsigned m_max_lut_size; 41 vector<svector<clause_filter>> m_clause_filters; // index of clauses. 42 uint64_t m_combination; // bit-mask of parities that have been found 43 unsigned m_num_combinations; 44 clause_vector m_clauses_to_remove; // remove clauses that become luts 45 unsigned_vector m_var_position; // position of var in main clause 46 bool_var_vector m_vars; // reference to variables being tested for LUT 47 literal_vector m_clause; // reference clause with literals sorted according to main clause 48 unsigned_vector m_missing; // set of indices not occurring in clause. 49 uint64_t m_masks[7]; 50 clause_vector m_removed_clauses; 51 std::function<void (uint64_t, svector<bool_var> const& vars, bool_var v)> m_on_lut; 52 53 void set_combination(unsigned mask); get_combination(unsigned mask)54 inline bool get_combination(unsigned mask) const { return (m_combination & (1ull << mask)) != 0; } 55 bool lut_is_defined(unsigned sz); 56 bool lut_is_defined(unsigned i, unsigned sz); 57 uint64_t convert_combination(bool_var_vector& vars, bool_var& v); 58 void check_lut(clause& c); 59 void add_lut(); 60 bool extract_lut(literal l1, literal l2); 61 bool extract_lut(clause& c2); 62 bool update_combinations(unsigned mask); 63 void init_clause_filter(); 64 void init_clause_filter(clause_vector& clauses); 65 unsigned get_clause_filter(clause const& c); 66 std::ostream& display_mask(std::ostream& out, uint64_t mask, unsigned sz) const; 67 68 public: lut_finder(solver & s)69 lut_finder(solver& s) : s(s), m_max_lut_size(5) { 70 memset(m_masks, 0, sizeof(uint64_t)*7); 71 } ~lut_finder()72 ~lut_finder() {} 73 set(std::function<void (uint64_t,bool_var_vector const &,bool_var)> & f)74 void set(std::function<void (uint64_t, bool_var_vector const&, bool_var)>& f) { m_on_lut = f; } 75 max_lut_size()76 unsigned max_lut_size() const { return m_max_lut_size; } 77 void operator()(clause_vector& clauses); 78 79 }; 80 } 81