1 /**CFile**************************************************************** 2 3 FileName [int.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 - June 24, 2008.] 16 17 Revision [$Id: int.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] 18 19 ***********************************************************************/ 20 21 #ifndef ABC__aig__int__int_h 22 #define ABC__aig__int__int_h 23 24 25 /* 26 The interpolation algorithm implemented here was introduced in the paper: 27 K. L. McMillan. Interpolation and SAT-based model checking. CAV�03, pp. 1-13. 28 */ 29 30 //////////////////////////////////////////////////////////////////////// 31 /// INCLUDES /// 32 //////////////////////////////////////////////////////////////////////// 33 34 //////////////////////////////////////////////////////////////////////// 35 /// PARAMETERS /// 36 //////////////////////////////////////////////////////////////////////// 37 38 39 40 ABC_NAMESPACE_HEADER_START 41 42 43 //////////////////////////////////////////////////////////////////////// 44 /// BASIC TYPES /// 45 //////////////////////////////////////////////////////////////////////// 46 47 // simulation manager 48 typedef struct Inter_ManParams_t_ Inter_ManParams_t; 49 struct Inter_ManParams_t_ 50 { 51 int nBTLimit; // limit on the number of conflicts 52 int nFramesMax; // the max number timeframes to unroll 53 int nSecLimit; // time limit in seconds 54 int nFramesK; // the number of timeframes to use in induction 55 int fRewrite; // use additional rewriting to simplify timeframes 56 int fTransLoop; // add transition into the init state under new PI var 57 int fUsePudlak; // use Pudluk interpolation procedure 58 int fUseOther; // use other undisclosed option 59 int fUseMiniSat; // use MiniSat-1.14p instead of internal proof engine 60 int fCheckKstep; // check using K-step induction 61 int fUseBias; // bias decisions to global variables 62 int fUseBackward; // perform backward interpolation 63 int fUseSeparate; // solve each output separately 64 int fUseTwoFrames; // create the OR of two last timeframes 65 int fDropSatOuts; // replace by 1 the solved outputs 66 int fDropInvar; // dump inductive invariant into file 67 int fVerbose; // print verbose statistics 68 int iFrameMax; // the time frame reached 69 char * pFileName; // file name to dump interpolant 70 }; 71 72 //////////////////////////////////////////////////////////////////////// 73 /// MACRO DEFINITIONS /// 74 //////////////////////////////////////////////////////////////////////// 75 76 //////////////////////////////////////////////////////////////////////// 77 /// FUNCTION DECLARATIONS /// 78 //////////////////////////////////////////////////////////////////////// 79 80 /*=== intCore.c ==========================================================*/ 81 extern void Inter_ManSetDefaultParams( Inter_ManParams_t * p ); 82 extern int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * piFrame ); 83 84 85 86 87 ABC_NAMESPACE_HEADER_END 88 89 90 91 #endif 92 93 //////////////////////////////////////////////////////////////////////// 94 /// END OF FILE /// 95 //////////////////////////////////////////////////////////////////////// 96 97