summaryrefslogtreecommitdiffstats
path: root/src/aig/cnf
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/cnf')
-rw-r--r--src/aig/cnf/cnf.h4
-rw-r--r--src/aig/cnf/cnfCore.c53
-rw-r--r--src/aig/cnf/cnfMan.c2
-rw-r--r--src/aig/cnf/cnfWrite.c171
4 files changed, 228 insertions, 2 deletions
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index 7c3bf06b..42dcd9a9 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -62,6 +62,8 @@ struct Cnf_Dat_t_
int nClauses; // the number of CNF clauses
int ** pClauses; // the CNF clauses
int * pVarNums; // the number of CNF variable for each node ID (-1 if unused)
+ int * pObj2Clause; // the mapping of objects into clauses
+ int * pObj2Count; // the mapping of objects into clause number
};
// the cut used to represent node in the AIG
@@ -125,6 +127,7 @@ static inline void Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut
/*=== cnfCore.c ========================================================*/
extern Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig );
extern Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs );
+extern Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig );
extern Cnf_Man_t * Cnf_ManRead();
extern void Cnf_ClearMemory();
/*=== cnfCut.c ========================================================*/
@@ -167,6 +170,7 @@ extern Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p
extern Vec_Int_t * Cnf_ManWriteCnfMapping( Cnf_Man_t * p, Vec_Ptr_t * vMapped );
extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs );
+extern Cnf_Dat_t * Cnf_ManWriteCnfOther( Cnf_Man_t * p, Vec_Ptr_t * vMapped );
extern Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs );
extern Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p );
diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c
index 85c971c2..eb46e704 100644
--- a/src/aig/cnf/cnfCore.c
+++ b/src/aig/cnf/cnfCore.c
@@ -138,6 +138,59 @@ p->timeSave = clock() - clk;
//ABC_PRT( "Saving ", p->timeSave );
return pCnf;
}
+
+/**Function*************************************************************
+
+ Synopsis [Converts AIG into the SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig )
+{
+ Cnf_Man_t * p;
+ Cnf_Dat_t * pCnf;
+ Vec_Ptr_t * vMapped;
+ Aig_MmFixed_t * pMemCuts;
+ int clk;
+ // allocate the CNF manager
+ if ( s_pManCnf == NULL )
+ s_pManCnf = Cnf_ManStart();
+ // connect the managers
+ p = s_pManCnf;
+ p->pManAig = pAig;
+
+ // generate cuts for all nodes, assign cost, and find best cuts
+clk = clock();
+ pMemCuts = Dar_ManComputeCuts( pAig, 10, 0 );
+p->timeCuts = clock() - clk;
+
+ // find the mapping
+clk = clock();
+ Cnf_DeriveMapping( p );
+p->timeMap = clock() - clk;
+// Aig_ManScanMapping( p, 1 );
+
+ // convert it into CNF
+clk = clock();
+ Cnf_ManTransferCuts( p );
+ vMapped = Cnf_ManScanMapping( p, 1, 1 );
+ pCnf = Cnf_ManWriteCnfOther( p, vMapped );
+ Vec_PtrFree( vMapped );
+ Aig_MmFixedStop( pMemCuts, 0 );
+p->timeSave = clock() - clk;
+
+ // reset reference counters
+ Aig_ManResetRefs( pAig );
+//ABC_PRT( "Cuts ", p->timeCuts );
+//ABC_PRT( "Map ", p->timeMap );
+//ABC_PRT( "Saving ", p->timeSave );
+ return pCnf;
+}
/**Function*************************************************************
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 762673ad..837ca2c2 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -180,6 +180,8 @@ void Cnf_DataFree( Cnf_Dat_t * p )
{
if ( p == NULL )
return;
+ ABC_FREE( p->pObj2Clause );
+ ABC_FREE( p->pObj2Count );
ABC_FREE( p->pClauses[0] );
ABC_FREE( p->pClauses );
ABC_FREE( p->pVarNums );
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index 4f737305..7a9443f2 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -245,8 +245,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
//printf( "\n" );
// allocate CNF
- pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
- memset( pCnf, 0, sizeof(Cnf_Dat_t) );
+ pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
pCnf->pMan = p->pManAig;
pCnf->nLiterals = nLiterals;
pCnf->nClauses = nClauses;
@@ -367,6 +366,174 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
// 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_ManPoNum( p->pManAig );
+ nClauses = 1 + 2 * Aig_ManPoNum( 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_ManForEachPi( 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_ManForEachPo( 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;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 09:59:17 +0000