diff options
| -rw-r--r-- | src/aig/gia/giaMan.c | 13 | ||||
| -rw-r--r-- | src/base/acb/acb.h | 1 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.c | 28 |
3 files changed, 31 insertions, 11 deletions
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 6dc395d2..e346b260 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -1315,18 +1315,21 @@ void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs ) fprintf( pFile, "\n" ); Gia_ManForEachAnd( p, pObj, i ) { + int fSkip = 0; if ( vObjs ) { Vec_IntForEachEntry( vObjs, iObj, k ) if ( iObj == i ) break; if ( k < Vec_IntSize(vObjs) ) - continue; + fSkip = 1; + } + if ( !fSkip ) + { + fprintf( pFile, " and( %s,", Gia_ObjGetDumpName(NULL, 'n', i, nDigits) ); + fprintf( pFile, " %s,", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC0(pObj)? 'i':'n'), Gia_ObjFaninId0(pObj, i), nDigits) ); + fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC1(pObj)? 'i':'n'), Gia_ObjFaninId1(pObj, i), nDigits) ); } - - fprintf( pFile, " and( %s,", Gia_ObjGetDumpName(NULL, 'n', i, nDigits) ); - fprintf( pFile, " %s,", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC0(pObj)? 'i':'n'), Gia_ObjFaninId0(pObj, i), nDigits) ); - fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC1(pObj)? 'i':'n'), Gia_ObjFaninId1(pObj, i), nDigits) ); if ( Vec_BitEntry(vInvs, i) ) { fprintf( pFile, " not( %s,", Gia_ObjGetDumpName(NULL, 'i', i, nDigits) ); diff --git a/src/base/acb/acb.h b/src/base/acb/acb.h index 76188f2e..36300efd 100644 --- a/src/base/acb/acb.h +++ b/src/base/acb/acb.h @@ -416,6 +416,7 @@ static inline int Acb_ObjWhatFanin( Acb_Ntk_t * p, int iObj, int iFaninGiven ) static inline void Acb_ObjAddFanin( Acb_Ntk_t * p, int iObj, int iFanin ) { int * pFanins = Acb_ObjFanins( p, iObj ); + assert( iFanin > 0 ); assert( pFanins[ 1 + pFanins[0] ] == -1 ); pFanins[ 1 + pFanins[0]++ ] = iFanin; } diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 31ae8dae..2f3a84db 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -217,16 +217,32 @@ static inline int order_select(sat_solver* s, float random_var_freq) // selectv void sat_solver_set_var_activity(sat_solver* s, int * pVars, int nVars) { int i; - assert( s->VarActType == 1 ); for (i = 0; i < s->size; i++) s->activity[i] = 0; - s->var_inc = Abc_Dbl2Word(1); - for ( i = 0; i < nVars; i++ ) + if ( s->VarActType == 0 ) { - int iVar = pVars ? pVars[i] : i; - s->activity[iVar] = Abc_Dbl2Word(nVars-i); - order_update( s, iVar ); + s->var_inc = (1 << 5); + s->var_decay = -1; + for ( i = 0; i < nVars; i++ ) + { + int iVar = pVars ? pVars[i] : i; + s->activity[iVar] = s->var_inc*(nVars-i); + if (s->orderpos[iVar] != -1) + order_update( s, iVar ); + } } + else if ( s->VarActType == 1 ) + { + s->var_inc = Abc_Dbl2Word(1); + for ( i = 0; i < nVars; i++ ) + { + int iVar = pVars ? pVars[i] : i; + s->activity[iVar] = Abc_Dbl2Word(nVars-i); + if (s->orderpos[iVar] != -1) + order_update( s, iVar ); + } + } + else assert( 0 ); } //================================================================================================= |