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