blob: 4182cd14467cf0f6ac1942bdbf9fa544b3749a36 (
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
|
#ifndef ABC__aig__gia__giaCSatP_h
#define ABC__aig__gia__giaCSatP_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "gia.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
typedef struct CbsP_Par_t_ CbsP_Par_t;
struct CbsP_Par_t_
{
// conflict limits
int nBTLimit; // limit on the number of conflicts
int nJustLimit; // limit on the size of justification queue
// current parameters
int nBTThis; // number of conflicts
int nBTThisNc; // number of conflicts
int nJustThis; // max size of the frontier
int nBTTotal; // total number of conflicts
int nJustTotal; // total size of the frontier
// decision heuristics
int fUseHighest; // use node with the highest ID
int fUseLowest; // use node with the highest ID
int fUseMaxFF; // use node with the largest fanin fanout
// other
int fVerbose;
int fUseProved;
// statistics
int nJscanThis;
int nRscanThis;
int nPropThis;
int maxJscanUndec;
int maxRscanUndec;
int maxPropUndec;
int maxJscanSolved;
int maxRscanSolved;
int maxPropSolved;
int nSat, nUnsat, nUndec;
long accJscanSat;
long accJscanUnsat;
long accJscanUndec;
long accRscanSat;
long accRscanUnsat;
long accRscanUndec;
long accPropSat;
long accPropUnsat;
long accPropUndec;
// other limits
int nJscanLimit;
int nRscanLimit;
int nPropLimit;
};
typedef struct CbsP_Que_t_ CbsP_Que_t;
struct CbsP_Que_t_
{
int iHead; // beginning of the queue
int iTail; // end of the queue
int nSize; // allocated size
Gia_Obj_t ** pData; // nodes stored in the queue
};
typedef struct CbsP_Man_t_ CbsP_Man_t;
struct CbsP_Man_t_
{
CbsP_Par_t Pars; // parameters
Gia_Man_t * pAig; // AIG manager
CbsP_Que_t pProp; // propagation queue
CbsP_Que_t pJust; // justification queue
CbsP_Que_t pClauses; // clause queue
Gia_Obj_t ** pIter; // iterator through clause vars
Vec_Int_t * vLevReas; // levels and decisions
Vec_Int_t * vValue;
Vec_Int_t * vModel; // satisfying assignment
Vec_Ptr_t * vTemp; // temporary storage
// SAT calls statistics
int nSatUnsat; // the number of proofs
int nSatSat; // the number of failure
int nSatUndec; // the number of timeouts
int nSatTotal; // the number of calls
// conflicts
int nConfUnsat; // conflicts in unsat problems
int nConfSat; // conflicts in sat problems
int nConfUndec; // conflicts in undec problems
// runtime stats
abctime timeSatUnsat; // unsat
abctime timeSatSat; // sat
abctime timeSatUndec; // undecided
abctime timeTotal; // total runtime
};
CbsP_Man_t * CbsP_ManAlloc( Gia_Man_t * pGia );
void CbsP_ManStop( CbsP_Man_t * p );
void CbsP_ManSatPrintStats( CbsP_Man_t * p );
void CbsP_PrintRecord( CbsP_Par_t * pPars );
int CbsP_ManSolve2( CbsP_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
#define CBS_UNSAT 1
#define CBS_SAT 0
#define CBS_UNDEC -1
ABC_NAMESPACE_HEADER_END
#endif
|
