pdr.h 4.12 KB
Newer Older
1 2 3 4 5 6
/**CFile****************************************************************

  FileName    [pdr.h]

  SystemName  [ABC: Logic synthesis and verification system.]

7
  PackageName [Property driven reachability.]
8 9 10 11 12 13 14 15 16 17 18 19 20

  Synopsis    [External declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - November 20, 2010.]

  Revision    [$Id: pdr.h,v 1.00 2010/11/20 00:00:00 alanmi Exp $]

***********************************************************************/
 
21 22
#ifndef ABC__sat__pdr__pdr_h
#define ABC__sat__pdr__pdr_h
23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42


ABC_NAMESPACE_HEADER_START


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

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

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

typedef struct Pdr_Par_t_ Pdr_Par_t;
struct Pdr_Par_t_
{
43
//    int iOutput;          // zero-based number of primary output to solve
44 45 46 47 48
    int nRecycle;         // limit on vars for recycling
    int nFrameMax;        // limit on frame count
    int nConfLimit;       // limit on SAT solver conflicts
    int nRestLimit;       // limit on the number of proof-obligations
    int nTimeOut;         // timeout in seconds
49
    int nTimeOutGap;      // approximate timeout in seconds since the last change
50
    int nTimeOutOne;      // approximate timeout in seconds per one output
51 52 53 54
    int fTwoRounds;       // use two rounds for generalization
    int fMonoCnf;         // monolythic CNF
    int fDumpInv;         // dump inductive invariant
    int fShortest;        // forces bug traces to be shortest
55
    int fShiftStart;      // allows clause pushing to start from an intermediate frame
56
    int fReuseProofOblig; // reuses proof-obligationgs in the last timeframe
57 58 59
    int fSkipGeneral;     // skips expensive generalization step
    int fVerbose;         // verbose output`
    int fVeryVerbose;     // very verbose output
60
    int fNotVerbose;      // not printing line by line progress
61
    int fSilent;          // totally silent execution
62
    int fSolveAll;        // do not stop when found a SAT output
63
    int fStoreCex;        // enable storing counter-examples in MO mode
64
    int fUseBridge;       // use bridge interface
65
    int nFailOuts;        // the number of failed outputs
66 67
    int nDropOuts;        // the number of timed out outputs
    int nProveOuts;       // the number of proved outputs
68 69 70
    int iFrame;           // explored up to this frame
    int RunId;            // PDR id in this run 
    int(*pFuncStop)(int); // callback to terminate
71
    int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
72
    abctime timeLastSolved; // the time when the last output was solved
73
    Vec_Int_t * vOutMap;  // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided)
74 75 76 77 78 79 80 81 82 83 84
};

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

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

/*=== pdrCore.c ==========================================================*/
85
extern void               Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
86
extern int                Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars );
87 88 89 90 91 92 93 94 95 96 97


ABC_NAMESPACE_HEADER_END


#endif

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