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