1 /**CFile****************************************************************
2
3 FileName [satUtil.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [C-language MiniSat solver.]
8
9 Synopsis [Additional SAT solver procedures.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: satUtil.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
18
19 ***********************************************************************/
20
21 #include <stdio.h>
22 #include <assert.h>
23 #include "satSolver.h"
24 #include "satSolver2.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
33 static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement );
34
35 ////////////////////////////////////////////////////////////////////////
36 /// FUNCTION DEFINITIONS ///
37 ////////////////////////////////////////////////////////////////////////
38
39 /**Function*************************************************************
40
41 Synopsis [Writes the given clause in a file in DIMACS format.]
42
43 Description []
44
45 SideEffects []
46
47 SeeAlso []
48
49 ***********************************************************************/
Sat_SolverClauseWriteDimacs(FILE * pFile,clause * pC,int fIncrement)50 void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement )
51 {
52 int i;
53 for ( i = 0; i < (int)pC->size; i++ )
54 fprintf( pFile, "%s%d ", (lit_sign(pC->lits[i])? "-": ""), lit_var(pC->lits[i]) + (fIncrement>0) );
55 if ( fIncrement )
56 fprintf( pFile, "0" );
57 fprintf( pFile, "\n" );
58 }
59
60 /**Function*************************************************************
61
62 Synopsis [Write the clauses in the solver into a file in DIMACS format.]
63
64 Description [This procedure by default does not print binary clauses. To enable
65 printing of binary clauses, please set fUseBinaryClauses to 0 in the body of
66 procedure sat_solver_clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
67 in file "satSolver.c".]
68
69 SideEffects []
70
71 SeeAlso []
72
73 ***********************************************************************/
Sat_SolverWriteDimacs(sat_solver * p,char * pFileName,lit * assumpBegin,lit * assumpEnd,int incrementVars)74 void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumpBegin, lit* assumpEnd, int incrementVars )
75 {
76 Sat_Mem_t * pMem = &p->Mem;
77 FILE * pFile;
78 clause * c;
79 int i, k, nUnits;
80
81 // count the number of unit clauses
82 nUnits = 0;
83 for ( i = 0; i < p->size; i++ )
84 if ( p->levels[i] == 0 && p->assigns[i] != 3 )
85 nUnits++;
86
87 // start the file
88 pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
89 if ( pFile == NULL )
90 {
91 printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
92 return;
93 }
94 // fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
95 fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)-1+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) );
96
97 // write the original clauses
98 Sat_MemForEachClause( pMem, c, i, k )
99 Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
100
101 // write the learned clauses
102 // Sat_MemForEachLearned( pMem, c, i, k )
103 // Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
104
105 // write zero-level assertions
106 for ( i = 0; i < p->size; i++ )
107 if ( p->levels[i] == 0 && p->assigns[i] != 3 ) // varX
108 fprintf( pFile, "%s%d%s\n",
109 (p->assigns[i] == 1)? "-": "", // var0
110 i + (int)(incrementVars>0),
111 (incrementVars) ? " 0" : "");
112
113 // write the assump
114 if (assumpBegin) {
115 for (; assumpBegin != assumpEnd; assumpBegin++) {
116 fprintf( pFile, "%s%d%s\n",
117 lit_sign(*assumpBegin)? "-": "",
118 lit_var(*assumpBegin) + (int)(incrementVars>0),
119 (incrementVars) ? " 0" : "");
120 }
121 }
122
123 fprintf( pFile, "\n" );
124 if ( pFileName ) fclose( pFile );
125 }
Sat_Solver2WriteDimacs(sat_solver2 * p,char * pFileName,lit * assumpBegin,lit * assumpEnd,int incrementVars)126 void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumpBegin, lit* assumpEnd, int incrementVars )
127 {
128 Sat_Mem_t * pMem = &p->Mem;
129 FILE * pFile;
130 clause * c;
131 int i, k, nUnits;
132
133 // count the number of unit clauses
134 nUnits = 0;
135 for ( i = 0; i < p->size; i++ )
136 if ( p->levels[i] == 0 && p->assigns[i] != 3 )
137 nUnits++;
138
139 // start the file
140 pFile = fopen( pFileName, "wb" );
141 if ( pFile == NULL )
142 {
143 printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
144 return;
145 }
146 // fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
147 fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)-1+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) );
148
149 // write the original clauses
150 Sat_MemForEachClause2( pMem, c, i, k )
151 Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
152
153 // write the learned clauses
154 // Sat_MemForEachLearned( pMem, c, i, k )
155 // Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
156
157 // write zero-level assertions
158 for ( i = 0; i < p->size; i++ )
159 if ( p->levels[i] == 0 && p->assigns[i] != 3 ) // varX
160 fprintf( pFile, "%s%d%s\n",
161 (p->assigns[i] == 1)? "-": "", // var0
162 i + (int)(incrementVars>0),
163 (incrementVars) ? " 0" : "");
164
165 // write the assump
166 if (assumpBegin) {
167 for (; assumpBegin != assumpEnd; assumpBegin++) {
168 fprintf( pFile, "%s%d%s\n",
169 lit_sign(*assumpBegin)? "-": "",
170 lit_var(*assumpBegin) + (int)(incrementVars>0),
171 (incrementVars) ? " 0" : "");
172 }
173 }
174
175 fprintf( pFile, "\n" );
176 fclose( pFile );
177 }
178
179
180 /**Function*************************************************************
181
182 Synopsis [Writes the given clause in a file in DIMACS format.]
183
184 Description []
185
186 SideEffects []
187
188 SeeAlso []
189
190 ***********************************************************************/
Sat_Wrd2Dbl(word w)191 static inline double Sat_Wrd2Dbl( word w ) { return (double)(unsigned)(w&0x3FFFFFFF) + (double)(1<<30)*(unsigned)(w>>30); }
192
Sat_SolverPrintStats(FILE * pFile,sat_solver * p)193 void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
194 {
195 printf( "starts : %16.0f\n", Sat_Wrd2Dbl(p->stats.starts) );
196 printf( "conflicts : %16.0f\n", Sat_Wrd2Dbl(p->stats.conflicts) );
197 printf( "decisions : %16.0f\n", Sat_Wrd2Dbl(p->stats.decisions) );
198 printf( "propagations : %16.0f\n", Sat_Wrd2Dbl(p->stats.propagations) );
199 // printf( "inspects : %10d\n", (int)p->stats.inspects );
200 // printf( "inspects2 : %10d\n", (int)p->stats.inspects2 );
201 }
202
203 /**Function*************************************************************
204
205 Synopsis [Writes the given clause in a file in DIMACS format.]
206
207 Description []
208
209 SideEffects []
210
211 SeeAlso []
212
213 ***********************************************************************/
Sat_Solver2PrintStats(FILE * pFile,sat_solver2 * s)214 void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * s )
215 {
216 printf( "starts : %10d\n", (int)s->stats.starts );
217 printf( "conflicts : %10d\n", (int)s->stats.conflicts );
218 printf( "decisions : %10d\n", (int)s->stats.decisions );
219 printf( "propagations : %10d\n", (int)s->stats.propagations );
220 // printf( "inspects : %10d\n", (int)s->stats.inspects );
221 // printf( "inspects2 : %10d\n", (int)s->stats.inspects2 );
222 /*
223 printf( "memory for variables %.1f MB (free %6.2f %%) and clauses %.1f MB (free %6.2f %%)\n",
224 1.0 * Sat_Solver2GetVarMem(s) * s->size / (1<<20),
225 100.0 * (s->cap - s->size) / s->cap,
226 4.0 * (s->clauses.cap + s->learnts.cap) / (1<<20),
227 100.0 * (s->clauses.cap - s->clauses.size +
228 s->learnts.cap - s->learnts.size) /
229 (s->clauses.cap + s->learnts.cap) );
230 */
231 }
232
233 /**Function*************************************************************
234
235 Synopsis [Returns the number of bytes used for each variable.]
236
237 Description []
238
239 SideEffects []
240
241 SeeAlso []
242
243 ***********************************************************************/
Sat_Solver2GetVarMem(sat_solver2 * s)244 int Sat_Solver2GetVarMem( sat_solver2 * s )
245 {
246 int Mem = 0;
247 Mem += (sizeof(s->activity[0]) == 4) ? sizeof(unsigned) : sizeof(double); // activity
248 Mem += 2 * sizeof(veci); // wlists
249 Mem += sizeof(int); // vi (variable info)
250 Mem += sizeof(int); // trail
251 Mem += sizeof(int); // orderpos
252 Mem += sizeof(int); // reasons
253 Mem += sizeof(int); // units
254 Mem += sizeof(int); // order
255 Mem += sizeof(int); // model
256 return Mem;
257 }
258
259 /**Function*************************************************************
260
261 Synopsis [Returns a counter-example.]
262
263 Description []
264
265 SideEffects []
266
267 SeeAlso []
268
269 ***********************************************************************/
Sat_SolverGetModel(sat_solver * p,int * pVars,int nVars)270 int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars )
271 {
272 int * pModel;
273 int i;
274 pModel = ABC_CALLOC( int, nVars+1 );
275 for ( i = 0; i < nVars; i++ )
276 pModel[i] = sat_solver_var_value(p, pVars[i]);
277 return pModel;
278 }
279
280 /**Function*************************************************************
281
282 Synopsis [Returns a counter-example.]
283
284 Description []
285
286 SideEffects []
287
288 SeeAlso []
289
290 ***********************************************************************/
Sat_Solver2GetModel(sat_solver2 * p,int * pVars,int nVars)291 int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars )
292 {
293 int * pModel;
294 int i;
295 pModel = ABC_CALLOC( int, nVars+1 );
296 for ( i = 0; i < nVars; i++ )
297 pModel[i] = sat_solver2_var_value(p, pVars[i]);
298 return pModel;
299 }
300
301 /**Function*************************************************************
302
303 Synopsis [Duplicates all clauses, complements unit clause of the given var.]
304
305 Description []
306
307 SideEffects []
308
309 SeeAlso []
310
311 ***********************************************************************/
Sat_SolverDoubleClauses(sat_solver * p,int iVar)312 void Sat_SolverDoubleClauses( sat_solver * p, int iVar )
313 {
314 assert( 0 );
315 /*
316 clause * pClause;
317 lit Lit, * pLits;
318 int RetValue, nClauses, nVarsOld, nLitsOld, nLits, c, v;
319 // get the number of variables
320 nVarsOld = p->size;
321 nLitsOld = 2 * p->size;
322 // extend the solver to depend on two sets of variables
323 sat_solver_setnvars( p, 2 * p->size );
324 // duplicate implications
325 for ( v = 0; v < nVarsOld; v++ )
326 if ( p->assigns[v] != l_Undef )
327 {
328 Lit = nLitsOld + toLitCond( v, p->assigns[v]==l_False );
329 if ( v == iVar )
330 Lit = lit_neg(Lit);
331 RetValue = sat_solver_addclause( p, &Lit, &Lit + 1 );
332 assert( RetValue );
333 }
334 // duplicate clauses
335 nClauses = vecp_size(&p->clauses);
336 for ( c = 0; c < nClauses; c++ )
337 {
338 pClause = (clause *)p->clauses.ptr[c];
339 nLits = clause_size(pClause);
340 pLits = clause_begin(pClause);
341 for ( v = 0; v < nLits; v++ )
342 pLits[v] += nLitsOld;
343 RetValue = sat_solver_addclause( p, pLits, pLits + nLits );
344 assert( RetValue );
345 for ( v = 0; v < nLits; v++ )
346 pLits[v] -= nLitsOld;
347 }
348 */
349 }
350
351
352 ////////////////////////////////////////////////////////////////////////
353 /// END OF FILE ///
354 ////////////////////////////////////////////////////////////////////////
355
356
357 ABC_NAMESPACE_IMPL_END
358
359