1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
|
/**CFile****************************************************************
FileName [cnf.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware AIG rewriting.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: cnf.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __CNF_H__
#define __CNF_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "vec.h"
#include "aig.h"
#include "darInt.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Cnf_Man_t_ Cnf_Man_t;
typedef struct Cnf_Dat_t_ Cnf_Dat_t;
typedef struct Cnf_Cut_t_ Cnf_Cut_t;
// the CNF asserting outputs of AIG to be 1
struct Cnf_Dat_t_
{
Aig_Man_t * pMan; // the AIG manager, for which CNF is computed
int nVars; // the number of variables
int nLiterals; // the number of CNF literals
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)
};
// the cut used to represent node in the AIG
struct Cnf_Cut_t_
{
char nFanins; // the number of leaves
char Cost; // the cost of this cut
short nWords; // the number of words in truth table
Vec_Int_t * vIsop[2]; // neg/pos ISOPs
int pFanins[0]; // the fanins (followed by the truth table)
};
// the CNF computation manager
struct Cnf_Man_t_
{
Aig_Man_t * pManAig; // the underlying AIG manager
char * pSopSizes; // sizes of SOPs for 4-variable functions
char ** pSops; // the SOPs for 4-variable functions
int aArea; // the area of the mapping
Aig_MmFlex_t * pMemCuts; // memory manager for cuts
int nMergeLimit; // the limit on the size of merged cut
unsigned * pTruths[4]; // temporary truth tables
Vec_Int_t * vMemory; // memory for intermediate ISOP representation
int timeCuts;
int timeMap;
int timeSave;
};
static inline Dar_Cut_t * Dar_ObjBestCut( Aig_Obj_t * pObj ) { Dar_Cut_t * pCut; int i; Dar_ObjForEachCut( pObj, pCut, i ) if ( pCut->fBest ) return pCut; return NULL; }
static inline int Cnf_CutSopCost( Cnf_Man_t * p, Dar_Cut_t * pCut ) { return p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth]; }
static inline int Cnf_CutLeaveNum( Cnf_Cut_t * pCut ) { return pCut->nFanins; }
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 void Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut ) { pObj->pData = pCut; }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
// iterator over leaves of the cut
#define Cnf_CutForEachLeaf( p, pCut, pLeaf, i ) \
for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== cnfCore.c ========================================================*/
extern Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs );
extern Cnf_Man_t * Cnf_ManRead();
extern void Cnf_ClearMemory();
/*=== cnfCut.c ========================================================*/
extern Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj );
extern void Cnf_CutPrint( Cnf_Cut_t * pCut );
extern void Cnf_CutFree( Cnf_Cut_t * pCut );
extern void Cnf_CutUpdateRefs( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, Cnf_Cut_t * pCutRes );
extern Cnf_Cut_t * Cnf_CutCompose( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, int iFan );
/*=== cnfData.c ========================================================*/
extern void Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops );
/*=== cnfMan.c ========================================================*/
extern Cnf_Man_t * Cnf_ManStart();
extern void Cnf_ManStop( Cnf_Man_t * p );
extern Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
extern Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals );
extern Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p );
extern void Cnf_DataFree( Cnf_Dat_t * p );
extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
extern void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable );
extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
extern int Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );
/*=== cnfMap.c ========================================================*/
extern void Cnf_DeriveMapping( Cnf_Man_t * p );
extern int Cnf_ManMapForCnf( Cnf_Man_t * p );
/*=== cnfPost.c ========================================================*/
extern void Cnf_ManTransferCuts( Cnf_Man_t * p );
extern void Cnf_ManFreeCuts( Cnf_Man_t * p );
extern void Cnf_ManPostprocess( Cnf_Man_t * p );
/*=== cnfUtil.c ========================================================*/
extern Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect );
extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder );
/*=== cnfWrite.c ========================================================*/
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
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
