private void addClause ( final Formula formula , int weight ) { this . result = UNDEF ; final LNGIntVector clauseVec = new LNGIntVector ( ( int ) formula . numberOfAtoms ( ) ) ; for ( Literal lit : formula . literals ( ) ) { Integer index = this . var2index . get ( lit . variable ( ) ) ; if ( index == null ) { index = this . solver . newLiteral ( false ) >> 1 ; this . var2index . put ( lit . variable ( ) , index ) ; this . index2var . put ( index , lit . variable ( ) ) ; } int litNum = lit . phase ( ) ? index * 2 : ( index * 2 ) ^ 1 ; clauseVec . push ( litNum ) ; } if ( weight == - 1 ) { this . solver . addHardClause ( clauseVec ) ; } else { this . solver . setCurrentWeight ( weight ) ; this . solver . updateSumWeights ( weight ) ; this . solver . addSoftClause ( weight , clauseVec ) ; } }
Adds a clause to the solver .