Context Navigation

← Previous Revision
Latest Revision
Next Revision →
Blame
Revision Log

satUtil.c @ 74

Last change on this file since 74 was 14, checked in by cecile, 13 years ago
vis2.3
File size: 70.0 KB

Line
1	/CFile*********************************************************************
2
3	FileName [satUtil.c]
4
5	PackageName [sat]
6
7	Synopsis [Routines for various utility function.]
8
9	Author [HoonSang Jin]
10
11	Copyright [ This file was created at the University of Colorado at
12	Boulder. The University of Colorado at Boulder makes no warranty
13	about the suitability of this software for any purpose. It is
14	presented on an AS IS basis.]
15
16
17	******************************************************************************/
18
19	#include "satInt.h"
20
21	static char rcsid[] UNUSED = "$Id: satUtil.c,v 1.37 2009/04/11 18:26:37 fabio Exp $";
22
23	/---------------------------------------------------------------------------/
24	/* Constant declarations */
25	/---------------------------------------------------------------------------/
26
27	/AutomaticStart***********************************************************/
28
29	/---------------------------------------------------------------------------/
30	/* Static function prototypes */
31	/---------------------------------------------------------------------------/
32
33	static int NodeIndexCompare(const void x, const void y);
34
35	/AutomaticEnd*************************************************************/
36
37
38	/---------------------------------------------------------------------------/
39	/* Definition of exported functions */
40	/---------------------------------------------------------------------------/
41
42
43	/Function******************************************************************
44
45	Synopsis [ Add conflict clause into clause database]
46
47	Description [ Add conflict clause into clause database]
48
49	SideEffects []
50
51	SeeAlso []
52
53	******************************************************************************/
54	long
55	sat_AddConflictClause(
56	satManager_t *cm,
57	satArray_t *clauseArray,
58	int objectFlag)
59	{
60	satStatistics_t *stats;
61	satLiteralDB_t *literals;
62	satVariable_t *var;
63	long v, c;
64	int inverted;
65	long *last;
66	long *space;
67	int i, size;
68	int maxLevel, maxIndex;
69	int value, level;
70	int otherWLIndex;
71
72	literals = cm->literals;
73
74	while(literals->last + clauseArray->num + 2 >= literals->end) {
75	if(!sat_EnlargeLiteralDB(cm)) {
76	fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
77	cm->comment);
78	exit(0);
79	}
80	}
81
82	c = 0;
83	if(cm->unusedAigQueue)
84	c = sat_Dequeue(cm->unusedAigQueue);
85	if(c == 0)
86	c = sat_CreateNode(cm, 2, 2);
87
88
89	last = literals->last;
90	*(last) = (-c);
91	last++;
92
93	/**
94	SATfirstLit(c) = (int)last;
95	**/
96	(cm->nodesArray[c+satFirstLit]) = (long)last;
97	SATnumLits(c) = clauseArray->num;
98	SATflags(c) \|= IsCNFMask;
99	SATsetInUse(c);
100	SATnumConflict(c) = 0;
101
102	size = clauseArray->num;
103	space = clauseArray->space;
104	for(i=0; i<size; i++, space++) {
105	v = *space;
106	inverted = !SATisInverted(v);
107	v = SATnormalNode(v);
108
109	*(last) = ((v^inverted) << 2);
110	last++;
111
112	var = SATgetVariable(v);
113
114	if(inverted){
115	(var->litsCount[0])++;
116	(var->conflictLits[0])++;
117	}
118	else {
119	(var->litsCount[1])++;
120	(var->conflictLits[1])++;
121	}
122	}
123	*(last) = (-c);
124	last++;
125
126	literals->last = last;
127
128	maxLevel = -1;
129	maxIndex = -1;
130	otherWLIndex = -1;
131	space = clauseArray->space;
132	for(i=0; i<size; i++, space++) {
133	v = *space;
134	inverted = SATisInverted(v);
135	v = SATnormalNode(v);
136	value = SATvalue(v);
137	if(value == 2) {
138	sat_AddWL(cm, c, i, 1);
139	otherWLIndex = i;
140	break;
141	}
142	else {
143	level = SATlevel(v);
144	if(level > maxLevel) {
145	maxLevel = level;
146	maxIndex = i;
147	}
148	}
149	}
150	if(i >= size) {
151	sat_AddWL(cm, c, maxIndex, 1);
152	otherWLIndex = maxIndex;
153	}
154
155	maxLevel = -1;
156	maxIndex = -1;
157	space = clauseArray->space+size-1;
158	for(i=size-1; i>=0; i--, space--) {
159	v = *space;
160	inverted = SATisInverted(v);
161	v = SATnormalNode(v);
162	value = SATvalue(v);
163	if(i != otherWLIndex) {
164	if(value == 2) {
165	sat_AddWL(cm, c, i, -1);
166	break;
167	}
168	else {
169	level = SATlevel(v);
170	if(level > maxLevel) {
171	maxLevel = level;
172	maxIndex = i;
173	}
174	}
175	}
176	}
177	if(i < 0)
178	sat_AddWL(cm, c, maxIndex, -1);
179
180
181	SATflags(c) \|= IsConflictMask;
182
183	stats = cm->each;
184	stats->nConflictCl++;
185	stats->nConflictLit += clauseArray->num;
186	if(objectFlag) {
187	stats->nObjConflictCl++;
188	stats->nObjConflictLit += clauseArray->num;
189	SATflags(c) \|= ObjMask;
190	}
191	else {
192	stats->nNonobjConflictCl++;
193	stats->nNonobjConflictLit += clauseArray->num;
194	SATflags(c) \|= NonobjMask;
195	}
196
197
198	return(c);
199	}
200
201	/Function******************************************************************
202
203	Synopsis [ Add conflict clause into clause database without updating score]
204
205	Description [ Add conflict clause into clause database without updating score]
206
207	SideEffects []
208
209	SeeAlso []
210
211	******************************************************************************/
212	long
213	sat_AddConflictClauseNoScoreUpdate(
214	satManager_t *cm,
215	satArray_t *clauseArray,
216	int objectFlag)
217	{
218	satStatistics_t *stats;
219	satLiteralDB_t *literals;
220	satVariable_t *var;
221	long v, c;
222	int inverted;
223	long *last;
224	long *space;
225	int i, size;
226	int maxLevel, maxIndex;
227	int value, level;
228	int otherWLIndex;
229
230	literals = cm->literals;
231
232	while(literals->last + clauseArray->num + 2 >= literals->end) {
233	if(!sat_EnlargeLiteralDB(cm)) {
234	fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
235	cm->comment);
236	exit(0);
237	}
238	}
239
240	c = 0;
241	if(cm->unusedAigQueue)
242	c = sat_Dequeue(cm->unusedAigQueue);
243	if(c == 0)
244	c = sat_CreateNode(cm, 2, 2);
245
246
247	last = literals->last;
248	*(last) = (-c);
249	last++;
250
251	/**
252	SATfirstLit(c) = (int)last;
253	**/
254	(cm->nodesArray[c+satFirstLit]) = (long)last;
255	SATnumLits(c) = clauseArray->num;
256	SATflags(c) \|= IsCNFMask;
257	SATsetInUse(c);
258	SATnumConflict(c) = 0;
259
260	size = clauseArray->num;
261	space = clauseArray->space;
262	for(i=0; i<size; i++, space++) {
263	v = *space;
264	inverted = !SATisInverted(v);
265	v = SATnormalNode(v);
266
267	*(last) = ((v^inverted) << 2);
268	last++;
269
270	var = SATgetVariable(v);
271
272	if(inverted){
273	(var->litsCount[0])++;
274	(var->conflictLits[0])++;
275	}
276	else {
277	(var->litsCount[1])++;
278	(var->conflictLits[1])++;
279	}
280	}
281	*(last) = (-c);
282	last++;
283
284	literals->last = last;
285
286	maxLevel = -1;
287	maxIndex = -1;
288	otherWLIndex = -1;
289	space = clauseArray->space;
290	for(i=0; i<size; i++, space++) {
291	v = *space;
292	inverted = SATisInverted(v);
293	v = SATnormalNode(v);
294	value = SATvalue(v);
295	if(value == 2) {
296	sat_AddWL(cm, c, i, 1);
297	otherWLIndex = i;
298	break;
299	}
300	else {
301	level = SATlevel(v);
302	if(level > maxLevel) {
303	maxLevel = level;
304	maxIndex = i;
305	}
306	}
307	}
308	if(i >= size) {
309	sat_AddWL(cm, c, maxIndex, 1);
310	otherWLIndex = maxIndex;
311	}
312
313	maxLevel = -1;
314	maxIndex = -1;
315	space = clauseArray->space+size-1;
316	for(i=size-1; i>=0; i--, space--) {
317	v = *space;
318	inverted = SATisInverted(v);
319	v = SATnormalNode(v);
320	value = SATvalue(v);
321	if(i != otherWLIndex) {
322	if(value == 2) {
323	sat_AddWL(cm, c, i, -1);
324	break;
325	}
326	else {
327	level = SATlevel(v);
328	if(level > maxLevel) {
329	maxLevel = level;
330	maxIndex = i;
331	}
332	}
333	}
334	}
335	if(i < 0)
336	sat_AddWL(cm, c, maxIndex, -1);
337
338
339	SATflags(c) \|= IsConflictMask;
340
341	stats = cm->each;
342	stats->nConflictCl++;
343	stats->nConflictLit += clauseArray->num;
344	if(objectFlag) {
345	stats->nObjConflictCl++;
346	stats->nObjConflictLit += clauseArray->num;
347	SATflags(c) \|= ObjMask;
348	}
349	else {
350	stats->nNonobjConflictCl++;
351	stats->nNonobjConflictLit += clauseArray->num;
352	SATflags(c) \|= NonobjMask;
353	}
354
355
356	return(c);
357	}
358	/Function******************************************************************
359
360	Synopsis [ Add unit conflict clause into clause database]
361
362	Description [ Add unit conflict clause into clause database]
363
364	SideEffects []
365
366	SeeAlso []
367
368	******************************************************************************/
369	long
370	sat_AddUnitConflictClause(
371	satManager_t *cm,
372	satArray_t *clauseArray,
373	int objectFlag)
374	{
375	satLiteralDB_t *literals;
376	satStatistics_t *stats;
377	long c, v;
378	int inverted;
379	long last, space;
380	int i, size;
381
382	literals = cm->literals;
383
384	while(literals->last + clauseArray->num + 2 >= literals->end) {
385	if(!sat_EnlargeLiteralDB(cm)) {
386	fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
387	cm->comment);
388	exit(0);
389	}
390	}
391
392	c = 0;
393	if(cm->unusedAigQueue)
394	c = sat_Dequeue(cm->unusedAigQueue);
395	if(c == 0)
396	c = sat_CreateNode(cm, 2, 2);
397
398
399	last = literals->last;
400	*(last) = (-c);
401	last++;
402
403	/**
404	SATfirstLit(c) = (int)last;
405	**/
406	(cm->nodesArray[c+satFirstLit]) = (long)last;
407	SATnumLits(c) = clauseArray->num;
408	SATflags(c) \|= IsCNFMask;
409	SATsetInUse(c);
410	SATnumConflict(c) = 0;
411
412	size = clauseArray->num;
413	space = clauseArray->space;
414	for(i=0; i<size; i++, space++) {
415	v = *space;
416	inverted = !SATisInverted(v);
417	v = SATnormalNode(v);
418
419	*(last) = ((v^inverted) << 2);
420	last++;
421	}
422	*(last) = (-c);
423	last++;
424
425	literals->last = last;
426
427	SATflags(c) \|= IsConflictMask;
428	stats = cm->each;
429	stats->nConflictCl++;
430	stats->nConflictLit += clauseArray->num;
431	if(objectFlag) {
432	stats->nObjConflictCl++;
433	stats->nObjConflictLit += clauseArray->num;
434	SATflags(c) \|= ObjMask;
435	}
436	else {
437	stats->nNonobjConflictCl++;
438	stats->nNonobjConflictLit += clauseArray->num;
439	SATflags(c) \|= NonobjMask;
440	}
441
442	return(c);
443	}
444	/Function******************************************************************
445
446	Synopsis [ Add unit blocking clause into clause database]
447
448	Description [ Add unit blocking clause into clause database]
449
450	SideEffects []
451
452	SeeAlso []
453
454	******************************************************************************/
455	long
456	sat_AddUnitBlockingClause(
457	satManager_t *cm,
458	satArray_t *clauseArray)
459	{
460	satLiteralDB_t *literals;
461	satStatistics_t *stats;
462	long c, v;
463	int inverted;
464	long last, space;
465	int i, size;
466
467	literals = cm->literals;
468	stats = cm->each;
469
470	while(literals->last + clauseArray->num + 2 >= literals->end) {
471	if(!sat_EnlargeLiteralDB(cm)) {
472	fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
473	cm->comment);
474	exit(0);
475	}
476	}
477
478	c = 0;
479	if(cm->unusedAigQueue)
480	c = sat_Dequeue(cm->unusedAigQueue);
481	if(c == 0)
482	c = sat_CreateNode(cm, 2, 2);
483
484
485	last = literals->last;
486	*(last) = (-c);
487	last++;
488
489	/**
490	SATfirstLit(c) = (int)last;
491	**/
492	(cm->nodesArray[c+satFirstLit]) = (long)last;
493	SATnumLits(c) = clauseArray->num;
494	SATflags(c) \|= IsCNFMask;
495	SATsetInUse(c);
496	SATnumConflict(c) = 0;
497
498	size = clauseArray->num;
499	space = clauseArray->space;
500	for(i=0; i<size; i++, space++) {
501	v = *space;
502	inverted = !SATisInverted(v);
503	v = SATnormalNode(v);
504
505	*(last) = ((v^inverted) << 2);
506	last++;
507	}
508	*(last) = (-c);
509	last++;
510
511	literals->last = last;
512
513	SATflags(c) \|= IsBlockingMask;
514
515	stats = cm->each;
516	stats->nBlockingCl++;
517	stats->nBlockingLit += clauseArray->num;
518	return(c);
519	}
520
521
522	/Function******************************************************************
523
524	Synopsis [ Add unit conflict clause into clause database]
525
526	Description [ Add unit conflict clause into clause database]
527
528	SideEffects [ UNSAT Core generation]
529
530	SeeAlso []
531
532	******************************************************************************/
533	long
534	sat_AddUnitClause(
535	satManager_t *cm,
536	satArray_t *clauseArray)
537	{
538	satLiteralDB_t *literals;
539	long c = 0, v;
540	int inverted;
541	long last, space;
542	int i, size;
543
544	literals = cm->literals;
545
546	while(literals->last + clauseArray->num + 2 >= literals->end) {
547	if(!sat_EnlargeLiteralDB(cm)) {
548	fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
549	cm->comment);
550	exit(0);
551	}
552	}
553
554
555	c = 0;
556	if(cm->unusedAigQueue)
557	c = sat_Dequeue(cm->unusedAigQueue);
558	if(c == 0)
559	c = sat_CreateNode(cm, 2, 2);
560
561
562	last = literals->last;
563	*(last) = (-c);
564	last++;
565
566	/**
567	SATfirstLit(c) = (int)last;
568	**/
569	(cm->nodesArray[c+satFirstLit]) = (long)last;
570	SATnumLits(c) = clauseArray->num;
571	SATflags(c) \|= IsCNFMask;
572	SATsetInUse(c);
573	SATnumConflict(c) = 0;
574
575	size = clauseArray->num;
576	space = clauseArray->space;
577	for(i=0; i<size; i++, space++) {
578	v = *space;
579	inverted = !SATisInverted(v);
580	v = SATnormalNode(v);
581
582	*(last) = ((v^inverted) << 2);
583	last++;
584	}
585	*(last) = (-c);
586	last++;
587
588	literals->last = last;
589
590	return(c);
591	}
592
593	/Function******************************************************************
594
595	Synopsis [ Add conflict clause into clause database]
596
597	Description [ Add conflict clause into clause database]
598
599	SideEffects []
600
601	SeeAlso []
602
603	******************************************************************************/
604	long
605	sat_AddClauseIncremental(
606	satManager_t *cm,
607	satArray_t *clauseArray,
608	int objectFlag,
609	int fromDistill)
610	{
611	satLiteralDB_t *literals;
612	satStatistics_t *stats;
613	satVariable_t *var;
614	long c, v;
615	int inverted;
616	long last, space;
617	int i, size;
618	int maxLevel, maxIndex;
619	int value, level;
620	int otherWLIndex;
621
622	literals = cm->literals;
623	stats = cm->each;
624
625	while(literals->last + clauseArray->num + 2 >= literals->end) {
626	if(!sat_EnlargeLiteralDB(cm)) {
627	fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
628	cm->comment);
629	exit(0);
630	}
631	}
632
633	c = 0;
634	if(cm->unusedAigQueue)
635	c = sat_Dequeue(cm->unusedAigQueue);
636	if(c == 0)
637	c = sat_CreateNode(cm, 2, 2);
638
639	last = literals->last;
640	*(last) = (-c);
641	last++;
642
643
644	/**
645	SATfirstLit(c) = (int)last;
646	**/
647	(cm->nodesArray[c+satFirstLit]) = (long)last;
648	SATnumLits(c) = clauseArray->num;
649	SATflags(c) \|= IsCNFMask;
650	SATsetInUse(c);
651	SATnumConflict(c) = 0;
652
653	size = clauseArray->num;
654	space = clauseArray->space;
655	for(i=0; i<size; i++, space++) {
656	v = *space;
657	inverted = !SATisInverted(v);
658	v = SATnormalNode(v);
659
660	*(last) = ((v^inverted) << 2);
661	last++;
662
663	var = SATgetVariable(v);
664	if(inverted){
665	if(fromDistill)
666	(var->litsCount[0])++;
667	(var->conflictLits[0])++;
668	}
669	else {
670	if(fromDistill)
671	(var->litsCount[1])++;
672	(var->conflictLits[1])++;
673	}
674	}
675	*(last) = (-c);
676	last++;
677
678	literals->last = last;
679
680
681	/* Bing: UNSAT core generation */
682	if(clauseArray->num>1){
683	maxLevel = -1;
684	maxIndex = -1;
685	otherWLIndex = -1;
686	space = clauseArray->space;
687	for(i=0; i<size; i++, space++) {
688	v = *space;
689	inverted = SATisInverted(v);
690	v = SATnormalNode(v);
691	value = SATvalue(v);
692	if(value == 2) {
693	sat_AddWL(cm, c, i, 1);
694	otherWLIndex = i;
695	break;
696	}
697	else {
698	level = SATlevel(v);
699	if(level > maxLevel) {
700	maxLevel = level;
701	maxIndex = i;
702	}
703	}
704	}
705	if(i >= size) {
706	sat_AddWL(cm, c, maxIndex, 1);
707	otherWLIndex = maxIndex;
708	}
709
710	maxLevel = -1;
711	maxIndex = -1;
712	space = clauseArray->space+size-1;
713	for(i=size-1; i>=0; i--, space--) {
714	v = *space;
715	inverted = SATisInverted(v);
716	v = SATnormalNode(v);
717	value = SATvalue(v);
718	if(i != otherWLIndex) {
719	if(value == 2) {
720	sat_AddWL(cm, c, i, -1);
721	break;
722	}
723	else {
724	level = SATlevel(v);
725	if(level > maxLevel) {
726	maxLevel = level;
727	maxIndex = i;
728	}
729	}
730	}
731	}
732	if(i < 0)
733	sat_AddWL(cm, c, maxIndex, -1);
734	}
735
736	if(objectFlag)SATflags(c) \|= ObjMask;
737	else SATflags(c) \|= NonobjMask;
738	/SATflags(c) \|= IsConflictMask;/
739	//Bing:change??
740	if(!cm->option->coreGeneration)
741	SATflags(c) \|= IsConflictMask;
742
743	if(objectFlag) {
744	stats->nInitObjConflictCl++;
745	stats->nInitObjConflictLit += clauseArray->num;
746	stats->nObjConflictCl++;
747	stats->nObjConflictLit += clauseArray->num;
748	}
749	else {
750	stats->nInitNonobjConflictCl++;
751	stats->nInitNonobjConflictLit += clauseArray->num;
752	stats->nObjConflictCl++;
753	stats->nObjConflictLit += clauseArray->num;
754	}
755	stats->nConflictCl++;
756	stats->nConflictLit += clauseArray->num;
757
758	return(c);
759	}
760
761	/Function******************************************************************
762
763	Synopsis [ Add clause into clause database]
764
765	Description [ Add clause into clause database]
766
767	SideEffects []
768
769	SeeAlso []
770
771	******************************************************************************/
772	long
773	sat_AddClause(
774	satManager_t *cm,
775	satArray_t *clauseArray)
776	{
777	satLiteralDB_t *literals;
778	long c, v;
779	int inverted;
780	long last, space;
781	int i, size;
782	int maxLevel, maxIndex;
783	int value, level;
784	int otherWLIndex;
785
786	literals = cm->literals;
787
788	while(literals->last + clauseArray->num + 2 >= literals->end) {
789	if(!sat_EnlargeLiteralDB(cm)) {
790	fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
791	cm->comment);
792	exit(0);
793	}
794	}
795	c = 0;
796	if(cm->unusedAigQueue)
797	c = sat_Dequeue(cm->unusedAigQueue);
798	if(c == 0)
799	c = sat_CreateNode(cm, 2, 2);
800
801	last = literals->last;
802	*(last) = (-c);
803	last++;
804
805	/**
806	SATfirstLit(c) = (int)last;
807	**/
808	(cm->nodesArray[c+satFirstLit]) = (long)last;
809	SATnumLits(c) = clauseArray->num;
810	SATflags(c) \|= IsCNFMask;
811	SATsetInUse(c);
812	SATnumConflict(c) = 0;
813
814	size = clauseArray->num;
815	space = clauseArray->space;
816	for(i=0; i<size; i++, space++) {
817	v = *space;
818	inverted = !SATisInverted(v);
819	v = SATnormalNode(v);
820
821	*(last) = ((v^inverted) << 2);
822	last++;
823	}
824	*(last) = (-c);
825	last++;
826
827	literals->last = last;
828
829	maxLevel = -1;
830	maxIndex = -1;
831	otherWLIndex = -1;
832	space = clauseArray->space;
833	for(i=0; i<size; i++, space++) {
834	v = *space;
835	inverted = SATisInverted(v);
836	v = SATnormalNode(v);
837	value = SATvalue(v);
838	if(value == 2) {
839	sat_AddWL(cm, c, i, 1);
840	otherWLIndex = i;
841	break;
842	}
843	else {
844	level = SATlevel(v);
845	if(level > maxLevel) {
846	maxLevel = level;
847	maxIndex = i;
848	}
849	}
850	}
851	if(i >= size) {
852	sat_AddWL(cm, c, maxIndex, 1);
853	otherWLIndex = maxIndex;
854	}
855
856	maxLevel = -1;
857	maxIndex = -1;
858	space = clauseArray->space+size-1;
859	for(i=size-1; i>=0; i--, space--) {
860	v = *space;
861	inverted = SATisInverted(v);
862	v = SATnormalNode(v);
863	value = SATvalue(v);
864	if(i != otherWLIndex) {
865	if(value == 2) {
866	sat_AddWL(cm, c, i, -1);
867	break;
868	}
869	else {
870	level = SATlevel(v);
871	if(level > maxLevel) {
872	maxLevel = level;
873	maxIndex = i;
874	}
875	}
876	}
877	}
878	if(i < 0)
879	sat_AddWL(cm, c, maxIndex, -1);
880
881
882	return(c);
883	}
884
885	/Function******************************************************************
886
887	Synopsis [ Add clause into clause database]
888
889	Description [ Add clause into clause database]
890
891	SideEffects []
892
893	SeeAlso []
894
895	******************************************************************************/
896	long
897	sat_AddBlockingClause(
898	satManager_t *cm,
899	satArray_t *clauseArray)
900	{
901	satLiteralDB_t *literals;
902	satStatistics_t *stats;
903	long c, v;
904	int inverted;
905	long last, space;
906	int i, size;
907	int maxLevel, maxIndex;
908	int value, level;
909	int otherWLIndex;
910
911	literals = cm->literals;
912	stats = cm->each;
913
914	while(literals->last + clauseArray->num + 2 >= literals->end) {
915	if(!sat_EnlargeLiteralDB(cm)) {
916	fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
917	cm->comment);
918	exit(0);
919	}
920	}
921
922	if(clauseArray->num == 1)
923	return(sat_AddUnitBlockingClause(cm, clauseArray));
924
925	c = 0;
926	if(cm->unusedAigQueue)
927	c = sat_Dequeue(cm->unusedAigQueue);
928	if(c == 0)
929	c = sat_CreateNode(cm, 2, 2);
930
931	last = literals->last;
932	*(last) = (-c);
933	last++;
934
935	/**
936	SATfirstLit(c) = (int)last;
937	**/
938	(cm->nodesArray[c+satFirstLit]) = (long)last;
939	SATnumLits(c) = clauseArray->num;
940	SATflags(c) \|= IsCNFMask;
941	SATsetInUse(c);
942	SATnumConflict(c) = 0;
943
944	size = clauseArray->num;
945	space = clauseArray->space;
946	for(i=0; i<size; i++, space++) {
947	v = *space;
948	inverted = !SATisInverted(v);
949	v = SATnormalNode(v);
950
951	*(last) = ((v^inverted) << 2);
952	last++;
953	}
954	*(last) = (-c);
955	last++;
956
957	literals->last = last;
958
959	maxLevel = -1;
960	maxIndex = -1;
961	otherWLIndex = -1;
962	space = clauseArray->space;
963	for(i=0; i<size; i++, space++) {
964	v = *space;
965	inverted = SATisInverted(v);
966	v = SATnormalNode(v);
967	value = SATvalue(v);
968	if(value == 2) {
969	sat_AddWL(cm, c, i, 1);
970	otherWLIndex = i;
971	break;
972	}
973	else {
974	level = SATlevel(v);
975	if(level > maxLevel) {
976	maxLevel = level;
977	maxIndex = i;
978	}
979	}
980	}
981	if(i >= size) {
982	sat_AddWL(cm, c, maxIndex, 1);
983	otherWLIndex = maxIndex;
984	}
985
986	maxLevel = -1;
987	maxIndex = -1;
988	space = clauseArray->space+size-1;
989	for(i=size-1; i>=0; i--, space--) {
990	v = *space;
991	inverted = SATisInverted(v);
992	v = SATnormalNode(v);
993	value = SATvalue(v);
994	if(i != otherWLIndex) {
995	if(value == 2) {
996	sat_AddWL(cm, c, i, -1);
997	break;
998	}
999	else {
1000	level = SATlevel(v);
1001	if(level > maxLevel) {
1002	maxLevel = level;
1003	maxIndex = i;
1004	}
1005	}
1006	}
1007	}
1008	if(i < 0)
1009	sat_AddWL(cm, c, maxIndex, -1);
1010
1011	SATflags(c) \|= IsBlockingMask;
1012
1013	stats = cm->each;
1014	stats->nBlockingCl++;
1015	stats->nBlockingLit += clauseArray->num;
1016
1017	return(c);
1018	}
1019
1020
1021	/Function******************************************************************
1022
1023	Synopsis [ Make literal watched ]
1024
1025	Description [ Make literal watched ]
1026
1027	SideEffects []
1028
1029	SeeAlso []
1030
1031	******************************************************************************/
1032	void
1033	sat_AddWL(
1034	satManager_t *cm,
1035	long c,
1036	int index,
1037	int dir)
1038	{
1039	long *plit, v;
1040	int inverted;
1041	satVariable_t *var;
1042
1043	plit = (long*)SATfirstLit(c) + index;
1044	v = SATgetNode(*plit);
1045	inverted = !SATisInverted(v);
1046	v = SATnormalNode(v);
1047	var = SATgetVariable(v);
1048
1049	if(var->wl[inverted] == 0)
1050	var->wl[inverted] = sat_ArrayAlloc(4);
1051	sat_ArrayInsert(var->wl[inverted], (long)plit);
1052	SATsetWL(plit, dir);
1053	}
1054
1055
1056	/Function******************************************************************
1057
1058	Synopsis [ Allocate array ]
1059
1060	Description [ Allocate array ]
1061
1062	SideEffects []
1063
1064	SeeAlso []
1065
1066	******************************************************************************/
1067	satArray_t *
1068	sat_ArrayAlloc(long number)
1069	{
1070	satArray_t *array;
1071
1072	array = ALLOC(satArray_t, 1);
1073	if (array) {
1074	array->num = 0;
1075	array->size = number;
1076	array->space = ALLOC(long, number);
1077	if (array->space) {
1078	return array;
1079	}
1080	}
1081	//Bing: To avoid segmentation fault
1082	if(array==0 \|\| (number>0&&array->space==0)){
1083	printf("can't alloc mem, exit\n");
1084	exit(0);
1085	}
1086	return 0;
1087	}
1088
1089	/Function******************************************************************
1090
1091	Synopsis [ Duplicate array ]
1092
1093	Description [ Duplicate array ]
1094
1095	SideEffects []
1096
1097	SeeAlso []
1098
1099	******************************************************************************/
1100	satArray_t *
1101	sat_ArrayDuplicate(satArray_t *old)
1102	{
1103	satArray_t *array;
1104
1105	array = (satArray_t *)malloc(sizeof(satArray_t));
1106	if (array) {
1107	array->num = old->num;
1108	array->size = old->num;
1109	array->space = (long )malloc(sizeof(long) old->num);
1110	memcpy(array->space, old->space, sizeof(long)*old->num);
1111	if (array->space) {
1112	return array;
1113	}
1114	}
1115	return 0;
1116	}
1117
1118	/Function******************************************************************
1119
1120	Synopsis [ Insert entries to array ]
1121
1122	Description [ Insert entries to array ]
1123
1124	SideEffects []
1125
1126	SeeAlso []
1127
1128	******************************************************************************/
1129	void
1130	sat_ArrayInsert(satArray_t *array, long datum)
1131	{
1132	if(array->num < array->size) {
1133	array->space[array->num++] = datum;
1134	}
1135	else {
1136	array->size <<= 1;
1137	array->space = REALLOC(long, array->space, array->size);
1138	if(array->space == 0) {
1139	fprintf(stdout, "ERROR : Can't allocate memory in sat_ArrayInsert\n");
1140	exit(0);
1141	}
1142	array->space[array->num++] = datum;
1143	}
1144	}
1145
1146	/Function******************************************************************
1147
1148	Synopsis [ Free array ]
1149
1150	Description [ Free array ]
1151
1152	SideEffects []
1153
1154	SeeAlso []
1155
1156	******************************************************************************/
1157	void
1158	sat_ArrayFree(satArray_t *array)
1159	{
1160	free(array->space);
1161	free(array);
1162	}
1163
1164
1165	/Function******************************************************************
1166
1167	Synopsis [ Create queue ]
1168
1169	Description [ Create queue ]
1170
1171	SideEffects []
1172
1173	SeeAlso []
1174
1175	******************************************************************************/
1176	satQueue_t *
1177	sat_CreateQueue( long MaxElements )
1178	{
1179	satQueue_t *Q;
1180
1181	Q = ALLOC(satQueue_t, 1);
1182	if( Q == NULL )
1183	fprintf(stderr, "Out of space!!!\n" );
1184
1185	Q->array = ALLOC(long, MaxElements );
1186	if( Q->array == NULL )
1187	fprintf(stderr, "Out of space!!!\n" );
1188	Q->max = MaxElements;
1189	Q->size = 0;
1190	Q->front = 1;
1191	Q->rear = 0;
1192	return Q;
1193	}
1194
1195	/Function******************************************************************
1196
1197	Synopsis [ Free queue ]
1198
1199	Description [ Free queue ]
1200
1201	SideEffects []
1202
1203	SeeAlso []
1204
1205	******************************************************************************/
1206	void
1207	sat_FreeQueue( satQueue_t *Q )
1208	{
1209	if( Q != NULL ) {
1210	free( Q->array );
1211	free( Q );
1212	}
1213	}
1214
1215
1216	/Function******************************************************************
1217
1218	Synopsis [ Enqueue node ]
1219
1220	Description [ Enqueue node ]
1221
1222	SideEffects []
1223
1224	SeeAlso []
1225
1226	******************************************************************************/
1227	void
1228	sat_Enqueue(satQueue_t *Q, long v)
1229	{
1230	long arr, oarr;
1231	long rear;
1232
1233	if(Q->size < Q->max) {
1234	Q->size++;
1235	rear = Q->rear;
1236	rear = (++(rear) == Q->max) ? 0 : rear;
1237	Q->array[rear] = v;
1238	Q->rear = rear;
1239	}
1240	else {
1241	arr = ALLOC(long, Q->size * 2 );
1242	if(arr == NULL )
1243	fprintf(stderr, "Out of space!!!\n" );
1244	oarr = Q->array;
1245	if(Q->front > Q->rear) {
1246	memcpy(&(arr[1]), &(oarr[Q->front]),
1247	sizeof(long) *(Q->max-Q->front));
1248	memcpy(&(arr[Q->size-Q->front+1]), &(oarr[0]),
1249	sizeof(long) *(Q->rear+1));
1250	}
1251	else if(Q->front < Q->rear) {
1252	memcpy(&(arr[1]), &(oarr[Q->front]), sizeof(long) *(Q->size));
1253	}
1254	free(oarr);
1255	Q->array = arr;
1256	Q->front = 1;
1257	Q->rear = Q->size;
1258	Q->max *= 2;
1259
1260	Q->size++;
1261	rear = Q->rear;
1262	rear = (++(rear) == Q->max) ? 0 : rear;
1263	Q->array[rear] = v;
1264	Q->rear = rear;
1265	}
1266	}
1267
1268
1269	/Function******************************************************************
1270
1271	Synopsis [ Dequeue ]
1272
1273	Description [ Dequeue ]
1274
1275	SideEffects []
1276
1277	SeeAlso []
1278
1279	******************************************************************************/
1280	long
1281	sat_Dequeue( satQueue_t * Q )
1282	{
1283	long front;
1284	long v;
1285
1286	if(Q->size > 0) {
1287	Q->size--;
1288	front = Q->front;
1289	v = Q->array[front];
1290	Q->front = (++(front) == Q->max) ? 0 : front;
1291	return v;
1292	}
1293	else
1294	return(0);
1295	}
1296
1297
1298	/Function******************************************************************
1299
1300	Synopsis [ Allocate decision level ]
1301
1302	Description [ Allocate decision level ]
1303
1304	SideEffects []
1305
1306	SeeAlso []
1307
1308	******************************************************************************/
1309	satLevel_t *
1310	sat_AllocLevel(
1311	satManager_t *cm)
1312	{
1313	satStatistics_t *stats;
1314	satLevel_t *d;
1315	satArray_t *implied;
1316	int size;
1317
1318	if(cm->decisionHeadSize == 0) {
1319	size = cm->currentDecision+2;
1320	cm->decisionHeadSize = size;
1321	cm->decisionHead = REALLOC(satLevel_t, cm->decisionHead, size);
1322	memset(cm->decisionHead, 0, sizeof(satLevel_t) * size);
1323	}
1324
1325	if(cm->currentDecision+1 >= cm->decisionHeadSize) {
1326	size = cm->decisionHeadSize;
1327	cm->decisionHeadSize <<=1;
1328	cm->decisionHead = REALLOC(satLevel_t, cm->decisionHead,
1329	cm->decisionHeadSize);
1330	memset(cm->decisionHead+size, 0, sizeof(satLevel_t) * size);
1331	}
1332
1333	cm->currentDecision++;
1334	d = &(cm->decisionHead[cm->currentDecision]);
1335	implied = d->implied;
1336	memset(d, 0, sizeof(satLevel_t));
1337	d->implied = implied;
1338	if(d->implied == 0){
1339	d->implied = sat_ArrayAlloc(64);
1340	//Bing: avoid seg fault
1341	if(d->implied == 0){
1342	printf("out of mem, exit\n");
1343	exit(0);
1344	}
1345	}
1346
1347	d->level = cm->currentDecision;
1348	d->conflict = 0;
1349
1350	stats = cm->each;
1351	if(stats->maxDecisionLevel < d->level)
1352	stats->maxDecisionLevel = d->level;
1353
1354	return(d);
1355
1356	}
1357
1358	/Function******************************************************************
1359
1360	Synopsis [ Clean decision level when backtracking ]
1361
1362	Description [ Clean decision level when backtracking ]
1363
1364	SideEffects []
1365
1366	SeeAlso []
1367
1368	******************************************************************************/
1369	void
1370	sat_CleanLevel(
1371	satLevel_t *d)
1372	{
1373	if(d->implied)
1374	d->implied->num = 0;
1375	if(d->satisfied)
1376	d->satisfied->num = 0;
1377	d->currentVarPos = 0;
1378	}
1379
1380	/Function******************************************************************
1381
1382	Synopsis [ Delete conflict clauses ]
1383
1384	Description [ Delete conflict clauses ]
1385
1386	SideEffects []
1387
1388	SeeAlso []
1389
1390	******************************************************************************/
1391	void
1392	sat_ClauseDeletion(satManager_t *cm)
1393	{
1394	satLiteralDB_t *literals;
1395	satOption_t *option;
1396	long v, *plit, nv, lit;
1397	int size, n0, n1x, deleteFlag;
1398	int unrelevance;
1399	int inverted, i;
1400	int value;
1401	double ratio;
1402
1403	/**
1404	LATEST_ACTIVITY_DELETION
1405	MAX_UNRELEVANCE_DELETION
1406	SIMPLE_LATEST_DELETION
1407	**/
1408
1409	option = cm->option;
1410	if(option->clauseDeletionHeuristic == 0) return;
1411
1412	literals = cm->literals;
1413	for(v=cm->beginConflict; v<cm->nodesArraySize; v+=satNodeSize) {
1414	if(!(SATflags(v) & IsCNFMask)) continue;
1415	if(SATreadInUse(v) == 0) continue;
1416
1417	if(option->incPreserveNonobjective && (SATflags(v) & NonobjMask))
1418	continue;
1419
1420	size = SATnumLits(v);
1421	if(size < option->minLitsLimit) continue;
1422
1423	plit = (long*)SATfirstLit(v);
1424
1425	unrelevance = option->unrelevance;
1426	if(option->clauseDeletionHeuristic & SIMPLE_LATEST_DELETION) {
1427	ratio = (double)(plit-literals->initialSize)/
1428	(double)(literals->last-literals->initialSize);
1429	if(ratio > 0.8) unrelevance <<= 3;
1430	}
1431	if(!(option->clauseDeletionHeuristic & MAX_UNRELEVANCE_DELETION)) {
1432	unrelevance = MAXINT;
1433	}
1434
1435	n0 = n1x = 0;
1436	deleteFlag = 0;
1437	for(i=0; i<size; i++, plit++) {
1438	lit = *plit;
1439	nv = SATgetNode(lit);
1440	inverted = SATisInverted(nv);
1441	nv = SATnormalNode(nv);
1442	value = SATvalue(nv) ^ inverted;
1443
1444	if(value == 0) n0++;
1445	else if(value == 1) {
1446	n1x++;
1447	if(SATlevel(nv) == 0 && cm->option->coreGeneration == 0)
1448	deleteFlag = 1;
1449	}
1450	else n1x++;
1451
1452	if(deleteFlag) {
1453	sat_DeleteClause(cm, v);
1454	sat_Enqueue(cm->unusedAigQueue, v);
1455	break;
1456	}
1457	if((size > option->maxLitsLimit) && (n1x > 1)) {
1458	sat_DeleteClause(cm, v);
1459	sat_Enqueue(cm->unusedAigQueue, v);
1460	break;
1461	}
1462	if(n1x > unrelevance) {
1463	sat_DeleteClause(cm, v);
1464	sat_Enqueue(cm->unusedAigQueue, v);
1465	break;
1466	}
1467	}
1468
1469	}
1470	}
1471
1472	/Function******************************************************************
1473
1474	Synopsis [ Delete conflict clauses ]
1475
1476	Description [ Delete conflict clauses ]
1477
1478	SideEffects []
1479
1480	SeeAlso []
1481
1482	******************************************************************************/
1483	void
1484	sat_DeleteClause(
1485	satManager_t *cm,
1486	long v)
1487	{
1488	satStatistics_t *stats;
1489	int size, i;
1490	long nv, *plit;
1491
1492	stats = cm->each;
1493	size = SATnumLits(v);
1494	stats->nDeletedCl++;
1495	stats->nDeletedLit += size;
1496
1497	/ SATresetInUse(v); /
1498	SATflags(v) = 0;
1499	SATflags(v) \|= IsCNFMask;
1500
1501	for(i=0, plit=(long*)SATfirstLit(v); i<size; i++, plit++) {
1502	nv = SATgetNode(*plit);
1503	*plit = 0;
1504	}
1505	}
1506
1507	/Function******************************************************************
1508
1509	Synopsis [ Compact clause database ]
1510
1511	Description [ Compact clause database ]
1512
1513	SideEffects []
1514
1515	SeeAlso []
1516
1517	******************************************************************************/
1518	void
1519	sat_CompactClauses(satManager_t *cm)
1520	{
1521	satLiteralDB_t *literals;
1522	long *plit, v, lit;
1523	int i, size, index;
1524	int inverted;
1525	satVariable_t *var;
1526
1527	literals = cm->literals;
1528	size = literals->last - literals->begin;
1529
1530	plit = literals->begin;
1531	index = literals->initialSize-literals->begin;
1532	for(i=literals->initialSize-literals->begin; i<size; i++) {
1533	if(i < 2) {
1534	plit[index] = plit[i];
1535	index++;
1536	continue;
1537	}
1538
1539	if(plit[i-1] == 0 && plit[i] < 0) continue;
1540	else if(plit[i-1] == 0 && plit[i] == 0) continue;
1541	else if(plit[i-1] < 0 && plit[i] == 0) continue;
1542	else if(plit[i-1] < 0 && plit[i] < 0 && plit[i+1] == 0) continue;
1543	else {
1544	plit[index] = plit[i];
1545	index++;
1546	}
1547	}
1548
1549	literals->last = literals->begin + index;
1550	for(v=satNodeSize; v<cm->beginConflict; v+=satNodeSize) {
1551	if(SATflags(v) & IsCNFMask) continue;
1552	var = SATgetVariable(v);
1553	if(var->wl[0]) var->wl[0]->num = 0;
1554	if(var->wl[1]) var->wl[1]->num = 0;
1555	}
1556
1557	size = literals->last - literals->begin;
1558	plit = literals->begin;
1559	for(i=0; i<size; i++) {
1560	lit = plit[i];
1561	if(lit > 0 && SATisWL(lit)) {
1562	v = SATgetNode(lit);
1563	inverted = !(SATisInverted(v));
1564	v = SATnormalNode(v);
1565	var = SATgetVariable(v);
1566	if(var->wl[inverted] == 0)
1567	var->wl[inverted] = sat_ArrayAlloc(4);
1568	sat_ArrayInsert(var->wl[inverted], (long)(&(plit[i])));
1569	}
1570
1571	if(lit <= 0) {
1572	v = -lit;
1573	/**
1574	SATfirstLit(v) = (int)(&(plit[i]) - SATnumLits(v));
1575	**/
1576	(cm->nodesArray[v+satFirstLit]) = (long)(&(plit[i]) - SATnumLits(v));
1577	}
1578	}
1579
1580	plit = literals->last - 1;
1581	cm->currentTopConflict = plit;
1582	cm->currentTopConflictCount = 0;
1583
1584	}
1585
1586	/Function******************************************************************
1587
1588	Synopsis [ Enlarge clause database ]
1589
1590	Description [ Enlarge clause database ]
1591
1592	SideEffects []
1593
1594	SeeAlso []
1595
1596	******************************************************************************/
1597	int
1598	sat_EnlargeLiteralDB(satManager_t *cm)
1599	{
1600	satLiteralDB_t *literals;
1601	int nLiveConflictCl, nLiveConflictLit;
1602	double ratio, growRatio;
1603	double memUsage;
1604	long oldBegin, oldEnd;
1605	long newSize, oldSize;
1606	int offset, index, size;
1607	int i, j, nodesSize;
1608	long tv;
1609	int arrSize;
1610	satVariable_t *var;
1611	satArray_t *wl;
1612	satStatistics_t *stats;
1613	satOption_t *option;
1614
1615
1616	literals = cm->literals;
1617	option = cm->option;
1618	stats = cm->each;
1619
1620	size = literals->last - literals->begin;
1621	nLiveConflictCl = cm->initNumClauses + stats->nConflictCl + stats->nBlockingCl - stats->nDeletedCl;
1622	nLiveConflictLit = cm->initNumLiterals + stats->nBlockingLit +
1623	stats->nConflictLit - stats->nDeletedLit ;
1624	ratio = (double)(nLiveConflictLit + (nLiveConflictCl << 1)) /
1625	(double)(size);
1626
1627	if(ratio < 0.8) {
1628	sat_CompactClauses(cm);
1629	return(1);
1630	}
1631
1632	memUsage = (double)sat_MemUsage(cm);
1633	growRatio = 1.0;
1634	if(memUsage < (double)option->memoryLimit/4.0) growRatio = 2.0;
1635	else if(memUsage < (double)option->memoryLimit/2.0) growRatio = 1.5;
1636	else if(memUsage < (double)option->memoryLimit*0.8) growRatio = 1.2;
1637
1638	if(growRatio < 1.5) {
1639	if(ratio < 0.9) {
1640	sat_CompactClauses(cm);
1641	return(1);
1642	}
1643	}
1644
1645	oldBegin = literals->begin;
1646	oldEnd = literals->end;
1647	oldSize = literals->last - literals->begin;
1648	newSize = oldSize * (int)growRatio;
1649
1650	literals->begin = REALLOC(long, oldBegin, newSize);
1651	literals->last = literals->begin + oldSize;
1652	literals->end = literals->begin + newSize;
1653
1654	offset = literals->begin - oldBegin;
1655	nodesSize = cm->nodesArraySize;
1656	for(i=satNodeSize; i<nodesSize; i+= satNodeSize) {
1657	tv = i;
1658	if(SATflags(tv) & IsCNFMask) {
1659	if(SATreadInUse(tv))
1660	(cm->nodesArray[tv+satFirstLit]) = (long)((long*)(SATfirstLit(tv)) + offset);
1661	/**
1662	SATfirstLit(tv) = (int)((int*)(SATfirstLit(tv)) + offset);
1663	**/
1664	}
1665	else if(SATflags(tv) & IsBDDMask) {
1666	(cm->nodesArray[tv+satFirstLit]) = (long)((long*)(SATfirstLit(tv)) + offset);
1667	/**
1668	SATfirstLit(tv) = (int)((int*)(SATfirstLit(tv)) + offset);
1669	**/
1670	}
1671	else {
1672	var = SATgetVariable(tv);
1673	wl = var->wl[0];
1674	if(wl) {
1675	arrSize = wl->num;
1676	for(j=0, index=0; j<arrSize; j++) {
1677	if(wl->space[j] == 0) continue;
1678	wl->space[j] = (long)(((long*)(wl->space[j])) + offset);
1679	}
1680	}
1681	wl = var->wl[1];
1682	if(wl) {
1683	arrSize = wl->num;
1684	for(j=0, index=0; j<arrSize; j++) {
1685	if(wl->space[j] == 0) continue;
1686	wl->space[j] = (long)(((long*)(wl->space[j])) + offset);
1687	}
1688	}
1689	}
1690	}
1691	literals->initialSize = literals->initialSize + offset;
1692	cm->currentTopConflict += offset;
1693
1694	return(1);
1695	}
1696
1697	/Function******************************************************************
1698
1699	Synopsis [ Allocate clause database ]
1700
1701	Description [ Allocate clause database ]
1702
1703	SideEffects []
1704
1705	SeeAlso []
1706
1707	******************************************************************************/
1708	void
1709	sat_AllocLiteralsDB(satManager_t *cm)
1710	{
1711	satLiteralDB_t *literals;
1712	int size;
1713
1714	literals = cm->literals;
1715	if(literals) return;
1716
1717	literals = ALLOC(satLiteralDB_t, 1);
1718	cm->literals = literals;
1719
1720	size = 1024 * 1024;
1721	literals->begin = ALLOC(long, size);
1722	*(literals->begin) = 0;
1723	literals->last = literals->begin + 1;
1724	literals->end = literals->begin + size;
1725	/ CONSIDER... /
1726	literals->initialSize = literals->last;
1727
1728	}
1729
1730
1731	/Function******************************************************************
1732
1733	Synopsis [ Free clause database ]
1734
1735	Description [ Free clause database ]
1736
1737	SideEffects []
1738
1739	SeeAlso []
1740
1741	******************************************************************************/
1742	void
1743	sat_FreeLiteralsDB(satLiteralDB_t *literals)
1744	{
1745
1746	if(literals == 0) return;
1747	free(literals->begin);
1748	literals->begin = 0;
1749	free(literals);
1750	}
1751
1752	/Function******************************************************************
1753
1754	Synopsis [ clean value and flag of node ]
1755
1756	Description [ clean value and flag of node ]
1757
1758	SideEffects []
1759
1760	SeeAlso []
1761
1762	******************************************************************************/
1763	void
1764	sat_CleanDatabase(satManager_t *cm)
1765	{
1766	long v, i;
1767
1768	for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
1769	v = i;
1770	SATvalue(v) = 2;
1771	SATflags(v) &= PreserveMask;
1772	}
1773	}
1774
1775	/Function******************************************************************
1776
1777	Synopsis [ Compact fanout of AIG node ]
1778
1779	Description [ Compact fanout of AIG node ]
1780
1781	SideEffects []
1782
1783	SeeAlso []
1784
1785	******************************************************************************/
1786	void
1787	sat_CompactFanout(satManager_t *cm)
1788	{
1789	int bufSize, bufIndex;
1790	long buf, fan;
1791	long i, v, cur;
1792	int j, size, tsize;
1793
1794	bufSize = 1024;
1795	bufIndex = 0;
1796	buf = ALLOC(long, bufSize);
1797	for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
1798	v = i;
1799
1800	if(!(SATflags(v) & CoiMask))
1801	continue;
1802
1803	size = SATnFanout(v);
1804	if(size >= bufSize) {
1805	bufSize <<= 1;
1806	if(size >= bufSize)
1807	bufSize = size + 1;
1808	buf = REALLOC(long, buf, bufSize);
1809	}
1810
1811	bufIndex = 0;
1812	for(j=0, fan = SATfanout(v); j<size; j++) {
1813	cur = fan[j];
1814	cur >>= 1;
1815	cur = SATnormalNode(cur);
1816	if(!(SATflags(cur) & CoiMask))
1817	continue;
1818	buf[bufIndex++] = fan[j];
1819	}
1820
1821	if(bufIndex > 0) {
1822	tsize = bufIndex;
1823	for(j=0, fan=SATfanout(v); j<size; j++) {
1824	cur = fan[j];
1825	cur >>= 1;
1826	cur = SATnormalNode(cur);
1827	if(!(SATflags(cur) & CoiMask)) {
1828	buf[bufIndex++] = fan[j];
1829	continue;
1830	}
1831	}
1832	buf[bufIndex] = 0;
1833	memcpy(fan, buf, sizeof(long)*(size+1));
1834	SATnFanout(v) = tsize;
1835	}
1836	else {
1837	SATnFanout(v) = 0;
1838	}
1839	}
1840
1841	free(buf);
1842
1843	for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
1844	v = i;
1845	if(!(SATflags(v) & CoiMask))
1846	continue;
1847	fan = SATfanout(v);
1848	size = SATnFanout(v);
1849	qsort(fan, size, sizeof(long), NodeIndexCompare);
1850	}
1851	}
1852
1853
1854
1855	/Function******************************************************************
1856
1857	Synopsis [ Restore fanout of AIG node ]
1858
1859	Description [ Restore fanout of AIG node ]
1860
1861	SideEffects []
1862
1863	SeeAlso []
1864
1865	******************************************************************************/
1866	void
1867	sat_RestoreFanout(satManager_t *cm)
1868	{
1869	long i, v;
1870
1871	for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
1872	v = i;
1873	if((SATflags(v) & IsCNFMask))
1874	continue;
1875	SATnFanout(v) = sat_GetFanoutSize(cm, v);
1876	}
1877	}
1878
1879	/Function******************************************************************
1880
1881	Synopsis [ Get fanout size of AIG node ]
1882
1883	Description [ Get fanout size of AIG node ]
1884
1885	SideEffects []
1886
1887	SeeAlso []
1888
1889	******************************************************************************/
1890	int
1891	sat_GetFanoutSize(
1892	satManager_t *cm,
1893	long v)
1894	{
1895	long *fan;
1896	int i;
1897
1898	fan = SATfanout(v);
1899	if(fan == 0) return(0);
1900
1901	for(i=0; fan[i]!=0; i++);
1902	return(i);
1903	}
1904
1905	/Function******************************************************************
1906
1907	Synopsis [ Mark transitive fanin of given array of node ]
1908
1909	Description [ Mark transitive fanin of given array of node ]
1910
1911	SideEffects []
1912
1913	SeeAlso []
1914
1915	******************************************************************************/
1916	void
1917	sat_MarkTransitiveFaninForArray(
1918	satManager_t *cm,
1919	satArray_t *arr,
1920	unsigned int mask)
1921	{
1922	long v;
1923	int i, size;
1924
1925	if(arr == 0) return;
1926	size = arr->num;
1927
1928	for(i=0; i<size; i++) {
1929	v = arr->space[i];
1930	sat_MarkTransitiveFaninForNode(cm, v, mask);
1931	}
1932	}
1933
1934	/Function******************************************************************
1935
1936	Synopsis [ Mark transitive fanin of given node ]
1937
1938	Description [ Mark transitive fanin of given node ]
1939
1940	SideEffects []
1941
1942	SeeAlso []
1943
1944	******************************************************************************/
1945	void
1946	sat_MarkTransitiveFaninForNode(
1947	satManager_t *cm,
1948	long v,
1949	unsigned int mask)
1950	{
1951	if(v == 2) return;
1952
1953	v = SATnormalNode(v);
1954
1955	if(SATflags(v) & mask) return;
1956
1957	SATflags(v) \|= mask;
1958
1959	sat_MarkTransitiveFaninForNode(cm, SATleftChild(v), mask);
1960	sat_MarkTransitiveFaninForNode(cm, SATrightChild(v), mask);
1961	}
1962
1963	/Function******************************************************************
1964
1965	Synopsis [ Unmark transitive fanin of given array of node ]
1966
1967	Description [ Unmark transitive fanin of given array of node ]
1968
1969	SideEffects []
1970
1971	SeeAlso []
1972
1973	******************************************************************************/
1974	void
1975	sat_UnmarkTransitiveFaninForArray(
1976	satManager_t *cm,
1977	satArray_t *arr,
1978	unsigned int mask,
1979	unsigned int resetMask)
1980	{
1981	long v;
1982	int i, size;
1983
1984	size = arr->num;
1985
1986	for(i=0; i<size; i++) {
1987	v = arr->space[i];
1988	sat_UnmarkTransitiveFaninForNode(cm, v, mask, resetMask);
1989	}
1990	}
1991
1992	/Function******************************************************************
1993
1994	Synopsis [ Unmark transitive fanin of given node ]
1995
1996	Description [ Unmark transitive fanin of given node ]
1997
1998	SideEffects []
1999
2000	SeeAlso []
2001
2002	******************************************************************************/
2003	void
2004	sat_UnmarkTransitiveFaninForNode(
2005	satManager_t *cm,
2006	long v,
2007	unsigned int mask,
2008	unsigned int resetMask)
2009	{
2010	if(v == 2) return;
2011
2012	v = SATnormalNode(v);
2013
2014	if(!(SATflags(v) & mask)) return;
2015
2016	SATflags(v) &= resetMask;
2017	sat_UnmarkTransitiveFaninForNode(cm, SATleftChild(v), mask, resetMask);
2018	sat_UnmarkTransitiveFaninForNode(cm, SATrightChild(v), mask, resetMask);
2019	}
2020
2021
2022	/Function******************************************************************
2023
2024	Synopsis [ Set COIMask ]
2025
2026	Description [ Set COIMask. The COIMask of flags of node has be set to
2027	apply implication on it ]
2028
2029	SideEffects []
2030
2031	SeeAlso []
2032
2033	******************************************************************************/
2034	void
2035	sat_SetConeOfInfluence(satManager_t *cm)
2036	{
2037	sat_MarkTransitiveFaninForArray(cm, cm->assertion, CoiMask);
2038	sat_MarkTransitiveFaninForArray(cm, cm->auxObj, CoiMask);
2039	sat_MarkTransitiveFaninForArray(cm, cm->obj, CoiMask);
2040	//Bing:
2041	sat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);
2042	}
2043
2044
2045	/Function******************************************************************
2046
2047	Synopsis [ Allocate manager for SAT solving]
2048
2049	Description [ Allocate manager for SAT solving]
2050
2051	SideEffects []
2052
2053	SeeAlso []
2054
2055	******************************************************************************/
2056	satManager_t *
2057	sat_InitManager(satInterface_t *interface)
2058	{
2059	satManager_t *cm;
2060
2061	cm = ALLOC(satManager_t, 1);
2062	memset(cm, 0, sizeof(satManager_t));
2063
2064	if(interface) {
2065	cm->total = interface->total;
2066	cm->nonobjUnitLitArray = interface->nonobjUnitLitArray;
2067	cm->savedConflictClauses = interface->savedConflictClauses;
2068	cm->trieArray = interface->trieArray;
2069	cm->objUnitLitArray = sat_ArrayAlloc(8);
2070	}
2071	else {
2072	cm->total = sat_InitStatistics();
2073	cm->objUnitLitArray = sat_ArrayAlloc(8);
2074	cm->nonobjUnitLitArray = sat_ArrayAlloc(8);
2075	}
2076
2077	return(cm);
2078	}
2079
2080	/Function******************************************************************
2081
2082	Synopsis [ Free manager after SAT solving]
2083
2084	Description [ Free manager after SAT solving]
2085
2086	SideEffects []
2087
2088	SeeAlso []
2089
2090	******************************************************************************/
2091	void
2092	sat_FreeManager(satManager_t *cm)
2093	{
2094	satVariable_t *var;
2095	satLevel_t *d;
2096	int i;
2097
2098	if(cm->option) sat_FreeOption(cm->option);
2099	if(cm->total) sat_FreeStatistics(cm->total);
2100	if(cm->each) sat_FreeStatistics(cm->each);
2101
2102	if(cm->literals) sat_FreeLiteralsDB(cm->literals);
2103
2104	if(cm->decisionHead) {
2105	for(i=0; i<cm->decisionHeadSize; i++) {
2106	d = &(cm->decisionHead[i]);
2107	if(d->implied)
2108	sat_ArrayFree(d->implied);
2109	if(d->satisfied)
2110	sat_ArrayFree(d->satisfied);
2111	}
2112	free(cm->decisionHead);
2113	cm->decisionHead = 0;
2114	cm->decisionHeadSize = 0;
2115	}
2116
2117	if(cm->queue) sat_FreeQueue(cm->queue);
2118	if(cm->BDDQueue) sat_FreeQueue(cm->BDDQueue);
2119	if(cm->unusedAigQueue)sat_FreeQueue(cm->unusedAigQueue);
2120	cm->queue = 0;
2121	cm->BDDQueue = 0;
2122	cm->unusedAigQueue = 0;
2123
2124	if(cm->auxObj) sat_ArrayFree(cm->auxObj);
2125	if(cm->obj) sat_ArrayFree(cm->obj);
2126	if(cm->unitLits) sat_ArrayFree(cm->unitLits);
2127	if(cm->pureLits) sat_ArrayFree(cm->pureLits);
2128	if(cm->assertion) sat_ArrayFree(cm->assertion);
2129	if(cm->auxArray) sat_ArrayFree(cm->auxArray);
2130	if(cm->nonobjUnitLitArray) sat_ArrayFree(cm->nonobjUnitLitArray);
2131	if(cm->objUnitLitArray) sat_ArrayFree(cm->objUnitLitArray);
2132	if(cm->orderedVariableArray) sat_ArrayFree(cm->orderedVariableArray);
2133	if(cm->clauseIndexInCore) sat_ArrayFree(cm->clauseIndexInCore);
2134	cm->auxObj = 0;
2135	cm->obj = 0;
2136	cm->unitLits = 0;
2137	cm->pureLits = 0;
2138	cm->assertion = 0;
2139	cm->auxArray = 0;
2140	cm->nonobjUnitLitArray = 0;
2141	cm->objUnitLitArray = 0;
2142	cm->orderedVariableArray = 0;
2143
2144	if(cm->variableArray) {
2145	for(i=0; i<=cm->initNumVariables; i++) {
2146	var = &(cm->variableArray[i]);
2147	if(var->wl[0]) {
2148	sat_ArrayFree(var->wl[0]);
2149	var->wl[0] = 0;
2150	}
2151	if(var->wl[1]) {
2152	sat_ArrayFree(var->wl[1]);
2153	var->wl[1] = 0;
2154	}
2155	}
2156	free(cm->variableArray);
2157	cm->variableArray = 0;
2158	}
2159
2160
2161	if(cm->comment) free(cm->comment);
2162
2163	if(cm->nodesArray) free(cm->nodesArray);
2164	free(cm);
2165	}
2166
2167	/Function******************************************************************
2168
2169	Synopsis [ Free option after SAT solving]
2170
2171	Description [ Free option after SAT solving]
2172
2173	SideEffects []
2174
2175	SeeAlso []
2176
2177	******************************************************************************/
2178	void
2179	sat_FreeOption(satOption_t * option)
2180	{
2181	if(option)
2182	free(option);
2183	}
2184
2185	/Function******************************************************************
2186
2187	Synopsis [ Free statistic after SAT solving]
2188
2189	Description [ Free statistic after SAT solving]
2190
2191	SideEffects []
2192
2193	SeeAlso []
2194
2195	******************************************************************************/
2196	void
2197	sat_FreeStatistics(satStatistics_t * stats)
2198	{
2199	if(stats)
2200	free(stats);
2201	}
2202
2203
2204	/Function******************************************************************
2205
2206	Synopsis [ Allocate option]
2207
2208	Description [ Allocate option ]
2209
2210	SideEffects []
2211
2212	SeeAlso []
2213
2214	******************************************************************************/
2215	satOption_t *
2216	sat_InitOption()
2217	{
2218	satOption_t *option;
2219
2220	option = ALLOC(satOption_t, 1);
2221	memset(option, 0, sizeof(satOption_t));
2222
2223	option->decisionHeuristic \|= LATEST_CONFLICT_DECISION;
2224	/**
2225	option->decisionHeuristic \|= DVH_DECISION;
2226	**/
2227	option->decisionAgeInterval = 0xff;
2228	option->decisionAgeRestart = 1;
2229	option->minConflictForDecision = 50;
2230	option->maxConflictForDecision = 10000;
2231	option->skipSatisfiedClauseForDecision = 0;
2232
2233
2234	/**
2235	option->clauseDeletionHeuristic \|= MAX_UNRELEVANCE_DELETION;
2236	option->clauseDeletionHeuristic \|= SIMPLE_LATEST_DELETION;
2237	**/
2238	option->clauseDeletionHeuristic \|= LATEST_ACTIVITY_DELETION;
2239	option->clauseDeletionInterval = 2500;
2240	option->nextClauseDeletion = option->clauseDeletionInterval*5;
2241	option->unrelevance = 20;
2242	option->minLitsLimit = 20;
2243	option->maxLitsLimit = 1000;
2244
2245	option->latestUnrelevance = 45;
2246	option->obsoleteUnrelevance = 20;//6
2247	option->latestUsage = 100;
2248	option->obsoleteUsage = 2;
2249	option->latestRate = 16;
2250
2251	option->incNumObjLitsLimit = 20; / 50 /
2252	option->incNumNonobjLitsLimit = 50;
2253
2254	option->incPreserveNonobjective = 1;
2255	option->minimizeConflictClause = 1;
2256
2257
2258	option->BDDMonolithic = 0;
2259	option->BDDDPLL = 0;
2260	option->maxLimitOfVariablesForMonolithicBDD = 2000;
2261	option->maxLimitOfClausesForMonolithicBDD = 20000;
2262	option->maxLimitOfCutSizeForMonolithicBDD = 2000;
2263
2264	option->maxLimitOfVariablesForBDDDPLL = 200;
2265	option->maxLimitOfClausesForBDDDPLL = 2000;
2266	option->maxLimitOfCutSizeForBDDDPLL = 500;
2267
2268	option->maxLimitOfVariablesForBDD = 50;
2269
2270	option->memoryLimit = 1024 * 1024 * 1024;
2271
2272	return(option);
2273	}
2274
2275	/Function******************************************************************
2276
2277	Synopsis [ Report statistics]
2278
2279	Description [ Report statistics]
2280
2281	SideEffects []
2282
2283	SeeAlso []
2284
2285	******************************************************************************/
2286	void
2287	sat_ReportStatistics(
2288	satManager_t *cm,
2289	satStatistics_t *stats)
2290	{
2291	satOption_t *option;
2292
2293	option = cm->option;
2294	fprintf(cm->stdOut, "%s Number of decisions %d\n",
2295	cm->comment, stats->nDecisions);
2296	if(option->decisionHeuristic & DVH_DECISION) {
2297	fprintf(cm->stdOut, "%s Number of DVH decisions %d\n",
2298	cm->comment, stats->nDVHDecisions);
2299	}
2300	if(option->decisionHeuristic & LATEST_CONFLICT_DECISION) {
2301	fprintf(cm->stdOut, "%s Number of latest conflict decisions %d\n",
2302	cm->comment, stats->nLatestConflictDecisions);
2303	}
2304	fprintf(cm->stdOut, "%s Number of backtracks %d\n",
2305	cm->comment, stats->nBacktracks);
2306
2307	fprintf(cm->stdOut, "%s Number of CNF implications %d\n",
2308	cm->comment, stats->nCNFImplications);
2309	fprintf(cm->stdOut, "%s Number of Aig implications %d\n",
2310	cm->comment, stats->nAigImplications);
2311	fprintf(cm->stdOut, "%s Number of BDD implications %d\n",
2312	cm->comment, stats->nBDDImplications);
2313
2314	fprintf(cm->stdOut, "%s Number of unit conflict clauses %d\n",
2315	cm->comment, stats->nUnitConflictCl);
2316	fprintf(cm->stdOut, "%s Number of conflict clauses %d\n",
2317	cm->comment, stats->nConflictCl);
2318	fprintf(cm->stdOut, "%s Number of conflict literals %d\n",
2319	cm->comment, stats->nConflictLit);
2320	fprintf(cm->stdOut, "%s Number of deleted clauses %d\n",
2321	cm->comment, stats->nDeletedCl);
2322	fprintf(cm->stdOut, "%s Number of deleted literals %d\n",
2323	cm->comment, stats->nDeletedLit);
2324
2325	if(option->incTraceObjective + option->incDistill) {
2326	fprintf(cm->stdOut, "%s Number of init object conflict clauses %d\n",
2327	cm->comment, stats->nInitObjConflictCl);
2328	fprintf(cm->stdOut, "%s Number of init object conflict literals %d\n",
2329	cm->comment, stats->nInitObjConflictLit);
2330	fprintf(cm->stdOut, "%s Number of init non-object conflict clauses %d\n",
2331	cm->comment, stats->nInitNonobjConflictCl);
2332	fprintf(cm->stdOut, "%s Number of init non-object conflict literals %d\n",
2333	cm->comment, stats->nInitNonobjConflictLit);
2334	fprintf(cm->stdOut, "%s Number of object conflict clauses %d\n",
2335	cm->comment, stats->nObjConflictCl);
2336	fprintf(cm->stdOut, "%s Number of object conflict literals %d\n",
2337	cm->comment, stats->nObjConflictLit);
2338	fprintf(cm->stdOut, "%s Number of non-object conflict clauses %d\n",
2339	cm->comment, stats->nNonobjConflictCl);
2340	fprintf(cm->stdOut, "%s Number of non-object conflict literals %d\n",
2341	cm->comment, stats->nNonobjConflictLit);
2342	}
2343	if(option->incDistill) {
2344	fprintf(cm->stdOut, "%s Number of distill object conflict clauses %d\n",
2345	cm->comment, stats->nDistillObjConflictCl);
2346	fprintf(cm->stdOut, "%s Number of distill object conflict literals %d\n",
2347	cm->comment, stats->nDistillObjConflictLit);
2348	fprintf(cm->stdOut, "%s Number of distill non-object conflict clauses %d\n",
2349	cm->comment, stats->nDistillNonobjConflictCl);
2350	fprintf(cm->stdOut, "%s Number of distill non-object conflict literals %d\n",
2351	cm->comment, stats->nDistillNonobjConflictLit);
2352	}
2353	if(option->allSatMode) {
2354	fprintf(cm->stdOut, "%s Number of blocking clauses %d\n",
2355	cm->comment, stats->nBlockingCl);
2356	fprintf(cm->stdOut, "%s Number of blocking literals %d\n",
2357	cm->comment, stats->nBlockingLit);
2358	}
2359
2360	fprintf(cm->stdOut, "%s Maximum decision level %d\n",
2361	cm->comment, stats->maxDecisionLevel);
2362	fprintf(cm->stdOut, "%s Number of low score decisions %d\n",
2363	cm->comment, stats->nLowScoreDecisions);
2364	fprintf(cm->stdOut, "%s Total nonchronological backtracks %d\n",
2365	cm->comment, stats->nNonchonologicalBacktracks);
2366	fprintf(cm->stdOut, "%s Total run time %10g\n", cm->comment, stats->satTime);
2367	fflush(cm->stdOut);
2368
2369	}
2370
2371	/Function******************************************************************
2372
2373	Synopsis [ Allocate statistics]
2374
2375	Description [ Allocate statistics]
2376
2377	SideEffects []
2378
2379	SeeAlso []
2380
2381	******************************************************************************/
2382	satStatistics_t *
2383	sat_InitStatistics(void)
2384	{
2385	satStatistics_t *stats;
2386
2387	stats = ALLOC(satStatistics_t, 1);
2388	memset(stats, 0, sizeof(satStatistics_t));
2389
2390	return(stats);
2391	}
2392
2393
2394	/Function******************************************************************
2395
2396	Synopsis [ Set incremental option ]
2397
2398	Description [ Set incremental option ]
2399
2400	SideEffects []
2401
2402	SeeAlso []
2403
2404	******************************************************************************/
2405	void
2406	sat_SetIncrementalOption(satOption_t *option, int incFlag)
2407	{
2408	if(incFlag == 0) return;
2409
2410	if(incFlag == 1) { /* TraceObjective */
2411	option->incTraceObjective = 1;
2412	}
2413	else if(incFlag == 2) { /* Distill */
2414	option->incDistill = 1;
2415	}
2416	else if(incFlag == 3) { /* TraceObjective & Distill */
2417	option->incTraceObjective = 1;
2418	option->incDistill = 1;
2419	}
2420
2421	}
2422
2423	/Function******************************************************************
2424
2425	Synopsis [ Restore blocking clauses]
2426
2427	Description [ Restore blocking clauses]
2428
2429	SideEffects []
2430
2431	SeeAlso []
2432
2433	******************************************************************************/
2434	void
2435	sat_RestoreBlockingClauses(satManager_t *cm)
2436	{
2437	long space, start;
2438	long c, v;
2439	int i;
2440	satArray_t *reached;
2441	satArray_t *clause;
2442	satArray_t *unitLits;
2443
2444	reached = cm->reached;
2445	if(reached == 0)
2446	return;
2447
2448	unitLits = cm->unitLits;
2449	if(unitLits == 0)
2450	unitLits = cm->unitLits = sat_ArrayAlloc(16);
2451
2452	clause = sat_ArrayAlloc(50);
2453
2454	for(i=0, space=reached->space; i<reached->num; i++, space++){
2455	if(*space <= 0) {
2456	space++;
2457	i++;
2458	if(i>=reached->num)
2459	break;
2460	start = space;
2461	clause->num = 0;
2462	while(*space > 0) {
2463	v = (*space);
2464	sat_ArrayInsert(clause, SATnot(v));
2465	i++;
2466	space++;
2467	}
2468
2469	c = sat_AddBlockingClause(cm, clause);
2470
2471	/**
2472	fprintf(stdout, "NOTICE : forwarded blocking clause\n");
2473	sat_PrintNode(cm, c);
2474	**/
2475
2476	if(clause->num == 1)
2477	sat_ArrayInsert(unitLits, (v));
2478	i--;
2479	space--;
2480	}
2481	}
2482	sat_ArrayFree(clause);
2483	}
2484
2485	/Function******************************************************************
2486
2487	Synopsis [ Restore Frontier clauses]
2488
2489	Description [ Restore Frontier clauses]
2490
2491	SideEffects []
2492
2493	SeeAlso []
2494
2495	******************************************************************************/
2496	void
2497	sat_RestoreFrontierClauses(satManager_t *cm)
2498	{
2499	long space, start;
2500	long c, v;
2501	int i;
2502	satArray_t *frontier;
2503	satArray_t *clause;
2504	satArray_t *unitLits;
2505
2506	frontier = cm->frontier;
2507	cm->frontierNodesEnd = cm->nodesArraySize;
2508	if(frontier == 0)
2509	return;
2510
2511	unitLits = cm->unitLits;
2512	if(unitLits == 0)
2513	unitLits = cm->unitLits = sat_ArrayAlloc(16);
2514
2515	clause = sat_ArrayAlloc(50);
2516
2517	for(i=0, space=frontier->space; i<frontier->num; i++, space++){
2518	if(*space <= 0) {
2519	space++;
2520	i++;
2521	if(i>=frontier->num)
2522	break;
2523	start = space;
2524	clause->num = 0;
2525	while(*space > 0) {
2526	v = (*space);
2527	sat_ArrayInsert(clause, SATnot(v));
2528	i++;
2529	space++;
2530	}
2531
2532	c = sat_AddClause(cm, clause);
2533
2534	/**
2535	sat_PrintNode(cm, c);
2536	**/
2537
2538	cm->initNumClauses++;
2539	cm->initNumLiterals += clause->num;
2540	if(clause->num == 1)
2541	sat_ArrayInsert(unitLits, (v));
2542
2543	i--;
2544	space--;
2545	}
2546	}
2547	sat_ArrayFree(clause);
2548	cm->frontierNodesEnd = cm->nodesArraySize;
2549	}
2550
2551	/Function******************************************************************
2552
2553	Synopsis [ Restore clauses]
2554
2555	Description [ Restore clauses]
2556
2557	SideEffects []
2558
2559	SeeAlso []
2560
2561	******************************************************************************/
2562	void
2563	sat_RestoreClauses(satManager_t cm, satArray_t cnfArray)
2564	{
2565	long space, start;
2566	long c, v;
2567	int i;
2568	satArray_t *clause;
2569	satArray_t *unitLits;
2570
2571
2572	unitLits = cm->unitLits;
2573	if(unitLits == 0)
2574	unitLits = cm->unitLits = sat_ArrayAlloc(16);
2575
2576	clause = sat_ArrayAlloc(50);
2577
2578	for(i=0, space=cnfArray->space; i<cnfArray->num; i++, space++){
2579	if(*space <= 0) {
2580	space++;
2581	i++;
2582	if(i>=cnfArray->num)
2583	break;
2584	start = space;
2585	clause->num = 0;
2586	while(*space > 0) {
2587	v = (*space);
2588	sat_ArrayInsert(clause, SATnot(v));
2589	i++;
2590	space++;
2591	}
2592
2593	if(clause->num == 1) {
2594	sat_ArrayInsert(unitLits, (v));
2595	}
2596	else {
2597	c = sat_AddClause(cm, clause);
2598	}
2599
2600	cm->initNumClauses++;
2601	cm->initNumLiterals += clause->num;
2602
2603	i--;
2604	space--;
2605	}
2606	}
2607	sat_ArrayFree(clause);
2608	}
2609
2610	/Function******************************************************************
2611
2612	Synopsis [ Collect blocking clauses]
2613
2614	Description [ Collect blocking clauses]
2615
2616	SideEffects []
2617
2618	SeeAlso []
2619
2620	******************************************************************************/
2621	void
2622	sat_CollectBlockingClause(satManager_t *cm)
2623	{
2624	satArray_t reached, frontier;
2625	long i, v, tv, *plit;
2626	int j, size;
2627	int inverted, num;
2628	int nReachs, nFrontiers;
2629
2630	if(cm->reached == 0) cm->reached = sat_ArrayAlloc(1024);
2631	if(cm->frontier == 0) cm->frontier = sat_ArrayAlloc(1024);
2632
2633	frontier = cm->frontier;
2634	reached = cm->reached;
2635
2636	frontier->num = 0;
2637	reached->num = 0;
2638	sat_ArrayInsert(frontier, 0);
2639	sat_ArrayInsert(reached, 0);
2640	nReachs = nFrontiers = 0;
2641
2642	for(i=cm->beginConflict; i<cm->nodesArraySize; i+=satNodeSize) {
2643	if(!(SATflags(i) & IsBlockingMask))
2644	continue;
2645
2646	if(SATreadInUse(i) == 0) continue;
2647
2648	if((SATflags(i) & IsFrontierMask)) {
2649
2650	/**
2651	fprintf(stdout, "Frontier processed\n");
2652	sat_PrintNode(cm, i);
2653	**/
2654	plit = (long*)SATfirstLit(i);
2655	size = SATnumLits(i);
2656	num = frontier->num;
2657	for(j=0; j<size; j++, plit++) {
2658	v = SATgetNode(*plit);
2659	inverted = SATisInverted(v);
2660	tv = SATnormalNode(v);
2661	sat_ArrayInsert(frontier, v);
2662	}
2663	nFrontiers++;
2664	sat_ArrayInsert(frontier, 0);
2665	}
2666
2667	plit = (long*)SATfirstLit(i);
2668	size = SATnumLits(i);
2669	for(j=0; j<size; j++, plit++) {
2670	v = SATgetNode(*plit);
2671	sat_ArrayInsert(reached, v);
2672	}
2673	sat_ArrayInsert(reached, 0);
2674	nReachs ++;
2675	}
2676
2677
2678
2679	cm->frontier = frontier;
2680	cm->reached = reached;
2681	fprintf(stdout, "NOTICE : %d frontier are collected\n", nFrontiers);
2682	fprintf(stdout, "NOTICE : %d blocking clauses are collected\n", nReachs);
2683	}
2684
2685
2686	/Function******************************************************************
2687
2688	Synopsis [ Free interface]
2689
2690	Description [ Free interface]
2691
2692	SideEffects []
2693
2694	SeeAlso []
2695
2696	******************************************************************************/
2697	void
2698	sat_FreeInterface(satInterface_t *interface)
2699	{
2700	if(interface == 0) return;
2701
2702	if(interface->total)
2703	free(interface->total);
2704	if(interface->nonobjUnitLitArray)
2705	sat_ArrayFree(interface->nonobjUnitLitArray);
2706	if(interface->objUnitLitArray)
2707	sat_ArrayFree(interface->objUnitLitArray);
2708	if(interface->savedConflictClauses)
2709	free(interface->savedConflictClauses);
2710	free(interface);
2711	}
2712
2713	/Function******************************************************************
2714
2715	Synopsis [ Create AIG node ]
2716
2717	Description [ Create AIG node,
2718	This function is identical with bAig_CreateNode,
2719	We have this function here to isolate this package from baig]
2720
2721	SideEffects []
2722
2723	SeeAlso []
2724
2725	******************************************************************************/
2726	long
2727	sat_CreateNode(
2728	satManager_t *cm,
2729	long left,
2730	long right)
2731	{
2732	long newNode;
2733
2734	newNode = cm->nodesArraySize;
2735	//Bing: to deal with the case that cm->maxNodesArraySize is not multiple of
2736	// satNodeSize
2737	cm->nodesArraySize += satNodeSize;
2738
2739	if(cm->nodesArraySize >= cm->maxNodesArraySize) {
2740	cm->maxNodesArraySize = 2* cm->maxNodesArraySize;
2741	cm->nodesArray = REALLOC(long, cm->nodesArray, cm->maxNodesArraySize);
2742	}
2743	cm->nodesArray[newNode + satRight] = right;
2744	cm->nodesArray[newNode + satLeft] = left;
2745
2746	//cm->nodesArraySize += satNodeSize;
2747
2748	SATflags(newNode) = 0;
2749	SATnext(newNode) = 2;
2750	SATnFanout(newNode) = 0;
2751	/**
2752	SATfanout(newNode) = 0;
2753	**/
2754	(cm->nodesArray[newNode+satFanout]) = 0;
2755	//Bing:
2756	SATvalue(newNode) = 2;
2757
2758	return(newNode);
2759	}
2760
2761	/Function******************************************************************
2762
2763	Synopsis [ Usage of memory ]
2764
2765	Description [ Usage of memory ]
2766
2767	SideEffects []
2768
2769	SeeAlso []
2770
2771	******************************************************************************/
2772	int
2773	sat_MemUsage(satManager_t *cm)
2774	{
2775	satLiteralDB_t *literals;
2776	satStatistics_t *stats;
2777	int aigSize, cnfSize, watchedSize;
2778
2779	literals = cm->literals;
2780	stats = cm->each;
2781	aigSize = sizeof(int) * cm->maxNodesArraySize;
2782	cnfSize = sizeof(int) * (literals->end - literals->begin);
2783	watchedSize = sizeof(int) * 2 *
2784	(stats->nConflictCl - stats->nDeletedCl);
2785	return(aigSize + cnfSize + watchedSize);
2786	}
2787
2788
2789
2790	/Function******************************************************************
2791
2792	Synopsis [ Get canonical node ]
2793
2794	Description [ Get canonical node ]
2795
2796	SideEffects []
2797
2798	SeeAlso []
2799
2800	******************************************************************************/
2801	long
2802	sat_GetCanonical(satManager_t *cm, long v)
2803	{
2804	long nv;
2805	int inverted;
2806
2807	if(v == 2) return(2);
2808
2809	while(!(SATflags(SATnormalNode(v))) & CanonicalBitMask) {
2810	inverted = SATisInverted(v);
2811	v = SATnormalNode(v);
2812	nv = SATcanonical(v);
2813	if(inverted)
2814	nv = SATnot(nv);
2815	v = nv;
2816	}
2817	return(v);
2818	}
2819
2820
2821	/Function******************************************************************
2822
2823	Synopsis [ Combine statistics of several runs]
2824
2825	Description [ Combine statistics of several runs]
2826
2827	SideEffects []
2828
2829	SeeAlso []
2830
2831	******************************************************************************/
2832	void
2833	sat_CombineStatistics(satManager_t *cm)
2834	{
2835	/* CONSIDER ... */
2836	}
2837
2838	/Function******************************************************************
2839
2840	Synopsis [ Get the number of initial clauses ]
2841
2842	Description [ Get the number of initial clauses.
2843	This function works properly only CNF sat case]
2844
2845	SideEffects []
2846
2847	SeeAlso []
2848
2849	******************************************************************************/
2850	int
2851	sat_GetNumberOfInitialClauses(satManager_t *cm)
2852	{
2853	return(cm->initNumClauses);
2854	}
2855
2856	/Function******************************************************************
2857
2858	Synopsis [ Get the number of initial variables ]
2859
2860	Description [ Get the number of initial variables.
2861	This function works properly only CNF sat case]
2862
2863	SideEffects []
2864
2865	SeeAlso []
2866
2867	******************************************************************************/
2868	int
2869	sat_GetNumberOfInitialVariables(satManager_t *cm)
2870	{
2871	return(cm->initNumVariables);
2872	}
2873
2874	/Function******************************************************************
2875
2876	Synopsis [ Read forced assignments.]
2877
2878	Description [ Read forced assignments.]
2879
2880	SideEffects []
2881
2882	SeeAlso []
2883
2884	******************************************************************************/
2885	satArray_t *
2886	sat_ReadForcedAssignment(
2887	char *filename)
2888	{
2889	FILE *fin;
2890	char line[102400], word[1024];
2891	char *lp;
2892	satArray_t *arr;
2893	long v;
2894
2895	if(!(fin = fopen(filename, "r"))) {
2896	fprintf(stdout, "ERROR : Can't open file %s\n", filename);
2897	return(0);
2898	}
2899
2900	arr = sat_ArrayAlloc(64);
2901	while(fgets(line, 102400, fin)) {
2902	lp = sat_RemoveSpace(line);
2903	if(lp[0] == '\n') continue;
2904	while(1) {
2905	lp = sat_RemoveSpace(lp);
2906	lp = sat_CopyWord(lp, word);
2907	if(strlen(word)) {
2908	v = atoi(word);
2909	v *= satNodeSize;
2910	if(v < 0) v = SATnot(-v);
2911	sat_ArrayInsert(arr, v);
2912	}
2913	else {
2914	break;
2915	}
2916	}
2917	}
2918	fclose(fin);
2919
2920	return(arr);
2921	}
2922
2923	/Function******************************************************************
2924
2925	Synopsis [ Apply forced assignments.]
2926
2927	Description [ Apply forced assignments.]
2928
2929	SideEffects []
2930
2931	SeeAlso []
2932
2933	******************************************************************************/
2934	int
2935	sat_ApplyForcedAssigment(
2936	satManager_t *cm,
2937	satArray_t *arr,
2938	satLevel_t *d)
2939	{
2940	long v;
2941	int i, inverted, errorFlag;
2942
2943	errorFlag = 0;
2944	for(i=0; i<arr->num; i++) {
2945	v = arr->space[i];
2946	inverted = SATisInverted(v);
2947	v = SATnormalNode(v);
2948
2949	SATvalue(v) = !inverted;
2950	SATmakeImplied(v, d);
2951	sat_Enqueue(cm->queue, v);
2952	SATflags(v) \|= InQueueMask;
2953	sat_ImplicationMain(cm, d);
2954	if(d->conflict) {
2955	fprintf(cm->stdOut,
2956	"%s WARNING : conflict happens at level %d while applying forced assignments\n", cm->comment, d->level);
2957	errorFlag = 1;
2958	break;
2959	}
2960	}
2961	if(errorFlag)
2962	return(SAT_UNSAT);
2963	else
2964	return(0);
2965	}
2966
2967	/Function******************************************************************
2968
2969	Synopsis [ Apply forced assignments.]
2970
2971	Description [ Apply forced assignments.]
2972
2973	SideEffects []
2974
2975	SeeAlso []
2976
2977	******************************************************************************/
2978	void
2979	sat_ApplyForcedAssignmentMain(
2980	satManager_t *cm,
2981	satLevel_t *d)
2982	{
2983	satArray_t *forcedArr;
2984	int flag;
2985
2986	forcedArr = cm->option->forcedAssignArr;
2987	flag = 0;
2988	if(forcedArr) {
2989	flag = sat_ApplyForcedAssigment(cm, forcedArr, d);
2990	}
2991
2992	if(flag == SAT_UNSAT) {
2993	cm->status = SAT_UNSAT;
2994	return;
2995	}
2996	}
2997
2998	/Function******************************************************************
2999
3000	Synopsis [ Put assignments.]
3001
3002	Description [ Put assignments.]
3003
3004	SideEffects []
3005
3006	SeeAlso []
3007
3008	******************************************************************************/
3009	void
3010	sat_PutAssignmentValueMain(
3011	satManager_t *cm,
3012	satLevel_t *d,
3013	satArray_t *arr)
3014	{
3015	long v;
3016	int i;
3017	int inverted;
3018
3019	if(arr == 0) return;
3020
3021	if(cm->variableArray == 0) {
3022	cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
3023	memset(cm->variableArray, 0,
3024	sizeof(satVariable_t) * (cm->initNumVariables+1));
3025	}
3026
3027	for(i=0; i<arr->num; i++) {
3028	v = arr->space[i];
3029	inverted = SATisInverted(v);
3030	v = SATnormalNode(v);
3031
3032	SATvalue(v) = !inverted;
3033	}
3034	}
3035
3036	/Function******************************************************************
3037
3038	Synopsis [ Clause deletion heuristic based on usage of conflict clause ]
3039
3040	Description [ Clause deletion heuristic based on usage of conflict clause ]
3041
3042	SideEffects []
3043
3044	SeeAlso []
3045
3046	******************************************************************************/
3047	void
3048	sat_ClauseDeletionLatestActivity(satManager_t *cm)
3049	{
3050	satLiteralDB_t *literals;
3051	satOption_t *option;
3052	long nv, v, plit, clit;
3053	long usage, totalConflictCl;
3054	long index, lit;
3055
3056	int size, n0, n1x, deleteFlag;
3057	int unrelevance;
3058	int usedLimit;
3059	int inverted, i;
3060	int value;
3061	int nLatestCl;
3062	int nDeletedCl;
3063	double ratio;
3064
3065	/**
3066	LATEST_ACTIVITY_DELETION
3067	MAX_UNRELEVANCE_DELETION
3068	SIMPLE_LATEST_DELETION
3069	**/
3070
3071	option = cm->option;
3072	if(option->clauseDeletionHeuristic == 0) return;
3073
3074	totalConflictCl = (cm->nodesArraySize - cm->beginConflict)/satNodeSize;
3075	nDeletedCl = cm->each->nDeletedCl;
3076	nLatestCl = totalConflictCl/option->latestRate;
3077	literals = cm->literals;
3078	index = 0;
3079	for(clit = literals->last-1; clit > literals->begin; clit--){
3080	if(*clit == 0)
3081	continue;
3082	if(index >= totalConflictCl)
3083	break;
3084	v = -(*clit);
3085
3086	plit = (long*)SATfirstLit(v);
3087	clit = plit - 1;
3088	index++;
3089
3090	if(nLatestCl > 0) {
3091	nLatestCl--;
3092	unrelevance = option->latestUnrelevance;
3093	}
3094	else {
3095	unrelevance = option->obsoleteUnrelevance;
3096	}
3097
3098	if(!(SATflags(v) & IsConflictMask)) continue;
3099	if((SATflags(v) & IsFrontierMask)) continue;
3100
3101	if(option->incPreserveNonobjective && (SATflags(v) & NonobjMask))
3102	continue;
3103
3104	usage = SATconflictUsage(v);
3105	SATconflictUsage(v) = usage/2;
3106	size = SATnumLits(v);
3107	// if(size < option->minLitsLimit) continue;
3108	if(size < unrelevance)
3109	continue;
3110
3111	usedLimit = option->obsoleteUsage +
3112	(option->latestUsage-option->obsoleteUsage)*index/totalConflictCl;
3113	if(usage > usedLimit)
3114	continue;
3115
3116
3117	n0 = n1x = 0;
3118	deleteFlag = 0;
3119	for(i=0; i<size; i++, plit++) {
3120	lit = *plit;
3121	nv = SATgetNode(lit);
3122	inverted = SATisInverted(nv);
3123	nv = SATnormalNode(nv);
3124	value = SATvalue(nv) ^ inverted;
3125
3126	if(value == 0) n0++;
3127	else if(value == 1) {
3128	n1x++;
3129	if(SATlevel(nv) == 0) deleteFlag = 1;
3130	}
3131	else n1x++;
3132
3133	if(deleteFlag) {
3134	sat_DeleteClause(cm, v);
3135	sat_Enqueue(cm->unusedAigQueue, v);
3136	break;
3137	}
3138	if((size > option->maxLitsLimit) && (n1x > 1)) {
3139	sat_DeleteClause(cm, v);
3140	sat_Enqueue(cm->unusedAigQueue, v);
3141	break;
3142	}
3143	if(n1x > unrelevance) {
3144	sat_DeleteClause(cm, v);
3145	sat_Enqueue(cm->unusedAigQueue, v);
3146	break;
3147	}
3148	}
3149
3150	}
3151
3152	cm->each->nDeletedButUncompacted += cm->each->nDeletedCl - nDeletedCl;
3153	ratio = (double)cm->each->nDeletedButUncompacted/
3154	(double)(cm->each->nConflictCl-cm->each->nDeletedCl);
3155
3156	if(ratio> 0.2) {
3157	sat_CompactClauses(cm);
3158	cm->each->nDeletedButUncompacted = 0;
3159	}
3160
3161	}
3162
3163
3164	/Function******************************************************************
3165
3166	Synopsis [ Find a clause index from literal pointer.]
3167
3168	Description [ Find a clause index from literal pointer.]
3169
3170	SideEffects []
3171
3172	SeeAlso []
3173
3174	******************************************************************************/
3175	long
3176	sat_GetClauseFromLit(
3177	satManager_t *cm,
3178	long *lit)
3179	{
3180	while(*lit > 0) {
3181	lit++;
3182	}
3183	return(-(*lit));
3184	}
3185	/Function******************************************************************
3186
3187	Synopsis [ Compare node index to sort ]
3188
3189	Description [ Compare node index to sort ]
3190
3191	SideEffects []
3192
3193	SeeAlso []
3194
3195	******************************************************************************/
3196	static int
3197	NodeIndexCompare(const void x, const void y)
3198	{
3199	long n1, n2;
3200
3201	n1 = (long )x;
3202	n2 = (long )y;
3203	return(n1 > n2);
3204	}

Note: See TracBrowser for help on using the repository browser.

Context Navigation

source: vis_dev/vis-2.3/src/sat/satUtil.c @ 74

Download in other formats: