Skip to content

A
abc
Commit 1d0b8276 by Alan Mishchenko
Options

Changes to CNF generation code.

parent 12b70d49
Showing with 178 additions and 265 deletions
src/aig/cnf/cnf.h
...@@ -138,7 +138,10 @@ extern void Cnf_CutUpdateRefs( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_C ...@@ -138,7 +138,10 @@ extern void Cnf_CutUpdateRefs( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_C
extern Cnf_Cut_t * Cnf_CutCompose( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, int iFan ); extern Cnf_Cut_t * Cnf_CutCompose( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, int iFan );
/*=== cnfData.c ========================================================*/ /*=== cnfData.c ========================================================*/
extern void Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops ); extern void Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops );
/*=== cnfData.c ========================================================*/ /*=== cnfFast.c ========================================================*/
extern void Cnf_CollectLeaves( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper, int fStopCompl );
extern void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves,
Vec_Ptr_t * vNodes, Vec_Int_t * vMap, Vec_Int_t * vCover, Vec_Int_t * vClauses );
extern Cnf_Dat_t * Cnf_DeriveFast( Aig_Man_t * p, int nOutputs ); extern Cnf_Dat_t * Cnf_DeriveFast( Aig_Man_t * p, int nOutputs );
/*=== cnfMan.c ========================================================*/ /*=== cnfMan.c ========================================================*/
extern Cnf_Man_t * Cnf_ManStart(); extern Cnf_Man_t * Cnf_ManStart();
......
src/aig/cnf/cnfFast.c
...@@ -43,7 +43,7 @@ ABC_NAMESPACE_IMPL_START ...@@ -43,7 +43,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Cnf_CollectSuper_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fStopCompl ) void Cnf_CollectLeaves_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fStopCompl )
{ {
if ( pRoot != pObj && (pObj->fMarkA || (fStopCompl && Aig_IsComplement(pObj))) ) if ( pRoot != pObj && (pObj->fMarkA || (fStopCompl && Aig_IsComplement(pObj))) )
{ {
...@@ -53,13 +53,13 @@ void Cnf_CollectSuper_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSup ...@@ -53,13 +53,13 @@ void Cnf_CollectSuper_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSup
assert( Aig_ObjIsNode(pObj) ); assert( Aig_ObjIsNode(pObj) );
if ( fStopCompl ) if ( fStopCompl )
{ {
Cnf_CollectSuper_rec( pRoot, Aig_ObjChild0(pObj), vSuper, 1 ); Cnf_CollectLeaves_rec( pRoot, Aig_ObjChild0(pObj), vSuper, 1 );
Cnf_CollectSuper_rec( pRoot, Aig_ObjChild1(pObj), vSuper, 1 ); Cnf_CollectLeaves_rec( pRoot, Aig_ObjChild1(pObj), vSuper, 1 );
} }
else else
{ {
Cnf_CollectSuper_rec( pRoot, Aig_ObjFanin0(pObj), vSuper, 0 ); Cnf_CollectLeaves_rec( pRoot, Aig_ObjFanin0(pObj), vSuper, 0 );
Cnf_CollectSuper_rec( pRoot, Aig_ObjFanin1(pObj), vSuper, 0 ); Cnf_CollectLeaves_rec( pRoot, Aig_ObjFanin1(pObj), vSuper, 0 );
} }
} }
...@@ -74,11 +74,11 @@ void Cnf_CollectSuper_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSup ...@@ -74,11 +74,11 @@ void Cnf_CollectSuper_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSup
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Cnf_CollectSuper( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper, int fStopCompl ) void Cnf_CollectLeaves( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper, int fStopCompl )
{ {
assert( !Aig_IsComplement(pRoot) ); assert( !Aig_IsComplement(pRoot) );
Vec_PtrClear( vSuper ); Vec_PtrClear( vSuper );
Cnf_CollectSuper_rec( pRoot, pRoot, vSuper, fStopCompl ); Cnf_CollectLeaves_rec( pRoot, pRoot, vSuper, fStopCompl );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -169,7 +169,7 @@ word Cnf_CutDeriveTruth( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes ...@@ -169,7 +169,7 @@ word Cnf_CutDeriveTruth( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes
/**Function************************************************************* /**Function*************************************************************
Synopsis [Marks AIG for CNF computation.] Synopsis [Collects nodes inside the cone.]
Description [] Description []
...@@ -178,136 +178,94 @@ word Cnf_CutDeriveTruth( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes ...@@ -178,136 +178,94 @@ word Cnf_CutDeriveTruth( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Cnf_DeriveFastMark_( Aig_Man_t * p ) void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot,
Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vMap, Vec_Int_t * vCover, Vec_Int_t * vClauses )
{ {
Vec_Ptr_t * vLeaves, * vNodes; Aig_Obj_t * pLeaf;
Aig_Obj_t * pObj, * pObjC, * pObj0, * pObj1; int c, k, Cube, OutLit, RetValue;
int i, k; word Truth;
// mark CIs assert( pRoot->fMarkA );
Aig_ManForEachPi( p, pObj, i )
pObj->fMarkA = 1;
// mark CO drivers
Aig_ManForEachPo( p, pObj, i )
Aig_ObjFanin0(pObj)->fMarkA = 1;
Vec_IntClear( vClauses );
// mark roots/leaves of MUX/XOR with MarkA OutLit = toLit( Vec_IntEntry(vMap, Aig_ObjId(pRoot)) );
// mark internal nodes of MUX/XOR with MarkB // detect cone
Aig_ManForEachNode( p, pObj, i ) Cnf_CollectLeaves( pRoot, vLeaves, 0 );
Cnf_CollectVolume( p, pRoot, vLeaves, vNodes );
assert( pObj == Vec_PtrEntryLast(vNodes) );
// check if this is an AND-gate
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pLeaf, k )
{ {
if ( !Aig_ObjIsMuxType(pObj) ) if ( Aig_ObjFaninC0(pLeaf) && !Aig_ObjFanin0(pLeaf)->fMarkA )
continue; break;
pObjC = Aig_ObjRecognizeMux( pObj, &pObj1, &pObj0 ); if ( Aig_ObjFaninC1(pLeaf) && !Aig_ObjFanin1(pLeaf)->fMarkA )
Aig_Regular(pObjC)->fMarkA = 1; break;
Aig_Regular(pObj1)->fMarkA = 1;
Aig_Regular(pObj0)->fMarkA = 1;
Aig_ObjFanin0(pObj)->fMarkB = 1;
Aig_ObjFanin1(pObj)->fMarkB = 1;
} }
if ( k == Vec_PtrSize(vNodes) )
// mark nodes with many fanouts or pointed to by a complemented edge
Aig_ManForEachNode( p, pObj, i )
{ {
if ( Aig_ObjRefs(pObj) > 1 ) Cnf_CollectLeaves( pRoot, vLeaves, 1 );
pObj->fMarkA = 1; // write big clause
if ( Aig_ObjFaninC0(pObj) ) Vec_IntPush( vClauses, 0 );
Aig_ObjFanin0(pObj)->fMarkA = 1; Vec_IntPush( vClauses, OutLit );
if ( Aig_ObjFaninC1(pObj) ) Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
Aig_ObjFanin1(pObj)->fMarkA = 1; Vec_IntPush( vClauses, toLitCond(Vec_IntEntry(vMap, Aig_ObjId(Aig_Regular(pLeaf))), !Aig_IsComplement(pLeaf)) );
// write small clauses
Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
{
Vec_IntPush( vClauses, 0 );
Vec_IntPush( vClauses, lit_neg(OutLit) );
Vec_IntPush( vClauses, toLitCond(Vec_IntEntry(vMap, Aig_ObjId(Aig_Regular(pLeaf))), Aig_IsComplement(pLeaf)) );
}
return;
} }
if ( Vec_PtrSize(vLeaves) > 6 )
printf( "FastCnfGeneration: Internal error!!!\n" );
assert( Vec_PtrSize(vLeaves) <= 6 );
// clean internal nodes of MUX/XOR Truth = Cnf_CutDeriveTruth( p, vLeaves, vNodes );
Aig_ManForEachNode( p, pObj, i ) if ( Truth == 0 || Truth == ~0 )
{ {
if ( pObj->fMarkB ) assert( RetValue == 0 );
pObj->fMarkB = pObj->fMarkA = 0; Vec_IntPush( vClauses, 0 );
// pObj->fMarkB = 0; Vec_IntPush( vClauses, (Truth == 0) ? lit_neg(OutLit) : OutLit );
return;
} }
// remove nodes those fanins are used
Aig_ManForEachNode( p, pObj, i )
if ( pObj->fMarkA && Aig_ObjFanin0(pObj)->fMarkA && Aig_ObjFanin1(pObj)->fMarkA )
pObj->fMarkA = 0;
// mark CO drivers RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
Aig_ManForEachPo( p, pObj, i ) assert( RetValue >= 0 );
Aig_ObjFanin0(pObj)->fMarkA = 1;
/* Vec_IntForEachEntry( vCover, Cube, c )
// if node has multiple fanout
Aig_ManForEachNode( p, pObj, i )
{
if ( Aig_ObjRefs(pObj) == 1 )
continue;
if ( Aig_ObjRefs(pObj) == 2 && Aig_ObjFanin0(pObj)->fMarkA && Aig_ObjFanin1(pObj)->fMarkA )
continue;
pObj->fMarkA = 1;
}
*/
// consider large cuts and mark inputs that are
vLeaves = Vec_PtrAlloc( 100 );
vNodes = Vec_PtrAlloc( 100 );
/*
while ( 1 )
{ {
int fChanges = 0; Vec_IntPush( vClauses, 0 );
Aig_ManForEachNode( p, pObj, i ) Vec_IntPush( vClauses, OutLit );
for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
{ {
if ( !pObj->fMarkA ) if ( (Cube & 3) == 0 )
continue;
if ( Aig_ObjRefs(pObj) == 1 )
continue; continue;
assert( (Cube & 3) != 3 );
Cnf_CollectSuper( pObj, vLeaves, 1 ); Vec_IntPush( vClauses, toLitCond( Vec_IntEntry(vMap, Aig_ObjId(Vec_PtrEntry(vLeaves,k))), (Cube&3)!=1 ) );
if ( Vec_PtrSize(vLeaves) <= 6 )
continue;
Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObjC, k )
{
if ( Aig_Regular(pObjC)->fMarkA == 0 )
fChanges = 1;
Aig_Regular(pObjC)->fMarkA = 1;
}
} }
printf( "Round 1 \n" );
if ( !fChanges )
break;
} }
*/
while ( 1 ) Truth = ~Truth;
RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
assert( RetValue >= 0 );
Vec_IntForEachEntry( vCover, Cube, c )
{ {
int fChanges = 0; Vec_IntPush( vClauses, 0 );
Aig_ManForEachNode( p, pObj, i ) Vec_IntPush( vClauses, lit_neg(OutLit) );
for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
{ {
if ( !pObj->fMarkA ) if ( (Cube & 3) == 0 )
continue;
Cnf_CollectSuper( pObj, vLeaves, 0 );
if ( Vec_PtrSize(vLeaves) <= 6 )
continue; continue;
Cnf_CollectVolume( p, pObj, vLeaves, vNodes ); assert( (Cube & 3) != 3 );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObjC, k ) Vec_IntPush( vClauses, toLitCond( Vec_IntEntry(vMap, Aig_ObjId(Vec_PtrEntry(vLeaves,k))), (Cube&3)!=1 ) );
{
if ( Aig_ObjFaninC0(pObjC) && !Aig_ObjFanin0(pObjC)->fMarkA )
{
Aig_ObjFanin0(pObjC)->fMarkA = 1;
// printf( "%d ", Aig_ObjFaninId0(pObjC) );
fChanges = 1;
}
if ( Aig_ObjFaninC1(pObjC) && !Aig_ObjFanin1(pObjC)->fMarkA )
{
Aig_ObjFanin1(pObjC)->fMarkA = 1;
// printf( "%d ", Aig_ObjFaninId1(pObjC) );
fChanges = 1;
}
}
} }
printf( "Round 2\n" );
if ( !fChanges )
break;
} }
}
Vec_PtrFree( vLeaves );
Vec_PtrFree( vNodes );
}
/**Function************************************************************* /**Function*************************************************************
...@@ -322,10 +280,14 @@ void Cnf_DeriveFastMark_( Aig_Man_t * p ) ...@@ -322,10 +280,14 @@ void Cnf_DeriveFastMark_( Aig_Man_t * p )
***********************************************************************/ ***********************************************************************/
void Cnf_DeriveFastMark( Aig_Man_t * p ) void Cnf_DeriveFastMark( Aig_Man_t * p )
{ {
Vec_Int_t * vSupps;
Vec_Ptr_t * vLeaves, * vNodes; Vec_Ptr_t * vLeaves, * vNodes;
Aig_Obj_t * pObj, * pObjC, * pObj0, * pObj1; Aig_Obj_t * pObj, * pTemp, * pObjC, * pObj0, * pObj1;
int i, k, Counter; int i, k, nFans, Counter;
Aig_ManCleanMarkAB( p );
vLeaves = Vec_PtrAlloc( 100 );
vNodes = Vec_PtrAlloc( 100 );
vSupps = Vec_IntStart( Aig_ManObjNumMax(p) );
// mark CIs // mark CIs
Aig_ManForEachPi( p, pObj, i ) Aig_ManForEachPi( p, pObj, i )
...@@ -335,90 +297,99 @@ void Cnf_DeriveFastMark( Aig_Man_t * p ) ...@@ -335,90 +297,99 @@ void Cnf_DeriveFastMark( Aig_Man_t * p )
Aig_ManForEachPo( p, pObj, i ) Aig_ManForEachPo( p, pObj, i )
Aig_ObjFanin0(pObj)->fMarkA = 1; Aig_ObjFanin0(pObj)->fMarkA = 1;
// mark MUX/XOR nodes
Aig_ManForEachNode( p, pObj, i )
{
assert( !pObj->fMarkB );
if ( !Aig_ObjIsMuxType(pObj) )
continue;
pObj0 = Aig_ObjFanin0(pObj);
if ( pObj0->fMarkB || Aig_ObjRefs(pObj0) > 1 )
continue;
pObj1 = Aig_ObjFanin1(pObj);
if ( pObj1->fMarkB || Aig_ObjRefs(pObj1) > 1 )
continue;
// mark nodes
pObj->fMarkB = 1;
pObj0->fMarkB = 1;
pObj1->fMarkB = 1;
// mark inputs and outputs
pObj->fMarkA = 1;
Aig_ObjFanin0(pObj0)->fMarkA = 1;
Aig_ObjFanin1(pObj0)->fMarkA = 1;
Aig_ObjFanin0(pObj1)->fMarkA = 1;
Aig_ObjFanin1(pObj1)->fMarkA = 1;
}
// mark nodes with multiple fanouts and pointed to by complemented edges
Aig_ManForEachNode( p, pObj, i ) Aig_ManForEachNode( p, pObj, i )
{ {
// mark nodes with many fanouts // mark nodes with many fanouts
if ( Aig_ObjRefs(pObj) > 1 ) if ( Aig_ObjRefs(pObj) > 1 )
pObj->fMarkA = 1; pObj->fMarkA = 1;
// mark nodes pointed to by a complemented edge // mark nodes pointed to by a complemented edge
if ( Aig_ObjFaninC0(pObj) ) if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFanin0(pObj)->fMarkB )
Aig_ObjFanin0(pObj)->fMarkA = 1; Aig_ObjFanin0(pObj)->fMarkA = 1;
if ( Aig_ObjFaninC1(pObj) ) if ( Aig_ObjFaninC1(pObj) && !Aig_ObjFanin1(pObj)->fMarkB )
Aig_ObjFanin1(pObj)->fMarkA = 1; Aig_ObjFanin1(pObj)->fMarkA = 1;
// mark roots/leaves of MUX/XOR with MarkA
// mark internal nodes of MUX/XOR with MarkB
if ( !Aig_ObjIsMuxType(pObj) )
continue;
pObjC = Aig_ObjRecognizeMux( pObj, &pObj1, &pObj0 );
Aig_Regular(pObjC)->fMarkA = 1;
Aig_Regular(pObj1)->fMarkA = 1;
Aig_Regular(pObj0)->fMarkA = 1;
Aig_ObjFanin0(pObj)->fMarkB = 1;
Aig_ObjFanin1(pObj)->fMarkB = 1;
} }
// clean internal nodes of MUX/XOR // compute supergate size for internal marked nodes
Aig_ManForEachNode( p, pObj, i ) Aig_ManForEachNode( p, pObj, i )
{ {
if ( !pObj->fMarkB ) if ( !pObj->fMarkA )
continue; continue;
pObj->fMarkB = 0; if ( pObj->fMarkB )
if ( Aig_ObjRefs(pObj) == 1 )
pObj->fMarkA = 0;
}
// remove nodes those fanins are used
Aig_ManForEachNode( p, pObj, i )
if ( pObj->fMarkA && Aig_ObjFanin0(pObj)->fMarkA && Aig_ObjFanin1(pObj)->fMarkA )
pObj->fMarkA = 0;
// mark CO drivers
Aig_ManForEachPo( p, pObj, i )
Aig_ObjFanin0(pObj)->fMarkA = 1;
vLeaves = Vec_PtrAlloc( 100 );
vNodes = Vec_PtrAlloc( 100 );
while ( 1 )
{
int nChanges = 0;
Aig_ManForEachNode( p, pObj, i )
{ {
if ( !pObj->fMarkA ) if ( !Aig_ObjIsMuxType(pObj) )
continue; continue;
Cnf_CollectSuper( pObj, vLeaves, 0 ); pObjC = Aig_ObjRecognizeMux( pObj, &pObj1, &pObj0 );
if ( Vec_PtrSize(vLeaves) <= 6 ) pObj0 = Aig_Regular(pObj0);
pObj1 = Aig_Regular(pObj1);
assert( pObj0->fMarkA );
assert( pObj1->fMarkA );
// if ( pObj0 == pObj1 )
// continue;
nFans = 1 + (pObj0 == pObj1);
if ( !pObj0->fMarkB && !Aig_ObjIsPi(pObj0) && Aig_ObjRefs(pObj0) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj0)) < 3 )
{
pObj0->fMarkA = 0;
continue; continue;
Cnf_CollectVolume( p, pObj, vLeaves, vNodes ); }
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObjC, k ) if ( !pObj1->fMarkB && !Aig_ObjIsPi(pObj1) && Aig_ObjRefs(pObj1) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj1)) < 3 )
{ {
if ( Aig_ObjFaninC0(pObjC) && !Aig_ObjFanin0(pObjC)->fMarkA ) pObj1->fMarkA = 0;
{ continue;
Aig_ObjFanin0(pObjC)->fMarkA = 1;
// printf( "%d ", Aig_ObjFaninId0(pObjC) );
nChanges++;
}
if ( Aig_ObjFaninC1(pObjC) && !Aig_ObjFanin1(pObjC)->fMarkA )
{
Aig_ObjFanin1(pObjC)->fMarkA = 1;
// printf( "%d ", Aig_ObjFaninId1(pObjC) );
nChanges++;
}
} }
continue;
} }
printf( "Made %d gate changes\n", nChanges );
if ( !nChanges ) Cnf_CollectLeaves( pObj, vLeaves, 1 );
Vec_IntWriteEntry( vSupps, Aig_ObjId(pObj), Vec_PtrSize(vLeaves) );
if ( Vec_PtrSize(vLeaves) >= 6 )
continue;
Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pTemp, k )
{
pTemp = Aig_Regular(pTemp);
assert( pTemp->fMarkA );
if ( pTemp->fMarkB || Aig_ObjIsPi(pTemp) || Aig_ObjRefs(pTemp) > 1 )
continue;
assert( Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 0 );
if ( Vec_PtrSize(vLeaves) - 1 + Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 6 )
continue;
pTemp->fMarkA = 0;
Vec_IntWriteEntry( vSupps, Aig_ObjId(pObj), 6 );
//printf( "%d %d ", Vec_PtrSize(vLeaves), Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) );
break; break;
}
} }
Aig_ManCleanMarkB( p );
// check CO drivers // check CO drivers
Counter = 0; Counter = 0;
Aig_ManForEachPo( p, pObj, i ) Aig_ManForEachPo( p, pObj, i )
Counter += !Aig_ObjFanin0(pObj)->fMarkA; Counter += !Aig_ObjFanin0(pObj)->fMarkA;
if ( Counter )
printf( "PO-driver rule is violated %d times.\n", Counter ); printf( "PO-driver rule is violated %d times.\n", Counter );
// check that the AND-gates are fine // check that the AND-gates are fine
...@@ -428,22 +399,24 @@ void Cnf_DeriveFastMark( Aig_Man_t * p ) ...@@ -428,22 +399,24 @@ void Cnf_DeriveFastMark( Aig_Man_t * p )
assert( pObj->fMarkB == 0 ); assert( pObj->fMarkB == 0 );
if ( !pObj->fMarkA ) if ( !pObj->fMarkA )
continue; continue;
Cnf_CollectSuper( pObj, vLeaves, 0 ); Cnf_CollectLeaves( pObj, vLeaves, 0 );
if ( Vec_PtrSize(vLeaves) <= 6 ) if ( Vec_PtrSize(vLeaves) <= 6 )
continue; continue;
Cnf_CollectVolume( p, pObj, vLeaves, vNodes ); Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj1, k ) Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pTemp, k )
{ {
if ( Aig_ObjFaninC0(pObj1) && !Aig_ObjFanin0(pObj1)->fMarkA ) if ( Aig_ObjFaninC0(pTemp) && !Aig_ObjFanin0(pTemp)->fMarkA )
Counter++; Counter++;
if ( Aig_ObjFaninC1(pObj1) && !Aig_ObjFanin1(pObj1)->fMarkA ) if ( Aig_ObjFaninC1(pTemp) && !Aig_ObjFanin1(pTemp)->fMarkA )
Counter++; Counter++;
} }
} }
if ( Counter )
printf( "AND-gate rule is violated %d times.\n", Counter );
Vec_PtrFree( vLeaves ); Vec_PtrFree( vLeaves );
Vec_PtrFree( vNodes ); Vec_PtrFree( vNodes );
Vec_IntFree( vSupps );
printf( "AND-gate rule is violated %d times.\n", Counter );
} }
...@@ -523,7 +496,7 @@ int Cnf_CountCnfSize( Aig_Man_t * p ) ...@@ -523,7 +496,7 @@ int Cnf_CountCnfSize( Aig_Man_t * p )
{ {
if ( !pObj->fMarkA ) if ( !pObj->fMarkA )
continue; continue;
Cnf_CollectSuper( pObj, vLeaves, 0 ); Cnf_CollectLeaves( pObj, vLeaves, 0 );
Cnf_CollectVolume( p, pObj, vLeaves, vNodes ); Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
assert( pObj == Vec_PtrEntryLast(vNodes) ); assert( pObj == Vec_PtrEntryLast(vNodes) );
...@@ -556,12 +529,11 @@ int Cnf_CountCnfSize( Aig_Man_t * p ) ...@@ -556,12 +529,11 @@ int Cnf_CountCnfSize( Aig_Man_t * p )
Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs ) Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs )
{ {
Cnf_Dat_t * pCnf; Cnf_Dat_t * pCnf;
Vec_Int_t * vLits, * vClas, * vMap; Vec_Int_t * vLits, * vClas, * vMap, * vTemp;
Vec_Ptr_t * vLeaves, * vNodes; Vec_Ptr_t * vLeaves, * vNodes;
Vec_Int_t * vCover; Vec_Int_t * vCover;
Aig_Obj_t * pObj, * pLeaf; Aig_Obj_t * pObj;
int i, c, k, nVars, Cube, Entry, OutLit, DriLit, RetValue; int i, k, nVars, Entry, OutLit, DriLit;
word Truth;
vLits = Vec_IntAlloc( 1 << 16 ); vLits = Vec_IntAlloc( 1 << 16 );
vClas = Vec_IntAlloc( 1 << 12 ); vClas = Vec_IntAlloc( 1 << 12 );
...@@ -597,87 +569,24 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs ) ...@@ -597,87 +569,24 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs )
vLeaves = Vec_PtrAlloc( 100 ); vLeaves = Vec_PtrAlloc( 100 );
vNodes = Vec_PtrAlloc( 100 ); vNodes = Vec_PtrAlloc( 100 );
vCover = Vec_IntAlloc( 1 << 16 ); vCover = Vec_IntAlloc( 1 << 16 );
vTemp = Vec_IntAlloc( 100 );
Aig_ManForEachNodeReverse( p, pObj, i ) Aig_ManForEachNodeReverse( p, pObj, i )
{ {
if ( !pObj->fMarkA ) if ( !pObj->fMarkA )
continue; continue;
OutLit = toLit( Vec_IntEntry(vMap, Aig_ObjId(pObj)) ); Cnf_ComputeClauses( p, pObj, vLeaves, vNodes, vMap, vCover, vTemp );
// detect cone Vec_IntForEachEntry( vTemp, Entry, k )
Cnf_CollectSuper( pObj, vLeaves, 0 );
Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
assert( pObj == Vec_PtrEntryLast(vNodes) );
// check if this is an AND-gate
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pLeaf, k )
{
if ( Aig_ObjFaninC0(pLeaf) && !Aig_ObjFanin0(pLeaf)->fMarkA )
break;
if ( Aig_ObjFaninC1(pLeaf) && !Aig_ObjFanin1(pLeaf)->fMarkA )
break;
}
if ( k == Vec_PtrSize(vNodes) )
{ {
Cnf_CollectSuper( pObj, vLeaves, 1 ); if ( Entry == 0 )
// write big clause
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPush( vLits, OutLit );
Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
Vec_IntPush( vLits, toLitCond(Vec_IntEntry(vMap, Aig_ObjId(Aig_Regular(pLeaf))), !Aig_IsComplement(pLeaf)) );
// write small clauses
Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
{
Vec_IntPush( vClas, Vec_IntSize(vLits) ); Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPush( vLits, lit_neg(OutLit) ); else
Vec_IntPush( vLits, toLitCond(Vec_IntEntry(vMap, Aig_ObjId(Aig_Regular(pLeaf))), Aig_IsComplement(pLeaf)) ); Vec_IntPush( vLits, Entry );
} }
continue;
}
assert( Vec_PtrSize(vLeaves) <= 6 );
Truth = Cnf_CutDeriveTruth( p, vLeaves, vNodes );
if ( Truth == 0 || Truth == ~0 )
{
assert( RetValue == 0 );
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPush( vLits, (Truth == 0) ? lit_neg(OutLit) : OutLit );
continue;
}
RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
assert( RetValue >= 0 );
Vec_IntForEachEntry( vCover, Cube, c )
{
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPush( vLits, OutLit );
for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
{
if ( (Cube & 3) == 0 )
continue;
assert( (Cube & 3) != 3 );
Vec_IntPush( vLits, toLitCond( Vec_IntEntry(vMap, Aig_ObjId(Vec_PtrEntry(vLeaves,k))), (Cube&3)!=1 ) );
}
}
Truth = ~Truth;
RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
assert( RetValue >= 0 );
Vec_IntForEachEntry( vCover, Cube, c )
{
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPush( vLits, lit_neg(OutLit) );
for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
{
if ( (Cube & 3) == 0 )
continue;
assert( (Cube & 3) != 3 );
Vec_IntPush( vLits, toLitCond( Vec_IntEntry(vMap, Aig_ObjId(Vec_PtrEntry(vLeaves,k))), (Cube&3)==1 ) );
}
}
} }
Vec_PtrFree( vLeaves ); Vec_PtrFree( vLeaves );
Vec_PtrFree( vNodes ); Vec_PtrFree( vNodes );
Vec_IntFree( vCover ); Vec_IntFree( vCover );
Vec_IntFree( vTemp );
// create clauses for the outputs // create clauses for the outputs
Aig_ManForEachPo( p, pObj, i ) Aig_ManForEachPo( p, pObj, i )
...@@ -742,21 +651,21 @@ Cnf_Dat_t * Cnf_DeriveFast( Aig_Man_t * p, int nOutputs ) ...@@ -742,21 +651,21 @@ Cnf_Dat_t * Cnf_DeriveFast( Aig_Man_t * p, int nOutputs )
{ {
Cnf_Dat_t * pCnf = NULL; Cnf_Dat_t * pCnf = NULL;
int clk, clkTotal = clock(); int clk, clkTotal = clock();
printf( "\n" ); // printf( "\n" );
Aig_ManCleanMarkAB( p ); Aig_ManCleanMarkAB( p );
// create initial marking // create initial marking
clk = clock(); clk = clock();
Cnf_DeriveFastMark( p ); Cnf_DeriveFastMark( p );
Abc_PrintTime( 1, "Marking", clock() - clk ); // Abc_PrintTime( 1, "Marking", clock() - clk );
// compute CNF size // compute CNF size
clk = clock(); clk = clock();
pCnf = Cnf_DeriveFastClauses( p, nOutputs ); pCnf = Cnf_DeriveFastClauses( p, nOutputs );
Abc_PrintTime( 1, "Clauses", clock() - clk ); // Abc_PrintTime( 1, "Clauses", clock() - clk );
// derive the resulting CNF // derive the resulting CNF
Aig_ManCleanMarkA( p ); Aig_ManCleanMarkA( p );
Abc_PrintTime( 1, "TOTAL ", clock() - clkTotal ); // Abc_PrintTime( 1, "TOTAL ", clock() - clkTotal );
printf( "Vars = %6d. Clauses = %7d. Literals = %8d. \n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); // printf( "Vars = %6d. Clauses = %7d. Literals = %8d. \n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
// Cnf_DataFree( pCnf ); // Cnf_DataFree( pCnf );
// pCnf = NULL; // pCnf = NULL;
......
src/aig/saig/saigAbsPba.c
...@@ -269,7 +269,8 @@ clk = clock(); ...@@ -269,7 +269,8 @@ clk = clock();
if ( fVerbose ) if ( fVerbose )
Aig_ManPrintStats( pFrames ); Aig_ManPrintStats( pFrames );
// pCnf = Cnf_DeriveSimple( pFrames, 0 ); // pCnf = Cnf_DeriveSimple( pFrames, 0 );
pCnf = Cnf_Derive( pFrames, 0 ); // pCnf = Cnf_Derive( pFrames, 0 );
pCnf = Cnf_DeriveFast( pFrames, 0 );
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL ) if ( pSat == NULL )
{ {
......
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