Skip to content

A
abc
Commit 12b70d49 by Alan Mishchenko
Options

Changes to CNF generation code.

parent 6f0b87dd
Showing with 839 additions and 18 deletions
abclib.dsp
...@@ -2971,6 +2971,10 @@ SOURCE=.\src\aig\cnf\cnfData.c ...@@ -2971,6 +2971,10 @@ SOURCE=.\src\aig\cnf\cnfData.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\aig\cnf\cnfFast.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\cnf\cnfMan.c SOURCE=.\src\aig\cnf\cnfMan.c
# End Source File # End Source File
# Begin Source File # Begin Source File
......
src/aig/aig/aig.h
...@@ -410,24 +410,33 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry ) ...@@ -410,24 +410,33 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
// iterator over the primary inputs // iterator over the primary inputs
#define Aig_ManForEachPi( p, pObj, i ) \ #define Aig_ManForEachPi( p, pObj, i ) \
Vec_PtrForEachEntry( Aig_Obj_t *, p->vPis, pObj, i ) Vec_PtrForEachEntry( Aig_Obj_t *, p->vPis, pObj, i )
#define Aig_ManForEachPiReverse( p, pObj, i ) \
Vec_PtrForEachEntryReverse( Aig_Obj_t *, p->vPis, pObj, i )
// iterator over the primary outputs // iterator over the primary outputs
#define Aig_ManForEachPo( p, pObj, i ) \ #define Aig_ManForEachPo( p, pObj, i ) \
Vec_PtrForEachEntry( Aig_Obj_t *, p->vPos, pObj, i ) Vec_PtrForEachEntry( Aig_Obj_t *, p->vPos, pObj, i )
// iterator over the assertions #define Aig_ManForEachPoReverse( p, pObj, i ) \
#define Aig_ManForEachAssert( p, pObj, i ) \ Vec_PtrForEachEntryReverse( Aig_Obj_t *, p->vPos, pObj, i )
Vec_PtrForEachEntryStart( Aig_Obj_t *, p->vPos, pObj, i, Aig_ManPoNum(p)-p->nAsserts ) // iterators over all objects, including those currently not used
// iterator over all objects, including those currently not used
#define Aig_ManForEachObj( p, pObj, i ) \ #define Aig_ManForEachObj( p, pObj, i ) \
Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
// iterator over the objects whose IDs are stored in an array #define Aig_ManForEachObjReverse( p, pObj, i ) \
#define Aig_ManForEachObjVec( vIds, p, pObj, i ) \ Vec_PtrForEachEntryReverse( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
// iterators over the objects whose IDs are stored in an array
#define Aig_ManForEachObjVec( vIds, p, pObj, i ) \
for ( i = 0; i < Vec_IntSize(vIds) && (((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))), 1); i++ ) for ( i = 0; i < Vec_IntSize(vIds) && (((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))), 1); i++ )
// iterator over all nodes #define Aig_ManForEachObjVecReverse( vIds, p, pObj, i ) \
for ( i = Vec_IntSize(vIds) - 1; i >= 0 && (((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))), 1); i-- )
// iterators over all nodes
#define Aig_ManForEachNode( p, pObj, i ) \ #define Aig_ManForEachNode( p, pObj, i ) \
Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
#define Aig_ManForEachNodeReverse( p, pObj, i ) \
Vec_PtrForEachEntryReverse( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
// iterator over all nodes // iterator over all nodes
#define Aig_ManForEachExor( p, pObj, i ) \ #define Aig_ManForEachExor( p, pObj, i ) \
Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsExor(pObj) ) {} else Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsExor(pObj) ) {} else
#define Aig_ManForEachExorReverse( p, pObj, i ) \
Vec_PtrForEachEntryReverse( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsExor(pObj) ) {} else
// these two procedures are only here for the use inside the iterator // these two procedures are only here for the use inside the iterator
static inline int Aig_ObjFanout0Int( Aig_Man_t * p, int ObjId ) { assert(ObjId < p->nFansAlloc); return p->pFanData[5*ObjId]; } static inline int Aig_ObjFanout0Int( Aig_Man_t * p, int ObjId ) { assert(ObjId < p->nFansAlloc); return p->pFanData[5*ObjId]; }
......
src/aig/cnf/cnf.h
...@@ -138,6 +138,8 @@ extern void Cnf_CutUpdateRefs( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_C ...@@ -138,6 +138,8 @@ 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 ========================================================*/
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();
extern void Cnf_ManStop( Cnf_Man_t * p ); extern void Cnf_ManStop( Cnf_Man_t * p );
......
src/aig/cnf/cnfFast.c 0 → 100644
/**CFile****************************************************************
FileName [cnfFast.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG-to-CNF conversion.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: cnfFast.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cnf.h"
#include "kit.h"
#include "satSolver.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Detects multi-input gate rooted at this node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_CollectSuper_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fStopCompl )
{
if ( pRoot != pObj && (pObj->fMarkA || (fStopCompl && Aig_IsComplement(pObj))) )
{
Vec_PtrPushUnique( vSuper, fStopCompl ? pObj : Aig_Regular(pObj) );
return;
}
assert( Aig_ObjIsNode(pObj) );
if ( fStopCompl )
{
Cnf_CollectSuper_rec( pRoot, Aig_ObjChild0(pObj), vSuper, 1 );
Cnf_CollectSuper_rec( pRoot, Aig_ObjChild1(pObj), vSuper, 1 );
}
else
{
Cnf_CollectSuper_rec( pRoot, Aig_ObjFanin0(pObj), vSuper, 0 );
Cnf_CollectSuper_rec( pRoot, Aig_ObjFanin1(pObj), vSuper, 0 );
}
}
/**Function*************************************************************
Synopsis [Detects multi-input gate rooted at this node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_CollectSuper( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper, int fStopCompl )
{
assert( !Aig_IsComplement(pRoot) );
Vec_PtrClear( vSuper );
Cnf_CollectSuper_rec( pRoot, pRoot, vSuper, fStopCompl );
}
/**Function*************************************************************
Synopsis [Collects nodes inside the cone.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_CollectVolume_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
{
if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
return;
Aig_ObjSetTravIdCurrent( p, pObj );
assert( Aig_ObjIsNode(pObj) );
Cnf_CollectVolume_rec( p, Aig_ObjFanin0(pObj), vNodes );
Cnf_CollectVolume_rec( p, Aig_ObjFanin1(pObj), vNodes );
Vec_PtrPush( vNodes, pObj );
}
/**Function*************************************************************
Synopsis [Collects nodes inside the cone.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_CollectVolume( Aig_Man_t * p, Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes )
{
Aig_Obj_t * pObj;
int i;
Aig_ManIncrementTravId( p );
Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
Aig_ObjSetTravIdCurrent( p, pObj );
Vec_PtrClear( vNodes );
Cnf_CollectVolume_rec( p, pRoot, vNodes );
}
/**Function*************************************************************
Synopsis [Derive truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
word Cnf_CutDeriveTruth( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes )
{
static word Truth6[6] = {
0xAAAAAAAAAAAAAAAA,
0xCCCCCCCCCCCCCCCC,
0xF0F0F0F0F0F0F0F0,
0xFF00FF00FF00FF00,
0xFFFF0000FFFF0000,
0xFFFFFFFF00000000
};
static word C[2] = { 0, ~0 };
static word S[256];
Aig_Obj_t * pObj;
int i;
assert( Vec_PtrSize(vLeaves) <= 6 && Vec_PtrSize(vNodes) > 0 );
assert( Vec_PtrSize(vLeaves) + Vec_PtrSize(vNodes) <= 256 );
Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
{
pObj->iData = i;
S[pObj->iData] = Truth6[i];
}
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
pObj->iData = Vec_PtrSize(vLeaves) + i;
S[pObj->iData] = (S[Aig_ObjFanin0(pObj)->iData] ^ C[Aig_ObjFaninC0(pObj)]) &
(S[Aig_ObjFanin1(pObj)->iData] ^ C[Aig_ObjFaninC1(pObj)]);
}
return S[pObj->iData];
}
/**Function*************************************************************
Synopsis [Marks AIG for CNF computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_DeriveFastMark_( Aig_Man_t * p )
{
Vec_Ptr_t * vLeaves, * vNodes;
Aig_Obj_t * pObj, * pObjC, * pObj0, * pObj1;
int i, k;
// mark CIs
Aig_ManForEachPi( p, pObj, i )
pObj->fMarkA = 1;
// mark CO drivers
Aig_ManForEachPo( p, pObj, i )
Aig_ObjFanin0(pObj)->fMarkA = 1;
// mark roots/leaves of MUX/XOR with MarkA
// mark internal nodes of MUX/XOR with MarkB
Aig_ManForEachNode( p, pObj, i )
{
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;
}
// mark nodes with many fanouts or pointed to by a complemented edge
Aig_ManForEachNode( p, pObj, i )
{
if ( Aig_ObjRefs(pObj) > 1 )
pObj->fMarkA = 1;
if ( Aig_ObjFaninC0(pObj) )
Aig_ObjFanin0(pObj)->fMarkA = 1;
if ( Aig_ObjFaninC1(pObj) )
Aig_ObjFanin1(pObj)->fMarkA = 1;
}
// clean internal nodes of MUX/XOR
Aig_ManForEachNode( p, pObj, i )
{
if ( pObj->fMarkB )
pObj->fMarkB = pObj->fMarkA = 0;
// pObj->fMarkB = 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;
/*
// 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;
Aig_ManForEachNode( p, pObj, i )
{
if ( !pObj->fMarkA )
continue;
if ( Aig_ObjRefs(pObj) == 1 )
continue;
Cnf_CollectSuper( pObj, vLeaves, 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 )
{
int fChanges = 0;
Aig_ManForEachNode( p, pObj, i )
{
if ( !pObj->fMarkA )
continue;
Cnf_CollectSuper( pObj, vLeaves, 0 );
if ( Vec_PtrSize(vLeaves) <= 6 )
continue;
Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObjC, k )
{
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*************************************************************
Synopsis [Marks AIG for CNF computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cnf_DeriveFastMark( Aig_Man_t * p )
{
Vec_Ptr_t * vLeaves, * vNodes;
Aig_Obj_t * pObj, * pObjC, * pObj0, * pObj1;
int i, k, Counter;
Aig_ManCleanMarkAB( p );
// mark CIs
Aig_ManForEachPi( p, pObj, i )
pObj->fMarkA = 1;
// mark CO drivers
Aig_ManForEachPo( p, pObj, i )
Aig_ObjFanin0(pObj)->fMarkA = 1;
Aig_ManForEachNode( p, pObj, i )
{
// mark nodes with many fanouts
if ( Aig_ObjRefs(pObj) > 1 )
pObj->fMarkA = 1;
// mark nodes pointed to by a complemented edge
if ( Aig_ObjFaninC0(pObj) )
Aig_ObjFanin0(pObj)->fMarkA = 1;
if ( Aig_ObjFaninC1(pObj) )
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
Aig_ManForEachNode( p, pObj, i )
{
if ( !pObj->fMarkB )
continue;
pObj->fMarkB = 0;
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 )
continue;
Cnf_CollectSuper( pObj, vLeaves, 0 );
if ( Vec_PtrSize(vLeaves) <= 6 )
continue;
Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObjC, k )
{
if ( Aig_ObjFaninC0(pObjC) && !Aig_ObjFanin0(pObjC)->fMarkA )
{
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++;
}
}
}
printf( "Made %d gate changes\n", nChanges );
if ( !nChanges )
break;
}
// check CO drivers
Counter = 0;
Aig_ManForEachPo( p, pObj, i )
Counter += !Aig_ObjFanin0(pObj)->fMarkA;
printf( "PO-driver rule is violated %d times.\n", Counter );
// check that the AND-gates are fine
Counter = 0;
Aig_ManForEachNode( p, pObj, i )
{
assert( pObj->fMarkB == 0 );
if ( !pObj->fMarkA )
continue;
Cnf_CollectSuper( pObj, vLeaves, 0 );
if ( Vec_PtrSize(vLeaves) <= 6 )
continue;
Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj1, k )
{
if ( Aig_ObjFaninC0(pObj1) && !Aig_ObjFanin0(pObj1)->fMarkA )
Counter++;
if ( Aig_ObjFaninC1(pObj1) && !Aig_ObjFanin1(pObj1)->fMarkA )
Counter++;
}
}
Vec_PtrFree( vLeaves );
Vec_PtrFree( vNodes );
printf( "AND-gate rule is violated %d times.\n", Counter );
}
/**Function*************************************************************
Synopsis [Counts the number of clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_CutCountClauses( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vCover )
{
word Truth;
Aig_Obj_t * pObj;
int i, RetValue, nSize = 0;
if ( Vec_PtrSize(vLeaves) > 6 )
{
// make sure this is an AND gate
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFanin0(pObj)->fMarkA )
printf( "Unusual 1!\n" );
if ( Aig_ObjFaninC1(pObj) && !Aig_ObjFanin1(pObj)->fMarkA )
printf( "Unusual 2!\n" );
continue;
assert( !Aig_ObjFaninC0(pObj) || Aig_ObjFanin0(pObj)->fMarkA );
assert( !Aig_ObjFaninC1(pObj) || Aig_ObjFanin1(pObj)->fMarkA );
}
return Vec_PtrSize(vLeaves) + 1;
}
Truth = Cnf_CutDeriveTruth( p, vLeaves, vNodes );
RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
assert( RetValue >= 0 );
nSize += Vec_IntSize(vCover);
Truth = ~Truth;
RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
assert( RetValue >= 0 );
nSize += Vec_IntSize(vCover);
return nSize;
}
/**Function*************************************************************
Synopsis [Counts the size of the CNF, assuming marks are set.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_CountCnfSize( Aig_Man_t * p )
{
Vec_Ptr_t * vLeaves, * vNodes;
Vec_Int_t * vCover;
Aig_Obj_t * pObj;
int nVars = 0, nClauses = 0;
int i, nSize;
vLeaves = Vec_PtrAlloc( 100 );
vNodes = Vec_PtrAlloc( 100 );
vCover = Vec_IntAlloc( 1 << 16 );
Aig_ManForEachObj( p, pObj, i )
nVars += pObj->fMarkA;
Aig_ManForEachNode( p, pObj, i )
{
if ( !pObj->fMarkA )
continue;
Cnf_CollectSuper( pObj, vLeaves, 0 );
Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
assert( pObj == Vec_PtrEntryLast(vNodes) );
nSize = Cnf_CutCountClauses( p, vLeaves, vNodes, vCover );
// printf( "%d(%d) ", Vec_PtrSize(vLeaves), nSize );
nClauses += nSize;
}
// printf( "\n" );
printf( "Vars = %d Clauses = %d\n", nVars, nClauses );
Vec_PtrFree( vLeaves );
Vec_PtrFree( vNodes );
Vec_IntFree( vCover );
return nClauses;
}
/**Function*************************************************************
Synopsis [Derives CNF from the marked AIG.]
Description [Assumes that marking is such that when we traverse from each
marked node, the logic cone has 6 inputs or less, or it is a multi-input AND.]
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs )
{
Cnf_Dat_t * pCnf;
Vec_Int_t * vLits, * vClas, * vMap;
Vec_Ptr_t * vLeaves, * vNodes;
Vec_Int_t * vCover;
Aig_Obj_t * pObj, * pLeaf;
int i, c, k, nVars, Cube, Entry, OutLit, DriLit, RetValue;
word Truth;
vLits = Vec_IntAlloc( 1 << 16 );
vClas = Vec_IntAlloc( 1 << 12 );
vMap = Vec_IntStartFull( Aig_ManObjNumMax(p) );
// assign variables for the outputs
nVars = 1;
if ( nOutputs )
{
if ( Aig_ManRegNum(p) == 0 )
{
assert( nOutputs == Aig_ManPoNum(p) );
Aig_ManForEachPo( p, pObj, i )
Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
}
else
{
assert( nOutputs == Aig_ManRegNum(p) );
Aig_ManForEachLiSeq( p, pObj, i )
Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
}
}
// assign variables to the internal nodes
Aig_ManForEachNodeReverse( p, pObj, i )
if ( pObj->fMarkA )
Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
// assign variables to the PIs and constant node
Aig_ManForEachPi( p, pObj, i )
Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
Vec_IntWriteEntry( vMap, Aig_ObjId(Aig_ManConst1(p)), nVars++ );
// create clauses
vLeaves = Vec_PtrAlloc( 100 );
vNodes = Vec_PtrAlloc( 100 );
vCover = Vec_IntAlloc( 1 << 16 );
Aig_ManForEachNodeReverse( p, pObj, i )
{
if ( !pObj->fMarkA )
continue;
OutLit = toLit( Vec_IntEntry(vMap, Aig_ObjId(pObj)) );
// detect cone
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 );
// 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( vLits, lit_neg(OutLit) );
Vec_IntPush( vLits, toLitCond(Vec_IntEntry(vMap, Aig_ObjId(Aig_Regular(pLeaf))), Aig_IsComplement(pLeaf)) );
}
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( vNodes );
Vec_IntFree( vCover );
// create clauses for the outputs
Aig_ManForEachPo( p, pObj, i )
{
DriLit = toLitCond( Vec_IntEntry(vMap, Aig_ObjFaninId0(pObj)), Aig_ObjFaninC0(pObj) );
if ( i < Aig_ManPoNum(p) - nOutputs )
{
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPush( vLits, DriLit );
}
else
{
OutLit = toLit( Vec_IntEntry(vMap, Aig_ObjId(pObj)) );
// first clause
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPush( vLits, OutLit );
Vec_IntPush( vLits, lit_neg(DriLit) );
// second clause
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPush( vLits, lit_neg(OutLit) );
Vec_IntPush( vLits, DriLit );
}
}
// write the constant literal
OutLit = toLit( Vec_IntEntry(vMap, Aig_ObjId(Aig_ManConst1(p))) );
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPush( vLits, OutLit );
// create structure
pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
pCnf->pMan = p;
pCnf->nVars = nVars;
pCnf->nLiterals = Vec_IntSize( vLits );
pCnf->nClauses = Vec_IntSize( vClas );
pCnf->pClauses = ABC_ALLOC( int *, pCnf->nClauses + 1 );
pCnf->pClauses[0] = Vec_IntReleaseArray( vLits );
Vec_IntForEachEntry( vClas, Entry, i )
pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
pCnf->pClauses[pCnf->nClauses] = pCnf->pClauses[0] + pCnf->nLiterals;
pCnf->pVarNums = Vec_IntReleaseArray( vMap );
// cleanup
Vec_IntFree( vLits );
Vec_IntFree( vClas );
Vec_IntFree( vMap );
return pCnf;
}
/**Function*************************************************************
Synopsis [Fast CNF computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Dat_t * Cnf_DeriveFast( Aig_Man_t * p, int nOutputs )
{
Cnf_Dat_t * pCnf = NULL;
int clk, clkTotal = clock();
printf( "\n" );
Aig_ManCleanMarkAB( p );
// create initial marking
clk = clock();
Cnf_DeriveFastMark( p );
Abc_PrintTime( 1, "Marking", clock() - clk );
// compute CNF size
clk = clock();
pCnf = Cnf_DeriveFastClauses( p, nOutputs );
Abc_PrintTime( 1, "Clauses", clock() - clk );
// derive the resulting CNF
Aig_ManCleanMarkA( p );
Abc_PrintTime( 1, "TOTAL ", clock() - clkTotal );
printf( "Vars = %6d. Clauses = %7d. Literals = %8d. \n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
// Cnf_DataFree( pCnf );
// pCnf = NULL;
return pCnf;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/aig/cnf/module.make
SRC += src/aig/cnf/cnfCore.c \ SRC += src/aig/cnf/cnfCore.c \
src/aig/cnf/cnfCut.c \ src/aig/cnf/cnfCut.c \
src/aig/cnf/cnfData.c \ src/aig/cnf/cnfData.c \
src/aig/cnf/cnfFast.c \
src/aig/cnf/cnfMan.c \ src/aig/cnf/cnfMan.c \
src/aig/cnf/cnfMap.c \ src/aig/cnf/cnfMap.c \
src/aig/cnf/cnfPost.c \ src/aig/cnf/cnfPost.c \
......
src/base/abci/abcDar.c
...@@ -1172,13 +1172,14 @@ Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t ...@@ -1172,13 +1172,14 @@ Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo, int fChangePol, int fVerbose )
{ {
Vec_Ptr_t * vMapped = NULL; Vec_Ptr_t * vMapped = NULL;
Aig_Man_t * pMan; Aig_Man_t * pMan;
Cnf_Man_t * pManCnf = NULL; Cnf_Man_t * pManCnf = NULL;
Cnf_Dat_t * pCnf; Cnf_Dat_t * pCnf;
Abc_Ntk_t * pNtkNew = NULL; Abc_Ntk_t * pNtkNew = NULL;
int clk = clock();
assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkIsStrash(pNtk) );
// convert to the AIG manager // convert to the AIG manager
...@@ -1192,12 +1193,25 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) ...@@ -1192,12 +1193,25 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
return NULL; return NULL;
} }
// perform balance // perform balance
if ( fVerbose )
Aig_ManPrintStats( pMan ); Aig_ManPrintStats( pMan );
// derive CNF // derive CNF
pCnf = Cnf_Derive( pMan, 0 ); if ( fFastAlgo )
Cnf_DataTranformPolarity( pCnf, 0 ); pCnf = Cnf_DeriveFast( pMan, 0 );
printf( "Vars = %6d. Clauses = %7d. Literals = %8d.\n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); else
pCnf = Cnf_Derive( pMan, 0 );
// adjust polarity
if ( fChangePol )
Cnf_DataTranformPolarity( pCnf, 0 );
// print stats
if ( fVerbose )
{
printf( "Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
Abc_PrintTime( 1, "Time", clock() - clk );
}
/* /*
// write the network for verification // write the network for verification
...@@ -1210,7 +1224,6 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) ...@@ -1210,7 +1224,6 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
Cnf_DataWriteIntoFile( pCnf, pFileName, 0 ); Cnf_DataWriteIntoFile( pCnf, pFileName, 0 );
Cnf_DataFree( pCnf ); Cnf_DataFree( pCnf );
Cnf_ClearMemory(); Cnf_ClearMemory();
Aig_ManStop( pMan ); Aig_ManStop( pMan );
return pNtkNew; return pNtkNew;
} }
......
src/base/io/io.c
...@@ -1865,23 +1865,38 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv ) ...@@ -1865,23 +1865,38 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
{ {
char * pFileName; char * pFileName;
int c; int c;
int fAllPrimes;
int fNewAlgo; int fNewAlgo;
extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ); int fFastAlgo;
int fAllPrimes;
int fChangePol;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo, int fChangePol, int fVerbose );
fNewAlgo = 1; fNewAlgo = 1;
fFastAlgo = 0;
fAllPrimes = 0; fAllPrimes = 0;
fChangePol = 1;
fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "nph" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "nfpcvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
case 'n': case 'n':
fNewAlgo ^= 1; fNewAlgo ^= 1;
break; break;
case 'f':
fFastAlgo ^= 1;
break;
case 'p': case 'p':
fAllPrimes ^= 1; fAllPrimes ^= 1;
break; break;
case 'c':
fChangePol ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h': case 'h':
goto usage; goto usage;
default: default:
...@@ -1904,8 +1919,10 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv ) ...@@ -1904,8 +1919,10 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
printf( "Warning: Selected option to write all primes has no effect when deriving CNF from AIG.\n" ); printf( "Warning: Selected option to write all primes has no effect when deriving CNF from AIG.\n" );
} }
// call the corresponding file writer // call the corresponding file writer
if ( fNewAlgo ) if ( fFastAlgo )
Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName ); Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName, 1, fChangePol, fVerbose );
else if ( fNewAlgo )
Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName, 0, fChangePol, fVerbose );
else if ( fAllPrimes ) else if ( fAllPrimes )
Io_WriteCnf( pAbc->pNtkCur, pFileName, 1 ); Io_WriteCnf( pAbc->pNtkCur, pFileName, 1 );
else else
...@@ -1913,10 +1930,13 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv ) ...@@ -1913,10 +1930,13 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
return 0; return 0;
usage: usage:
fprintf( pAbc->Err, "usage: write_cnf [-nph] <file>\n" ); fprintf( pAbc->Err, "usage: write_cnf [-nfpcvh] <file>\n" );
fprintf( pAbc->Err, "\t writes the miter cone into a CNF file\n" ); fprintf( pAbc->Err, "\t writes the miter cone into a CNF file\n" );
fprintf( pAbc->Err, "\t-n : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes" : "no" ); fprintf( pAbc->Err, "\t-n : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes" : "no" );
fprintf( pAbc->Err, "\t-f : toggle using fast algorithm [default = %s]\n", fFastAlgo? "yes" : "no" );
fprintf( pAbc->Err, "\t-p : toggle using all primes to enhance implicativity [default = %s]\n", fAllPrimes? "yes" : "no" ); fprintf( pAbc->Err, "\t-p : toggle using all primes to enhance implicativity [default = %s]\n", fAllPrimes? "yes" : "no" );
fprintf( pAbc->Err, "\t-c : toggle adjasting polarity of internal variables [default = %s]\n", fChangePol? "yes" : "no" );
fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
return 1; return 1;
......
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