abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraSat.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [fraSat.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [New FRAIG package.]
8 
9  Synopsis []
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 30, 2007.]
16 
17  Revision [$Id: fraSat.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include <math.h>
22 #include "fra.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
32 
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36 
37 /**Function*************************************************************
38 
39  Synopsis [Runs equivalence test for the two nodes.]
40 
41  Description []
42 
43  SideEffects []
44 
45  SeeAlso []
46 
47 ***********************************************************************/
48 int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
49 {
50  int pLits[4], RetValue, RetValue1, nBTLimit;
51  abctime clk;//, clk2 = Abc_Clock();
52  int status;
53 
54  // make sure the nodes are not complemented
55  assert( !Aig_IsComplement(pNew) );
56  assert( !Aig_IsComplement(pOld) );
57  assert( pNew != pOld );
58 
59  // if at least one of the nodes is a failed node, perform adjustments:
60  // if the backtrack limit is small, simply skip this node
61  // if the backtrack limit is > 10, take the quare root of the limit
62  nBTLimit = p->pPars->nBTLimitNode;
63  if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
64  {
65  p->nSatFails++;
66  // fail immediately
67 // return -1;
68  if ( nBTLimit <= 10 )
69  return -1;
70  nBTLimit = (int)pow(nBTLimit, 0.7);
71  }
72 
73  p->nSatCalls++;
74  p->nSatCallsRecent++;
75 
76  // make sure the solver is allocated and has enough variables
77  if ( p->pSat == NULL )
78  {
79  p->pSat = sat_solver_new();
80  p->nSatVars = 1;
81  sat_solver_setnvars( p->pSat, 1000 );
82  // var 0 is reserved for const1 node - add the clause
83  pLits[0] = toLit( 0 );
84  sat_solver_addclause( p->pSat, pLits, pLits + 1 );
85  }
86 
87  // if the nodes do not have SAT variables, allocate them
88  Fra_CnfNodeAddToSolver( p, pOld, pNew );
89 
90  if ( p->pSat->qtail != p->pSat->qhead )
91  {
92  status = sat_solver_simplify(p->pSat);
93  assert( status != 0 );
94  assert( p->pSat->qtail == p->pSat->qhead );
95  }
96 
97  // prepare variable activity
98  if ( p->pPars->fConeBias )
99  Fra_SetActivityFactors( p, pOld, pNew );
100 
101  // solve under assumptions
102  // A = 1; B = 0 OR A = 1; B = 1
103 clk = Abc_Clock();
104  pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
105  pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
106 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
107  RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
108  (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
109  p->nBTLimitGlobal, p->nInsLimitGlobal );
110 p->timeSat += Abc_Clock() - clk;
111  if ( RetValue1 == l_False )
112  {
113 p->timeSatUnsat += Abc_Clock() - clk;
114  pLits[0] = lit_neg( pLits[0] );
115  pLits[1] = lit_neg( pLits[1] );
116  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
117  assert( RetValue );
118  // continue solving the other implication
119  p->nSatCallsUnsat++;
120  }
121  else if ( RetValue1 == l_True )
122  {
123 p->timeSatSat += Abc_Clock() - clk;
124  Fra_SmlSavePattern( p );
125  p->nSatCallsSat++;
126  return 0;
127  }
128  else // if ( RetValue1 == l_Undef )
129  {
130 p->timeSatFail += Abc_Clock() - clk;
131  // mark the node as the failed node
132  if ( pOld != p->pManFraig->pConst1 )
133  pOld->fMarkB = 1;
134  pNew->fMarkB = 1;
135  p->nSatFailsReal++;
136  return -1;
137  }
138 
139  // if the old node was constant 0, we already know the answer
140  if ( pOld == p->pManFraig->pConst1 )
141  {
142  p->nSatProof++;
143  return 1;
144  }
145 
146  // solve under assumptions
147  // A = 0; B = 1 OR A = 0; B = 0
148 clk = Abc_Clock();
149  pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 1 );
150  pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
151  RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
152  (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
153  p->nBTLimitGlobal, p->nInsLimitGlobal );
154 p->timeSat += Abc_Clock() - clk;
155  if ( RetValue1 == l_False )
156  {
157 p->timeSatUnsat += Abc_Clock() - clk;
158  pLits[0] = lit_neg( pLits[0] );
159  pLits[1] = lit_neg( pLits[1] );
160  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
161  assert( RetValue );
162  p->nSatCallsUnsat++;
163  }
164  else if ( RetValue1 == l_True )
165  {
166 p->timeSatSat += Abc_Clock() - clk;
167  Fra_SmlSavePattern( p );
168  p->nSatCallsSat++;
169  return 0;
170  }
171  else // if ( RetValue1 == l_Undef )
172  {
173 p->timeSatFail += Abc_Clock() - clk;
174  // mark the node as the failed node
175  pOld->fMarkB = 1;
176  pNew->fMarkB = 1;
177  p->nSatFailsReal++;
178  return -1;
179  }
180 /*
181  // check BDD proof
182  {
183  int RetVal;
184  ABC_PRT( "Sat", Abc_Clock() - clk2 );
185  clk2 = Abc_Clock();
186  RetVal = Fra_NodesAreEquivBdd( pOld, pNew );
187 // printf( "%d ", RetVal );
188  assert( RetVal );
189  ABC_PRT( "Bdd", Abc_Clock() - clk2 );
190  printf( "\n" );
191  }
192 */
193  // return SAT proof
194  p->nSatProof++;
195  return 1;
196 }
197 
198 /**Function*************************************************************
199 
200  Synopsis [Runs the result of test for pObj => pNew.]
201 
202  Description []
203 
204  SideEffects []
205 
206  SeeAlso []
207 
208 ***********************************************************************/
209 int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR )
210 {
211  int pLits[4], RetValue, RetValue1, nBTLimit;
212  abctime clk;//, clk2 = Abc_Clock();
213  int status;
214 
215  // make sure the nodes are not complemented
216  assert( !Aig_IsComplement(pNew) );
217  assert( !Aig_IsComplement(pOld) );
218  assert( pNew != pOld );
219 
220  // if at least one of the nodes is a failed node, perform adjustments:
221  // if the backtrack limit is small, simply skip this node
222  // if the backtrack limit is > 10, take the quare root of the limit
223  nBTLimit = p->pPars->nBTLimitNode;
224 /*
225  if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
226  {
227  p->nSatFails++;
228  // fail immediately
229 // return -1;
230  if ( nBTLimit <= 10 )
231  return -1;
232  nBTLimit = (int)pow(nBTLimit, 0.7);
233  }
234 */
235  p->nSatCalls++;
236 
237  // make sure the solver is allocated and has enough variables
238  if ( p->pSat == NULL )
239  {
240  p->pSat = sat_solver_new();
241  p->nSatVars = 1;
242  sat_solver_setnvars( p->pSat, 1000 );
243  // var 0 is reserved for const1 node - add the clause
244  pLits[0] = toLit( 0 );
245  sat_solver_addclause( p->pSat, pLits, pLits + 1 );
246  }
247 
248  // if the nodes do not have SAT variables, allocate them
249  Fra_CnfNodeAddToSolver( p, pOld, pNew );
250 
251  if ( p->pSat->qtail != p->pSat->qhead )
252  {
253  status = sat_solver_simplify(p->pSat);
254  assert( status != 0 );
255  assert( p->pSat->qtail == p->pSat->qhead );
256  }
257 
258  // prepare variable activity
259  if ( p->pPars->fConeBias )
260  Fra_SetActivityFactors( p, pOld, pNew );
261 
262  // solve under assumptions
263  // A = 1; B = 0 OR A = 1; B = 1
264 clk = Abc_Clock();
265 // pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
266 // pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
267  pLits[0] = toLitCond( Fra_ObjSatNum(pOld), fComplL );
268  pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
269 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
270  RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
271  (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
272  p->nBTLimitGlobal, p->nInsLimitGlobal );
273 p->timeSat += Abc_Clock() - clk;
274  if ( RetValue1 == l_False )
275  {
276 p->timeSatUnsat += Abc_Clock() - clk;
277  pLits[0] = lit_neg( pLits[0] );
278  pLits[1] = lit_neg( pLits[1] );
279  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
280  assert( RetValue );
281  // continue solving the other implication
282  p->nSatCallsUnsat++;
283  }
284  else if ( RetValue1 == l_True )
285  {
286 p->timeSatSat += Abc_Clock() - clk;
287  Fra_SmlSavePattern( p );
288  p->nSatCallsSat++;
289  return 0;
290  }
291  else // if ( RetValue1 == l_Undef )
292  {
293 p->timeSatFail += Abc_Clock() - clk;
294  // mark the node as the failed node
295  if ( pOld != p->pManFraig->pConst1 )
296  pOld->fMarkB = 1;
297  pNew->fMarkB = 1;
298  p->nSatFailsReal++;
299  return -1;
300  }
301  // return SAT proof
302  p->nSatProof++;
303  return 1;
304 }
305 
306 /**Function*************************************************************
307 
308  Synopsis [Runs the result of test for pObj => pNew.]
309 
310  Description []
311 
312  SideEffects []
313 
314  SeeAlso []
315 
316 ***********************************************************************/
317 int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR )
318 {
319  int pLits[4], RetValue, RetValue1, nBTLimit;
320  abctime clk;//, clk2 = Abc_Clock();
321  int status;
322 
323  // make sure the nodes are not complemented
324  assert( !Aig_IsComplement(pNew) );
325  assert( !Aig_IsComplement(pOld) );
326  assert( pNew != pOld );
327 
328  // if at least one of the nodes is a failed node, perform adjustments:
329  // if the backtrack limit is small, simply skip this node
330  // if the backtrack limit is > 10, take the quare root of the limit
331  nBTLimit = p->pPars->nBTLimitNode;
332 /*
333  if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
334  {
335  p->nSatFails++;
336  // fail immediately
337 // return -1;
338  if ( nBTLimit <= 10 )
339  return -1;
340  nBTLimit = (int)pow(nBTLimit, 0.7);
341  }
342 */
343  p->nSatCalls++;
344 
345  // make sure the solver is allocated and has enough variables
346  if ( p->pSat == NULL )
347  {
348  p->pSat = sat_solver_new();
349  p->nSatVars = 1;
350  sat_solver_setnvars( p->pSat, 1000 );
351  // var 0 is reserved for const1 node - add the clause
352  pLits[0] = toLit( 0 );
353  sat_solver_addclause( p->pSat, pLits, pLits + 1 );
354  }
355 
356  // if the nodes do not have SAT variables, allocate them
357  Fra_CnfNodeAddToSolver( p, pOld, pNew );
358 
359  if ( p->pSat->qtail != p->pSat->qhead )
360  {
361  status = sat_solver_simplify(p->pSat);
362  assert( status != 0 );
363  assert( p->pSat->qtail == p->pSat->qhead );
364  }
365 
366  // prepare variable activity
367  if ( p->pPars->fConeBias )
368  Fra_SetActivityFactors( p, pOld, pNew );
369 
370  // solve under assumptions
371  // A = 1; B = 0 OR A = 1; B = 1
372 clk = Abc_Clock();
373 // pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
374 // pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
375  pLits[0] = toLitCond( Fra_ObjSatNum(pOld), !fComplL );
376  pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
377 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
378  RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
379  (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
380  p->nBTLimitGlobal, p->nInsLimitGlobal );
381 p->timeSat += Abc_Clock() - clk;
382  if ( RetValue1 == l_False )
383  {
384 p->timeSatUnsat += Abc_Clock() - clk;
385  pLits[0] = lit_neg( pLits[0] );
386  pLits[1] = lit_neg( pLits[1] );
387  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
388  assert( RetValue );
389  // continue solving the other implication
390  p->nSatCallsUnsat++;
391  }
392  else if ( RetValue1 == l_True )
393  {
394 p->timeSatSat += Abc_Clock() - clk;
395  Fra_SmlSavePattern( p );
396  p->nSatCallsSat++;
397  return 0;
398  }
399  else // if ( RetValue1 == l_Undef )
400  {
401 p->timeSatFail += Abc_Clock() - clk;
402  // mark the node as the failed node
403  if ( pOld != p->pManFraig->pConst1 )
404  pOld->fMarkB = 1;
405  pNew->fMarkB = 1;
406  p->nSatFailsReal++;
407  return -1;
408  }
409  // return SAT proof
410  p->nSatProof++;
411  return 1;
412 }
413 
414 /**Function*************************************************************
415 
416  Synopsis [Runs equivalence test for one node.]
417 
418  Description [Returns the fraiged node.]
419 
420  SideEffects []
421 
422  SeeAlso []
423 
424 ***********************************************************************/
425 int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
426 {
427  int pLits[2], RetValue1, RetValue;
428  abctime clk;
429 
430  // make sure the nodes are not complemented
431  assert( !Aig_IsComplement(pNew) );
432  assert( pNew != p->pManFraig->pConst1 );
433  p->nSatCalls++;
434 
435  // make sure the solver is allocated and has enough variables
436  if ( p->pSat == NULL )
437  {
438  p->pSat = sat_solver_new();
439  p->nSatVars = 1;
440  sat_solver_setnvars( p->pSat, 1000 );
441  // var 0 is reserved for const1 node - add the clause
442  pLits[0] = toLit( 0 );
443  sat_solver_addclause( p->pSat, pLits, pLits + 1 );
444  }
445 
446  // if the nodes do not have SAT variables, allocate them
447  Fra_CnfNodeAddToSolver( p, NULL, pNew );
448 
449  // prepare variable activity
450  if ( p->pPars->fConeBias )
451  Fra_SetActivityFactors( p, NULL, pNew );
452 
453  // solve under assumptions
454 clk = Abc_Clock();
455  pLits[0] = toLitCond( Fra_ObjSatNum(pNew), pNew->fPhase );
456  RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1,
457  (ABC_INT64_T)p->pPars->nBTLimitMiter, (ABC_INT64_T)0,
458  p->nBTLimitGlobal, p->nInsLimitGlobal );
459 p->timeSat += Abc_Clock() - clk;
460  if ( RetValue1 == l_False )
461  {
462 p->timeSatUnsat += Abc_Clock() - clk;
463  pLits[0] = lit_neg( pLits[0] );
464  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
465  assert( RetValue );
466  // continue solving the other implication
467  p->nSatCallsUnsat++;
468  }
469  else if ( RetValue1 == l_True )
470  {
471 p->timeSatSat += Abc_Clock() - clk;
472  if ( p->pPatWords )
473  Fra_SmlSavePattern( p );
474  p->nSatCallsSat++;
475  return 0;
476  }
477  else // if ( RetValue1 == l_Undef )
478  {
479 p->timeSatFail += Abc_Clock() - clk;
480  // mark the node as the failed node
481  pNew->fMarkB = 1;
482  p->nSatFailsReal++;
483  return -1;
484  }
485 
486  // return SAT proof
487  p->nSatProof++;
488  return 1;
489 }
490 
491 /**Function*************************************************************
492 
493  Synopsis [Sets variable activities in the cone.]
494 
495  Description []
496 
497  SideEffects []
498 
499  SeeAlso []
500 
501 ***********************************************************************/
502 int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, int LevelMax )
503 {
504  Vec_Ptr_t * vFanins;
505  Aig_Obj_t * pFanin;
506  int i, Counter = 0;
507  assert( !Aig_IsComplement(pObj) );
508  assert( Fra_ObjSatNum(pObj) );
509  // skip visited variables
510  if ( Aig_ObjIsTravIdCurrent(p->pManFraig, pObj) )
511  return 0;
512  Aig_ObjSetTravIdCurrent(p->pManFraig, pObj);
513  // add the PI to the list
514  if ( pObj->Level <= (unsigned)LevelMin || Aig_ObjIsCi(pObj) )
515  return 0;
516  // set the factor of this variable
517  // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump
518  if ( p->pSat->factors == NULL )
519  p->pSat->factors = ABC_CALLOC( double, p->pSat->cap );
520  p->pSat->factors[Fra_ObjSatNum(pObj)] = p->pPars->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin);
521  veci_push(&p->pSat->act_vars, Fra_ObjSatNum(pObj));
522  // explore the fanins
523  vFanins = Fra_ObjFaninVec( pObj );
524  Vec_PtrForEachEntry( Aig_Obj_t *, vFanins, pFanin, i )
525  Counter += Fra_SetActivityFactors_rec( p, Aig_Regular(pFanin), LevelMin, LevelMax );
526  return 1 + Counter;
527 }
528 
529 /**Function*************************************************************
530 
531  Synopsis [Sets variable activities in the cone.]
532 
533  Description []
534 
535  SideEffects []
536 
537  SeeAlso []
538 
539 ***********************************************************************/
540 int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
541 {
542  int LevelMin, LevelMax;
543  abctime clk;
544  assert( pOld || pNew );
545 clk = Abc_Clock();
546  // reset the active variables
547  veci_resize(&p->pSat->act_vars, 0);
548  // prepare for traversal
549  Aig_ManIncrementTravId( p->pManFraig );
550  // determine the min and max level to visit
551  assert( p->pPars->dActConeRatio > 0 && p->pPars->dActConeRatio < 1 );
552  LevelMax = Abc_MaxInt( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
553  LevelMin = (int)(LevelMax * (1.0 - p->pPars->dActConeRatio));
554  // traverse
555  if ( pOld && !Aig_ObjIsConst1(pOld) )
556  Fra_SetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
557  if ( pNew && !Aig_ObjIsConst1(pNew) )
558  Fra_SetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
559 //Fra_PrintActivity( p );
560 p->timeTrav += Abc_Clock() - clk;
561  return 1;
562 }
563 
564 
565 ////////////////////////////////////////////////////////////////////////
566 /// END OF FILE ///
567 ////////////////////////////////////////////////////////////////////////
568 
569 
570 ABC_NAMESPACE_IMPL_END
571 
Fra_SetActivityFactors
static ABC_NAMESPACE_IMPL_START int Fra_SetActivityFactors(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
DECLARATIONS ///.
Definition: fraSat.c:540
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
sat_solver_t::act_vars
veci act_vars
Definition: satSolver.h:167
Fra_Man_t_::nSatProof
int nSatProof
Definition: fra.h:231
Aig_Obj_t_::Level
unsigned Level
Definition: aig.h:82
Fra_Man_t_::nInsLimitGlobal
ABC_INT64_T nInsLimitGlobal
Definition: fra.h:214
sat_solver_t::cap
int cap
Definition: satSolver.h:94
Fra_Man_t_::nSatCallsUnsat
int nSatCallsUnsat
Definition: fra.h:230
Fra_Man_t_::timeSatSat
abctime timeSatSat
Definition: fra.h:245
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition: aig.h:80
Fra_Man_t_::pPars
Fra_Par_t * pPars
Definition: fra.h:189
sat_solver_solve
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
Fra_Man_t_::pSat
sat_solver * pSat
Definition: fra.h:210
Fra_NodeIsConst
int Fra_NodeIsConst(Fra_Man_t *p, Aig_Obj_t *pNew)
Definition: fraSat.c:425
veci_push
static void veci_push(veci *v, int e)
Definition: satVec.h:53
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Fra_Man_t_::timeTrav
abctime timeTrav
Definition: fra.h:241
Fra_Man_t_::nBTLimitGlobal
ABC_INT64_T nBTLimitGlobal
Definition: fra.h:213
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Fra_Man_t_::timeSat
abctime timeSat
Definition: fra.h:243
l_True
#define l_True
Definition: SolverTypes.h:84
Fra_Man_t_::nSatVars
int nSatVars
Definition: fra.h:211
veci_resize
static void veci_resize(veci *v, int k)
Definition: satVec.h:47
sat_solver_t::qhead
int qhead
Definition: satSolver.h:95
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Fra_SetActivityFactors_rec
int Fra_SetActivityFactors_rec(Fra_Man_t *p, Aig_Obj_t *pObj, int LevelMin, int LevelMax)
Definition: fraSat.c:502
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Fra_CnfNodeAddToSolver
void Fra_CnfNodeAddToSolver(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
Definition: fraCnf.c:238
Fra_Man_t_::pPatWords
unsigned * pPatWords
Definition: fra.h:205
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
sat_solver_t::factors
double * factors
Definition: satSolver.h:168
Fra_Man_t_::pManFraig
Aig_Man_t * pManFraig
Definition: fra.h:192
Fra_Man_t_::nSatCalls
int nSatCalls
Definition: fra.h:228
Fra_NodesAreClause
int Fra_NodesAreClause(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew, int fComplL, int fComplR)
Definition: fraSat.c:317
toLit
static lit toLit(int v)
Definition: satVec.h:142
Fra_NodesAreEquiv
int Fra_NodesAreEquiv(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
FUNCTION DEFINITIONS ///.
Definition: fraSat.c:48
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Fra_Man_t_::timeSatFail
abctime timeSatFail
Definition: fra.h:246
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Fra_Man_t_::nSatFails
int nSatFails
Definition: fra.h:232
Aig_Obj_t_
Definition: aig.h:69
Counter
static int Counter
Definition: extraBddMisc.c:1877
Fra_Man_t_::timeSatUnsat
abctime timeSatUnsat
Definition: fra.h:244
Fra_Man_t_::nSatFailsReal
int nSatFailsReal
Definition: fra.h:233
Fra_Man_t_::nSatCallsRecent
int nSatCallsRecent
Definition: fra.h:237
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
sat_solver_simplify
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
Fra_NodesAreImp
int Fra_NodesAreImp(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew, int fComplL, int fComplR)
Definition: fraSat.c:209
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
sat_solver_t::qtail
int qtail
Definition: satSolver.h:96
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
l_False
#define l_False
Definition: SolverTypes.h:85
Fra_Man_t_
Definition: fra.h:186
Fra_ObjSatNum
static int Fra_ObjSatNum(Aig_Obj_t *pObj)
Definition: fra.h:266
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Fra_Man_t_::nSatCallsSat
int nSatCallsSat
Definition: fra.h:229
Fra_ObjFaninVec
static Vec_Ptr_t * Fra_ObjFaninVec(Aig_Obj_t *pObj)
Definition: fra.h:263
Fra_SmlSavePattern
void Fra_SmlSavePattern(Fra_Man_t *p)
Definition: fraSim.c:241