mirror of https://github.com/YosysHQ/abc.git
807 lines
26 KiB
C
807 lines
26 KiB
C
/**CFile****************************************************************
|
|
|
|
FileName [cnfWrite.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: cnfWrite.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
|
|
|
|
***********************************************************************/
|
|
|
|
#include "cnf.h"
|
|
|
|
ABC_NAMESPACE_IMPL_START
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// DECLARATIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// FUNCTION DEFINITIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Derives CNF mapping.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Vec_Int_t * Cnf_ManWriteCnfMapping( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
|
|
{
|
|
Vec_Int_t * vResult;
|
|
Aig_Obj_t * pObj;
|
|
Cnf_Cut_t * pCut;
|
|
int i, k, nOffset;
|
|
nOffset = Aig_ManObjNumMax(p->pManAig);
|
|
vResult = Vec_IntStart( nOffset );
|
|
Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
|
|
{
|
|
assert( Aig_ObjIsNode(pObj) );
|
|
pCut = Cnf_ObjBestCut( pObj );
|
|
assert( pCut->nFanins < 5 );
|
|
Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), nOffset );
|
|
Vec_IntPush( vResult, *Cnf_CutTruth(pCut) );
|
|
for ( k = 0; k < pCut->nFanins; k++ )
|
|
Vec_IntPush( vResult, pCut->pFanins[k] );
|
|
for ( ; k < 4; k++ )
|
|
Vec_IntPush( vResult, -1 );
|
|
nOffset += 5;
|
|
}
|
|
return vResult;
|
|
}
|
|
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Writes the cover into the array.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover )
|
|
{
|
|
int Lits[4], Cube, iCube, i, b;
|
|
Vec_IntClear( vCover );
|
|
for ( i = 0; i < nCubes; i++ )
|
|
{
|
|
Cube = pSop[i];
|
|
for ( b = 0; b < 4; b++ )
|
|
{
|
|
if ( Cube % 3 == 0 )
|
|
Lits[b] = 1;
|
|
else if ( Cube % 3 == 1 )
|
|
Lits[b] = 2;
|
|
else
|
|
Lits[b] = 0;
|
|
Cube = Cube / 3;
|
|
}
|
|
iCube = 0;
|
|
for ( b = 0; b < 4; b++ )
|
|
iCube = (iCube << 2) | Lits[b];
|
|
Vec_IntPush( vCover, iCube );
|
|
}
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Returns the number of literals in the SOP.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Cnf_SopCountLiterals( char * pSop, int nCubes )
|
|
{
|
|
int nLits = 0, Cube, i, b;
|
|
for ( i = 0; i < nCubes; i++ )
|
|
{
|
|
Cube = pSop[i];
|
|
for ( b = 0; b < 4; b++ )
|
|
{
|
|
if ( Cube % 3 != 2 )
|
|
nLits++;
|
|
Cube = Cube / 3;
|
|
}
|
|
}
|
|
return nLits;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Returns the number of literals in the SOP.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Cnf_IsopCountLiterals( Vec_Int_t * vIsop, int nVars )
|
|
{
|
|
int nLits = 0, Cube, i, b;
|
|
Vec_IntForEachEntry( vIsop, Cube, i )
|
|
{
|
|
for ( b = 0; b < nVars; b++ )
|
|
{
|
|
if ( (Cube & 3) == 1 || (Cube & 3) == 2 )
|
|
nLits++;
|
|
Cube >>= 2;
|
|
}
|
|
}
|
|
return nLits;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Writes the cube and returns the number of literals in it.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int * pLiterals )
|
|
{
|
|
int nLits = nVars, b;
|
|
for ( b = 0; b < nVars; b++ )
|
|
{
|
|
if ( (Cube & 3) == 1 ) // value 0 --> write positive literal
|
|
*pLiterals++ = 2 * pVars[b];
|
|
else if ( (Cube & 3) == 2 ) // value 1 --> write negative literal
|
|
*pLiterals++ = 2 * pVars[b] + 1;
|
|
else
|
|
nLits--;
|
|
Cube >>= 2;
|
|
}
|
|
return nLits;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Derives CNF for the mapping.]
|
|
|
|
Description [The last argument shows the number of last outputs
|
|
of the manager, which will not be converted into clauses but the
|
|
new variables for which will be introduced.]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
|
|
{
|
|
int fChangeVariableOrder = 0; // should be set to 0 to improve performance
|
|
Aig_Obj_t * pObj;
|
|
Cnf_Dat_t * pCnf;
|
|
Cnf_Cut_t * pCut;
|
|
Vec_Int_t * vCover, * vSopTemp;
|
|
int OutVar, PoVar, pVars[32], * pLits, ** pClas;
|
|
unsigned uTruth;
|
|
int i, k, nLiterals, nClauses, Cube, Number;
|
|
|
|
// count the number of literals and clauses
|
|
nLiterals = 1 + Aig_ManCoNum( p->pManAig ) + 3 * nOutputs;
|
|
nClauses = 1 + Aig_ManCoNum( p->pManAig ) + nOutputs;
|
|
Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
|
|
{
|
|
assert( Aig_ObjIsNode(pObj) );
|
|
pCut = Cnf_ObjBestCut( pObj );
|
|
|
|
// positive polarity of the cut
|
|
if ( pCut->nFanins < 5 )
|
|
{
|
|
uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
|
|
nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
|
|
assert( p->pSopSizes[uTruth] >= 0 );
|
|
nClauses += p->pSopSizes[uTruth];
|
|
}
|
|
else
|
|
{
|
|
nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]);
|
|
nClauses += Vec_IntSize(pCut->vIsop[1]);
|
|
}
|
|
// negative polarity of the cut
|
|
if ( pCut->nFanins < 5 )
|
|
{
|
|
uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
|
|
nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
|
|
assert( p->pSopSizes[uTruth] >= 0 );
|
|
nClauses += p->pSopSizes[uTruth];
|
|
}
|
|
else
|
|
{
|
|
nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
|
|
nClauses += Vec_IntSize(pCut->vIsop[0]);
|
|
}
|
|
//printf( "%d ", nClauses-(1 + Aig_ManCoNum( p->pManAig )) );
|
|
}
|
|
//printf( "\n" );
|
|
|
|
// allocate CNF
|
|
pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
|
|
pCnf->pMan = p->pManAig;
|
|
pCnf->nLiterals = nLiterals;
|
|
pCnf->nClauses = nClauses;
|
|
pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
|
|
pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
|
|
pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
|
|
// create room for variable numbers
|
|
pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
|
|
// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p->pManAig) );
|
|
for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ )
|
|
pCnf->pVarNums[i] = -1;
|
|
|
|
if ( !fChangeVariableOrder )
|
|
{
|
|
// assign variables to the last (nOutputs) POs
|
|
Number = 1;
|
|
if ( nOutputs )
|
|
{
|
|
if ( Aig_ManRegNum(p->pManAig) == 0 )
|
|
{
|
|
assert( nOutputs == Aig_ManCoNum(p->pManAig) );
|
|
Aig_ManForEachCo( p->pManAig, pObj, i )
|
|
pCnf->pVarNums[pObj->Id] = Number++;
|
|
}
|
|
else
|
|
{
|
|
assert( nOutputs == Aig_ManRegNum(p->pManAig) );
|
|
Aig_ManForEachLiSeq( p->pManAig, pObj, i )
|
|
pCnf->pVarNums[pObj->Id] = Number++;
|
|
}
|
|
}
|
|
// assign variables to the internal nodes
|
|
Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
|
|
pCnf->pVarNums[pObj->Id] = Number++;
|
|
// assign variables to the PIs and constant node
|
|
Aig_ManForEachCi( p->pManAig, pObj, i )
|
|
pCnf->pVarNums[pObj->Id] = Number++;
|
|
pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number++;
|
|
pCnf->nVars = Number;
|
|
}
|
|
else
|
|
{
|
|
// assign variables to the last (nOutputs) POs
|
|
Number = Aig_ManObjNumMax(p->pManAig) + 1;
|
|
pCnf->nVars = Number + 1;
|
|
if ( nOutputs )
|
|
{
|
|
if ( Aig_ManRegNum(p->pManAig) == 0 )
|
|
{
|
|
assert( nOutputs == Aig_ManCoNum(p->pManAig) );
|
|
Aig_ManForEachCo( p->pManAig, pObj, i )
|
|
pCnf->pVarNums[pObj->Id] = Number--;
|
|
}
|
|
else
|
|
{
|
|
assert( nOutputs == Aig_ManRegNum(p->pManAig) );
|
|
Aig_ManForEachLiSeq( p->pManAig, pObj, i )
|
|
pCnf->pVarNums[pObj->Id] = Number--;
|
|
}
|
|
}
|
|
// assign variables to the internal nodes
|
|
Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
|
|
pCnf->pVarNums[pObj->Id] = Number--;
|
|
// assign variables to the PIs and constant node
|
|
Aig_ManForEachCi( p->pManAig, pObj, i )
|
|
pCnf->pVarNums[pObj->Id] = Number--;
|
|
pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number--;
|
|
assert( Number >= 0 );
|
|
}
|
|
|
|
// assign the clauses
|
|
vSopTemp = Vec_IntAlloc( 1 << 16 );
|
|
pLits = pCnf->pClauses[0];
|
|
pClas = pCnf->pClauses;
|
|
Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
|
|
{
|
|
pCut = Cnf_ObjBestCut( pObj );
|
|
|
|
// save variables of this cut
|
|
OutVar = pCnf->pVarNums[ pObj->Id ];
|
|
for ( k = 0; k < (int)pCut->nFanins; k++ )
|
|
{
|
|
pVars[k] = pCnf->pVarNums[ pCut->pFanins[k] ];
|
|
assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) );
|
|
}
|
|
|
|
// positive polarity of the cut
|
|
if ( pCut->nFanins < 5 )
|
|
{
|
|
uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
|
|
Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
|
|
vCover = vSopTemp;
|
|
}
|
|
else
|
|
vCover = pCut->vIsop[1];
|
|
Vec_IntForEachEntry( vCover, Cube, k )
|
|
{
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar;
|
|
pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
|
|
}
|
|
|
|
// negative polarity of the cut
|
|
if ( pCut->nFanins < 5 )
|
|
{
|
|
uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
|
|
Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
|
|
vCover = vSopTemp;
|
|
}
|
|
else
|
|
vCover = pCut->vIsop[0];
|
|
Vec_IntForEachEntry( vCover, Cube, k )
|
|
{
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar + 1;
|
|
pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
|
|
}
|
|
}
|
|
Vec_IntFree( vSopTemp );
|
|
|
|
// write the constant literal
|
|
OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ];
|
|
assert( OutVar <= Aig_ManObjNumMax(p->pManAig) );
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar;
|
|
|
|
// write the output literals
|
|
Aig_ManForEachCo( p->pManAig, pObj, i )
|
|
{
|
|
OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
|
|
if ( i < Aig_ManCoNum(p->pManAig) - nOutputs )
|
|
{
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
|
|
}
|
|
else
|
|
{
|
|
PoVar = pCnf->pVarNums[ pObj->Id ];
|
|
// first clause
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * PoVar;
|
|
*pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
|
|
// second clause
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * PoVar + 1;
|
|
*pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
|
|
}
|
|
}
|
|
|
|
// verify that the correct number of literals and clauses was written
|
|
assert( pLits - pCnf->pClauses[0] == nLiterals );
|
|
assert( pClas - pCnf->pClauses == nClauses );
|
|
//Cnf_DataPrint( pCnf, 1 );
|
|
return pCnf;
|
|
}
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Derives CNF for the mapping.]
|
|
|
|
Description [Derives CNF with obj IDs as SAT vars and mapping of
|
|
objects into clauses (pObj2Clause and pObj2Count).]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Cnf_Dat_t * Cnf_ManWriteCnfOther( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
|
|
{
|
|
Aig_Obj_t * pObj;
|
|
Cnf_Dat_t * pCnf;
|
|
Cnf_Cut_t * pCut;
|
|
Vec_Int_t * vCover, * vSopTemp;
|
|
int OutVar, PoVar, pVars[32], * pLits, ** pClas;
|
|
unsigned uTruth;
|
|
int i, k, nLiterals, nClauses, Cube;
|
|
|
|
// count the number of literals and clauses
|
|
nLiterals = 1 + 4 * Aig_ManCoNum( p->pManAig );
|
|
nClauses = 1 + 2 * Aig_ManCoNum( p->pManAig );
|
|
Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
|
|
{
|
|
assert( Aig_ObjIsNode(pObj) );
|
|
pCut = Cnf_ObjBestCut( pObj );
|
|
// positive polarity of the cut
|
|
if ( pCut->nFanins < 5 )
|
|
{
|
|
uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
|
|
nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
|
|
assert( p->pSopSizes[uTruth] >= 0 );
|
|
nClauses += p->pSopSizes[uTruth];
|
|
}
|
|
else
|
|
{
|
|
nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]);
|
|
nClauses += Vec_IntSize(pCut->vIsop[1]);
|
|
}
|
|
// negative polarity of the cut
|
|
if ( pCut->nFanins < 5 )
|
|
{
|
|
uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
|
|
nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
|
|
assert( p->pSopSizes[uTruth] >= 0 );
|
|
nClauses += p->pSopSizes[uTruth];
|
|
}
|
|
else
|
|
{
|
|
nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
|
|
nClauses += Vec_IntSize(pCut->vIsop[0]);
|
|
}
|
|
}
|
|
|
|
// allocate CNF
|
|
pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
|
|
pCnf->pMan = p->pManAig;
|
|
pCnf->nLiterals = nLiterals;
|
|
pCnf->nClauses = nClauses;
|
|
pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
|
|
pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
|
|
pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
|
|
// create room for variable numbers
|
|
pCnf->pObj2Clause = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
|
|
pCnf->pObj2Count = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
|
|
for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ )
|
|
pCnf->pObj2Clause[i] = pCnf->pObj2Count[i] = -1;
|
|
pCnf->nVars = Aig_ManObjNumMax(p->pManAig);
|
|
|
|
// clear the PI counters
|
|
Aig_ManForEachCi( p->pManAig, pObj, i )
|
|
pCnf->pObj2Count[pObj->Id] = 0;
|
|
|
|
// assign the clauses
|
|
vSopTemp = Vec_IntAlloc( 1 << 16 );
|
|
pLits = pCnf->pClauses[0];
|
|
pClas = pCnf->pClauses;
|
|
Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
|
|
{
|
|
// remember the starting clause
|
|
pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses;
|
|
pCnf->pObj2Count[pObj->Id] = 0;
|
|
|
|
// get the best cut
|
|
pCut = Cnf_ObjBestCut( pObj );
|
|
// save variables of this cut
|
|
OutVar = pObj->Id;
|
|
for ( k = 0; k < (int)pCut->nFanins; k++ )
|
|
{
|
|
pVars[k] = pCut->pFanins[k];
|
|
assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) );
|
|
}
|
|
|
|
// positive polarity of the cut
|
|
if ( pCut->nFanins < 5 )
|
|
{
|
|
uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
|
|
Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
|
|
vCover = vSopTemp;
|
|
}
|
|
else
|
|
vCover = pCut->vIsop[1];
|
|
Vec_IntForEachEntry( vCover, Cube, k )
|
|
{
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar;
|
|
pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
|
|
}
|
|
pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover);
|
|
|
|
// negative polarity of the cut
|
|
if ( pCut->nFanins < 5 )
|
|
{
|
|
uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
|
|
Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
|
|
vCover = vSopTemp;
|
|
}
|
|
else
|
|
vCover = pCut->vIsop[0];
|
|
Vec_IntForEachEntry( vCover, Cube, k )
|
|
{
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar + 1;
|
|
pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
|
|
}
|
|
pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover);
|
|
}
|
|
Vec_IntFree( vSopTemp );
|
|
|
|
// write the output literals
|
|
Aig_ManForEachCo( p->pManAig, pObj, i )
|
|
{
|
|
// remember the starting clause
|
|
pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses;
|
|
pCnf->pObj2Count[pObj->Id] = 2;
|
|
// get variables
|
|
OutVar = Aig_ObjFanin0(pObj)->Id;
|
|
PoVar = pObj->Id;
|
|
// first clause
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * PoVar;
|
|
*pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
|
|
// second clause
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * PoVar + 1;
|
|
*pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
|
|
}
|
|
|
|
// remember the starting clause
|
|
pCnf->pObj2Clause[Aig_ManConst1(p->pManAig)->Id] = pClas - pCnf->pClauses;
|
|
pCnf->pObj2Count[Aig_ManConst1(p->pManAig)->Id] = 1;
|
|
// write the constant literal
|
|
OutVar = Aig_ManConst1(p->pManAig)->Id;
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar;
|
|
|
|
// verify that the correct number of literals and clauses was written
|
|
assert( pLits - pCnf->pClauses[0] == nLiterals );
|
|
assert( pClas - pCnf->pClauses == nClauses );
|
|
//Cnf_DataPrint( pCnf, 1 );
|
|
return pCnf;
|
|
}
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Derives a simple CNF for the AIG.]
|
|
|
|
Description [The last argument lists the number of last outputs
|
|
of the manager, which will not be converted into clauses.
|
|
New variables will be introduced for these outputs.]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
|
|
{
|
|
Aig_Obj_t * pObj;
|
|
Cnf_Dat_t * pCnf;
|
|
int OutVar, PoVar, pVars[32], * pLits, ** pClas;
|
|
int i, nLiterals, nClauses, Number;
|
|
|
|
// count the number of literals and clauses
|
|
nLiterals = 1 + 7 * Aig_ManNodeNum(p) + Aig_ManCoNum( p ) + 3 * nOutputs;
|
|
nClauses = 1 + 3 * Aig_ManNodeNum(p) + Aig_ManCoNum( p ) + nOutputs;
|
|
|
|
// allocate CNF
|
|
pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
|
|
memset( pCnf, 0, sizeof(Cnf_Dat_t) );
|
|
pCnf->pMan = p;
|
|
pCnf->nLiterals = nLiterals;
|
|
pCnf->nClauses = nClauses;
|
|
pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
|
|
pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
|
|
pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
|
|
|
|
// create room for variable numbers
|
|
pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p) );
|
|
// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
|
|
for ( i = 0; i < Aig_ManObjNumMax(p); i++ )
|
|
pCnf->pVarNums[i] = -1;
|
|
// assign variables to the last (nOutputs) POs
|
|
Number = 1;
|
|
if ( nOutputs )
|
|
{
|
|
// assert( nOutputs == Aig_ManRegNum(p) );
|
|
// Aig_ManForEachLiSeq( p, pObj, i )
|
|
// pCnf->pVarNums[pObj->Id] = Number++;
|
|
Aig_ManForEachCo( p, pObj, i )
|
|
pCnf->pVarNums[pObj->Id] = Number++;
|
|
}
|
|
// assign variables to the internal nodes
|
|
Aig_ManForEachNode( p, pObj, i )
|
|
pCnf->pVarNums[pObj->Id] = Number++;
|
|
// assign variables to the PIs and constant node
|
|
Aig_ManForEachCi( p, pObj, i )
|
|
pCnf->pVarNums[pObj->Id] = Number++;
|
|
pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
|
|
pCnf->nVars = Number;
|
|
/*
|
|
// print CNF numbers
|
|
printf( "SAT numbers of each node:\n" );
|
|
Aig_ManForEachObj( p, pObj, i )
|
|
printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] );
|
|
printf( "\n" );
|
|
*/
|
|
// assign the clauses
|
|
pLits = pCnf->pClauses[0];
|
|
pClas = pCnf->pClauses;
|
|
Aig_ManForEachNode( p, pObj, i )
|
|
{
|
|
OutVar = pCnf->pVarNums[ pObj->Id ];
|
|
pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
|
|
pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
|
|
|
|
// positive phase
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar;
|
|
*pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj);
|
|
*pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj);
|
|
// negative phase
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar + 1;
|
|
*pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj);
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar + 1;
|
|
*pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj);
|
|
}
|
|
|
|
// write the constant literal
|
|
OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
|
|
assert( OutVar <= Aig_ManObjNumMax(p) );
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar;
|
|
|
|
// write the output literals
|
|
Aig_ManForEachCo( p, pObj, i )
|
|
{
|
|
OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
|
|
if ( i < Aig_ManCoNum(p) - nOutputs )
|
|
{
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
|
|
}
|
|
else
|
|
{
|
|
PoVar = pCnf->pVarNums[ pObj->Id ];
|
|
// first clause
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * PoVar;
|
|
*pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
|
|
// second clause
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * PoVar + 1;
|
|
*pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
|
|
}
|
|
}
|
|
|
|
// verify that the correct number of literals and clauses was written
|
|
assert( pLits - pCnf->pClauses[0] == nLiterals );
|
|
assert( pClas - pCnf->pClauses == nClauses );
|
|
return pCnf;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Derives a simple CNF for backward retiming computation.]
|
|
|
|
Description [The last argument shows the number of last outputs
|
|
of the manager, which will not be converted into clauses.
|
|
New variables will be introduced for these outputs.]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p )
|
|
{
|
|
Aig_Obj_t * pObj;
|
|
Cnf_Dat_t * pCnf;
|
|
int OutVar, PoVar, pVars[32], * pLits, ** pClas;
|
|
int i, nLiterals, nClauses, Number;
|
|
|
|
// count the number of literals and clauses
|
|
nLiterals = 1 + 7 * Aig_ManNodeNum(p) + 5 * Aig_ManCoNum(p);
|
|
nClauses = 1 + 3 * Aig_ManNodeNum(p) + 3 * Aig_ManCoNum(p);
|
|
|
|
// allocate CNF
|
|
pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
|
|
memset( pCnf, 0, sizeof(Cnf_Dat_t) );
|
|
pCnf->pMan = p;
|
|
pCnf->nLiterals = nLiterals;
|
|
pCnf->nClauses = nClauses;
|
|
pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
|
|
pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
|
|
pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
|
|
|
|
// create room for variable numbers
|
|
pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p) );
|
|
// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
|
|
for ( i = 0; i < Aig_ManObjNumMax(p); i++ )
|
|
pCnf->pVarNums[i] = -1;
|
|
// assign variables to the last (nOutputs) POs
|
|
Number = 1;
|
|
Aig_ManForEachCo( p, pObj, i )
|
|
pCnf->pVarNums[pObj->Id] = Number++;
|
|
// assign variables to the internal nodes
|
|
Aig_ManForEachNode( p, pObj, i )
|
|
pCnf->pVarNums[pObj->Id] = Number++;
|
|
// assign variables to the PIs and constant node
|
|
Aig_ManForEachCi( p, pObj, i )
|
|
pCnf->pVarNums[pObj->Id] = Number++;
|
|
pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
|
|
pCnf->nVars = Number;
|
|
// assign the clauses
|
|
pLits = pCnf->pClauses[0];
|
|
pClas = pCnf->pClauses;
|
|
Aig_ManForEachNode( p, pObj, i )
|
|
{
|
|
OutVar = pCnf->pVarNums[ pObj->Id ];
|
|
pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
|
|
pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
|
|
|
|
// positive phase
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar;
|
|
*pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj);
|
|
*pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj);
|
|
// negative phase
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar + 1;
|
|
*pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj);
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar + 1;
|
|
*pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj);
|
|
}
|
|
|
|
// write the constant literal
|
|
OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
|
|
assert( OutVar <= Aig_ManObjNumMax(p) );
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * OutVar;
|
|
|
|
// write the output literals
|
|
Aig_ManForEachCo( p, pObj, i )
|
|
{
|
|
OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
|
|
PoVar = pCnf->pVarNums[ pObj->Id ];
|
|
// first clause
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * PoVar;
|
|
*pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
|
|
// second clause
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * PoVar + 1;
|
|
*pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
|
|
// final clause (init-state is always 0 -> set the output to 0)
|
|
*pClas++ = pLits;
|
|
*pLits++ = 2 * PoVar + 1;
|
|
}
|
|
|
|
// verify that the correct number of literals and clauses was written
|
|
assert( pLits - pCnf->pClauses[0] == nLiterals );
|
|
assert( pClas - pCnf->pClauses == nClauses );
|
|
return pCnf;
|
|
}
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// END OF FILE ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
ABC_NAMESPACE_IMPL_END
|
|
|