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