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