private LNGIntVector generateClauseVector ( final Collection < Literal > literals ) { final LNGIntVector clauseVec = new LNGIntVector ( literals . size ( ) ) ; for ( final Literal lit : literals ) { int index = this . solver . idxForName ( lit . name ( ) ) ; if ( index == - 1 ) { index = this . solver . newVar ( ! this . initialPhase , true ) ; this . solver . addName ( lit . name ( ) , index ) ; } final int litNum = lit . phase ( ) ? index * 2 : ( index * 2 ) ^ 1 ; clauseVec . push ( litNum ) ; } return clauseVec ; }
Generates a clause vector of a collection of literals .