src/aig/fra/fraSat.c File Reference

#include <math.h>
#include "fra.h"
Include dependency graph for fraSat.c:

Go to the source code of this file.

Functions

static int Fra_SetActivityFactors (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
int Fra_NodesAreEquiv (Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
int Fra_NodesAreImp (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 312 of file fraSat.c.

00313 {
00314     int pLits[2], RetValue1, RetValue, clk;
00315 
00316     // make sure the nodes are not complemented
00317     assert( !Aig_IsComplement(pNew) );
00318     assert( pNew != p->pManFraig->pConst1 );
00319     p->nSatCalls++;
00320 
00321     // make sure the solver is allocated and has enough variables
00322     if ( p->pSat == NULL )
00323     {
00324         p->pSat = sat_solver_new();
00325         p->nSatVars = 1;
00326         sat_solver_setnvars( p->pSat, 1000 );
00327         // var 0 is reserved for const1 node - add the clause
00328         pLits[0] = toLit( 0 );
00329         sat_solver_addclause( p->pSat, pLits, pLits + 1 );
00330     }
00331 
00332     // if the nodes do not have SAT variables, allocate them
00333     Fra_CnfNodeAddToSolver( p, NULL, pNew );
00334 
00335     // prepare variable activity
00336     if ( p->pPars->fConeBias )
00337         Fra_SetActivityFactors( p, NULL, pNew ); 
00338 
00339     // solve under assumptions
00340 clk = clock();
00341     pLits[0] = toLitCond( Fra_ObjSatNum(pNew), pNew->fPhase );
00342     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1, 
00343         (sint64)p->pPars->nBTLimitMiter, (sint64)0, 
00344         p->nBTLimitGlobal, p->nInsLimitGlobal );
00345 p->timeSat += clock() - clk;
00346     if ( RetValue1 == l_False )
00347     {
00348 p->timeSatUnsat += clock() - clk;
00349         pLits[0] = lit_neg( pLits[0] );
00350         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
00351         assert( RetValue );
00352         // continue solving the other implication
00353         p->nSatCallsUnsat++;
00354     }
00355     else if ( RetValue1 == l_True )
00356     {
00357 p->timeSatSat += clock() - clk;
00358         if ( p->pPatWords )
00359             Fra_SmlSavePattern( p );
00360         p->nSatCallsSat++;
00361         return 0;
00362     }
00363     else // if ( RetValue1 == l_Undef )
00364     {
00365 p->timeSatFail += clock() - clk;
00366         // mark the node as the failed node
00367         pNew->fMarkB = 1;
00368         p->nSatFailsReal++;
00369         return -1;
00370     }
00371 
00372     // return SAT proof
00373     p->nSatProof++;
00374     return 1;
00375 }

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 45 of file fraSat.c.

00046 {
00047     int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
00048     int status;
00049 
00050     // make sure the nodes are not complemented
00051     assert( !Aig_IsComplement(pNew) );
00052     assert( !Aig_IsComplement(pOld) );
00053     assert( pNew != pOld );
00054 
00055     // if at least one of the nodes is a failed node, perform adjustments:
00056     // if the backtrack limit is small, simply skip this node
00057     // if the backtrack limit is > 10, take the quare root of the limit
00058     nBTLimit = p->pPars->nBTLimitNode;
00059     if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
00060     {
00061         p->nSatFails++;
00062         // fail immediately
00063 //        return -1;
00064         if ( nBTLimit <= 10 )
00065             return -1;
00066         nBTLimit = (int)pow(nBTLimit, 0.7);
00067     }
00068 
00069     p->nSatCalls++;
00070     p->nSatCallsRecent++;
00071 
00072     // make sure the solver is allocated and has enough variables
00073     if ( p->pSat == NULL )
00074     {
00075         p->pSat = sat_solver_new();
00076         p->nSatVars = 1;
00077         sat_solver_setnvars( p->pSat, 1000 );
00078         // var 0 is reserved for const1 node - add the clause
00079         pLits[0] = toLit( 0 );
00080         sat_solver_addclause( p->pSat, pLits, pLits + 1 );
00081     }
00082 
00083     // if the nodes do not have SAT variables, allocate them
00084     Fra_CnfNodeAddToSolver( p, pOld, pNew );
00085 
00086     if ( p->pSat->qtail != p->pSat->qhead )
00087     {
00088         status = sat_solver_simplify(p->pSat);
00089         assert( status != 0 );
00090         assert( p->pSat->qtail == p->pSat->qhead );
00091     }
00092 
00093     // prepare variable activity
00094     if ( p->pPars->fConeBias )
00095         Fra_SetActivityFactors( p, pOld, pNew ); 
00096 
00097     // solve under assumptions
00098     // A = 1; B = 0     OR     A = 1; B = 1 
00099 clk = clock();
00100     pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
00101     pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
00102 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
00103     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
00104         (sint64)nBTLimit, (sint64)0, 
00105         p->nBTLimitGlobal, p->nInsLimitGlobal );
00106 p->timeSat += clock() - clk;
00107     if ( RetValue1 == l_False )
00108     {
00109 p->timeSatUnsat += clock() - clk;
00110         pLits[0] = lit_neg( pLits[0] );
00111         pLits[1] = lit_neg( pLits[1] );
00112         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
00113         assert( RetValue );
00114         // continue solving the other implication
00115         p->nSatCallsUnsat++;
00116     }
00117     else if ( RetValue1 == l_True )
00118     {
00119 p->timeSatSat += clock() - clk;
00120         Fra_SmlSavePattern( p );
00121         p->nSatCallsSat++;
00122         return 0;
00123     }
00124     else // if ( RetValue1 == l_Undef )
00125     {
00126 p->timeSatFail += clock() - clk;
00127         // mark the node as the failed node
00128         if ( pOld != p->pManFraig->pConst1 ) 
00129             pOld->fMarkB = 1;
00130         pNew->fMarkB = 1;
00131         p->nSatFailsReal++;
00132         return -1;
00133     }
00134 
00135     // if the old node was constant 0, we already know the answer
00136     if ( pOld == p->pManFraig->pConst1 )
00137     {
00138         p->nSatProof++;
00139         return 1;
00140     }
00141 
00142     // solve under assumptions
00143     // A = 0; B = 1     OR     A = 0; B = 0 
00144 clk = clock();
00145     pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 1 );
00146     pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
00147     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
00148         (sint64)nBTLimit, (sint64)0, 
00149         p->nBTLimitGlobal, p->nInsLimitGlobal );
00150 p->timeSat += clock() - clk;
00151     if ( RetValue1 == l_False )
00152     {
00153 p->timeSatUnsat += clock() - clk;
00154         pLits[0] = lit_neg( pLits[0] );
00155         pLits[1] = lit_neg( pLits[1] );
00156         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
00157         assert( RetValue );
00158         p->nSatCallsUnsat++;
00159     }
00160     else if ( RetValue1 == l_True )
00161     {
00162 p->timeSatSat += clock() - clk;
00163         Fra_SmlSavePattern( p );
00164         p->nSatCallsSat++;
00165         return 0;
00166     }
00167     else // if ( RetValue1 == l_Undef )
00168     {
00169 p->timeSatFail += clock() - clk;
00170         // mark the node as the failed node
00171         pOld->fMarkB = 1;
00172         pNew->fMarkB = 1;
00173         p->nSatFailsReal++;
00174         return -1;
00175     }
00176 /*
00177     // check BDD proof
00178     {
00179         int RetVal;
00180         PRT( "Sat", clock() - clk2 );
00181         clk2 = clock();
00182         RetVal = Fra_NodesAreEquivBdd( pOld, pNew );
00183 //        printf( "%d ", RetVal );
00184         assert( RetVal );
00185         PRT( "Bdd", clock() - clk2 );
00186         printf( "\n" );
00187     }
00188 */
00189     // return SAT proof
00190     p->nSatProof++;
00191     return 1;
00192 }

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 205 of file fraSat.c.

00206 {
00207     int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
00208     int status;
00209 
00210     // make sure the nodes are not complemented
00211     assert( !Aig_IsComplement(pNew) );
00212     assert( !Aig_IsComplement(pOld) );
00213     assert( pNew != pOld );
00214 
00215     // if at least one of the nodes is a failed node, perform adjustments:
00216     // if the backtrack limit is small, simply skip this node
00217     // if the backtrack limit is > 10, take the quare root of the limit
00218     nBTLimit = p->pPars->nBTLimitNode;
00219 /*
00220     if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
00221     {
00222         p->nSatFails++;
00223         // fail immediately
00224 //        return -1;
00225         if ( nBTLimit <= 10 )
00226             return -1;
00227         nBTLimit = (int)pow(nBTLimit, 0.7);
00228     }
00229 */
00230     p->nSatCalls++;
00231 
00232     // make sure the solver is allocated and has enough variables
00233     if ( p->pSat == NULL )
00234     {
00235         p->pSat = sat_solver_new();
00236         p->nSatVars = 1;
00237         sat_solver_setnvars( p->pSat, 1000 );
00238         // var 0 is reserved for const1 node - add the clause
00239         pLits[0] = toLit( 0 );
00240         sat_solver_addclause( p->pSat, pLits, pLits + 1 );
00241     }
00242 
00243     // if the nodes do not have SAT variables, allocate them
00244     Fra_CnfNodeAddToSolver( p, pOld, pNew );
00245 
00246     if ( p->pSat->qtail != p->pSat->qhead )
00247     {
00248         status = sat_solver_simplify(p->pSat);
00249         assert( status != 0 );
00250         assert( p->pSat->qtail == p->pSat->qhead );
00251     }
00252 
00253     // prepare variable activity
00254     if ( p->pPars->fConeBias )
00255         Fra_SetActivityFactors( p, pOld, pNew ); 
00256 
00257     // solve under assumptions
00258     // A = 1; B = 0     OR     A = 1; B = 1 
00259 clk = clock();
00260 //    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
00261 //    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
00262     pLits[0] = toLitCond( Fra_ObjSatNum(pOld),  fComplL );
00263     pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
00264 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
00265     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
00266         (sint64)nBTLimit, (sint64)0, 
00267         p->nBTLimitGlobal, p->nInsLimitGlobal );
00268 p->timeSat += clock() - clk;
00269     if ( RetValue1 == l_False )
00270     {
00271 p->timeSatUnsat += clock() - clk;
00272         pLits[0] = lit_neg( pLits[0] );
00273         pLits[1] = lit_neg( pLits[1] );
00274         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
00275         assert( RetValue );
00276         // continue solving the other implication
00277         p->nSatCallsUnsat++;
00278     }
00279     else if ( RetValue1 == l_True )
00280     {
00281 p->timeSatSat += clock() - clk;
00282         Fra_SmlSavePattern( p );
00283         p->nSatCallsSat++;
00284         return 0;
00285     }
00286     else // if ( RetValue1 == l_Undef )
00287     {
00288 p->timeSatFail += clock() - clk;
00289         // mark the node as the failed node
00290         if ( pOld != p->pManFraig->pConst1 ) 
00291             pOld->fMarkB = 1;
00292         pNew->fMarkB = 1;
00293         p->nSatFailsReal++;
00294         return -1;
00295     }
00296     // return SAT proof
00297     p->nSatProof++;
00298     return 1;
00299 }

int Fra_SetActivityFactors ( Fra_Man_t *  p,
Aig_Obj_t *  pOld,
Aig_Obj_t *  pNew 
) [static]

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

] DECLARATIONS ///

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

Synopsis [Sets variable activities in the cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 424 of file fraSat.c.

00425 {
00426     int clk, LevelMin, LevelMax;
00427     assert( pOld || pNew );
00428 clk = clock(); 
00429     // reset the active variables
00430     veci_resize(&p->pSat->act_vars, 0);
00431     // prepare for traversal
00432     Aig_ManIncrementTravId( p->pManFraig );
00433     // determine the min and max level to visit
00434     assert( p->pPars->dActConeRatio > 0 && p->pPars->dActConeRatio < 1 );
00435     LevelMax = AIG_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
00436     LevelMin = (int)(LevelMax * (1.0 - p->pPars->dActConeRatio));
00437     // traverse
00438     if ( pOld && !Aig_ObjIsConst1(pOld) )
00439         Fra_SetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
00440     if ( pNew && !Aig_ObjIsConst1(pNew) )
00441         Fra_SetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
00442 //Fra_PrintActivity( p );
00443 p->timeTrav += clock() - clk;
00444     return 1;
00445 }

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 388 of file fraSat.c.

00389 {
00390     Vec_Ptr_t * vFanins;
00391     Aig_Obj_t * pFanin;
00392     int i, Counter = 0;
00393     assert( !Aig_IsComplement(pObj) );
00394     assert( Fra_ObjSatNum(pObj) );
00395     // skip visited variables
00396     if ( Aig_ObjIsTravIdCurrent(p->pManFraig, pObj) )
00397         return 0;
00398     Aig_ObjSetTravIdCurrent(p->pManFraig, pObj);
00399     // add the PI to the list
00400     if ( pObj->Level <= (unsigned)LevelMin || Aig_ObjIsPi(pObj) )
00401         return 0;
00402     // set the factor of this variable
00403     // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump
00404     p->pSat->factors[Fra_ObjSatNum(pObj)] = p->pPars->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin);
00405     veci_push(&p->pSat->act_vars, Fra_ObjSatNum(pObj));
00406     // explore the fanins
00407     vFanins = Fra_ObjFaninVec( pObj );
00408     Vec_PtrForEachEntry( vFanins, pFanin, i )
00409         Counter += Fra_SetActivityFactors_rec( p, Aig_Regular(pFanin), LevelMin, LevelMax );
00410     return 1 + Counter;
00411 }

Generated on Tue Jan 5 12:18:20 2010 for abc70930 by  doxygen 1.6.1