cnfCore.c 7.03 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
/**CFile****************************************************************

  FileName    [cnfCore.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: cnfCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]

***********************************************************************/

#include "cnf.h"

23 24 25
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
26 27 28 29
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

Alan Mishchenko committed
30 31
static Cnf_Man_t * s_pManCnf = NULL;

Alan Mishchenko committed
32 33 34
////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////
35 36 37 38 39 40 41 42 43 44 45 46 47 48 49
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cnf_ManPrepare()
{
    if ( s_pManCnf == NULL )
    {
50
//        printf( "\n\nCreating CNF manager!!!!!\n\n" );
51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
        s_pManCnf = Cnf_ManStart();
    }
}
Cnf_Man_t * Cnf_ManRead()
{
    return s_pManCnf;
}
void Cnf_ManFree()
{
    if ( s_pManCnf == NULL )
        return;
    Cnf_ManStop( s_pManCnf );
    s_pManCnf = NULL;
}

Alan Mishchenko committed
66 67 68

/**Function*************************************************************

Alan Mishchenko committed
69
  Synopsis    [Converts AIG into the SAT solver.]
Alan Mishchenko committed
70 71 72 73 74 75 76 77

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
78 79 80 81 82 83
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;
84
    abctime clk;
85
    // allocate the CNF manager
86
    p = Cnf_ManStart();
87 88 89
    p->pManAig = pAig;

    // generate cuts for all nodes, assign cost, and find best cuts
90
clk = Abc_Clock();
91
    pMemCuts = Dar_ManComputeCuts( pAig, 10, 0, 0 );
92
p->timeCuts = Abc_Clock() - clk;
93 94

    // find the mapping
95
clk = Abc_Clock();
96
    Cnf_DeriveMapping( p );
97
p->timeMap = Abc_Clock() - clk;
98 99 100
//    Aig_ManScanMapping( p, 1 );

    // convert it into CNF
101
clk = Abc_Clock();
102 103 104 105 106
    Cnf_ManTransferCuts( p );
    vMapped = Cnf_ManScanMapping( p, 1, 0 );
    vResult = Cnf_ManWriteCnfMapping( p, vMapped );
    Vec_PtrFree( vMapped );
    Aig_MmFixedStop( pMemCuts, 0 );
107
p->timeSave = Abc_Clock() - clk;
108 109 110 111 112 113

   // reset reference counters
    Aig_ManResetRefs( pAig );
//ABC_PRT( "Cuts   ", p->timeCuts );
//ABC_PRT( "Map    ", p->timeMap  );
//ABC_PRT( "Saving ", p->timeSave );
114
    Cnf_ManStop( p );
115 116 117 118 119 120 121 122 123 124 125 126 127 128
    return vResult;
}
 
/**Function*************************************************************

  Synopsis    [Converts AIG into the SAT solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
129
Cnf_Dat_t * Cnf_DeriveWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int nOutputs )
Alan Mishchenko committed
130
{
Alan Mishchenko committed
131
    Cnf_Dat_t * pCnf;
Alan Mishchenko committed
132
    Vec_Ptr_t * vMapped;
Alan Mishchenko committed
133
    Aig_MmFixed_t * pMemCuts;
134
    abctime clk;
Alan Mishchenko committed
135 136 137 138
    // connect the managers
    p->pManAig = pAig;

    // generate cuts for all nodes, assign cost, and find best cuts
139
clk = Abc_Clock();
140
    pMemCuts = Dar_ManComputeCuts( pAig, 10, 0, 0 );
141
p->timeCuts = Abc_Clock() - clk;
Alan Mishchenko committed
142 143

    // find the mapping
144
clk = Abc_Clock();
Alan Mishchenko committed
145
    Cnf_DeriveMapping( p );
146
p->timeMap = Abc_Clock() - clk;
Alan Mishchenko committed
147 148 149
//    Aig_ManScanMapping( p, 1 );

    // convert it into CNF
150
clk = Abc_Clock();
Alan Mishchenko committed
151 152
    Cnf_ManTransferCuts( p );
    vMapped = Cnf_ManScanMapping( p, 1, 1 );
Alan Mishchenko committed
153
    pCnf = Cnf_ManWriteCnf( p, vMapped, nOutputs );
Alan Mishchenko committed
154 155
    Vec_PtrFree( vMapped );
    Aig_MmFixedStop( pMemCuts, 0 );
156
p->timeSave = Abc_Clock() - clk;
Alan Mishchenko committed
157

Alan Mishchenko committed
158 159
   // reset reference counters
    Aig_ManResetRefs( pAig );
Alan Mishchenko committed
160 161 162
//ABC_PRT( "Cuts   ", p->timeCuts );
//ABC_PRT( "Map    ", p->timeMap  );
//ABC_PRT( "Saving ", p->timeSave );
163 164
    return pCnf;
}
165 166 167 168 169
Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs )
{
    Cnf_ManPrepare();
    return Cnf_DeriveWithMan( s_pManCnf, pAig, nOutputs );
}
170 171 172 173 174 175 176 177 178 179 180 181
 
/**Function*************************************************************

  Synopsis    [Converts AIG into the SAT solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
182
Cnf_Dat_t * Cnf_DeriveOtherWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int fSkipTtMin )
183 184 185 186
{
    Cnf_Dat_t * pCnf;
    Vec_Ptr_t * vMapped;
    Aig_MmFixed_t * pMemCuts;
187
    abctime clk;
188 189 190 191
    // connect the managers
    p->pManAig = pAig;

    // generate cuts for all nodes, assign cost, and find best cuts
192
clk = Abc_Clock();
193
    pMemCuts = Dar_ManComputeCuts( pAig, 10, fSkipTtMin, 0 );
194
p->timeCuts = Abc_Clock() - clk;
195 196

    // find the mapping
197
clk = Abc_Clock();
198
    Cnf_DeriveMapping( p );
199
p->timeMap = Abc_Clock() - clk;
200 201 202
//    Aig_ManScanMapping( p, 1 );

    // convert it into CNF
203
clk = Abc_Clock();
204 205 206
    Cnf_ManTransferCuts( p );
    vMapped = Cnf_ManScanMapping( p, 1, 1 );
    pCnf = Cnf_ManWriteCnfOther( p, vMapped );
207
    pCnf->vMapping = Cnf_ManWriteCnfMapping( p, vMapped );
208 209
    Vec_PtrFree( vMapped );
    Aig_MmFixedStop( pMemCuts, 0 );
210
p->timeSave = Abc_Clock() - clk;
211 212 213 214 215 216

   // reset reference counters
    Aig_ManResetRefs( pAig );
//ABC_PRT( "Cuts   ", p->timeCuts );
//ABC_PRT( "Map    ", p->timeMap  );
//ABC_PRT( "Saving ", p->timeSave );
Alan Mishchenko committed
217 218
    return pCnf;
}
219
Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig, int fSkipTtMin )
Alan Mishchenko committed
220
{
221 222
    Cnf_ManPrepare();
    return Cnf_DeriveOtherWithMan( s_pManCnf, pAig, fSkipTtMin );
Alan Mishchenko committed
223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239
}

#if 0

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Cnf_Dat_t * Cnf_Derive_old( Aig_Man_t * pAig )
{
Alan Mishchenko committed
240 241 242 243
/*
    // iteratively improve area flow
    for ( i = 0; i < nIters; i++ )
    {
244
clk = Abc_Clock();
Alan Mishchenko committed
245 246
        Cnf_ManScanMapping( p, 0 );
        Cnf_ManMapForCnf( p );
247
ABC_PRT( "iter ", Abc_Clock() - clk );
Alan Mishchenko committed
248 249 250
    }
*/
    // write the file
Alan Mishchenko committed
251
    vMapped = Aig_ManScanMapping( p, 1 );
Alan Mishchenko committed
252 253
    Vec_PtrFree( vMapped );

254
clk = Abc_Clock();
Alan Mishchenko committed
255 256 257 258 259 260 261 262 263 264
    Cnf_ManTransferCuts( p );

    Cnf_ManPostprocess( p );
    Cnf_ManScanMapping( p, 0 );
/*
    Cnf_ManPostprocess( p );
    Cnf_ManScanMapping( p, 0 );
    Cnf_ManPostprocess( p );
    Cnf_ManScanMapping( p, 0 );
*/
265
ABC_PRT( "Ext ", Abc_Clock() - clk );
Alan Mishchenko committed
266 267 268 269 270 271 272 273 274 275 276

/*
    vMapped = Cnf_ManScanMapping( p, 1 );
    pCnf = Cnf_ManWriteCnf( p, vMapped );
    Vec_PtrFree( vMapped );

    // clean up
    Cnf_ManFreeCuts( p );
    Dar_ManCutsFree( pAig );
    return pCnf;
*/
Alan Mishchenko committed
277
    Aig_MmFixedStop( pMemCuts, 0 );
Alan Mishchenko committed
278 279 280
    return NULL;
}

Alan Mishchenko committed
281 282 283
#endif


Alan Mishchenko committed
284 285 286 287 288
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


289 290
ABC_NAMESPACE_IMPL_END