ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
sbdWin.c
Go to the documentation of this file.
1
20
21#include "sbdInt.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
29
33
52sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors,
53 int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var,
54 Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf )
55{
56 Gia_Obj_t * pObj;
57 int i, iLit = 1, iObj, Fan0, Fan1, Lit0m, Lit1m, Node, fCompl0, fCompl1, RetValue;
58 int TfoStart = Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo);
59 int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
60 int LastVar = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
61 //Vec_IntPrint( vWinObjs );
62 //Vec_IntPrint( vTfo );
63 //Vec_IntPrint( vRoots );
64 // create SAT solver
65 if ( pSat == NULL )
66 pSat = sat_solver_new();
67 else
68 sat_solver_restart( pSat );
69 sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + SBD_FVAR_MAX );
70 // create constant 0 clause
71 sat_solver_addclause( pSat, &iLit, &iLit + 1 );
72 // add clauses for all nodes
73 Vec_IntForEachEntryStart( vWinObjs, iObj, i, 1 )
74 {
75 pObj = Gia_ManObj( p, iObj );
76 if ( Gia_ObjIsCi(pObj) )
77 continue;
78 assert( Gia_ObjIsAnd(pObj) );
79 assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
80 Node = Vec_IntEntry( vObj2Var, iObj );
81 Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
82 Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) );
83 Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
84 Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
85 Fan0 = Vec_IntEntry( vObj2Var, Fan0 );
86 Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
87 fCompl0 = Gia_ObjFaninC0(pObj) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
88 fCompl1 = Gia_ObjFaninC1(pObj) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
89 if ( Gia_ObjIsXor(pObj) )
90 sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
91 else
92 sat_solver_add_and( pSat, Node, Fan0, Fan1, fCompl0, fCompl1, 0 );
93 }
94 // add second clauses for the TFO
95 Vec_IntForEachEntryStart( vWinObjs, iObj, i, TfoStart )
96 {
97 pObj = Gia_ManObj( p, iObj );
98 assert( Gia_ObjIsAnd(pObj) );
99 assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
100 Node = Vec_IntEntry( vObj2Var, iObj ) + Vec_IntSize(vTfo);
101 Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
102 Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) );
103 Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
104 Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
105 Fan0 = Vec_IntEntry( vObj2Var, Fan0 );
106 Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
107 Fan0 = Fan0 < TfoStart ? Fan0 : Fan0 + Vec_IntSize(vTfo);
108 Fan1 = Fan1 < TfoStart ? Fan1 : Fan1 + Vec_IntSize(vTfo);
109 if ( fQbf )
110 {
111 Fan0 = Fan0 == PivotVar ? LastVar : Fan0;
112 Fan1 = Fan1 == PivotVar ? LastVar : Fan1;
113 }
114 fCompl0 = Gia_ObjFaninC0(pObj) ^ (!fQbf && Fan0 == PivotVar) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
115 fCompl1 = Gia_ObjFaninC1(pObj) ^ (!fQbf && Fan1 == PivotVar) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
116 if ( Gia_ObjIsXor(pObj) )
117 sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
118 else
119 sat_solver_add_and( pSat, Node, Fan0, Fan1, fCompl0, fCompl1, 0 );
120 }
121 if ( Vec_IntSize(vRoots) > 0 )
122 {
123 // create XOR clauses for the roots
124 int nVars = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo);
125 Vec_Int_t * vFaninVars = Vec_IntAlloc( Vec_IntSize(vRoots) );
126 Vec_IntForEachEntry( vRoots, iObj, i )
127 {
128 assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
129 Node = Vec_IntEntry( vObj2Var, iObj );
130 Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) );
131 sat_solver_add_xor( pSat, Node, Node + Vec_IntSize(vTfo), nVars++, 0 );
132 }
133 // make OR clause for the last nRoots variables
134 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vFaninVars), Vec_IntLimit(vFaninVars) );
135 Vec_IntFree( vFaninVars );
136 if ( RetValue == 0 )
137 {
138 sat_solver_delete( pSat );
139 return NULL;
140 }
141 assert( sat_solver_nvars(pSat) == nVars + SBD_FVAR_MAX );
142 }
143 else if ( fQbf )
144 {
145 int n, pLits[2];
146 for ( n = 0; n < 2; n++ )
147 {
148 pLits[0] = Abc_Var2Lit( PivotVar, n );
149 pLits[1] = Abc_Var2Lit( LastVar, n );
150 RetValue = sat_solver_addclause( pSat, pLits, pLits + 2 );
151 assert( RetValue );
152 }
153 }
154 // finalize
155 RetValue = sat_solver_simplify( pSat );
156 if ( RetValue == 0 )
157 {
158 sat_solver_delete( pSat );
159 return NULL;
160 }
161 return pSat;
162}
163
178word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp )
179{
180 int nBTLimit = 0;
181 word uCube, uTruth = 0;
182 int status, i, iVar, nFinal, * pFinal, pLits[2], nIter = 0;
183 assert( FreeVar < sat_solver_nvars(pSat) );
184 assert( Vec_IntSize(vDivVars) == Vec_IntSize(vDivValues) );
185 pLits[0] = Abc_Var2Lit( PivotVar, 0 ); // F = 1
186 pLits[1] = Abc_Var2Lit( FreeVar, 0 ); // iNewLit
187 while ( 1 )
188 {
189 // find onset minterm
190 status = sat_solver_solve( pSat, pLits, pLits + 2, nBTLimit, 0, 0, 0 );
191 if ( status == l_Undef )
192 return SBD_SAT_UNDEC;
193 if ( status == l_False )
194 return uTruth;
195 assert( status == l_True );
196 // remember variable values
197 Vec_IntForEachEntry( vDivVars, iVar, i )
198 Vec_IntWriteEntry( vDivValues, i, 2*sat_solver_var_value(pSat, iVar) );
199 // collect divisor literals
200 Vec_IntClear( vTemp );
201 Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0
202 Vec_IntForEachEntry( vDivSet, iVar, i )
203 Vec_IntPush( vTemp, sat_solver_var_literal(pSat, iVar) );
204 // check against offset
205 status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
206 if ( status == l_Undef )
207 return SBD_SAT_UNDEC;
208 if ( status == l_True )
209 break;
210 assert( status == l_False );
211 // compute cube and add clause
212 nFinal = sat_solver_final( pSat, &pFinal );
213 uCube = ~(word)0;
214 Vec_IntClear( vTemp );
215 Vec_IntPush( vTemp, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
216 for ( i = 0; i < nFinal; i++ )
217 {
218 if ( pFinal[i] == pLits[0] )
219 continue;
220 Vec_IntPush( vTemp, pFinal[i] );
221 iVar = Vec_IntFind( vDivSet, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
222 uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
223 }
224 uTruth |= uCube;
225 status = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp) );
226 assert( status );
227 nIter++;
228 }
229 assert( status == l_True );
230 // store the counter-example
231 Vec_IntForEachEntry( vDivVars, iVar, i )
232 Vec_IntAddToEntry( vDivValues, i, sat_solver_var_value(pSat, iVar) );
233
234 for ( i = 0; i < Vec_IntSize(vDivValues); i++ )
235 Vec_IntAddToEntry( vDivValues, i, 0xC );
236/*
237 // reduce the counter example
238 for ( n = 0; n < 2; n++ )
239 {
240 Vec_IntClear( vTemp );
241 Vec_IntPush( vTemp, Abc_Var2Lit(PivotVar, n) ); // n = 0 => F = 1 (expanding offset against onset)
242 for ( i = 0; i < Vec_IntSize(vValues); i++ )
243 Vec_IntPush( vTemp, Abc_Var2Lit(i, !((Vec_IntEntry(vValues, i) >> n) & 1)) );
244 status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
245 assert( status == l_False );
246 // compute cube and add clause
247 nFinal = sat_solver_final( pSat, &pFinal );
248 for ( i = 0; i < nFinal; i++ )
249 if ( Abc_Lit2Var(pFinal[i]) != PivotVar )
250 Vec_IntAddToEntry( vValues, Abc_Lit2Var(pFinal[i]), 1 << (n+2) );
251 }
252*/
253 return SBD_SAT_SAT;
254}
255
267int Sbd_ManSolve2( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp, Vec_Int_t * vSop )
268{
269 int nBTLimit = 0;
270 int status, i, iVar, nFinal, * pFinal, pLits[2], nIter = 0;
271 assert( FreeVar < sat_solver_nvars(pSat) );
272 assert( Vec_IntSize(vDivVars) == Vec_IntSize(vDivValues) );
273 pLits[0] = Abc_Var2Lit( PivotVar, 0 ); // F = 1
274 pLits[1] = Abc_Var2Lit( FreeVar, 0 ); // iNewLit
275 Vec_IntClear( vSop );
276 while ( 1 )
277 {
278 // find onset minterm
279 status = sat_solver_solve( pSat, pLits, pLits + 2, nBTLimit, 0, 0, 0 );
280 if ( status == l_Undef )
281 return 0;
282 if ( status == l_False )
283 return 1;
284 assert( status == l_True );
285 // remember variable values
286 //for ( i = 0; i < Vec_IntSize(vValues); i++ )
287 // Vec_IntWriteEntry( vValues, i, 2*sat_solver_var_value(pSat, i) );
288 // collect divisor literals
289 Vec_IntClear( vTemp );
290 Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0
291 //Vec_IntForEachEntry( vDivSet, iVar, i )
292 Vec_IntForEachEntry( vDivVars, iVar, i )
293 Vec_IntPush( vTemp, sat_solver_var_literal(pSat, iVar) );
294 // check against offset
295 status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
296 if ( status == l_Undef )
297 return 0;
298 if ( status == l_True )
299 break;
300 assert( status == l_False );
301 // compute cube and add clause
302 nFinal = sat_solver_final( pSat, &pFinal );
303 Vec_IntClear( vTemp );
304 Vec_IntPush( vTemp, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
305 for ( i = 0; i < nFinal; i++ )
306 {
307 if ( pFinal[i] == pLits[0] )
308 continue;
309 Vec_IntPush( vTemp, pFinal[i] );
310 iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
311 //uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
312 Vec_IntPush( vSop, Abc_Var2Lit( iVar, !Abc_LitIsCompl(pFinal[i]) ) );
313 }
314 //uTruth |= uCube;
315 Vec_IntPush( vSop, -1 );
316 status = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp) );
317 assert( status );
318 nIter++;
319 }
320 assert( status == l_True );
321 // store the counter-example
322 //for ( i = 0; i < Vec_IntSize(vValues); i++ )
323 // Vec_IntAddToEntry( vValues, i, sat_solver_var_value(pSat, i) );
324 return 0;
325}
326
327word Sbd_ManSolverSupp( Vec_Int_t * vSop, int * pInds, int * pnVars )
328{
329 word Supp = 0;
330 int i, Entry, nVars = 0;
331 Vec_IntForEachEntry( vSop, Entry, i )
332 {
333 if ( Entry == -1 )
334 continue;
335 assert( Abc_Lit2Var(Entry) < 64 );
336 if ( (Supp >> Abc_Lit2Var(Entry)) & 1 )
337 continue;
338 pInds[Abc_Lit2Var(Entry)] = nVars++;
339 Supp |= (word)1 << Abc_Lit2Var(Entry);
340 }
341 *pnVars = nVars;
342 return Supp;
343}
344void Sbd_ManSolverPrint( Vec_Int_t * vSop )
345{
346 int v, i, Entry, nVars, pInds[64];
347 word Supp = Sbd_ManSolverSupp( vSop, pInds, &nVars );
348 char Cube[65] = {'\0'};
349 assert( Cube[nVars] == '\0' );
350 for ( v = 0; v < nVars; v++ )
351 Cube[v] = '-';
352 Vec_IntForEachEntry( vSop, Entry, i )
353 {
354 if ( Entry == -1 )
355 {
356 printf( "%s\n", Cube );
357 for ( v = 0; v < nVars; v++ )
358 Cube[v] = '-';
359 continue;
360 }
361 Cube[pInds[Abc_Lit2Var(Entry)]] = '1' - (char)Abc_LitIsCompl(Entry);
362 }
363 Supp = 0;
364}
365void Sbd_ManSolveSelect( Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots )
366{
367 Vec_Int_t * vSop = Vec_IntAlloc( 100 );
368 Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
369 sat_solver * pSat = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoots, 0 );
370 int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
371 int FreeVar = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
372 int Status = Sbd_ManSolve2( pSat, PivotVar, FreeVar, vDivVars, vDivValues, vTemp, vSop );
373 printf( "Pivot = %4d. Divs = %4d. ", Pivot, Vec_IntSize(vDivVars) );
374 if ( Status == 0 )
375 printf( "UNSAT.\n" );
376 else
377 {
378 int nVars, pInds[64];
379 word Supp = Sbd_ManSolverSupp( vSop, pInds, &nVars );
380 //Sbd_ManSolverPrint( vSop );
381 printf( "SAT with %d vars and %d cubes.\n", nVars, Vec_IntCountEntry(vSop, -1) );
382 Supp = 0;
383 }
384 Vec_IntFree( vTemp );
385 Vec_IntFree( vSop );
386 sat_solver_delete( pSat );
387}
388
389
401static void sat_solver_random_polarity(sat_solver* s)
402{
403 int i, k;
404 for ( i = 0; i < s->size; i += 64 )
405 {
406 word Polar = Gia_ManRandomW(0);
407 for ( k = 0; k < 64 && (i << 6) + k < s->size; k++ )
408 s->polarity[(i << 6) + k] = Abc_TtGetBit(&Polar, k);
409 }
410}
411int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds )
412{
413 int nBTLimit = 0;
414 int i, Ind;
415 assert( Vec_IntSize(vInds) == nCareMints[0] + nCareMints[1] );
416 Vec_IntForEachEntry( vInds, Ind, i )
417 {
418 int fOffSet = (int)(i < nCareMints[0]);
419 int status, k, iLit = Abc_Var2Lit( PivotVar, fOffSet );
420 sat_solver_random_polarity( pSat );
421 status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
422 if ( status == l_Undef )
423 return -2;
424 if ( status == l_False )
425 return fOffSet;
426 for ( k = 0; k <= PivotVar; k++ )
427 if ( Abc_TtGetBit(pVarSims[k], Ind) != sat_solver_var_value(pSat, k) )
428 Abc_TtXorBit(pVarSims[k], Ind);
429 }
430 return -1;
431}
432
433int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset )
434{
435 int nBTLimit = 0;
436 int n, i, k, status, iLit, iVar;
437 word * pPats[2] = {pOnset, pOffset};
438 assert( Vec_IntSize(vDivVars) < 64 );
439 for ( n = 0; n < 2; n++ )
440 for ( i = 0; i < nConsts; i++ )
441 {
442 sat_solver_random_polarity( pSat );
443 iLit = Abc_Var2Lit( PivotVar, n );
444 status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
445 if ( status == l_Undef )
446 return -2;
447 if ( status == l_False )
448 return n;
449 pPats[n][i] = ((word)!n) << Vec_IntSize(vDivVars);
450 Vec_IntForEachEntry( vDivVars, iVar, k )
451 if ( sat_solver_var_value(pSat, iVar) )
452 Abc_TtXorBit(&pPats[n][i], k);
453 }
454 return -1;
455}
456
457
461
462
463ABC_NAMESPACE_IMPL_END
464
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
l_True
#define l_True
Definition bmcBmcS.c:35
l_Undef
#define l_Undef
Definition bmcBmcS.c:34
l_False
#define l_False
Definition bmcBmcS.c:36
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver_add_and
#define sat_solver_add_and
Definition cecSatG2.c:38
sat_solver_add_xor
#define sat_solver_add_xor
Definition cecSatG2.c:39
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
p
Cube * p
Definition exorList.c:222
Cube
struct cube Cube
Gia_ManRandomW
word Gia_ManRandomW(int fReset)
Definition giaUtil.c:67
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
sat_solver_simplify
int sat_solver_simplify(sat_solver *s)
Definition satSolver.c:1515
sat_solver_restart
void sat_solver_restart(sat_solver *s)
Definition satSolver.c:1389
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition satSolver.c:2369
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
SBD_FVAR_MAX
#define SBD_FVAR_MAX
Definition sbdInt.h:58
SBD_SAT_SAT
#define SBD_SAT_SAT
Definition sbdInt.h:53
SBD_SAT_UNDEC
#define SBD_SAT_UNDEC
INCLUDES ///.
Definition sbdInt.h:52
Sbd_ManSolve2
int Sbd_ManSolve2(sat_solver *pSat, int PivotVar, int FreeVar, Vec_Int_t *vDivVars, Vec_Int_t *vDivValues, Vec_Int_t *vTemp, Vec_Int_t *vSop)
Definition sbdWin.c:267
Sbd_ManSolverPrint
void Sbd_ManSolverPrint(Vec_Int_t *vSop)
Definition sbdWin.c:344
Sbd_ManSolve
word Sbd_ManSolve(sat_solver *pSat, int PivotVar, int FreeVar, Vec_Int_t *vDivSet, Vec_Int_t *vDivVars, Vec_Int_t *vDivValues, Vec_Int_t *vTemp)
Definition sbdWin.c:178
Sbd_ManSolveSelect
void Sbd_ManSolveSelect(Gia_Man_t *p, Vec_Int_t *vMirrors, int Pivot, Vec_Int_t *vDivVars, Vec_Int_t *vDivValues, Vec_Int_t *vWinObjs, Vec_Int_t *vObj2Var, Vec_Int_t *vTfo, Vec_Int_t *vRoots)
Definition sbdWin.c:365
Sbd_ManSolverSupp
word Sbd_ManSolverSupp(Vec_Int_t *vSop, int *pInds, int *pnVars)
Definition sbdWin.c:327
Sbd_ManCollectConstants
int Sbd_ManCollectConstants(sat_solver *pSat, int nCareMints[2], int PivotVar, word *pVarSims[], Vec_Int_t *vInds)
Definition sbdWin.c:411
Sbd_ManCollectConstantsNew
int Sbd_ManCollectConstantsNew(sat_solver *pSat, Vec_Int_t *vDivVars, int nConsts, int PivotVar, word *pOnset, word *pOffset)
Definition sbdWin.c:433
Sbd_ManSatSolver
ABC_NAMESPACE_IMPL_START sat_solver * Sbd_ManSatSolver(sat_solver *pSat, Gia_Man_t *p, Vec_Int_t *vMirrors, int Pivot, Vec_Int_t *vWinObjs, Vec_Int_t *vObj2Var, Vec_Int_t *vTfo, Vec_Int_t *vRoots, int fQbf)
DECLARATIONS ///.
Definition sbdWin.c:52
sat_solver_t::polarity
char * polarity
Definition satSolver.h:137
sat_solver_t::size
int size
Definition satSolver.h:102
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56