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