summaryrefslogtreecommitdiffstats
path: root/src/sat/cnf/cnf.h
blob: f4c96709080c0dc5bb2becfbbd2c96b9bb09bba3 (plain)
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
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
/**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 ABC__aig__cnf__cnf_h
#define ABC__aig__cnf__cnf_h


////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>

#include "misc/vec/vec.h"
#include "aig/aig/aig.h"
#include "opt/dar/darInt.h"

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////



ABC_NAMESPACE_HEADER_START
 

////////////////////////////////////////////////////////////////////////
///                         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)
    int *           pObj2Clause;     // the mapping of objects into clauses
    int *           pObj2Count;      // the mapping of objects into clause number
    Vec_Int_t *     vMapping;        // mapping of internal nodes
};

// 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
    clock_t         timeCuts; 
    clock_t         timeMap;
    clock_t         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 (Cnf_Cut_t *)pObj->pData;  }
static inline void         Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut )  { pObj->pData = pCut;  }

////////////////////////////////////////////////////////////////////////
///                      MACRO DEFINITIONS                           ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                           ITERATORS                              ///
////////////////////////////////////////////////////////////////////////

// iterator over the clauses
#define Cnf_CnfForClause( p, pBeg, pEnd, i )                         \
    for ( i = 0; i < p->nClauses && (pBeg = p->pClauses[i]) && (pEnd = p->pClauses[i+1]); i++ )

// 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 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_DeriveWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int nOutputs );
extern Cnf_Dat_t *     Cnf_DeriveOther( Aig_Man_t * pAig, int fSkipTtMin );
extern Cnf_Dat_t *     Cnf_DeriveOtherWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int fSkipTtMin );
extern void            Cnf_ManPrepare();
extern Cnf_Man_t *     Cnf_ManRead();
extern void            Cnf_ManFree();
/*=== 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 );
/*=== cnfFast.c ========================================================*/
extern void            Cnf_CollectLeaves( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper, int fStopCompl );
extern void            Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, 
                           Vec_Ptr_t * vNodes, Vec_Int_t * vMap, Vec_Int_t * vCover, Vec_Int_t * vClauses );
extern void            Cnf_DeriveFastMark( Aig_Man_t * p );
extern Cnf_Dat_t *     Cnf_DeriveFast( Aig_Man_t * p, int nOutputs );
/*=== 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_DataFlipLastLiteral( Cnf_Dat_t * p );
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 void *          Cnf_DataWriteIntoSolverInt( void * pSat, Cnf_Dat_t * p, int nFrames, int fInit );
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 );
/*=== 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 );
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_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 );



ABC_NAMESPACE_HEADER_END



#endif

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////