private long computeLBD ( final MSClause c ) { long nblevels = 0 ; myflag ++ ; if ( incremental ) { long nbDone = 0 ; for ( int i = 0 ; i < c . size ( ) ; i ++ ) { if ( nbDone >= c . sizeWithoutSelectors ( ) ) break ; if ( isSelector ( var ( c . get ( i ) ) ) ) continue ; nbDone ++ ; int l = v ( c . get ( i ) ) . level ( ) ; if ( permDiff . get ( l ) != myflag ) { permDiff . set ( l , myflag ) ; nblevels ++ ; } } } else { for ( int i = 0 ; i < c . size ( ) ; i ++ ) { int l = v ( c . get ( i ) ) . level ( ) ; if ( permDiff . get ( l ) != myflag ) { permDiff . set ( l , myflag ) ; nblevels ++ ; } } } if ( ! reduceOnSize ) return nblevels ; if ( c . size ( ) < reduceOnSizeSize ) return c . size ( ) ; return c . size ( ) + nblevels ; }
Computes the LBD for a given clause