1 #include "sat/sat_solver.h"
2 #include "sat/sat_npn3_finder.h"
3
4 #include <fstream>
5 #include <functional>
6 #include <iostream>
7
_init_solver(sat::solver & s)8 static void _init_solver(sat::solver& s)
9 {
10 s.mk_var();
11 s.mk_var();
12 s.mk_var();
13 s.mk_var();
14 }
15
_mk_clause4(sat::solver & s,sat::literal w,sat::literal x,sat::literal y,sat::literal z)16 static void _mk_clause4(sat::solver& s, sat::literal w, sat::literal x, sat::literal y, sat::literal z)
17 {
18 sat::literal lits[] = {w, x, y, z};
19 s.mk_clause(4, lits);
20 }
21
22 template<class CbFn>
_check_finder(sat::solver & s,CbFn && fn,const std::string & name,unsigned head_exp,unsigned a_exp,unsigned b_exp,unsigned c_exp)23 static void _check_finder(sat::solver& s, CbFn&& fn, const std::string& name, unsigned head_exp, unsigned a_exp, unsigned b_exp, unsigned c_exp)
24 {
25 using namespace std::placeholders;
26
27 uint32_t found{0u};
28 sat::npn3_finder f_npn(s);
29 fn(f_npn, [&](sat::literal head, sat::literal a, sat::literal b, sat::literal c) {
30 std::cout << "[" << name << "]\n";
31 ENSURE(head.to_uint() == head_exp && a.to_uint() == a_exp && b.to_uint() == b_exp && c.to_uint() == c_exp);
32 ++found;
33 });
34 sat::clause_vector clauses(s.clauses());
35 f_npn(clauses);
36 ENSURE(found == 1u);
37 }
38
tst_single_mux()39 static void tst_single_mux() {
40 reslimit r;
41 sat::solver s({}, r);
42 _init_solver(s);
43
44 s.mk_clause({ 0, true }, { 1, true }, { 3, false });
45 s.mk_clause({ 0, true }, { 1, false }, { 3, true });
46 s.mk_clause({ 0, false }, { 2, true }, { 3, false });
47 s.mk_clause({ 0, false }, { 2, false }, { 3, true });
48
49 _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_mux), "mux", 7, 0, 3, 5);
50 }
51
tst_single_maj()52 static void tst_single_maj() {
53 reslimit r;
54 sat::solver s({}, r);
55 _init_solver(s);
56
57 s.mk_clause({ 0, false }, { 1, false }, { 3, true });
58 s.mk_clause({ 0, false }, { 2, false }, { 3, true });
59 s.mk_clause({ 1, false }, { 2, false }, { 3, true });
60 s.mk_clause({ 0, true }, { 1, true }, { 3, false });
61 s.mk_clause({ 0, true }, { 2, true }, { 3, false });
62 s.mk_clause({ 1, true }, { 2, true }, { 3, false });
63
64 _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_maj), "maj", 6, 0, 2, 4);
65 }
66
tst_single_orand()67 static void tst_single_orand() {
68 reslimit r;
69 sat::solver s({}, r);
70 _init_solver(s);
71
72 s.mk_clause({0, false}, {3, true});
73 s.mk_clause({1, false}, {2, false}, {3, true});
74 s.mk_clause({0, true}, {1, true}, {3, false});
75 s.mk_clause({0, true}, {2, true}, {3, false});
76
77 _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_orand), "orand", 6, 0, 2, 4);
78 }
79
tst_single_and()80 static void tst_single_and() {
81 reslimit r;
82 sat::solver s({}, r);
83 _init_solver(s);
84
85 sat::literal ls1[] = {{0, true}, {1, true}, {2, true}, {3, false}};
86 s.mk_clause(4, ls1);
87 s.mk_clause({0, false}, {3, true});
88 s.mk_clause({1, false}, {3, true});
89 s.mk_clause({2, false}, {3, true});
90
91 _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_and), "and", 6, 0, 2, 4);
92 }
93
tst_single_xor()94 static void tst_single_xor() {
95 reslimit r;
96 sat::solver s({}, r);
97 _init_solver(s);
98
99 _mk_clause4(s, {0, true}, {1, false}, {2, false}, {3, false});
100 _mk_clause4(s, {0, false}, {1, true}, {2, false}, {3, false});
101 _mk_clause4(s, {0, false}, {1, false}, {2, true}, {3, false});
102 _mk_clause4(s, {0, false}, {1, false}, {2, false}, {3, true});
103 _mk_clause4(s, {0, false}, {1, true}, {2, true}, {3, true});
104 _mk_clause4(s, {0, true}, {1, false}, {2, true}, {3, true});
105 _mk_clause4(s, {0, true}, {1, true}, {2, false}, {3, true});
106 _mk_clause4(s, {0, true}, {1, true}, {2, true}, {3, false});
107
108 _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_xor), "xor", 1, 3, 4, 6);
109 }
110
tst_single_andxor()111 static void tst_single_andxor() {
112 reslimit r;
113 sat::solver s({}, r);
114 _init_solver(s);
115
116 s.mk_clause({0, true}, {1, false}, {3, true});
117 s.mk_clause({0, true}, {2, false}, {3, true});
118 _mk_clause4(s, {0, true}, {1, true}, {2, true}, {3, false});
119 s.mk_clause({0, false}, {1, false}, {3, false});
120 s.mk_clause({0, false}, {2, false}, {3, false});
121 _mk_clause4(s, {0, false}, {1, true}, {2, true}, {3, true});
122
123 _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_andxor), "andxor", 0, 6, 2, 4);
124 }
125
tst_single_xorand()126 static void tst_single_xorand() {
127 reslimit r;
128 sat::solver s({}, r);
129 _init_solver(s);
130
131 s.mk_clause({0, false}, {3, true});
132 s.mk_clause({1, false}, {2, false}, {3, true});
133 s.mk_clause({1, true}, {2, true}, {3, true});
134 _mk_clause4(s, {0, true}, {1, true}, {2, false}, {3, false});
135 _mk_clause4(s, {0, true}, {1, false}, {2, true}, {3, false});
136
137 _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_xorand), "xorand", 6, 0, 3, 5);
138 }
139
tst_single_gamble()140 static void tst_single_gamble() {
141 reslimit r;
142 sat::solver s({}, r);
143 _init_solver(s);
144
145 s.mk_clause({0, true}, {1, false}, {3, true});
146 s.mk_clause({1, true}, {2, false}, {3, true});
147 s.mk_clause({0, false}, {2, true}, {3, true});
148 _mk_clause4(s, {0, false}, {1, false}, {2, false}, {3, false});
149 _mk_clause4(s, {0, true}, {1, true}, {2, true}, {3, false});
150
151 _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_gamble), "gamble", 6, 0, 2, 4);
152 }
153
tst_single_onehot()154 static void tst_single_onehot() {
155 reslimit r;
156 sat::solver s({}, r);
157 _init_solver(s);
158
159 s.mk_clause({0, true}, {1, true}, {3, true});
160 s.mk_clause({0, true}, {2, true}, {3, true});
161 s.mk_clause({1, true}, {2, true}, {3, true});
162 _mk_clause4(s, {0, false}, {1, false}, {2, false}, {3, true});
163 _mk_clause4(s, {0, true}, {1, false}, {2, false}, {3, false});
164 _mk_clause4(s, {0, false}, {1, true}, {2, false}, {3, false});
165 _mk_clause4(s, {0, false}, {1, false}, {2, true}, {3, false});
166
167 _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_onehot), "onehot", 6, 0, 2, 4);
168 }
169
tst_single_dot()170 static void tst_single_dot() {
171 reslimit r;
172 sat::solver s({}, r);
173 _init_solver(s);
174
175 s.mk_clause({0, false}, {2, false}, {3, true});
176 s.mk_clause({0, true}, {1, true}, {3, true});
177 s.mk_clause({0, true}, {2, true}, {3, true});
178 s.mk_clause({0, false}, {2, true}, {3, false});
179 _mk_clause4(s, {0, true}, {1, false}, {2, false}, {3, false});
180
181 _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_dot), "dot", 6, 0, 2, 4);
182 }
183
tst_finder()184 void tst_finder() {
185 tst_single_mux();
186 tst_single_maj();
187 tst_single_orand();
188 tst_single_and();
189 tst_single_xor();
190 tst_single_andxor();
191 tst_single_xorand();
192 tst_single_gamble();
193 tst_single_onehot();
194 tst_single_dot();
195 }
196