1 /**CFile****************************************************************
2 
3   FileName    [int2.h]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Interpolation engine.]
8 
9   Synopsis    [External declarations.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - Dec 1, 2013.]
16 
17   Revision    [$Id: int2.h,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #ifndef ABC__aig__int2__int_h
22 #define ABC__aig__int2__int_h
23 
24 
25 /*
26     The interpolation algorithm implemented here was introduced in the papers:
27     K. L. McMillan. Interpolation and SAT-based model checking. CAV�03, pp. 1-13.
28     C.-Y. Wu et al. A CEX-Guided Interpolant Generation Algorithm for
29     SAT-based Model Checking. DAC'13.
30 */
31 
32 ////////////////////////////////////////////////////////////////////////
33 ///                          INCLUDES                                ///
34 ////////////////////////////////////////////////////////////////////////
35 
36 ////////////////////////////////////////////////////////////////////////
37 ///                         PARAMETERS                               ///
38 ////////////////////////////////////////////////////////////////////////
39 
40 
41 
42 ABC_NAMESPACE_HEADER_START
43 
44 
45 ////////////////////////////////////////////////////////////////////////
46 ///                         BASIC TYPES                              ///
47 ////////////////////////////////////////////////////////////////////////
48 
49 // simulation manager
50 typedef struct Int2_ManPars_t_ Int2_ManPars_t;
51 struct Int2_ManPars_t_
52 {
53     int     nBTLimit;       // limit on the number of conflicts
54     int     nFramesS;       // the starting number timeframes
55     int     nFramesMax;     // the max number timeframes to unroll
56     int     nSecLimit;      // time limit in seconds
57     int     nFramesK;       // the number of timeframes to use in induction
58     int     fRewrite;       // use additional rewriting to simplify timeframes
59     int     fTransLoop;     // add transition into the init state under new PI var
60     int     fDropInvar;     // dump inductive invariant into file
61     int     fVerbose;       // print verbose statistics
62     int     iFrameMax;      // the time frame reached
63     char *  pFileName;      // file name to dump interpolant
64 };
65 
66 ////////////////////////////////////////////////////////////////////////
67 ///                      MACRO DEFINITIONS                           ///
68 ////////////////////////////////////////////////////////////////////////
69 
70 ////////////////////////////////////////////////////////////////////////
71 ///                    FUNCTION DECLARATIONS                         ///
72 ////////////////////////////////////////////////////////////////////////
73 
74 /*=== intCore.c ==========================================================*/
75 extern void       Int2_ManSetDefaultParams( Int2_ManPars_t * p );
76 extern int        Int2_ManPerformInterpolation( Gia_Man_t * p, Int2_ManPars_t * pPars );
77 
78 
79 
80 
81 ABC_NAMESPACE_HEADER_END
82 
83 
84 
85 #endif
86 
87 ////////////////////////////////////////////////////////////////////////
88 ///                       END OF FILE                                ///
89 ////////////////////////////////////////////////////////////////////////
90 
91