ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
fraSat.c
Go to the documentation of this file.
1
20
21#include <math.h>
22#include "fra.h"
23
24ABC_NAMESPACE_IMPL_START
25
26
30
31static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
32
36
48int 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
103clk = 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 );
110p->timeSat += Abc_Clock() - clk;
111 if ( RetValue1 == l_False )
112 {
113p->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 {
123p->timeSatSat += Abc_Clock() - clk;
124 Fra_SmlSavePattern( p );
125 p->nSatCallsSat++;
126 return 0;
127 }
128 else // if ( RetValue1 == l_Undef )
129 {
130p->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
148clk = 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 );
154p->timeSat += Abc_Clock() - clk;
155 if ( RetValue1 == l_False )
156 {
157p->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 {
166p->timeSatSat += Abc_Clock() - clk;
167 Fra_SmlSavePattern( p );
168 p->nSatCallsSat++;
169 return 0;
170 }
171 else // if ( RetValue1 == l_Undef )
172 {
173p->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
209int 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
264clk = 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 );
273p->timeSat += Abc_Clock() - clk;
274 if ( RetValue1 == l_False )
275 {
276p->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 {
286p->timeSatSat += Abc_Clock() - clk;
287 Fra_SmlSavePattern( p );
288 p->nSatCallsSat++;
289 return 0;
290 }
291 else // if ( RetValue1 == l_Undef )
292 {
293p->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
317int 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
372clk = 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 );
381p->timeSat += Abc_Clock() - clk;
382 if ( RetValue1 == l_False )
383 {
384p->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 {
394p->timeSatSat += Abc_Clock() - clk;
395 Fra_SmlSavePattern( p );
396 p->nSatCallsSat++;
397 return 0;
398 }
399 else // if ( RetValue1 == l_Undef )
400 {
401p->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
425int 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
454clk = 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 );
459p->timeSat += Abc_Clock() - clk;
460 if ( RetValue1 == l_False )
461 {
462p->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 {
471p->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 {
479p->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
502int 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
540int 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 );
545clk = 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 );
560p->timeTrav += Abc_Clock() - clk;
561 return 1;
562}
563
564
568
569
570ABC_NAMESPACE_IMPL_END
571
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigUtil.c:44
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
l_True
#define l_True
Definition bmcBmcS.c:35
l_False
#define l_False
Definition bmcBmcS.c:36
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
p
Cube * p
Definition exorList.c:222
Fra_NodeIsConst
int Fra_NodeIsConst(Fra_Man_t *p, Aig_Obj_t *pNew)
Definition fraSat.c:425
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
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
Fra_SetActivityFactors_rec
int Fra_SetActivityFactors_rec(Fra_Man_t *p, Aig_Obj_t *pObj, int LevelMin, int LevelMax)
Definition fraSat.c:502
Fra_NodesAreEquiv
int Fra_NodesAreEquiv(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
FUNCTION DEFINITIONS ///.
Definition fraSat.c:48
Fra_Man_t
struct Fra_Man_t_ Fra_Man_t
Definition fra.h:56
Fra_CnfNodeAddToSolver
void Fra_CnfNodeAddToSolver(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
Definition fraCnf.c:238
Fra_SmlSavePattern
void Fra_SmlSavePattern(Fra_Man_t *p)
Definition fraSim.c:241
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
sat_solver_simplify
int sat_solver_simplify(sat_solver *s)
Definition satSolver.c:1515
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition aig.h:80
Aig_Obj_t_::Level
unsigned Level
Definition aig.h:82
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition aig.h:78
assert
#define assert(ex)
Definition util_old.h:213
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55