summaryrefslogtreecommitdiffstats
path: root/src/aig/fra/fra.h
blob: f661d2e58cbb7aa0cc03b950cec6a3d4ce4a0069 (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
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
/**CFile****************************************************************

  FileName    [fra.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [[New FRAIG package.]

  Synopsis    [External declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 30, 2007.]

  Revision    [$Id: fra.h,v 1.00 2007/06/30 00:00:00 alanmi Exp $]

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

#ifndef __FRA_H__
#define __FRA_H__

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

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

#include "vec.h"
#include "aig.h"
#include "dar.h"
#include "satSolver.h"
#include "ioa.h"

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

#ifdef __cplusplus
extern "C" {
#endif 

////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Fra_Par_t_   Fra_Par_t;
typedef struct Fra_Ssw_t_   Fra_Ssw_t;
typedef struct Fra_Sec_t_   Fra_Sec_t;
typedef struct Fra_Man_t_   Fra_Man_t;
typedef struct Fra_Cla_t_   Fra_Cla_t;
typedef struct Fra_Sml_t_   Fra_Sml_t;
typedef struct Fra_Cex_t_   Fra_Cex_t;
typedef struct Fra_Bmc_t_   Fra_Bmc_t;

// FRAIG parameters
struct Fra_Par_t_
{
    int              nSimWords;         // the number of words in the simulation info
    double           dSimSatur;         // the ratio of refined classes when saturation is reached
    int              fPatScores;        // enables simulation pattern scoring
    int              MaxScore;          // max score after which resimulation is used
    double           dActConeRatio;     // the ratio of cone to be bumped
    double           dActConeBumpMax;   // the largest bump in activity
    int              fChoicing;         // enables choicing
    int              fSpeculate;        // use speculative reduction
    int              fProve;            // prove the miter outputs
    int              fVerbose;          // verbose output
    int              fDoSparse;         // skip sparse functions
    int              fConeBias;         // bias variables in the cone (good for unsat runs)
    int              nBTLimitNode;      // conflict limit at a node
    int              nBTLimitMiter;     // conflict limit at an output
    int              nLevelMax;         // the max level to consider seriously
    int              nFramesP;          // the number of timeframes to in the prefix
    int              nFramesK;          // the number of timeframes to unroll
    int              nMaxImps;          // the maximum number of implications to consider
    int              nMaxLevs;          // the maximum number of levels to consider
    int              fRewrite;          // use rewriting for constraint reduction
    int              fLatchCorr;        // computes latch correspondence only
    int              fUseImps;          // use implications
    int              fUse1Hot;          // use one-hotness conditions
    int              fWriteImps;        // record implications
    int              fDontShowBar;      // does not show progressbar during fraiging
};

// seq SAT sweeping parameters
struct Fra_Ssw_t_
{
    int              nPartSize;         // size of the partition
    int              nOverSize;         // size of the overlap between partitions
    int              nFramesP;          // number of frames in the prefix
    int              nFramesK;          // number of frames for induction (1=simple) 
    int              nMaxImps;          // max implications to consider
    int              nMaxLevs;          // max levels to consider
    int              nMinDomSize;       // min clock domain considered for optimization
    int              fUseImps;          // use implications  
    int              fRewrite;          // enable rewriting of the specualatively reduced model
    int              fFraiging;         // enable comb SAT sweeping as preprocessing 
    int              fLatchCorr;        // perform register correspondence
    int              fWriteImps;        // write implications into a file
    int              fUse1Hot;          // use one-hotness constraints
    int              fVerbose;          // enable verbose output 
    int              fSilent;           // disable any output 
    int              nIters;            // the number of iterations performed
    float            TimeLimit;         // the runtime budget for this call
};

// SEC parametesr
struct Fra_Sec_t_
{
    int              fTryComb;          // try CEC call as a preprocessing step
    int              fTryBmc;           // try BMC call as a preprocessing step 
    int              nFramesMax;        // the max number of frames used for induction
    int              nBTLimit;          // the conflict limit at a node
    int              nBTLimitGlobal;    // the global conflict limit
    int              nBTLimitInter;     // the conflict limit for interpolation
    int              nBddVarsMax;       // the state space limit for BDD reachability
    int              nBddMax;           // the max number of BDD nodes
    int              nBddIterMax;       // the limit on the number of BDD iterations
    int              fPhaseAbstract;    // enables phase abstraction
    int              fRetimeFirst;      // enables most-forward retiming at the beginning
    int              fRetimeRegs;       // enables min-register retiming at the beginning
    int              fFraiging;         // enables fraiging at the beginning
    int              fInduction;        // enable the use of induction
    int              fInterpolation;    // enables interpolation
    int              fInterSeparate;    // enables interpolation for each outputs separately
    int              fReachability;     // enables BDD based reachability
    int              fReorderImage;     // enables BDD reordering during image computation
    int              fStopOnFirstFail;  // enables stopping after first output of a miter has failed to prove
    int              fUseNewProver;     // the new prover
    int              fSilent;           // disables all output
    int              fVerbose;          // enables verbose reporting of statistics
    int              fVeryVerbose;      // enables very verbose reporting  
    int              TimeLimit;         // enables the timeout
    int              fReadUnsolved;     // inserts the unsolved model back
    int              nSMnumber;         // the number of model written
    // internal parameters
    int              fRecursive;        // set to 1 when SEC is called recursively
    int              fReportSolution;   // enables report solution in a special form
};

// FRAIG equivalence classes
struct Fra_Cla_t_
{
    Aig_Man_t *      pAig;              // the original AIG manager
    Aig_Obj_t **     pMemRepr;          // pointers to representatives of each node
    Vec_Ptr_t *      vClasses;          // equivalence classes
    Vec_Ptr_t *      vClasses1;         // equivalence class of Const1 node
    Vec_Ptr_t *      vClassesTemp;      // temporary storage for new classes
    Aig_Obj_t **     pMemClasses;       // memory allocated for equivalence classes
    Aig_Obj_t **     pMemClassesFree;   // memory allocated for equivalence classes to be used
    Vec_Ptr_t *      vClassOld;         // old equivalence class after splitting
    Vec_Ptr_t *      vClassNew;         // new equivalence class(es) after splitting
    int              nPairs;            // the number of pairs of nodes
    int              fRefinement;       // set to 1 when refinement has happened
    Vec_Int_t *      vImps;             // implications
    // procedures used for class refinement
    int (*pFuncNodeHash)     (Aig_Obj_t *, int);         // returns has key of the node
    int (*pFuncNodeIsConst)  (Aig_Obj_t *);              // returns 1 if the node is a constant
    int (*pFuncNodesAreEqual)(Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
};

// simulation manager
struct Fra_Sml_t_
{
    Aig_Man_t *      pAig;              // the original AIG manager
    int              nPref;             // the number of times frames in the prefix
    int              nFrames;           // the number of times frames 
    int              nWordsFrame;       // the number of words in each time frame
    int              nWordsTotal;       // the total number of words at a node
    int              nWordsPref;        // the number of word in the prefix
    int              fNonConstOut;      // have seen a non-const-0 output during simulation
    int              nSimRounds;        // statistics
    int              timeSim;           // statistics
    unsigned         pData[0];          // simulation data for the nodes
};

// simulation manager
struct Fra_Cex_t_
{
    int              iPo;               // the zero-based number of PO, for which verification failed
    int              iFrame;            // the zero-based number of the time-frame, for which verificaiton failed
    int              nRegs;             // the number of registers in the miter 
    int              nPis;              // the number of primary inputs in the miter
    int              nBits;             // the number of words of bit data used
    unsigned         pData[0];          // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis)
};

// FRAIG manager
struct Fra_Man_t_
{
    // high-level data    
    Fra_Par_t *      pPars;             // parameters governing fraiging
    // AIG managers
    Aig_Man_t *      pManAig;           // the starting AIG manager
    Aig_Man_t *      pManFraig;         // the final AIG manager
    // mapping AIG into FRAIG
    int              nFramesAll;        // the number of timeframes used
    Aig_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
    int              nSizeAlloc;        // allocated size of the arrays for timeframe nodes
    // equivalence classes 
    Fra_Cla_t *      pCla;              // representation of (candidate) equivalent nodes
    // simulation info
    Fra_Sml_t *      pSml;              // simulation manager
    // bounded model checking manager
    Fra_Bmc_t *      pBmc;
    // counter example storage
    int              nPatWords;         // the number of words in the counter example
    unsigned *       pPatWords;         // the counter example
    Vec_Int_t *      vCex;
    // one-hotness conditions
    Vec_Int_t *      vOneHots;          
    // satisfiability solving
    sat_solver *     pSat;              // SAT solver
    int              nSatVars;          // the number of variables currently used
    Vec_Ptr_t *      vPiVars;           // the PIs of the cone used 
    ABC_INT64_T           nBTLimitGlobal;    // resource limit
    ABC_INT64_T           nInsLimitGlobal;   // resource limit
    Vec_Ptr_t **     pMemFanins;        // the arrays of fanins for some FRAIG nodes
    int *            pMemSatNums;       // the array of SAT numbers for some FRAIG nodes
    int              nMemAlloc;         // allocated size of the arrays for FRAIG varnums and fanins
    Vec_Ptr_t *      vTimeouts;         // the nodes, for which equivalence checking timed out
    // statistics
    int              nSimRounds;
    int              nNodesMiter;
    int              nLitsBeg;
    int              nLitsEnd;
    int              nNodesBeg;
    int              nNodesEnd;
    int              nRegsBeg;
    int              nRegsEnd;
    int              nSatCalls;
    int              nSatCallsSat;
    int              nSatCallsUnsat;
    int              nSatProof;
    int              nSatFails;
    int              nSatFailsReal;
    int              nSpeculs;   
    int              nChoices;
    int              nChoicesFake;
    int              nSatCallsRecent;
    int              nSatCallsSkipped;
    // runtime
    int              timeSim;
    int              timeTrav;
    int              timeRwr;
    int              timeSat;
    int              timeSatUnsat;
    int              timeSatSat;
    int              timeSatFail;
    int              timeRef;
    int              timeTotal;
    int              time1;
    int              time2;
};

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

static inline unsigned *   Fra_ObjSim( Fra_Sml_t * p, int Id )                           { return p->pData + p->nWordsTotal * Id; }
static inline unsigned     Fra_ObjRandomSim()                                            { return Aig_ManRandom(0);               }

static inline Aig_Obj_t *  Fra_ObjFraig( Aig_Obj_t * pObj, int i )                       { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i];  }
static inline void         Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; }

static inline Vec_Ptr_t *  Fra_ObjFaninVec( Aig_Obj_t * pObj )                           { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];      }
static inline void         Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins )   { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins;   }

static inline int          Fra_ObjSatNum( Aig_Obj_t * pObj )                             { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];     }
static inline void         Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num )                 { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;      }

static inline Aig_Obj_t *  Fra_ClassObjRepr( Aig_Obj_t * pObj )                          { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id];  }
static inline void         Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode )    { ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id] = pNode; }

static inline Aig_Obj_t *  Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL;  }
static inline Aig_Obj_t *  Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL;  }

static inline int          Fra_ImpLeft( int Imp )                                        { return Imp & 0xFFFF;         }
static inline int          Fra_ImpRight( int Imp )                                       { return Imp >> 16;            }
static inline int          Fra_ImpCreate( int Left, int Right )                          { return (Right << 16) | Left; }

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

////////////////////////////////////////////////////////////////////////
///                    FUNCTION DECLARATIONS                         ///
////////////////////////////////////////////////////////////////////////

/*=== fraCec.c ========================================================*/
extern int                 Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
extern int                 Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
extern int                 Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
/*=== fraClass.c ========================================================*/
extern int                 Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
extern int                 Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern void                Fra_BmcStop( Fra_Bmc_t * p );
extern void                Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth );
extern void                Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose );
/*=== fraClass.c ========================================================*/
extern Fra_Cla_t *         Fra_ClassesStart( Aig_Man_t * pAig );
extern void                Fra_ClassesStop( Fra_Cla_t * p );
extern void                Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
extern void                Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
extern void                Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs );
extern int                 Fra_ClassesRefine( Fra_Cla_t * p );
extern int                 Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped );
extern int                 Fra_ClassesCountLits( Fra_Cla_t * p );
extern int                 Fra_ClassesCountPairs( Fra_Cla_t * p );
extern void                Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
extern void                Fra_ClassesLatchCorr( Fra_Man_t * p );
extern void                Fra_ClassesPostprocess( Fra_Cla_t * p );
extern void                Fra_ClassesSelectRepr( Fra_Cla_t * p );
extern Aig_Man_t *         Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK );
/*=== fraCnf.c ========================================================*/
extern void                Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
/*=== fraCore.c ========================================================*/
extern void                Fra_FraigSweep( Fra_Man_t * pManAig );
extern int                 Fra_FraigMiterStatus( Aig_Man_t * p );
extern int                 Fra_FraigMiterAssertedOutput( Aig_Man_t * p );
extern Aig_Man_t *         Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
extern Aig_Man_t *         Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
/*=== fraHot.c ========================================================*/
extern Vec_Int_t *         Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim );
extern void                Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern void                Fra_OneHotCheck( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern int                 Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern int                 Fra_OneHotCount( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern void                Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern Aig_Man_t *         Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern void                Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots );
/*=== fraImp.c ========================================================*/
extern Vec_Int_t *         Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
extern void                Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
extern int                 Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos );
extern int                 Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
extern void                Fra_ImpCompactArray( Vec_Int_t * vImps );
extern double              Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
extern int                 Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
extern void                Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
/*=== fraInd.c ========================================================*/
extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars );
/*=== fraIndVer.c =====================================================*/
extern int                 Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits );
/*=== fraLcr.c ========================================================*/
extern Aig_Man_t *         Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit );
/*=== fraMan.c ========================================================*/
extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
extern Fra_Man_t *         Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams );
extern void                Fra_ManClean( Fra_Man_t * p, int nNodesMax );
extern Aig_Man_t *         Fra_ManPrepareComb( Fra_Man_t * p );
extern void                Fra_ManFinalizeComb( Fra_Man_t * p );
extern void                Fra_ManStop( Fra_Man_t * p );
extern void                Fra_ManPrint( Fra_Man_t * p );
/*=== fraSat.c ========================================================*/
extern int                 Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
extern int                 Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
extern int                 Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
/*=== fraSec.c ========================================================*/
extern void                Fra_SecSetDefaultParams( Fra_Sec_t * p );
extern int                 Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult );
/*=== fraSim.c ========================================================*/
extern int                 Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
extern int                 Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
extern int                 Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern int                 Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right );
extern int                 Fra_SmlNodeCountOnes( Fra_Sml_t * p, Aig_Obj_t * pObj );
extern int                 Fra_SmlCheckOutput( Fra_Man_t * p );
extern void                Fra_SmlSavePattern( Fra_Man_t * p );
extern void                Fra_SmlSimulate( Fra_Man_t * p, int fInit );
extern void                Fra_SmlResimulate( Fra_Man_t * p );
extern Fra_Sml_t *         Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
extern void                Fra_SmlStop( Fra_Sml_t * p );
extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter );
extern Fra_Sml_t *         Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
extern Fra_Cex_t *         Fra_SmlGetCounterExample( Fra_Sml_t * p );
extern Fra_Cex_t *         Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
extern void                Fra_SmlFreeCounterExample( Fra_Cex_t * p );
extern Fra_Cex_t *         Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut );
extern int                 Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p );
extern int                 Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p );

#ifdef __cplusplus
}
#endif

#endif

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