1 /**CFile****************************************************************
2
3 FileName [giaCSat2.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [Circuit-based SAT solver.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: giaCSat2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 typedef struct Tas_Par_t_ Tas_Par_t;
31 struct Tas_Par_t_
32 {
33 // conflict limits
34 int nBTLimit; // limit on the number of conflicts
35 // current parameters
36 int nBTThis; // number of conflicts
37 int nBTTotal; // total number of conflicts
38 // decision heuristics
39 int fUseHighest; // use node with the highest ID
40 // other parameters
41 int fVerbose;
42 };
43
44 typedef struct Tas_Sto_t_ Tas_Sto_t;
45 struct Tas_Sto_t_
46 {
47 int iCur; // currently used
48 int nSize; // allocated size
49 char * pBuffer; // handles of objects stored in the queue
50 };
51
52 typedef struct Tas_Que_t_ Tas_Que_t;
53 struct Tas_Que_t_
54 {
55 int iHead; // beginning of the queue
56 int iTail; // end of the queue
57 int nSize; // allocated size
58 int * pData; // handles of objects stored in the queue
59 };
60
61 typedef struct Tas_Var_t_ Tas_Var_t;
62 struct Tas_Var_t_
63 {
64 unsigned fTerm : 1; // terminal node
65 unsigned fVal : 1; // current value
66 unsigned fValOld : 1; // previous value
67 unsigned fAssign : 1; // assigned status
68 unsigned fJQueue : 1; // part of J-frontier
69 unsigned fCompl0 : 1; // complemented attribute
70 unsigned fCompl1 : 1; // complemented attribute
71 unsigned fMark0 : 1; // multi-purpose mark
72 unsigned fMark1 : 1; // multi-purpose mark
73 unsigned fPhase : 1; // polarity
74 unsigned Level : 22; // decision level
75 int Id; // unique ID of this variable
76 int IdAig; // original ID of this variable
77 int Reason0; // reason of this variable
78 int Reason1; // reason of this variable
79 int Diff0; // difference for the first fanin
80 int Diff1; // difference for the second fanin
81 int Watch0; // handle of first watch
82 int Watch1; // handle of second watch
83 };
84
85 typedef struct Tas_Cls_t_ Tas_Cls_t;
86 struct Tas_Cls_t_
87 {
88 int Watch0; // next clause to watch
89 int Watch1; // next clause to watch
90 int pVars[0]; // variable handles
91 };
92
93 typedef struct Tas_Man_t_ Tas_Man_t;
94 struct Tas_Man_t_
95 {
96 // user data
97 Gia_Man_t * pAig; // AIG manager
98 Tas_Par_t Pars; // parameters
99 // solver data
100 Tas_Sto_t * pVars; // variables
101 Tas_Sto_t * pClauses; // clauses
102 // state representation
103 Tas_Que_t pProp; // propagation queue
104 Tas_Que_t pJust; // justification queue
105 Vec_Int_t * vModel; // satisfying assignment
106 Vec_Ptr_t * vTemp; // temporary storage
107 // SAT calls statistics
108 int nSatUnsat; // the number of proofs
109 int nSatSat; // the number of failure
110 int nSatUndec; // the number of timeouts
111 int nSatTotal; // the number of calls
112 // conflicts
113 int nConfUnsat; // conflicts in unsat problems
114 int nConfSat; // conflicts in sat problems
115 int nConfUndec; // conflicts in undec problems
116 int nConfTotal; // total conflicts
117 // runtime stats
118 clock_t timeSatUnsat; // unsat
119 clock_t timeSatSat; // sat
120 clock_t timeSatUndec; // undecided
121 clock_t timeTotal; // total runtime
122 };
123
Tas_VarIsAssigned(Tas_Var_t * pVar)124 static inline int Tas_VarIsAssigned( Tas_Var_t * pVar ) { return pVar->fAssign; }
Tas_VarAssign(Tas_Var_t * pVar)125 static inline void Tas_VarAssign( Tas_Var_t * pVar ) { assert(!pVar->fAssign); pVar->fAssign = 1; }
Tas_VarUnassign(Tas_Var_t * pVar)126 static inline void Tas_VarUnassign( Tas_Var_t * pVar ) { assert(pVar->fAssign); pVar->fAssign = 0; pVar->fVal = 0; }
Tas_VarValue(Tas_Var_t * pVar)127 static inline int Tas_VarValue( Tas_Var_t * pVar ) { assert(pVar->fAssign); return pVar->fVal; }
Tas_VarSetValue(Tas_Var_t * pVar,int v)128 static inline void Tas_VarSetValue( Tas_Var_t * pVar, int v ) { assert(pVar->fAssign); pVar->fVal = v; }
Tas_VarIsJust(Tas_Var_t * pVar)129 static inline int Tas_VarIsJust( Tas_Var_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)); }
Tas_VarFanin0Value(Tas_Var_t * pVar)130 static inline int Tas_VarFanin0Value( Tas_Var_t * pVar ) { return !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
Tas_VarFanin1Value(Tas_Var_t * pVar)131 static inline int Tas_VarFanin1Value( Tas_Var_t * pVar ) { return !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
132
Tas_VarDecLevel(Tas_Man_t * p,Tas_Var_t * pVar)133 static inline int Tas_VarDecLevel( Tas_Man_t * p, Tas_Var_t * pVar ) { assert( pVar->Value != ~0 ); return Vec_IntEntry(p->vLevReas, 3*pVar->Value); }
Tas_VarReason0(Tas_Man_t * p,Tas_Var_t * pVar)134 static inline Tas_Var_t * Tas_VarReason0( Tas_Man_t * p, Tas_Var_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+1); }
Tas_VarReason1(Tas_Man_t * p,Tas_Var_t * pVar)135 static inline Tas_Var_t * Tas_VarReason1( Tas_Man_t * p, Tas_Var_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+2); }
Tas_ClauseDecLevel(Tas_Man_t * p,int hClause)136 static inline int Tas_ClauseDecLevel( Tas_Man_t * p, int hClause ) { return Tas_VarDecLevel( p, p->pClauses.pData[hClause] ); }
137
Tas_ManVar(Tas_Man_t * p,int h)138 static inline Tas_Var_t * Tas_ManVar( Tas_Man_t * p, int h ) { return (Tas_Var_t *)(p->pVars->pBuffer + h); }
Tas_ManClause(Tas_Man_t * p,int h)139 static inline Tas_Cls_t * Tas_ManClause( Tas_Man_t * p, int h ) { return (Tas_Cls_t *)(p->pClauses->pBuffer + h); }
140
141 #define Tas_ClaForEachVar( p, pClause, pVar, i ) \
142 for ( pVar = Tas_ManVar(p, pClause->pVars[(i=0)]); pClause->pVars[i]; pVar = (Tas_Var_t *)(((char *)pVar + pClause->pVars[++i])) )
143
144 #define Tas_QueForEachVar( p, pQue, pVar, i ) \
145 for ( pVar = Tas_ManVar(p, pQue->pVars[(i=pQue->iHead)]); i < pQue->iTail; pVar = Tas_ManVar(p, pQue->pVars[i++]) )
146
147
148 ////////////////////////////////////////////////////////////////////////
149 /// FUNCTION DEFINITIONS ///
150 ////////////////////////////////////////////////////////////////////////
151
152 /**Function*************************************************************
153
154 Synopsis []
155
156 Description []
157
158 SideEffects []
159
160 SeeAlso []
161
162 ***********************************************************************/
Tas_ManCreateVar(Tas_Man_t * p)163 Tas_Var_t * Tas_ManCreateVar( Tas_Man_t * p )
164 {
165 Tas_Var_t * pVar;
166 if ( p->pVars->iCur + sizeof(Tas_Var_t) > p->pVars->nSize )
167 {
168 p->pVars->nSize *= 2;
169 p->pVars->pData = ABC_REALLOC( char, p->pVars->pData, p->pVars->nSize );
170 }
171 pVar = p->pVars->pData + p->pVars->iCur;
172 p->pVars->iCur += sizeof(Tas_Var_t);
173 memset( pVar, 0, sizeof(Tas_Var_t) );
174 pVar->Id = pVar - ((Tas_Var_t *)p->pVars->pData);
175 return pVar;
176 }
177
178 /**Function*************************************************************
179
180 Synopsis []
181
182 Description []
183
184 SideEffects []
185
186 SeeAlso []
187
188 ***********************************************************************/
Tas_ManObj2Var(Tas_Man_t * p,Gia_Obj_t * pObj)189 Tas_Var_t * Tas_ManObj2Var( Tas_Man_t * p, Gia_Obj_t * pObj )
190 {
191 Tas_Var_t * pVar;
192 assert( !Gia_ObjIsComplement(pObj) );
193 if ( pObj->Value == 0 )
194 {
195 pVar = Tas_ManCreateVar( p );
196 pVar->
197
198 }
199 return Tas_ManVar( p, pObj->Value );
200 }
201
202 ////////////////////////////////////////////////////////////////////////
203 /// END OF FILE ///
204 ////////////////////////////////////////////////////////////////////////
205
206
207 ABC_NAMESPACE_IMPL_END
208
209