1 //===--- solver_api.h -------------------------------------------------------===
2 //
3 // satoko: Satisfiability solver
4 //
5 // This file is distributed under the BSD 2-Clause License.
6 // See LICENSE for details.
7 //
8 //===------------------------------------------------------------------------===
9 #include <stdio.h>
10 #include <assert.h>
11 #include <string.h>
12 #include <math.h>
13
14 #include "act_var.h"
15 #include "solver.h"
16 #include "utils/misc.h"
17
18 #include "misc/util/abc_global.h"
19 ABC_NAMESPACE_IMPL_START
20
21 //===------------------------------------------------------------------------===
22 // Satoko internal functions
23 //===------------------------------------------------------------------------===
solver_rebuild_order(solver_t * s)24 static inline void solver_rebuild_order(solver_t *s)
25 {
26 unsigned var;
27 vec_uint_t *vars = vec_uint_alloc(vec_char_size(s->assigns));
28
29 for (var = 0; var < vec_char_size(s->assigns); var++)
30 if (var_value(s, var) == SATOKO_VAR_UNASSING)
31 vec_uint_push_back(vars, var);
32 heap_build(s->var_order, vars);
33 vec_uint_free(vars);
34 }
35
clause_is_satisfied(solver_t * s,struct clause * clause)36 static inline int clause_is_satisfied(solver_t *s, struct clause *clause)
37 {
38 unsigned i;
39 unsigned *lits = &(clause->data[0].lit);
40 for (i = 0; i < clause->size; i++)
41 if (lit_value(s, lits[i]) == SATOKO_LIT_TRUE)
42 return SATOKO_OK;
43 return SATOKO_ERR;
44 }
45
solver_clean_stats(solver_t * s)46 static inline void solver_clean_stats(solver_t *s)
47 {
48 long n_conflicts_all = s->stats.n_conflicts_all;
49 long n_propagations_all = s->stats.n_propagations_all;
50 memset(&(s->stats), 0, sizeof(struct satoko_stats));
51 s->stats.n_conflicts_all = n_conflicts_all;
52 s->stats.n_propagations_all = n_propagations_all;
53 }
54
print_opts(solver_t * s)55 static inline void print_opts(solver_t *s)
56 {
57 printf( "+-[ BLACK MAGIC - PARAMETERS ]-+\n");
58 printf( "| |\n");
59 printf( "|--> Restarts heuristic |\n");
60 printf( "| * LBD Queue = %6d |\n", s->opts.sz_lbd_bqueue);
61 printf( "| * Trail Queue = %6d |\n", s->opts.sz_trail_bqueue);
62 printf( "| * f_rst = %6.2f |\n", s->opts.f_rst);
63 printf( "| * b_rst = %6.2f |\n", s->opts.b_rst);
64 printf( "| |\n");
65 printf( "|--> Clause DB reduction: |\n");
66 printf( "| * First = %6d |\n", s->opts.n_conf_fst_reduce);
67 printf( "| * Inc = %6d |\n", s->opts.inc_reduce);
68 printf( "| * Special Inc = %6d |\n", s->opts.inc_special_reduce);
69 printf( "| * Protected (LBD) < %2d |\n", s->opts.lbd_freeze_clause);
70 printf( "| |\n");
71 printf( "|--> Binary resolution: |\n");
72 printf( "| * Clause size < %3d |\n", s->opts.clause_max_sz_bin_resol);
73 printf( "| * Clause lbd < %3d |\n", s->opts.clause_min_lbd_bin_resol);
74 printf( "+------------------------------+\n\n");
75 }
76
print_stats(solver_t * s)77 static inline void print_stats(solver_t *s)
78 {
79 printf("starts : %10d\n", s->stats.n_starts);
80 printf("conflicts : %10ld\n", s->stats.n_conflicts);
81 printf("decisions : %10ld\n", s->stats.n_decisions);
82 printf("propagations : %10ld\n", s->stats.n_propagations);
83 }
84
85 //===------------------------------------------------------------------------===
86 // Satoko external functions
87 //===------------------------------------------------------------------------===
satoko_create()88 solver_t * satoko_create()
89 {
90 solver_t *s = satoko_calloc(solver_t, 1);
91
92 satoko_default_opts(&s->opts);
93 s->status = SATOKO_OK;
94 /* User data */
95 s->assumptions = vec_uint_alloc(0);
96 s->final_conflict = vec_uint_alloc(0);
97 /* Clauses Database */
98 s->all_clauses = cdb_alloc(0);
99 s->originals = vec_uint_alloc(0);
100 s->learnts = vec_uint_alloc(0);
101 s->watches = vec_wl_alloc(0);
102 /* Activity heuristic */
103 s->var_act_inc = VAR_ACT_INIT_INC;
104 s->clause_act_inc = CLAUSE_ACT_INIT_INC;
105 /* Variable Information */
106 s->activity = vec_act_alloc(0);
107 s->var_order = heap_alloc(s->activity);
108 s->levels = vec_uint_alloc(0);
109 s->reasons = vec_uint_alloc(0);
110 s->assigns = vec_char_alloc(0);
111 s->polarity = vec_char_alloc(0);
112 /* Assignments */
113 s->trail = vec_uint_alloc(0);
114 s->trail_lim = vec_uint_alloc(0);
115 /* Temporary data used by Search method */
116 s->bq_trail = b_queue_alloc(s->opts.sz_trail_bqueue);
117 s->bq_lbd = b_queue_alloc(s->opts.sz_lbd_bqueue);
118 s->n_confl_bfr_reduce = s->opts.n_conf_fst_reduce;
119 s->RC1 = 1;
120 s->RC2 = s->opts.n_conf_fst_reduce;
121 /* Temporary data used by Analyze */
122 s->temp_lits = vec_uint_alloc(0);
123 s->seen = vec_char_alloc(0);
124 s->tagged = vec_uint_alloc(0);
125 s->stack = vec_uint_alloc(0);
126 s->last_dlevel = vec_uint_alloc(0);
127 /* Misc temporary */
128 s->stamps = vec_uint_alloc(0);
129 return s;
130 }
131
satoko_destroy(solver_t * s)132 void satoko_destroy(solver_t *s)
133 {
134 vec_uint_free(s->assumptions);
135 vec_uint_free(s->final_conflict);
136 cdb_free(s->all_clauses);
137 vec_uint_free(s->originals);
138 vec_uint_free(s->learnts);
139 vec_wl_free(s->watches);
140 vec_act_free(s->activity);
141 heap_free(s->var_order);
142 vec_uint_free(s->levels);
143 vec_uint_free(s->reasons);
144 vec_char_free(s->assigns);
145 vec_char_free(s->polarity);
146 vec_uint_free(s->trail);
147 vec_uint_free(s->trail_lim);
148 b_queue_free(s->bq_lbd);
149 b_queue_free(s->bq_trail);
150 vec_uint_free(s->temp_lits);
151 vec_char_free(s->seen);
152 vec_uint_free(s->tagged);
153 vec_uint_free(s->stack);
154 vec_uint_free(s->last_dlevel);
155 vec_uint_free(s->stamps);
156 if (s->marks)
157 vec_char_free(s->marks);
158 satoko_free(s);
159 }
160
satoko_default_opts(satoko_opts_t * opts)161 void satoko_default_opts(satoko_opts_t *opts)
162 {
163 memset(opts, 0, sizeof(satoko_opts_t));
164 opts->verbose = 0;
165 opts->no_simplify = 0;
166 /* Limits */
167 opts->conf_limit = 0;
168 opts->prop_limit = 0;
169 /* Constants used for restart heuristic */
170 opts->f_rst = 0.8;
171 opts->b_rst = 1.4;
172 opts->fst_block_rst = 10000;
173 opts->sz_lbd_bqueue = 50;
174 opts->sz_trail_bqueue = 5000;
175 /* Constants used for clause database reduction heuristic */
176 opts->n_conf_fst_reduce = 2000;
177 opts->inc_reduce = 300;
178 opts->inc_special_reduce = 1000;
179 opts->lbd_freeze_clause = 30;
180 opts->learnt_ratio = 0.5;
181 /* VSIDS heuristic */
182 opts->var_act_limit = VAR_ACT_LIMIT;
183 opts->var_act_rescale = VAR_ACT_RESCALE;
184 opts->var_decay = 0.95;
185 opts->clause_decay = (clause_act_t) 0.995;
186 /* Binary resolution */
187 opts->clause_max_sz_bin_resol = 30;
188 opts->clause_min_lbd_bin_resol = 6;
189
190 opts->garbage_max_ratio = (float) 0.3;
191 }
192
193 /**
194 * TODO: sanity check on configuration options
195 */
satoko_configure(satoko_t * s,satoko_opts_t * user_opts)196 void satoko_configure(satoko_t *s, satoko_opts_t *user_opts)
197 {
198 assert(user_opts);
199 memcpy(&s->opts, user_opts, sizeof(satoko_opts_t));
200 }
201
satoko_simplify(solver_t * s)202 int satoko_simplify(solver_t * s)
203 {
204 unsigned i, j = 0;
205 unsigned cref;
206
207 assert(solver_dlevel(s) == 0);
208 if (solver_propagate(s) != UNDEF)
209 return SATOKO_ERR;
210 if (s->n_assigns_simplify == vec_uint_size(s->trail) || s->n_props_simplify > 0)
211 return SATOKO_OK;
212
213 vec_uint_foreach(s->originals, cref, i) {
214 struct clause *clause = clause_fetch(s, cref);
215
216 if (clause_is_satisfied(s, clause)) {
217 clause->f_mark = 1;
218 s->stats.n_original_lits -= clause->size;
219 clause_unwatch(s, cref);
220 } else
221 vec_uint_assign(s->originals, j++, cref);
222 }
223 vec_uint_shrink(s->originals, j);
224 solver_rebuild_order(s);
225 s->n_assigns_simplify = vec_uint_size(s->trail);
226 s->n_props_simplify = s->stats.n_original_lits + s->stats.n_learnt_lits;
227 return SATOKO_OK;
228 }
229
satoko_setnvars(solver_t * s,int nvars)230 void satoko_setnvars(solver_t *s, int nvars)
231 {
232 int i;
233 for (i = satoko_varnum(s); i < nvars; i++)
234 satoko_add_variable(s, 0);
235 }
236
satoko_add_variable(solver_t * s,char sign)237 int satoko_add_variable(solver_t *s, char sign)
238 {
239 unsigned var = vec_act_size(s->activity);
240 vec_wl_push(s->watches);
241 vec_wl_push(s->watches);
242 vec_act_push_back(s->activity, 0);
243 vec_uint_push_back(s->levels, 0);
244 vec_char_push_back(s->assigns, SATOKO_VAR_UNASSING);
245 vec_char_push_back(s->polarity, sign);
246 vec_uint_push_back(s->reasons, UNDEF);
247 vec_uint_push_back(s->stamps, 0);
248 vec_char_push_back(s->seen, 0);
249 heap_insert(s->var_order, var);
250 if (s->marks)
251 vec_char_push_back(s->marks, 0);
252 return var;
253 }
254
satoko_add_clause(solver_t * s,int * lits,int size)255 int satoko_add_clause(solver_t *s, int *lits, int size)
256 {
257 unsigned i, j;
258 unsigned prev_lit;
259 unsigned max_var;
260 unsigned cref;
261
262 qsort((void *) lits, (size_t)size, sizeof(unsigned), stk_uint_compare);
263 max_var = lit2var(lits[size - 1]);
264 while (max_var >= vec_act_size(s->activity))
265 satoko_add_variable(s, SATOKO_LIT_FALSE);
266
267 vec_uint_clear(s->temp_lits);
268 j = 0;
269 prev_lit = UNDEF;
270 for (i = 0; i < (unsigned)size; i++) {
271 if ((unsigned)lits[i] == lit_compl(prev_lit) || lit_value(s, lits[i]) == SATOKO_LIT_TRUE)
272 return SATOKO_OK;
273 else if ((unsigned)lits[i] != prev_lit && var_value(s, lit2var(lits[i])) == SATOKO_VAR_UNASSING) {
274 prev_lit = lits[i];
275 vec_uint_push_back(s->temp_lits, lits[i]);
276 }
277 }
278
279 if (vec_uint_size(s->temp_lits) == 0) {
280 s->status = SATOKO_ERR;
281 return SATOKO_ERR;
282 } if (vec_uint_size(s->temp_lits) == 1) {
283 solver_enqueue(s, vec_uint_at(s->temp_lits, 0), UNDEF);
284 return (s->status = (solver_propagate(s) == UNDEF));
285 }
286 if ( 0 ) {
287 for ( i = 0; i < vec_uint_size(s->temp_lits); i++ ) {
288 int lit = vec_uint_at(s->temp_lits, i);
289 printf( "%s%d ", lit&1 ? "!":"", lit>>1 );
290 }
291 printf( "\n" );
292 }
293 cref = solver_clause_create(s, s->temp_lits, 0);
294 clause_watch(s, cref);
295 return SATOKO_OK;
296 }
297
satoko_assump_push(solver_t * s,int lit)298 void satoko_assump_push(solver_t *s, int lit)
299 {
300 assert(lit2var(lit) < (unsigned)satoko_varnum(s));
301 // printf("[Satoko] Push assumption: %d\n", lit);
302 vec_uint_push_back(s->assumptions, lit);
303 vec_char_assign(s->polarity, lit2var(lit), lit_polarity(lit));
304 }
305
satoko_assump_pop(solver_t * s)306 void satoko_assump_pop(solver_t *s)
307 {
308 assert(vec_uint_size(s->assumptions) > 0);
309 // printf("[Satoko] Pop assumption: %d\n", vec_uint_pop_back(s->assumptions));
310 vec_uint_pop_back(s->assumptions);
311 solver_cancel_until(s, vec_uint_size(s->assumptions));
312 }
313
satoko_solve(solver_t * s)314 int satoko_solve(solver_t *s)
315 {
316 int status = SATOKO_UNDEC;
317
318 assert(s);
319 solver_clean_stats(s);
320 //if (s->opts.verbose)
321 // print_opts(s);
322 if (s->status == SATOKO_ERR) {
323 printf("Satoko in inconsistent state\n");
324 return SATOKO_UNDEC;
325 }
326
327 if (!s->opts.no_simplify)
328 if (satoko_simplify(s) != SATOKO_OK)
329 return SATOKO_UNDEC;
330
331 while (status == SATOKO_UNDEC) {
332 status = solver_search(s);
333 if (solver_check_limits(s) == 0 || solver_stop(s))
334 break;
335 if (s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit)
336 break;
337 if (s->pFuncStop && s->pFuncStop(s->RunId))
338 break;
339 }
340 if (s->opts.verbose)
341 print_stats(s);
342
343 solver_cancel_until(s, vec_uint_size(s->assumptions));
344 return status;
345 }
346
satoko_solve_assumptions(solver_t * s,int * plits,int nlits)347 int satoko_solve_assumptions(solver_t *s, int * plits, int nlits)
348 {
349 int i, status;
350 // printf("\n[Satoko] Solve with assumptions.. (%d)\n", vec_uint_size(s->assumptions));
351 // printf("[Satoko] + Variables: %d\n", satoko_varnum(s));
352 // printf("[Satoko] + Clauses: %d\n", satoko_clausenum(s));
353 // printf("[Satoko] + Trail size: %d\n", vec_uint_size(s->trail));
354 // printf("[Satoko] + Queue head: %d\n", s->i_qhead);
355 // solver_debug_check_trail(s);
356 for ( i = 0; i < nlits; i++ )
357 satoko_assump_push( s, plits[i] );
358 status = satoko_solve( s );
359 for ( i = 0; i < nlits; i++ )
360 satoko_assump_pop( s );
361 return status;
362 }
363
satoko_solve_assumptions_limit(satoko_t * s,int * plits,int nlits,int nconflim)364 int satoko_solve_assumptions_limit(satoko_t *s, int * plits, int nlits, int nconflim)
365 {
366 int temp = s->opts.conf_limit, status;
367 s->opts.conf_limit = nconflim ? s->stats.n_conflicts + nconflim : 0;
368 status = satoko_solve_assumptions(s, plits, nlits);
369 s->opts.conf_limit = temp;
370 return status;
371 }
satoko_minimize_assumptions(satoko_t * s,int * plits,int nlits,int nconflim)372 int satoko_minimize_assumptions(satoko_t * s, int * plits, int nlits, int nconflim)
373 {
374 int i, nlitsL, nlitsR, nresL, nresR, status;
375 if ( nlits == 1 )
376 {
377 // since the problem is UNSAT, we try to solve it without assuming the last literal
378 // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
379 status = satoko_solve_assumptions_limit( s, NULL, 0, nconflim );
380 return (int)(status != SATOKO_UNSAT); // return 1 if the problem is not UNSAT
381 }
382 assert( nlits >= 2 );
383 nlitsL = nlits / 2;
384 nlitsR = nlits - nlitsL;
385 // assume the left lits
386 for ( i = 0; i < nlitsL; i++ )
387 satoko_assump_push(s, plits[i]);
388 // solve with these assumptions
389 status = satoko_solve_assumptions_limit( s, NULL, 0, nconflim );
390 if ( status == SATOKO_UNSAT ) // these are enough
391 {
392 for ( i = 0; i < nlitsL; i++ )
393 satoko_assump_pop(s);
394 return satoko_minimize_assumptions( s, plits, nlitsL, nconflim );
395 }
396 // these are not enoguh
397 // solve for the right lits
398 nresL = nlitsR == 1 ? 1 : satoko_minimize_assumptions( s, plits + nlitsL, nlitsR, nconflim );
399 for ( i = 0; i < nlitsL; i++ )
400 satoko_assump_pop(s);
401 // swap literals
402 vec_uint_clear(s->temp_lits);
403 for ( i = 0; i < nlitsL; i++ )
404 vec_uint_push_back(s->temp_lits, plits[i]);
405 for ( i = 0; i < nresL; i++ )
406 plits[i] = plits[nlitsL+i];
407 for ( i = 0; i < nlitsL; i++ )
408 plits[nresL+i] = vec_uint_at(s->temp_lits, i);
409 // assume the right lits
410 for ( i = 0; i < nresL; i++ )
411 satoko_assump_push(s, plits[i]);
412 // solve with these assumptions
413 status = satoko_solve_assumptions_limit( s, NULL, 0, nconflim );
414 if ( status == SATOKO_UNSAT ) // these are enough
415 {
416 for ( i = 0; i < nresL; i++ )
417 satoko_assump_pop(s);
418 return nresL;
419 }
420 // solve for the left lits
421 nresR = nlitsL == 1 ? 1 : satoko_minimize_assumptions( s, plits + nresL, nlitsL, nconflim );
422 for ( i = 0; i < nresL; i++ )
423 satoko_assump_pop(s);
424 return nresL + nresR;
425 }
426
satoko_final_conflict(solver_t * s,int ** out)427 int satoko_final_conflict(solver_t *s, int **out)
428 {
429 *out = (int *)vec_uint_data(s->final_conflict);
430 return vec_uint_size(s->final_conflict);
431 }
432
satoko_stats(satoko_t * s)433 satoko_stats_t * satoko_stats(satoko_t *s)
434 {
435 return &s->stats;
436 }
437
satoko_options(satoko_t * s)438 satoko_opts_t * satoko_options(satoko_t *s)
439 {
440 return &s->opts;
441 }
442
satoko_bookmark(satoko_t * s)443 void satoko_bookmark(satoko_t *s)
444 {
445 // printf("[Satoko] Bookmark.\n");
446 assert(s->status == SATOKO_OK);
447 assert(solver_dlevel(s) == 0);
448 s->book_cl_orig = vec_uint_size(s->originals);
449 s->book_cl_lrnt = vec_uint_size(s->learnts);
450 s->book_vars = vec_char_size(s->assigns);
451 s->book_trail = vec_uint_size(s->trail);
452 // s->book_qhead = s->i_qhead;
453 s->opts.no_simplify = 1;
454 }
455
satoko_unbookmark(satoko_t * s)456 void satoko_unbookmark(satoko_t *s)
457 {
458 // printf("[Satoko] Unbookmark.\n");
459 assert(s->status == SATOKO_OK);
460 s->book_cl_orig = 0;
461 s->book_cl_lrnt = 0;
462 s->book_cdb = 0;
463 s->book_vars = 0;
464 s->book_trail = 0;
465 // s->book_qhead = 0;
466 s->opts.no_simplify = 0;
467 }
468
satoko_reset(satoko_t * s)469 void satoko_reset(satoko_t *s)
470 {
471 // printf("[Satoko] Reset.\n");
472 vec_uint_clear(s->assumptions);
473 vec_uint_clear(s->final_conflict);
474 cdb_clear(s->all_clauses);
475 vec_uint_clear(s->originals);
476 vec_uint_clear(s->learnts);
477 vec_wl_clean(s->watches);
478 vec_act_clear(s->activity);
479 heap_clear(s->var_order);
480 vec_uint_clear(s->levels);
481 vec_uint_clear(s->reasons);
482 vec_char_clear(s->assigns);
483 vec_char_clear(s->polarity);
484 vec_uint_clear(s->trail);
485 vec_uint_clear(s->trail_lim);
486 b_queue_clean(s->bq_lbd);
487 b_queue_clean(s->bq_trail);
488 vec_uint_clear(s->temp_lits);
489 vec_char_clear(s->seen);
490 vec_uint_clear(s->tagged);
491 vec_uint_clear(s->stack);
492 vec_uint_clear(s->last_dlevel);
493 vec_uint_clear(s->stamps);
494 s->status = SATOKO_OK;
495 s->var_act_inc = VAR_ACT_INIT_INC;
496 s->clause_act_inc = CLAUSE_ACT_INIT_INC;
497 s->n_confl_bfr_reduce = s->opts.n_conf_fst_reduce;
498 s->RC1 = 1;
499 s->RC2 = s->opts.n_conf_fst_reduce;
500 s->book_cl_orig = 0;
501 s->book_cl_lrnt = 0;
502 s->book_cdb = 0;
503 s->book_vars = 0;
504 s->book_trail = 0;
505 s->i_qhead = 0;
506 }
507
satoko_rollback(satoko_t * s)508 void satoko_rollback(satoko_t *s)
509 {
510 unsigned i, cref;
511 unsigned n_originals = vec_uint_size(s->originals) - s->book_cl_orig;
512 unsigned n_learnts = vec_uint_size(s->learnts) - s->book_cl_lrnt;
513 struct clause **cl_to_remove;
514
515 // printf("[Satoko] rollback.\n");
516 assert(s->status == SATOKO_OK);
517 assert(solver_dlevel(s) == 0);
518 if (!s->book_vars) {
519 satoko_reset(s);
520 return;
521 }
522 cl_to_remove = satoko_alloc(struct clause *, n_originals + n_learnts);
523 /* Mark clauses */
524 vec_uint_foreach_start(s->originals, cref, i, s->book_cl_orig)
525 cl_to_remove[i] = clause_fetch(s, cref);
526 vec_uint_foreach_start(s->learnts, cref, i, s->book_cl_lrnt)
527 cl_to_remove[n_originals + i] = clause_fetch(s, cref);
528 for (i = 0; i < n_originals + n_learnts; i++) {
529 clause_unwatch(s, cdb_cref(s->all_clauses, (unsigned *)cl_to_remove[i]));
530 cl_to_remove[i]->f_mark = 1;
531 }
532 satoko_free(cl_to_remove);
533 vec_uint_shrink(s->originals, s->book_cl_orig);
534 vec_uint_shrink(s->learnts, s->book_cl_lrnt);
535 /* Shrink variable related vectors */
536 for (i = s->book_vars; i < 2 * vec_char_size(s->assigns); i++) {
537 vec_wl_at(s->watches, i)->size = 0;
538 vec_wl_at(s->watches, i)->n_bin = 0;
539 }
540 // s->i_qhead = s->book_qhead;
541 s->watches->size = s->book_vars;
542 vec_act_shrink(s->activity, s->book_vars);
543 vec_uint_shrink(s->levels, s->book_vars);
544 vec_uint_shrink(s->reasons, s->book_vars);
545 vec_uint_shrink(s->stamps, s->book_vars);
546 vec_char_shrink(s->assigns, s->book_vars);
547 vec_char_shrink(s->seen, s->book_vars);
548 vec_char_shrink(s->polarity, s->book_vars);
549 solver_rebuild_order(s);
550 /* Rewind solver and cancel level 0 assignments to the trail */
551 solver_cancel_until(s, 0);
552 vec_uint_shrink(s->trail, s->book_trail);
553 if (s->book_cdb)
554 s->all_clauses->size = s->book_cdb;
555 s->book_cl_orig = 0;
556 s->book_cl_lrnt = 0;
557 s->book_vars = 0;
558 s->book_trail = 0;
559 // s->book_qhead = 0;
560 }
561
satoko_mark_cone(satoko_t * s,int * pvars,int n_vars)562 void satoko_mark_cone(satoko_t *s, int * pvars, int n_vars)
563 {
564 int i;
565 if (!solver_has_marks(s))
566 s->marks = vec_char_init(satoko_varnum(s), 0);
567 for (i = 0; i < n_vars; i++) {
568 var_set_mark(s, pvars[i]);
569 vec_sdbl_assign(s->activity, pvars[i], 0);
570 if (!heap_in_heap(s->var_order, pvars[i]))
571 heap_insert(s->var_order, pvars[i]);
572 }
573 }
574
satoko_unmark_cone(satoko_t * s,int * pvars,int n_vars)575 void satoko_unmark_cone(satoko_t *s, int *pvars, int n_vars)
576 {
577 int i;
578 assert(solver_has_marks(s));
579 for (i = 0; i < n_vars; i++)
580 var_clean_mark(s, pvars[i]);
581 }
582
satoko_write_dimacs(satoko_t * s,char * fname,int wrt_lrnt,int zero_var)583 void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
584 {
585 FILE *file;
586 unsigned i;
587 unsigned n_vars = vec_act_size(s->activity);
588 unsigned n_orig = vec_uint_size(s->originals) + vec_uint_size(s->trail);
589 unsigned n_lrnts = vec_uint_size(s->learnts);
590 unsigned *array;
591
592 assert(wrt_lrnt == 0 || wrt_lrnt == 1);
593 assert(zero_var == 0 || zero_var == 1);
594 if (fname != NULL)
595 file = fopen(fname, "w");
596 else
597 file = stdout;
598
599 if (file == NULL) {
600 printf( "Error: Cannot open output file.\n");
601 return;
602 }
603 fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig);
604 for (i = 0; i < vec_char_size(s->assigns); i++) {
605 if ( var_value(s, i) != SATOKO_VAR_UNASSING ) {
606 if (zero_var)
607 fprintf(file, "%d\n", var_value(s, i) == SATOKO_LIT_FALSE ? -(int)(i) : i);
608 else
609 fprintf(file, "%d 0\n", var_value(s, i) == SATOKO_LIT_FALSE ? -(int)(i + 1) : i + 1);
610 }
611 }
612 array = vec_uint_data(s->originals);
613 for (i = 0; i < vec_uint_size(s->originals); i++)
614 clause_dump(file, clause_fetch(s, array[i]), !zero_var);
615
616 if (wrt_lrnt) {
617 array = vec_uint_data(s->learnts);
618 for (i = 0; i < n_lrnts; i++)
619 clause_dump(file, clause_fetch(s, array[i]), !zero_var);
620 }
621 fclose(file);
622
623 }
624
satoko_varnum(satoko_t * s)625 int satoko_varnum(satoko_t *s)
626 {
627 return vec_char_size(s->assigns);
628 }
629
satoko_clausenum(satoko_t * s)630 int satoko_clausenum(satoko_t *s)
631 {
632 return vec_uint_size(s->originals);
633 }
634
satoko_learntnum(satoko_t * s)635 int satoko_learntnum(satoko_t *s)
636 {
637 return vec_uint_size(s->learnts);
638 }
639
satoko_conflictnum(satoko_t * s)640 int satoko_conflictnum(satoko_t *s)
641 {
642 return satoko_stats(s)->n_conflicts_all;
643 }
644
satoko_set_stop(satoko_t * s,int * pstop)645 void satoko_set_stop(satoko_t *s, int * pstop)
646 {
647 s->pstop = pstop;
648 }
649
satoko_set_stop_func(satoko_t * s,int (* fnct)(int))650 void satoko_set_stop_func(satoko_t *s, int (*fnct)(int))
651 {
652 s->pFuncStop = fnct;
653 }
654
satoko_set_runid(satoko_t * s,int id)655 void satoko_set_runid(satoko_t *s, int id)
656 {
657 s->RunId = id;
658 }
659
satoko_read_cex_varvalue(satoko_t * s,int ivar)660 int satoko_read_cex_varvalue(satoko_t *s, int ivar)
661 {
662 return satoko_var_polarity(s, ivar) == SATOKO_LIT_TRUE;
663 }
664
satoko_set_runtime_limit(satoko_t * s,abctime Limit)665 abctime satoko_set_runtime_limit(satoko_t* s, abctime Limit)
666 {
667 abctime nRuntimeLimit = s->nRuntimeLimit;
668 s->nRuntimeLimit = Limit;
669 return nRuntimeLimit;
670 }
671
satoko_var_polarity(satoko_t * s,unsigned var)672 char satoko_var_polarity(satoko_t *s, unsigned var)
673 {
674 return vec_char_at(s->polarity, var);
675 }
676
677 ABC_NAMESPACE_IMPL_END
678