@@ -71,11 +71,14 @@ void _c3_print_cnf (C3List *cnf) {
71
71
int32_t * num ;
72
72
c3_list_foreach (cnf , iter , disj ) {
73
73
printf ("(" );
74
+ //printf ("[%p] ", iter);
74
75
c3_list_foreach (disj , iter2 , num ) {
75
76
if (* num < 0 ) {
76
77
printf ("!x%d" , - (* num ));
78
+ //printf ("!x%d(%p)", -(*num), num);
77
79
} else {
78
80
printf ("x%d" , * num );
81
+ //printf ("x%d(%p)", *num, num);
79
82
}
80
83
if (iter2 != disj -> tail ) { //XXX
81
84
printf (" or " );
@@ -305,9 +308,9 @@ static bool _c3_dpll_simplify2(C3 *c3, C3List *cnf, int32_t *res) {
305
308
continue ;
306
309
}
307
310
absi = abs (i );
308
- printf ("pure literal %d\n" , i );
309
311
res [absi - 1 ] = (i < 0 ) ? -1 : 1 ;
310
312
iter = cnf -> head ;
313
+ //printf ("pure literal %d\t%p\n", i, iter);
311
314
while (iter ) {
312
315
disj = iter -> data ;
313
316
next = iter -> n ;
@@ -318,6 +321,7 @@ static bool _c3_dpll_simplify2(C3 *c3, C3List *cnf, int32_t *res) {
318
321
iter = next ;
319
322
}
320
323
updated = true;
324
+ _c3_print_cnf (cnf );
321
325
}
322
326
c3_hmap_clear (c3 -> literals );
323
327
return updated ;
@@ -512,7 +516,7 @@ int main(int argc, char **argv, char **envp) {
512
516
}
513
517
c3_print_cnf (& c3 );
514
518
c3_sort_cnf (& c3 );
515
- res = (int8_t * ) calloc (c3 .valnum , sizeof (int8_t ));
519
+ res = (int8_t * ) calloc (c3 .valnum , sizeof (int32_t ));
516
520
status = c3_derive_sat (& c3 , res );
517
521
//c3_print_cnf (&c3);
518
522
printf ("s %s\n" , status_str [status ]);
0 commit comments