ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Macros | Functions
bmcClp.c File Reference
#include "bmc.h"
#include "misc/vec/vecWec.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
Include dependency graph for bmcClp.c:

Go to the source code of this file.

Macros

#define Bmc_SopForEachCube(pSop, nVars, pCube)
 

Functions

ABC_NAMESPACE_IMPL_START int Bmc_ComputeSimDiff (Gia_Man_t *p, Vec_Int_t *vPat, Vec_Int_t *vPat2)
 DECLARATIONS ///.
 
void Bmc_ComputeSimTest (Gia_Man_t *p)
 
int Bmc_CollapseIrredundant (Vec_Str_t *vSop, int nCubes, int nVars)
 
int Bmc_CollapseIrredundantFull (Vec_Str_t *vSop, int nCubes, int nVars)
 
int Bmc_CollapseExpandRound2 (sat_solver *pSat, Vec_Int_t *vLits, Vec_Int_t *vTemp, int nBTLimit, int fOnOffSetLit)
 
int Bmc_CollapseExpandRound (sat_solver *pSat, sat_solver *pSatOn, Vec_Int_t *vLits, Vec_Int_t *vNums, Vec_Int_t *vTemp, int nBTLimit, int fCanon, int fOnOffSetLit)
 
int Bmc_CollapseExpand (sat_solver *pSat, sat_solver *pSatOn, Vec_Int_t *vLits, Vec_Int_t *vNums, Vec_Int_t *vTemp, int nBTLimit, int fCanon, int fOnOffSetLit)
 
int Bmc_CollapseExpand2 (sat_solver *pSat, sat_solver *pSatOn, Vec_Int_t *vLits, Vec_Int_t *vNums, Vec_Int_t *vTemp, int nBTLimit, int fCanon, int fOnOffSetLit)
 
int Bmc_ComputeCanonical2 (sat_solver *pSat, Vec_Int_t *vLits, Vec_Int_t *vTemp, int nBTLimit)
 
int Bmc_ComputeCanonical (sat_solver *pSat, Vec_Int_t *vLits, Vec_Int_t *vTemp, int nBTLimit)
 
Vec_Str_t * Bmc_CollapseOneInt2 (Gia_Man_t *p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose, int fCompl)
 
Vec_Str_t * Bmc_CollapseOneOld2 (Gia_Man_t *p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose)
 
Vec_Str_t * Bmc_CollapseOneOld (Gia_Man_t *p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose)
 
Vec_Str_t * Bmc_CollapseOne_int3 (sat_solver *pSat0, sat_solver *pSat1, sat_solver *pSat2, sat_solver *pSat3, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose)
 
Vec_Str_t * Bmc_CollapseOne3 (Gia_Man_t *p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose)
 
Vec_Str_t * Bmc_CollapseOne_int2 (sat_solver *pSat1, sat_solver *pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose)
 
Vec_Str_t * Bmc_CollapseOne_int (sat_solver *pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose)
 
Vec_Str_t * Bmc_CollapseOne (Gia_Man_t *p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose)
 

Macro Definition Documentation

◆ Bmc_SopForEachCube

#define Bmc_SopForEachCube ( pSop,
nVars,
pCube )
Value:
for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 )

Definition at line 188 of file bmcClp.c.

Function Documentation

◆ Bmc_CollapseExpand()

int Bmc_CollapseExpand ( sat_solver * pSat,
sat_solver * pSatOn,
Vec_Int_t * vLits,
Vec_Int_t * vNums,
Vec_Int_t * vTemp,
int nBTLimit,
int fCanon,
int fOnOffSetLit )

Function*************************************************************

Synopsis [Expends minterm into a cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 460 of file bmcClp.c.

461{
462 // perform one quick reduction if it is non-canonical
463 if ( !fCanon )
464 {
465 int i, k, iLit, status, nFinal, * pFinal;
466 // check against offset
467 if ( fOnOffSetLit >= 0 )
468 Vec_IntPush( vLits, fOnOffSetLit );
469 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
470 if ( fOnOffSetLit >= 0 )
471 Vec_IntPop( vLits );
472 if ( status == l_Undef )
473 return -1;
474 assert( status == l_False );
475 // get subset of literals
476 nFinal = sat_solver_final( pSat, &pFinal );
477 // mark unused literals
478 Vec_IntForEachEntry( vLits, iLit, i )
479 {
480 for ( k = 0; k < nFinal; k++ )
481 if ( iLit == Abc_LitNot(pFinal[k]) )
482 break;
483 if ( k == nFinal )
484 Vec_IntWriteEntry( vLits, i, -1 );
485 }
486 if ( Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon, fOnOffSetLit ) == -1 )
487 return -1;
488 }
489 else
490 {
491 if ( Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ) == -1 )
492 return -1;
493 if ( Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ) == -1 )
494 return -1;
495 }
496 {
497 // put into new array
498 int i, iLit;
499 Vec_IntClear( vNums );
500 Vec_IntForEachEntry( vLits, iLit, i )
501 if ( iLit != -1 )
502 Vec_IntPush( vNums, i );
503 }
504 return 0;
505}
l_Undef
#define l_Undef
Definition bmcBmcS.c:34
l_False
#define l_False
Definition bmcBmcS.c:36
Bmc_CollapseExpandRound
int Bmc_CollapseExpandRound(sat_solver *pSat, sat_solver *pSatOn, Vec_Int_t *vLits, Vec_Int_t *vNums, Vec_Int_t *vTemp, int nBTLimit, int fCanon, int fOnOffSetLit)
Definition bmcClp.c:381
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CollapseExpand2()

int Bmc_CollapseExpand2 ( sat_solver * pSat,
sat_solver * pSatOn,
Vec_Int_t * vLits,
Vec_Int_t * vNums,
Vec_Int_t * vTemp,
int nBTLimit,
int fCanon,
int fOnOffSetLit )

Definition at line 507 of file bmcClp.c.

508{
509 // perform one quick reduction if it is non-canonical
510 if ( !fCanon )
511 {
512 int i, k, iLit, j, iNum, status, nFinal, * pFinal;
513
514 // check against offset
515 if ( fOnOffSetLit >= 0 )
516 Vec_IntPush( vLits, fOnOffSetLit );
517 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
518 if ( fOnOffSetLit >= 0 )
519 Vec_IntPop( vLits );
520 if ( status == l_Undef )
521 return -1;
522 assert( status == l_False );
523
524 // get subset of literals
525 nFinal = sat_solver_final( pSat, &pFinal );
526 Vec_IntClear( vNums );
527 Vec_IntClear( vTemp );
528 if ( fOnOffSetLit >= 0 )
529 {
530 //Vec_IntPush( vNums, -1 );
531 Vec_IntPush( vTemp, fOnOffSetLit );
532 }
533 Vec_IntForEachEntry( vLits, iLit, i )
534 {
535 for ( k = 0; k < nFinal; k++ )
536 if ( iLit == Abc_LitNot(pFinal[k]) )
537 break;
538 if ( k == nFinal )
539 continue;
540 Vec_IntPush( vNums, i );
541 Vec_IntPush( vTemp, iLit );
542 }
543
544 // check against offset
545 status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 );
546 if ( status == l_Undef )
547 return -1;
548 assert( status == l_False );
549
550 // get subset of literals
551 nFinal = sat_solver_final( pSat, &pFinal );
552 j = 0;
553 Vec_IntForEachEntry( vTemp, iLit, i )
554 {
555 if ( iLit == fOnOffSetLit )
556 continue;
557 for ( k = 0; k < nFinal; k++ )
558 if ( iLit == Abc_LitNot(pFinal[k]) )
559 break;
560 if ( k == nFinal )
561 continue;
562 Vec_IntWriteEntry( vNums, j++, Vec_IntEntry(vNums, i) );
563 }
564 Vec_IntShrink( vNums, j );
565
566
567 // try removing each literal
568 for ( i = 0; i < Vec_IntSize(vNums); i++ )
569 {
570 Vec_IntClear( vTemp );
571 if ( fOnOffSetLit >= 0 )
572 Vec_IntPush( vTemp, fOnOffSetLit );
573 Vec_IntForEachEntry( vNums, iNum, k )
574 if ( k != i )
575 Vec_IntPush( vTemp, Vec_IntEntry(vLits, iNum) );
576 // check against offset
577 status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 );
578 if ( status == l_Undef )
579 return -1;
580 if ( status == l_True )
581 continue;
582 // remove literal
583 Vec_IntDrop( vNums, i );
584 i--;
585 }
586 }
587 else
588 {
589 if ( Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ) == -1 )
590 return -1;
591 if ( Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ) == -1 )
592 return -1;
593 }
594/*
595 {
596 // put into new array
597 int i, iLit;
598 Vec_IntClear( vNums );
599 Vec_IntForEachEntry( vLits, iLit, i )
600 if ( iLit != -1 )
601 Vec_IntPush( vNums, i );
602 //printf( "%d(%d) ", Vec_IntSize(vNums), Vec_IntSize(vLits) );
603 }
604*/
605 return 0;
606}
l_True
#define l_True
Definition bmcBmcS.c:35
Here is the call graph for this function:

◆ Bmc_CollapseExpandRound()

int Bmc_CollapseExpandRound ( sat_solver * pSat,
sat_solver * pSatOn,
Vec_Int_t * vLits,
Vec_Int_t * vNums,
Vec_Int_t * vTemp,
int nBTLimit,
int fCanon,
int fOnOffSetLit )

Definition at line 381 of file bmcClp.c.

382{
383 int fProfile = 0;
384 int k, n, iLit, status;
385 abctime clk;
386 //return Bmc_CollapseExpandRound2( pSat, vLits, vTemp, nBTLimit, fOnOffSetLit );
387 // try removing one literal at a time
388 for ( k = Vec_IntSize(vLits) - 1; k >= 0; k-- )
389 {
390 int Save = Vec_IntEntry( vLits, k );
391 if ( Save == -1 )
392 continue;
393 // check if this literal when expanded overlaps with the on-set
394 if ( pSatOn )
395 {
396 assert( fOnOffSetLit == -1 );
397 // it is ok to skip the first round if the literal is positive
398 if ( fCanon && !Abc_LitIsCompl(Save) )
399 continue;
400 // put into new array
401 Vec_IntClear( vTemp );
402 Vec_IntForEachEntry( vLits, iLit, n )
403 if ( iLit != -1 )
404 Vec_IntPush( vTemp, Abc_LitNotCond(iLit, k==n) );
405 // check against onset
406 if ( fProfile ) clk = Abc_Clock();
407 status = sat_solver_solve( pSatOn, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 );
408 if ( fProfile ) clkCheck1 += Abc_Clock() - clk;
409 if ( status == l_Undef )
410 return -1;
411 //printf( "%d", status == l_True );
412 if ( status == l_False )
413 {
414 if ( fProfile ) clkCheckU += Abc_Clock() - clk;
415 continue;
416 }
417 if ( fProfile ) clkCheckS += Abc_Clock() - clk;
418 // otherwise keep trying to remove it
419 }
420 Vec_IntWriteEntry( vLits, k, -1 );
421 // put into new array
422 Vec_IntClear( vTemp );
423 if ( fOnOffSetLit >= 0 )
424 Vec_IntPush( vTemp, fOnOffSetLit );
425 Vec_IntForEachEntry( vLits, iLit, n )
426 if ( iLit != -1 )
427 Vec_IntPush( vTemp, iLit );
428 // check against offset
429 if ( fProfile ) clk = Abc_Clock();
430 status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 );
431 if ( fProfile ) clkCheck2 += Abc_Clock() - clk;
432// if ( fOnOffSetLit >= 0 )
433// Vec_IntPop( vTemp );
434 if ( status == l_Undef )
435 return -1;
436 if ( status == l_True )
437 {
438 Vec_IntWriteEntry( vLits, k, Save );
439 if ( fProfile ) clkCheckS += Abc_Clock() - clk;
440 }
441 else
442 if ( fProfile ) clkCheckU += Abc_Clock() - clk;
443 }
444// if ( pSatOn )
445// printf( "\n" );
446 return 0;
447}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Here is the caller graph for this function:

◆ Bmc_CollapseExpandRound2()

int Bmc_CollapseExpandRound2 ( sat_solver * pSat,
Vec_Int_t * vLits,
Vec_Int_t * vTemp,
int nBTLimit,
int fOnOffSetLit )

Function*************************************************************

Synopsis [Performs one round of removing literals.]

Description []

SideEffects []

SeeAlso []

Definition at line 356 of file bmcClp.c.

357{
358 // put into new array
359 int i, iLit, nLits;
360 Vec_IntClear( vTemp );
361 Vec_IntForEachEntry( vLits, iLit, i )
362 if ( iLit != -1 )
363 Vec_IntPush( vTemp, iLit );
364 assert( Vec_IntSize(vTemp) > 0 );
365 // assume condition literal
366 if ( fOnOffSetLit >= 0 )
367 sat_solver_push( pSat, fOnOffSetLit );
368 // minimize
369 nLits = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vTemp), Vec_IntSize(vTemp), nBTLimit );
370 Vec_IntShrink( vTemp, nLits );
371 // assume conditional literal
372 if ( fOnOffSetLit >= 0 )
373 sat_solver_pop( pSat );
374 // modify output literas
375 Vec_IntForEachEntry( vLits, iLit, i )
376 if ( iLit != -1 && Vec_IntFind(vTemp, iLit) == -1 )
377 Vec_IntWriteEntry( vLits, i, -1 );
378 return 0;
379}
sat_solver_push
int sat_solver_push(sat_solver *s, int p)
Definition satSolver.c:2002
sat_solver_pop
void sat_solver_pop(sat_solver *s)
Definition satSolver.c:2045
sat_solver_minimize_assumptions
int sat_solver_minimize_assumptions(sat_solver *s, int *pLits, int nLits, int nConfLimit)
Definition satSolver.c:2209
Here is the call graph for this function:

◆ Bmc_CollapseIrredundant()

int Bmc_CollapseIrredundant ( Vec_Str_t * vSop,
int nCubes,
int nVars )

Function*************************************************************

Synopsis [Perform approximate irredundant step on the cover.]

Description [Iterate through the cubes in the reverse order and check if each cube is contained in the previously seen cubes.]

SideEffects []

SeeAlso []

Definition at line 202 of file bmcClp.c.

203{
204 int nBTLimit = 0;
205 sat_solver * pSat;
206 int i, k, status, iLit, nRemoved = 0;
207 Vec_Int_t * vLits = Vec_IntAlloc(nVars);
208 // collect cubes
209 char * pCube, * pSop = Vec_StrArray(vSop);
210 Vec_Ptr_t * vCubes = Vec_PtrAlloc(nCubes);
211 assert( Vec_StrSize(vSop) == nCubes * (nVars + 3) + 1 );
212 Bmc_SopForEachCube( pSop, nVars, pCube )
213 Vec_PtrPush( vCubes, pCube );
214 // create SAT solver
215 pSat = sat_solver_new();
216 sat_solver_setnvars( pSat, nVars );
217 // iterate through cubes in the reverse order
218 Vec_PtrForEachEntryReverse( char *, vCubes, pCube, i )
219 {
220 // collect literals
221 Vec_IntClear( vLits );
222 for ( k = 0; k < nVars; k++ )
223 if ( pCube[k] != '-' )
224 Vec_IntPush( vLits, Abc_Var2Lit(k, pCube[k] == '1') );
225 // check if this cube intersects with the complement of other cubes in the solver
226 // if it does not intersect, then it is redundant and can be skipped
227 // if it does, then it should be added
228 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
229 if ( status == l_Undef ) // timeout
230 break;
231 if ( status == l_False ) // unsat
232 {
233 Vec_PtrWriteEntry( vCubes, i, NULL );
234 nRemoved++;
235 continue;
236 }
237 assert( status == l_True );
238 // make a clause out of the cube by complementing its literals
239 Vec_IntForEachEntry( vLits, iLit, k )
240 Vec_IntWriteEntry( vLits, k, Abc_LitNot(iLit) );
241 // add it to the solver
242 status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
243 assert( status == 1 );
244 }
245 //printf( "Approximate irrendundant reduced %d cubes (out of %d).\n", nRemoved, nCubes );
246 // cleanup cover
247 if ( i == -1 && nRemoved > 0 ) // finished without timeout and removed some cubes
248 {
249 int j = 0;
250 Vec_PtrForEachEntry( char *, vCubes, pCube, i )
251 if ( pCube != NULL )
252 for ( k = 0; k < nVars + 3; k++ )
253 Vec_StrWriteEntry( vSop, j++, pCube[k] );
254 Vec_StrWriteEntry( vSop, j++, '\0' );
255 Vec_StrShrink( vSop, j );
256 }
257 sat_solver_delete( pSat );
258 Vec_PtrFree( vCubes );
259 Vec_IntFree( vLits );
260 return i == -1 ? 1 : 0;
261}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Bmc_SopForEachCube
#define Bmc_SopForEachCube(pSop, nVars, pCube)
Definition bmcClp.c:188
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Vec_PtrForEachEntryReverse
#define Vec_PtrForEachEntryReverse(Type, vVec, pEntry, i)
Definition vecPtr.h:63
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CollapseIrredundantFull()

int Bmc_CollapseIrredundantFull ( Vec_Str_t * vSop,
int nCubes,
int nVars )

Function*************************************************************

Synopsis [Perform full irredundant step on the cover.]

Description [Iterate through the cubes in the direct order and check if each cube is contained in all other cubes.]

SideEffects []

SeeAlso []

Definition at line 275 of file bmcClp.c.

276{
277 int nBTLimit = 0;
278 sat_solver * pSat;
279 int i, k, status, nRemoved = 0;
280 Vec_Int_t * vLits = Vec_IntAlloc(nVars+nCubes);
281 // collect cubes
282 char * pCube, * pSop = Vec_StrArray(vSop);
283 Vec_Ptr_t * vCubes = Vec_PtrAlloc(nCubes);
284 assert( Vec_StrSize(vSop) == nCubes * (nVars + 3) + 1 );
285 Bmc_SopForEachCube( pSop, nVars, pCube )
286 Vec_PtrPush( vCubes, pCube );
287 // create SAT solver
288 pSat = sat_solver_new();
289 sat_solver_setnvars( pSat, nVars + nCubes );
290 // add cubes
291 Vec_PtrForEachEntry( char *, vCubes, pCube, i )
292 {
293 // collect literals
294 Vec_IntFill( vLits, 1, Abc_Var2Lit(nVars + i, 1) ); // neg literal
295 for ( k = 0; k < nVars; k++ )
296 if ( pCube[k] != '-' )
297 Vec_IntPush( vLits, Abc_Var2Lit(k, pCube[k] == '0') );
298 // add it to the solver
299 status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
300 assert( status == 1 );
301 }
302 // iterate through cubes in the direct order
303 Vec_PtrForEachEntry( char *, vCubes, pCube, i )
304 {
305 // collect literals
306 Vec_IntClear( vLits );
307 for ( k = 0; k < nCubes; k++ )
308 if ( k != i && Vec_PtrEntry(vCubes, k) ) // skip this cube and already removed cubes
309 Vec_IntPush( vLits, Abc_Var2Lit(nVars + k, 0) ); // pos literal
310 // collect cube
311 for ( k = 0; k < nVars; k++ )
312 if ( pCube[k] != '-' )
313 Vec_IntPush( vLits, Abc_Var2Lit(k, pCube[k] == '1') );
314 // check if this cube intersects with the complement of other cubes in the solver
315 // if it does not intersect, then it is redundant and can be skipped
316 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
317 if ( status == l_Undef ) // timeout
318 break;
319 if ( status == l_False ) // unsat
320 {
321 Vec_PtrWriteEntry( vCubes, i, NULL );
322 nRemoved++;
323 continue;
324 }
325 assert( status == l_True );
326 }
327 //printf( "Approximate irrendundant reduced %d cubes (out of %d).\n", nRemoved, nCubes );
328 // cleanup cover
329 if ( i == Vec_PtrSize(vCubes) && nRemoved > 0 ) // finished without timeout and removed some cubes
330 {
331 int j = 0;
332 Vec_PtrForEachEntry( char *, vCubes, pCube, i )
333 if ( pCube != NULL )
334 for ( k = 0; k < nVars + 3; k++ )
335 Vec_StrWriteEntry( vSop, j++, pCube[k] );
336 Vec_StrWriteEntry( vSop, j++, '\0' );
337 Vec_StrShrink( vSop, j );
338 }
339 sat_solver_delete( pSat );
340 Vec_PtrFree( vCubes );
341 Vec_IntFree( vLits );
342 return i == -1 ? 1 : 0;
343}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CollapseOne()

Vec_Str_t * Bmc_CollapseOne ( Gia_Man_t * p,
int nCubeLim,
int nBTLimit,
int fCanon,
int fReverse,
int fVerbose )

Definition at line 1532 of file bmcClp.c.

1533{
1534 Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
1535 sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
1536 Vec_Str_t * vSop = Bmc_CollapseOne_int( pSat, Gia_ManCiNum(p), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
1537 sat_solver_delete( pSat );
1538 Cnf_DataFree( pCnf );
1539 return vSop;
1540}
Vec_Str_t
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
Bmc_CollapseOne_int
Vec_Str_t * Bmc_CollapseOne_int(sat_solver *pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose)
Definition bmcClp.c:1389
Cnf_Dat_t
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition cnfMan.c:207
p
Cube * p
Definition exorList.c:222
Mf_ManGenerateCnf
void * Mf_ManGenerateCnf(Gia_Man_t *pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose)
Definition giaMf.c:1877
Cnf_DataWriteIntoSolver
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition cnfMan.c:579
Here is the call graph for this function:

◆ Bmc_CollapseOne3()

Vec_Str_t * Bmc_CollapseOne3 ( Gia_Man_t * p,
int nCubeLim,
int nBTLimit,
int fCanon,
int fReverse,
int fVerbose )

Definition at line 1198 of file bmcClp.c.

1199{
1200 Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
1201 sat_solver * pSat0 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
1202 sat_solver * pSat1 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
1203 sat_solver * pSat2 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
1204 sat_solver * pSat3 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
1205 Vec_Str_t * vSop = Bmc_CollapseOne_int3( pSat0, pSat1, pSat2, pSat3, Gia_ManCiNum(p), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
1206 sat_solver_delete( pSat0 );
1207 sat_solver_delete( pSat1 );
1208 sat_solver_delete( pSat2 );
1209 sat_solver_delete( pSat3 );
1210 Cnf_DataFree( pCnf );
1211 return vSop;
1212}
Bmc_CollapseOne_int3
Vec_Str_t * Bmc_CollapseOne_int3(sat_solver *pSat0, sat_solver *pSat1, sat_solver *pSat2, sat_solver *pSat3, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose)
Definition bmcClp.c:1040
Here is the call graph for this function:

◆ Bmc_CollapseOne_int()

Vec_Str_t * Bmc_CollapseOne_int ( sat_solver * pSat,
int nVars,
int nCubeLim,
int nBTLimit,
int fCanon,
int fReverse,
int fVerbose )

Function*************************************************************

Synopsis [This code computes on-set and off-set simultaneously.]

Description []

SideEffects []

SeeAlso []

Definition at line 1389 of file bmcClp.c.

1390{
1391 int fVeryVerbose = fVerbose;
1392 Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL;
1393 Vec_Int_t * vVars = Vec_IntAlloc( nVars+1 );
1394 Vec_Int_t * vLits = Vec_IntAlloc( nVars+1 );
1395 Vec_Int_t * vNums = Vec_IntAlloc( nVars+1 );
1396 Vec_Int_t * vCube = Vec_IntAlloc( nVars+1 );
1397 int n, v, iVar, pLits[2], iCube = 0, Start, status;
1398 abctime clk = 0, Time[2][2] = {{0}};
1399 int fComplete[2] = {0};
1400 // variables
1401 int iOutVar = 2;
1402 int iOOVars[2] = {0, 1};
1403// int iOutVar = 1;
1404// int iOOVars[2] = {sat_solver_nvars(pSat) - 5, sat_solver_nvars(pSat) - 5 + 1};
1405
1406 // collect CI variables (0 = onset enable, 1 = offset enable, 2 = output)
1407 int iCiVarBeg = 3;
1408// int iCiVarBeg = sat_solver_nvars(pSat) - 5 - nVars;
1409 if ( fReverse )
1410 for ( v = nVars - 1; v >= 0; v-- )
1411 Vec_IntPush( vVars, iCiVarBeg + v );
1412 else
1413 for ( v = 0; v < nVars; v++ )
1414 Vec_IntPush( vVars, iCiVarBeg + v );
1415
1416 // check that on-set/off-set is sat
1417 for ( n = 0; n < 2; n++ )
1418 {
1419 pLits[0] = Abc_Var2Lit( iOutVar, n ); // n=0 => F=1 n=1 => F=0
1420 status = sat_solver_solve( pSat, pLits, pLits + 1, nBTLimit, 0, 0, 0 );
1421 if ( status == l_Undef )
1422 goto cleanup; // timeout
1423 if ( status == l_False )
1424 {
1425 Vec_StrClear( vSop[0] );
1426 Vec_StrPrintStr( vSop[0], n ? " 1\n" : " 0\n" );
1427 Vec_StrPush( vSop[0], '\0' );
1428 fComplete[0] = 1;
1429 goto cleanup; // const0/1
1430 }
1431 // start cover
1432 Vec_StrPush( vSop[n], '\0' );
1433 }
1434
1435 // compute cube pairs
1436 for ( iCube = 0; nCubeLim == 0 || iCube < nCubeLim; iCube++ )
1437 {
1438 for ( n = 0; n < 2; n++ )
1439 {
1440 if ( fVeryVerbose ) clk = Abc_Clock();
1441 // get the assignment
1442 sat_solver_clean_polarity( pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) );
1443 pLits[0] = Abc_Var2Lit( iOutVar, n ); // set output
1444 pLits[1] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses
1445 status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
1446 if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk;
1447 if ( status == l_Undef )
1448 goto cleanup; // timeout
1449 if ( status == l_False )
1450 {
1451 fComplete[n] = 1;
1452 break;
1453 }
1454 // collect values
1455 Vec_IntClear( vLits );
1456 Vec_IntForEachEntry( vVars, iVar, v )
1457 Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat, iVar)) );
1458 // expand the values
1459 if ( fVeryVerbose ) clk = Abc_Clock();
1460 status = Bmc_CollapseExpand( pSat, NULL, vLits, vNums, vCube, nBTLimit, fCanon, Abc_Var2Lit(iOutVar, !n) );
1461 if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk;
1462 if ( status < 0 )
1463 goto cleanup; // timeout
1464 // collect cube
1465 Vec_StrPop( vSop[n] );
1466 Start = Vec_StrSize( vSop[n] );
1467 Vec_StrFillExtra( vSop[n], Start + nVars + 4, '-' );
1468 Vec_StrWriteEntry( vSop[n], Start + nVars + 0, ' ' );
1469 Vec_StrWriteEntry( vSop[n], Start + nVars + 1, (char)(n ? '0' : '1') );
1470 Vec_StrWriteEntry( vSop[n], Start + nVars + 2, '\n' );
1471 Vec_StrWriteEntry( vSop[n], Start + nVars + 3, '\0' );
1472 Vec_IntClear( vCube );
1473 Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) );
1474 Vec_IntForEachEntry( vNums, iVar, v )
1475 {
1476 int iLit = Vec_IntEntry( vLits, iVar );
1477 Vec_IntPush( vCube, Abc_LitNot(iLit) );
1478 if ( fReverse )
1479 Vec_StrWriteEntry( vSop[n], Start + nVars - iVar - 1, (char)('0' + !Abc_LitIsCompl(iLit)) );
1480 else
1481 Vec_StrWriteEntry( vSop[n], Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) );
1482 }
1483 // add cube
1484 status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) );
1485 if ( status == 0 )
1486 {
1487 fComplete[n] = 1;
1488 break;
1489 }
1490 assert( status == 1 );
1491 }
1492 if ( fComplete[0] || fComplete[1] )
1493 break;
1494 }
1495cleanup:
1496 Vec_IntFree( vVars );
1497 Vec_IntFree( vLits );
1498 Vec_IntFree( vNums );
1499 Vec_IntFree( vCube );
1500 assert( !fComplete[0] || !fComplete[1] );
1501 if ( fComplete[0] || fComplete[1] ) // one of the cover is computed
1502 {
1503 vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL;
1504 if ( iCube > 1 )
1505// Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
1506 Bmc_CollapseIrredundantFull( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
1507 }
1508 if ( fVeryVerbose )
1509 {
1510 int fProfile = 0;
1511 printf( "Processed output with %d supp vars. ", nVars );
1512 if ( vRes == NULL )
1513 printf( "The resulting SOP exceeded %d cubes.\n", nCubeLim );
1514 else
1515 printf( "The best cover contains %d cubes.\n", Vec_StrSize(vRes)/(nVars +3) );
1516 Abc_PrintTime( 1, "Onset minterm", Time[0][0] );
1517 Abc_PrintTime( 1, "Onset expand ", Time[0][1] );
1518 Abc_PrintTime( 1, "Offset minterm", Time[1][0] );
1519 Abc_PrintTime( 1, "Offset expand ", Time[1][1] );
1520 if ( fProfile )
1521 {
1522 Abc_PrintTime( 1, "Expand check1 ", clkCheck1 ); clkCheck1 = 0;
1523 Abc_PrintTime( 1, "Expand check2 ", clkCheck2 ); clkCheck2 = 0;
1524 Abc_PrintTime( 1, "Expand sat ", clkCheckS ); clkCheckS = 0;
1525 Abc_PrintTime( 1, "Expand unsat ", clkCheckU ); clkCheckU = 0;
1526 }
1527 }
1528 Vec_StrFreeP( &vSop[0] );
1529 Vec_StrFreeP( &vSop[1] );
1530 return vRes;
1531}
Bmc_CollapseExpand
int Bmc_CollapseExpand(sat_solver *pSat, sat_solver *pSatOn, Vec_Int_t *vLits, Vec_Int_t *vNums, Vec_Int_t *vTemp, int nBTLimit, int fCanon, int fOnOffSetLit)
Definition bmcClp.c:460
Bmc_CollapseIrredundantFull
int Bmc_CollapseIrredundantFull(Vec_Str_t *vSop, int nCubes, int nVars)
Definition bmcClp.c:275
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CollapseOne_int2()

Vec_Str_t * Bmc_CollapseOne_int2 ( sat_solver * pSat1,
sat_solver * pSat2,
int nVars,
int nCubeLim,
int nBTLimit,
int fCanon,
int fReverse,
int fVerbose )

Function*************************************************************

Synopsis [This code computes on-set and off-set simultaneously.]

Description []

SideEffects []

SeeAlso []

Definition at line 1226 of file bmcClp.c.

1227{
1228 int fVeryVerbose = fVerbose;
1229 sat_solver * pSat[2] = { pSat1, pSat2 };
1230 Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL;
1231 Vec_Int_t * vVars = Vec_IntAlloc( nVars+1 );
1232 Vec_Int_t * vLits = Vec_IntAlloc( nVars+1 );
1233 Vec_Int_t * vNums = Vec_IntAlloc( nVars+1 );
1234 Vec_Int_t * vCube = Vec_IntAlloc( nVars+1 );
1235 int n, v, iVar, pLits[2], iCube = 0, Start, status;
1236 abctime clk = 0, Time[2][2] = {{0}};
1237 int fComplete[2] = {0};
1238 // variables
1239 int iOutVar = 2;
1240 int iOOVars[2] = {0, 1};
1241// int iOutVar = 1;
1242// int iOOVars[2] = {sat_solver_nvars(pSat) - 5, sat_solver_nvars(pSat) - 5 + 1};
1243
1244 // collect CI variables (0 = onset enable, 1 = offset enable, 2 = output)
1245 int iCiVarBeg = 3;
1246// int iCiVarBeg = sat_solver_nvars(pSat) - 5 - nVars;
1247 if ( fReverse )
1248 for ( v = nVars - 1; v >= 0; v-- )
1249 Vec_IntPush( vVars, iCiVarBeg + v );
1250 else
1251 for ( v = 0; v < nVars; v++ )
1252 Vec_IntPush( vVars, iCiVarBeg + v );
1253
1254 // check that on-set/off-set is sat
1255 for ( n = 0; n < 2; n++ )
1256 {
1257 pLits[0] = Abc_Var2Lit( iOutVar, n ); // n=0 => F=1 n=1 => F=0
1258 status = sat_solver_solve( pSat[n], pLits, pLits + 1, nBTLimit, 0, 0, 0 );
1259 if ( status == l_Undef )
1260 goto cleanup; // timeout
1261 if ( status == l_False )
1262 {
1263 Vec_StrClear( vSop[0] );
1264 Vec_StrPrintStr( vSop[0], n ? " 1\n" : " 0\n" );
1265 Vec_StrPush( vSop[0], '\0' );
1266 fComplete[0] = 1;
1267 goto cleanup; // const0/1
1268 }
1269 // add literals to the solver
1270 status = sat_solver_addclause( pSat[n], pLits, pLits + 1 );
1271 assert( status );
1272 // start cover
1273 Vec_StrPush( vSop[n], '\0' );
1274 }
1275
1276 // compute cube pairs
1277 for ( iCube = 0; nCubeLim == 0 || iCube < nCubeLim; iCube++ )
1278 {
1279 for ( n = 0; n < 2; n++ )
1280 {
1281 if ( fVeryVerbose ) clk = Abc_Clock();
1282 // get the assignment
1283 sat_solver_clean_polarity( pSat[n], Vec_IntArray(vVars), Vec_IntSize(vVars) );
1284 pLits[0] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses
1285// pLits[1] = Abc_Var2Lit( iOutVar, n ); // set output
1286// status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
1287 status = sat_solver_solve( pSat[n], pLits, pLits + 1, 0, 0, 0, 0 );
1288 if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk;
1289 if ( status == l_Undef )
1290 goto cleanup; // timeout
1291 if ( status == l_False )
1292 {
1293 fComplete[n] = 1;
1294 break;
1295 }
1296 // collect values
1297 Vec_IntClear( vLits );
1298 Vec_IntForEachEntry( vVars, iVar, v )
1299 Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[n], iVar)) );
1300 // expand the values
1301 if ( fVeryVerbose ) clk = Abc_Clock();
1302// status = Bmc_CollapseExpand( pSat, NULL, vLits, vNums, vCube, nBTLimit, fCanon, Abc_Var2Lit(iOutVar, !n) );
1303 status = Bmc_CollapseExpand( pSat[!n], NULL, vLits, vNums, vCube, nBTLimit, fCanon, -1 );
1304 if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk;
1305 if ( status < 0 )
1306 goto cleanup; // timeout
1307 // collect cube
1308 Vec_StrPop( vSop[n] );
1309 Start = Vec_StrSize( vSop[n] );
1310 Vec_StrFillExtra( vSop[n], Start + nVars + 4, '-' );
1311 Vec_StrWriteEntry( vSop[n], Start + nVars + 0, ' ' );
1312 Vec_StrWriteEntry( vSop[n], Start + nVars + 1, (char)(n ? '0' : '1') );
1313 Vec_StrWriteEntry( vSop[n], Start + nVars + 2, '\n' );
1314 Vec_StrWriteEntry( vSop[n], Start + nVars + 3, '\0' );
1315 Vec_IntClear( vCube );
1316 Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) );
1317 Vec_IntForEachEntry( vNums, iVar, v )
1318 {
1319 int iLit = Vec_IntEntry( vLits, iVar );
1320 Vec_IntPush( vCube, Abc_LitNot(iLit) );
1321 if ( fReverse )
1322 Vec_StrWriteEntry( vSop[n], Start + nVars - iVar - 1, (char)('0' + !Abc_LitIsCompl(iLit)) );
1323 else
1324 Vec_StrWriteEntry( vSop[n], Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) );
1325 }
1326 // add cube
1327// status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) );
1328 status = sat_solver_addclause( pSat[n], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
1329 if ( status == 0 )
1330 {
1331 fComplete[n] = 1;
1332 break;
1333 }
1334 assert( status == 1 );
1335 }
1336 if ( fComplete[0] || fComplete[1] )
1337 break;
1338 }
1339cleanup:
1340 Vec_IntFree( vVars );
1341 Vec_IntFree( vLits );
1342 Vec_IntFree( vNums );
1343 Vec_IntFree( vCube );
1344 assert( !fComplete[0] || !fComplete[1] );
1345 if ( fComplete[0] || fComplete[1] ) // one of the cover is computed
1346 {
1347 vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL;
1348 if ( iCube > 1 )
1349// Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
1350 Bmc_CollapseIrredundantFull( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
1351 }
1352 if ( fVeryVerbose )
1353 {
1354 int fProfile = 0;
1355 printf( "Processed output with %d supp vars. ", nVars );
1356 if ( vRes == NULL )
1357 printf( "The resulting SOP exceeded %d cubes.\n", nCubeLim );
1358 else
1359 printf( "The best cover contains %d cubes.\n", Vec_StrSize(vRes)/(nVars +3) );
1360 Abc_PrintTime( 1, "Onset minterm", Time[0][0] );
1361 Abc_PrintTime( 1, "Onset expand ", Time[0][1] );
1362 Abc_PrintTime( 1, "Offset minterm", Time[1][0] );
1363 Abc_PrintTime( 1, "Offset expand ", Time[1][1] );
1364 if ( fProfile )
1365 {
1366 Abc_PrintTime( 1, "Expand check1 ", clkCheck1 ); clkCheck1 = 0;
1367 Abc_PrintTime( 1, "Expand check2 ", clkCheck2 ); clkCheck2 = 0;
1368 Abc_PrintTime( 1, "Expand sat ", clkCheckS ); clkCheckS = 0;
1369 Abc_PrintTime( 1, "Expand unsat ", clkCheckU ); clkCheckU = 0;
1370 }
1371 }
1372 Vec_StrFreeP( &vSop[0] );
1373 Vec_StrFreeP( &vSop[1] );
1374 return vRes;
1375}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CollapseOne_int3()

Vec_Str_t * Bmc_CollapseOne_int3 ( sat_solver * pSat0,
sat_solver * pSat1,
sat_solver * pSat2,
sat_solver * pSat3,
int nVars,
int nCubeLim,
int nBTLimit,
int fCanon,
int fReverse,
int fVerbose )

Function*************************************************************

Synopsis [This code computes on-set and off-set simultaneously.]

Description []

SideEffects []

SeeAlso []

Definition at line 1040 of file bmcClp.c.

1041{
1042 int fVeryVerbose = fVerbose;
1043 sat_solver * pSat[2] = { pSat0, pSat1 };
1044 sat_solver * pSatClean[2] = { pSat2, pSat3 };
1045 Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL;
1046 Vec_Int_t * vLitsC[2] = { Vec_IntAlloc(nVars), Vec_IntAlloc(nVars) };
1047 Vec_Int_t * vVars = Vec_IntAlloc( nVars );
1048 Vec_Int_t * vLits = Vec_IntAlloc( nVars );
1049 Vec_Int_t * vNums = Vec_IntAlloc( nVars );
1050 Vec_Int_t * vCube = Vec_IntAlloc( nVars );
1051 int n, v, iVar, iLit, iCiVarBeg, iCube = 0, Start, status;
1052 abctime clk = 0, Time[2][2] = {{0}};
1053 int fComplete[2] = {0};
1054
1055 // collect CI variables
1056// iCiVarBeg = pCnf->nVars - nVars;// - 1;
1057 iCiVarBeg = sat_solver_nvars(pSat0) - nVars;
1058 if ( fReverse )
1059 for ( v = nVars - 1; v >= 0; v-- )
1060 Vec_IntPush( vVars, iCiVarBeg + v );
1061 else
1062 for ( v = 0; v < nVars; v++ )
1063 Vec_IntPush( vVars, iCiVarBeg + v );
1064
1065 // check that on-set/off-set is sat
1066 for ( n = 0; n < 2; n++ )
1067 {
1068 iLit = Abc_Var2Lit( 1, n ); // n=0 => F=1 n=1 => F=0
1069 status = sat_solver_solve( pSat[n], &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
1070 if ( status == l_Undef )
1071 goto cleanup; // timeout
1072 if ( status == l_False )
1073 {
1074 Vec_StrClear( vSop[0] );
1075 Vec_StrPrintStr( vSop[0], n ? " 1\n" : " 0\n" );
1076 Vec_StrPush( vSop[0], '\0' );
1077 fComplete[0] = 1;
1078 goto cleanup; // const0/1
1079 }
1080 // start with all negative literals
1081 Vec_IntForEachEntry( vVars, iVar, v )
1082 Vec_IntPush( vLitsC[n], Abc_Var2Lit(iVar, 1) );
1083 // add literals to the solver
1084 status = sat_solver_addclause( pSat[n], &iLit, &iLit + 1 );
1085 assert( status );
1086 status = sat_solver_addclause( pSatClean[n], &iLit, &iLit + 1 );
1087 assert( status );
1088 // start cover
1089 Vec_StrPush( vSop[n], '\0' );
1090 }
1091
1092 // compute cube pairs
1093 for ( iCube = 0; nCubeLim == 0 || iCube < nCubeLim; iCube++ )
1094 {
1095 for ( n = 0; n < 2; n++ )
1096 {
1097 if ( fVeryVerbose ) clk = Abc_Clock();
1098 // get the assignment
1099 if ( fCanon )
1100 status = Bmc_ComputeCanonical( pSat[n], vLitsC[n], vCube, nBTLimit );
1101 else
1102 {
1103 sat_solver_clean_polarity( pSat[n], Vec_IntArray(vVars), Vec_IntSize(vVars) );
1104 status = sat_solver_solve( pSat[n], NULL, NULL, 0, 0, 0, 0 );
1105 }
1106 if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk;
1107 if ( status == l_Undef )
1108 goto cleanup; // timeout
1109 if ( status == l_False )
1110 {
1111 fComplete[n] = 1;
1112 break;
1113 }
1114 // collect values
1115 Vec_IntClear( vLits );
1116 Vec_IntClear( vLitsC[n] );
1117 Vec_IntForEachEntry( vVars, iVar, v )
1118 {
1119 iLit = Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[n], iVar));
1120 Vec_IntPush( vLits, iLit );
1121 Vec_IntPush( vLitsC[n], iLit );
1122 }
1123 // expand the values
1124 if ( fVeryVerbose ) clk = Abc_Clock();
1125 status = Bmc_CollapseExpand( pSatClean[!n], pSat[n], vLits, vNums, vCube, nBTLimit, fCanon, -1 );
1126 if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk;
1127 if ( status < 0 )
1128 goto cleanup; // timeout
1129 // collect cube
1130 Vec_StrPop( vSop[n] );
1131 Start = Vec_StrSize( vSop[n] );
1132 Vec_StrFillExtra( vSop[n], Start + nVars + 4, '-' );
1133 Vec_StrWriteEntry( vSop[n], Start + nVars + 0, ' ' );
1134 Vec_StrWriteEntry( vSop[n], Start + nVars + 1, (char)(n ? '0' : '1') );
1135 Vec_StrWriteEntry( vSop[n], Start + nVars + 2, '\n' );
1136 Vec_StrWriteEntry( vSop[n], Start + nVars + 3, '\0' );
1137 Vec_IntClear( vCube );
1138 Vec_IntForEachEntry( vNums, iVar, v )
1139 {
1140 iLit = Vec_IntEntry( vLits, iVar );
1141 Vec_IntPush( vCube, Abc_LitNot(iLit) );
1142 if ( fReverse )
1143 Vec_StrWriteEntry( vSop[n], Start + nVars - iVar - 1, (char)('0' + !Abc_LitIsCompl(iLit)) );
1144 else
1145 Vec_StrWriteEntry( vSop[n], Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) );
1146 }
1147 // add cube
1148 status = sat_solver_addclause( pSat[n], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
1149 if ( status == 0 )
1150 {
1151 fComplete[n] = 1;
1152 break;
1153 }
1154 assert( status == 1 );
1155 }
1156 if ( fComplete[0] || fComplete[1] )
1157 break;
1158 }
1159cleanup:
1160 Vec_IntFree( vVars );
1161 Vec_IntFree( vLits );
1162 Vec_IntFree( vLitsC[0] );
1163 Vec_IntFree( vLitsC[1] );
1164 Vec_IntFree( vNums );
1165 Vec_IntFree( vCube );
1166 assert( !fComplete[0] || !fComplete[1] );
1167 if ( fComplete[0] || fComplete[1] ) // one of the cover is computed
1168 {
1169 vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL;
1170 if ( iCube > 1 )
1171// Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
1172 Bmc_CollapseIrredundantFull( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
1173 }
1174 if ( fVeryVerbose )
1175 {
1176 int fProfile = 0;
1177 printf( "Processed output with %d supp vars. ", nVars );
1178 if ( vRes == NULL )
1179 printf( "The resulting SOP exceeded %d cubes.\n", nCubeLim );
1180 else
1181 printf( "The best cover contains %d cubes.\n", Vec_StrSize(vRes)/(nVars +3) );
1182 Abc_PrintTime( 1, "Onset minterm", Time[0][0] );
1183 Abc_PrintTime( 1, "Onset expand ", Time[0][1] );
1184 Abc_PrintTime( 1, "Offset minterm", Time[1][0] );
1185 Abc_PrintTime( 1, "Offset expand ", Time[1][1] );
1186 if ( fProfile )
1187 {
1188 Abc_PrintTime( 1, "Expand check1 ", clkCheck1 ); clkCheck1 = 0;
1189 Abc_PrintTime( 1, "Expand check2 ", clkCheck2 ); clkCheck2 = 0;
1190 Abc_PrintTime( 1, "Expand sat ", clkCheckS ); clkCheckS = 0;
1191 Abc_PrintTime( 1, "Expand unsat ", clkCheckU ); clkCheckU = 0;
1192 }
1193 }
1194 Vec_StrFreeP( &vSop[0] );
1195 Vec_StrFreeP( &vSop[1] );
1196 return vRes;
1197}
Bmc_ComputeCanonical
int Bmc_ComputeCanonical(sat_solver *pSat, Vec_Int_t *vLits, Vec_Int_t *vTemp, int nBTLimit)
Definition bmcClp.c:648
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition satSolver.c:2369
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CollapseOneInt2()

Vec_Str_t * Bmc_CollapseOneInt2 ( Gia_Man_t * p,
int nCubeLim,
int nBTLimit,
int fCanon,
int fReverse,
int fVerbose,
int fCompl )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 665 of file bmcClp.c.

666{
667 int fPrintMinterm = 0;
668 int nVars = Gia_ManCiNum(p);
669 Vec_Int_t * vVars = Vec_IntAlloc( nVars );
670 Vec_Int_t * vLits = Vec_IntAlloc( nVars );
671 Vec_Int_t * vLitsC= Vec_IntAlloc( nVars );
672 Vec_Int_t * vNums = Vec_IntAlloc( nVars );
673 Vec_Int_t * vCube = Vec_IntAlloc( nVars );
674 Vec_Str_t * vSop = Vec_StrAlloc( 100 );
675 int iOut = 0, iLit, iVar, status, n, Count, Start;
676
677 // create SAT solver
678 Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
679 sat_solver * pSat[3] = {
680 (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0),
681 (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0),
682 fCanon ? (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) : NULL
683 };
684
685 // collect CI variables
686 int iCiVarBeg = pCnf->nVars - nVars;// - 1;
687 if ( fReverse )
688 for ( n = nVars - 1; n >= 0; n-- )
689 Vec_IntPush( vVars, iCiVarBeg + n );
690 else
691 for ( n = 0; n < nVars; n++ )
692 Vec_IntPush( vVars, iCiVarBeg + n );
693
694 // start with all negative literals
695 Vec_IntForEachEntry( vVars, iVar, n )
696 Vec_IntPush( vLitsC, Abc_Var2Lit(iVar, 1) );
697
698 // check that on-set/off-set is sat
699 for ( n = 0; n < 2 + fCanon; n++ )
700 {
701 iLit = Abc_Var2Lit( iOut + 1, n&1 ); // n=0 => F=1 n=1 => F=0
702 status = sat_solver_addclause( pSat[n], &iLit, &iLit + 1 );
703 if ( status == 0 )
704 {
705 Vec_StrPrintStr( vSop, ((n&1) ^ fCompl) ? " 1\n" : " 0\n" );
706 Vec_StrPush( vSop, '\0' );
707 goto cleanup; // const0/1
708 }
709 status = sat_solver_solve( pSat[n], NULL, NULL, nBTLimit, 0, 0, 0 );
710 if ( status == l_Undef )
711 {
712 Vec_StrFreeP( &vSop );
713 goto cleanup; // timeout
714 }
715 if ( status == l_False )
716 {
717 Vec_StrPrintStr( vSop, ((n&1) ^ fCompl) ? " 1\n" : " 0\n" );
718 Vec_StrPush( vSop, '\0' );
719 goto cleanup; // const0/1
720 }
721 }
722 Vec_StrPush( vSop, '\0' );
723
724 // prepare on-set for solving
725// if ( fCanon )
726// sat_solver_prepare_enum( pSat[0], Vec_IntArray(vVars), Vec_IntSize(vVars) );
727 Count = 0;
728 while ( 1 )
729 {
730 // get the assignment
731 if ( fCanon )
732 status = Bmc_ComputeCanonical( pSat[0], vLitsC, vCube, nBTLimit );
733 else
734 {
735 sat_solver_clean_polarity( pSat[0], Vec_IntArray(vVars), Vec_IntSize(vVars) );
736 status = sat_solver_solve( pSat[0], NULL, NULL, 0, 0, 0, 0 );
737 }
738 if ( status == l_Undef )
739 {
740 Vec_StrFreeP( &vSop );
741 goto cleanup; // timeout
742 }
743 if ( status == l_False )
744 break;
745 // check number of cubes
746 if ( nCubeLim > 0 && Count == nCubeLim )
747 {
748 //printf( "The number of cubes exceeded the limit (%d).\n", nCubeLim );
749 Vec_StrFreeP( &vSop );
750 goto cleanup; // cube out
751 }
752 // collect values
753 Vec_IntClear( vLits );
754 Vec_IntClear( vLitsC );
755 Vec_IntForEachEntry( vVars, iVar, n )
756 {
757 iLit = Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[0], iVar));
758 Vec_IntPush( vLits, iLit );
759 Vec_IntPush( vLitsC, iLit );
760 }
761 // print minterm
762 if ( fPrintMinterm )
763 {
764 printf( "Mint: " );
765 Vec_IntForEachEntry( vLits, iLit, n )
766 printf( "%d", !Abc_LitIsCompl(iLit) );
767 printf( "\n" );
768 }
769 // expand the values
770 status = Bmc_CollapseExpand( pSat[1], fCanon ? pSat[2] : pSat[0], vLits, vNums, vCube, nBTLimit, fCanon, -1 );
771 if ( status < 0 )
772 {
773 Vec_StrFreeP( &vSop );
774 goto cleanup; // timeout
775 }
776 // collect cube
777 Vec_StrPop( vSop );
778 Start = Vec_StrSize( vSop );
779 Vec_StrFillExtra( vSop, Start + nVars + 4, '-' );
780 Vec_StrWriteEntry( vSop, Start + nVars + 0, ' ' );
781 Vec_StrWriteEntry( vSop, Start + nVars + 1, (char)(fCompl ? '0' : '1') );
782 Vec_StrWriteEntry( vSop, Start + nVars + 2, '\n' );
783 Vec_StrWriteEntry( vSop, Start + nVars + 3, '\0' );
784 Vec_IntClear( vCube );
785 Vec_IntForEachEntry( vNums, iVar, n )
786 {
787 iLit = Vec_IntEntry( vLits, iVar );
788 Vec_IntPush( vCube, Abc_LitNot(iLit) );
789 if ( fReverse )
790 Vec_StrWriteEntry( vSop, Start + nVars - iVar - 1, (char)('0' + !Abc_LitIsCompl(iLit)) );
791 else
792 Vec_StrWriteEntry( vSop, Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) );
793 }
794 //if ( fVerbose )
795 // printf( "Cube %4d: %s", Count, Vec_StrArray(vSop) + Start );
796 Count++;
797 // add cube
798 status = sat_solver_addclause( pSat[0], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
799 if ( status == 0 )
800 break;
801 // add cube
802 if ( fCanon )
803 status = sat_solver_addclause( pSat[2], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
804 assert( status == 1 );
805 }
806 //printf( "Finished enumerating %d assignments.\n", Count );
807cleanup:
808 Vec_IntFree( vVars );
809 Vec_IntFree( vLits );
810 Vec_IntFree( vLitsC );
811 Vec_IntFree( vNums );
812 Vec_IntFree( vCube );
813 sat_solver_delete( pSat[0] );
814 sat_solver_delete( pSat[1] );
815 if ( fCanon )
816 sat_solver_delete( pSat[2] );
817 Cnf_DataFree( pCnf );
818 // quickly reduce contained cubes
819 if ( vSop != NULL )
820 Bmc_CollapseIrredundant( vSop, Vec_StrSize(vSop)/(nVars +3), nVars );
821 return vSop;
822}
Bmc_CollapseIrredundant
int Bmc_CollapseIrredundant(Vec_Str_t *vSop, int nCubes, int nVars)
Definition bmcClp.c:202
Cnf_Dat_t_::nVars
int nVars
Definition cnf.h:59
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CollapseOneOld()

Vec_Str_t * Bmc_CollapseOneOld ( Gia_Man_t * p,
int nCubeLim,
int nBTLimit,
int fCanon,
int fReverse,
int fVerbose )

Function*************************************************************

Synopsis [This code computes on-set and off-set simultaneously.]

Description []

SideEffects []

SeeAlso []

Definition at line 864 of file bmcClp.c.

865{
866 int fVeryVerbose = fVerbose;
867 int nVars = Gia_ManCiNum(p);
868 Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
869 sat_solver * pSat[2] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) };
870 sat_solver * pSatClean[2] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) };
871 Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL;
872 Vec_Int_t * vLitsC[2] = { Vec_IntAlloc(nVars), Vec_IntAlloc(nVars) };
873 Vec_Int_t * vVars = Vec_IntAlloc( nVars );
874 Vec_Int_t * vLits = Vec_IntAlloc( nVars );
875 Vec_Int_t * vNums = Vec_IntAlloc( nVars );
876 Vec_Int_t * vCube = Vec_IntAlloc( nVars );
877 int n, v, iVar, iLit, iCiVarBeg, iCube = 0, Start, status;
878 abctime clk = 0, Time[2][2] = {{0}};
879 int fComplete[2] = {0};
880
881 // collect CI variables
882 iCiVarBeg = pCnf->nVars - nVars;// - 1;
883 if ( fReverse )
884 for ( v = nVars - 1; v >= 0; v-- )
885 Vec_IntPush( vVars, iCiVarBeg + v );
886 else
887 for ( v = 0; v < nVars; v++ )
888 Vec_IntPush( vVars, iCiVarBeg + v );
889
890 // check that on-set/off-set is sat
891 for ( n = 0; n < 2; n++ )
892 {
893 iLit = Abc_Var2Lit( 1, n ); // n=0 => F=1 n=1 => F=0
894 status = sat_solver_solve( pSat[n], &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
895 if ( status == l_Undef )
896 goto cleanup; // timeout
897 if ( status == l_False )
898 {
899 Vec_StrClear( vSop[0] );
900 Vec_StrPrintStr( vSop[0], n ? " 1\n" : " 0\n" );
901 Vec_StrPush( vSop[0], '\0' );
902 fComplete[0] = 1;
903 goto cleanup; // const0/1
904 }
905 // start with all negative literals
906 Vec_IntForEachEntry( vVars, iVar, v )
907 Vec_IntPush( vLitsC[n], Abc_Var2Lit(iVar, 1) );
908 // add literals to the solver
909 status = sat_solver_addclause( pSat[n], &iLit, &iLit + 1 );
910 assert( status );
911 status = sat_solver_addclause( pSatClean[n], &iLit, &iLit + 1 );
912 assert( status );
913 // start cover
914 Vec_StrPush( vSop[n], '\0' );
915 }
916
917 // compute cube pairs
918 for ( iCube = 0; nCubeLim == 0 || iCube < nCubeLim; iCube++ )
919 {
920 for ( n = 0; n < 2; n++ )
921 {
922 if ( fVeryVerbose ) clk = Abc_Clock();
923 // get the assignment
924 if ( fCanon )
925 status = Bmc_ComputeCanonical( pSat[n], vLitsC[n], vCube, nBTLimit );
926 else
927 {
928 sat_solver_clean_polarity( pSat[n], Vec_IntArray(vVars), Vec_IntSize(vVars) );
929 status = sat_solver_solve( pSat[n], NULL, NULL, 0, 0, 0, 0 );
930 }
931 if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk;
932 if ( status == l_Undef )
933 goto cleanup; // timeout
934 if ( status == l_False )
935 {
936 fComplete[n] = 1;
937 break;
938 }
939 // collect values
940 Vec_IntClear( vLits );
941 Vec_IntClear( vLitsC[n] );
942 Vec_IntForEachEntry( vVars, iVar, v )
943 {
944 iLit = Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[n], iVar));
945 Vec_IntPush( vLits, iLit );
946 Vec_IntPush( vLitsC[n], iLit );
947 }
948 // expand the values
949 if ( fVeryVerbose ) clk = Abc_Clock();
950 status = Bmc_CollapseExpand( pSatClean[!n], pSat[n], vLits, vNums, vCube, nBTLimit, fCanon, -1 );
951 if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk;
952 if ( status < 0 )
953 goto cleanup; // timeout
954 // collect cube
955 Vec_StrPop( vSop[n] );
956 Start = Vec_StrSize( vSop[n] );
957 Vec_StrFillExtra( vSop[n], Start + nVars + 4, '-' );
958 Vec_StrWriteEntry( vSop[n], Start + nVars + 0, ' ' );
959 Vec_StrWriteEntry( vSop[n], Start + nVars + 1, (char)(n ? '0' : '1') );
960 Vec_StrWriteEntry( vSop[n], Start + nVars + 2, '\n' );
961 Vec_StrWriteEntry( vSop[n], Start + nVars + 3, '\0' );
962 Vec_IntClear( vCube );
963 Vec_IntForEachEntry( vNums, iVar, v )
964 {
965 iLit = Vec_IntEntry( vLits, iVar );
966 Vec_IntPush( vCube, Abc_LitNot(iLit) );
967 if ( fReverse )
968 Vec_StrWriteEntry( vSop[n], Start + nVars - iVar - 1, (char)('0' + !Abc_LitIsCompl(iLit)) );
969 else
970 Vec_StrWriteEntry( vSop[n], Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) );
971 }
972 // add cube
973 status = sat_solver_addclause( pSat[n], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
974 if ( status == 0 )
975 {
976 fComplete[n] = 1;
977 break;
978 }
979 assert( status == 1 );
980 }
981 if ( fComplete[0] || fComplete[1] )
982 break;
983 }
984cleanup:
985 Vec_IntFree( vVars );
986 Vec_IntFree( vLits );
987 Vec_IntFree( vLitsC[0] );
988 Vec_IntFree( vLitsC[1] );
989 Vec_IntFree( vNums );
990 Vec_IntFree( vCube );
991 Cnf_DataFree( pCnf );
992 sat_solver_delete( pSat[0] );
993 sat_solver_delete( pSat[1] );
994 sat_solver_delete( pSatClean[0] );
995 sat_solver_delete( pSatClean[1] );
996 assert( !fComplete[0] || !fComplete[1] );
997 if ( fComplete[0] || fComplete[1] ) // one of the cover is computed
998 {
999 vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL;
1000 if ( iCube > 1 )
1001// Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
1002 Bmc_CollapseIrredundantFull( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
1003 }
1004 if ( fVeryVerbose )
1005 {
1006 int fProfile = 0;
1007 printf( "Processed output with %d supp vars. ", nVars );
1008 if ( vRes == NULL )
1009 printf( "The resulting SOP exceeded %d cubes.\n", nCubeLim );
1010 else
1011 printf( "The best cover contains %d cubes.\n", Vec_StrSize(vRes)/(nVars +3) );
1012 Abc_PrintTime( 1, "Onset minterm", Time[0][0] );
1013 Abc_PrintTime( 1, "Onset expand ", Time[0][1] );
1014 Abc_PrintTime( 1, "Offset minterm", Time[1][0] );
1015 Abc_PrintTime( 1, "Offset expand ", Time[1][1] );
1016 if ( fProfile )
1017 {
1018 Abc_PrintTime( 1, "Expand check1 ", clkCheck1 ); clkCheck1 = 0;
1019 Abc_PrintTime( 1, "Expand check2 ", clkCheck2 ); clkCheck2 = 0;
1020 Abc_PrintTime( 1, "Expand sat ", clkCheckS ); clkCheckS = 0;
1021 Abc_PrintTime( 1, "Expand unsat ", clkCheckU ); clkCheckU = 0;
1022 }
1023 }
1024 Vec_StrFreeP( &vSop[0] );
1025 Vec_StrFreeP( &vSop[1] );
1026 return vRes;
1027}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CollapseOneOld2()

Vec_Str_t * Bmc_CollapseOneOld2 ( Gia_Man_t * p,
int nCubeLim,
int nBTLimit,
int fCanon,
int fReverse,
int fVerbose )

Definition at line 823 of file bmcClp.c.

824{
825 Vec_Str_t * vSopOn, * vSopOff;
826 int nCubesOn = ABC_INFINITY;
827 int nCubesOff = ABC_INFINITY;
828 vSopOn = Bmc_CollapseOneInt2( p, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose, 0 );
829 if ( vSopOn )
830 nCubesOn = Vec_StrCountEntry(vSopOn,'\n');
831 Gia_ObjFlipFaninC0( Gia_ManPo(p, 0) );
832 vSopOff = Bmc_CollapseOneInt2( p, Abc_MinInt(nCubeLim, nCubesOn), nBTLimit, fCanon, fReverse, fVerbose, 1 );
833 Gia_ObjFlipFaninC0( Gia_ManPo(p, 0) );
834 if ( vSopOff )
835 nCubesOff = Vec_StrCountEntry(vSopOff,'\n');
836 if ( vSopOn == NULL )
837 return vSopOff;
838 if ( vSopOff == NULL )
839 return vSopOn;
840 if ( nCubesOn <= nCubesOff )
841 {
842 Vec_StrFree( vSopOff );
843 return vSopOn;
844 }
845 else
846 {
847 Vec_StrFree( vSopOn );
848 return vSopOff;
849 }
850}
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
Bmc_CollapseOneInt2
Vec_Str_t * Bmc_CollapseOneInt2(Gia_Man_t *p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose, int fCompl)
Definition bmcClp.c:665
Here is the call graph for this function:

◆ Bmc_ComputeCanonical()

int Bmc_ComputeCanonical ( sat_solver * pSat,
Vec_Int_t * vLits,
Vec_Int_t * vTemp,
int nBTLimit )

Definition at line 648 of file bmcClp.c.

649{
650 sat_solver_set_resource_limits( pSat, nBTLimit, 0, 0, 0 );
651 return sat_solver_solve_lexsat( pSat, Vec_IntArray(vLits), Vec_IntSize(vLits) );
652}
sat_solver_set_resource_limits
void sat_solver_set_resource_limits(sat_solver *s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition satSolver.c:2051
sat_solver_solve_lexsat
int sat_solver_solve_lexsat(sat_solver *s, int *pLits, int nLits)
Definition satSolver.c:2143
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_ComputeCanonical2()

int Bmc_ComputeCanonical2 ( sat_solver * pSat,
Vec_Int_t * vLits,
Vec_Int_t * vTemp,
int nBTLimit )

Function*************************************************************

Synopsis [Returns SAT solver in the 'sat' state with the given assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 619 of file bmcClp.c.

620{
621 int i, k, iLit, status = l_Undef;
622 for ( i = 0; i < Vec_IntSize(vLits); i++ )
623 {
624 // copy the first i+1 literals
625 Vec_IntClear( vTemp );
626 Vec_IntForEachEntryStop( vLits, iLit, k, i+1 )
627 Vec_IntPush( vTemp, iLit );
628 // check if it satisfies the on-set
629 status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 );
630 if ( status == l_Undef )
631 return l_Undef;
632 if ( status == l_True )
633 continue;
634 // if it is UNSAT, try the opposite literal
635 iLit = Vec_IntEntry( vLits, i );
636 // if literal is positive, there is no way to flip it
637 if ( !Abc_LitIsCompl(iLit) )
638 return l_False;
639 Vec_IntWriteEntry( vLits, i, Abc_LitNot(iLit) );
640 Vec_IntForEachEntryStart( vLits, iLit, k, i+1 )
641 Vec_IntWriteEntry( vLits, k, Abc_LitNot(Abc_LitRegular(iLit)) );
642 // recheck
643 i--;
644 }
645 assert( status == l_True );
646 return status;
647}
if
if(last==0)
Definition sparse_int.h:34
Vec_IntForEachEntryStop
#define Vec_IntForEachEntryStop(vVec, Entry, i, Stop)
Definition vecInt.h:58
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56

◆ Bmc_ComputeSimDiff()

ABC_NAMESPACE_IMPL_START int Bmc_ComputeSimDiff ( Gia_Man_t * p,
Vec_Int_t * vPat,
Vec_Int_t * vPat2 )

DECLARATIONS ///.

CFile****************************************************************

FileName [bmcClp.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [INT-FX: Interpolation-based logic sharing extraction.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
bmcClp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [For a given random pattern, compute output change.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file bmcClp.c.

49{
50 Gia_Obj_t * pObj;
51 int i, Id; word Sim, Sim0, Sim1;
52 Gia_ManForEachCiId( p, Id, i )
53 {
54 Sim = Vec_IntEntry(vPat, i) ? ~(word)0 : 0;
55 Sim ^= (word)1 << (i + 1);
56 Vec_WrdWriteEntry( p->vSims, Id, Sim );
57 }
58 Gia_ManForEachAnd( p, pObj, i )
59 {
60 Sim0 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId0(pObj, i) );
61 Sim1 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId1(pObj, i) );
62 Sim0 = Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0;
63 Sim1 = Gia_ObjFaninC1(pObj) ? ~Sim1 : Sim1;
64 Vec_WrdWriteEntry( p->vSims, i, Sim0 & Sim1 );
65 }
66 Gia_ManForEachCo( p, pObj, i )
67 {
68 Id = Gia_ObjId( p, pObj );
69 Sim0 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId0(pObj, Id) );
70 Sim0 = Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0;
71 Vec_WrdWriteEntry( p->vSims, Id, Sim0 );
72 }
73 pObj = Gia_ManCo( p, 0 );
74 Sim = Vec_WrdEntry( p->vSims, Gia_ObjId(p, pObj) );
75 Vec_IntClear( vPat2 );
76 for ( i = 1; i <= Gia_ManCiNum(p); i++ )
77 Vec_IntPush( vPat2, (int)((Sim & 1) ^ ((Sim >> i) & 1)) );
78 return (int)(Sim & 1);
79}
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachCiId
#define Gia_ManForEachCiId(p, Id, i)
Definition gia.h:1230
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Here is the caller graph for this function:

◆ Bmc_ComputeSimTest()

void Bmc_ComputeSimTest ( Gia_Man_t * p)

Definition at line 80 of file bmcClp.c.

81{
82 int i, v, w, Res, Bit, Bit2, nPats = 256;
83 int Count[2][64][64] = {{{0}}};
84 int PatCount[64][2][2] = {{{0}}};
85 int DiffCount[64] = {0};
86 Vec_Int_t * vPat = Vec_IntAlloc( Gia_ManCiNum(p) );
87 Vec_Int_t * vPat2 = Vec_IntAlloc( Gia_ManCiNum(p) );
88 Vec_WrdFreeP( &p->vSims );
89 p->vSims = Vec_WrdStart( Gia_ManObjNum(p) );
90 printf( "Number of patterns = %d.\n", nPats );
91 for ( i = 0; i < nPats; i++ )
92 {
93 Vec_IntClear( vPat );
94 for ( v = 0; v < Gia_ManCiNum(p); v++ )
95 Vec_IntPush( vPat, rand() & 1 );
96
97// Vec_IntForEachEntry( vPat, Bit, v )
98// printf( "%d", Bit );
99// printf( " " );
100
101 Res = Bmc_ComputeSimDiff( p, vPat, vPat2 );
102// printf( "%d ", Res );
103
104// Vec_IntForEachEntry( vPat2, Bit, v )
105// printf( "%d", Bit );
106// printf( "\n" );
107
108 Vec_IntForEachEntry( vPat, Bit, v )
109 PatCount[v][Res][Bit]++;
110
111 Vec_IntForEachEntry( vPat2, Bit, v )
112 {
113 if ( Bit )
114 DiffCount[v]++;
115 Vec_IntForEachEntryStart( vPat2, Bit2, w, v + 1 )
116 if ( Bit && Bit2 )
117 Count[Res][v][w]++;
118 }
119 }
120 Vec_IntFree( vPat );
121 Vec_IntFree( vPat2 );
122 Vec_WrdFreeP( &p->vSims );
123
124
125 printf( "\n" );
126 printf( " " );
127 for ( v = 0; v < Gia_ManCiNum(p); v++ )
128 printf( "%3c ", 'a'+v );
129 printf( "\n" );
130
131 printf( "Off0 " );
132 for ( v = 0; v < Gia_ManCiNum(p); v++ )
133 printf( "%3d ", PatCount[v][0][0] );
134 printf( "\n" );
135
136 printf( "Off1 " );
137 for ( v = 0; v < Gia_ManCiNum(p); v++ )
138 printf( "%3d ", PatCount[v][0][1] );
139 printf( "\n" );
140
141 printf( "On0 " );
142 for ( v = 0; v < Gia_ManCiNum(p); v++ )
143 printf( "%3d ", PatCount[v][1][0] );
144 printf( "\n" );
145
146 printf( "On1 " );
147 for ( v = 0; v < Gia_ManCiNum(p); v++ )
148 printf( "%3d ", PatCount[v][1][1] );
149 printf( "\n" );
150 printf( "\n" );
151
152 printf( "Diff " );
153 for ( v = 0; v < Gia_ManCiNum(p); v++ )
154 printf( "%3d ", DiffCount[v] );
155 printf( "\n" );
156 printf( "\n" );
157
158 for ( i = 0; i < 2; i++ )
159 {
160 printf( " " );
161 for ( v = 0; v < Gia_ManCiNum(p); v++ )
162 printf( "%3c ", 'a'+v );
163 printf( "\n" );
164
165 for ( v = 0; v < Gia_ManCiNum(p); v++ )
166 {
167 printf( " %c ", 'a'+v );
168 for ( w = 0; w < Gia_ManCiNum(p); w++ )
169 {
170 if ( Count[i][v][w] )
171 printf( "%3d ", Count[i][v][w] );
172 else
173 printf( " . " );
174 }
175 printf( "\n" );
176 }
177 printf( "\n" );
178 }
179}
Bmc_ComputeSimDiff
ABC_NAMESPACE_IMPL_START int Bmc_ComputeSimDiff(Gia_Man_t *p, Vec_Int_t *vPat, Vec_Int_t *vPat2)
DECLARATIONS ///.
Definition bmcClp.c:48
for
for(p=first;p->value< newval;p=p->next)
Here is the call graph for this function: