(!******************************************************
   Mosel Example Programs
   ======================

   file cnf2mos.mos
   ````````````````
   A (W)CNF to MOS converter.

   (c) 2020 Fair Isaac Corporation
       author: Y.Colombani, Jun. 2020
*******************************************************!)

model cnf2mos
version 0.0.1
uses 'mmsystem','deploy'

parameters
  MAXLEN=80              ! Maximum length of lines (for printing the objective)
end-parameters

declarations
 ! The following text is added before calling 'minimise'
  before_solve=`
setparam('xprs_loadnames', true)
`
  src,dest,fname,prefix: text         ! Handling of filenames
  line,objtext: text                  ! Aux. texts
  nbvar,nbcl,nbwc: integer            ! Various counters
  whrd: real                          ! Weight value for binding clauses
  iswcnf: boolean                     ! Whether problem is a WCNF
  curlen: integer                     ! Line length indicator
  wcfile="tmp:"+newmuid

 ! Subroutines defined by this program
  procedure skipcomment(l:text)
  procedure parseoptions(l:text)
  procedure parseclause(l:text)
  procedure displayclause(lst:list of integer)
  procedure displaynotclause(lst:list of integer)
end-declarations

! Check for filename argument and display 'usage' banner if none is found
if argc=1 then
  writeln("Usage: mosel cnf2mos -- filename (.cnf[.gz] or .wcnf[.gz])")
  exit(1)
elif argc<>2 then
  writeln("Usage: cnf2mos filename (.cnf[.gz] or .wcnf[.gz])")
  exit(1)
else
  fname:=argv(2)
end-if

! Check whether input file is compressed
src:=pathsplit(SYS_FNAME,fname)
if endswith(src,".gz") then
  prefix:="zlib.gzip:"
  dest:=src-".gz"
else
  dest:=src
end-if

! Supported extensions: .cnf and .wcnf
if endswith(dest,".cnf") then
  dest:=(dest-".cnf")+".mos"
elif endswith(dest,".wcnf") then
  dest:=(dest-".wcnf")+".mos"
else
  dest+=".mos"
end-if

! Don't overwrite existing file
if getfstat(dest)<>0 then
  writeln("File '", dest, "' exists - aborting")
  exit(2)
end-if

! Start the transformation
fopen(prefix+fname,F_INPUT)
writeln("Generating '", dest, "'...")
fopen(dest,F_OUTPUT)

! Header text for generated file
writeln("! Generated by cnf2mos v",getparam("model_version")," from '",src,"'");
writeln("model sat\nuses 'mmxprs'\n")

! Process the clauses
nbcl:=1
curlen:=5
while(readtextline(line)>0 and nbcl>0) do
 case getchar(line,1) of
  99:  ! c
	skipcomment(line)
  112: ! p
	parseoptions(line)
  else
   parseclause(line)
 end-case
end-do

writeln

! Objective function for MAXSAT case, solver call and solution reporting
if iswcnf and objtext.size>0 then
  if nbwc>0 then
    writeln("RW:=1..",nbwc,"\nfinalise(RW)")
    fclose(F_OUTPUT)
    fcopy(wcfile,0,dest,F_APPEND)
    fopen(dest,F_OUTPUT+F_APPEND)
    writeln
  end-if
  deltext(objtext,1,1)  ! remove leading '+'
  writeln("Obj:=",objtext,"\n")
  write(before_solve)
  writeln("minimise(Obj)")
else
  write(before_solve)
  writeln("minimise(1)")
end-if
write(`
if getprobstat<>XPRS_OPT then
  writeln("Problem is infeasible")
else
  writeln("Solution:")
`)
if iswcnf then
 writeln('  writeln(" Obj=", getobjval)')
end-if
writeln(`
  forall(i in R | b(i).sol) write(" b(", i, ")")
  writeln
end-if
end-model
`)

!**************** Implementation of subroutines ****************

! Skip comment line
procedure skipcomment(l:text)
  deltext(l,1,1)
  write("! ",l)
end-procedure

! Read options/instance parameters and generate Mosel declarations
procedure parseoptions(l:text)
  type:=parsetext(l,3)
  if type<>"cnf" and type<>"wcnf" then
    fclose(F_INPUT)
    fclose(F_OUTPUT)
    writeln("Unsupported format '",type,"' - aborting")
    exit(3)
  end-if
  asproc(nextfield(l))
  nbvar:=parseint(l)
  asproc(nextfield(l))
  nbcl:=parseint(l)
  if type="wcnf" then
    iswcnf:=true
    asproc(nextfield(l))
    whrd:=parsereal(l)
  end-if
  writeln("public declarations\n  R=1..",nbvar,"\n  b: array(R) of boolvar")
  if iswcnf then
    writeln("  RW: range\n  w: array(RW) of boolvar")
  end-if
  writeln("end-declarations\n")
  writeln("writeln('Model generated from file \"",src,"\"')")
  writeln("writeln('Problem size:')")
  writeln("writeln(' variables: ",nbvar,"')")
  writeln("writeln(' clauses:   ",nbcl,"')")
  if iswcnf then
    writeln("writeln(' top weight:",whrd,"')")
  end-if
  writeln
end-procedure

! Read a clause
procedure parseclause(l:text)
  declarations
    lst:list of integer
    firstval:boolean
    txtline:text
  end-declarations

  setparam("sys_endparse",0)
  firstval:=true
  while(nextfield(l))
    if iswcnf and firstval then
      firstval:=false
      weight:=parsereal(l)
    else
      lst+=[parseint(l)]
    end-if

  if iswcnf and weight<>whrd then
    wtxt:=if(weight<>1,text(weight)+"*",text(""))
    if lst.size=2 then        ! only 1 value and 0
      if lst(1)<0 then
        txtline:=wtxt+"b("+(-lst(1))+").var"
      else
        txtline:=wtxt+"getvar(not b("+lst(1)+"))"
      end-if
    else                      ! 2 or more values
      nbwc+=1
      txtline:=wtxt+"w("+nbwc+").var"
      fopen(wcfile,F_OUTPUT+F_APPEND)
      write("w(",nbwc,")=(")
      displaynotclause(lst)
      writeln(")")
      fclose(F_OUTPUT)
    end-if
    if curlen+txtline.size+1>MAXLEN then
      curlen:=4+txtline.size
      objtext+=text("+\n   ")+txtline
    else
      curlen+=txtline.size+1
      objtext+=text("+")+txtline
    end-if
  else
    displayclause(lst)
    writeln
  end-if

  nbcl-=1
end-procedure

! Output a clause in Mosel format
procedure displayclause(lst:list of integer)
  declarations
    firstdone:boolean
  end-declarations

  forall(i in lst|i<>0) do
    if firstdone then
      write(" or ")
    else
      firstdone:=true
    end-if
    if i<0 then
      write("not b(",-i,")")
    else
      write("b(",i,")")
    end-if
  end-do
end-procedure

! Output the negation of a clause in Mosel format
procedure displaynotclause(lst:list of integer)
  declarations
    firstdone:boolean
  end-declarations

  forall(i in lst|i<>0) do
    if firstdone then
      write(" and ")
    else
      firstdone:=true
    end-if
    if i<0 then
      write("b(",-i,")")
    else
      write("not b(",i,")")
    end-if
  end-do
end-procedure

end-model