1 /**CFile****************************************************************
2 
3   FileName    [pdr.h]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Property driven reachability.]
8 
9   Synopsis    [External declarations.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - November 20, 2010.]
16 
17   Revision    [$Id: pdr.h,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #ifndef ABC__sat__pdr__pdr_h
22 #define ABC__sat__pdr__pdr_h
23 
24 
25 ABC_NAMESPACE_HEADER_START
26 
27 
28 ////////////////////////////////////////////////////////////////////////
29 ///                          INCLUDES                                ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 ////////////////////////////////////////////////////////////////////////
33 ///                         PARAMETERS                               ///
34 ////////////////////////////////////////////////////////////////////////
35 
36 ////////////////////////////////////////////////////////////////////////
37 ///                         BASIC TYPES                              ///
38 ////////////////////////////////////////////////////////////////////////
39 
40 typedef struct Pdr_Par_t_ Pdr_Par_t;
41 struct Pdr_Par_t_
42 {
43 //    int iOutput;          // zero-based number of primary output to solve
44     int nRecycle;         // limit on vars for recycling
45     int nFrameMax;        // limit on frame count
46     int nConfLimit;       // limit on SAT solver conflicts
47     int nConfGenLimit;    // limit on SAT solver conflicts during generalization
48     int nRestLimit;       // limit on the number of proof-obligations
49     int nTimeOut;         // timeout in seconds
50     int nTimeOutGap;      // approximate timeout in seconds since the last change
51     int nTimeOutOne;      // approximate timeout in seconds per one output
52     int nRandomSeed;      // value to seed the SAT solver with
53     int fTwoRounds;       // use two rounds for generalization
54     int fMonoCnf;         // monolythic CNF
55     int fNewXSim;         // updated X-valued simulation
56     int fFlopPrio;        // use structural flop priorities
57     int fFlopOrder;       // order flops for 'analyze_final' during generalization
58     int fDumpInv;         // dump inductive invariant
59     int fUseSupp;         // use support in the invariant
60     int fShortest;        // forces bug traces to be shortest
61     int fShiftStart;      // allows clause pushing to start from an intermediate frame
62     int fReuseProofOblig; // reuses proof-obligationgs in the last timeframe
63     int fSimpleGeneral;   // simplified generalization
64     int fSkipGeneral;     // skips expensive generalization step
65     int fSkipDown;        // skips the application of down
66     int fCtgs;            // handle CTGs in down
67     int fUseAbs;          // use abstraction
68     int fUseSimpleRef;    // simplified CEX refinement
69     int fVerbose;         // verbose output`
70     int fVeryVerbose;     // very verbose output
71     int fNotVerbose;      // not printing line by line progress
72     int fSilent;          // totally silent execution
73     int fSolveAll;        // do not stop when found a SAT output
74     int fStoreCex;        // enable storing counter-examples in MO mode
75     int fUseBridge;       // use bridge interface
76     int fUsePropOut;      // use property output
77     int nFailOuts;        // the number of failed outputs
78     int nDropOuts;        // the number of timed out outputs
79     int nProveOuts;       // the number of proved outputs
80     int iFrame;           // explored up to this frame
81     int RunId;            // PDR id in this run
82     int(*pFuncStop)(int); // callback to terminate
83     int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
84     abctime timeLastSolved; // the time when the last output was solved
85     Vec_Int_t * vOutMap;  // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided)
86     char * pInvFileName;  // invariable file name
87 };
88 
89 ////////////////////////////////////////////////////////////////////////
90 ///                      MACRO DEFINITIONS                           ///
91 ////////////////////////////////////////////////////////////////////////
92 
93 ////////////////////////////////////////////////////////////////////////
94 ///                    FUNCTION DECLARATIONS                         ///
95 ////////////////////////////////////////////////////////////////////////
96 
97 /*=== pdrCore.c ==========================================================*/
98 extern void               Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
99 extern int                Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars );
100 
101 
102 ABC_NAMESPACE_HEADER_END
103 
104 
105 #endif
106 
107 ////////////////////////////////////////////////////////////////////////
108 ///                       END OF FILE                                ///
109 ////////////////////////////////////////////////////////////////////////
110 
111