summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaPat2.c1273
-rw-r--r--src/aig/gia/giaSimBase.c100
-rw-r--r--src/aig/gia/module.make1
4 files changed, 1376 insertions, 0 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 66ac9e13..fb924ce5 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -622,6 +622,8 @@ static inline void Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * p
static inline void Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1; }
static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds); }
static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1); }
+static inline int Gia_ObjUpdateTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { if ( Gia_ObjIsTravIdCurrent(p, pObj) ) return 1; Gia_ObjSetTravIdCurrent(p, pObj); return 0; }
+static inline int Gia_ObjUpdateTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { if ( Gia_ObjIsTravIdPrevious(p, pObj) ) return 1; Gia_ObjSetTravIdPrevious(p, pObj); return 0; }
static inline void Gia_ObjSetTravIdCurrentId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds; }
static inline void Gia_ObjSetTravIdPreviousId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds - 1; }
static inline int Gia_ObjIsTravIdCurrentId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds); }
diff --git a/src/aig/gia/giaPat2.c b/src/aig/gia/giaPat2.c
new file mode 100644
index 00000000..3151ed22
--- /dev/null
+++ b/src/aig/gia/giaPat2.c
@@ -0,0 +1,1273 @@
+/**CFile****************************************************************
+
+ FileName [giaPat2.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Scalable AIG package.]
+
+ Synopsis [Pattern generation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: giaPat2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "misc/vec/vecHsh.h"
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satStore.h"
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Min_Man_t_ Min_Man_t;
+struct Min_Man_t_
+{
+ int nCis;
+ int nCos;
+ int FirstAndLit;
+ int FirstCoLit;
+ Vec_Int_t vFans;
+ Vec_Str_t vValsN;
+ Vec_Str_t vValsL;
+ Vec_Int_t vVis;
+ Vec_Int_t vPat;
+};
+
+static inline int Min_ManCiNum( Min_Man_t * p ) { return p->nCis; }
+static inline int Min_ManCoNum( Min_Man_t * p ) { return p->nCos; }
+static inline int Min_ManObjNum( Min_Man_t * p ) { return Vec_IntSize(&p->vFans) >> 1; }
+static inline int Min_ManAndNum( Min_Man_t * p ) { return Min_ManObjNum(p) - p->nCis - p->nCos - 1; }
+
+static inline int Min_ManCi( Min_Man_t * p, int i ) { return 1 + i; }
+static inline int Min_ManCo( Min_Man_t * p, int i ) { return Min_ManObjNum(p) - Min_ManCoNum(p) + i; }
+
+static inline int Min_ObjIsCi( Min_Man_t * p, int i ) { return i > 0 && i <= Min_ManCiNum(p); }
+static inline int Min_ObjIsNode( Min_Man_t * p, int i ) { return i > Min_ManCiNum(p) && i < Min_ManObjNum(p) - Min_ManCoNum(p); }
+static inline int Min_ObjIsAnd( Min_Man_t * p, int i ) { return Min_ObjIsNode(p, i) && Vec_IntEntry(&p->vFans, 2*i) < Vec_IntEntry(&p->vFans, 2*i+1); }
+static inline int Min_ObjIsXor( Min_Man_t * p, int i ) { return Min_ObjIsNode(p, i) && Vec_IntEntry(&p->vFans, 2*i) > Vec_IntEntry(&p->vFans, 2*i+1); }
+static inline int Min_ObjIsBuf( Min_Man_t * p, int i ) { return Min_ObjIsNode(p, i) && Vec_IntEntry(&p->vFans, 2*i) ==Vec_IntEntry(&p->vFans, 2*i+1); }
+static inline int Min_ObjIsCo( Min_Man_t * p, int i ) { return i >= Min_ManObjNum(p) - Min_ManCoNum(p) && i < Min_ManObjNum(p); }
+
+static inline int Min_ObjLit( Min_Man_t * p, int i, int n ) { return Vec_IntEntry(&p->vFans, i + i + n); }
+static inline int Min_ObjLit0( Min_Man_t * p, int i ) { return Vec_IntEntry(&p->vFans, i + i + 0); }
+static inline int Min_ObjLit1( Min_Man_t * p, int i ) { return Vec_IntEntry(&p->vFans, i + i + 1); }
+static inline int Min_ObjCioId( Min_Man_t * p, int i ) { assert( i && !Min_ObjIsNode(p, i) ); return Min_ObjLit1(p, i); }
+
+static inline int Min_ObjFan0( Min_Man_t * p, int i ) { return Abc_Lit2Var( Min_ObjLit0(p, i) ); }
+static inline int Min_ObjFan1( Min_Man_t * p, int i ) { return Abc_Lit2Var( Min_ObjLit1(p, i) ); }
+
+static inline int Min_ObjFanC0( Min_Man_t * p, int i ) { return Abc_LitIsCompl( Min_ObjLit0(p, i) ); }
+static inline int Min_ObjFanC1( Min_Man_t * p, int i ) { return Abc_LitIsCompl( Min_ObjLit1(p, i) ); }
+
+static inline char Min_ObjValN( Min_Man_t * p, int i ) { return Vec_StrEntry(&p->vValsN, i); }
+static inline void Min_ObjSetValN( Min_Man_t * p, int i, char v ){ Vec_StrWriteEntry(&p->vValsN, i, v); }
+
+static inline char Min_LitValL( Min_Man_t * p, int i ) { return Vec_StrEntry(&p->vValsL, i); }
+static inline void Min_LitSetValL( Min_Man_t * p, int i, char v ){ assert(v==0 || v==1); Vec_StrWriteEntry(&p->vValsL, i, v); Vec_StrWriteEntry(&p->vValsL, i^1, (char)!v); Vec_IntPush(&p->vVis, Abc_Lit2Var(i)); }
+static inline void Min_ObjCleanValL( Min_Man_t * p, int i ) { ((short *)Vec_StrArray(&p->vValsL))[i] = 0x0202; }
+static inline void Min_ObjMarkValL( Min_Man_t * p, int i ) { ((short *)Vec_StrArray(&p->vValsL))[i] |= 0x0404; }
+
+static inline int Min_LitIsCi( Min_Man_t * p, int v ) { return v > 1 && v < p->FirstAndLit; }
+static inline int Min_LitIsNode( Min_Man_t * p, int v ) { return v >= p->FirstAndLit && v < p->FirstCoLit; }
+static inline int Min_LitIsCo( Min_Man_t * p, int v ) { return v >= p->FirstCoLit; }
+
+static inline int Min_LitIsAnd( int v, int v0, int v1 ) { return Abc_LitIsCompl(v) ^ (v0 < v1); }
+static inline int Min_LitIsXor( int v, int v0, int v1 ) { return Abc_LitIsCompl(v) ^ (v0 > v1); }
+static inline int Min_LitIsBuf( int v, int v0, int v1 ) { return v0 == v1; }
+
+static inline int Min_LitFan( Min_Man_t * p, int v ) { return Vec_IntEntry(&p->vFans, v); }
+static inline int Min_LitFanC( Min_Man_t * p, int v ) { return Abc_LitIsCompl( Min_LitFan(p, v) ); }
+
+static inline void Min_ManStartValsN( Min_Man_t * p ) { Vec_StrGrow(&p->vValsN, Vec_IntCap(&p->vFans)/2); Vec_StrFill(&p->vValsN, Min_ManObjNum(p), 2); }
+static inline void Min_ManStartValsL( Min_Man_t * p ) { Vec_StrGrow(&p->vValsL, Vec_IntCap(&p->vFans)); Vec_StrFill(&p->vValsL, Vec_IntSize(&p->vFans), 2); }
+static inline int Min_ManCheckCleanValsL( Min_Man_t * p ) { int i; char c; Vec_StrForEachEntry( &p->vValsL, c, i ) if ( c != 2 ) return 0; return 1; }
+static inline void Min_ManCleanVisitedValL( Min_Man_t * p ) { int i, iObj; Vec_IntForEachEntry(&p->vVis, iObj, i) Min_ObjCleanValL(p, iObj); Vec_IntClear(&p->vVis); }
+
+
+#define Min_ManForEachObj( p, i ) \
+ for ( i = 0; i < Min_ManObjNum(p); i++ )
+#define Min_ManForEachCi( p, i ) \
+ for ( i = 1; i <= Min_ManCiNum(p); i++ )
+#define Min_ManForEachCo( p, i ) \
+ for ( i = Min_ManObjNum(p) - Min_ManCoNum(p); i < Min_ManObjNum(p); i++ )
+#define Min_ManForEachAnd( p, i ) \
+ for ( i = 1 + Min_ManCiNum(p); i < Min_ManObjNum(p) - Min_ManCoNum(p); i++ )
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Min_Man_t * Min_ManStart( int nObjMax )
+{
+ Min_Man_t * p = ABC_CALLOC( Min_Man_t, 1 );
+ Vec_IntGrow( &p->vFans, nObjMax );
+ Vec_IntPushTwo( &p->vFans, -1, -1 );
+ return p;
+}
+static inline void Min_ManStop( Min_Man_t * p )
+{
+ Vec_IntErase( &p->vFans );
+ Vec_StrErase( &p->vValsN );
+ Vec_StrErase( &p->vValsL );
+ Vec_IntErase( &p->vVis );
+ Vec_IntErase( &p->vPat );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Min_ManAppendObj( Min_Man_t * p, int iLit0, int iLit1 )
+{
+ int iLit = Vec_IntSize(&p->vFans);
+ Vec_IntPushTwo( &p->vFans, iLit0, iLit1 );
+ return iLit;
+}
+static inline int Min_ManAppendCi( Min_Man_t * p )
+{
+ p->nCis++;
+ p->FirstAndLit = Vec_IntSize(&p->vFans) + 2;
+ return Min_ManAppendObj( p, 0, p->nCis-1 );
+}
+static inline int Min_ManAppendCo( Min_Man_t * p, int iLit0 )
+{
+ p->nCos++;
+ if ( p->FirstCoLit == 0 )
+ p->FirstCoLit = Vec_IntSize(&p->vFans);
+ return Min_ManAppendObj( p, iLit0, p->nCos-1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Min_ManFromGia_rec( Min_Man_t * pNew, Gia_Man_t * p, int iObj )
+{
+ Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
+ if ( ~pObj->Value )
+ return;
+ assert( Gia_ObjIsAnd(pObj) );
+ Min_ManFromGia_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj) );
+ Min_ManFromGia_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj) );
+ pObj->Value = Min_ManAppendObj( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+Min_Man_t * Min_ManFromGia( Gia_Man_t * p, Vec_Int_t * vOuts )
+{
+ Gia_Obj_t * pObj; int i;
+ Min_Man_t * pNew = Min_ManStart( Gia_ManObjNum(p) );
+ Gia_ManFillValue(p);
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachCi( p, pObj, i )
+ pObj->Value = Min_ManAppendCi( pNew );
+ if ( vOuts == NULL )
+ {
+ Gia_ManForEachAnd( p, pObj, i )
+ pObj->Value = Min_ManAppendObj( pNew, Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i) );
+ Gia_ManForEachCo( p, pObj, i )
+ pObj->Value = Min_ManAppendCo( pNew, Gia_ObjFaninLit0p(p, pObj) );
+ }
+ else
+ {
+ Gia_ManForEachCoVec( vOuts, p, pObj, i )
+ Min_ManFromGia_rec( pNew, p, Gia_ObjFaninId0p(p, pObj) );
+ Gia_ManForEachCoVec( vOuts, p, pObj, i )
+ Min_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ }
+ return pNew;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline char Min_XsimNot( char Val )
+{
+ if ( Val < 2 )
+ return Val ^ 1;
+ return 2;
+}
+static inline char Min_XsimXor( char Val0, char Val1 )
+{
+ if ( Val0 < 2 && Val1 < 2 )
+ return Val0 ^ Val1;
+ return 2;
+}
+static inline char Min_XsimAnd( char Val0, char Val1 )
+{
+ if ( Val0 == 0 || Val1 == 0 )
+ return 0;
+ if ( Val0 == 1 && Val1 == 1 )
+ return 1;
+ return 2;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char Min_LitVerify_rec( Min_Man_t * p, int iLit )
+{
+ char Val = Min_LitValL(p, iLit);
+ if ( Val == 2 && Min_LitIsNode(p, iLit) ) // unassigned
+ {
+ int iLit0 = Min_LitFan(p, iLit);
+ int iLit1 = Min_LitFan(p, iLit^1);
+ char Val0 = Min_LitVerify_rec( p, iLit0 );
+ char Val1 = Min_LitVerify_rec( p, iLit1 );
+ assert( Min_LitIsNode(p, iLit) ); // internal node
+ if ( Min_LitIsXor(iLit, iLit0, iLit1) )
+ Val = Min_XsimXor( Val0, Val1 );
+ else
+ Val = Min_XsimAnd( Val0, Val1 );
+ if ( Val < 2 )
+ {
+ Val ^= Abc_LitIsCompl(iLit);
+ Min_LitSetValL( p, iLit, Val );
+ }
+ }
+ return Val;
+}
+char Min_LitVerify( Min_Man_t * p, int iLit, Vec_Int_t * vLits )
+{
+ int i, Entry; char Res;
+ if ( iLit < 2 ) return 1;
+ assert( !Min_LitIsCo(p, iLit) );
+ //assert( Min_ManCheckCleanValsL(p) );
+ assert( Vec_IntSize(&p->vVis) == 0 );
+ Vec_IntForEachEntry( vLits, Entry, i )
+ Min_LitSetValL( p, Entry, 1 ); // ms notation
+ Res = Min_LitVerify_rec( p, iLit );
+ Min_ManCleanVisitedValL( p );
+ return Res;
+}
+
+void Min_LitMinimize( Min_Man_t * p, int iLit, Vec_Int_t * vLits )
+{
+ int i, iObj, iTemp; char Res;
+ Vec_IntClear( &p->vPat );
+ if ( iLit < 2 ) return;
+ assert( !Min_LitIsCo(p, iLit) );
+ //assert( Min_ManCheckCleanValsL(p) );
+ assert( Vec_IntSize(&p->vVis) == 0 );
+ Vec_IntForEachEntry( vLits, iTemp, i )
+ Min_LitSetValL( p, iTemp, 1 ); // ms notation
+ Res = Min_LitVerify_rec( p, iLit );
+ assert( Res == 1 );
+ Min_ObjMarkValL( p, Abc_Lit2Var(iLit) );
+ Vec_IntForEachEntryReverse( &p->vVis, iObj, i )
+ {
+ int iLit = Abc_Var2Lit( iObj, 0 );
+ int Value = Min_LitValL(p, iLit);
+ if ( Value >= 4 )
+ {
+ if ( Min_LitIsCi(p, iLit) )
+ Vec_IntPush( &p->vPat, Abc_LitNotCond(iLit, !(Value&1)) );
+ else
+ {
+ int iLit0 = Min_LitFan(p, iLit);
+ int iLit1 = Min_LitFan(p, iLit^1);
+ char Val0 = Min_LitValL( p, iLit0 );
+ char Val1 = Min_LitValL( p, iLit1 );
+ if ( Value == 5 ) // value == 1
+ {
+ assert( (Val0&1) && (Val1&1) );
+ Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) );
+ Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) );
+ }
+ else // value == 0
+ {
+ int Zero0 = !(Val0&3);
+ int Zero1 = !(Val1&3);
+ assert( Zero0 || Zero1 );
+ if ( Zero0 && !Zero1 )
+ Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) );
+ else if ( !Zero0 && Zero1 )
+ Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) );
+ else if ( Val0 == 4 && Val1 != 4 )
+ Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) );
+ else if ( Val1 == 4 && Val1 != 4 )
+ Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) );
+ else if ( Abc_Random(0) & 1 )
+ Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) );
+ else
+ Min_ObjMarkValL( p, Abc_Lit2Var(iLit1) );
+ }
+ }
+ }
+ Min_ObjCleanValL( p, Abc_Lit2Var(iLit) );
+ }
+ Vec_IntClear( &p->vVis );
+ //Min_ManCleanVisitedValL( p );
+ //assert( Min_LitVerify(p, iLit, &p->vPat) == 1 );
+ assert( Vec_IntSize(&p->vPat) <= Vec_IntSize(vLits) );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline char Min_LitIsImplied1( Min_Man_t * p, int iLit )
+{
+ char Val = 2;
+ int iLit0 = Min_LitFan(p, iLit);
+ int iLit1 = Min_LitFan(p, iLit^1);
+ char Val0 = Min_LitValL(p, iLit0);
+ char Val1 = Min_LitValL(p, iLit1);
+ assert( Min_LitIsNode(p, iLit) ); // internal node
+ assert( Min_LitValL(p, iLit) == 2 ); // unassigned
+ if ( Min_LitIsXor(iLit, iLit0, iLit1) )
+ Val = Min_XsimXor( Val0, Val1 );
+ else
+ Val = Min_XsimAnd( Val0, Val1 );
+ if ( Val < 2 )
+ {
+ Val ^= Abc_LitIsCompl(iLit);
+ Min_LitSetValL( p, iLit, Val );
+ }
+ return Val;
+}
+static inline char Min_LitIsImplied2( Min_Man_t * p, int iLit )
+{
+ char Val = 2;
+ int iLit0 = Min_LitFan(p, iLit);
+ int iLit1 = Min_LitFan(p, iLit^1);
+ char Val0 = Min_LitValL(p, iLit0);
+ char Val1 = Min_LitValL(p, iLit1);
+ assert( Min_LitIsNode(p, iLit) ); // internal node
+ assert( Min_LitValL(p, iLit) == 2 ); // unassigned
+ if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
+ Val0 = Min_LitIsImplied1(p, iLit0);
+ if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
+ Val1 = Min_LitIsImplied1(p, iLit1);
+ if ( Min_LitIsXor(iLit, iLit0, iLit1) )
+ Val = Min_XsimXor( Val0, Val1 );
+ else
+ Val = Min_XsimAnd( Val0, Val1 );
+ if ( Val < 2 )
+ {
+ Val ^= Abc_LitIsCompl(iLit);
+ Min_LitSetValL( p, iLit, Val );
+ }
+ return Val;
+}
+static inline char Min_LitIsImplied3( Min_Man_t * p, int iLit )
+{
+ char Val = 2;
+ int iLit0 = Min_LitFan(p, iLit);
+ int iLit1 = Min_LitFan(p, iLit^1);
+ char Val0 = Min_LitValL(p, iLit0);
+ char Val1 = Min_LitValL(p, iLit1);
+ assert( Min_LitIsNode(p, iLit) ); // internal node
+ assert( Min_LitValL(p, iLit) == 2 ); // unassigned
+ if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
+ Val0 = Min_LitIsImplied2(p, iLit0);
+ if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
+ Val1 = Min_LitIsImplied2(p, iLit1);
+ if ( Min_LitIsXor(iLit, iLit0, iLit1) )
+ Val = Min_XsimXor( Val0, Val1 );
+ else
+ Val = Min_XsimAnd( Val0, Val1 );
+ if ( Val < 2 )
+ {
+ Val ^= Abc_LitIsCompl(iLit);
+ Min_LitSetValL( p, iLit, Val );
+ }
+ return Val;
+}
+static inline char Min_LitIsImplied4( Min_Man_t * p, int iLit )
+{
+ char Val = 2;
+ int iLit0 = Min_LitFan(p, iLit);
+ int iLit1 = Min_LitFan(p, iLit^1);
+ char Val0 = Min_LitValL(p, iLit0);
+ char Val1 = Min_LitValL(p, iLit1);
+ assert( Min_LitIsNode(p, iLit) ); // internal node
+ assert( Min_LitValL(p, iLit) == 2 ); // unassigned
+ if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
+ Val0 = Min_LitIsImplied3(p, iLit0);
+ if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
+ Val1 = Min_LitIsImplied3(p, iLit1);
+ if ( Min_LitIsXor(iLit, iLit0, iLit1) )
+ Val = Min_XsimXor( Val0, Val1 );
+ else
+ Val = Min_XsimAnd( Val0, Val1 );
+ if ( Val < 2 )
+ {
+ Val ^= Abc_LitIsCompl(iLit);
+ Min_LitSetValL( p, iLit, Val );
+ }
+ return Val;
+}
+static inline char Min_LitIsImplied5( Min_Man_t * p, int iLit )
+{
+ char Val = 2;
+ int iLit0 = Min_LitFan(p, iLit);
+ int iLit1 = Min_LitFan(p, iLit^1);
+ char Val0 = Min_LitValL(p, iLit0);
+ char Val1 = Min_LitValL(p, iLit1);
+ assert( Min_LitIsNode(p, iLit) ); // internal node
+ assert( Min_LitValL(p, iLit) == 2 ); // unassigned
+ if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
+ Val0 = Min_LitIsImplied4(p, iLit0);
+ if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
+ Val1 = Min_LitIsImplied4(p, iLit1);
+ if ( Min_LitIsXor(iLit, iLit0, iLit1) )
+ Val = Min_XsimXor( Val0, Val1 );
+ else
+ Val = Min_XsimAnd( Val0, Val1 );
+ if ( Val < 2 )
+ {
+ Val ^= Abc_LitIsCompl(iLit);
+ Min_LitSetValL( p, iLit, Val );
+ }
+ return Val;
+}
+
+// this recursive procedure is about 10% slower
+char Min_LitIsImplied_rec( Min_Man_t * p, int iLit, int Depth )
+{
+ char Val = 2;
+ int iLit0 = Min_LitFan(p, iLit);
+ int iLit1 = Min_LitFan(p, iLit^1);
+ char Val0 = Min_LitValL(p, iLit0);
+ char Val1 = Min_LitValL(p, iLit1);
+ assert( Depth > 0 );
+ assert( Min_LitIsNode(p, iLit) ); // internal node
+ assert( Min_LitValL(p, iLit) == 2 ); // unassigned
+ if ( Depth > 1 && Val0 == 2 && Min_LitIsNode(p, iLit0) )
+ {
+ Val0 = Min_LitIsImplied_rec(p, iLit0, Depth-1);
+ Val1 = Min_LitValL(p, iLit1);
+ }
+ if ( Depth > 1 && Val1 == 2 && Min_LitIsNode(p, iLit1) )
+ {
+ Val1 = Min_LitIsImplied_rec(p, iLit1, Depth-1);
+ Val0 = Min_LitValL(p, iLit0);
+ }
+ if ( Min_LitIsXor(iLit, iLit0, iLit1) )
+ Val = Min_XsimXor( Val0, Val1 );
+ else
+ Val = Min_XsimAnd( Val0, Val1 );
+ if ( Val < 2 )
+ {
+ Val ^= Abc_LitIsCompl(iLit);
+ Min_LitSetValL( p, iLit, Val );
+ }
+ return Val;
+}
+int Min_LitJustify_rec( Min_Man_t * p, int iLit )
+{
+ int Res = 1, LitValue = !Abc_LitIsCompl(iLit);
+ int Val = (int)Min_LitValL(p, iLit);
+ if ( Val < 2 ) // assigned
+ return Val == LitValue;
+ // unassigned
+ if ( Min_LitIsCi(p, iLit) )
+ Vec_IntPush( &p->vPat, iLit ); // ms notation
+ else
+ {
+ int iLit0 = Min_LitFan(p, iLit);
+ int iLit1 = Min_LitFan(p, iLit^1);
+ char Val0 = Min_LitValL(p, iLit0);
+ char Val1 = Min_LitValL(p, iLit1);
+ if ( Min_LitIsXor(iLit, iLit0, iLit1) )
+ {
+ if ( Val0 < 2 && Val1 < 2 )
+ Res = LitValue == (Val0 ^ Val1);
+ else if ( Val0 < 2 )
+ Res = Min_LitJustify_rec(p, iLit1^Val0^!LitValue);
+ else if ( Val1 < 2 )
+ Res = Min_LitJustify_rec(p, iLit0^Val1^!LitValue);
+ else if ( Abc_Random(0) & 1 )
+ Res = Min_LitJustify_rec(p, iLit0) && Min_LitJustify_rec(p, iLit1^ LitValue);
+ else
+ Res = Min_LitJustify_rec(p, iLit0^1) && Min_LitJustify_rec(p, iLit1^!LitValue);
+ assert( !Res || LitValue == Min_XsimXor(Min_LitValL(p, iLit0), Min_LitValL(p, iLit1)) );
+ }
+ else if ( LitValue ) // value 1
+ {
+ if ( Val0 == 0 || Val1 == 0 )
+ Res = 0;
+ else if ( Val0 == 1 && Val1 == 1 )
+ Res = 1;
+ else if ( Val0 == 1 )
+ Res = Min_LitJustify_rec(p, iLit1);
+ else if ( Val1 == 1 )
+ Res = Min_LitJustify_rec(p, iLit0);
+ else
+ Res = Min_LitJustify_rec(p, iLit0) && Min_LitJustify_rec(p, iLit1);
+ assert( !Res || 1 == Min_XsimAnd(Min_LitValL(p, iLit0), Min_LitValL(p, iLit1)) );
+ }
+ else // value 0
+ {
+/*
+ int Depth = 3;
+ if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
+ {
+ Val0 = Min_LitIsImplied_rec(p, iLit0, Depth);
+ Val1 = Min_LitValL(p, iLit1);
+ }
+ if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
+ {
+ Val1 = Min_LitIsImplied_rec(p, iLit1, Depth);
+ Val0 = Min_LitValL(p, iLit0);
+ }
+*/
+ if ( Val0 == 2 && Min_LitIsNode(p, iLit0) )
+ {
+ Val0 = Min_LitIsImplied3(p, iLit0);
+ Val1 = Min_LitValL(p, iLit1);
+ }
+ if ( Val1 == 2 && Min_LitIsNode(p, iLit1) )
+ {
+ Val1 = Min_LitIsImplied3(p, iLit1);
+ Val0 = Min_LitValL(p, iLit0);
+ }
+ if ( Val0 == 0 || Val1 == 0 )
+ Res = 1;
+ else if ( Val0 == 1 && Val1 == 1 )
+ Res = 0;
+ else if ( Val0 == 1 )
+ Res = Min_LitJustify_rec(p, iLit1^1);
+ else if ( Val1 == 1 )
+ Res = Min_LitJustify_rec(p, iLit0^1);
+ else if ( Abc_Random(0) & 1 )
+ //else if ( (p->Random >> (iLit & 0x1F)) & 1 )
+ Res = Min_LitJustify_rec(p, iLit0^1);
+ else
+ Res = Min_LitJustify_rec(p, iLit1^1);
+ //Val0 = Min_LitValL(p, iLit0);
+ //Val1 = Min_LitValL(p, iLit1);
+ assert( !Res || 0 == Min_XsimAnd(Min_LitValL(p, iLit0), Min_LitValL(p, iLit1)) );
+ }
+ }
+ if ( Res )
+ Min_LitSetValL( p, iLit, 1 );
+ return Res;
+}
+int Min_LitJustify( Min_Man_t * p, int iLit )
+{
+ int Res, fCheck = 1;
+ Vec_IntClear( &p->vPat );
+ if ( iLit < 2 ) return 1;
+ assert( !Min_LitIsCo(p, iLit) );
+ //assert( Min_ManCheckCleanValsL(p) );
+ assert( Vec_IntSize(&p->vVis) == 0 );
+ //p->Random = Abc_Random(0);
+ Res = Min_LitJustify_rec( p, iLit );
+ Min_ManCleanVisitedValL( p );
+ if ( Res )
+ {
+ Vec_IntSort( &p->vPat, 0 );
+ if ( fCheck && Min_LitVerify(p, iLit, &p->vPat) != 1 )
+ printf( "Verification FAILED for literal %d.\n", iLit );
+ //else
+ // printf( "Verification succeeded for literal %d.\n", iLit );
+ }
+ //else
+ // printf( "Could not justify literal %d.\n", iLit );
+ return Res;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Min_TargGenerateCexes( Min_Man_t * p, Vec_Int_t * vCoErrs, int nCexes, int nCexesStop, int * pnComputed, int fVerbose )
+{
+ abctime clk = Abc_Clock();
+ int t, iObj, Count = 0, CountPos = 0, CountPosSat = 0, nRuns[2] = {0}, nCountCexes[2] = {0};
+ Vec_Int_t * vPats = Vec_IntAlloc( 1000 );
+ Vec_Int_t * vPatBest = Vec_IntAlloc( Min_ManCiNum(p) );
+ Hsh_VecMan_t * pHash = Hsh_VecManStart( 10000 );
+ Min_ManForEachCo( p, iObj ) if ( Min_ObjLit0(p, iObj) > 1 )
+ {
+ int nCexesGenSim0 = 0;
+ int nCexesGenSim = 0;
+ int nCexesGenSat = 0;
+ if ( vCoErrs && Vec_IntEntry(vCoErrs, Min_ObjCioId(p, iObj)) >= nCexesStop )
+ continue;
+ //printf( "%d ", i );
+ for ( t = 0; t < nCexes; t++ )
+ {
+ nRuns[0]++;
+ if ( Min_LitJustify( p, Min_ObjLit0(p, iObj) ) )
+ {
+ int Before, After;
+ assert( Vec_IntSize(&p->vPat) > 0 );
+ //printf( "%d ", Vec_IntSize(vPat) );
+ Vec_IntClear( vPatBest );
+ if ( 1 ) // no minimization
+ Vec_IntAppend( vPatBest, &p->vPat );
+ else
+ {
+/*
+ for ( k = 0; k < 10; k++ )
+ {
+ Vec_IntClear( vPat2 );
+ Gia_ManIncrementTravId( p );
+ Cexes_MinimizePattern_rec( p, Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), vPat2 );
+ assert( Vec_IntSize(vPat2) <= Vec_IntSize(vPat) );
+ if ( Vec_IntSize(vPatBest) == 0 || Vec_IntSize(vPatBest) > Vec_IntSize(vPat2) )
+ {
+ Vec_IntClear( vPatBest );
+ Vec_IntAppend( vPatBest, vPat2 );
+ }
+ //printf( "%d ", Vec_IntSize(vPat2) );
+ }
+*/
+ }
+
+ //Gia_CexVerify( p, Gia_ObjFaninId0p(p, pObj), !Gia_ObjFaninC0(pObj), vPatBest );
+ //printf( "\n" );
+ Before = Hsh_VecSize( pHash );
+ Vec_IntSort( vPatBest, 0 );
+ Hsh_VecManAdd( pHash, vPatBest );
+ After = Hsh_VecSize( pHash );
+ if ( Before != After )
+ {
+ Vec_IntPush( vPats, Min_ObjCioId(p, iObj) );
+ Vec_IntPush( vPats, Vec_IntSize(vPatBest) );
+ Vec_IntAppend( vPats, vPatBest );
+ nCexesGenSim++;
+ }
+ nCexesGenSim0++;
+ if ( nCexesGenSim0 > nCexesGenSim*10 )
+ {
+ printf( "**** Skipping output %d (out of %d)\n", Min_ObjCioId(p, iObj), Min_ManCoNum(p) );
+ break;
+ }
+ }
+ if ( nCexesGenSim == nCexesStop )
+ break;
+ }
+ //printf( "(%d %d) ", nCexesGenSim0, nCexesGenSim );
+ //printf( "%d ", t/nCexesGenSim );
+
+ //printf( "The number of CEXes = %d\n", nCexesGen );
+ //if ( fVerbose )
+ // printf( "%d ", nCexesGen );
+ nCountCexes[0] += nCexesGenSim;
+ nCountCexes[1] += nCexesGenSat;
+ Count += nCexesGenSim + nCexesGenSat;
+ CountPos++;
+
+ if ( nCexesGenSim0 == 0 && t == nCexes )
+ printf( "#### Output %d (out of %d)\n", Min_ObjCioId(p, iObj), Min_ManCoNum(p) );
+ }
+ //printf( "\n" );
+ if ( fVerbose )
+ printf( "\n" );
+ if ( fVerbose )
+ printf( "Got %d unique CEXes using %d sim (%d) and %d SAT (%d) runs (ave size %.1f). PO = %d ErrPO = %d SatPO = %d ",
+ Count, nRuns[0], nCountCexes[0], nRuns[1], nCountCexes[1],
+ 1.0*Vec_IntSize(vPats)/Abc_MaxInt(1, Count)-2, Min_ManCoNum(p), CountPos, CountPosSat );
+ if ( fVerbose )
+ Abc_PrintTime( 0, "Time", Abc_Clock() - clk );
+ Hsh_VecManStop( pHash );
+ Vec_IntFree( vPatBest );
+ *pnComputed = Count;
+ return vPats;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Min_ManTest3( Gia_Man_t * p, Vec_Int_t * vCoErrs )
+{
+ int fXor = 0;
+ int nComputed;
+ Vec_Int_t * vPats;
+ Gia_Man_t * pXor = fXor ? Gia_ManDupMuxes(p, 1) : NULL;
+ Min_Man_t * pNew = Min_ManFromGia( fXor ? pXor : p, NULL );
+ Gia_ManStopP( &pXor );
+ Min_ManStartValsL( pNew );
+ //Vec_IntFill( vCoErrs, Vec_IntSize(vCoErrs), 0 );
+ //vPats = Min_TargGenerateCexes( pNew, vCoErrs, 10000, 10, &nComputed, 1 );
+ vPats = Min_TargGenerateCexes( pNew, vCoErrs, 10000, 10, &nComputed, 1 );
+ Vec_IntFree( vPats );
+ Min_ManStop( pNew );
+}
+void Min_ManTest4( Gia_Man_t * p )
+{
+ Vec_Int_t * vCoErrs = Vec_IntStartNatural( Gia_ManCoNum(p) );
+ Min_ManTest3(p, vCoErrs);
+ Vec_IntFree( vCoErrs );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManDupCones2CollectPis_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vMap )
+{
+ Gia_Obj_t * pObj;
+ if ( Gia_ObjUpdateTravIdCurrentId(p, iObj) )
+ return;
+ pObj = Gia_ManObj( p, iObj );
+ if ( Gia_ObjIsAnd(pObj) )
+ {
+ Gia_ManDupCones2CollectPis_rec( p, Gia_ObjFaninId0(pObj, iObj), vMap );
+ Gia_ManDupCones2CollectPis_rec( p, Gia_ObjFaninId1(pObj, iObj), vMap );
+ }
+ else if ( Gia_ObjIsCi(pObj) )
+ Vec_IntPush( vMap, iObj );
+ else assert( 0 );
+}
+void Gia_ManDupCones2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ if ( Gia_ObjIsCi(pObj) || Gia_ObjUpdateTravIdCurrent(p, pObj) )
+ return;
+ assert( Gia_ObjIsAnd(pObj) );
+ Gia_ManDupCones2_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManDupCones2_rec( pNew, p, Gia_ObjFanin1(pObj) );
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+Gia_Man_t * Gia_ManDupCones2( Gia_Man_t * p, int * pOuts, int nOuts, Vec_Int_t * vMap )
+{
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj; int i;
+ Vec_IntClear( vMap );
+ Gia_ManIncrementTravId( p );
+ for ( i = 0; i < nOuts; i++ )
+ Gia_ManDupCones2CollectPis_rec( p, Gia_ManCoDriverId(p, pOuts[i]), vMap );
+ pNew = Gia_ManStart( 1000 );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachObjVec( vMap, p, pObj, i )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ Gia_ManIncrementTravId( p );
+ for ( i = 0; i < nOuts; i++ )
+ Gia_ManDupCones2_rec( pNew, p, Gia_ObjFanin0(Gia_ManCo(p, pOuts[i])) );
+ for ( i = 0; i < nOuts; i++ )
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p, pOuts[i])) );
+ return pNew;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Min_ManRemoveItem( Vec_Wec_t * vCexes, int iItem, int iFirst, int iLimit )
+{
+ Vec_Int_t * vLevel, * vLevel0 = Vec_WecEntry(vCexes, iItem); int i;
+ assert( iFirst <= iItem && iItem < iLimit );
+ Vec_WecForEachLevelReverseStartStop( vCexes, vLevel, i, iLimit, iFirst )
+ if ( Vec_IntSize(vLevel) > 0 )
+ break;
+ assert( iFirst <= i && iItem <= i );
+ Vec_IntClear( vLevel0 );
+ if ( iItem < i )
+ ABC_SWAP( Vec_Int_t, *vLevel0, *vLevel );
+ return -1;
+}
+int Min_ManAccumulate( Vec_Wec_t * vCexes, int iFirst, int iLimit, Vec_Int_t * vCex )
+{
+ Vec_Int_t * vLevel; int i, nCommon, nDiff = 0;
+ Vec_WecForEachLevelStartStop( vCexes, vLevel, i, iFirst, iLimit )
+ {
+ if ( Vec_IntSize(vLevel) == 0 )
+ {
+ Vec_IntAppend(vLevel, vCex);
+ return nDiff+1;
+ }
+ nCommon = Vec_IntTwoCountCommon( vLevel, vCex );
+ if ( nCommon == Vec_IntSize(vLevel) ) // ignore vCex
+ return nDiff;
+ if ( nCommon == Vec_IntSize(vCex) ) // remove vLevel
+ nDiff += Min_ManRemoveItem( vCexes, i, iFirst, iLimit );
+ }
+ assert( 0 );
+ return ABC_INFINITY;
+}
+int Min_ManCountSize( Vec_Wec_t * vCexes, int iFirst, int iLimit )
+{
+ Vec_Int_t * vLevel; int i, nTotal = 0;
+ Vec_WecForEachLevelStartStop( vCexes, vLevel, i, iFirst, iLimit )
+ nTotal += Vec_IntSize(vLevel) > 0;
+ return nTotal;
+}
+Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTries, int nMinCexes, Vec_Int_t * vStats[3], int fUseSim, int fUseSat, int fVerbose )
+{
+ Vec_Int_t * vOuts = vOuts0 ? vOuts0 : Vec_IntStartNatural( Gia_ManCoNum(p) );
+ Min_Man_t * pNew = Min_ManFromGia( p, vOuts );
+ Vec_Wec_t * vCexes = Vec_WecStart( Vec_IntSize(vOuts) * nMinCexes );
+ Vec_Int_t * vPatBest = Vec_IntAlloc( 100 );
+ Vec_Int_t * vLits = Vec_IntAlloc( 100 );
+ Gia_Obj_t * pObj; int i, iObj, nOuts = 0, nSimOuts = 0, nSatOuts = 0;
+ vStats[0] = Vec_IntAlloc( Vec_IntSize(vOuts) ); // total calls
+ vStats[1] = Vec_IntAlloc( Vec_IntSize(vOuts) ); // successful calls + SAT runs
+ vStats[2] = Vec_IntAlloc( Vec_IntSize(vOuts) ); // results
+ Min_ManStartValsL( pNew );
+ Min_ManForEachCo( pNew, iObj )
+ {
+ int nAllCalls = 0;
+ int nGoodCalls = 0;
+ int nCurrCexes = 0;
+ if ( fUseSim && Min_ObjLit0(pNew, iObj) >= 2 )
+ {
+ while ( nAllCalls++ < nMaxTries )
+ {
+ if ( Min_LitJustify( pNew, Min_ObjLit0(pNew, iObj) ) )
+ {
+ Vec_IntClearAppend( vLits, &pNew->vPat );
+ Vec_IntClearAppend( vPatBest, &pNew->vPat );
+ if ( 1 ) // minimization
+ {
+ //printf( "%d -> ", Vec_IntSize(vPatBest) );
+ for ( i = 0; i < 10; i++ )
+ {
+ Min_LitMinimize( pNew, Min_ObjLit0(pNew, iObj), vLits );
+ if ( Vec_IntSize(vPatBest) > Vec_IntSize(&pNew->vPat) )
+ Vec_IntClearAppend( vPatBest, &pNew->vPat );
+ }
+ //printf( "%d ", Vec_IntSize(vPatBest) );
+ }
+ assert( Vec_IntSize(vPatBest) > 0 );
+ nCurrCexes += Min_ManAccumulate( vCexes, nOuts*nMinCexes, (nOuts+1)*nMinCexes, vPatBest );
+ nGoodCalls++;
+ }
+ if ( nCurrCexes == nMinCexes || nGoodCalls > 10*nCurrCexes )
+ break;
+ }
+ nSimOuts++;
+ }
+ assert( nCurrCexes <= nMinCexes );
+ assert( nCurrCexes == Min_ManCountSize(vCexes, nOuts*nMinCexes, (nOuts+1)*nMinCexes) );
+ Vec_IntPush( vStats[0], nAllCalls );
+ Vec_IntPush( vStats[1], nGoodCalls );
+ Vec_IntPush( vStats[2], nCurrCexes );
+ nOuts++;
+ }
+ assert( Vec_IntSize(vOuts) == nOuts );
+ assert( Vec_IntSize(vOuts) == Vec_IntSize(vStats[0]) );
+ assert( Vec_IntSize(vOuts) == Vec_IntSize(vStats[1]) );
+ assert( Vec_IntSize(vOuts) == Vec_IntSize(vStats[2]) );
+
+ if ( fUseSat )
+ Gia_ManForEachCoVec( vOuts, p, pObj, i )
+ {
+ if ( Vec_IntEntry(vStats[2], i) >= nMinCexes || Vec_IntEntry(vStats[1], i) > 10*Vec_IntEntry(vStats[2], i) )
+ continue;
+ {
+ int iObj = Min_ManCo(pNew, i);
+ int Index = Gia_ObjCioId(pObj);
+ Vec_Int_t * vMap = Vec_IntAlloc( 100 );
+ Gia_Man_t * pCon = Gia_ManDupCones2( p, &Index, 1, vMap );
+ Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCon, 8, 0, 0, 0, 0 );
+ sat_solver* pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+ int Lit = Abc_Var2Lit( 1, 0 );
+ int status = sat_solver_addclause( pSat, &Lit, &Lit+1 );
+ int nAllCalls = 0;
+ int nCurrCexes = Vec_IntEntry(vStats[2], i);
+ //Gia_AigerWrite( pCon, "temp_miter.aig", 0, 0, 0 );
+ if ( status == l_True )
+ {
+ nSatOuts++;
+ //printf( "Running SAT for output %d\n", i );
+ if ( Min_ObjLit0(pNew, iObj) >= 2 )
+ {
+ while ( nAllCalls++ < 100 )
+ {
+ int v, iVar = pCnf->nVars - Gia_ManPiNum(pCon), nVars = Gia_ManPiNum(pCon);
+ sat_solver_randomize( pSat, iVar, nVars );
+ status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
+ assert( status == l_True );
+ Vec_IntClear( vLits );
+ for ( v = 0; v < nVars; v++ )
+ Vec_IntPush( vLits, Abc_Var2Lit(Vec_IntEntry(vMap, v), !sat_solver_var_value(pSat, iVar + v)) );
+ Min_LitMinimize( pNew, Min_ObjLit0(pNew, iObj), vLits );
+ Vec_IntClearAppend( vPatBest, &pNew->vPat );
+ if ( 1 ) // minimization
+ {
+ //printf( "%d -> ", Vec_IntSize(vPatBest) );
+ for ( v = 0; v < 20; v++ )
+ {
+ Min_LitMinimize( pNew, Min_ObjLit0(pNew, iObj), vLits );
+ if ( Vec_IntSize(vPatBest) > Vec_IntSize(&pNew->vPat) )
+ Vec_IntClearAppend( vPatBest, &pNew->vPat );
+ }
+ //printf( "%d ", Vec_IntSize(vPatBest) );
+ }
+ Vec_IntSort( vPatBest, 0 );
+ nCurrCexes += Min_ManAccumulate( vCexes, i*nMinCexes, (i+1)*nMinCexes, vPatBest );
+ if ( nCurrCexes == nMinCexes || nAllCalls > 10*nCurrCexes )
+ break;
+ }
+ }
+ }
+ Vec_IntWriteEntry( vStats[0], i, nAllCalls*nMaxTries );
+ Vec_IntWriteEntry( vStats[1], i, nAllCalls*nMaxTries );
+ Vec_IntWriteEntry( vStats[2], i, nCurrCexes );
+ sat_solver_delete( pSat );
+ Cnf_DataFree( pCnf );
+ Gia_ManStop( pCon );
+ Vec_IntFree( vMap );
+ }
+ }
+ if ( fVerbose )
+ printf( "Used simulation for %d and SAT for %d outputs (out of %d).\n", nSimOuts, nSatOuts, nOuts );
+ //Vec_WecPrint( vCexes, 0 );
+ if ( vOuts != vOuts0 )
+ Vec_IntFreeP( &vOuts );
+ Min_ManStop( pNew );
+ Vec_IntFree( vPatBest );
+ Vec_IntFree( vLits );
+ return vCexes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Bit-packing for selected patterns.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Min_ManBitPackTry( Vec_Wrd_t * vSimsPi, int nWords, int iPat, Vec_Int_t * vLits )
+{
+ int i, Lit;
+ assert( iPat >= 0 && iPat < 64 * nWords );
+ Vec_IntForEachEntry( vLits, Lit, i )
+ {
+ word * pInfo = Vec_WrdEntryP( vSimsPi, nWords * Abc_Lit2Var(Lit-2) ); // Lit is based on ObjId
+ word * pCare = pInfo + Vec_WrdSize(vSimsPi);
+ if ( Abc_InfoHasBit( (unsigned *)pCare, iPat ) &&
+ Abc_InfoHasBit( (unsigned *)pInfo, iPat ) == Abc_LitIsCompl(Lit) ) // Lit is in ms notation
+ return 0;
+ }
+ Vec_IntForEachEntry( vLits, Lit, i )
+ {
+ word * pInfo = Vec_WrdEntryP( vSimsPi, nWords * Abc_Lit2Var(Lit-2) ); // Lit is based on ObjId
+ word * pCare = pInfo + Vec_WrdSize(vSimsPi);
+ Abc_InfoSetBit( (unsigned *)pCare, iPat );
+ if ( Abc_InfoHasBit( (unsigned *)pInfo, iPat ) == Abc_LitIsCompl(Lit) ) // Lit is in ms notation
+ Abc_InfoXorBit( (unsigned *)pInfo, iPat );
+ }
+ return 1;
+}
+int Min_ManBitPackOne( Vec_Wrd_t * vSimsPi, int iPat0, int nWords, Vec_Int_t * vLits )
+{
+ int iPat, nTotal = 64*nWords;
+ for ( iPat = iPat0 + 1; iPat != iPat0; iPat = (iPat + 1) % nTotal )
+ if ( Min_ManBitPackTry( vSimsPi, nWords, iPat, vLits ) )
+ break;
+ return iPat;
+}
+Vec_Wrd_t * Min_ManBitPack( Gia_Man_t * p, Vec_Wec_t * vCexes, int fRandom, int nMinCexes, Vec_Int_t * vScores, int fVerbose )
+{
+ abctime clk = Abc_Clock();
+ int fVeryVerbose = 0;
+ Vec_Wrd_t * vSimsPi = NULL;
+ Vec_Int_t * vLevel;
+ int w, nBits, nTotal = 0, fFailed = ABC_INFINITY;
+ Vec_Int_t * vOrder = Vec_IntStartNatural( Vec_WecSize(vCexes)/nMinCexes );
+ assert( Vec_IntSize(vOrder) == Vec_IntSize(vScores) );
+ assert( Vec_WecSize(vCexes)%nMinCexes == 0 );
+ Abc_MergeSortCost2Reverse( Vec_IntArray(vOrder), Vec_IntSize(vOrder), Vec_IntArray(vScores) );
+ if ( fVerbose )
+ printf( "Packing: " );
+ //for ( w = 1; fFailed > 100; w++ )
+ for ( w = 1; fFailed > 0; w++ )
+ {
+ int i, k, iOut, iPatUsed, iPat = 0;
+ Vec_WrdFreeP( &vSimsPi );
+ vSimsPi = fRandom ? Vec_WrdStartRandom(2 * Gia_ManCiNum(p) * w) : Vec_WrdStart(2 * Gia_ManCiNum(p) * w);
+ Vec_WrdShrink( vSimsPi, Vec_WrdSize(vSimsPi)/2 );
+ Abc_TtClear( Vec_WrdLimit(vSimsPi), Vec_WrdSize(vSimsPi) );
+ fFailed = nTotal = 0;
+ Vec_IntForEachEntry( vOrder, iOut, k )
+ Vec_WecForEachLevelStartStop( vCexes, vLevel, i, iOut*nMinCexes, (iOut+1)*nMinCexes )
+ {
+ if ( fVeryVerbose && i%nMinCexes == 0 )
+ printf( "\n" );
+ if ( Vec_IntSize(vLevel) == 0 )
+ continue;
+ iPatUsed = Min_ManBitPackOne( vSimsPi, iPat, w, vLevel );
+ fFailed += iPatUsed == iPat;
+ iPat = (iPatUsed + 1) % (64*w - 1);
+ if ( fVeryVerbose )
+ printf( "Adding output %3d cex %3d to pattern %3d ", i/nMinCexes, i%nMinCexes, iPatUsed );
+ if ( fVeryVerbose )
+ Vec_IntPrint( vLevel );
+ nTotal++;
+ }
+ if ( fVerbose )
+ printf( "W = %d (F = %d) ", w, fFailed );
+ }
+ if ( fVerbose )
+ printf( "Total = %d\n", nTotal );
+ if ( fVerbose )
+ {
+ nBits = Abc_TtCountOnesVec( Vec_WrdLimit(vSimsPi), Vec_WrdSize(vSimsPi) );
+ printf( "Bit-packing is using %d words and %d bits. Density =%8.4f %%. ",
+ Vec_WrdSize(vSimsPi)/Gia_ManCiNum(p), nBits, 100.0*nBits/64/Vec_WrdSize(vSimsPi) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ }
+ Vec_IntFree( vOrder );
+ return vSimsPi;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Patt_ManOutputErrorCoverage( Vec_Wrd_t * vErrors, int nOuts )
+{
+ Vec_Int_t * vCounts = Vec_IntAlloc( nOuts );
+ int i, nWords = Vec_WrdSize(vErrors)/nOuts;
+ assert( Vec_WrdSize(vErrors) == nOuts * nWords );
+ for ( i = 0; i < nOuts; i++ )
+ Vec_IntPush( vCounts, Abc_TtCountOnesVec(Vec_WrdEntryP(vErrors, nWords * i), nWords) );
+ return vCounts;
+}
+Vec_Wrd_t * Patt_ManTransposeErrors( Vec_Wrd_t * vErrors, int nOuts )
+{
+ extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut );
+ int nWordsIn = Vec_WrdSize(vErrors) / nOuts;
+ int nWordsOut = Abc_Bit6WordNum(nOuts);
+ Vec_Wrd_t * vSims1 = Vec_WrdStart( 64*nWordsIn*nWordsOut );
+ Vec_Wrd_t * vSims2 = Vec_WrdStart( 64*nWordsIn*nWordsOut );
+ assert( Vec_WrdSize(vErrors) == nWordsIn * nOuts );
+ Abc_TtCopy( Vec_WrdArray(vSims1), Vec_WrdArray(vErrors), Vec_WrdSize(vErrors), 0 );
+ Extra_BitMatrixTransposeP( vSims1, nWordsIn, vSims2, nWordsOut );
+ Vec_WrdFree( vSims1 );
+ return vSims2;
+}
+Vec_Int_t * Patt_ManPatternErrorCoverage( Vec_Wrd_t * vErrors, int nOuts )
+{
+ int nWords = Vec_WrdSize(vErrors)/nOuts;
+ Vec_Wrd_t * vErrors2 = Patt_ManTransposeErrors( vErrors, nOuts );
+ Vec_Int_t * vPatErrs = Patt_ManOutputErrorCoverage( vErrors2, 64*nWords );
+ Vec_WrdFree( vErrors2 );
+ return vPatErrs;
+}
+
+#define ERR_REPT_SIZE 32
+void Patt_ManProfileErrors( Vec_Int_t * vOutErrs, Vec_Int_t * vPatErrs )
+{
+ int nOuts = Vec_IntSize(vOutErrs);
+ int nPats = Vec_IntSize(vPatErrs);
+ int ErrOuts[ERR_REPT_SIZE+1] = {0};
+ int ErrPats[ERR_REPT_SIZE+1] = {0};
+ int i, Errs, nErrors1 = 0, nErrors2 = 0;
+ Vec_IntForEachEntry( vOutErrs, Errs, i )
+ {
+ nErrors1 += Errs;
+ ErrOuts[Errs < ERR_REPT_SIZE ? Errs : ERR_REPT_SIZE]++;
+ }
+ Vec_IntForEachEntry( vPatErrs, Errs, i )
+ {
+ nErrors2 += Errs;
+ ErrPats[Errs < ERR_REPT_SIZE ? Errs : ERR_REPT_SIZE]++;
+ }
+ assert( nErrors1 == nErrors2 );
+ // errors/error_outputs/error_patterns
+ //printf( "\nError statistics:\n" );
+ printf( "Errors =%6d ", nErrors1 );
+ printf( "ErrPOs =%5d (Ave = %5.2f) ", nOuts-ErrOuts[0], 1.0*nErrors1/Abc_MaxInt(1, nOuts-ErrOuts[0]) );
+ printf( "Patterns =%5d (Ave = %5.2f) ", nPats, 1.0*nErrors1/nPats );
+ printf( "Density =%8.4f %%\n", 100.0*nErrors1/nPats/Abc_MaxInt(1, nOuts-ErrOuts[0]) );
+ // how many times each output fails
+ printf( "Outputs: " );
+ for ( i = 0; i <= ERR_REPT_SIZE; i++ )
+ if ( ErrOuts[i] )
+ printf( "%s%d=%d ", i == ERR_REPT_SIZE? ">" : "", i, ErrOuts[i] );
+ printf( "\n" );
+ // how many times each patterns fails an output
+ printf( "Patterns: " );
+ for ( i = 0; i <= ERR_REPT_SIZE; i++ )
+ if ( ErrPats[i] )
+ printf( "%s%d=%d ", i == ERR_REPT_SIZE? ">" : "", i, ErrPats[i] );
+ printf( "\n" );
+}
+int Patt_ManProfileErrorsOne( Vec_Wrd_t * vErrors, int nOuts )
+{
+ Vec_Int_t * vCoErrs = Patt_ManOutputErrorCoverage( vErrors, nOuts );
+ Vec_Int_t * vPatErrs = Patt_ManPatternErrorCoverage( vErrors, nOuts );
+ Patt_ManProfileErrors( vCoErrs, vPatErrs );
+ Vec_IntFree( vPatErrs );
+ Vec_IntFree( vCoErrs );
+ return 1;
+}
+
+Vec_Int_t * Min_ManGetUnsolved( Gia_Man_t * p )
+{
+ Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+ int i, Driver;
+ Gia_ManForEachCoDriverId( p, Driver, i )
+ if ( Driver > 0 )
+ Vec_IntPush( vRes, i );
+ return vRes;
+}
+Vec_Wrd_t * Min_ManCollect( Gia_Man_t * p, int nConf, int nConf2, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fVerbose )
+{
+ abctime clk = Abc_Clock();
+ Vec_Int_t * vStats[3] = {0}; int i, iObj;
+ extern Gia_Man_t * Cec4_ManSimulateTest4( Gia_Man_t * p, int nBTLimit, int nBTLimitPo, int fVerbose );
+ Gia_Man_t * pSwp = Cec4_ManSimulateTest4( p, nConf, nConf2, 0 );
+ abctime clkSweep = Abc_Clock() - clk;
+ int nArgs = fVerbose ? printf( "Generating patterns: Conf = %d (%d). Tries = %d. Pats = %d. Sim = %d. SAT = %d.\n",
+ nConf, nConf2, nMaxTries, nMinCexes, fUseSim, fUseSat ) : 0;
+ Vec_Int_t * vOuts = Min_ManGetUnsolved( pSwp );
+ Gia_Man_t * pSwp2 = Gia_ManDupSelectedOutputs( pSwp, vOuts );
+ Vec_Wec_t * vCexes = Min_ManComputeCexes( pSwp2, NULL, nMaxTries, nMinCexes, vStats, fUseSim, fUseSat, fVerbose );
+ Vec_Wrd_t * vSimsPi = Min_ManBitPack( p, vCexes, 1, nMinCexes, vStats[0], fVerbose );
+ Vec_Wrd_t * vSimsPo = Gia_ManSimPatSimOut( pSwp2, vSimsPi, 1 );
+ Vec_Int_t * vCounts = Patt_ManOutputErrorCoverage( vSimsPo, Vec_IntSize(vOuts) );
+ if ( fVerbose )
+ {
+ Patt_ManProfileErrorsOne( vSimsPo, Vec_IntSize(vOuts) );
+ Abc_PrintTime( 1, "Sweep time", clkSweep );
+ Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
+ }
+ if ( 0 )
+ {
+ printf( "Unsolved = %4d ", Vec_IntSize(vOuts) );
+ Gia_ManPrintStats( pSwp2, NULL );
+ Vec_IntForEachEntry( vOuts, iObj, i )
+ {
+ printf( "%4d : ", i );
+ printf( "Out = %5d ", iObj );
+ printf( "SimAll =%8d ", Vec_IntEntry(vStats[0], i) );
+ printf( "SimGood =%8d ", Vec_IntEntry(vStats[1], i) );
+ printf( "PatsAll =%8d ", Vec_IntEntry(vStats[2], i) );
+ printf( "Count = %5d ", Vec_IntEntry(vCounts, i) );
+ printf( "\n" );
+ if ( i == 20 )
+ break;
+ }
+ }
+ for ( i = 0; i < 3; i++ )
+ Vec_IntFree( vStats[i] );
+ Vec_IntFree( vCounts );
+ Vec_WrdFree( vSimsPo );
+ Vec_WecFree( vCexes );
+ Vec_IntFree( vOuts );
+ Gia_ManStop( pSwp );
+ Gia_ManStop( pSwp2 );
+ nArgs = 0;
+ return vSimsPi;
+}
+void Min_ManTest2( Gia_Man_t * p )
+{
+ Vec_Wrd_t * vSimsPi = Min_ManCollect( p, 100000, 100000, 10000, 20, 1, 1, 0 );
+ Vec_WrdFreeP( &vSimsPi );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c
index bfafdcfd..a9706742 100644
--- a/src/aig/gia/giaSimBase.c
+++ b/src/aig/gia/giaSimBase.c
@@ -2522,6 +2522,106 @@ int Gia_ManSimTwo( Gia_Man_t * p0, Gia_Man_t * p1, int nWords, int nRounds, int
return RetValue;
}
+/**Function*************************************************************
+
+ Synopsis [Serialization.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManSim2ArrayOne( Vec_Wrd_t * vSimsPi, Vec_Int_t * vRes )
+{
+ word * pInfo = Vec_WrdArray(vSimsPi); int w, i;
+ word * pCare = pInfo + Vec_WrdSize(vSimsPi);
+ Vec_IntClear( vRes );
+ for ( w = 0; w < Vec_WrdSize(vSimsPi); w++ )
+ if ( pCare[w] )
+ for ( i = 0; i < 64; i++ )
+ if ( Abc_TtGetBit(pCare, w*64+i) )
+ Vec_IntPush( vRes, Abc_Var2Lit(w*64+i, Abc_TtGetBit(pInfo, w*64+i)) );
+ Vec_IntPush( vRes, Vec_WrdSize(vSimsPi) );
+}
+Vec_Wec_t * Gia_ManSim2Array( Vec_Ptr_t * vSims )
+{
+ Vec_Wec_t * vRes = Vec_WecStart( Vec_PtrSize(vSims) );
+ Vec_Int_t * vLevel; int i;
+ Vec_WecForEachLevel( vRes, vLevel, i )
+ Gia_ManSim2ArrayOne( (Vec_Wrd_t *)Vec_PtrEntry(vSims, i), vLevel );
+ return vRes;
+}
+
+Vec_Wrd_t * Gia_ManArray2SimOne( Vec_Int_t * vRes )
+{
+ int i, iLit, nWords = Vec_IntEntryLast(vRes);
+ Vec_Wrd_t * vSimsPi = Vec_WrdStart( 2*nWords );
+ word * pInfo = Vec_WrdArray(vSimsPi);
+ word * pCare = pInfo + nWords;
+ Vec_IntPop( vRes );
+ Vec_IntForEachEntry( vRes, iLit, i )
+ {
+ Abc_TtXorBit( pCare, Abc_Lit2Var(iLit) );
+ if ( Abc_LitIsCompl(iLit) )
+ Abc_TtXorBit( pInfo, Abc_Lit2Var(iLit) );
+ }
+ Vec_IntPush( vRes, nWords );
+ Vec_WrdShrink( vSimsPi, Vec_WrdSize(vSimsPi)/2 );
+ return vSimsPi;
+}
+Vec_Ptr_t * Gia_ManArray2Sim( Vec_Wec_t * vRes )
+{
+ Vec_Ptr_t * vSims = Vec_PtrAlloc( Vec_WecSize(vRes) );
+ Vec_Int_t * vLevel; int i;
+ Vec_WecForEachLevel( vRes, vLevel, i )
+ Vec_PtrPush( vSims, Gia_ManArray2SimOne(vLevel) );
+ return vSims;
+}
+
+void Gia_ManSimArrayTest( Vec_Wrd_t * vSimsPi )
+{
+ Vec_Ptr_t * vTemp = Vec_PtrAlloc( 2 );
+ Vec_PtrPushTwo( vTemp, vSimsPi, vSimsPi );
+ {
+ Vec_Wec_t * vRes = Gia_ManSim2Array( vTemp );
+ Vec_WecDumpBin( "temp.sims", vRes, 1 );
+ {
+ Vec_Wec_t * vRes = Vec_WecReadBin( "temp.sims", 1 );
+ Vec_Ptr_t * vTemp2 = Gia_ManArray2Sim( vRes );
+ Vec_Wrd_t * vSimsPi2 = (Vec_Wrd_t *)Vec_PtrEntry( vTemp2, 0 );
+ Vec_Wrd_t * vSimsPi3 = (Vec_Wrd_t *)Vec_PtrEntry( vTemp2, 1 );
+
+ Abc_TtAnd( Vec_WrdArray(vSimsPi), Vec_WrdArray(vSimsPi), Vec_WrdArray(vSimsPi)+Vec_WrdSize(vSimsPi), Vec_WrdSize(vSimsPi), 0 );
+
+ vSimsPi->nSize *= 2;
+ vSimsPi2->nSize *= 2;
+ vSimsPi3->nSize *= 2;
+ Vec_WrdDumpHex( "test1.hex", vSimsPi, 1, 1 );
+ Vec_WrdDumpHex( "test2.hex", vSimsPi2, 1, 1 );
+ Vec_WrdDumpHex( "test3.hex", vSimsPi3, 1, 1 );
+ vSimsPi->nSize /= 2;
+ vSimsPi2->nSize /= 2;
+ vSimsPi3->nSize /= 2;
+
+ if ( Vec_WrdEqual( vSimsPi, vSimsPi2 ) )
+ printf( "Success.\n" );
+ else
+ printf( "Failure.\n" );
+ if ( Vec_WrdEqual( vSimsPi, vSimsPi3 ) )
+ printf( "Success.\n" );
+ else
+ printf( "Failure.\n" );
+ Vec_WrdFree( vSimsPi2 );
+ Vec_WrdFree( vSimsPi3 );
+ Vec_PtrFree( vTemp2 );
+ Vec_WecFree( vRes );
+ }
+ Vec_WecFree( vRes );
+ }
+ Vec_PtrFree( vTemp );
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 8cbcaa25..d801a243 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -60,6 +60,7 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaOf.c \
src/aig/gia/giaPack.c \
src/aig/gia/giaPat.c \
+ src/aig/gia/giaPat2.c \
src/aig/gia/giaPf.c \
src/aig/gia/giaQbf.c \
src/aig/gia/giaReshape1.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 02:40:10 +0000