summaryrefslogtreecommitdiffstats
path: root/src/aig/cnf
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/cnf')
-rw-r--r--src/aig/cnf/cnf.h21
-rw-r--r--src/aig/cnf/cnfCore.c58
-rw-r--r--src/aig/cnf/cnfCut.c5
-rw-r--r--src/aig/cnf/cnfData.c9
-rw-r--r--src/aig/cnf/cnfMan.c52
-rw-r--r--src/aig/cnf/cnfMap.c7
-rw-r--r--src/aig/cnf/cnfPost.c7
-rw-r--r--src/aig/cnf/cnfUtil.c11
-rw-r--r--src/aig/cnf/cnfWrite.c48
-rw-r--r--src/aig/cnf/cnf_.c5
10 files changed, 204 insertions, 19 deletions
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index f7d1d38c..7c3bf06b 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -21,6 +21,7 @@
#ifndef __CNF_H__
#define __CNF_H__
+
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -39,9 +40,10 @@
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
-#ifdef __cplusplus
-extern "C" {
-#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
@@ -97,7 +99,7 @@ static inline int Cnf_CutLeaveNum( Cnf_Cut_t * pCut ) { return pCut-
static inline int * Cnf_CutLeaves( Cnf_Cut_t * pCut ) { return pCut->pFanins; }
static inline unsigned * Cnf_CutTruth( Cnf_Cut_t * pCut ) { return (unsigned *)(pCut->pFanins + pCut->nFanins); }
-static inline Cnf_Cut_t * Cnf_ObjBestCut( Aig_Obj_t * pObj ) { return pObj->pData; }
+static inline Cnf_Cut_t * Cnf_ObjBestCut( Aig_Obj_t * pObj ) { return (Cnf_Cut_t *)pObj->pData; }
static inline void Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut ) { pObj->pData = pCut; }
////////////////////////////////////////////////////////////////////////
@@ -121,6 +123,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_Man_t * Cnf_ManRead();
extern void Cnf_ClearMemory();
@@ -147,6 +150,7 @@ extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int
extern int Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );
extern int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf );
extern void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf, int fTransformPos );
+extern int Cnf_DataAddXorClause( void * pSat, int iVarA, int iVarB, int iVarC );
/*=== cnfMap.c ========================================================*/
extern void Cnf_DeriveMapping( Cnf_Man_t * p );
extern int Cnf_ManMapForCnf( Cnf_Man_t * p );
@@ -160,14 +164,17 @@ extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPre
extern Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
extern Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
/*=== cnfWrite.c ========================================================*/
+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_DeriveSimple( Aig_Man_t * p, int nOutputs );
extern Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p );
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
#endif
diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c
index 11a7af43..85c971c2 100644
--- a/src/aig/cnf/cnfCore.c
+++ b/src/aig/cnf/cnfCore.c
@@ -20,6 +20,9 @@
#include "cnf.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -41,6 +44,59 @@ static Cnf_Man_t * s_pManCnf = NULL;
SeeAlso []
***********************************************************************/
+Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig )
+{
+ Vec_Int_t * vResult;
+ Cnf_Man_t * p;
+ 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, 0 );
+ vResult = Cnf_ManWriteCnfMapping( 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 vResult;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts AIG into the SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs )
{
Cnf_Man_t * p;
@@ -183,3 +239,5 @@ ABC_PRT( "Ext ", clock() - clk );
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cnf/cnfCut.c b/src/aig/cnf/cnfCut.c
index 17ab0c78..d41fc1fc 100644
--- a/src/aig/cnf/cnfCut.c
+++ b/src/aig/cnf/cnfCut.c
@@ -21,6 +21,9 @@
#include "cnf.h"
#include "kit.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -369,3 +372,5 @@ Cnf_Cut_t * Cnf_CutCompose( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cnf/cnfData.c b/src/aig/cnf/cnfData.c
index 8df93fdb..e4798688 100644
--- a/src/aig/cnf/cnfData.c
+++ b/src/aig/cnf/cnfData.c
@@ -20,13 +20,16 @@
#include "cnf.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static char s_Data3[81] = "!#&()*+,-.0123456789:;<=>?ABCDEFGHIJKLMNOPQRSTUVWXYZ[]abcdefghijklmnopqrstuvwxyz|";
+static const char s_Data3[82] = "!#&()*+,-.0123456789:;<=>?ABCDEFGHIJKLMNOPQRSTUVWXYZ[]abcdefghijklmnopqrstuvwxyz|";
-static char * s_Data4[] = {
+static const char * s_Data4[] = {
"! B a . 8 .B 8a K !K T Ta j 8j Tj s ( + (B +a (. +8 .B( +8a (K +K T( +T j( ",
"+j Tj( s+ E !E H Ha E. 8E H. H8 EK EK! HT HTa jE 8jE Hj sH d +d Hd g d. 8d ",
"Hd. g8 dK +dK Td gT dj +jd Hjd gs 2 !2 2B a2 5 58 5B 5a 2K 2K! T2 Ta2 5j 58",
@@ -4782,3 +4785,5 @@ int Aig_ManDeriveCnfTest2()
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index f8e88b8f..762673ad 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -22,6 +22,9 @@
#include "satSolver.h"
#include "zlib.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -422,7 +425,7 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
***********************************************************************/
int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
{
- sat_solver * pSat = p;
+ sat_solver * pSat = (sat_solver *)p;
Aig_Obj_t * pObj;
int i, * pLits;
pLits = ABC_ALLOC( int, Aig_ManPoNum(pCnf->pMan) );
@@ -450,7 +453,7 @@ int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
***********************************************************************/
int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf )
{
- sat_solver * pSat = p;
+ sat_solver * pSat = (sat_solver *)p;
Aig_Obj_t * pObj;
int i, Lit;
Aig_ManForEachPo( pCnf->pMan, pObj, i )
@@ -498,8 +501,53 @@ void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf, int fTransformPos )
ABC_FREE( pVarToPol );
}
+/**Function*************************************************************
+
+ Synopsis [Adds constraints for the two-input AND-gate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cnf_DataAddXorClause( void * pSat, int iVarA, int iVarB, int iVarC )
+{
+ lit Lits[3];
+ assert( iVarA > 0 && iVarB > 0 && iVarC > 0 );
+
+ Lits[0] = toLitCond( iVarA, 1 );
+ Lits[1] = toLitCond( iVarB, 1 );
+ Lits[2] = toLitCond( iVarC, 1 );
+ if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
+ return 0;
+
+ Lits[0] = toLitCond( iVarA, 1 );
+ Lits[1] = toLitCond( iVarB, 0 );
+ Lits[2] = toLitCond( iVarC, 0 );
+ if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
+ return 0;
+
+ Lits[0] = toLitCond( iVarA, 0 );
+ Lits[1] = toLitCond( iVarB, 1 );
+ Lits[2] = toLitCond( iVarC, 0 );
+ if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
+ return 0;
+
+ Lits[0] = toLitCond( iVarA, 0 );
+ Lits[1] = toLitCond( iVarB, 0 );
+ Lits[2] = toLitCond( iVarC, 1 );
+ if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
+ return 0;
+
+ return 1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cnf/cnfMap.c b/src/aig/cnf/cnfMap.c
index 58c9b803..8907485e 100644
--- a/src/aig/cnf/cnfMap.c
+++ b/src/aig/cnf/cnfMap.c
@@ -20,6 +20,9 @@
#include "cnf.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -72,7 +75,7 @@ int Cnf_CutSuperAreaFlow( Vec_Ptr_t * vSuper, int * pAreaFlows )
Aig_Obj_t * pLeaf;
int i, nAreaFlow;
nAreaFlow = 100 * (Vec_PtrSize(vSuper) + 1);
- Vec_PtrForEachEntry( vSuper, pLeaf, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pLeaf, i )
{
pLeaf = Aig_Regular(pLeaf);
if ( !Aig_ObjIsNode(pLeaf) )
@@ -355,3 +358,5 @@ int Cnf_ManMapForCnf( Cnf_Man_t * p )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cnf/cnfPost.c b/src/aig/cnf/cnfPost.c
index 988275b2..f7491889 100644
--- a/src/aig/cnf/cnfPost.c
+++ b/src/aig/cnf/cnfPost.c
@@ -20,6 +20,9 @@
#include "cnf.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -143,7 +146,7 @@ void Cnf_ManFreeCuts( Cnf_Man_t * p )
Aig_ManForEachObj( p->pManAig, pObj, i )
if ( pObj->pData )
{
- Cnf_CutFree( pObj->pData );
+ Cnf_CutFree( (Cnf_Cut_t *)pObj->pData );
pObj->pData = NULL;
}
}
@@ -231,3 +234,5 @@ void Cnf_ManPostprocess( Cnf_Man_t * p )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cnf/cnfUtil.c b/src/aig/cnf/cnfUtil.c
index 7da9fb47..236b6bfa 100644
--- a/src/aig/cnf/cnfUtil.c
+++ b/src/aig/cnf/cnfUtil.c
@@ -20,6 +20,9 @@
#include "cnf.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -56,7 +59,7 @@ int Aig_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 );
Aig_ObjCollectSuper( pObj, vSuper );
aArea = Vec_PtrSize(vSuper) + 1;
- Vec_PtrForEachEntry( vSuper, pLeaf, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pLeaf, i )
aArea += Aig_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped );
Vec_PtrFree( vSuper );
////////////////////////////
@@ -131,7 +134,7 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 );
Aig_ObjCollectSuper( pObj, vSuper );
aArea = Vec_PtrSize(vSuper) + 1;
- Vec_PtrForEachEntry( vSuper, pLeaf, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pLeaf, i )
aArea += Cnf_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped, fPreorder );
Vec_PtrFree( vSuper );
////////////////////////////
@@ -139,7 +142,7 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
}
else
{
- pCutBest = pObj->pData;
+ pCutBest = (Cnf_Cut_t *)pObj->pData;
// assert( pCutBest->nFanins > 0 );
assert( pCutBest->Cost < 127 );
aArea = pCutBest->Cost;
@@ -231,3 +234,5 @@ Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index 638e67da..4f737305 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -20,6 +20,9 @@
#include "cnf.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -30,6 +33,43 @@
/**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 []
@@ -169,7 +209,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
// count the number of literals and clauses
nLiterals = 1 + Aig_ManPoNum( p->pManAig ) + 3 * nOutputs;
nClauses = 1 + Aig_ManPoNum( p->pManAig ) + nOutputs;
- Vec_PtrForEachEntry( vMapped, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
{
assert( Aig_ObjIsNode(pObj) );
pCut = Cnf_ObjBestCut( pObj );
@@ -237,7 +277,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
}
}
// assign variables to the internal nodes
- Vec_PtrForEachEntry( vMapped, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
// assign variables to the PIs and constant node
Aig_ManForEachPi( p->pManAig, pObj, i )
@@ -249,7 +289,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
vSopTemp = Vec_IntAlloc( 1 << 16 );
pLits = pCnf->pClauses[0];
pClas = pCnf->pClauses;
- Vec_PtrForEachEntry( vMapped, pObj, i )
+ Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
{
pCut = Cnf_ObjBestCut( pObj );
@@ -562,3 +602,5 @@ Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cnf/cnf_.c b/src/aig/cnf/cnf_.c
index 7c9ca499..acf75093 100644
--- a/src/aig/cnf/cnf_.c
+++ b/src/aig/cnf/cnf_.c
@@ -20,6 +20,9 @@
#include "cnf.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -46,3 +49,5 @@
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 18:27:21 +0000