import Ġjava . io . File Ċ import Ġjava . io . BufferedReader Ċ import Ġkotlin . math . abs Ċ Ċ class ĠParser ( filename : ĠString ) Ġ{ ĊĠĠĠ Ġprivate Ġval Ġbuffered Reader : ĠBufferedReader Ġ= ĠFile ( filename ). buffered Reader () ĊĊĠĠĠ Ġfun Ġparse (): ĠPair < List < Clause >, ĠInt >? Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġparameters String Ġ= Ġskip Comments () ĊĠĠĠĠĠĠĠ Ġif Ġ(! parameters String . startsWith (" p Ġc nf ")) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġreturn Ġnull ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġval Ġparams Ġ= Ġparameters String . drop While Ġ{ Ġc : ĠChar Ġ-> Ġ! c . is Digit () Ġ} ĊĠĠĠĠĠĠĠ Ġval Ġ( num Vars , Ġnum Clause s ) Ġ= Ġparams . split (" Ġ"). map Ġ{ Ġs Ġ-> Ġs . toInt () Ġ} ĊĊĠĠĠĠĠĠĠ Ġval Ġc nf Ġ= Ġmutable ListOf < Clause >() ĊĠĠĠĠĠĠĠ Ġfor Ġ( i Ġin Ġ 1 .. num Clause s ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġraw Clause Ġ= Ġbuffered Reader . readLine () ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ. split (" Ġ") ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ. filter Ġ{ it . isNotEmpty ()} ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ. map Ġ{ Ġs Ġ-> Ġs . toInt () Ġ} ĊĊĠĠĠĠĠĠĠĠĠĠĠ Ġif Ġ( raw Clause . last () Ġ!= Ġ 0 ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ|| Ġraw Clause . count Ġ{ Ġit Ġ== Ġ 0 Ġ} Ġ!= Ġ 1 ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ|| Ġraw Clause . count Ġ{ abs ( it ) Ġ> Ġnum Vars } Ġ!= Ġ 0 ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġreturn Ġnull ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠĠĠĠĠ Ġc nf . add ( Clause ( raw Clause . drop Last ( 1 ))) ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġreturn ĠPair ( cnf , Ġnum Vars ) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġprivate Ġfun Ġskip Comments (): ĠString Ġ{ ĊĠĠĠĠĠĠĠ Ġvar Ġinput String Ġ= Ġbuffered Reader . readLine () ĊĠĠĠĠĠĠĠ Ġwhile Ġ( input String [ 0 ] Ġ== Ġ' c ') Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġinput String Ġ= Ġbuffered Reader . readLine () ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġreturn Ġinput String ĊĠĠĠ Ġ} Ċ } Ċ