Branch data Line data Source code
1 : : #include <mutable/IR/CNF.hpp>
2 : :
3 : : #include <mutable/parse/AST.hpp>
4 : : #include "parse/ASTPrinter.hpp"
5 : : #include <mutable/util/fn.hpp>
6 : : #include <mutable/util/macro.hpp>
7 : :
8 : :
9 : : using namespace m;
10 : : using namespace m::ast;
11 : : using namespace m::cnf;
12 : :
13 : :
14 : : /*======================================================================================================================
15 : : * CNF Operations
16 : : *====================================================================================================================*/
17 : :
18 : 152 : bool cnf::Clause::operator<=(const Clause &other) const
19 : : {
20 [ + + ]: 344 : for (auto pred : *this) {
21 [ + + ]: 230 : if (not contains(other, pred))
22 : 38 : return false;
23 : : }
24 : 114 : return true;
25 : 152 : }
26 : :
27 : 35 : bool CNF::operator<=(const CNF &other) const
28 : : {
29 [ + + ]: 71 : for (auto clause : *this) {
30 [ + - + + ]: 41 : if (not contains(other, clause))
31 : 5 : return false;
32 [ - + + ]: 41 : }
33 : 30 : return true;
34 : 35 : }
35 : :
36 : 13 : cnf::Clause cnf::operator||(const cnf::Clause &lhs, const cnf::Clause &rhs)
37 : : {
38 : 13 : cnf::Clause res;
39 [ + - ]: 13 : res.reserve(lhs.size() + rhs.size());
40 [ + - ]: 13 : res.insert(res.end(), lhs.begin(), lhs.end());
41 [ + - ]: 13 : res.insert(res.end(), rhs.begin(), rhs.end());
42 : 13 : return res;
43 [ + - ]: 13 : }
44 : :
45 : 1 : CNF cnf::operator&&(const cnf::Clause &lhs, const cnf::Clause &rhs)
46 : : {
47 : 1 : CNF res;
48 [ + - ]: 1 : res.push_back(lhs);
49 [ + - ]: 1 : res.push_back(rhs);
50 : 1 : return res;
51 [ + - ]: 1 : }
52 : :
53 : 208 : CNF cnf::operator&&(const CNF &lhs, const CNF &rhs)
54 : : {
55 : 208 : CNF res;
56 [ + - ]: 208 : res.reserve(lhs.size() + rhs.size());
57 [ + - ]: 208 : res.insert(res.end(), lhs.begin(), lhs.end());
58 [ + - ]: 208 : res.insert(res.end(), rhs.begin(), rhs.end());
59 : 208 : return res;
60 [ + - ]: 208 : }
61 : :
62 : 7 : CNF cnf::operator||(const CNF &lhs, const CNF &rhs)
63 : : {
64 : 7 : CNF res;
65 [ + + ]: 7 : if (lhs.size() == 0)
66 [ + - ]: 1 : return rhs;
67 [ - + ]: 6 : else if (rhs.size() == 0)
68 [ # # ]: 0 : return lhs;
69 : :
70 [ + - ]: 6 : res.reserve(lhs.size() * rhs.size());
71 [ + + ]: 14 : for (auto &clause_left : lhs) {
72 [ + + ]: 20 : for (auto &clause_right : rhs)
73 [ + - + - ]: 12 : res.push_back(clause_left or clause_right);
74 : 1 : }
75 : 6 : return res;
76 : 7 : }
77 : :
78 : 3 : CNF cnf::operator!(const cnf::Clause &clause)
79 : : {
80 : 3 : CNF res;
81 [ + + ]: 9 : for (auto &p : clause)
82 [ + - - + : 6 : res.emplace_back(Clause({not p}));
- + ]
83 : 3 : return res;
84 [ + - ]: 3 : }
85 : :
86 : 1 : CNF cnf::operator!(const CNF &cnf)
87 : : {
88 : 1 : CNF res;
89 [ + + ]: 3 : for (auto &clause : cnf)
90 [ + - + - ]: 2 : res = res or not clause;
91 : 1 : return res;
92 [ + - ]: 1 : }
93 : :
94 : :
95 : : /*======================================================================================================================
96 : : * Print/Dump
97 : : *====================================================================================================================*/
98 : :
99 : 0 : void Predicate::to_sql(std::ostream &out) const
100 : : {
101 [ # # ]: 0 : if (negative())
102 : 0 : out << "NOT (" << expr() << ')';
103 : : else
104 : 0 : out << expr();
105 : 0 : }
106 : :
107 : 0 : void cnf::Clause::to_sql(std::ostream &out) const
108 : : {
109 [ # # # ]: 0 : switch (size()) {
110 : : case 0:
111 : 0 : out << "TRUE";
112 : 0 : return;
113 : :
114 : : case 1:
115 : 0 : out << *begin();
116 : 0 : return;
117 : :
118 : : default:
119 [ # # ]: 0 : for (auto it = begin(); it != end(); ++it) {
120 [ # # ]: 0 : if (it != begin()) out << " OR ";
121 : 0 : out << '(' << *it << ')';
122 : 0 : }
123 : 0 : return;
124 : : }
125 : 0 : }
126 : :
127 : 0 : void CNF::to_sql(std::ostream &out) const
128 : : {
129 [ # # # ]: 0 : switch (size()) {
130 : : case 0:
131 : 0 : out << "TRUE";
132 : 0 : return;
133 : :
134 : : case 1:
135 : 0 : out << *begin();
136 : 0 : return;
137 : :
138 : : default:
139 [ # # ]: 0 : for (auto it = begin(); it != end(); ++it) {
140 [ # # ]: 0 : if (it != begin()) out << " AND ";
141 : 0 : out << *it;
142 : 0 : }
143 : 0 : return;
144 : : }
145 : 0 : }
146 : :
147 : : M_LCOV_EXCL_START
148 : : std::ostream & cnf::operator<<(std::ostream &out, const Predicate &pred)
149 : : {
150 : : if (pred.negative())
151 : : out << '-';
152 : : ast::ASTPrinter print(out);
153 : : print.expand_nested_queries(false);
154 : : print(*pred);
155 : : return out;
156 : : }
157 : :
158 : : std::ostream & cnf::operator<<(std::ostream &out, const cnf::Clause &clause)
159 : : {
160 : : for (auto it = clause.begin(); it != clause.end(); ++it) {
161 : : if (it != clause.begin()) out << " v ";
162 : : out << *it;
163 : : }
164 : : return out;
165 : : }
166 : :
167 : : std::ostream & cnf::operator<<(std::ostream &out, const CNF &cnf)
168 : : {
169 : : if (cnf.empty())
170 : : out << "TRUE";
171 : : else if (cnf.size() == 1)
172 : : out << cnf[0];
173 : : else {
174 : : for (auto it = cnf.begin(); it != cnf.end(); ++it) {
175 : : if (it != cnf.begin()) out << " ^ ";
176 : : out << '(' << *it << ')';
177 : : }
178 : : }
179 : : return out;
180 : : }
181 : :
182 : : void Predicate::dump(std::ostream &out) const
183 : : {
184 : : out << *this << std::endl;
185 : : }
186 : : void Predicate::dump() const { dump(std::cerr); }
187 : :
188 : : void cnf::Clause::dump(std::ostream &out) const
189 : : {
190 : : out << *this << std::endl;
191 : : }
192 : : void cnf::Clause::dump() const { dump(std::cerr); }
193 : :
194 : : void CNF::dump(std::ostream &out) const
195 : : {
196 : : out << *this << std::endl;
197 : : }
198 : : void CNF::dump() const { dump(std::cerr); }
199 : : M_LCOV_EXCL_STOP
200 : :
201 : :
202 : : /*======================================================================================================================
203 : : * CNF Generator
204 : : *====================================================================================================================*/
205 : :
206 : : /** Helper class to convert `Expr` and `Clause` to `cnf::CNF`. */
207 : : struct CNFGenerator : ConstASTExprVisitor
208 : : {
209 : : private:
210 : 162 : bool is_negative_ = false;
211 : : CNF result_;
212 : :
213 : : public:
214 : 324 : CNFGenerator() { }
215 : :
216 : 162 : CNF get() const { return result_; }
217 : :
218 : : using ConstASTExprVisitor::operator();
219 : : void operator()(Const<ErrorExpr> &e);
220 : : void operator()(Const<Designator> &e);
221 : : void operator()(Const<Constant> &e);
222 : : void operator()(Const<FnApplicationExpr> &e);
223 : : void operator()(Const<UnaryExpr> &e);
224 : : void operator()(Const<BinaryExpr> &e);
225 : : void operator()(Const<QueryExpr> &e);
226 : : };
227 : :
228 : 0 : void CNFGenerator::operator()(Const<ErrorExpr> &e)
229 : : {
230 [ # # # # : 0 : result_ = CNF({cnf::Clause({Predicate::Create(&e, is_negative_)})});
# # # # ]
231 : 0 : }
232 : :
233 : 10 : void CNFGenerator::operator()(Const<Designator> &e)
234 : : {
235 [ + - + - : 10 : result_ = CNF({cnf::Clause({Predicate::Create(&e, is_negative_)})});
+ - # # ]
236 : 10 : }
237 : :
238 : 27 : void CNFGenerator::operator()(Const<Constant> &e)
239 : : {
240 [ + - + - : 27 : result_ = CNF({cnf::Clause({Predicate::Create(&e, is_negative_)})});
+ - # # ]
241 : 27 : }
242 : :
243 : 0 : void CNFGenerator::operator()(Const<FnApplicationExpr> &e)
244 : : {
245 [ # # # # : 0 : result_ = CNF({cnf::Clause({Predicate::Create(&e, is_negative_)})});
# # # # ]
246 : 0 : }
247 : :
248 : 12 : void CNFGenerator::operator()(Const<UnaryExpr> &e)
249 : : {
250 [ + - ]: 12 : switch (e.op().type) {
251 : : case TK_Not:
252 : 12 : is_negative_ = not is_negative_;
253 : 12 : (*this)(*e.expr);
254 : 12 : is_negative_ = not is_negative_;
255 : 12 : break;
256 : :
257 : : default:
258 [ # # # # : 0 : result_ = CNF({cnf::Clause({Predicate::Create(&e, is_negative_)})});
# # # # ]
259 : 0 : break;
260 : :
261 : : }
262 : 12 : }
263 : :
264 : 519 : void CNFGenerator::operator()(Const<BinaryExpr> &e)
265 : : {
266 [ + + - + ]: 519 : if (e.lhs->type()->is_boolean() and e.rhs->type()->is_boolean()) {
267 : : /* This is an expression in predicate logic. Convert to CNF. */
268 : 197 : (*this)(*e.lhs);
269 : 197 : auto cnf_lhs = result_;
270 [ + - ]: 197 : (*this)(*e.rhs);
271 [ + - ]: 197 : auto cnf_rhs = result_;
272 : :
273 [ + + + - : 197 : if ((not is_negative_ and e.op() == TK_And) or (is_negative_ and e.op() == TK_Or)) {
+ - + + +
+ + - + -
+ + + + +
+ # # #
# ]
274 [ + - ]: 193 : result_ = cnf_lhs and cnf_rhs;
275 [ + - + - : 197 : } else if ((not is_negative_ and e.op() == TK_Or) or (is_negative_ and e.op() == TK_And)) {
+ - + - #
# # # # #
+ - - + +
- # # #
# ]
276 [ + - ]: 4 : result_ = cnf_lhs or cnf_rhs;
277 [ # # # # : 4 : } else if (e.op() == TK_EQUAL or e.op() == TK_BANG_EQUAL) {
# # # # #
# # # # #
# # ]
278 : : /* A ↔ B ⇔ (A → B) ^ (B → A) ⇔ (¬A v B) ^ (¬B v A) */
279 [ # # # # : 0 : auto equiv = ((not cnf_lhs) or cnf_rhs) and ((not cnf_rhs) or cnf_lhs);
# # # # #
# ]
280 [ # # # # : 0 : if ((not is_negative_ and e.op() == TK_BANG_EQUAL) or (is_negative_ and e.op() == TK_EQUAL))
# # # # #
# # # # #
# # # # #
# # # #
# ]
281 [ # # ]: 0 : result_ = not equiv; // A ↮ B ⇔ ¬(A ↔ B)
282 : : else
283 [ # # ]: 0 : result_ = equiv;
284 : 0 : } else {
285 [ # # ]: 0 : M_unreachable("unsupported boolean expression");
286 : : }
287 : 197 : } else {
288 : : /* This expression is a literal. */
289 [ + - + - : 322 : result_ = CNF({cnf::Clause({Predicate::Create(&e, is_negative_)})});
+ - # # ]
290 : : }
291 : 519 : }
292 : :
293 : 0 : void CNFGenerator::operator()(Const<QueryExpr> &e)
294 : : {
295 [ # # # # : 0 : result_ = CNF({cnf::Clause({Predicate::Create(&e, is_negative_)})});
# # # # ]
296 : 0 : }
297 : :
298 : 162 : CNF cnf::to_CNF(const Expr &e)
299 : : {
300 : 162 : CNFGenerator G;
301 [ + - ]: 162 : G(e);
302 [ + - ]: 162 : return G.get();
303 : 162 : }
|
