ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Functions
giaSupp.c File Reference
#include "gia.h"
#include "sat/satoko/satoko.h"
Include dependency graph for giaSupp.c:

Go to the source code of this file.

Classes

struct  Gia_Man2Min_t_
 

Functions

ABC_NAMESPACE_IMPL_START Gia_ManMin_t * Gia_ManSuppStart (Gia_Man_t *pGia)
 DECLARATIONS ///.
 
int Gia_ManSupportAnd (Gia_ManMin_t *p, int iLit0, int iLit1)
 
void Gia_ManSuppStop (Gia_ManMin_t *p)
 
Gia_Man_t * Gia_ManSupportAndTest (Gia_Man_t *pGia)
 
Gia_Man2Min_t * Gia_Man2SuppStart (Gia_Man_t *pGia)
 
void Gia_Man2SuppStop (Gia_Man2Min_t *p)
 
void Gia_Min2AddClausesMux (Gia_Man_t *p, Gia_Obj_t *pNode, satoko_t *pSat)
 
void Gia_Min2AddClausesSuper (Gia_Man_t *p, Gia_Obj_t *pNode, Vec_Ptr_t *vSuper, satoko_t *pSat)
 
void Gia_Min2CollectSuper_rec (Gia_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
 
void Gia_Min2CollectSuper (Gia_Obj_t *pObj, int fUseMuxes, Vec_Ptr_t *vSuper)
 
void Gia_Min2ObjAddToFrontier (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Ptr_t *vFrontier, satoko_t *pSat, Vec_Int_t *vSatVars)
 
int Gia_Min2ObjGetCnfVar (Gia_Man2Min_t *p, int iObj)
 
int Gia_Min2ManSimulate (Gia_Man2Min_t *p)
 
int Gia_Min2ManSolve (Gia_Man2Min_t *p)
 
int Gia_Min2ManGatherSupp (Gia_Man2Min_t *p)
 
int Gia_Man2SupportAnd (Gia_Man2Min_t *p, int iLit0, int iLit1)
 
Gia_Man_t * Gia_Man2SupportAndTest (Gia_Man_t *pGia)
 

Function Documentation

◆ Gia_Man2SupportAnd()

int Gia_Man2SupportAnd ( Gia_Man2Min_t * p,
int iLit0,
int iLit1 )

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

Synopsis [Takes a literal and returns a support-minized literal.]

Description []

SideEffects []

SeeAlso []

Definition at line 815 of file giaSupp.c.

816{
817 p->nCalls++;
818 //return Gia_ManHashAnd( p->pGia, iLit0, iLit1 );
819 p->iLits[0] = iLit0;
820 p->iLits[1] = iLit1;
821 if ( iLit0 < 2 || iLit1 < 2 || Abc_Lit2Var(iLit0) == Abc_Lit2Var(iLit1) || Gia_ManHashLookupInt(p->pGia, iLit0, iLit1) ||
822 !Gia_Min2ManGatherSupp(p) || !Gia_Min2ManSimulate(p) || !Gia_Min2ManSolve(p) )
823 return Gia_ManHashAnd( p->pGia, iLit0, iLit1 );
824 //printf( "%d %d\n", iLit0, iLit1 );
825 p->nSatUnsat++;
826 return 0;
827}
p
Cube * p
Definition exorList.c:222
Gia_Min2ManSimulate
int Gia_Min2ManSimulate(Gia_Man2Min_t *p)
Definition giaSupp.c:671
Gia_Min2ManGatherSupp
int Gia_Min2ManGatherSupp(Gia_Man2Min_t *p)
Definition giaSupp.c:788
Gia_Min2ManSolve
int Gia_Min2ManSolve(Gia_Man2Min_t *p)
Definition giaSupp.c:717
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
Gia_ManHashLookupInt
int Gia_ManHashLookupInt(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:81
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_Man2SupportAndTest()

Gia_Man_t * Gia_Man2SupportAndTest ( Gia_Man_t * pGia)

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

Synopsis [Testbench.]

Description []

SideEffects []

SeeAlso []

Definition at line 840 of file giaSupp.c.

841{
842 Gia_Man2Min_t * pMan;
843 Gia_Man_t * pNew, * pTemp;
844 Gia_Obj_t * pObj;
845 int i;
846 Gia_ManRandomW( 1 );
847 Gia_ManFillValue( pGia );
848 pNew = Gia_ManStart( Gia_ManObjNum(pGia) );
849 pNew->pName = Abc_UtilStrsav( pGia->pName );
850 pNew->pSpec = Abc_UtilStrsav( pGia->pSpec );
851 Gia_ManHashAlloc( pNew );
852 Gia_ManConst0(pGia)->Value = 0;
853 pMan = Gia_Man2SuppStart( pNew );
854 Gia_ManForEachObj1( pGia, pObj, i )
855 {
856 if ( Gia_ObjIsAnd(pObj) )
857 {
858// pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
859 pObj->Value = Gia_Man2SupportAnd( pMan, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
860 }
861 else if ( Gia_ObjIsCi(pObj) )
862 pObj->Value = Gia_ManAppendCi( pNew );
863 else if ( Gia_ObjIsCo(pObj) )
864 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
865 else assert( 0 );
866
867 //if ( i % 10000 == 0 )
868 // printf( "%d\n", i );
869 }
870 Gia_Man2SuppStop( pMan );
871 Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia) );
872 pNew = Gia_ManCleanup( pTemp = pNew );
873 Gia_ManStop( pTemp );
874 return pNew;
875}
Gia_Man2SuppStart
Gia_Man2Min_t * Gia_Man2SuppStart(Gia_Man_t *pGia)
Definition giaSupp.c:375
Gia_Man2SuppStop
void Gia_Man2SuppStop(Gia_Man2Min_t *p)
Definition giaSupp.c:394
Gia_Man2SupportAnd
int Gia_Man2SupportAnd(Gia_Man2Min_t *p, int iLit0, int iLit1)
Definition giaSupp.c:815
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManRandomW
word Gia_ManRandomW(int fReset)
Definition giaUtil.c:67
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition giaUtil.c:369
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManForEachObj1
#define Gia_ManForEachObj1(p, pObj, i)
Definition gia.h:1192
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_Man2Min_t
struct Gia_Man2Min_t_ Gia_Man2Min_t
Definition gia.h:1669
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:

◆ Gia_Man2SuppStart()

Gia_Man2Min_t * Gia_Man2SuppStart ( Gia_Man_t * pGia)

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

Synopsis [Create/delete the data representation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 375 of file giaSupp.c.

376{
377 Gia_Man2Min_t * p;
378 p = ABC_CALLOC( Gia_Man2Min_t, 1 );
379 p->pGia = pGia;
380 p->vCis[0] = Vec_IntAlloc( 512 );
381 p->vCis[1] = Vec_IntAlloc( 512 );
382 p->vObjs[0] = Vec_IntAlloc( 512 );
383 p->vObjs[1] = Vec_IntAlloc( 512 );
384 // SAT solving
385 p->pSat = satoko_create();
386 p->vSims = Vec_WrdAlloc( 1000 );
387 p->vFrontier = Vec_PtrAlloc( 1000 );
388 p->vFanins = Vec_PtrAlloc( 100 );
389 p->vSatVars = Vec_IntAlloc( 100 );
390 p->iPattern = 1;
391 satoko_options(p->pSat)->learnt_ratio = 0; // prevent garbage collection
392 return p;
393}
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
satoko_create
satoko_t * satoko_create(void)
Definition solver_api.c:88
satoko_options
satoko_opts_t * satoko_options(satoko_t *)
Definition solver_api.c:438
satoko_opts::learnt_ratio
float learnt_ratio
Definition satoko.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_Man2SuppStop()

void Gia_Man2SuppStop ( Gia_Man2Min_t * p)

Definition at line 394 of file giaSupp.c.

395{
396// printf( "Total calls = %8d. Supps = %6d. Sims = %6d. SAT = %6d. UNSAT = %6d.\n",
397// p->nCalls, p->nSupps, p->nSims, p->nSatSat, p->nSatUnsat );
398 Vec_IntFreeP( &p->vCis[0] );
399 Vec_IntFreeP( &p->vCis[1] );
400 Vec_IntFreeP( &p->vObjs[0] );
401 Vec_IntFreeP( &p->vObjs[1] );
402 Gia_ManCleanMark01( p->pGia );
403 satoko_destroy( p->pSat );
404 Vec_WrdFreeP( &p->vSims );
405 Vec_PtrFreeP( &p->vFrontier );
406 Vec_PtrFreeP( &p->vFanins );
407 Vec_IntFreeP( &p->vSatVars );
408 ABC_FREE( p );
409}
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Gia_ManCleanMark01
void Gia_ManCleanMark01(Gia_Man_t *p)
Definition giaUtil.c:218
satoko_destroy
void satoko_destroy(satoko_t *)
Definition solver_api.c:132
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_ManSupportAnd()

int Gia_ManSupportAnd ( Gia_ManMin_t * p,
int iLit0,
int iLit1 )

Definition at line 280 of file giaSupp.c.

280{ return 0; }
Here is the caller graph for this function:

◆ Gia_ManSupportAndTest()

Gia_Man_t * Gia_ManSupportAndTest ( Gia_Man_t * pGia)

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

Synopsis [Testbench.]

Description []

SideEffects []

SeeAlso []

Definition at line 297 of file giaSupp.c.

298{
299 Gia_ManMin_t * pMan;
300 Gia_Man_t * pNew, * pTemp;
301 Gia_Obj_t * pObj;
302 int i;
303 Gia_ManFillValue( pGia );
304 pNew = Gia_ManStart( Gia_ManObjNum(pGia) );
305 pNew->pName = Abc_UtilStrsav( pGia->pName );
306 pNew->pSpec = Abc_UtilStrsav( pGia->pSpec );
307 Gia_ManHashAlloc( pNew );
308 Gia_ManConst0(pGia)->Value = 0;
309 pMan = Gia_ManSuppStart( pNew );
310 Gia_ManForEachObj1( pGia, pObj, i )
311 {
312 if ( Gia_ObjIsAnd(pObj) )
313 {
314// pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
315 pObj->Value = Gia_ManSupportAnd( pMan, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
316 }
317 else if ( Gia_ObjIsCi(pObj) )
318 pObj->Value = Gia_ManAppendCi( pNew );
319 else if ( Gia_ObjIsCo(pObj) )
320 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
321 else assert( 0 );
322
323 if ( i % 10000 == 0 )
324 printf( "%d\n", i );
325 }
326 Gia_ManSuppStop( pMan );
327 Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia) );
328 pNew = Gia_ManCleanup( pTemp = pNew );
329 Gia_ManStop( pTemp );
330 return pNew;
331}
Gia_ManSupportAnd
int Gia_ManSupportAnd(Gia_ManMin_t *p, int iLit0, int iLit1)
Definition giaSupp.c:280
Gia_ManSuppStart
ABC_NAMESPACE_IMPL_START Gia_ManMin_t * Gia_ManSuppStart(Gia_Man_t *pGia)
DECLARATIONS ///.
Definition giaSupp.c:279
Gia_ManSuppStop
void Gia_ManSuppStop(Gia_ManMin_t *p)
Definition giaSupp.c:281
Gia_ManMin_t
struct Gia_ManMin_t_ Gia_ManMin_t
Definition gia.h:1665
Here is the call graph for this function:

◆ Gia_ManSuppStart()

ABC_NAMESPACE_IMPL_START Gia_ManMin_t * Gia_ManSuppStart ( Gia_Man_t * pGia)

DECLARATIONS ///.

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

FileName [giaSupp.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [Support minimization for AIGs.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

Definition at line 279 of file giaSupp.c.

279{ return NULL; }
Here is the caller graph for this function:

◆ Gia_ManSuppStop()

void Gia_ManSuppStop ( Gia_ManMin_t * p)

Definition at line 281 of file giaSupp.c.

281{}
Here is the caller graph for this function:

◆ Gia_Min2AddClausesMux()

void Gia_Min2AddClausesMux ( Gia_Man_t * p,
Gia_Obj_t * pNode,
satoko_t * pSat )

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

Synopsis [Adds clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 422 of file giaSupp.c.

423{
424 int fPolarFlip = 0;
425 Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
426 int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
427
428 assert( !Gia_IsComplement( pNode ) );
429 assert( pNode->fMark0 );
430 // get nodes (I = if, T = then, E = else)
431 pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
432 // get the variable numbers
433 VarF = Gia_Min2ObjSatId(p, pNode);
434 VarI = Gia_Min2ObjSatId(p, pNodeI);
435 VarT = Gia_Min2ObjSatId(p, Gia_Regular(pNodeT));
436 VarE = Gia_Min2ObjSatId(p, Gia_Regular(pNodeE));
437 // get the complementation flags
438 fCompT = Gia_IsComplement(pNodeT);
439 fCompE = Gia_IsComplement(pNodeE);
440
441 // f = ITE(i, t, e)
442
443 // i' + t' + f
444 // i' + t + f'
445 // i + e' + f
446 // i + e + f'
447
448 // create four clauses
449 pLits[0] = Abc_Var2Lit(VarI, 1);
450 pLits[1] = Abc_Var2Lit(VarT, 1^fCompT);
451 pLits[2] = Abc_Var2Lit(VarF, 0);
452 if ( fPolarFlip )
453 {
454 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
455 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
456 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
457 }
458 RetValue = satoko_add_clause( pSat, pLits, 3 );
459 assert( RetValue );
460 pLits[0] = Abc_Var2Lit(VarI, 1);
461 pLits[1] = Abc_Var2Lit(VarT, 0^fCompT);
462 pLits[2] = Abc_Var2Lit(VarF, 1);
463 if ( fPolarFlip )
464 {
465 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
466 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
467 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
468 }
469 RetValue = satoko_add_clause( pSat, pLits, 3 );
470 assert( RetValue );
471 pLits[0] = Abc_Var2Lit(VarI, 0);
472 pLits[1] = Abc_Var2Lit(VarE, 1^fCompE);
473 pLits[2] = Abc_Var2Lit(VarF, 0);
474 if ( fPolarFlip )
475 {
476 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
477 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
478 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
479 }
480 RetValue = satoko_add_clause( pSat, pLits, 3 );
481 assert( RetValue );
482 pLits[0] = Abc_Var2Lit(VarI, 0);
483 pLits[1] = Abc_Var2Lit(VarE, 0^fCompE);
484 pLits[2] = Abc_Var2Lit(VarF, 1);
485 if ( fPolarFlip )
486 {
487 if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
488 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
489 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
490 }
491 RetValue = satoko_add_clause( pSat, pLits, 3 );
492 assert( RetValue );
493
494 // two additional clauses
495 // t' & e' -> f'
496 // t & e -> f
497
498 // t + e + f'
499 // t' + e' + f
500
501 if ( VarT == VarE )
502 {
503// assert( fCompT == !fCompE );
504 return;
505 }
506
507 pLits[0] = Abc_Var2Lit(VarT, 0^fCompT);
508 pLits[1] = Abc_Var2Lit(VarE, 0^fCompE);
509 pLits[2] = Abc_Var2Lit(VarF, 1);
510 if ( fPolarFlip )
511 {
512 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
513 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
514 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
515 }
516 RetValue = satoko_add_clause( pSat, pLits, 3 );
517 assert( RetValue );
518 pLits[0] = Abc_Var2Lit(VarT, 1^fCompT);
519 pLits[1] = Abc_Var2Lit(VarE, 1^fCompE);
520 pLits[2] = Abc_Var2Lit(VarF, 0);
521 if ( fPolarFlip )
522 {
523 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
524 if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
525 if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
526 }
527 RetValue = satoko_add_clause( pSat, pLits, 3 );
528 assert( RetValue );
529}
Gia_ObjRecognizeMux
Gia_Obj_t * Gia_ObjRecognizeMux(Gia_Obj_t *pNode, Gia_Obj_t **ppNodeT, Gia_Obj_t **ppNodeE)
Definition giaUtil.c:1056
satoko_add_clause
int satoko_add_clause(satoko_t *, int *, int)
Definition solver_api.c:255
Gia_Obj_t_::fPhase
unsigned fPhase
Definition gia.h:87
Gia_Obj_t_::fMark0
unsigned fMark0
Definition gia.h:81
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_Min2AddClausesSuper()

void Gia_Min2AddClausesSuper ( Gia_Man_t * p,
Gia_Obj_t * pNode,
Vec_Ptr_t * vSuper,
satoko_t * pSat )

Definition at line 530 of file giaSupp.c.

531{
532 int fPolarFlip = 0;
533 Gia_Obj_t * pFanin;
534 int * pLits, nLits, RetValue, i;
535 assert( !Gia_IsComplement(pNode) );
536 assert( Gia_ObjIsAnd( pNode ) );
537 // create storage for literals
538 nLits = Vec_PtrSize(vSuper) + 1;
539 pLits = ABC_ALLOC( int, nLits );
540 // suppose AND-gate is A & B = C
541 // add !A => !C or A + !C
542 Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
543 {
544 pLits[0] = Abc_Var2Lit(Gia_Min2ObjSatId(p, Gia_Regular(pFanin)), Gia_IsComplement(pFanin));
545 pLits[1] = Abc_Var2Lit(Gia_Min2ObjSatId(p, pNode), 1);
546 if ( fPolarFlip )
547 {
548 if ( Gia_Regular(pFanin)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
549 if ( pNode->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
550 }
551 RetValue = satoko_add_clause( pSat, pLits, 2 );
552 assert( RetValue );
553 }
554 // add A & B => C or !A + !B + C
555 Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
556 {
557 pLits[i] = Abc_Var2Lit(Gia_Min2ObjSatId(p, Gia_Regular(pFanin)), !Gia_IsComplement(pFanin));
558 if ( fPolarFlip )
559 {
560 if ( Gia_Regular(pFanin)->fPhase ) pLits[i] = Abc_LitNot( pLits[i] );
561 }
562 }
563 pLits[nLits-1] = Abc_Var2Lit(Gia_Min2ObjSatId(p, pNode), 0);
564 if ( fPolarFlip )
565 {
566 if ( pNode->fPhase ) pLits[nLits-1] = Abc_LitNot( pLits[nLits-1] );
567 }
568 RetValue = satoko_add_clause( pSat, pLits, nLits );
569 assert( RetValue );
570 ABC_FREE( pLits );
571}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
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:

◆ Gia_Min2CollectSuper()

void Gia_Min2CollectSuper ( Gia_Obj_t * pObj,
int fUseMuxes,
Vec_Ptr_t * vSuper )

Definition at line 598 of file giaSupp.c.

599{
600 assert( !Gia_IsComplement(pObj) );
601 assert( !Gia_ObjIsCi(pObj) );
602 Vec_PtrClear( vSuper );
603 Gia_Min2CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
604}
Gia_Min2CollectSuper_rec
void Gia_Min2CollectSuper_rec(Gia_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Definition giaSupp.c:584
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_Min2CollectSuper_rec()

void Gia_Min2CollectSuper_rec ( Gia_Obj_t * pObj,
Vec_Ptr_t * vSuper,
int fFirst,
int fUseMuxes )

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

Synopsis [Adds clauses and returns CNF variable of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 584 of file giaSupp.c.

585{
586 // if the new node is complemented or a PI, another gate begins
587 if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) ||
588 (!fFirst && Gia_ObjValue(pObj) > 1) ||
589 (fUseMuxes && pObj->fMark0) )
590 {
591 Vec_PtrPushUnique( vSuper, pObj );
592 return;
593 }
594 // go through the branches
595 Gia_Min2CollectSuper_rec( Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes );
596 Gia_Min2CollectSuper_rec( Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes );
597}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_Min2ManGatherSupp()

int Gia_Min2ManGatherSupp ( Gia_Man2Min_t * p)

Definition at line 788 of file giaSupp.c.

789{
790 int n, Overlap = 0;
791 p->nSupps++;
792 Gia_ManIncrementTravId( p->pGia );
793 for ( n = 0; n < 2; n++ )
794 {
795 Vec_IntClear( p->vCis[n] );
796 Vec_IntClear( p->vObjs[n] );
797 Gia_ManIncrementTravId( p->pGia );
798 Overlap = Gia_Min2ManGatherSupp_rec( p->pGia, Abc_Lit2Var(p->iLits[n]), p->vCis[n], p->vObjs[n] );
799 assert( n || !Overlap );
800 }
801 return Overlap;
802}
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_Min2ManSimulate()

int Gia_Min2ManSimulate ( Gia_Man2Min_t * p)

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

Synopsis [Returns 0 if the node is not a constant.]

Description []

SideEffects []

SeeAlso []

Definition at line 671 of file giaSupp.c.

672{
673 word Sim0, Sim1; int n, i, iObj;
674 p->nSims++;
675 // add random values to new CIs
676 Vec_WrdFillExtra( p->vSims, Gia_ManObjNum(p->pGia), 0 );
677 for ( i = p->nCisOld; i < Gia_ManCiNum(p->pGia); i++ )
678 Vec_WrdWriteEntry( p->vSims, Gia_ManCiIdToId(p->pGia, i), Gia_ManRandomW( 0 ) << 1 );
679 p->nCisOld = Gia_ManCiNum(p->pGia);
680 // simulate internal nodes
681 for ( n = 0; n < 2; n++ )
682 Vec_IntForEachEntry( p->vObjs[n], iObj, i )
683 {
684 Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
685 Sim0 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId0p(p->pGia, pObj) );
686 Sim1 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId1p(p->pGia, pObj) );
687 Sim0 = Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0;
688 Sim1 = Gia_ObjFaninC1(pObj) ? ~Sim1 : Sim1;
689 Vec_WrdWriteEntry( p->vSims, iObj, Sim0 & Sim1 );
690 }
691 Sim0 = Vec_WrdEntry( p->vSims, Abc_Lit2Var(p->iLits[0]) );
692 Sim1 = Vec_WrdEntry( p->vSims, Abc_Lit2Var(p->iLits[1]) );
693 Sim0 = Abc_LitIsCompl(p->iLits[0]) ? ~Sim0 : Sim0;
694 Sim1 = Abc_LitIsCompl(p->iLits[1]) ? ~Sim1 : Sim1;
695// assert( (Sim0 & Sim1) != ~0 );
696 return (Sim0 & Sim1) == 0;
697}
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
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:

◆ Gia_Min2ManSolve()

int Gia_Min2ManSolve ( Gia_Man2Min_t * p)

Definition at line 717 of file giaSupp.c.

718{
719 int iObj0 = Abc_Lit2Var(p->iLits[0]);
720 int iObj1 = Abc_Lit2Var(p->iLits[1]);
721 int n, i, status, iVar0, iVar1, iTemp;
722 assert( iObj0 > 0 && iObj1 > 0 );
723// Vec_IntForEachEntry( &p->pGia->vCopies, iTemp, i )
724// assert( iTemp == -1 );
725 Vec_IntFillExtra( &p->pGia->vCopies, Gia_ManObjNum(p->pGia), -1 );
726 Vec_IntClear( p->vSatVars );
727 assert( satoko_varnum(p->pSat) == 0 );
728 iVar0 = Gia_Min2ObjGetCnfVar( p, iObj0 );
729 iVar1 = Gia_Min2ObjGetCnfVar( p, iObj1 );
730 satoko_assump_push( p->pSat, Abc_Var2Lit(iVar0, Abc_LitIsCompl(p->iLits[0])) );
731 satoko_assump_push( p->pSat, Abc_Var2Lit(iVar1, Abc_LitIsCompl(p->iLits[1])) );
732 status = satoko_solve( p->pSat );
733 satoko_assump_pop( p->pSat );
734 satoko_assump_pop( p->pSat );
735 if ( status == SATOKO_SAT )
736 {
737 //printf( "Disproved %d %d\n", p->iLits[0], p->iLits[1] );
738 assert( Gia_Min2ManSimulate(p) == 1 );
739 for ( n = 0; n < 2; n++ )
740 Vec_IntForEachEntry( p->vCis[n], iTemp, i )
741 Gia_Min2SimSetInputBit( p, iTemp, satoko_var_polarity(p->pSat, Gia_Min2ObjSatId(p->pGia, Gia_ManObj(p->pGia, iTemp))) == SATOKO_LIT_TRUE, p->iPattern );
742 //assert( Gia_Min2ManSimulate(p) == 0 );
743 p->iPattern = p->iPattern == 63 ? 1 : p->iPattern + 1;
744 p->nSatSat++;
745 }
746 //printf( "supp %d node %d vars %d\n",
747 // Vec_IntSize(p->vCis[0]) + Vec_IntSize(p->vCis[1]),
748 // Vec_IntSize(p->vObjs[0]) + Vec_IntSize(p->vObjs[1]),
749 // Vec_IntSize(p->vSatVars) );
750 satoko_rollback( p->pSat );
751 Vec_IntForEachEntry( p->vSatVars, iTemp, i )
752 Gia_Min2ObjCleanSatId( p->pGia, Gia_ManObj(p->pGia, iTemp) );
753 return status == SATOKO_UNSAT;
754}
Gia_Min2ObjGetCnfVar
int Gia_Min2ObjGetCnfVar(Gia_Man2Min_t *p, int iObj)
Definition giaSupp.c:617
satoko_solve
int satoko_solve(satoko_t *)
Definition solver_api.c:314
SATOKO_UNSAT
@ SATOKO_UNSAT
Definition satoko.h:25
SATOKO_SAT
@ SATOKO_SAT
Definition satoko.h:24
satoko_var_polarity
char satoko_var_polarity(satoko_t *, unsigned)
Definition solver_api.c:672
satoko_varnum
int satoko_varnum(satoko_t *)
Definition solver_api.c:625
SATOKO_LIT_TRUE
@ SATOKO_LIT_TRUE
Definition satoko.h:30
satoko_rollback
void satoko_rollback(satoko_t *)
Definition solver_api.c:508
satoko_assump_push
void satoko_assump_push(satoko_t *s, int)
Definition solver_api.c:298
satoko_assump_pop
void satoko_assump_pop(satoko_t *s)
Definition solver_api.c:306
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_Min2ObjAddToFrontier()

void Gia_Min2ObjAddToFrontier ( Gia_Man_t * p,
Gia_Obj_t * pObj,
Vec_Ptr_t * vFrontier,
satoko_t * pSat,
Vec_Int_t * vSatVars )

Definition at line 605 of file giaSupp.c.

606{
607 assert( !Gia_IsComplement(pObj) );
608 assert( !Gia_ObjIsConst0(pObj) );
609 if ( Gia_Min2ObjSatId(p, pObj) >= 0 )
610 return;
611 assert( Gia_Min2ObjSatId(p, pObj) == -1 );
612 Vec_IntPush( vSatVars, Gia_ObjId(p, pObj) );
613 Gia_Min2ObjSetSatId( p, pObj, satoko_add_variable(pSat, 0) );
614 if ( Gia_ObjIsAnd(pObj) )
615 Vec_PtrPush( vFrontier, pObj );
616}
satoko_add_variable
int satoko_add_variable(satoko_t *, char)
Definition solver_api.c:237
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_Min2ObjGetCnfVar()

int Gia_Min2ObjGetCnfVar ( Gia_Man2Min_t * p,
int iObj )

Definition at line 617 of file giaSupp.c.

618{
619 Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
620 Gia_Obj_t * pNode, * pFanin;
621 int i, k, fUseMuxes = 1;
622 if ( Gia_Min2ObjSatId(p->pGia, pObj) >= 0 )
623 return Gia_Min2ObjSatId(p->pGia, pObj);
624 if ( Gia_ObjIsCi(pObj) )
625 {
626 Vec_IntPush( p->vSatVars, iObj );
627 return Gia_Min2ObjSetSatId( p->pGia, pObj, satoko_add_variable(p->pSat, 0) );
628 }
629 assert( Gia_ObjIsAnd(pObj) );
630 // start the frontier
631 Vec_PtrClear( p->vFrontier );
632 Gia_Min2ObjAddToFrontier( p->pGia, pObj, p->vFrontier, p->pSat, p->vSatVars );
633 // explore nodes in the frontier
634 Vec_PtrForEachEntry( Gia_Obj_t *, p->vFrontier, pNode, i )
635 {
636 assert( Gia_Min2ObjSatId(p->pGia,pNode) >= 0 );
637 if ( fUseMuxes && pNode->fMark0 )
638 {
639 Vec_PtrClear( p->vFanins );
640 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin0(pNode) ) );
641 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) );
642 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) );
643 Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) );
644 Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
645 Gia_Min2ObjAddToFrontier( p->pGia, Gia_Regular(pFanin), p->vFrontier, p->pSat, p->vSatVars );
646 Gia_Min2AddClausesMux( p->pGia, pNode, p->pSat );
647 }
648 else
649 {
650 Gia_Min2CollectSuper( pNode, fUseMuxes, p->vFanins );
651 Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
652 Gia_Min2ObjAddToFrontier( p->pGia, Gia_Regular(pFanin), p->vFrontier, p->pSat, p->vSatVars );
653 Gia_Min2AddClausesSuper( p->pGia, pNode, p->vFanins, p->pSat );
654 }
655 assert( Vec_PtrSize(p->vFanins) > 1 );
656 }
657 return Gia_Min2ObjSatId(p->pGia,pObj);
658}
Gia_Min2AddClausesSuper
void Gia_Min2AddClausesSuper(Gia_Man_t *p, Gia_Obj_t *pNode, Vec_Ptr_t *vSuper, satoko_t *pSat)
Definition giaSupp.c:530
Gia_Min2ObjAddToFrontier
void Gia_Min2ObjAddToFrontier(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Ptr_t *vFrontier, satoko_t *pSat, Vec_Int_t *vSatVars)
Definition giaSupp.c:605
Gia_Min2AddClausesMux
void Gia_Min2AddClausesMux(Gia_Man_t *p, Gia_Obj_t *pNode, satoko_t *pSat)
Definition giaSupp.c:422
Gia_Min2CollectSuper
void Gia_Min2CollectSuper(Gia_Obj_t *pObj, int fUseMuxes, Vec_Ptr_t *vSuper)
Definition giaSupp.c:598
Here is the call graph for this function:
Here is the caller graph for this function: