-
Notifications
You must be signed in to change notification settings - Fork 1.5k
/
sat_cut_simplifier.h
174 lines (150 loc) · 6.52 KB
/
sat_cut_simplifier.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sat_cut_simplifier.h
Abstract:
extract AIG definitions from clauses
Perform cut-set enumeration to identify equivalences.
Author:
Nikolaj Bjorner 2020-01-02
--*/
#pragma once
#include "util/union_find.h"
#include "sat/sat_aig_finder.h"
#include "sat/sat_aig_cuts.h"
namespace sat {
class cut_simplifier {
public:
struct stats {
unsigned m_num_eqs, m_num_units, m_num_cuts, m_num_xors, m_num_ands, m_num_ites;
unsigned m_xxors, m_xands, m_xites, m_xluts; // extrated gates
unsigned m_num_calls, m_num_dont_care_reductions, m_num_learned_implies;
stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
};
struct config {
bool m_enable_units; // enable learning units
bool m_enable_dont_cares; // enable applying don't cares to LUTs
bool m_learn_implies; // learn binary clauses
bool m_learned2aig; // add learned clauses to AIGs used by cut-set enumeration
bool m_validate_cuts; // enable direct validation of generated cuts
bool m_validate_lemmas; // enable direct validation of learned lemmas
bool m_simulate_eqs; // use symbolic simulation to control size of cutsets.
config():
m_enable_units(true),
m_enable_dont_cares(true),
m_learn_implies(false),
m_learned2aig(true),
m_validate_cuts(false),
m_validate_lemmas(false),
m_simulate_eqs(false) {}
};
private:
struct report;
struct validator;
/**
* collect pairs of literal combinations that are impossible
* base on binary implication graph queries. Apply the masks
* on cut sets so to allow detecting equivalences modulo
* implications.
*
* The encoding is as follows:
* a or b -> op = nn because (~a & ~b) is a don't care
* ~a or b -> op = pn because (a & ~b) is a don't care
* a or ~b -> op = np because (~a & b) is a don't care
* ~a or ~b -> op = pp because (a & b) is a don't care
*
*/
enum class op_code { pp, pn, np, nn, none };
struct bin_rel {
unsigned u, v;
op_code op;
bin_rel(unsigned _u, unsigned _v): u(_u), v(_v), op(op_code::none) {
if (u > v) std::swap(u, v);
}
// convert binary clause into a bin-rel
bin_rel(literal _u, literal _v): u(_u.var()), v(_v.var()), op(op_code::none) {
if (_u.sign() && _v.sign()) op = op_code::pp;
else if (_u.sign()) op = op_code::pn;
else if (_v.sign()) op = op_code::np;
else op = op_code::nn;
if (u > v) {
std::swap(u, v);
if (op == op_code::np) op = op_code::pn;
else if (op == op_code::pn) op = op_code::np;
}
}
bin_rel(): u(UINT_MAX), v(UINT_MAX), op(op_code::none) {}
struct hash {
unsigned operator()(bin_rel const& p) const {
return p.u + 65599*p.v; // Weinberger's should be a bit cheaper mk_mix(p.u, p.v, 1);
}
};
struct eq {
bool operator()(bin_rel const& a, bin_rel const& b) const {
return a.u == b.u && a.v == b.v;
}
};
void to_binary(literal& lu, literal& lv) const {
switch (op) {
case op_code::pp: lu = literal(u, true); lv = literal(v, true); break;
case op_code::pn: lu = literal(u, true); lv = literal(v, false); break;
case op_code::np: lu = literal(u, false); lv = literal(v, true); break;
case op_code::nn: lu = literal(u, false); lv = literal(v, false); break;
default: UNREACHABLE(); break;
}
}
};
solver& s;
stats m_stats;
config m_config;
aig_cuts m_aig_cuts;
unsigned m_trail_size;
literal_vector m_lits;
validator* m_validator;
hashtable<bin_rel, bin_rel::hash, bin_rel::eq> m_bins;
void clauses2aig();
void aig2clauses();
void simulate_eqs();
void cuts2equiv(vector<cut_set> const& cuts);
void cuts2implies(vector<cut_set> const& cuts);
void uf2equiv(union_find<> const& uf);
void assign_unit(cut const& c, literal lit);
void assign_equiv(cut const& c, literal u, literal v);
void learn_implies(big& big, cut const& c, literal u, literal v);
void ensure_validator();
void validate_unit(literal lit);
void validate_eq(literal a, literal b);
void certify_unit(literal u, cut const& c);
void certify_implies(literal u, literal v, cut const& c);
void certify_equivalence(literal u, literal v, cut const& c);
void track_binary(literal u, literal v);
void untrack_binary(literal u, literal v);
void track_binary(bin_rel const& p);
void untrack_binary(bin_rel const& p);
void add_dont_cares(vector<cut_set> const& cuts);
void cuts2bins(vector<cut_set> const& cuts);
void bins2dont_cares();
void dont_cares2cuts(vector<cut_set> const& cuts);
bool add_dont_care(cut const & c);
uint64_t op2dont_care(unsigned i, unsigned j, bin_rel const& p);
public:
cut_simplifier(solver& s);
~cut_simplifier();
void operator()();
void collect_statistics(statistics& st) const;
/**
* The clausifier may know that some literal is defined as a
* function of other literals. This API is exposed so that
* the clausifier can instrument the simplifier with an initial
* AIG.
* set_root is issued from the equivalence finder.
*/
void add_and(literal head, unsigned sz, literal const* args);
void add_or(literal head, unsigned sz, literal const* args);
void add_xor(literal head, unsigned sz, literal const* args);
void add_ite(literal head, literal c, literal t, literal e);
void add_iff(literal head, literal l1, literal l2);
void set_root(bool_var v, literal r);
};
}