1 /**CFile****************************************************************
2 
3   FileName    [ssc.h]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [SAT sweeping under constraints.]
8 
9   Synopsis    [External declarations.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 29, 2008.]
16 
17   Revision    [$Id: ssc.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #ifndef ABC__aig__ssc__ssc_h
22 #define ABC__aig__ssc__ssc_h
23 
24 
25 ////////////////////////////////////////////////////////////////////////
26 ///                          INCLUDES                                ///
27 ////////////////////////////////////////////////////////////////////////
28 
29 ////////////////////////////////////////////////////////////////////////
30 ///                         PARAMETERS                               ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 
34 
35 ABC_NAMESPACE_HEADER_START
36 
37 
38 ////////////////////////////////////////////////////////////////////////
39 ///                         BASIC TYPES                              ///
40 ////////////////////////////////////////////////////////////////////////
41 
42 // choicing parameters
43 typedef struct Ssc_Pars_t_ Ssc_Pars_t;
44 struct Ssc_Pars_t_
45 {
46     int              nWords;        // the number of simulation words
47     int              nBTLimit;      // conflict limit at a node
48     int              nSatVarMax;    // the max number of SAT variables
49     int              nCallsRecycle; // calls to perform before recycling SAT solver
50     int              fAppend;       // append constraints to the resulting AIG
51     int              fVerbose;      // verbose stats
52     int              fVerify;       // enable internal verification
53 };
54 
55 ////////////////////////////////////////////////////////////////////////
56 ///                      MACRO DEFINITIONS                           ///
57 ////////////////////////////////////////////////////////////////////////
58 
59 ////////////////////////////////////////////////////////////////////////
60 ///                    FUNCTION DECLARATIONS                         ///
61 ////////////////////////////////////////////////////////////////////////
62 
63 /*=== sscCore.c ==========================================================*/
64 extern void          Ssc_ManSetDefaultParams( Ssc_Pars_t * p );
65 extern Gia_Man_t *   Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars );
66 extern Gia_Man_t *   Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars );
67 
68 
69 ABC_NAMESPACE_HEADER_END
70 
71 
72 
73 #endif
74 
75 ////////////////////////////////////////////////////////////////////////
76 ///                       END OF FILE                                ///
77 ////////////////////////////////////////////////////////////////////////
78 
79