abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
sscSat.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [sscSat.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [SAT sweeping under constraints.]
8 
9  Synopsis [SAT procedures.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 29, 2008.]
16 
17  Revision [$Id: sscSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "sscInt.h"
22 #include "sat/cnf/cnf.h"
23 #include "aig/gia/giaAig.h"
24 
26 
27 
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 static inline int Ssc_ObjSatLit( Ssc_Man_t * p, int Lit ) { return Abc_Var2Lit( Ssc_ObjSatVar(p, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit) ); }
33 
34 ////////////////////////////////////////////////////////////////////////
35 /// FUNCTION DEFINITIONS ///
36 ////////////////////////////////////////////////////////////////////////
37 
38 /**Function*************************************************************
39 
40  Synopsis [Addes clauses to the solver.]
41 
42  Description []
43 
44  SideEffects []
45 
46  SeeAlso []
47 
48 ***********************************************************************/
49 static void Gia_ManAddClausesMux( Ssc_Man_t * p, Gia_Obj_t * pNode )
50 {
51  Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
52  int pLits[4], LitF, LitI, LitT, LitE, RetValue;
53  assert( !Gia_IsComplement( pNode ) );
54  assert( Gia_ObjIsMuxType( pNode ) );
55  // get nodes (I = if, T = then, E = else)
56  pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
57  // get the Litiable numbers
58  LitF = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNode) );
59  LitI = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNodeI) );
60  LitT = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNodeT) );
61  LitE = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNodeE) );
62 
63  // f = ITE(i, t, e)
64 
65  // i' + t' + f
66  // i' + t + f'
67  // i + e' + f
68  // i + e + f'
69 
70  // create four clauses
71  pLits[0] = Abc_LitNotCond(LitI, 1);
72  pLits[1] = Abc_LitNotCond(LitT, 1);
73  pLits[2] = Abc_LitNotCond(LitF, 0);
74  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
75  assert( RetValue );
76  pLits[0] = Abc_LitNotCond(LitI, 1);
77  pLits[1] = Abc_LitNotCond(LitT, 0);
78  pLits[2] = Abc_LitNotCond(LitF, 1);
79  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
80  assert( RetValue );
81  pLits[0] = Abc_LitNotCond(LitI, 0);
82  pLits[1] = Abc_LitNotCond(LitE, 1);
83  pLits[2] = Abc_LitNotCond(LitF, 0);
84  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
85  assert( RetValue );
86  pLits[0] = Abc_LitNotCond(LitI, 0);
87  pLits[1] = Abc_LitNotCond(LitE, 0);
88  pLits[2] = Abc_LitNotCond(LitF, 1);
89  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
90  assert( RetValue );
91 
92  // two additional clauses
93  // t' & e' -> f'
94  // t & e -> f
95 
96  // t + e + f'
97  // t' + e' + f
98 
99  if ( LitT == LitE )
100  {
101 // assert( fCompT == !fCompE );
102  return;
103  }
104 
105  pLits[0] = Abc_LitNotCond(LitT, 0);
106  pLits[1] = Abc_LitNotCond(LitE, 0);
107  pLits[2] = Abc_LitNotCond(LitF, 1);
108  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
109  assert( RetValue );
110  pLits[0] = Abc_LitNotCond(LitT, 1);
111  pLits[1] = Abc_LitNotCond(LitE, 1);
112  pLits[2] = Abc_LitNotCond(LitF, 0);
113  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
114  assert( RetValue );
115 }
116 
117 /**Function*************************************************************
118 
119  Synopsis [Addes clauses to the solver.]
120 
121  Description []
122 
123  SideEffects []
124 
125  SeeAlso []
126 
127 ***********************************************************************/
128 static void Gia_ManAddClausesSuper( Ssc_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSuper )
129 {
130  int i, RetValue, Lit, LitNode, pLits[2];
131  assert( !Gia_IsComplement(pNode) );
132  assert( Gia_ObjIsAnd( pNode ) );
133  // suppose AND-gate is A & B = C
134  // add !A => !C or A + !C
135  // add !B => !C or B + !C
136  LitNode = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNode) );
137  Vec_IntForEachEntry( vSuper, Lit, i )
138  {
139  pLits[0] = Ssc_ObjSatLit( p, Lit );
140  pLits[1] = Abc_LitNot( LitNode );
141  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
142  assert( RetValue );
143  // update literals
144  Vec_IntWriteEntry( vSuper, i, Abc_LitNot(pLits[0]) );
145  }
146  // add A & B => C or !A + !B + C
147  Vec_IntPush( vSuper, LitNode );
148  RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vSuper), Vec_IntArray(vSuper) + Vec_IntSize(vSuper) );
149  assert( RetValue );
150  (void) RetValue;
151 }
152 
153 
154 /**Function*************************************************************
155 
156  Synopsis [Collects the supergate.]
157 
158  Description []
159 
160  SideEffects []
161 
162  SeeAlso []
163 
164 ***********************************************************************/
165 static void Ssc_ManCollectSuper_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
166 {
167  // stop at complements, PIs, and MUXes
168  if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) || Gia_ObjIsMuxType(pObj) )
169  {
170  Vec_IntPushUnique( vSuper, Gia_Obj2Lit(p, pObj) );
171  return;
172  }
173  Ssc_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper );
174  Ssc_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper );
175 }
176 static void Ssc_ManCollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
177 {
178  assert( !Gia_IsComplement(pObj) );
179  assert( Gia_ObjIsAnd(pObj) );
180  Vec_IntClear( vSuper );
181  Ssc_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper );
182  Ssc_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper );
183 }
184 
185 /**Function*************************************************************
186 
187  Synopsis [Updates the solver clause database.]
188 
189  Description []
190 
191  SideEffects []
192 
193  SeeAlso []
194 
195 ***********************************************************************/
196 static void Ssc_ManCnfAddToFrontier( Ssc_Man_t * p, int Id, Vec_Int_t * vFront )
197 {
198  Gia_Obj_t * pObj;
199  assert( Id > 0 );
200  if ( Ssc_ObjSatVar(p, Id) )
201  return;
202  pObj = Gia_ManObj( p->pFraig, Id );
203  Ssc_ObjSetSatVar( p, Id, p->nSatVars++ );
204  sat_solver_setnvars( p->pSat, p->nSatVars + 100 );
205  if ( Gia_ObjIsAnd(pObj) )
206  Vec_IntPush( vFront, Id );
207 }
208 static void Ssc_ManCnfNodeAddToSolver( Ssc_Man_t * p, int NodeId )
209 {
210  Gia_Obj_t * pNode;
211  int i, k, Id, Lit;
212  abctime clk;
213  assert( NodeId > 0 );
214  // quit if CNF is ready
215  if ( Ssc_ObjSatVar(p, NodeId) )
216  return;
217 clk = Abc_Clock();
218  // start the frontier
219  Vec_IntClear( p->vFront );
220  Ssc_ManCnfAddToFrontier( p, NodeId, p->vFront );
221  // explore nodes in the frontier
222  Gia_ManForEachObjVec( p->vFront, p->pFraig, pNode, i )
223  {
224  // create the supergate
225  assert( Ssc_ObjSatVar(p, Gia_ObjId(p->pFraig, pNode)) );
226  if ( Gia_ObjIsMuxType(pNode) )
227  {
228  Vec_IntClear( p->vFanins );
229  Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pFraig, Gia_ObjFanin0(pNode) ) );
230  Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pFraig, Gia_ObjFanin1(pNode) ) );
231  Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pFraig, Gia_ObjFanin0(pNode) ) );
232  Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pFraig, Gia_ObjFanin1(pNode) ) );
233  Vec_IntForEachEntry( p->vFanins, Id, k )
234  Ssc_ManCnfAddToFrontier( p, Id, p->vFront );
235  Gia_ManAddClausesMux( p, pNode );
236  }
237  else
238  {
239  Ssc_ManCollectSuper( p->pFraig, pNode, p->vFanins );
240  Vec_IntForEachEntry( p->vFanins, Lit, k )
241  Ssc_ManCnfAddToFrontier( p, Abc_Lit2Var(Lit), p->vFront );
242  Gia_ManAddClausesSuper( p, pNode, p->vFanins );
243  }
244  assert( Vec_IntSize(p->vFanins) > 1 );
245  }
246 p->timeCnfGen += Abc_Clock() - clk;
247 }
248 
249 
250 /**Function*************************************************************
251 
252  Synopsis [Starts the SAT solver for constraints.]
253 
254  Description []
255 
256  SideEffects []
257 
258  SeeAlso []
259 
260 ***********************************************************************/
262 {
263  Aig_Man_t * pMan = Gia_ManToAigSimple( p->pFraig );
264  Cnf_Dat_t * pDat = Cnf_Derive( pMan, 0 );
265  Gia_Obj_t * pObj;
266  sat_solver * pSat;
267  int i, status;
268  assert( p->pSat == NULL && p->vId2Var == NULL );
269  assert( Aig_ManObjNumMax(pMan) == Gia_ManObjNum(p->pFraig) );
270  Aig_ManStop( pMan );
271  // save variable mapping
272  p->nSatVarsPivot = p->nSatVars = pDat->nVars;
273  p->vId2Var = Vec_IntStart( Gia_ManCandNum(p->pAig) + Gia_ManCandNum(p->pCare) + 10 ); // mapping of each node into its SAT var
274  p->vVar2Id = Vec_IntStart( Gia_ManCandNum(p->pAig) + Gia_ManCandNum(p->pCare) + 10 ); // mapping of each SAT var into its node
275  Ssc_ObjSetSatVar( p, 0, pDat->pVarNums[0] );
276  Gia_ManForEachCi( p->pFraig, pObj, i )
277  {
278  int iObj = Gia_ObjId( p->pFraig, pObj );
279  Ssc_ObjSetSatVar( p, iObj, pDat->pVarNums[iObj] );
280  }
281 //Cnf_DataWriteIntoFile( pDat, "dump.cnf", 1, NULL, NULL );
282  // start the SAT solver
283  pSat = sat_solver_new();
284  sat_solver_setnvars( pSat, pDat->nVars + 1000 );
285  for ( i = 0; i < pDat->nClauses; i++ )
286  {
287  if ( !sat_solver_addclause( pSat, pDat->pClauses[i], pDat->pClauses[i+1] ) )
288  {
289  Cnf_DataFree( pDat );
290  sat_solver_delete( pSat );
291  return;
292  }
293  }
294  Cnf_DataFree( pDat );
295  status = sat_solver_simplify( pSat );
296  if ( status == 0 )
297  {
298  sat_solver_delete( pSat );
299  return;
300  }
301  p->pSat = pSat;
302 }
303 
304 /**Function*************************************************************
305 
306  Synopsis []
307 
308  Description []
309 
310  SideEffects []
311 
312  SeeAlso []
313 
314 ***********************************************************************/
316 {
317  Gia_Obj_t * pObj;
318  int i;
319  Vec_IntClear( vPattern );
320  Gia_ManForEachCi( p->pFraig, pObj, i )
321  Vec_IntPush( vPattern, sat_solver_var_value(p->pSat, Ssc_ObjSatVar(p, Gia_ObjId(p->pFraig, pObj))) );
322 }
324 {
325  Vec_Int_t * vInit;
326  int status = sat_solver_solve( p->pSat, NULL, NULL, p->pPars->nBTLimit, 0, 0, 0 );
327  if ( status == l_False )
328  return (Vec_Int_t *)(ABC_PTRINT_T)1;
329  if ( status == l_Undef )
330  return NULL;
331  assert( status == l_True );
332  vInit = Vec_IntAlloc( Gia_ManCiNum(p->pFraig) );
333  Ssc_ManCollectSatPattern( p, vInit );
334  return vInit;
335 }
336 
337 /**Function*************************************************************
338 
339  Synopsis []
340 
341  Description []
342 
343  SideEffects []
344 
345  SeeAlso []
346 
347 ***********************************************************************/
348 int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
349 {
350  int pLitsSat[2], RetValue;
351  abctime clk;
352  assert( iRepr != iNode );
353  if ( iRepr > iNode )
354  return l_Undef;
355  assert( iRepr < iNode );
356 // if ( p->nTimeOut )
357 // sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
358 
359  // create CNF
360  if ( iRepr )
361  Ssc_ManCnfNodeAddToSolver( p, iRepr );
362  Ssc_ManCnfNodeAddToSolver( p, iNode );
363  sat_solver_compress( p->pSat );
364 
365  // order the literals
366  pLitsSat[0] = Abc_Var2Lit( Ssc_ObjSatVar(p, iRepr), 0 );
367  pLitsSat[1] = Abc_Var2Lit( Ssc_ObjSatVar(p, iNode), fCompl ^ (int)(iRepr > 0) );
368 
369  // solve under assumptions
370  // A = 1; B = 0
371  clk = Abc_Clock();
372  RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
373  if ( RetValue == l_False )
374  {
375  pLitsSat[0] = Abc_LitNot( pLitsSat[0] ); // compl
376  pLitsSat[1] = Abc_LitNot( pLitsSat[1] ); // compl
377  RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
378  assert( RetValue );
379  p->timeSatUnsat += Abc_Clock() - clk;
380  }
381  else if ( RetValue == l_True )
382  {
383  Ssc_ManCollectSatPattern( p, p->vPattern );
384  p->timeSatSat += Abc_Clock() - clk;
385  return l_True;
386  }
387  else // if ( RetValue1 == l_Undef )
388  {
389  p->timeSatUndec += Abc_Clock() - clk;
390  return l_Undef;
391  }
392 
393  // if the old node was constant 0, we already know the answer
394  if ( iRepr == 0 )
395  return l_False;
396 
397  // solve under assumptions
398  // A = 0; B = 1
399  clk = Abc_Clock();
400  RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
401  if ( RetValue == l_False )
402  {
403  pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
404  pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
405  RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
406  assert( RetValue );
407  p->timeSatUnsat += Abc_Clock() - clk;
408  }
409  else if ( RetValue == l_True )
410  {
411  Ssc_ManCollectSatPattern( p, p->vPattern );
412  p->timeSatSat += Abc_Clock() - clk;
413  return l_True;
414  }
415  else // if ( RetValue1 == l_Undef )
416  {
417  p->timeSatUndec += Abc_Clock() - clk;
418  return l_Undef;
419  }
420  return l_False;
421 }
422 
423 
424 ////////////////////////////////////////////////////////////////////////
425 /// END OF FILE ///
426 ////////////////////////////////////////////////////////////////////////
427 
428 
430 
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static ABC_NAMESPACE_IMPL_START int Ssc_ObjSatLit(Ssc_Man_t *p, int Lit)
DECLARATIONS ///.
Definition: sscSat.c:32
static Gia_Obj_t * Gia_ObjChild0(Gia_Obj_t *pObj)
Definition: gia.h:457
static int Ssc_ObjSatVar(Ssc_Man_t *p, int iObj)
MACRO DEFINITIONS ///.
Definition: sscInt.h:90
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static void Gia_ManAddClausesMux(Ssc_Man_t *p, Gia_Obj_t *pNode)
FUNCTION DEFINITIONS ///.
Definition: sscSat.c:49
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
#define l_Undef
Definition: SolverTypes.h:86
int nClauses
Definition: cnf.h:61
typedefABC_NAMESPACE_HEADER_START struct Ssc_Man_t_ Ssc_Man_t
INCLUDES ///.
Definition: sscInt.h:46
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
static void sat_solver_compress(sat_solver *s)
Definition: satSolver.h:217
void Ssc_ManCollectSatPattern(Ssc_Man_t *p, Vec_Int_t *vPattern)
Definition: sscSat.c:315
int nVars
Definition: cnf.h:59
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
int * pVarNums
Definition: cnf.h:63
static int Gia_ObjFaninId1p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:464
#define l_True
Definition: SolverTypes.h:84
static abctime Abc_Clock()
Definition: abc_global.h:279
Definition: cnf.h:56
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Definition: gia.h:75
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
static void Ssc_ManCollectSuper(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vSuper)
Definition: sscSat.c:176
static Gia_Obj_t * Gia_ObjChild1(Gia_Obj_t *pObj)
Definition: gia.h:458
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
int ** pClauses
Definition: cnf.h:62
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static void Ssc_ManCnfNodeAddToSolver(Ssc_Man_t *p, int NodeId)
Definition: sscSat.c:208
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static void Gia_ManAddClausesSuper(Ssc_Man_t *p, Gia_Obj_t *pNode, Vec_Int_t *vSuper)
Definition: sscSat.c:128
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static void Ssc_ObjSetSatVar(Ssc_Man_t *p, int iObj, int Num)
Definition: sscInt.h:91
static int Gia_ManCandNum(Gia_Man_t *p)
Definition: gia.h:394
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
int Gia_ObjIsMuxType(Gia_Obj_t *pNode)
Definition: giaUtil.c:885
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Vec_Int_t * Ssc_ManFindPivotSat(Ssc_Man_t *p)
Definition: sscSat.c:323
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static int Gia_IsComplement(Gia_Obj_t *p)
Definition: gia.h:380
void Ssc_ManStartSolver(Ssc_Man_t *p)
Definition: sscSat.c:261
static void Ssc_ManCnfAddToFrontier(Ssc_Man_t *p, int Id, Vec_Int_t *vFront)
Definition: sscSat.c:196
Gia_Obj_t * Gia_ObjRecognizeMux(Gia_Obj_t *pNode, Gia_Obj_t **ppNodeT, Gia_Obj_t **ppNodeE)
Definition: giaUtil.c:959
Definition: gia.h:95
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
#define l_False
Definition: SolverTypes.h:85
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
#define assert(ex)
Definition: util_old.h:213
static int Vec_IntPushUnique(Vec_Int_t *p, int Entry)
Definition: vecInt.h:832
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
ABC_INT64_T abctime
Definition: abc_global.h:278
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int Ssc_ManCheckEquivalence(Ssc_Man_t *p, int iRepr, int iNode, int fCompl)
Definition: sscSat.c:348
static int Gia_Obj2Lit(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:433
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static void Ssc_ManCollectSuper_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vSuper)
Definition: sscSat.c:165