Skip to content

A
abc
Commit fdfb8888 by Alan Mishchenko
Options

Experiments with don't-cares.

parent 2ccd0f9b
Showing with 429 additions and 366 deletions
src/base/acb/acb.h
...@@ -30,6 +30,7 @@ ...@@ -30,6 +30,7 @@
#include "misc/util/utilNam.h" #include "misc/util/utilNam.h"
#include "misc/vec/vecHash.h" #include "misc/vec/vecHash.h"
#include "aig/miniaig/abcOper.h" #include "aig/miniaig/abcOper.h"
#include "misc/vec/vecQue.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// PARAMETERS /// /// PARAMETERS ///
...@@ -70,7 +71,6 @@ struct Acb_Ntk_t_ ...@@ -70,7 +71,6 @@ struct Acb_Ntk_t_
Vec_Str_t vObjType; // type Vec_Str_t vObjType; // type
Vec_Int_t vObjFans; // fanin offsets Vec_Int_t vObjFans; // fanin offsets
Vec_Int_t vFanSto; // fanin storage Vec_Int_t vFanSto; // fanin storage
Vec_Wec_t vFanouts; // fanouts
// optional // optional
Vec_Int_t vObjCopy; // copy Vec_Int_t vObjCopy; // copy
Vec_Int_t vObjFunc; // function Vec_Int_t vObjFunc; // function
...@@ -88,19 +88,20 @@ struct Acb_Ntk_t_ ...@@ -88,19 +88,20 @@ struct Acb_Ntk_t_
Vec_Int_t vLevelR; // level Vec_Int_t vLevelR; // level
Vec_Int_t vPathD; // path Vec_Int_t vPathD; // path
Vec_Int_t vPathR; // path Vec_Int_t vPathR; // path
Vec_Wec_t vClauses; Vec_Flt_t vCounts; // priority counts
Vec_Wec_t vCnfs; Vec_Wec_t vFanouts; // fanouts
Vec_Int_t vCover; Vec_Wec_t vCnfs; // CNF
// other // other
Vec_Int_t vArray0; Vec_Que_t * vQue; // temporary
Vec_Int_t vArray1; Vec_Int_t vCover; // temporary
Vec_Int_t vArray2; Vec_Int_t vArray0; // temporary
Vec_Int_t vArray1; // temporary
Vec_Int_t vArray2; // temporary
}; };
// design // design
struct Acb_Man_t_ struct Acb_Man_t_
{ {
// design names
char * pName; // design name char * pName; // design name
char * pSpec; // spec file name char * pSpec; // spec file name
Abc_Nam_t * pStrs; // string manager Abc_Nam_t * pStrs; // string manager
...@@ -185,7 +186,7 @@ static inline int Acb_NtkNodeNum( Acb_Ntk_t * p ) { r ...@@ -185,7 +186,7 @@ static inline int Acb_NtkNodeNum( Acb_Ntk_t * p ) { r
static inline int Acb_NtkSeqNum( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vSeq); } static inline int Acb_NtkSeqNum( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vSeq); }
static inline void Acb_NtkCleanObjCopies( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjCopy, Vec_StrCap(&p->vObjType), -1); } static inline void Acb_NtkCleanObjCopies( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjCopy, Vec_StrCap(&p->vObjType), -1); }
static inline void Acb_NtkCleanObjFuncs( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjFunc, Vec_StrCap(&p->vObjType), 0); } static inline void Acb_NtkCleanObjFuncs( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjFunc, Vec_StrCap(&p->vObjType), -1); }
static inline void Acb_NtkCleanObjWeights( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjWeight,Vec_StrCap(&p->vObjType), 0); } static inline void Acb_NtkCleanObjWeights( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjWeight,Vec_StrCap(&p->vObjType), 0); }
static inline void Acb_NtkCleanObjTruths( Acb_Ntk_t * p ) { Vec_WrdFill(&p->vObjTruth, Vec_StrCap(&p->vObjType), 0); } static inline void Acb_NtkCleanObjTruths( Acb_Ntk_t * p ) { Vec_WrdFill(&p->vObjTruth, Vec_StrCap(&p->vObjType), 0); }
static inline void Acb_NtkCleanObjNames( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjName, Vec_StrCap(&p->vObjType), 0); } static inline void Acb_NtkCleanObjNames( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjName, Vec_StrCap(&p->vObjType), 0); }
...@@ -196,6 +197,9 @@ static inline void Acb_NtkCleanObjLevelD( Acb_Ntk_t * p ) { V ...@@ -196,6 +197,9 @@ static inline void Acb_NtkCleanObjLevelD( Acb_Ntk_t * p ) { V
static inline void Acb_NtkCleanObjLevelR( Acb_Ntk_t * p ) { Vec_IntFill(&p->vLevelR, Vec_StrCap(&p->vObjType), 0); } static inline void Acb_NtkCleanObjLevelR( Acb_Ntk_t * p ) { Vec_IntFill(&p->vLevelR, Vec_StrCap(&p->vObjType), 0); }
static inline void Acb_NtkCleanObjPathD( Acb_Ntk_t * p ) { Vec_IntFill(&p->vPathD, Vec_StrCap(&p->vObjType), 0); } static inline void Acb_NtkCleanObjPathD( Acb_Ntk_t * p ) { Vec_IntFill(&p->vPathD, Vec_StrCap(&p->vObjType), 0); }
static inline void Acb_NtkCleanObjPathR( Acb_Ntk_t * p ) { Vec_IntFill(&p->vPathR, Vec_StrCap(&p->vObjType), 0); } static inline void Acb_NtkCleanObjPathR( Acb_Ntk_t * p ) { Vec_IntFill(&p->vPathR, Vec_StrCap(&p->vObjType), 0); }
static inline void Acb_NtkCleanObjCounts( Acb_Ntk_t * p ) { Vec_FltFill(&p->vCounts, Vec_StrCap(&p->vObjType), 0); }
static inline void Acb_NtkCleanObjFanout( Acb_Ntk_t * p ) { Vec_WecInit(&p->vFanouts, Vec_StrCap(&p->vObjType) ); }
static inline void Acb_NtkCleanObjCnfs( Acb_Ntk_t * p ) { Vec_WecInit(&p->vCnfs, Vec_StrCap(&p->vObjType) ); }
static inline int Acb_NtkHasObjCopies( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjCopy) > 0; } static inline int Acb_NtkHasObjCopies( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjCopy) > 0; }
static inline int Acb_NtkHasObjFuncs( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjFunc) > 0; } static inline int Acb_NtkHasObjFuncs( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjFunc) > 0; }
...@@ -209,6 +213,9 @@ static inline int Acb_NtkHasObjLevelD( Acb_Ntk_t * p ) { r ...@@ -209,6 +213,9 @@ static inline int Acb_NtkHasObjLevelD( Acb_Ntk_t * p ) { r
static inline int Acb_NtkHasObjLevelR( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vLevelR) > 0; } static inline int Acb_NtkHasObjLevelR( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vLevelR) > 0; }
static inline int Acb_NtkHasObjPathD( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vPathD) > 0; } static inline int Acb_NtkHasObjPathD( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vPathD) > 0; }
static inline int Acb_NtkHasObjPathR( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vPathR) > 0; } static inline int Acb_NtkHasObjPathR( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vPathR) > 0; }
static inline int Acb_NtkHasObjCounts( Acb_Ntk_t * p ) { return Vec_FltSize(&p->vCounts) > 0; }
static inline int Acb_NtkHasObjFanout( Acb_Ntk_t * p ) { return Vec_WecSize(&p->vFanouts) > 0; }
static inline int Acb_NtkHasObjCnfs( Acb_Ntk_t * p ) { return Vec_WecSize(&p->vCnfs) > 0; }
static inline void Acb_NtkFreeObjCopies( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjCopy); } static inline void Acb_NtkFreeObjCopies( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjCopy); }
static inline void Acb_NtkFreeObjFuncs( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjFunc); } static inline void Acb_NtkFreeObjFuncs( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjFunc); }
...@@ -222,6 +229,9 @@ static inline void Acb_NtkFreeObjLevelD( Acb_Ntk_t * p ) { V ...@@ -222,6 +229,9 @@ static inline void Acb_NtkFreeObjLevelD( Acb_Ntk_t * p ) { V
static inline void Acb_NtkFreeObjLevelR( Acb_Ntk_t * p ) { Vec_IntErase(&p->vLevelR); } static inline void Acb_NtkFreeObjLevelR( Acb_Ntk_t * p ) { Vec_IntErase(&p->vLevelR); }
static inline void Acb_NtkFreeObjPathD( Acb_Ntk_t * p ) { Vec_IntErase(&p->vPathD); } static inline void Acb_NtkFreeObjPathD( Acb_Ntk_t * p ) { Vec_IntErase(&p->vPathD); }
static inline void Acb_NtkFreeObjPathR( Acb_Ntk_t * p ) { Vec_IntErase(&p->vPathR); } static inline void Acb_NtkFreeObjPathR( Acb_Ntk_t * p ) { Vec_IntErase(&p->vPathR); }
static inline void Acb_NtkFreeObjCounts( Acb_Ntk_t * p ) { Vec_FltErase(&p->vCounts); }
static inline void Acb_NtkFreeObjFanout( Acb_Ntk_t * p ) { Vec_WecErase(&p->vFanouts); }
static inline void Acb_NtkFreeObjCnfs( Acb_Ntk_t * p ) { Vec_WecErase(&p->vCnfs); }
static inline Acb_ObjType_t Acb_ObjType( Acb_Ntk_t * p, int i ) { assert(i>0); return (Acb_ObjType_t)(int)(unsigned char)Vec_StrEntry(&p->vObjType, i); } static inline Acb_ObjType_t Acb_ObjType( Acb_Ntk_t * p, int i ) { assert(i>0); return (Acb_ObjType_t)(int)(unsigned char)Vec_StrEntry(&p->vObjType, i); }
static inline void Acb_ObjCleanType( Acb_Ntk_t * p, int i ) { assert(i>0); Vec_StrWriteEntry( &p->vObjType, i, (char)ABC_OPER_NONE ); } static inline void Acb_ObjCleanType( Acb_Ntk_t * p, int i ) { assert(i>0); Vec_StrWriteEntry( &p->vObjType, i, (char)ABC_OPER_NONE ); }
...@@ -248,14 +258,14 @@ static inline Vec_Int_t * Acb_ObjFanoutVec( Acb_Ntk_t * p, int i ) { r ...@@ -248,14 +258,14 @@ static inline Vec_Int_t * Acb_ObjFanoutVec( Acb_Ntk_t * p, int i ) { r
static inline int Acb_ObjFanin0( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[1]; } static inline int Acb_ObjFanin0( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[1]; }
static inline int Acb_ObjCioId( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[2]; } static inline int Acb_ObjCioId( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[2]; }
static inline int Acb_ObjCopy( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjCopies(p) ); return Vec_IntGetEntryFull(&p->vObjCopy, i); } static inline int Acb_ObjCopy( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjCopies(p) ); return Vec_IntEntry(&p->vObjCopy, i); }
static inline int Acb_ObjFunc( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjFuncs(p) ); return Vec_IntGetEntry(&p->vObjFunc, i); } static inline int Acb_ObjFunc( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjFuncs(p) ); return Vec_IntEntry(&p->vObjFunc, i); }
static inline int Acb_ObjWeight( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjWeights(p) );return Vec_IntGetEntry(&p->vObjWeight, i); } static inline int Acb_ObjWeight( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjWeights(p) );return Vec_IntEntry(&p->vObjWeight, i); }
static inline word Acb_ObjTruth( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjTruths(p) ); return Vec_WrdGetEntry(&p->vObjTruth, i); } static inline word Acb_ObjTruth( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjTruths(p) ); return Vec_WrdEntry(&p->vObjTruth, i); }
static inline word * Acb_ObjTruthP( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjTruths(p) ); return Vec_WrdEntryP(&p->vObjTruth, i); } static inline word * Acb_ObjTruthP( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjTruths(p) ); return Vec_WrdEntryP(&p->vObjTruth, i); }
static inline int Acb_ObjName( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjNames(p) ); return Vec_IntGetEntry(&p->vObjName, i); } static inline int Acb_ObjName( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjNames(p) ); return Vec_IntEntry(&p->vObjName, i); }
static inline char * Acb_ObjNameStr( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_NtkStr(p, Acb_ObjName(p, i)); } static inline char * Acb_ObjNameStr( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_NtkStr(p, Acb_ObjName(p, i)); }
static inline int Acb_ObjAttr( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_NtkHasObjAttrs(p) ? Vec_IntGetEntry(&p->vObjAttr, i) : 0; } static inline int Acb_ObjAttr( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_NtkHasObjAttrs(p) ? Vec_IntEntry(&p->vObjAttr, i) : 0; }
static inline int Acb_ObjAttrSize( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntry(&p->vAttrSto, Acb_ObjAttr(p, i)) : 0; } static inline int Acb_ObjAttrSize( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntry(&p->vAttrSto, Acb_ObjAttr(p, i)) : 0; }
static inline int * Acb_ObjAttrArray( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntryP(&p->vAttrSto, Acb_ObjAttr(p, i)+1) : NULL; } static inline int * Acb_ObjAttrArray( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntryP(&p->vAttrSto, Acb_ObjAttr(p, i)+1) : NULL; }
static inline int Acb_ObjAttrValue( Acb_Ntk_t * p, int i, int x ) { int k, s = Acb_ObjAttrSize(p, i), * a = Acb_ObjAttrArray(p, i); for ( k = 0; k < s; k += 2) if (a[k] == x) return a[k+1]; return 0; } static inline int Acb_ObjAttrValue( Acb_Ntk_t * p, int i, int x ) { int k, s = Acb_ObjAttrSize(p, i), * a = Acb_ObjAttrArray(p, i); for ( k = 0; k < s; k += 2) if (a[k] == x) return a[k+1]; return 0; }
...@@ -263,17 +273,21 @@ static inline int Acb_ObjLevelD( Acb_Ntk_t * p, int i ) { a ...@@ -263,17 +273,21 @@ static inline int Acb_ObjLevelD( Acb_Ntk_t * p, int i ) { a
static inline int Acb_ObjLevelR( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vLevelR, i); } static inline int Acb_ObjLevelR( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vLevelR, i); }
static inline int Acb_ObjPathD( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vPathD, i); } static inline int Acb_ObjPathD( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vPathD, i); }
static inline int Acb_ObjPathR( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vPathR, i); } static inline int Acb_ObjPathR( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vPathR, i); }
static inline float Acb_ObjCounts( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_FltEntry(&p->vCounts, i); }
static inline void Acb_ObjSetCopy( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjCopy(p, i) == -1); Vec_IntSetEntry( &p->vObjCopy, i, x ); } static inline Vec_Int_t * Acb_ObjFanout( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_WecEntry(&p->vFanouts, i); }
static inline void Acb_ObjSetFunc( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjFunc(p, i) == 0); Vec_IntSetEntry( &p->vObjFunc, i, x ); } static inline Vec_Str_t * Acb_ObjCnfs( Acb_Ntk_t * p, int i ) { assert(i>0); return (Vec_Str_t *)Vec_WecEntry(&p->vCnfs, i); }
static inline void Acb_ObjSetWeight( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjWeight(p, i) == 0); Vec_IntSetEntry( &p->vObjWeight, i, x ); }
static inline void Acb_ObjSetTruth( Acb_Ntk_t * p, int i, word x ) { assert(Acb_ObjTruth(p, i) == 0);Vec_WrdSetEntry( &p->vObjTruth, i, x ); } static inline void Acb_ObjSetCopy( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjCopy(p, i) == -1); Vec_IntWriteEntry( &p->vObjCopy, i, x ); }
static inline void Acb_ObjSetName( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjName(p, i) == 0); Vec_IntSetEntry( &p->vObjName, i, x ); } static inline void Acb_ObjSetFunc( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjFunc(p, i) == -1); Vec_IntWriteEntry( &p->vObjFunc, i, x ); }
static inline void Acb_ObjSetAttrs( Acb_Ntk_t * p, int i, int * a, int s ) { assert(Acb_ObjAttr(p, i) == 0); if ( !a ) return; Vec_IntSetEntry(&p->vObjAttr, i, Vec_IntSize(&p->vAttrSto)); Vec_IntPush(&p->vAttrSto, s); Vec_IntPushArray(&p->vAttrSto, a, s); } static inline void Acb_ObjSetWeight( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjWeight(p, i)== 0); Vec_IntWriteEntry( &p->vObjWeight, i, x ); }
static inline int Acb_ObjSetLevelD( Acb_Ntk_t * p, int i, int x ) { Vec_IntSetEntry( &p->vLevelD, i, x ); return x; } static inline void Acb_ObjSetTruth( Acb_Ntk_t * p, int i, word x ) { assert(Acb_ObjTruth(p, i) == 0); Vec_WrdWriteEntry( &p->vObjTruth, i, x ); }
static inline int Acb_ObjSetLevelR( Acb_Ntk_t * p, int i, int x ) { Vec_IntSetEntry( &p->vLevelR, i, x ); return x; } static inline void Acb_ObjSetName( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjName(p, i) == 0); Vec_IntWriteEntry( &p->vObjName, i, x ); }
static inline int Acb_ObjSetPathD( Acb_Ntk_t * p, int i, int x ) { Vec_IntSetEntry( &p->vPathD, i, x ); return x; } static inline void Acb_ObjSetAttrs( Acb_Ntk_t * p, int i, int * a, int s ) { assert(Acb_ObjAttr(p, i) == 0); if ( !a ) return; Vec_IntWriteEntry(&p->vObjAttr, i, Vec_IntSize(&p->vAttrSto)); Vec_IntPush(&p->vAttrSto, s); Vec_IntPushArray(&p->vAttrSto, a, s); }
static inline int Acb_ObjSetPathR( Acb_Ntk_t * p, int i, int x ) { Vec_IntSetEntry( &p->vPathR, i, x ); return x; } static inline int Acb_ObjSetLevelD( Acb_Ntk_t * p, int i, int x ) { Vec_IntWriteEntry( &p->vLevelD, i, x ); return x; }
static inline int Acb_ObjSetLevelR( Acb_Ntk_t * p, int i, int x ) { Vec_IntWriteEntry( &p->vLevelR, i, x ); return x; }
static inline int Acb_ObjSetPathD( Acb_Ntk_t * p, int i, int x ) { Vec_IntWriteEntry( &p->vPathD, i, x ); return x; }
static inline int Acb_ObjSetPathR( Acb_Ntk_t * p, int i, int x ) { Vec_IntWriteEntry( &p->vPathR, i, x ); return x; }
static inline float Acb_ObjSetCounts( Acb_Ntk_t * p, int i, float x ) { Vec_FltWriteEntry( &p->vCounts, i, x ); return x; }
static inline int Acb_ObjUpdateLevelD( Acb_Ntk_t * p, int i, int x ) { Vec_IntUpdateEntry( &p->vLevelD, i, x ); return x; } static inline int Acb_ObjUpdateLevelD( Acb_Ntk_t * p, int i, int x ) { Vec_IntUpdateEntry( &p->vLevelD, i, x ); return x; }
static inline int Acb_ObjUpdateLevelR( Acb_Ntk_t * p, int i, int x ) { Vec_IntUpdateEntry( &p->vLevelR, i, x ); return x; } static inline int Acb_ObjUpdateLevelR( Acb_Ntk_t * p, int i, int x ) { Vec_IntUpdateEntry( &p->vLevelR, i, x ); return x; }
static inline int Acb_ObjAddToPathD( Acb_Ntk_t * p, int i, int x ) { Vec_IntAddToEntry( &p->vPathD, i, x ); return x; } static inline int Acb_ObjAddToPathD( Acb_Ntk_t * p, int i, int x ) { Vec_IntAddToEntry( &p->vPathD, i, x ); return x; }
...@@ -283,19 +297,19 @@ static inline int Acb_ObjNtkId( Acb_Ntk_t * p, int i ) ...@@ -283,19 +297,19 @@ static inline int Acb_ObjNtkId( Acb_Ntk_t * p, int i )
static inline Acb_Ntk_t * Acb_ObjNtk( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_NtkNtk(p, Acb_ObjNtkId(p, i)); } static inline Acb_Ntk_t * Acb_ObjNtk( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_NtkNtk(p, Acb_ObjNtkId(p, i)); }
static inline int Acb_ObjIsSeq( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjNtk(p, i)->fSeq : Acb_TypeIsSeq(Acb_ObjType(p, i)); } static inline int Acb_ObjIsSeq( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjNtk(p, i)->fSeq : Acb_TypeIsSeq(Acb_ObjType(p, i)); }
static inline int Acb_ObjRangeId( Acb_Ntk_t * p, int i ) { return Acb_NtkHasObjRanges(p) ? Vec_IntGetEntry(&p->vObjRange, i) : 0; } static inline int Acb_ObjRangeId( Acb_Ntk_t * p, int i ) { return Acb_NtkHasObjRanges(p) ? Vec_IntEntry(&p->vObjRange, i) : 0; }
static inline int Acb_ObjRange( Acb_Ntk_t * p, int i ) { return Abc_Lit2Var( Acb_ObjRangeId(p, i) ); } static inline int Acb_ObjRange( Acb_Ntk_t * p, int i ) { return Abc_Lit2Var( Acb_ObjRangeId(p, i) ); }
static inline int Acb_ObjLeft( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeLeft(p, Acb_ObjRange(p, i)); } static inline int Acb_ObjLeft( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeLeft(p, Acb_ObjRange(p, i)); }
static inline int Acb_ObjRight( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeRight(p, Acb_ObjRange(p, i)); } static inline int Acb_ObjRight( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeRight(p, Acb_ObjRange(p, i)); }
static inline int Acb_ObjSigned( Acb_Ntk_t * p, int i ) { return Abc_LitIsCompl(Acb_ObjRangeId(p, i)); } static inline int Acb_ObjSigned( Acb_Ntk_t * p, int i ) { return Abc_LitIsCompl(Acb_ObjRangeId(p, i)); }
static inline int Acb_ObjRangeSize( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeSize(p, Acb_ObjRange(p, i)); } static inline int Acb_ObjRangeSize( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeSize(p, Acb_ObjRange(p, i)); }
static inline void Acb_ObjSetRangeSign( Acb_Ntk_t * p, int i, int x ) { assert(Acb_NtkHasObjRanges(p)); Vec_IntSetEntry(&p->vObjRange, i, x); } static inline void Acb_ObjSetRangeSign( Acb_Ntk_t * p, int i, int x ) { assert(Acb_NtkHasObjRanges(p)); Vec_IntWriteEntry(&p->vObjRange, i, x); }
static inline void Acb_ObjSetRange( Acb_Ntk_t * p, int i, int x ) { assert(Acb_NtkHasObjRanges(p)); Vec_IntSetEntry(&p->vObjRange, i, Abc_Var2Lit(x,0)); } static inline void Acb_ObjSetRange( Acb_Ntk_t * p, int i, int x ) { assert(Acb_NtkHasObjRanges(p)); Vec_IntWriteEntry(&p->vObjRange, i, Abc_Var2Lit(x,0)); }
static inline void Acb_ObjHashRange( Acb_Ntk_t * p, int i, int l, int r ) { Acb_ObjSetRange( p, i, Acb_NtkHashRange(p, l, r) ); } static inline void Acb_ObjHashRange( Acb_Ntk_t * p, int i, int l, int r ) { Acb_ObjSetRange( p, i, Acb_NtkHashRange(p, l, r) ); }
static inline int Acb_ObjRangeSign( Acb_Ntk_t * p, int i ) { return Abc_Var2Lit( Acb_ObjRangeSize(p, i), Acb_ObjSigned(p, i) ); } static inline int Acb_ObjRangeSign( Acb_Ntk_t * p, int i ) { return Abc_Var2Lit( Acb_ObjRangeSize(p, i), Acb_ObjSigned(p, i) ); }
static inline int Acb_ObjTravId( Acb_Ntk_t * p, int i ) { return Vec_IntGetEntry(&p->vObjTrav, i); } static inline int Acb_ObjTravId( Acb_Ntk_t * p, int i ) { return Vec_IntEntry(&p->vObjTrav, i); }
static inline int Acb_ObjTravIdDiff( Acb_Ntk_t * p, int i ) { return p->nObjTravs - Vec_IntGetEntry(&p->vObjTrav, i); } static inline int Acb_ObjTravIdDiff( Acb_Ntk_t * p, int i ) { return p->nObjTravs - Vec_IntEntry(&p->vObjTrav, i); }
static inline int Acb_ObjIsTravIdCur( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs; } static inline int Acb_ObjIsTravIdCur( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs; }
static inline int Acb_ObjIsTravIdPrev( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs-1; } static inline int Acb_ObjIsTravIdPrev( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs-1; }
static inline int Acb_ObjIsTravIdDiff( Acb_Ntk_t * p, int i, int d ) { return Acb_ObjTravId(p, i) == p->nObjTravs-d; } static inline int Acb_ObjIsTravIdDiff( Acb_Ntk_t * p, int i, int d ) { return Acb_ObjTravId(p, i) == p->nObjTravs-d; }
...@@ -393,6 +407,13 @@ static inline void Acb_ObjAddFanin( Acb_Ntk_t * p, int iObj, int iFanin ) ...@@ -393,6 +407,13 @@ static inline void Acb_ObjAddFanin( Acb_Ntk_t * p, int iObj, int iFanin )
assert( pFanins[ 1 + pFanins[0] ] == -1 ); assert( pFanins[ 1 + pFanins[0] ] == -1 );
pFanins[ 1 + pFanins[0]++ ] = iFanin; pFanins[ 1 + pFanins[0]++ ] = iFanin;
} }
static inline void Acb_ObjAddFanins( Acb_Ntk_t * p, int iObj, Vec_Int_t * vFanins )
{
int i, iFanin;
if ( vFanins )
Vec_IntForEachEntry( vFanins, iFanin, i )
Acb_ObjAddFanin( p, iObj, iFanin );
}
static inline void Acb_ObjSetNtkId( Acb_Ntk_t * p, int iObj, int iNtk ) // should be called after fanins are added static inline void Acb_ObjSetNtkId( Acb_Ntk_t * p, int iObj, int iNtk ) // should be called after fanins are added
{ {
int * pFanins = Acb_ObjFanins( p, iObj ); int * pFanins = Acb_ObjFanins( p, iObj );
...@@ -438,6 +459,23 @@ static inline int Acb_ObjAlloc( Acb_Ntk_t * p, Acb_ObjType_t Type, int nFans, in ...@@ -438,6 +459,23 @@ static inline int Acb_ObjAlloc( Acb_Ntk_t * p, Acb_ObjType_t Type, int nFans, in
assert( !Acb_ObjIsBox(p, iObj) || nFons > 0 ); assert( !Acb_ObjIsBox(p, iObj) || nFons > 0 );
for ( i = 0; i < nFons; i++ ) for ( i = 0; i < nFons; i++ )
Acb_ObjAddFanin( p, Acb_ObjAlloc(p, ABC_OPER_FON, 1, 0), iObj ); Acb_ObjAddFanin( p, Acb_ObjAlloc(p, ABC_OPER_FON, 1, 0), iObj );
// extend storage
if ( Acb_NtkHasObjCopies(p) ) Vec_IntPush(&p->vObjCopy , -1);
if ( Acb_NtkHasObjFuncs(p) ) Vec_IntPush(&p->vObjFunc , -1);
if ( Acb_NtkHasObjWeights(p)) Vec_IntPush(&p->vObjWeight, 0);
if ( Acb_NtkHasObjTruths(p) ) Vec_WrdPush(&p->vObjTruth , 0);
if ( Acb_NtkHasObjNames(p) ) Vec_IntPush(&p->vObjName , 0);
if ( Acb_NtkHasObjRanges(p) ) Vec_IntPush(&p->vObjRange , 0);
if ( Acb_NtkHasObjTravs(p) ) Vec_IntPush(&p->vObjTrav , 0);
if ( Acb_NtkHasObjAttrs(p) ) Vec_IntPush(&p->vObjAttr , 0);
if ( Acb_NtkHasObjLevelD(p) ) Vec_IntPush(&p->vLevelD , 0);
if ( Acb_NtkHasObjLevelR(p) ) Vec_IntPush(&p->vLevelR , 0);
if ( Acb_NtkHasObjPathD(p) ) Vec_IntPush(&p->vPathD , 0);
if ( Acb_NtkHasObjPathR(p) ) Vec_IntPush(&p->vPathR , 0);
if ( Acb_NtkHasObjCounts(p) ) Vec_FltPush(&p->vCounts , 0);
if ( Acb_NtkHasObjFanout(p) ) Vec_WecPushLevel(&p->vFanouts);
if ( Acb_NtkHasObjCnfs(p) ) Vec_WecPushLevel(&p->vCnfs);
if ( p->vQue ) Vec_QueSetPriority( p->vQue, Vec_FltArrayP(&p->vCounts) );
return iObj; return iObj;
} }
static inline int Acb_ObjDup( Acb_Ntk_t * pNew, Acb_Ntk_t * p, int i ) static inline int Acb_ObjDup( Acb_Ntk_t * pNew, Acb_Ntk_t * p, int i )
...@@ -455,6 +493,25 @@ static inline void Acb_ObjDelete( Acb_Ntk_t * p, int iObj ) ...@@ -455,6 +493,25 @@ static inline void Acb_ObjDelete( Acb_Ntk_t * p, int iObj )
Acb_ObjForEachFon( p, iObj, i ) Acb_ObjForEachFon( p, iObj, i )
Acb_ObjCleanType( p, i ); Acb_ObjCleanType( p, i );
} }
static inline void Acb_ObjAddFaninFanout( Acb_Ntk_t * p, int iObj )
{
int k, iFanin, * pFanins;
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntPush( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
}
static inline void Acb_ObjRemoveFaninFanout( Acb_Ntk_t * p, int iObj )
{
int k, iFanin, * pFanins;
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
}
static inline void Acb_NtkCreateFanout( Acb_Ntk_t * p )
{
int iObj;
Acb_NtkCleanObjFanout( p );
Acb_NtkForEachObj( p, iObj )
Acb_ObjAddFaninFanout( p, iObj );
}
/**Function************************************************************* /**Function*************************************************************
...@@ -492,7 +549,6 @@ static inline void Acb_NtkFree( Acb_Ntk_t * p ) ...@@ -492,7 +549,6 @@ static inline void Acb_NtkFree( Acb_Ntk_t * p )
Vec_StrErase( &p->vObjType ); Vec_StrErase( &p->vObjType );
Vec_IntErase( &p->vObjFans ); Vec_IntErase( &p->vObjFans );
Vec_IntErase( &p->vFanSto ); Vec_IntErase( &p->vFanSto );
Vec_WecErase( &p->vFanouts );
// optional // optional
Vec_IntErase( &p->vObjCopy ); Vec_IntErase( &p->vObjCopy );
Vec_IntErase( &p->vObjFunc ); Vec_IntErase( &p->vObjFunc );
...@@ -510,7 +566,12 @@ static inline void Acb_NtkFree( Acb_Ntk_t * p ) ...@@ -510,7 +566,12 @@ static inline void Acb_NtkFree( Acb_Ntk_t * p )
Vec_IntErase( &p->vLevelR ); Vec_IntErase( &p->vLevelR );
Vec_IntErase( &p->vPathD ); Vec_IntErase( &p->vPathD );
Vec_IntErase( &p->vPathR ); Vec_IntErase( &p->vPathR );
Vec_FltErase( &p->vCounts );
Vec_WecErase( &p->vFanouts );
Vec_WecErase( &p->vCnfs );
// other // other
Vec_QueFreeP( &p->vQue );
Vec_IntErase( &p->vCover );
Vec_IntErase( &p->vArray0 ); Vec_IntErase( &p->vArray0 );
Vec_IntErase( &p->vArray1 ); Vec_IntErase( &p->vArray1 );
Vec_IntErase( &p->vArray2 ); Vec_IntErase( &p->vArray2 );
...@@ -572,42 +633,6 @@ static inline Vec_Int_t * Acb_NtkCollect( Acb_Ntk_t * p ) ...@@ -572,42 +633,6 @@ static inline Vec_Int_t * Acb_NtkCollect( Acb_Ntk_t * p )
Vec_IntPush( vObjs, iObj ); Vec_IntPush( vObjs, iObj );
return vObjs; return vObjs;
} }
static inline int Acb_NtkIsSeq( Acb_Ntk_t * p )
{
int iObj;
if ( p->fSeq )
return 1;
if ( p->fComb )
return 0;
assert( !p->fSeq && !p->fComb );
Acb_NtkForEachBox( p, iObj )
if ( Acb_ObjIsBox(p, iObj) )
{
if ( Acb_NtkIsSeq( Acb_ObjNtk(p, iObj) ) )
{
p->fSeq = 1;
return 1;
}
}
else if ( Acb_ObjIsSeq(p, iObj) )
{
p->fSeq = 1;
return 1;
}
p->fComb = 1;
return 0;
}
static inline void Acb_NtkPrepareSeq( Acb_Ntk_t * p )
{
int iObj;
assert( Acb_NtkSeqNum(p) == 0 );
if ( !Acb_NtkIsSeq(p) )
return;
Acb_NtkForEachBox( p, iObj )
if ( Acb_ObjIsSeq(p, iObj) )
Vec_IntPush( &p->vSeq, iObj );
// Acb_NtkObjOrder( p, &p->vSeq, NULL );
}
static inline Acb_Ntk_t * Acb_NtkDup( Acb_Man_t * pMan, Acb_Ntk_t * p, Vec_Int_t * vObjs ) static inline Acb_Ntk_t * Acb_NtkDup( Acb_Man_t * pMan, Acb_Ntk_t * p, Vec_Int_t * vObjs )
{ {
Acb_Ntk_t * pNew; Acb_Ntk_t * pNew;
...@@ -684,6 +709,7 @@ static inline int Acb_NtkMemory( Acb_Ntk_t * p ) ...@@ -684,6 +709,7 @@ static inline int Acb_NtkMemory( Acb_Ntk_t * p )
nMem += (int)Vec_IntMemory(&p->vNtkObjs ); nMem += (int)Vec_IntMemory(&p->vNtkObjs );
nMem += (int)Vec_IntMemory(&p->vTargets ); nMem += (int)Vec_IntMemory(&p->vTargets );
// other // other
nMem += (int)Vec_IntMemory(&p->vCover );
nMem += (int)Vec_IntMemory(&p->vArray0 ); nMem += (int)Vec_IntMemory(&p->vArray0 );
nMem += (int)Vec_IntMemory(&p->vArray1 ); nMem += (int)Vec_IntMemory(&p->vArray1 );
nMem += (int)Vec_IntMemory(&p->vArray2 ); nMem += (int)Vec_IntMemory(&p->vArray2 );
...@@ -774,12 +800,6 @@ static inline Acb_Man_t * Acb_ManDup( Acb_Man_t * p, Vec_Int_t*(* pFuncOrder)(Ac ...@@ -774,12 +800,6 @@ static inline Acb_Man_t * Acb_ManDup( Acb_Man_t * p, Vec_Int_t*(* pFuncOrder)(Ac
pNew->iRoot = Acb_ManNtkNum(pNew); pNew->iRoot = Acb_ManNtkNum(pNew);
return pNew; return pNew;
} }
static inline void Acb_ManPrepareSeq( Acb_Man_t * p )
{
Acb_Ntk_t * pNtk; int i;
Acb_ManForEachNtk( p, pNtk, i )
Acb_NtkPrepareSeq( pNtk );
}
static inline void Acb_ManFree( Acb_Man_t * p ) static inline void Acb_ManFree( Acb_Man_t * p )
{ {
Acb_Ntk_t * pNtk; int i; Acb_Ntk_t * pNtk; int i;
...@@ -939,7 +959,15 @@ static inline void Acb_ManPrintStats( Acb_Man_t * p, int nModules, int fVerbose ...@@ -939,7 +959,15 @@ static inline void Acb_ManPrintStats( Acb_Man_t * p, int nModules, int fVerbose
/*=== acbUtil.c =============================================================*/ /*=== acbUtil.c =============================================================*/
extern Vec_Int_t * Acb_ObjCollectTfi( Acb_Ntk_t * p, int iObj, int fTerm );
extern Vec_Int_t * Acb_ObjCollectTfo( Acb_Ntk_t * p, int iObj, int fTerm );
extern int Acb_ObjComputeLevelD( Acb_Ntk_t * p, int iObj );
extern int Acb_NtkComputeLevelD( Acb_Ntk_t * p, Vec_Int_t * vTfo );
extern void Acb_NtkUpdateLevelD( Acb_Ntk_t * p, int iObj );
extern void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj ); extern void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj );
extern void Acb_NtkCreateNode( Acb_Ntk_t * p, word uTruth, Vec_Int_t * vSupp );
extern void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp ); extern void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp );
ABC_NAMESPACE_HEADER_END ABC_NAMESPACE_HEADER_END
......
src/base/acb/acbAbc.c
...@@ -46,15 +46,25 @@ ABC_NAMESPACE_IMPL_START ...@@ -46,15 +46,25 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/ ***********************************************************************/
Acb_Ntk_t * Acb_NtkFromAbc( Abc_Ntk_t * p ) Acb_Ntk_t * Acb_NtkFromAbc( Abc_Ntk_t * p )
{ {
int fTrack = 1;
Acb_Man_t * pMan = Acb_ManAlloc( Abc_NtkSpec(p), 1, NULL, NULL, NULL, NULL ); Acb_Man_t * pMan = Acb_ManAlloc( Abc_NtkSpec(p), 1, NULL, NULL, NULL, NULL );
int i, k, NameId = Abc_NamStrFindOrAdd( pMan->pStrs, Abc_NtkName(p), NULL ); int i, k, NameId = Abc_NamStrFindOrAdd( pMan->pStrs, Abc_NtkName(p), NULL );
Acb_Ntk_t * pNtk = Acb_NtkAlloc( pMan, NameId, Abc_NtkCiNum(p), Abc_NtkCoNum(p), Abc_NtkObjNum(p) ); Acb_Ntk_t * pNtk = Acb_NtkAlloc( pMan, NameId, Abc_NtkCiNum(p), Abc_NtkCoNum(p), Abc_NtkObjNum(p) );
Abc_Obj_t * pObj, * pFanin; Abc_Obj_t * pObj, * pFanin;
assert( Abc_NtkIsSopLogic(p) ); assert( Abc_NtkIsSopLogic(p) );
pNtk->nFaninMax = 6;
if ( fTrack ) Vec_IntFill( &pNtk->vArray2, Abc_NtkObjNumMax(p), -1 );
Abc_NtkForEachCi( p, pObj, i ) Abc_NtkForEachCi( p, pObj, i )
{
pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_CI, 0, 0 ); pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_CI, 0, 0 );
if ( fTrack ) Vec_IntWriteEntry( &pNtk->vArray2, pObj->iTemp, Abc_ObjId(pObj) );
}
Abc_NtkForEachNode( p, pObj, i ) Abc_NtkForEachNode( p, pObj, i )
{
pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_LUT, Abc_ObjFaninNum(pObj), 0 ); pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_LUT, Abc_ObjFaninNum(pObj), 0 );
if ( fTrack ) Vec_IntWriteEntry( &pNtk->vArray2, pObj->iTemp, Abc_ObjId(pObj) );
// printf( "%d -> %d\n%s", i, pObj->iTemp, (char *)pObj->pData );
}
Abc_NtkForEachCo( p, pObj, i ) Abc_NtkForEachCo( p, pObj, i )
pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_CO, 1, 0 ); pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_CO, 1, 0 );
Abc_NtkForEachNode( p, pObj, i ) Abc_NtkForEachNode( p, pObj, i )
...@@ -199,8 +209,8 @@ void Acb_ParSetDefault( Acb_Par_t * pPars ) ...@@ -199,8 +209,8 @@ void Acb_ParSetDefault( Acb_Par_t * pPars )
{ {
memset( pPars, 0, sizeof(Acb_Par_t) ); memset( pPars, 0, sizeof(Acb_Par_t) );
pPars->nLutSize = 4; // LUT size pPars->nLutSize = 4; // LUT size
pPars->nTfoLevMax = 3; // the maximum fanout levels pPars->nTfoLevMax = 1; // the maximum fanout levels
pPars->nTfiLevMax = 3; // the maximum fanin levels pPars->nTfiLevMax = 2; // the maximum fanin levels
pPars->nFanoutMax = 10; // the maximum number of fanouts pPars->nFanoutMax = 10; // the maximum number of fanouts
pPars->nDivMax = 16; // the maximum divisor count pPars->nDivMax = 16; // the maximum divisor count
pPars->nTabooMax = 4; // the minimum MFFC size pPars->nTabooMax = 4; // the minimum MFFC size
...@@ -208,7 +218,7 @@ void Acb_ParSetDefault( Acb_Par_t * pPars ) ...@@ -208,7 +218,7 @@ void Acb_ParSetDefault( Acb_Par_t * pPars )
pPars->nBTLimit = 0; // the maximum number of conflicts in one SAT run pPars->nBTLimit = 0; // the maximum number of conflicts in one SAT run
pPars->nNodesMax = 0; // the maximum number of nodes to try pPars->nNodesMax = 0; // the maximum number of nodes to try
pPars->iNodeOne = 0; // one particular node to try pPars->iNodeOne = 0; // one particular node to try
pPars->fArea = 0; // performs optimization for area pPars->fArea = 1; // performs optimization for area
pPars->fMoreEffort = 0; // enables using more effort pPars->fMoreEffort = 0; // enables using more effort
pPars->fVerbose = 0; // enable basic stats pPars->fVerbose = 0; // enable basic stats
pPars->fVeryVerbose = 0; // enable detailed stats pPars->fVeryVerbose = 0; // enable detailed stats
...@@ -230,7 +240,7 @@ Abc_Ntk_t * Abc_NtkOptMfse( Abc_Ntk_t * pNtk, Acb_Par_t * pPars ) ...@@ -230,7 +240,7 @@ Abc_Ntk_t * Abc_NtkOptMfse( Abc_Ntk_t * pNtk, Acb_Par_t * pPars )
extern void Acb_NtkOpt( Acb_Ntk_t * p, Acb_Par_t * pPars ); extern void Acb_NtkOpt( Acb_Ntk_t * p, Acb_Par_t * pPars );
Abc_Ntk_t * pNtkNew; Abc_Ntk_t * pNtkNew;
Acb_Ntk_t * p = Acb_NtkFromAbc( pNtk ); Acb_Ntk_t * p = Acb_NtkFromAbc( pNtk );
//Acb_NtkOpt( p, pPars ); Acb_NtkOpt( p, pPars );
pNtkNew = Acb_NtkToAbc( pNtk, p ); pNtkNew = Acb_NtkToAbc( pNtk, p );
Acb_ManFree( p->pDesign ); Acb_ManFree( p->pDesign );
return pNtkNew; return pNtkNew;
......
src/base/acb/acbMfs.c
...@@ -94,7 +94,8 @@ Vec_Wec_t * Acb_DeriveCnfForWindow( Acb_Ntk_t * p, Vec_Int_t * vWin, int PivotVa ...@@ -94,7 +94,8 @@ Vec_Wec_t * Acb_DeriveCnfForWindow( Acb_Ntk_t * p, Vec_Int_t * vWin, int PivotVa
{ {
if ( Abc_LitIsCompl(iObj) && i < PivotVar ) if ( Abc_LitIsCompl(iObj) && i < PivotVar )
continue; continue;
vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, iObj ); iObj = Abc_Lit2Var(iObj);
vCnfBase = Acb_ObjCnfs( p, iObj );
if ( Vec_StrSize(vCnfBase) > 0 ) if ( Vec_StrSize(vCnfBase) > 0 )
continue; continue;
if ( vCnf == NULL ) if ( vCnf == NULL )
...@@ -163,7 +164,10 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot ) ...@@ -163,7 +164,10 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
Vec_Int_t * vLits = Vec_IntAlloc( 1000 ); Vec_Int_t * vLits = Vec_IntAlloc( 1000 );
// mark new SAT variables // mark new SAT variables
Vec_IntForEachEntry( vWinObjs, iObj, i ) Vec_IntForEachEntry( vWinObjs, iObj, i )
Acb_ObjSetCopy( p, i, iObj ); {
Acb_ObjSetFunc( p, Abc_Lit2Var(iObj), i );
//printf( "Node %d -> SAT var %d\n", Vec_IntEntry(&p->vArray2, Abc_Lit2Var(iObj)), i );
}
// add clauses for all nodes // add clauses for all nodes
Vec_IntPush( vClas, Vec_IntSize(vLits) ); Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntForEachEntry( vWinObjs, iObjLit, i ) Vec_IntForEachEntry( vWinObjs, iObjLit, i )
...@@ -175,8 +179,8 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot ) ...@@ -175,8 +179,8 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
// collect SAT variables // collect SAT variables
Vec_IntClear( vFaninVars ); Vec_IntClear( vFaninVars );
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iFanin) ); Vec_IntPush( vFaninVars, Acb_ObjFunc(p, iFanin) );
Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iObj) ); Vec_IntPush( vFaninVars, Acb_ObjFunc(p, iObj) );
// derive CNF for the node // derive CNF for the node
Acb_TranslateCnf( vClas, vLits, (Vec_Str_t *)Vec_WecEntry(vCnfs, iObj), vFaninVars, -1 ); Acb_TranslateCnf( vClas, vLits, (Vec_Str_t *)Vec_WecEntry(vCnfs, iObj), vFaninVars, -1 );
} }
...@@ -188,8 +192,8 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot ) ...@@ -188,8 +192,8 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
// collect SAT variables // collect SAT variables
Vec_IntClear( vFaninVars ); Vec_IntClear( vFaninVars );
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iFanin) + (iFanin > PivotVar) * nTfoSize ); Vec_IntPush( vFaninVars, Acb_ObjFunc(p, iFanin) + (Acb_ObjFunc(p, iFanin) > PivotVar) * nTfoSize );
Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iObj) + nTfoSize ); Vec_IntPush( vFaninVars, Acb_ObjFunc(p, iObj) + nTfoSize );
// derive CNF for the node // derive CNF for the node
Acb_TranslateCnf( vClas, vLits, (Vec_Str_t *)Vec_WecEntry(vCnfs, iObj), vFaninVars, PivotVar ); Acb_TranslateCnf( vClas, vLits, (Vec_Str_t *)Vec_WecEntry(vCnfs, iObj), vFaninVars, PivotVar );
} }
...@@ -204,13 +208,13 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot ) ...@@ -204,13 +208,13 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
continue; continue;
iObj = Abc_Lit2Var(iObjLit); iObj = Abc_Lit2Var(iObjLit);
// add clauses // add clauses
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 0), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 0), Abc_Var2Lit(nVars, 0) ); Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjFunc(p, iObj), 1), Abc_Var2Lit(Acb_ObjFunc(p, iObj) + nTfoSize, 0), Abc_Var2Lit(nVars, 0) );
Vec_IntPush( vClas, Vec_IntSize(vLits) ); Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 1), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 1), Abc_Var2Lit(nVars, 0) ); Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjFunc(p, iObj), 0), Abc_Var2Lit(Acb_ObjFunc(p, iObj) + nTfoSize, 1), Abc_Var2Lit(nVars, 0) );
Vec_IntPush( vClas, Vec_IntSize(vLits) ); Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 0), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 1), Abc_Var2Lit(nVars, 1) ); Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjFunc(p, iObj), 0), Abc_Var2Lit(Acb_ObjFunc(p, iObj) + nTfoSize, 0), Abc_Var2Lit(nVars, 1) );
Vec_IntPush( vClas, Vec_IntSize(vLits) ); Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 1), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 0), Abc_Var2Lit(nVars, 1) ); Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjFunc(p, iObj), 1), Abc_Var2Lit(Acb_ObjFunc(p, iObj) + nTfoSize, 1), Abc_Var2Lit(nVars, 1) );
Vec_IntPush( vClas, Vec_IntSize(vLits) ); Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars++, 0) ); Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars++, 0) );
} }
...@@ -222,7 +226,7 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot ) ...@@ -222,7 +226,7 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
Vec_IntFree( vFaninVars ); Vec_IntFree( vFaninVars );
// undo SAT variables // undo SAT variables
Vec_IntForEachEntry( vWinObjs, iObj, i ) Vec_IntForEachEntry( vWinObjs, iObj, i )
Vec_IntWriteEntry( &p->vObjCopy, iObj, -1 ); Vec_IntWriteEntry( &p->vObjFunc, Abc_Lit2Var(iObj), -1 );
// create CNF structure // create CNF structure
pCnf = ABC_CALLOC( Cnf_Dat_t, 1 ); pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
pCnf->nVars = nVarsAll; pCnf->nVars = nVarsAll;
...@@ -235,6 +239,7 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot ) ...@@ -235,6 +239,7 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
// cleanup // cleanup
Vec_IntFree( vClas ); Vec_IntFree( vClas );
Vec_IntFree( vLits ); Vec_IntFree( vLits );
//Cnf_DataPrint( pCnf, 1 );
return pCnf; return pCnf;
} }
...@@ -252,7 +257,7 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot ) ...@@ -252,7 +257,7 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
***********************************************************************/ ***********************************************************************/
sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, int nTimes ) sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, int nTimes )
{ {
int n, i, RetValue, nRounds = nTimes <= 2 ? nTimes-1 : nTimes; int n, i, RetValue, nRounds = nTimes <= 2 ? nTimes-1 : 2;
Vec_Int_t * vFlips = Cnf_DataCollectFlipLits( pCnf, PivotVar ); Vec_Int_t * vFlips = Cnf_DataCollectFlipLits( pCnf, PivotVar );
sat_solver * pSat = sat_solver_new(); sat_solver * pSat = sat_solver_new();
sat_solver_setnvars( pSat, nTimes * pCnf->nVars + nRounds * nDivs + 1 ); sat_solver_setnvars( pSat, nTimes * pCnf->nVars + nRounds * nDivs + 1 );
...@@ -283,7 +288,7 @@ sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, in ...@@ -283,7 +288,7 @@ sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, in
{ {
int BaseA = n * pCnf->nVars; int BaseA = n * pCnf->nVars;
int BaseB = ((n + 1) % nTimes) * pCnf->nVars; int BaseB = ((n + 1) % nTimes) * pCnf->nVars;
int BaseC = nTimes * pCnf->nVars + n * nDivs; int BaseC = nTimes * pCnf->nVars + (n & 1) * nDivs;
for ( i = 0; i < nDivs; i++ ) for ( i = 0; i < nDivs; i++ )
sat_solver_add_buffer_enable( pSat, BaseA + i, BaseB + i, BaseC + i, 0 ); sat_solver_add_buffer_enable( pSat, BaseA + i, BaseB + i, BaseC + i, 0 );
} }
...@@ -298,6 +303,92 @@ sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, in ...@@ -298,6 +303,92 @@ sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, in
} }
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acb_NtkPrintVec( Acb_Ntk_t * p, Vec_Int_t * vVec, char * pName )
{
int i;
printf( "%s: ", pName );
for ( i = 0; i < vVec->nSize; i++ )
printf( "%d ", Vec_IntEntry(&p->vArray2, vVec->pArray[i]) );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Collects divisors in a non-topo order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, int nDivsMax )
{
Vec_Int_t * vDivs = Vec_IntAlloc( 100 );
Vec_Int_t * vFront = Vec_IntAlloc( 100 );
int i, k, iFanin, * pFanins;
// mark taboo nodes
Acb_NtkIncTravId( p );
assert( !Acb_ObjIsCio(p, Pivot) );
Acb_ObjSetTravIdCur( p, Pivot );
for ( i = 0; i < nTaboo; i++ )
{
assert( !Acb_ObjIsCio(p, pTaboo[i]) );
if ( Acb_ObjSetTravIdCur( p, pTaboo[i] ) )
assert( 0 );
}
// collect non-taboo fanins of pivot but do not use them as frontier
Acb_ObjForEachFaninFast( p, Pivot, pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur( p, iFanin ) )
Vec_IntPush( vDivs, iFanin );
// collect non-taboo fanins of taboo nodes and use them as frontier
for ( i = 0; i < nTaboo; i++ )
Acb_ObjForEachFaninFast( p, pTaboo[i], pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur( p, iFanin ) )
{
Vec_IntPush( vDivs, iFanin );
if ( !Acb_ObjIsCio(p, iFanin) )
Vec_IntPush( vFront, iFanin );
}
// select divisors incrementally
while ( Vec_IntSize(vFront) > 0 && Vec_IntSize(vDivs) < nDivsMax )
{
// select the topmost
int iObj, iObjMax = -1, LevelMax = -1;
Vec_IntForEachEntry( vFront, iObj, k )
if ( LevelMax < Acb_ObjLevelD(p, iObj) )
LevelMax = Acb_ObjLevelD(p, (iObjMax = iObj));
assert( iObjMax > 0 );
Vec_IntRemove( vFront, iObjMax );
// expand the topmost
Acb_ObjForEachFaninFast( p, iObjMax, pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur( p, iFanin ) )
{
Vec_IntPush( vDivs, iFanin );
if ( !Acb_ObjIsCio(p, iFanin) )
Vec_IntPush( vFront, iFanin );
}
}
Vec_IntFree( vFront );
// sort them by level
Vec_IntSelectSortCost( Vec_IntArray(vDivs), Vec_IntSize(vDivs), &p->vLevelD );
return vDivs;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Marks TFO of divisors.] Synopsis [Marks TFO of divisors.]
...@@ -314,7 +405,8 @@ void Acb_ObjMarkTfo_rec( Acb_Ntk_t * p, int iObj, int Pivot, int nTfoLevMax, int ...@@ -314,7 +405,8 @@ void Acb_ObjMarkTfo_rec( Acb_Ntk_t * p, int iObj, int Pivot, int nTfoLevMax, int
int iFanout, i; int iFanout, i;
if ( Acb_ObjSetTravIdCur(p, iObj) ) if ( Acb_ObjSetTravIdCur(p, iObj) )
return; return;
if ( Acb_ObjLevelD(p, iObj) > nTfoLevMax || Acb_ObjFanoutNum(p, iObj) >= nFanMax || iObj == Pivot ) //printf( "Labeling %d.\n", Vec_IntEntry(&p->vArray2, iObj) );
if ( Acb_ObjLevelD(p, iObj) > nTfoLevMax || Acb_ObjFanoutNum(p, iObj) > nFanMax || iObj == Pivot )
return; return;
Acb_ObjForEachFanout( p, iObj, iFanout, i ) Acb_ObjForEachFanout( p, iObj, iFanout, i )
Acb_ObjMarkTfo_rec( p, iFanout, Pivot, nTfoLevMax, nFanMax ); Acb_ObjMarkTfo_rec( p, iFanout, Pivot, nTfoLevMax, nFanMax );
...@@ -323,6 +415,7 @@ void Acb_ObjMarkTfo( Acb_Ntk_t * p, Vec_Int_t * vDivs, int Pivot, int nTfoLevMax ...@@ -323,6 +415,7 @@ void Acb_ObjMarkTfo( Acb_Ntk_t * p, Vec_Int_t * vDivs, int Pivot, int nTfoLevMax
{ {
int i, iObj; int i, iObj;
Acb_NtkIncTravId( p ); Acb_NtkIncTravId( p );
Acb_ObjSetTravIdCur( p, Pivot );
Vec_IntForEachEntry( vDivs, iObj, i ) Vec_IntForEachEntry( vDivs, iObj, i )
Acb_ObjMarkTfo_rec( p, iObj, Pivot, nTfoLevMax, nFanMax ); Acb_ObjMarkTfo_rec( p, iObj, Pivot, nTfoLevMax, nFanMax );
} }
...@@ -341,6 +434,7 @@ void Acb_ObjMarkTfo( Acb_Ntk_t * p, Vec_Int_t * vDivs, int Pivot, int nTfoLevMax ...@@ -341,6 +434,7 @@ void Acb_ObjMarkTfo( Acb_Ntk_t * p, Vec_Int_t * vDivs, int Pivot, int nTfoLevMax
int Acb_ObjLabelTfo_rec( Acb_Ntk_t * p, int iObj, int nTfoLevMax, int nFanMax ) int Acb_ObjLabelTfo_rec( Acb_Ntk_t * p, int iObj, int nTfoLevMax, int nFanMax )
{ {
int iFanout, i, Diff, fHasNone = 0; int iFanout, i, Diff, fHasNone = 0;
//printf( "Visiting %d\n", Vec_IntEntry(&p->vArray2, iObj) );
if ( (Diff = Acb_ObjTravIdDiff(p, iObj)) <= 2 ) if ( (Diff = Acb_ObjTravIdDiff(p, iObj)) <= 2 )
return Diff; return Diff;
Acb_ObjSetTravIdDiff( p, iObj, 2 ); Acb_ObjSetTravIdDiff( p, iObj, 2 );
...@@ -348,15 +442,15 @@ int Acb_ObjLabelTfo_rec( Acb_Ntk_t * p, int iObj, int nTfoLevMax, int nFanMax ) ...@@ -348,15 +442,15 @@ int Acb_ObjLabelTfo_rec( Acb_Ntk_t * p, int iObj, int nTfoLevMax, int nFanMax )
return 2; return 2;
if ( Acb_ObjLevelD(p, iObj) == nTfoLevMax || Acb_ObjFanoutNum(p, iObj) >= nFanMax ) if ( Acb_ObjLevelD(p, iObj) == nTfoLevMax || Acb_ObjFanoutNum(p, iObj) >= nFanMax )
{ {
if ( Diff == 3 ) if ( Diff == 3 ) // belongs to TFO of TFI
Acb_ObjSetTravIdDiff( p, iObj, 1 ); // mark root Acb_ObjSetTravIdDiff( p, iObj, 1 ); // root
return Acb_ObjTravIdDiff(p, iObj); return Acb_ObjTravIdDiff(p, iObj);
} }
Acb_ObjForEachFanout( p, iObj, iFanout, i ) Acb_ObjForEachFanout( p, iObj, iFanout, i )
fHasNone |= 2 == Acb_ObjLabelTfo_rec( p, iFanout, nTfoLevMax, nFanMax ); fHasNone |= 2 == Acb_ObjLabelTfo_rec( p, iFanout, nTfoLevMax, nFanMax );
if ( fHasNone && Diff == 3 ) if ( fHasNone && Diff == 3 ) // belongs to TFO of TFI
Acb_ObjSetTravIdDiff( p, iObj, 1 ); // root Acb_ObjSetTravIdDiff( p, iObj, 1 ); // root
else else if ( !fHasNone )
Acb_ObjSetTravIdDiff( p, iObj, 0 ); // inner Acb_ObjSetTravIdDiff( p, iObj, 0 ); // inner
return Acb_ObjTravIdDiff(p, iObj); return Acb_ObjTravIdDiff(p, iObj);
} }
...@@ -365,7 +459,7 @@ int Acb_ObjLabelTfo( Acb_Ntk_t * p, int Root, int nTfoLevMax, int nFanMax ) ...@@ -365,7 +459,7 @@ int Acb_ObjLabelTfo( Acb_Ntk_t * p, int Root, int nTfoLevMax, int nFanMax )
Acb_NtkIncTravId( p ); // none (2) marked (3) unmarked (4) Acb_NtkIncTravId( p ); // none (2) marked (3) unmarked (4)
Acb_NtkIncTravId( p ); // root (1) Acb_NtkIncTravId( p ); // root (1)
Acb_NtkIncTravId( p ); // inner (0) Acb_NtkIncTravId( p ); // inner (0)
assert( Acb_ObjTravIdDiff(p, Root) < 3 ); assert( Acb_ObjTravIdDiff(p, Root) > 2 );
return Acb_ObjLabelTfo_rec( p, Root, nTfoLevMax, nFanMax ); return Acb_ObjLabelTfo_rec( p, Root, nTfoLevMax, nFanMax );
} }
...@@ -387,19 +481,20 @@ void Acb_ObjDeriveTfo_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfo, Vec_Int_t ...@@ -387,19 +481,20 @@ void Acb_ObjDeriveTfo_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfo, Vec_Int_t
return; return;
if ( Diff == 2 ) // root if ( Diff == 2 ) // root
{ {
Vec_IntPush( vRoots, Diff ); Vec_IntPush( vRoots, iObj );
Vec_IntPush( vTfo, iObj );
return; return;
} }
assert( Diff == 1 ); assert( Diff == 1 );
Acb_ObjForEachFanout( p, iObj, iFanout, i ) Acb_ObjForEachFanout( p, iObj, iFanout, i )
Acb_ObjDeriveTfo_rec( p, iFanout, vTfo, vRoots ); Acb_ObjDeriveTfo_rec( p, iFanout, vTfo, vRoots );
Vec_IntPush( vTfo, Diff ); Vec_IntPush( vTfo, iObj );
} }
void Acb_ObjDeriveTfo( Acb_Ntk_t * p, int Pivot, int nTfoLevMax, int nFanMax, Vec_Int_t ** pvTfo, Vec_Int_t ** pvRoots ) void Acb_ObjDeriveTfo( Acb_Ntk_t * p, int Pivot, int nTfoLevMax, int nFanMax, Vec_Int_t ** pvTfo, Vec_Int_t ** pvRoots )
{ {
int Res = Acb_ObjLabelTfo( p, Pivot, nTfoLevMax, nFanMax ); int Res = Acb_ObjLabelTfo( p, Pivot, nTfoLevMax, nFanMax );
Vec_Int_t * vTfo = *pvTfo = Vec_IntAlloc( 100 ); Vec_Int_t * vTfo = *pvTfo = Vec_IntAlloc( 10 );
Vec_Int_t * vRoots = *pvRoots = Vec_IntAlloc( 100 ); Vec_Int_t * vRoots = *pvRoots = Vec_IntAlloc( 10 );
if ( Res ) // none or root if ( Res ) // none or root
return; return;
Acb_NtkIncTravId( p ); // root (2) inner (1) visited (0) Acb_NtkIncTravId( p ); // root (2) inner (1) visited (0)
...@@ -472,15 +567,18 @@ void Acb_NtkCollectNewTfi2_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfiNew ) ...@@ -472,15 +567,18 @@ void Acb_NtkCollectNewTfi2_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfiNew )
Acb_NtkCollectNewTfi2_rec( p, iFanin, vTfiNew ); Acb_NtkCollectNewTfi2_rec( p, iFanin, vTfiNew );
Vec_IntPush( vTfiNew, iObj ); Vec_IntPush( vTfiNew, iObj );
} }
Vec_Int_t * Acb_NtkCollectNewTfi( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vDivs, Vec_Int_t * vSide ) Vec_Int_t * Acb_NtkCollectNewTfi( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vDivs, Vec_Int_t * vSide, int * pnDivs )
{ {
Vec_Int_t * vTfiNew = Vec_IntAlloc( 100 ); Vec_Int_t * vTfiNew = Vec_IntAlloc( 100 );
int i, Node; int i, Node;
Acb_NtkIncTravId( p ); Acb_NtkIncTravId( p );
//Acb_NtkPrintVec( p, vDivs, "vDivs" );
Vec_IntForEachEntry( vDivs, Node, i ) Vec_IntForEachEntry( vDivs, Node, i )
Acb_NtkCollectNewTfi1_rec( p, Node, vTfiNew ); Acb_NtkCollectNewTfi1_rec( p, Node, vTfiNew );
assert( Vec_IntSize(vTfiNew) == Vec_IntSize(vDivs) ); *pnDivs = Vec_IntSize(vTfiNew);
//Acb_NtkPrintVec( p, vTfiNew, "vTfiNew" );
Acb_NtkCollectNewTfi1_rec( p, Pivot, vTfiNew ); Acb_NtkCollectNewTfi1_rec( p, Pivot, vTfiNew );
//Acb_NtkPrintVec( p, vTfiNew, "vTfiNew" );
assert( Vec_IntEntryLast(vTfiNew) == Pivot ); assert( Vec_IntEntryLast(vTfiNew) == Pivot );
Vec_IntPop( vTfiNew ); Vec_IntPop( vTfiNew );
Vec_IntForEachEntry( vSide, Node, i ) Vec_IntForEachEntry( vSide, Node, i )
...@@ -505,95 +603,32 @@ Vec_Int_t * Acb_NtkCollectWindow( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vTfi, Ve ...@@ -505,95 +603,32 @@ Vec_Int_t * Acb_NtkCollectWindow( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vTfi, Ve
Vec_Int_t * vWin = Vec_IntAlloc( 100 ); Vec_Int_t * vWin = Vec_IntAlloc( 100 );
int i, k, iObj, iFanin, * pFanins; int i, k, iObj, iFanin, * pFanins;
assert( Vec_IntEntryLast(vTfi) == Pivot ); assert( Vec_IntEntryLast(vTfi) == Pivot );
// mark leaves // mark nodes
Acb_NtkIncTravId( p ); Acb_NtkIncTravId( p );
Vec_IntForEachEntry( vTfi, iObj, i ) Vec_IntForEachEntry( vTfi, iObj, i )
Acb_ObjSetTravIdCur(p, iObj); Acb_ObjSetTravIdCur(p, iObj);
Acb_NtkIncTravId( p );
Vec_IntForEachEntry( vTfi, iObj, i )
if ( !Acb_ObjIsCi(p, iObj) )
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
if ( !Acb_ObjIsTravIdCur(p, iFanin) )
Acb_ObjSetTravIdCur(p, iObj);
// add TFI // add TFI
Vec_IntForEachEntry( vTfi, iObj, i ) Vec_IntForEachEntry( vTfi, iObj, i )
Vec_IntPush( vWin, Abc_Var2Lit( iObj, Acb_ObjIsTravIdCur(p, iObj)) ); {
int fIsTfiInput = 0;
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
if ( !Acb_ObjIsTravIdCur(p, iFanin) ) // fanin is not in TFI
fIsTfiInput = 1; // mark as leaf
Vec_IntPush( vWin, Abc_Var2Lit(iObj, Acb_ObjIsCi(p, iObj) || fIsTfiInput) );
}
// mark roots // mark roots
Acb_NtkIncTravId( p );
Vec_IntForEachEntry( vRoots, iObj, i ) Vec_IntForEachEntry( vRoots, iObj, i )
Acb_ObjSetTravIdCur(p, iObj); Acb_ObjSetTravIdCur(p, iObj);
// add TFO // add TFO
Vec_IntForEachEntry( vTfo, iObj, i ) Vec_IntForEachEntry( vTfo, iObj, i )
Vec_IntPush( vWin, Abc_Var2Lit( iObj, Acb_ObjIsTravIdCur(p, iObj)) );
return vWin;
}
/**Function*************************************************************
Synopsis [Collects divisors in a non-topo order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, int nDivsMax )
{
Vec_Int_t * vDivs = Vec_IntAlloc( 100 );
Vec_Int_t * vFront = Vec_IntAlloc( 100 );
int i, k, iFanin, * pFanins;
// mark taboo nodes
Acb_NtkIncTravId( p );
assert( !Acb_ObjIsCio(p, Pivot) );
Acb_ObjSetTravIdCur( p, Pivot );
for ( i = 0; i < nTaboo; i++ )
{
assert( !Acb_ObjIsCio(p, pTaboo[i]) );
if ( Acb_ObjSetTravIdCur( p, pTaboo[i] ) )
assert( 0 );
}
// collect non-taboo fanins of pivot but do not use them as frontier
Acb_ObjForEachFaninFast( p, Pivot, pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur( p, iFanin ) )
Vec_IntPush( vDivs, iFanin );
// collect non-tabook fanins of taboo nodes and use them as frontier
for ( i = 0; i < nTaboo; i++ )
Acb_ObjForEachFaninFast( p, pTaboo[i], pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur( p, iFanin ) )
{ {
Vec_IntPush( vDivs, iFanin ); assert( !Acb_ObjIsCo(p, iObj) );
if ( !Acb_ObjIsCio(p, iFanin) ) Vec_IntPush( vWin, Abc_Var2Lit(iObj, Acb_ObjIsTravIdCur(p, iObj)) );
Vec_IntPush( vFront, iFanin );
} }
// select divisors incrementally return vWin;
while ( Vec_IntSize(vFront) > 0 && Vec_IntSize(vDivs) < nDivsMax )
{
// select the topmost
int iObj, iObjMax = -1, LevelMax = -1;
Vec_IntForEachEntry( vFront, iObj, k )
if ( LevelMax < Acb_ObjLevelD(p, iObj) )
LevelMax = Acb_ObjLevelD(p, (iObjMax = iObj));
assert( iObjMax > 0 );
Vec_IntRemove( vFront, iObjMax );
// expand the topmost
Acb_ObjForEachFaninFast( p, iObjMax, pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur( p, iFanin ) )
{
Vec_IntPush( vDivs, iFanin );
if ( !Acb_ObjIsCio(p, iFanin) )
Vec_IntPush( vFront, iFanin );
}
}
Vec_IntFree( vFront );
// sort them by level
Vec_IntSelectSortCost( Vec_IntArray(vDivs), Vec_IntSize(vDivs), &p->vLevelD );
return vDivs;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
...@@ -607,20 +642,26 @@ Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, ...@@ -607,20 +642,26 @@ Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo,
***********************************************************************/ ***********************************************************************/
Vec_Int_t * Acb_NtkWindow( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, int nDivsMax, int nTfoLevs, int nFanMax, int * pnDivs ) Vec_Int_t * Acb_NtkWindow( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, int nDivsMax, int nTfoLevs, int nFanMax, int * pnDivs )
{ {
int fVerbose = 0;
int nTfoLevMax = Acb_ObjLevelD(p, Pivot) + nTfoLevs; int nTfoLevMax = Acb_ObjLevelD(p, Pivot) + nTfoLevs;
Vec_Int_t * vWin, * vDivs, * vTfo, * vRoots, * vSide, * vTfi; Vec_Int_t * vWin, * vDivs, * vTfo, * vRoots, * vSide, * vTfi;
// collect divisors by traversing limited TFI // collect divisors by traversing limited TFI
vDivs = Acb_NtkDivisors( p, Pivot, pTaboo, nTaboo, nDivsMax ); vDivs = Acb_NtkDivisors( p, Pivot, pTaboo, nTaboo, nDivsMax );
if ( fVerbose ) Acb_NtkPrintVec( p, vDivs, "vDivs" );
// mark limited TFO of the divisors // mark limited TFO of the divisors
Acb_ObjMarkTfo( p, vDivs, Pivot, nTfoLevMax, nFanMax ); Acb_ObjMarkTfo( p, vDivs, Pivot, nTfoLevMax, nFanMax );
// collect TFO and roots // collect TFO and roots
Acb_ObjDeriveTfo( p, Pivot, nTfoLevMax, nFanMax, &vTfo, &vRoots ); Acb_ObjDeriveTfo( p, Pivot, nTfoLevMax, nFanMax, &vTfo, &vRoots );
if ( fVerbose ) Acb_NtkPrintVec( p, vTfo, "vTfo" );
if ( fVerbose ) Acb_NtkPrintVec( p, vRoots, "vRoots" );
// collect side inputs of the TFO // collect side inputs of the TFO
vSide = Acb_NtkCollectTfoSideInputs( p, Pivot, vTfo ); vSide = Acb_NtkCollectTfoSideInputs( p, Pivot, vTfo );
if ( fVerbose ) Acb_NtkPrintVec( p, vSide, "vSide" );
// mark limited TFO of the divisors // mark limited TFO of the divisors
Acb_ObjMarkTfo( p, vDivs, Pivot, nTfoLevMax, nFanMax ); Acb_ObjMarkTfo( p, vDivs, Pivot, nTfoLevMax, nFanMax );
// collect new TFI // collect new TFI
vTfi = Acb_NtkCollectNewTfi( p, Pivot, vDivs, vSide ); vTfi = Acb_NtkCollectNewTfi( p, Pivot, vDivs, vSide, pnDivs );
if ( fVerbose ) Acb_NtkPrintVec( p, vTfi, "vTfi" );
Vec_IntFree( vSide ); Vec_IntFree( vSide );
Vec_IntFree( vDivs ); Vec_IntFree( vDivs );
// collect all nodes // collect all nodes
...@@ -636,34 +677,6 @@ Vec_Int_t * Acb_NtkWindow( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, i ...@@ -636,34 +677,6 @@ Vec_Int_t * Acb_NtkWindow( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, i
/**Function************************************************************* /**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Acb_NtkFindSupp( sat_solver * pSat, Acb_Ntk_t * p, Vec_Int_t * vWin, Vec_Int_t * vDivs, int nBTLimit )
{
int i, iObj, nDivsNew;
// reload divisors in terms of SAT variables
Vec_IntForEachEntry( vDivs, iObj, i )
Vec_IntWriteEntry( vDivs, i, Acb_ObjCopy(p, iObj) );
// try solving
nDivsNew = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vDivs), Vec_IntSize(vDivs), nBTLimit );
Vec_IntShrink( vDivs, nDivsNew );
// reload divisors in terms of network variables
Vec_IntForEachEntry( vDivs, iObj, i )
Vec_IntWriteEntry( vDivs, i, Vec_IntEntry(vWin, iObj) );
return Vec_IntSize(vDivs);
}
/**Function*************************************************************
Synopsis [Computes function of the node] Synopsis [Computes function of the node]
Description [] Description []
...@@ -704,7 +717,6 @@ word Acb_ComputeFunction( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_ ...@@ -704,7 +717,6 @@ word Acb_ComputeFunction( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_
// compute cube and add clause // compute cube and add clause
nFinal = sat_solver_final( pSat, &pFinal ); nFinal = sat_solver_final( pSat, &pFinal );
Vec_IntFill( vTempLits, 1, Abc_LitNot(pLits[1]) ); // NOT(iNewLit) Vec_IntFill( vTempLits, 1, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
uCube = ~(word)0;
for ( i = 0; i < nFinal; i++ ) for ( i = 0; i < nFinal; i++ )
if ( pFinal[i] != pLits[0] ) if ( pFinal[i] != pLits[0] )
Vec_IntPush( vTempLits, pFinal[i] ); Vec_IntPush( vTempLits, pFinal[i] );
...@@ -716,7 +728,8 @@ word Acb_ComputeFunction( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_ ...@@ -716,7 +728,8 @@ word Acb_ComputeFunction( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_
Vec_IntForEachEntry( vDivVars, iVar, i ) Vec_IntForEachEntry( vDivVars, iVar, i )
Vec_IntPush( vTempLits, Abc_LitNot(sat_solver_var_literal(pSat, iVar)) ); Vec_IntPush( vTempLits, Abc_LitNot(sat_solver_var_literal(pSat, iVar)) );
} }
Vec_IntForEachEntry( vTempLits, iLit, i ) uCube = ~(word)0;
Vec_IntForEachEntryStart( vTempLits, iLit, i, 1 )
{ {
iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(iLit) ); assert( iVar >= 0 ); iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(iLit) ); assert( iVar >= 0 );
uCube &= Abc_LitIsCompl(iLit) ? s_Truths6[iVar] : ~s_Truths6[iVar]; uCube &= Abc_LitIsCompl(iLit) ? s_Truths6[iVar] : ~s_Truths6[iVar];
...@@ -736,7 +749,7 @@ word Acb_ComputeFunction( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_ ...@@ -736,7 +749,7 @@ word Acb_ComputeFunction( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_
/**Function************************************************************* /**Function*************************************************************
Synopsis [Collects the taboo nodes.] Synopsis [Collects the taboo nodes (nodes that cannot be divisors).]
Description [] Description []
...@@ -820,6 +833,12 @@ int Acb_NtkCollectTaboo( Acb_Ntk_t * p, int Pivot, int nTabooMax, int * pTaboo ) ...@@ -820,6 +833,12 @@ int Acb_NtkCollectTaboo( Acb_Ntk_t * p, int Pivot, int nTabooMax, int * pTaboo )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline void Vec_IntVars2Vars( Vec_Int_t * p, int Shift )
{
int i;
for ( i = 0; i < p->nSize; i++ )
p->pArray[i] += Shift;
}
static inline void Vec_IntVars2Lits( Vec_Int_t * p, int Shift, int fCompl ) static inline void Vec_IntVars2Lits( Vec_Int_t * p, int Shift, int fCompl )
{ {
int i; int i;
...@@ -830,7 +849,7 @@ static inline void Vec_IntLits2Vars( Vec_Int_t * p, int Shift ) ...@@ -830,7 +849,7 @@ static inline void Vec_IntLits2Vars( Vec_Int_t * p, int Shift )
{ {
int i; int i;
for ( i = 0; i < p->nSize; i++ ) for ( i = 0; i < p->nSize; i++ )
p->pArray[i] = Abc_Lit2Var( p->pArray[i] ) - Shift; p->pArray[i] = Abc_Lit2Var( p->pArray[i] ) + Shift;
} }
static inline void Vec_IntRemap( Vec_Int_t * p, Vec_Int_t * vMap ) static inline void Vec_IntRemap( Vec_Int_t * p, Vec_Int_t * vMap )
{ {
...@@ -839,21 +858,53 @@ static inline void Vec_IntRemap( Vec_Int_t * p, Vec_Int_t * vMap ) ...@@ -839,21 +858,53 @@ static inline void Vec_IntRemap( Vec_Int_t * p, Vec_Int_t * vMap )
p->pArray[i] = Vec_IntEntry(vMap, p->pArray[i]); p->pArray[i] = Vec_IntEntry(vMap, p->pArray[i]);
} }
void Acb_NtkOptNode( Acb_Ntk_t * p, int Pivot, int nTabooMax, int nDivMax, int nTfoLevs, int nFanMax, int nLutSize ) void Acb_WinPrint( Acb_Ntk_t * p, Vec_Int_t * vWin, int Pivot, int nDivs )
{
int i, Node;
printf( "Window for node %d with %d divisors:\n", Vec_IntEntry(&p->vArray2, Pivot), nDivs );
Vec_IntForEachEntry( vWin, Node, i )
{
if ( i == nDivs )
printf( " | " );
if ( Abc_Lit2Var(Node) == Pivot )
printf( "(%d) ", Vec_IntEntry(&p->vArray2, Pivot) );
else
printf( "%s%d ", Abc_LitIsCompl(Node) ? "*":"", Vec_IntEntry(&p->vArray2, Abc_Lit2Var(Node)) );
}
printf( "\n" );
}
Vec_Int_t * Acb_NtkFindSupp( Acb_Ntk_t * p, sat_solver * pSat2, int nVars, int nDivs )
{
int nSuppNew;
Vec_Int_t * vSupp = Vec_IntStartNatural( nDivs );
Vec_IntReverseOrder( vSupp );
Vec_IntVars2Lits( vSupp, 2*nVars, 0 );
nSuppNew = sat_solver_minimize_assumptions( pSat2, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 );
Vec_IntShrink( vSupp, nSuppNew );
Vec_IntLits2Vars( vSupp, -2*nVars );
return vSupp;
}
void Acb_NtkOptNode( Acb_Ntk_t * p, int Pivot, int nTabooMax, int nDivMax, int nTfoLevs, int nFanMax, int nLutSize, int fVerbose )
{ {
Cnf_Dat_t * pCnf; Cnf_Dat_t * pCnf;
Vec_Int_t * vWin, * vSupp = NULL; Vec_Int_t * vWin, * vSupp = NULL;
sat_solver * pSat1 = NULL, * pSat2 = NULL, * pSat3 = NULL; sat_solver * pSat1 = NULL, * pSat2 = NULL, * pSat3 = NULL;
int c, nSuppNew, PivotVar, nDivs = 0; int c, PivotVar, nDivs = 0; word uTruth;
int pTaboo[16], nTaboo = Acb_NtkCollectTaboo( p, Pivot, nTabooMax, pTaboo ); int pTaboo[16], nTaboo = Acb_NtkCollectTaboo( p, Pivot, nTabooMax, pTaboo );
if ( nTaboo == 0 ) if ( nTaboo == 0 )
return; return;
assert( nTabooMax == 0 || nTaboo <= nTabooMax ); assert( nTabooMax == 0 || nTaboo <= nTabooMax );
assert( nTaboo <= 16 ); assert( nTaboo <= 16 );
// compute divisor and window for these nodes // compute divisors and window for this target node with these taboo nodes
vWin = Acb_NtkWindow( p, Pivot, pTaboo, nTaboo, nDivMax, nTfoLevs, nFanMax, &nDivs ); vWin = Acb_NtkWindow( p, Pivot, pTaboo, nTaboo, nDivMax, nTfoLevs, nFanMax, &nDivs );
PivotVar = Vec_IntFind(vWin, Abc_Var2Lit(Pivot, 0)); PivotVar = Vec_IntFind( vWin, Abc_Var2Lit(Pivot, 0) );
if ( fVerbose )
printf( "Node %d: Window contains %d objects and %d divisors. ", Vec_IntEntry(&p->vArray2, Pivot), Vec_IntSize(vWin), nDivs );
// Acb_WinPrint( p, vWin, Pivot, nDivs );
// return;
// derive CNF and SAT solvers // derive CNF and SAT solvers
pCnf = Acb_NtkWindow2Cnf( p, vWin, Pivot ); pCnf = Acb_NtkWindow2Cnf( p, vWin, Pivot );
...@@ -865,66 +916,84 @@ void Acb_NtkOptNode( Acb_Ntk_t * p, int Pivot, int nTabooMax, int nDivMax, int n ...@@ -865,66 +916,84 @@ void Acb_NtkOptNode( Acb_Ntk_t * p, int Pivot, int nTabooMax, int nDivMax, int n
int status = sat_solver_solve( pSat1, &Lit, &Lit + 1, 0, 0, 0, 0 ); int status = sat_solver_solve( pSat1, &Lit, &Lit + 1, 0, 0, 0, 0 );
if ( status == l_False ) if ( status == l_False )
{ {
if ( fVerbose )
printf( "Found constant %d.\n", c );
Acb_NtkUpdateNode( p, Pivot, c ? ~(word)0 : 0, NULL ); Acb_NtkUpdateNode( p, Pivot, c ? ~(word)0 : 0, NULL );
goto cleanup; goto cleanup;
} }
assert( status == l_True ); assert( status == l_True );
} }
// check for one-node implementation
pSat2 = Acb_NtkWindow2Solver( pCnf, PivotVar, nDivs, 2 ); pSat2 = Acb_NtkWindow2Solver( pCnf, PivotVar, nDivs, 2 );
//pSat6 = Acb_NtkWindow2Solver( pCnf, PivotVar, nDivs, 6 ); vSupp = Acb_NtkFindSupp( p, pSat2, pCnf->nVars, nDivs );
if ( Vec_IntSize(vSupp) <= nLutSize )
// try solving the original support {
vSupp = Vec_IntStartNatural( nDivs ); if ( fVerbose )
Vec_IntVars2Lits( vSupp, 2*pCnf->nVars, 0 ); printf( "Found %d inputs: ", Vec_IntSize(vSupp) );
nSuppNew = sat_solver_minimize_assumptions( pSat2, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 ); uTruth = Acb_ComputeFunction( pSat1, PivotVar, sat_solver_nvars(pSat1)-1, vSupp );
Vec_IntShrink( vSupp, nSuppNew ); if ( fVerbose )
Vec_IntLits2Vars( vSupp, -2*pCnf->nVars ); Extra_PrintHex( stdout, (unsigned *)&uTruth, Vec_IntSize(vSupp) );
if ( fVerbose )
if ( nSuppNew <= nLutSize ) printf( "\n" );
{
int FreeVar = sat_solver_nvars( pSat1 ) - 1;
word uTruth;
Vec_IntVars2Lits( vSupp, pCnf->nVars, 0 );
uTruth = Acb_ComputeFunction( pSat1, PivotVar, FreeVar, vSupp );
Vec_IntLits2Vars( vSupp, -pCnf->nVars );
// create support in terms of nodes // create support in terms of nodes
Vec_IntRemap( vSupp, vWin ); Vec_IntRemap( vSupp, vWin );
Vec_IntLits2Vars( vSupp, 0 ); Vec_IntLits2Vars( vSupp, 0 );
Acb_NtkUpdateNode( p, Pivot, uTruth, vSupp ); Acb_NtkUpdateNode( p, Pivot, uTruth, vSupp );
goto cleanup; goto cleanup;
} }
if ( fVerbose )
printf( "\n" );
// cleanup
cleanup: cleanup:
if ( pSat1 ) sat_solver_delete( pSat1 ); if ( pSat1 ) sat_solver_delete( pSat1 );
if ( pSat2 ) sat_solver_delete( pSat2 ); if ( pSat2 ) sat_solver_delete( pSat2 );
if ( pSat3 ) sat_solver_delete( pSat3 ); if ( pSat3 ) sat_solver_delete( pSat3 );
Cnf_DataFree( pCnf ); Cnf_DataFree( pCnf );
Vec_IntFree( vWin ); Vec_IntFree( vWin );
Vec_IntFree( vSupp ); Vec_IntFreeP( &vSupp );
} }
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acb_NtkOpt( Acb_Ntk_t * p, Acb_Par_t * pPars ) void Acb_NtkOpt( Acb_Ntk_t * p, Acb_Par_t * pPars )
{ {
int iObj; if ( pPars->fVerbose )
printf( "Performing %s-oriented optimization with DivMax = %d. TfoLev = %d. LutSize = %d.\n",
pPars->fArea ? "area" : "delay", pPars->nDivMax, pPars->nTfoLevMax, pPars->nLutSize );
Acb_NtkCreateFanout( p ); // fanout data structure
Acb_NtkCleanObjFuncs( p ); // SAT variables
Acb_NtkCleanObjCnfs( p ); // CNF representations
if ( pPars->fArea ) if ( pPars->fArea )
{ {
int iObj;
Acb_NtkUpdateLevelD( p, -1 ); // compute forward logic level
Acb_NtkForEachNode( p, iObj ) Acb_NtkForEachNode( p, iObj )
Acb_NtkOptNode( p, iObj, pPars->nTabooMax, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize ); {
//if ( iObj != 433 )
// continue;
Acb_NtkOptNode( p, iObj, pPars->nTabooMax, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize, pPars->fVerbose );
}
} }
else else
{ {
Acb_NtkUpdateTiming( p, -1 ); Acb_NtkUpdateTiming( p, -1 ); // compute delay information
while ( 1 ) while ( Vec_QueTopPriority(p->vQue) > 0 )
{ {
int iObj = 0; int iObj = Vec_QuePop(p->vQue);
Acb_NtkOptNode( p, iObj, 0, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize ); //if ( iObj != 28 )
// continue;
Acb_NtkOptNode( p, iObj, 0, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize, pPars->fVerbose );
} }
} }
} }
......
src/base/acb/acbUtil.c
...@@ -33,38 +33,7 @@ ABC_NAMESPACE_IMPL_START ...@@ -33,38 +33,7 @@ ABC_NAMESPACE_IMPL_START
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Collecting TFI and TFO.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acb_ObjAddFanout( Acb_Ntk_t * p, int iObj )
{
int k, iFanin, * pFanins;
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntPush( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
}
void Acb_ObjRemoveFanout( Acb_Ntk_t * p, int iObj )
{
int k, iFanin, * pFanins;
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
}
void Acb_NtkCreateFanout( Acb_Ntk_t * p )
{
int iObj;
Vec_WecInit( &p->vFanouts, Acb_NtkObjNumMax(p) );
Acb_NtkForEachObj( p, iObj )
Acb_ObjAddFanout( p, iObj );
}
/**Function*************************************************************
Synopsis []
Description [] Description []
...@@ -86,8 +55,13 @@ void Acb_ObjCollectTfi_rec( Acb_Ntk_t * p, int iObj, int fTerm ) ...@@ -86,8 +55,13 @@ void Acb_ObjCollectTfi_rec( Acb_Ntk_t * p, int iObj, int fTerm )
} }
Vec_Int_t * Acb_ObjCollectTfi( Acb_Ntk_t * p, int iObj, int fTerm ) Vec_Int_t * Acb_ObjCollectTfi( Acb_Ntk_t * p, int iObj, int fTerm )
{ {
int i;
Vec_IntClear( &p->vArray0 ); Vec_IntClear( &p->vArray0 );
Acb_NtkIncTravId( p ); Acb_NtkIncTravId( p );
if ( iObj > 0 )
Acb_ObjCollectTfi_rec( p, iObj, fTerm );
else
Acb_NtkForEachCo( p, iObj, i )
Acb_ObjCollectTfi_rec( p, iObj, fTerm ); Acb_ObjCollectTfi_rec( p, iObj, fTerm );
return &p->vArray0; return &p->vArray0;
} }
...@@ -105,16 +79,20 @@ void Acb_ObjCollectTfo_rec( Acb_Ntk_t * p, int iObj, int fTerm ) ...@@ -105,16 +79,20 @@ void Acb_ObjCollectTfo_rec( Acb_Ntk_t * p, int iObj, int fTerm )
} }
Vec_Int_t * Acb_ObjCollectTfo( Acb_Ntk_t * p, int iObj, int fTerm ) Vec_Int_t * Acb_ObjCollectTfo( Acb_Ntk_t * p, int iObj, int fTerm )
{ {
int i;
Vec_IntClear( &p->vArray1 ); Vec_IntClear( &p->vArray1 );
Acb_NtkIncTravId( p ); Acb_NtkIncTravId( p );
if ( iObj > 0 )
Acb_ObjCollectTfo_rec( p, iObj, fTerm );
else
Acb_NtkForEachCi( p, iObj, i )
Acb_ObjCollectTfo_rec( p, iObj, fTerm ); Acb_ObjCollectTfo_rec( p, iObj, fTerm );
return &p->vArray1; return &p->vArray1;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Computing and updating direct and reverse logic level.]
Description [] Description []
...@@ -132,19 +110,12 @@ int Acb_ObjComputeLevelD( Acb_Ntk_t * p, int iObj ) ...@@ -132,19 +110,12 @@ int Acb_ObjComputeLevelD( Acb_Ntk_t * p, int iObj )
} }
int Acb_NtkComputeLevelD( Acb_Ntk_t * p, Vec_Int_t * vTfo ) int Acb_NtkComputeLevelD( Acb_Ntk_t * p, Vec_Int_t * vTfo )
{ {
// it is assumed that vTfo contains CO nodes and level of new nodes was already updated
int i, iObj, Level = 0; int i, iObj, Level = 0;
if ( vTfo == NULL ) if ( !Acb_NtkHasObjLevelD( p ) )
{
Acb_NtkCleanObjLevelD( p ); Acb_NtkCleanObjLevelD( p );
Acb_NtkForEachObj( p, iObj ) Vec_IntForEachEntryReverse( vTfo, iObj, i )
Acb_ObjComputeLevelD( p, iObj ); Acb_ObjComputeLevelD( p, iObj );
}
else
{
// it is assumed that vTfo contains CO nodes and level of new nodes was already updated
Vec_IntForEachEntry( vTfo, iObj, i )
Acb_ObjComputeLevelD( p, iObj );
}
Acb_NtkForEachCo( p, iObj, i ) Acb_NtkForEachCo( p, iObj, i )
Level = Abc_MaxInt( Level, Acb_ObjLevelD(p, iObj) ); Level = Abc_MaxInt( Level, Acb_ObjLevelD(p, iObj) );
p->LevelMax = Level; p->LevelMax = Level;
...@@ -160,28 +131,27 @@ int Acb_ObjComputeLevelR( Acb_Ntk_t * p, int iObj ) ...@@ -160,28 +131,27 @@ int Acb_ObjComputeLevelR( Acb_Ntk_t * p, int iObj )
} }
int Acb_NtkComputeLevelR( Acb_Ntk_t * p, Vec_Int_t * vTfi ) int Acb_NtkComputeLevelR( Acb_Ntk_t * p, Vec_Int_t * vTfi )
{ {
int i, iObj, Level = 0;
if ( vTfi == NULL )
{
Acb_NtkCleanObjLevelR( p );
Acb_NtkForEachObjReverse( p, iObj )
Acb_ObjComputeLevelR( p, iObj );
}
else
{
// it is assumed that vTfi contains CI nodes // it is assumed that vTfi contains CI nodes
int i, iObj, Level = 0;
if ( !Acb_NtkHasObjLevelD( p ) )
Acb_NtkCleanObjLevelD( p );
Vec_IntForEachEntryReverse( vTfi, iObj, i ) Vec_IntForEachEntryReverse( vTfi, iObj, i )
Acb_ObjComputeLevelR( p, iObj ); Acb_ObjComputeLevelR( p, iObj );
}
Acb_NtkForEachCi( p, iObj, i ) Acb_NtkForEachCi( p, iObj, i )
Level = Abc_MaxInt( Level, Acb_ObjLevelR(p, iObj) ); Level = Abc_MaxInt( Level, Acb_ObjLevelR(p, iObj) );
assert( p->LevelMax == Level ); assert( p->LevelMax == Level );
return Level; return Level;
} }
void Acb_NtkUpdateLevelD( Acb_Ntk_t * p, int Pivot )
{
Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, Pivot, 1 );
Acb_NtkComputeLevelD( p, vTfo );
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Computing and updating direct and reverse path count.]
Description [] Description []
...@@ -192,9 +162,11 @@ int Acb_NtkComputeLevelR( Acb_Ntk_t * p, Vec_Int_t * vTfi ) ...@@ -192,9 +162,11 @@ int Acb_NtkComputeLevelR( Acb_Ntk_t * p, Vec_Int_t * vTfi )
***********************************************************************/ ***********************************************************************/
int Acb_ObjSlack( Acb_Ntk_t * p, int iObj ) int Acb_ObjSlack( Acb_Ntk_t * p, int iObj )
{ {
assert( !Acb_ObjIsCio(p, iObj) + p->LevelMax >= Acb_ObjLevelD(p, iObj) + Acb_ObjLevelR(p, iObj) ); int LevelSum = Acb_ObjLevelD(p, iObj) + Acb_ObjLevelR(p, iObj);
return !Acb_ObjIsCio(p, iObj) + p->LevelMax - Acb_ObjLevelD(p, iObj) - Acb_ObjLevelR(p, iObj); assert( !Acb_ObjIsCio(p, iObj) + p->LevelMax >= LevelSum );
return !Acb_ObjIsCio(p, iObj) + p->LevelMax - LevelSum;
} }
int Acb_ObjComputePathD( Acb_Ntk_t * p, int iObj ) int Acb_ObjComputePathD( Acb_Ntk_t * p, int iObj )
{ {
int * pFanins, iFanin, k, Path = 0; int * pFanins, iFanin, k, Path = 0;
...@@ -207,26 +179,13 @@ int Acb_ObjComputePathD( Acb_Ntk_t * p, int iObj ) ...@@ -207,26 +179,13 @@ int Acb_ObjComputePathD( Acb_Ntk_t * p, int iObj )
int Acb_NtkComputePathsD( Acb_Ntk_t * p, Vec_Int_t * vTfo ) int Acb_NtkComputePathsD( Acb_Ntk_t * p, Vec_Int_t * vTfo )
{ {
int i, iObj, Path = 0; int i, iObj, Path = 0;
if ( vTfo == NULL )
{
Acb_NtkCleanObjPathD( p );
Acb_NtkForEachCi( p, iObj, i )
if ( Acb_ObjLevelR(p, iObj) == p->LevelMax )
Acb_ObjSetPathD( p, iObj, 1 );
Acb_NtkForEachObj( p, iObj )
if ( !Acb_ObjIsCi(p, iObj) && !Acb_ObjSlack(p, iObj) )
Acb_ObjComputePathD( p, iObj );
}
else
{
// it is assumed that vTfo contains CO nodes // it is assumed that vTfo contains CO nodes
assert( Acb_ObjSlack(p, Vec_IntEntry(vTfo, 0)) ); //assert( Acb_ObjSlack(p, Vec_IntEntry(vTfo, 0)) );
Vec_IntForEachEntry( vTfo, iObj, i ) Vec_IntForEachEntryReverse( vTfo, iObj, i )
if ( !Acb_ObjSlack(p, iObj) ) if ( !Acb_ObjSlack(p, iObj) )
Acb_ObjComputePathD( p, iObj ); Acb_ObjComputePathD( p, iObj );
else else
Acb_ObjSetPathD( p, iObj, 0 ); Acb_ObjSetPathD( p, iObj, 0 );
}
Acb_NtkForEachCo( p, iObj, i ) Acb_NtkForEachCo( p, iObj, i )
Path += Acb_ObjPathD(p, iObj); Path += Acb_ObjPathD(p, iObj);
p->nPaths = Path; p->nPaths = Path;
...@@ -245,55 +204,39 @@ int Acb_ObjComputePathR( Acb_Ntk_t * p, int iObj ) ...@@ -245,55 +204,39 @@ int Acb_ObjComputePathR( Acb_Ntk_t * p, int iObj )
int Acb_NtkComputePathsR( Acb_Ntk_t * p, Vec_Int_t * vTfi ) int Acb_NtkComputePathsR( Acb_Ntk_t * p, Vec_Int_t * vTfi )
{ {
int i, iObj, Path = 0; int i, iObj, Path = 0;
if ( vTfi == NULL )
{
Acb_NtkCleanObjPathR( p );
Acb_NtkForEachCo( p, iObj, i )
if ( Acb_ObjLevelD(p, iObj) == p->LevelMax )
Acb_ObjSetPathR( p, iObj, 1 );
Acb_NtkForEachObjReverse( p, iObj )
if ( !Acb_ObjIsCo(p, iObj) && !Acb_ObjSlack(p, iObj) )
Acb_ObjComputePathR( p, iObj );
}
else
{
// it is assumed that vTfi contains CI nodes // it is assumed that vTfi contains CI nodes
assert( Acb_ObjSlack(p, Vec_IntEntry(vTfi, 0)) ); //assert( Acb_ObjSlack(p, Vec_IntEntry(vTfi, 0)) );
Vec_IntForEachEntryReverse( vTfi, iObj, i ) Vec_IntForEachEntryReverse( vTfi, iObj, i )
if ( !Acb_ObjSlack(p, iObj) ) if ( !Acb_ObjSlack(p, iObj) )
Acb_ObjComputePathR( p, iObj ); Acb_ObjComputePathR( p, iObj );
else else
Acb_ObjSetPathR( p, iObj, 0 ); Acb_ObjSetPathR( p, iObj, 0 );
}
Acb_NtkForEachCi( p, iObj, i ) Acb_NtkForEachCi( p, iObj, i )
Path += Acb_ObjPathR(p, iObj); Path += Acb_ObjPathR(p, iObj);
assert( p->nPaths == Path ); assert( p->nPaths == Path );
return Path; return Path;
} }
int Acb_NtkComputePaths( Acb_Ntk_t * p ) int Acb_NtkComputePaths( Acb_Ntk_t * p )
{ {
Acb_NtkComputeLevelD( p, NULL ); Vec_Int_t * vTfi = Acb_ObjCollectTfi( p, -1, 1 );
Acb_NtkComputeLevelR( p, NULL ); Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, -1, 1 );
Acb_NtkComputePathsD( p, NULL ); Acb_NtkComputeLevelD( p, vTfi );
Acb_NtkComputePathsR( p, NULL ); Acb_NtkComputeLevelR( p, vTfo );
Acb_NtkComputePathsD( p, vTfi );
Acb_NtkComputePathsR( p, vTfo );
return p->nPaths; return p->nPaths;
} }
void Abc_NtkComputePaths( Abc_Ntk_t * p ) void Abc_NtkComputePaths( Abc_Ntk_t * p )
{ {
extern Acb_Ntk_t * Acb_NtkFromAbc( Abc_Ntk_t * p ); extern Acb_Ntk_t * Acb_NtkFromAbc( Abc_Ntk_t * p );
Acb_Ntk_t * pNtk = Acb_NtkFromAbc( p ); Acb_Ntk_t * pNtk = Acb_NtkFromAbc( p );
Acb_NtkCreateFanout( pNtk ); Acb_NtkCreateFanout( pNtk );
printf( "Computed %d paths.\n", Acb_NtkComputePaths(pNtk) ); printf( "Computed %d paths.\n", Acb_NtkComputePaths(pNtk) );
Acb_ManFree( pNtk->pDesign ); Acb_ManFree( pNtk->pDesign );
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
...@@ -305,42 +248,47 @@ void Abc_NtkComputePaths( Abc_Ntk_t * p ) ...@@ -305,42 +248,47 @@ void Abc_NtkComputePaths( Abc_Ntk_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Acb_ObjPath( Acb_Ntk_t * p, int iObj ) void Acb_ObjUpdatePriority( Acb_Ntk_t * p, int iObj )
{
return Acb_ObjPathD(p, iObj) + Acb_ObjPathR(p, iObj);
}
void Acb_ObjUpdateTiming( Acb_Ntk_t * p, int iObj )
{ {
int nPaths;
if ( p->vQue == NULL )
{
Acb_NtkCleanObjCounts( p );
p->vQue = Vec_QueAlloc( 1000 );
Vec_QueSetPriority( p->vQue, Vec_FltArrayP(&p->vCounts) );
}
nPaths = Acb_ObjPathD(p, iObj) + Acb_ObjPathR(p, iObj);
if ( nPaths == 0 )
return;
Acb_ObjSetCounts( p, iObj, (float)nPaths );
if ( Vec_QueIsMember( p->vQue, iObj ) )
Vec_QueUpdate( p->vQue, iObj );
else
Vec_QuePush( p->vQue, iObj );
} }
void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj ) void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj )
{ {
int i, Entry; int i, Entry, LevelMax = p->LevelMax;
if ( iObj > 0 )
{
// assuming that level of the new nodes is up to date // assuming that level of the new nodes is up to date
Vec_Int_t * vTfi = Acb_ObjCollectTfi( p, iObj, 1 ); Vec_Int_t * vTfi = Acb_ObjCollectTfi( p, iObj, 1 );
Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, iObj, 1 ); Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, iObj, 1 );
Acb_NtkComputeLevelD( p, vTfo ); Acb_NtkComputeLevelD( p, vTfo );
Acb_NtkComputeLevelR( p, vTfi ); Acb_NtkComputeLevelR( p, vTfi );
if ( iObj > 0 && LevelMax > p->LevelMax ) // reduced level
{
vTfi = Acb_ObjCollectTfi( p, -1, 1 );
vTfo = Acb_ObjCollectTfo( p, -1, 1 );
Vec_QueClear( p->vQue );
// add backup here
}
Acb_NtkComputePathsD( p, vTfo ); Acb_NtkComputePathsD( p, vTfo );
Acb_NtkComputePathsR( p, vTfi ); Acb_NtkComputePathsR( p, vTfi );
Vec_IntForEachEntry( vTfi, Entry, i ) Vec_IntForEachEntry( vTfi, Entry, i )
Acb_ObjUpdateTiming( p, Entry ); Acb_ObjUpdatePriority( p, Entry );
Vec_IntForEachEntry( vTfo, Entry, i ) Vec_IntForEachEntry( vTfo, Entry, i )
Acb_ObjUpdateTiming( p, Entry ); Acb_ObjUpdatePriority( p, Entry );
}
else
{
Acb_NtkComputeLevelD( p, NULL );
Acb_NtkComputeLevelR( p, NULL );
Acb_NtkComputePathsD( p, NULL );
Acb_NtkComputePathsR( p, NULL );
Acb_NtkForEachNode( p, Entry )
Acb_ObjUpdateTiming( p, Entry );
}
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
...@@ -352,20 +300,28 @@ void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj ) ...@@ -352,20 +300,28 @@ void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Acb_NtkCreateNode( Acb_Ntk_t * p, word uTruth, Vec_Int_t * vSupp )
{
int Pivot = Acb_ObjAlloc( p, ABC_OPER_LUT, Vec_IntSize(vSupp), 0 );
Acb_ObjSetTruth( p, Pivot, uTruth );
Acb_ObjAddFanins( p, Pivot, vSupp );
Acb_ObjAddFaninFanout( p, Pivot );
Acb_ObjComputeLevelD( p, Pivot );
}
void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp ) void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp )
{ {
int i, iFanin;
Vec_WrdSetEntry( &p->vObjTruth, Pivot, uTruth ); Vec_WrdSetEntry( &p->vObjTruth, Pivot, uTruth );
Acb_ObjRemoveFanout( p, Pivot ); Vec_IntErase( Vec_WecEntry(&p->vCnfs, Pivot) );
Acb_ObjRemoveFaninFanout( p, Pivot );
Acb_ObjRemoveFanins( p, Pivot ); Acb_ObjRemoveFanins( p, Pivot );
Vec_IntForEachEntry( vSupp, iFanin, i ) Acb_ObjAddFanins( p, Pivot, vSupp );
Acb_ObjAddFanin( p, Pivot, iFanin ); Acb_ObjAddFaninFanout( p, Pivot );
Acb_ObjAddFanout( p, Pivot ); if ( p->vQue == NULL )
Acb_NtkUpdateLevelD( p, Pivot );
else
Acb_NtkUpdateTiming( p, Pivot ); Acb_NtkUpdateTiming( p, Pivot );
Vec_IntErase( Vec_WecEntry(&p->vCnfs, Pivot) );
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/sat/cnf/cnfMan.c
...@@ -251,7 +251,7 @@ void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ) ...@@ -251,7 +251,7 @@ void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable )
for ( i = 0; i < p->nClauses; i++ ) for ( i = 0; i < p->nClauses; i++ )
{ {
for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); fprintf( pFile, "%s%d ", Abc_LitIsCompl(*pLit) ? "-":"", fReadable? Abc_Lit2Var(*pLit) : Abc_Lit2Var(*pLit)+1 );
fprintf( pFile, "\n" ); fprintf( pFile, "\n" );
} }
fprintf( pFile, "\n" ); fprintf( pFile, "\n" );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment