abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraSat.c File Reference
#include <math.h>
#include "fra.h"

Go to the source code of this file.

Functions

static ABC_NAMESPACE_IMPL_START int Fra_SetActivityFactors (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
 DECLARATIONS ///. More...
 
int Fra_NodesAreEquiv (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
 FUNCTION DEFINITIONS ///. More...
 
int Fra_NodesAreImp (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew, int fComplL, int fComplR)
 
int Fra_NodesAreClause (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew, int fComplL, int fComplR)
 
int Fra_NodeIsConst (Fra_Man_t *p, Aig_Obj_t *pNew)
 
int Fra_SetActivityFactors_rec (Fra_Man_t *p, Aig_Obj_t *pObj, int LevelMin, int LevelMax)
 

Function Documentation

int Fra_NodeIsConst ( Fra_Man_t p,
Aig_Obj_t pNew 
)

Function*************************************************************

Synopsis [Runs equivalence test for one node.]

Description [Returns the fraiged node.]

SideEffects []

SeeAlso []

Definition at line 425 of file fraSat.c.

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,
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 }
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
int nSatProof
Definition: fra.h:231
ABC_INT64_T nInsLimitGlobal
Definition: fra.h:214
int nSatCallsUnsat
Definition: fra.h:230
abctime timeSatSat
Definition: fra.h:245
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
unsigned int fMarkB
Definition: aig.h:80
Fra_Par_t * pPars
Definition: fra.h:189
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
sat_solver * pSat
Definition: fra.h:210
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
ABC_INT64_T nBTLimitGlobal
Definition: fra.h:213
abctime timeSat
Definition: fra.h:243
#define l_True
Definition: SolverTypes.h:84
int nSatVars
Definition: fra.h:211
static abctime Abc_Clock()
Definition: abc_global.h:279
void Fra_CnfNodeAddToSolver(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
Definition: fraCnf.c:238
unsigned * pPatWords
Definition: fra.h:205
static lit lit_neg(lit l)
Definition: satVec.h:144
Aig_Man_t * pManFraig
Definition: fra.h:192
int nSatCalls
Definition: fra.h:228
static lit toLit(int v)
Definition: satVec.h:142
static lit toLitCond(int v, int c)
Definition: satVec.h:143
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
abctime timeSatFail
Definition: fra.h:246
abctime timeSatUnsat
Definition: fra.h:244
int nSatFailsReal
Definition: fra.h:233
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
unsigned int fPhase
Definition: aig.h:78
#define l_False
Definition: SolverTypes.h:85
static int Fra_ObjSatNum(Aig_Obj_t *pObj)
Definition: fra.h:266
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
int nSatCallsSat
Definition: fra.h:229
void Fra_SmlSavePattern(Fra_Man_t *p)
Definition: fraSim.c:241
int Fra_NodesAreClause ( Fra_Man_t p,
Aig_Obj_t pOld,
Aig_Obj_t pNew,
int  fComplL,
int  fComplR 
)

Function*************************************************************

Synopsis [Runs the result of test for pObj => pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 317 of file fraSat.c.

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,
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 }
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
int nSatProof
Definition: fra.h:231
ABC_INT64_T nInsLimitGlobal
Definition: fra.h:214
int nSatCallsUnsat
Definition: fra.h:230
abctime timeSatSat
Definition: fra.h:245
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
unsigned int fMarkB
Definition: aig.h:80
Fra_Par_t * pPars
Definition: fra.h:189
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
sat_solver * pSat
Definition: fra.h:210
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
ABC_INT64_T nBTLimitGlobal
Definition: fra.h:213
abctime timeSat
Definition: fra.h:243
#define l_True
Definition: SolverTypes.h:84
int nSatVars
Definition: fra.h:211
static abctime Abc_Clock()
Definition: abc_global.h:279
void Fra_CnfNodeAddToSolver(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
Definition: fraCnf.c:238
static lit lit_neg(lit l)
Definition: satVec.h:144
Aig_Man_t * pManFraig
Definition: fra.h:192
int nSatCalls
Definition: fra.h:228
static lit toLit(int v)
Definition: satVec.h:142
static lit toLitCond(int v, int c)
Definition: satVec.h:143
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
abctime timeSatFail
Definition: fra.h:246
abctime timeSatUnsat
Definition: fra.h:244
int nSatFailsReal
Definition: fra.h:233
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
#define l_False
Definition: SolverTypes.h:85
static int Fra_ObjSatNum(Aig_Obj_t *pObj)
Definition: fra.h:266
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
int nSatCallsSat
Definition: fra.h:229
void Fra_SmlSavePattern(Fra_Man_t *p)
Definition: fraSim.c:241
int Fra_NodesAreEquiv ( Fra_Man_t p,
Aig_Obj_t pOld,
Aig_Obj_t pNew 
)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Runs equivalence test for the two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file fraSat.c.

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,
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,
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 }
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
int nSatProof
Definition: fra.h:231
ABC_INT64_T nInsLimitGlobal
Definition: fra.h:214
int nSatCallsUnsat
Definition: fra.h:230
abctime timeSatSat
Definition: fra.h:245
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
unsigned int fMarkB
Definition: aig.h:80
Fra_Par_t * pPars
Definition: fra.h:189
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
sat_solver * pSat
Definition: fra.h:210
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
ABC_INT64_T nBTLimitGlobal
Definition: fra.h:213
abctime timeSat
Definition: fra.h:243
#define l_True
Definition: SolverTypes.h:84
int nSatVars
Definition: fra.h:211
static abctime Abc_Clock()
Definition: abc_global.h:279
void Fra_CnfNodeAddToSolver(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
Definition: fraCnf.c:238
static lit lit_neg(lit l)
Definition: satVec.h:144
Aig_Man_t * pManFraig
Definition: fra.h:192
int nSatCalls
Definition: fra.h:228
static lit toLit(int v)
Definition: satVec.h:142
static lit toLitCond(int v, int c)
Definition: satVec.h:143
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
abctime timeSatFail
Definition: fra.h:246
int nSatFails
Definition: fra.h:232
abctime timeSatUnsat
Definition: fra.h:244
int nSatFailsReal
Definition: fra.h:233
int nSatCallsRecent
Definition: fra.h:237
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
unsigned int fPhase
Definition: aig.h:78
#define l_False
Definition: SolverTypes.h:85
static int Fra_ObjSatNum(Aig_Obj_t *pObj)
Definition: fra.h:266
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
int nSatCallsSat
Definition: fra.h:229
void Fra_SmlSavePattern(Fra_Man_t *p)
Definition: fraSim.c:241
int Fra_NodesAreImp ( Fra_Man_t p,
Aig_Obj_t pOld,
Aig_Obj_t pNew,
int  fComplL,
int  fComplR 
)

Function*************************************************************

Synopsis [Runs the result of test for pObj => pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 209 of file fraSat.c.

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,
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 }
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
int nSatProof
Definition: fra.h:231
ABC_INT64_T nInsLimitGlobal
Definition: fra.h:214
int nSatCallsUnsat
Definition: fra.h:230
abctime timeSatSat
Definition: fra.h:245
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
unsigned int fMarkB
Definition: aig.h:80
Fra_Par_t * pPars
Definition: fra.h:189
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
sat_solver * pSat
Definition: fra.h:210
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
ABC_INT64_T nBTLimitGlobal
Definition: fra.h:213
abctime timeSat
Definition: fra.h:243
#define l_True
Definition: SolverTypes.h:84
int nSatVars
Definition: fra.h:211
static abctime Abc_Clock()
Definition: abc_global.h:279
void Fra_CnfNodeAddToSolver(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
Definition: fraCnf.c:238
static lit lit_neg(lit l)
Definition: satVec.h:144
Aig_Man_t * pManFraig
Definition: fra.h:192
int nSatCalls
Definition: fra.h:228
static lit toLit(int v)
Definition: satVec.h:142
static lit toLitCond(int v, int c)
Definition: satVec.h:143
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
abctime timeSatFail
Definition: fra.h:246
abctime timeSatUnsat
Definition: fra.h:244
int nSatFailsReal
Definition: fra.h:233
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
#define l_False
Definition: SolverTypes.h:85
static int Fra_ObjSatNum(Aig_Obj_t *pObj)
Definition: fra.h:266
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
int nSatCallsSat
Definition: fra.h:229
void Fra_SmlSavePattern(Fra_Man_t *p)
Definition: fraSim.c:241
int Fra_SetActivityFactors ( Fra_Man_t p,
Aig_Obj_t pOld,
Aig_Obj_t pNew 
)
static

DECLARATIONS ///.

CFile****************************************************************

FileName [fraSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:
fraSat.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

]

Function*************************************************************

Synopsis [Sets variable activities in the cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 540 of file fraSat.c.

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
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 }
veci act_vars
Definition: satSolver.h:167
unsigned Level
Definition: aig.h:82
Fra_Par_t * pPars
Definition: fra.h:189
sat_solver * pSat
Definition: fra.h:210
abctime timeTrav
Definition: fra.h:241
static void veci_resize(veci *v, int k)
Definition: satVec.h:47
static abctime Abc_Clock()
Definition: abc_global.h:279
int Fra_SetActivityFactors_rec(Fra_Man_t *p, Aig_Obj_t *pObj, int LevelMin, int LevelMax)
Definition: fraSat.c:502
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Aig_Man_t * pManFraig
Definition: fra.h:192
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
int Fra_SetActivityFactors_rec ( Fra_Man_t p,
Aig_Obj_t pObj,
int  LevelMin,
int  LevelMax 
)

Function*************************************************************

Synopsis [Sets variable activities in the cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 502 of file fraSat.c.

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;
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 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
veci act_vars
Definition: satSolver.h:167
unsigned Level
Definition: aig.h:82
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Fra_Par_t * pPars
Definition: fra.h:189
sat_solver * pSat
Definition: fra.h:210
static void veci_push(veci *v, int e)
Definition: satVec.h:53
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
int Fra_SetActivityFactors_rec(Fra_Man_t *p, Aig_Obj_t *pObj, int LevelMin, int LevelMax)
Definition: fraSat.c:502
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
double * factors
Definition: satSolver.h:168
Aig_Man_t * pManFraig
Definition: fra.h:192
Definition: aig.h:69
static int Counter
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
static int Fra_ObjSatNum(Aig_Obj_t *pObj)
Definition: fra.h:266
#define assert(ex)
Definition: util_old.h:213
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
static Vec_Ptr_t * Fra_ObjFaninVec(Aig_Obj_t *pObj)
Definition: fra.h:263