1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 #include "mcsat/bool/cnf.h"
20
21 #include "mcsat/tracing.h"
22
cnf_construct(cnf_t * cnf,plugin_context_t * ctx,clause_db_t * clause_db)23 void cnf_construct(cnf_t* cnf, plugin_context_t* ctx, clause_db_t* clause_db) {
24 cnf->clause_db = clause_db;
25 cnf->ctx = ctx;
26 cnf->variable = variable_null;
27 int_lset_construct(&cnf->converted);
28 }
29
cnf_destruct(cnf_t * cnf)30 void cnf_destruct(cnf_t* cnf) {
31 int_lset_destruct(&cnf->converted);
32 }
33
34 static
cnf_is_converted(const cnf_t * cnf,variable_t var)35 bool cnf_is_converted(const cnf_t* cnf, variable_t var) {
36 return int_lset_has_list(&cnf->converted, var);
37 }
38
39 static
cnf_begin(cnf_t * cnf,variable_t var)40 void cnf_begin(cnf_t* cnf, variable_t var) {
41 assert(!cnf_is_converted(cnf, var));
42 cnf->variable = var;
43 }
44
45 static
cnf_end(cnf_t * cnf)46 void cnf_end(cnf_t* cnf) {
47 cnf->variable = variable_null;
48 }
49
50 static
cnf_remove(cnf_t * cnf,variable_t var)51 void cnf_remove(cnf_t* cnf, variable_t var) {
52 int_lset_remove(&cnf->converted, var);
53 }
54
55 static
cnf_add_clause(cnf_t * cnf,const mcsat_literal_t * lits,uint32_t lits_size,ivector_t * clauses_out,mcsat_clause_tag_t tag)56 void cnf_add_clause(cnf_t* cnf, const mcsat_literal_t* lits, uint32_t lits_size, ivector_t* clauses_out, mcsat_clause_tag_t tag) {
57 uint32_t i, keep;
58 clause_ref_t clause_ref;
59 mcsat_literal_t* lits_copy;
60
61 lits_copy = NULL;
62
63 if (ctx_trace_enabled(cnf->ctx, "bool::cnf")) {
64 ctx_trace_printf(cnf->ctx, "cnf_add_clause:");
65 literals_print(lits, lits_size, cnf->ctx->var_db, ctx_trace_out(cnf->ctx));
66 ctx_trace_printf(cnf->ctx, "\n");
67 }
68
69 // Make a copy of the literals
70 lits_copy = safe_malloc(sizeof(mcsat_literal_t) * lits_size);
71 for (i = 0, keep = 0; i < lits_size; ++ i) {
72 if (literal_has_value(lits[i], cnf->ctx->trail)) {
73 if (literal_get_value(lits[i], cnf->ctx->trail)) {
74 // true literal, true clause
75 goto finish;
76 } else {
77 // false literal, just skip it
78 }
79 }
80 lits_copy[keep ++] = lits[i];
81 }
82 lits_size = keep;
83
84 if (ctx_trace_enabled(cnf->ctx, "bool::cnf")) {
85 ctx_trace_printf(cnf->ctx, "cnf_add_clause: after simpl: ");
86 literals_print(lits_copy, lits_size, cnf->ctx->var_db, ctx_trace_out(cnf->ctx));
87 ctx_trace_printf(cnf->ctx, "\n");
88 }
89
90 // Add the clause
91 clause_ref = clause_db_new_clause(cnf->clause_db, lits_copy, lits_size, tag);
92 ivector_push(clauses_out, clause_ref);
93 assert(clause_db_is_clause(cnf->clause_db, clause_ref, true));
94
95 // If defining a variable, remember it
96 assert(cnf->variable == variable_null || tag.type == CLAUSE_DEFINITION);
97 if (cnf->variable != variable_null) {
98 assert(tag.var == cnf->variable);
99 int_lset_add(&cnf->converted, cnf->variable, clause_ref);
100 }
101
102 finish:
103 safe_free(lits_copy);
104 }
105
106 static
cnf_convert_or(cnf_t * cnf,term_t or,ivector_t * or_clauses)107 void cnf_convert_or(cnf_t* cnf, term_t or, ivector_t* or_clauses) {
108 uint32_t i;
109 composite_term_t* or_composite;
110 mcsat_literal_t* or_literals;
111 mcsat_clause_tag_t or_tag;
112
113 assert(term_kind(cnf->ctx->terms, or) == OR_TERM);
114
115 // Get the or description
116 or_composite = composite_term_desc(cnf->ctx->terms, or);
117 or_tag.type = CLAUSE_DEFINITION;
118 or_tag.var = variable_db_get_variable(cnf->ctx->var_db, or);
119 or_tag.level = cnf->ctx->trail->decision_level_base;
120
121 // Make some space
122 or_literals = safe_malloc(sizeof(mcsat_literal_t) * (or_composite->arity + 1));
123
124 or_literals[0] = literal_construct(or_tag.var, true);
125 for (i = 0; i < or_composite->arity; ++ i) {
126 or_literals[i + 1] = cnf_convert(cnf, or_composite->arg[i], or_clauses);
127 }
128
129 cnf_begin(cnf, or_tag.var);
130
131 // a => (or t1 ... tn)
132 // (or !a t1 ... tn)
133 cnf_add_clause(cnf, or_literals, or_composite->arity + 1, or_clauses, or_tag);
134
135 // a <= (or t1 ... tn)
136 // (a or !t1) ... (a or !tn)
137 or_literals[0] = literal_construct(or_tag.var, false);
138 for (i = 0; i < or_composite->arity; ++ i) {
139 or_literals[1] = literal_negate(or_literals[i + 1]);
140 cnf_add_clause(cnf, or_literals, 2, or_clauses, or_tag);
141 }
142
143 cnf_end(cnf);
144
145 // Free the children
146 safe_free(or_literals);
147 }
148
149 static
cnf_convert_xor(cnf_t * cnf,term_t xor,ivector_t * xor_clauses)150 void cnf_convert_xor(cnf_t* cnf, term_t xor, ivector_t* xor_clauses) {
151 composite_term_t* xor_composite;
152 mcsat_clause_tag_t xor_tag;
153 mcsat_literal_t xor_literals[3];
154
155 assert(term_kind(cnf->ctx->terms, xor) == XOR_TERM);
156
157 // Get the or description
158 xor_composite = composite_term_desc(cnf->ctx->terms, xor);
159 assert(xor_composite->arity >= 2);
160
161 xor_tag.type = CLAUSE_DEFINITION;
162 xor_tag.var = variable_db_get_variable(cnf->ctx->var_db, xor);
163 xor_tag.level = cnf->ctx->trail->decision_level_base;
164
165 // Get the arguments
166 term_t t1 = xor_composite->arg[0];
167 term_t t2;
168 if (xor_composite->arity == 2) {
169 t2 = xor_composite->arg[1];
170 } else {
171 t2 = mk_xor_safe(cnf->ctx->tm, xor_composite->arity-1, xor_composite->arg+1);
172 }
173
174 // Convert the children and setup the literals
175 mcsat_literal_t xor_lit, t1_lit, t2_lit;
176 t1_lit = cnf_convert(cnf, t1, xor_clauses);
177 t2_lit = cnf_convert(cnf, t2, xor_clauses);
178 xor_lit = literal_construct(xor_tag.var, false);
179
180 cnf_begin(cnf, xor_tag.var);
181
182 // a => (xor t1 t2)
183 // (!a or t1 or t2) and (!a or !t1 or !t2)
184
185 xor_literals[0] = literal_negate(xor_lit);
186
187 xor_literals[1] = t1_lit;
188 xor_literals[2] = t2_lit;
189 cnf_add_clause(cnf, xor_literals, 3, xor_clauses, xor_tag);
190
191 xor_literals[1] = literal_negate(t1_lit);
192 xor_literals[2] = literal_negate(t2_lit);
193 cnf_add_clause(cnf, xor_literals, 3, xor_clauses, xor_tag);
194
195 // a <= (xor t1 t2)
196 // (a or t1 or !t2) and (a or !t1 or t2)
197
198 xor_literals[0] = xor_lit;
199
200 xor_literals[1] = t1_lit;
201 xor_literals[2] = literal_negate(t2_lit);
202 cnf_add_clause(cnf, xor_literals, 3, xor_clauses, xor_tag);
203
204 xor_literals[1] = literal_negate(t1_lit);
205 xor_literals[2] = t2_lit;
206 cnf_add_clause(cnf, xor_literals, 3, xor_clauses, xor_tag);
207
208 cnf_end(cnf);
209 }
210
211 static
cnf_convert_eq(cnf_t * cnf,term_t eq,ivector_t * eq_clauses)212 void cnf_convert_eq(cnf_t* cnf, term_t eq, ivector_t* eq_clauses) {
213 composite_term_t* eq_composite;
214 mcsat_literal_t eq_literals[3];
215 mcsat_clause_tag_t eq_tag;
216 mcsat_literal_t a, b;
217
218 // Get the eq description
219 assert(term_kind(cnf->ctx->terms, eq) == EQ_TERM);
220 eq_composite = composite_term_desc(cnf->ctx->terms, eq);
221 assert(eq_composite->arity == 2);
222
223 eq_tag.type = CLAUSE_DEFINITION;
224 eq_tag.var = variable_db_get_variable(cnf->ctx->var_db, eq);
225 eq_tag.level = cnf->ctx->trail->decision_level_base;
226
227 // Convert the children
228 a = cnf_convert(cnf, eq_composite->arg[0], eq_clauses);
229 b = cnf_convert(cnf, eq_composite->arg[1], eq_clauses);
230
231 cnf_begin(cnf, eq_tag.var);
232
233 // eq => (!a | b) & (a | !b)
234 // (!eq | !a | b) & (!eq | a | !b)
235 eq_literals[0] = literal_construct(eq_tag.var, true);
236
237 eq_literals[1] = literal_negate(a);
238 eq_literals[2] = b;
239 cnf_add_clause(cnf, eq_literals, 3, eq_clauses, eq_tag);
240
241 eq_literals[1] = a;
242 eq_literals[2] = literal_negate(b);
243 cnf_add_clause(cnf, eq_literals, 3, eq_clauses, eq_tag);
244
245 // !eq => (a | b) & (!a | !b)
246 // (eq | a | b) & (eq | !a | !b)
247 eq_literals[0] = literal_construct(eq_tag.var, false);
248
249 eq_literals[1] = a;
250 eq_literals[2] = b;
251 cnf_add_clause(cnf, eq_literals, 3, eq_clauses, eq_tag);
252
253 eq_literals[1] = literal_negate(a);
254 eq_literals[2] = literal_negate(b);
255 cnf_add_clause(cnf, eq_literals, 3, eq_clauses, eq_tag);
256
257 cnf_end(cnf);
258 }
259
260 static
cnf_convert_ite(cnf_t * cnf,term_t ite,ivector_t * ite_clauses)261 void cnf_convert_ite(cnf_t* cnf, term_t ite, ivector_t* ite_clauses) {
262 composite_term_t* ite_composite;
263 mcsat_literal_t ite_literals[3];
264 mcsat_clause_tag_t ite_tag;
265 mcsat_literal_t cond, b_true, b_false;
266
267 // Get the ite description
268 assert(is_ite_term(cnf->ctx->terms, ite));
269 ite_composite = composite_term_desc(cnf->ctx->terms, ite);
270 assert(ite_composite->arity == 3);
271
272 ite_tag.type = CLAUSE_DEFINITION;
273 ite_tag.var = variable_db_get_variable(cnf->ctx->var_db, ite);
274 ite_tag.level = cnf->ctx->trail->decision_level_base;
275
276 // Convert the children
277 cond = cnf_convert(cnf, ite_composite->arg[0], ite_clauses);
278 b_true= cnf_convert(cnf, ite_composite->arg[1], ite_clauses);
279 b_false = cnf_convert(cnf, ite_composite->arg[2], ite_clauses);
280
281 cnf_begin(cnf, ite_tag.var);
282
283 // ite => (ite cond b_true b_false)
284 // ite => (b_true | b_false) & (cond => b_true) & (!cond => b_false)
285 // ite => (b_true | b_false) & (!cond | b_true) & (cond | b_false)
286 // (!ite | b_true | b_false) & (!ite | !cond | b_true) & (!ite | cond | b_false)
287 ite_literals[0] = literal_construct(ite_tag.var, true);
288
289 ite_literals[1] = b_true;
290 ite_literals[2] = b_false;
291 cnf_add_clause(cnf, ite_literals, 3, ite_clauses, ite_tag);
292
293 ite_literals[1] = literal_negate(cond);
294 ite_literals[2] = b_true;
295 cnf_add_clause(cnf, ite_literals, 3, ite_clauses, ite_tag);
296
297 ite_literals[1] = cond;
298 ite_literals[2] = b_false;
299 cnf_add_clause(cnf, ite_literals, 3, ite_clauses, ite_tag);
300
301 // !ite => !(ite cond b_true b_false)
302 // !ite => (!b_true | !b_false) & (cond => !b_true) & (!cond -> !b_false)
303 // !ite => (!b_true | !b_false) & (!cond | !b_true) & (cond | !b_false)
304 // (ite | !b_true | !b_false) & (ite | !cond | !b_true) & (ite | cond | !b_false)
305
306 ite_literals[0] = literal_construct(ite_tag.var, false);
307
308 ite_literals[1] = literal_negate(b_true);
309 ite_literals[2] = literal_negate(b_false);
310 cnf_add_clause(cnf, ite_literals, 3, ite_clauses, ite_tag);
311
312 ite_literals[1] = literal_negate(cond);
313 ite_literals[2] = literal_negate(b_true);
314 cnf_add_clause(cnf, ite_literals, 3, ite_clauses, ite_tag);
315
316 ite_literals[1] = cond;
317 ite_literals[2] = literal_negate(b_false);
318 cnf_add_clause(cnf, ite_literals, 3, ite_clauses, ite_tag);
319
320 cnf_end(cnf);
321 }
322
cnf_convert(cnf_t * cnf,term_t t,ivector_t * t_clauses)323 mcsat_literal_t cnf_convert(cnf_t* cnf, term_t t, ivector_t* t_clauses) {
324 bool t_negated;
325 term_kind_t t_kind;
326 mcsat_literal_t t_lit;
327 variable_t t_lit_var;
328
329 assert(is_boolean_term(cnf->ctx->terms, t));
330
331 // Only convert positive ones
332 t_negated = is_neg_term(t);
333 t = unsigned_term(t);
334
335 // The variable
336 t_lit_var = variable_db_get_variable(cnf->ctx->var_db, t);
337 t_lit = literal_construct(t_lit_var, t_negated);
338
339 // Check if converted already
340 if (!cnf_is_converted(cnf, t_lit_var)) {
341 // Convert based on the kind
342 t_kind = term_kind(cnf->ctx->terms, t);
343 switch (t_kind) {
344 case OR_TERM:
345 cnf_convert_or(cnf, t, t_clauses);
346 break;
347 case XOR_TERM:
348 cnf_convert_xor(cnf, t, t_clauses);
349 break;
350 case EQ_TERM: {
351 term_t lhs = eq_term_desc(cnf->ctx->terms, t)->arg[0];
352 type_kind_t lhs_type = term_type_kind(cnf->ctx->terms, lhs);
353 if (lhs_type == BOOL_TYPE) {
354 cnf_convert_eq(cnf, t, t_clauses);
355 }
356 break;
357 }
358 case ITE_TERM:
359 case ITE_SPECIAL:
360 cnf_convert_ite(cnf, t, t_clauses);
361 break;
362 default:
363 // We're fine, just a variable
364 break;
365 }
366 }
367
368 return t_lit;
369 }
370
cnf_convert_lemma(cnf_t * cnf,const ivector_t * lemma,ivector_t * clauses)371 void cnf_convert_lemma(cnf_t* cnf, const ivector_t* lemma, ivector_t* clauses) {
372 uint32_t i;
373 mcsat_literal_t* or_literals;
374 mcsat_clause_tag_t or_tag;
375
376 or_literals = safe_malloc(sizeof(mcsat_literal_t) * lemma->size);
377
378 for (i = 0; i < lemma->size; ++ i) {
379 or_literals[i] = cnf_convert(cnf, lemma->data[i], clauses);
380 }
381
382 or_tag.type = CLAUSE_LEMMA;
383 or_tag.score = 0;
384 or_tag.level = cnf->ctx->trail->decision_level_base;
385
386 cnf_add_clause(cnf, or_literals, lemma->size, clauses, or_tag);
387
388 safe_free(or_literals);
389 }
390
cnf_gc_mark(cnf_t * cnf,gc_info_t * gc_clauses,const gc_info_t * gc_vars)391 void cnf_gc_mark(cnf_t* cnf, gc_info_t* gc_clauses, const gc_info_t* gc_vars) {
392 static uint32_t i;
393
394 variable_t var;
395 clause_ref_t clause_ref;
396 int_lset_iterator_t it;
397
398 // If first time at gc, reset the index
399 if (gc_vars->level == 0) {
400 i = 0;
401 }
402
403 // CNF marks only the clauses that are definitions of the variables to keep
404 for (; i < gc_vars->marked.size; ++ i) {
405 var = gc_vars->marked.data[i];
406 if (trace_enabled(cnf->ctx->tracer, "mcsat::gc")) {
407 ctx_trace_term(cnf->ctx, variable_db_get_term(cnf->ctx->var_db, var));
408 }
409 if (cnf_is_converted(cnf, var)) {
410 int_lset_iterator_construct(&it, &cnf->converted, var);
411 while (!int_lset_iterator_done(&it)) {
412 clause_ref = *int_lset_iterator_get(&it);
413 assert(clause_db_is_clause(cnf->clause_db, clause_ref, true));
414 gc_info_mark(gc_clauses, clause_ref);
415 int_lset_iterator_next_and_keep(&it);
416 }
417 int_lset_iterator_destruct(&it);
418 }
419 }
420 }
421
cnf_gc_sweep(cnf_t * cnf,const gc_info_t * gc_clauses,int_mset_t * vars_undefined)422 void cnf_gc_sweep(cnf_t* cnf, const gc_info_t* gc_clauses, int_mset_t* vars_undefined) {
423
424 uint32_t i;
425 variable_t var;
426 ivector_t* vars_to_undef;
427
428 // List of variables that lost a clause of their definition
429 // we need to mark them as untranslated
430 vars_to_undef = int_mset_get_list(vars_undefined);
431 for (i = 0; i < vars_to_undef->size; ++ i) {
432 var = vars_to_undef->data[i];
433 cnf_remove(cnf, var);
434 }
435
436 // Update the converted list
437 int_lset_reloc_elements(&cnf->converted, gc_clauses);
438 }
439