(!******************************************************
   Mosel Example Problems
   ======================

   file boolvars.mos
   `````````````````
   Using type boolvar for stating logic clauses
   - Example discussed in mipformref whitepaper -  

   (c) 2020 Fair Isaac Corporation
       author: S. Heipcke, July 2020
*******************************************************!)
model boolvars
uses 'mmxprs'

public declarations
 R=1..5
 bv: array(R) of boolvar
 LC1, LC2: logctr
end-declarations

! Simple clause, same as:  bv(1) and not bv(5) = true
bv(1) and not bv(5)

! Association of clauses
bv(3)=(not bv(4))

! The opposite of 'bv(1) or bv(3)' must be false
(not (bv(1) or bv(3)))=false

! Defining a logic expression (not recorded in the constraint store)
LC1:= and(i in 1..3) bv(i) or and(i in 4..5) not bv(i)

! Turn expression into a constraint
LC1:= LC1=true

! A named logic expression (this defines a constraint)
LC2:= (or(i in 1..3) not bv(i)) = false

! Solve as feasibility (SAT) problem
setparam("XPRS_loadnames", true)
maximise(0)
if getprobstat=XPRS_OPT then
  forall(i in R) writeln(i, ": ", bv(i).sol)
else
  writeln("Problem is unsatisfiable")
end-if

! Retrieve associated binary variables for formulation of an objective function
Obj:=sum(i in R) bv(i).var

! Solve as optimization problem
maximise(Obj)
if getprobstat=XPRS_OPT then
  writeln("Solution: ", getobjval)
  forall(i in R) writeln(i, ": ", bv(i).sol)
else
  writeln("Problem is unsatisfiable")
end-if

writeprob("testout.lp","l")

end-model