summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr/pdrInt.h
blob: 0eb6bd816d4c57207741197cf0cd82ad4c201fa9 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
/**CFile****************************************************************

  FileName    [pdrInt.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Property driven reachability.]

  Synopsis    [Internal declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

***********************************************************************/
 
#ifndef ABC__sat__pdr__pdrInt_h
#define ABC__sat__pdr__pdrInt_h

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

#include "aig/saig/saig.h"
#include "misc/vec/vecWec.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
#include "pdr.h" 

ABC_NAMESPACE_HEADER_START

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////
             
////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Pdr_Set_t_ Pdr_Set_t;
struct Pdr_Set_t_
{
    word        Sign;      // signature
    int         nRefs;     // ref counter
    int         nTotal;    // total literals
    int         nLits;     // num flop literals
    int         Lits[0];
};

typedef struct Pdr_Obl_t_ Pdr_Obl_t;
struct Pdr_Obl_t_
{
    int         iFrame;    // time frame
    int         prio;      // priority
    int         nRefs;     // reference counter
    Pdr_Set_t * pState;    // state cube
    Pdr_Obl_t * pNext;     // next one
    Pdr_Obl_t * pLink;     // queue link
};

typedef struct Pdr_Man_t_ Pdr_Man_t;
struct Pdr_Man_t_
{
    // input problem
    Pdr_Par_t * pPars;     // parameters
    Aig_Man_t * pAig;      // user's AIG
    // static CNF representation
    Cnf_Man_t * pCnfMan;   // CNF manager
    Cnf_Dat_t * pCnf1;     // CNF for this AIG
    Vec_Int_t * vVar2Reg;  // mapping of SAT var into registers
    // dynamic CNF representation
    Cnf_Dat_t * pCnf2;     // CNF for this AIG
    Vec_Int_t * pvId2Vars; // for each used ObjId, maps frame into SAT var
    Vec_Ptr_t   vVar2Ids;  // for each used frame, maps SAT var into ObjId
    Vec_Wec_t * vVLits;    // CNF literals
    // data representation
    int         iOutCur;   // current output
    Vec_Ptr_t * vCexes;    // counter-examples for each output
    Vec_Ptr_t * vSolvers;  // SAT solvers
    Vec_Vec_t * vClauses;  // clauses by timeframe
    Pdr_Obl_t * pQueue;    // proof obligations
    int *       pOrder;    // ordering of the lits
    Vec_Int_t * vActVars;  // the counter of activation variables
    int         iUseFrame; // the first used frame
    // internal use
    Vec_Int_t * vPrio;     // priority flops
    Vec_Int_t * vLits;     // array of literals
    Vec_Int_t * vCiObjs;   // cone leaves
    Vec_Int_t * vCoObjs;   // cone roots
    Vec_Int_t * vCiVals;   // cone leaf values
    Vec_Int_t * vCoVals;   // cone root values
    Vec_Int_t * vNodes;    // cone nodes
    Vec_Int_t * vUndo;     // cone undos
    Vec_Int_t * vVisits;   // intermediate
    Vec_Int_t * vCi2Rem;   // CIs to be removed
    Vec_Int_t * vRes;      // final result
    Vec_Int_t * vSuppLits; // support literals
    Pdr_Set_t * pCubeJust; // justification
    abctime *   pTime4Outs;// timeout per output
    // statistics
    int         nBlocks;   // the number of times blockState was called
    int         nObligs;   // the number of proof obligations derived
    int         nCubes;    // the number of cubes derived
    int         nCalls;    // the number of SAT calls
    int         nCallsS;   // the number of SAT calls (sat)
    int         nCallsU;   // the number of SAT calls (unsat)
    int         nStarts;   // the number of SAT solver restarts
    int         nFrames;   // frames explored
    int         nCasesSS;
    int         nCasesSU;
    int         nCasesUS;
    int         nCasesUU;
    int         nQueCur;
    int         nQueMax;
    int         nQueLim;
    // runtime
    abctime     timeToStop;
    abctime     timeToStopOne;
    // time stats
    abctime     tSat;
    abctime     tSatSat;
    abctime     tSatUnsat;
    abctime     tGeneral;
    abctime     tPush;
    abctime     tTsim;
    abctime     tContain;
    abctime     tCnf;
    abctime     tTotal;
};

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

static inline sat_solver * Pdr_ManSolver( Pdr_Man_t * p, int k )  { return (sat_solver *)Vec_PtrEntry(p->vSolvers, k); }

static inline abctime      Pdr_ManTimeLimit( Pdr_Man_t * p )
{
    if ( p->timeToStop == 0 )
        return p->timeToStopOne;
    if ( p->timeToStopOne == 0 )
        return p->timeToStop;
    if ( p->timeToStop < p->timeToStopOne )
        return p->timeToStop;
    return p->timeToStopOne;
}

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

/*=== pdrCex.c ==========================================================*/
extern Abc_Cex_t *     Pdr_ManDeriveCex( Pdr_Man_t * p );
/*=== pdrCnf.c ==========================================================*/
extern int             Pdr_ObjSatVar( Pdr_Man_t * p, int k, int Pol, Aig_Obj_t * pObj );
extern int             Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar );
extern int             Pdr_ManFreeVar( Pdr_Man_t * p, int k );
extern sat_solver *    Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit );
/*=== pdrCore.c ==========================================================*/
extern int             Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet );
/*=== pdrInv.c ==========================================================*/
extern void            Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time );
extern void            Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart );
extern void            Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved );
extern void            Pdr_ManReportInvariant( Pdr_Man_t * p );
extern void            Pdr_ManVerifyInvariant( Pdr_Man_t * p );
/*=== pdrMan.c ==========================================================*/
extern Pdr_Man_t *     Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit );
extern void            Pdr_ManStop( Pdr_Man_t * p );
extern Abc_Cex_t *     Pdr_ManDeriveCex( Pdr_Man_t * p );
/*=== pdrSat.c ==========================================================*/
extern sat_solver *    Pdr_ManCreateSolver( Pdr_Man_t * p, int k );
extern sat_solver *    Pdr_ManFetchSolver( Pdr_Man_t * p, int k );
extern void            Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k );
extern Vec_Int_t *     Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext );
extern Vec_Int_t *     Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray );
extern void            Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
extern void            Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues );
extern int             Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
extern int             Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit );
/*=== pdrTsim.c ==========================================================*/
extern Pdr_Set_t *     Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
/*=== pdrUtil.c ==========================================================*/
extern Pdr_Set_t *     Pdr_SetAlloc( int nSize );
extern Pdr_Set_t *     Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits );
extern Pdr_Set_t *     Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove );
extern Pdr_Set_t *     Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits );
extern Pdr_Set_t *     Pdr_SetDup( Pdr_Set_t * pSet );
extern Pdr_Set_t *     Pdr_SetRef( Pdr_Set_t * p );
extern void            Pdr_SetDeref( Pdr_Set_t * p );
extern int             Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
extern int             Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
extern int             Pdr_SetIsInit( Pdr_Set_t * p, int iRemove );
extern void            Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
extern int             Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 );
extern Pdr_Obl_t *     Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext );
extern Pdr_Obl_t *     Pdr_OblRef( Pdr_Obl_t * p );
extern void            Pdr_OblDeref( Pdr_Obl_t * p );
extern int             Pdr_QueueIsEmpty( Pdr_Man_t * p );
extern Pdr_Obl_t *     Pdr_QueueHead( Pdr_Man_t * p );
extern Pdr_Obl_t *     Pdr_QueuePop( Pdr_Man_t * p );
extern void            Pdr_QueueClean( Pdr_Man_t * p );
extern void            Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl );
extern void            Pdr_QueuePrint( Pdr_Man_t * p );
extern void            Pdr_QueueStop( Pdr_Man_t * p );
extern int             Pdr_ManCubeJust( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );

ABC_NAMESPACE_HEADER_END


#endif

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