{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE OverloadedStrings #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.MIP2SMT
-- Copyright   :  (c) Masahiro Sakai 2012-2014,2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.Converter.MIP2SMT
  ( mip2smt
  , Options (..)
  , Language (..)
  , YicesVersion (..)
  ) where

import Data.Char
import Data.Default.Class
import Data.Interned
import Data.Ord
import Data.List
import Data.Ratio
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Text as T
import qualified Data.Text.Lazy.IO as TLIO
import Data.Text.Lazy.Builder (Builder)
import qualified Data.Text.Lazy.Builder as B
import qualified Data.Text.Lazy.Builder.Int as B
import Text.Printf

import qualified Numeric.Optimization.MIP as MIP
import ToySolver.Internal.Util (showRationalAsFiniteDecimal, isInteger)

-- | Translation options.
--
-- The default option can be obtained by 'def'.
data Options
  = Options
  { Options -> Language
optLanguage     :: Language
  , Options -> Maybe [Char]
optSetLogic     :: Maybe String
  , Options -> Bool
optCheckSAT     :: Bool
  , Options -> Bool
optProduceModel :: Bool
  , Options -> Bool
optOptimize     :: Bool
  }
  deriving (Int -> Options -> ShowS
[Options] -> ShowS
Options -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Options] -> ShowS
$cshowList :: [Options] -> ShowS
show :: Options -> [Char]
$cshow :: Options -> [Char]
showsPrec :: Int -> Options -> ShowS
$cshowsPrec :: Int -> Options -> ShowS
Show, Options -> Options -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Options -> Options -> Bool
$c/= :: Options -> Options -> Bool
== :: Options -> Options -> Bool
$c== :: Options -> Options -> Bool
Eq, Eq Options
Options -> Options -> Bool
Options -> Options -> Ordering
Options -> Options -> Options
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Options -> Options -> Options
$cmin :: Options -> Options -> Options
max :: Options -> Options -> Options
$cmax :: Options -> Options -> Options
>= :: Options -> Options -> Bool
$c>= :: Options -> Options -> Bool
> :: Options -> Options -> Bool
$c> :: Options -> Options -> Bool
<= :: Options -> Options -> Bool
$c<= :: Options -> Options -> Bool
< :: Options -> Options -> Bool
$c< :: Options -> Options -> Bool
compare :: Options -> Options -> Ordering
$ccompare :: Options -> Options -> Ordering
Ord)

instance Default Options where
  def :: Options
def =
    Options
    { optLanguage :: Language
optLanguage     = Language
SMTLIB2
    , optSetLogic :: Maybe [Char]
optSetLogic     = forall a. Maybe a
Nothing
    , optCheckSAT :: Bool
optCheckSAT     = Bool
True
    , optProduceModel :: Bool
optProduceModel = Bool
True
    , optOptimize :: Bool
optOptimize     = Bool
False
    }

data Language
  = SMTLIB2
  | YICES YicesVersion
  deriving (Int -> Language -> ShowS
[Language] -> ShowS
Language -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Language] -> ShowS
$cshowList :: [Language] -> ShowS
show :: Language -> [Char]
$cshow :: Language -> [Char]
showsPrec :: Int -> Language -> ShowS
$cshowsPrec :: Int -> Language -> ShowS
Show, Language -> Language -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Language -> Language -> Bool
$c/= :: Language -> Language -> Bool
== :: Language -> Language -> Bool
$c== :: Language -> Language -> Bool
Eq, Eq Language
Language -> Language -> Bool
Language -> Language -> Ordering
Language -> Language -> Language
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Language -> Language -> Language
$cmin :: Language -> Language -> Language
max :: Language -> Language -> Language
$cmax :: Language -> Language -> Language
>= :: Language -> Language -> Bool
$c>= :: Language -> Language -> Bool
> :: Language -> Language -> Bool
$c> :: Language -> Language -> Bool
<= :: Language -> Language -> Bool
$c<= :: Language -> Language -> Bool
< :: Language -> Language -> Bool
$c< :: Language -> Language -> Bool
compare :: Language -> Language -> Ordering
$ccompare :: Language -> Language -> Ordering
Ord)

data YicesVersion
  = Yices1
  | Yices2
  deriving (Int -> YicesVersion -> ShowS
[YicesVersion] -> ShowS
YicesVersion -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [YicesVersion] -> ShowS
$cshowList :: [YicesVersion] -> ShowS
show :: YicesVersion -> [Char]
$cshow :: YicesVersion -> [Char]
showsPrec :: Int -> YicesVersion -> ShowS
$cshowsPrec :: Int -> YicesVersion -> ShowS
Show, YicesVersion -> YicesVersion -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: YicesVersion -> YicesVersion -> Bool
$c/= :: YicesVersion -> YicesVersion -> Bool
== :: YicesVersion -> YicesVersion -> Bool
$c== :: YicesVersion -> YicesVersion -> Bool
Eq, Eq YicesVersion
YicesVersion -> YicesVersion -> Bool
YicesVersion -> YicesVersion -> Ordering
YicesVersion -> YicesVersion -> YicesVersion
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: YicesVersion -> YicesVersion -> YicesVersion
$cmin :: YicesVersion -> YicesVersion -> YicesVersion
max :: YicesVersion -> YicesVersion -> YicesVersion
$cmax :: YicesVersion -> YicesVersion -> YicesVersion
>= :: YicesVersion -> YicesVersion -> Bool
$c>= :: YicesVersion -> YicesVersion -> Bool
> :: YicesVersion -> YicesVersion -> Bool
$c> :: YicesVersion -> YicesVersion -> Bool
<= :: YicesVersion -> YicesVersion -> Bool
$c<= :: YicesVersion -> YicesVersion -> Bool
< :: YicesVersion -> YicesVersion -> Bool
$c< :: YicesVersion -> YicesVersion -> Bool
compare :: YicesVersion -> YicesVersion -> Ordering
$ccompare :: YicesVersion -> YicesVersion -> Ordering
Ord, Int -> YicesVersion
YicesVersion -> Int
YicesVersion -> [YicesVersion]
YicesVersion -> YicesVersion
YicesVersion -> YicesVersion -> [YicesVersion]
YicesVersion -> YicesVersion -> YicesVersion -> [YicesVersion]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: YicesVersion -> YicesVersion -> YicesVersion -> [YicesVersion]
$cenumFromThenTo :: YicesVersion -> YicesVersion -> YicesVersion -> [YicesVersion]
enumFromTo :: YicesVersion -> YicesVersion -> [YicesVersion]
$cenumFromTo :: YicesVersion -> YicesVersion -> [YicesVersion]
enumFromThen :: YicesVersion -> YicesVersion -> [YicesVersion]
$cenumFromThen :: YicesVersion -> YicesVersion -> [YicesVersion]
enumFrom :: YicesVersion -> [YicesVersion]
$cenumFrom :: YicesVersion -> [YicesVersion]
fromEnum :: YicesVersion -> Int
$cfromEnum :: YicesVersion -> Int
toEnum :: Int -> YicesVersion
$ctoEnum :: Int -> YicesVersion
pred :: YicesVersion -> YicesVersion
$cpred :: YicesVersion -> YicesVersion
succ :: YicesVersion -> YicesVersion
$csucc :: YicesVersion -> YicesVersion
Enum, YicesVersion
forall a. a -> a -> Bounded a
maxBound :: YicesVersion
$cmaxBound :: YicesVersion
minBound :: YicesVersion
$cminBound :: YicesVersion
Bounded)

-- ------------------------------------------------------------------------

type Var = T.Text
type Env = Map MIP.Var Var

list :: [Builder] -> Builder
list :: [Builder] -> Builder
list [Builder]
xs = Char -> Builder
B.singleton Char
'(' forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat (forall a. a -> [a] -> [a]
intersperse (Char -> Builder
B.singleton Char
' ') [Builder]
xs) forall a. Semigroup a => a -> a -> a
<> Char -> Builder
B.singleton Char
')'

and' :: [Builder] -> Builder
and' :: [Builder] -> Builder
and' [] = Builder
"true"
and' [Builder
x] = Builder
x
and' [Builder]
xs = [Builder] -> Builder
list (Builder
"and" forall a. a -> [a] -> [a]
: [Builder]
xs)

or' :: [Builder] -> Builder
or' :: [Builder] -> Builder
or' [] = Builder
"false"
or' [Builder
x] = Builder
x
or' [Builder]
xs = [Builder] -> Builder
list (Builder
"or" forall a. a -> [a] -> [a]
: [Builder]
xs)

not' :: Builder -> Builder
not' :: Builder -> Builder
not' Builder
x = [Builder] -> Builder
list [Builder
"not", Builder
x]

intExpr :: Options -> Env -> MIP.Problem Rational -> MIP.Expr Rational -> Builder
intExpr :: Options -> Env -> Problem Rational -> Expr Rational -> Builder
intExpr Options
opt Env
env Problem Rational
_mip Expr Rational
e =
  case forall c. Expr c -> [Term c]
MIP.terms Expr Rational
e of
    [] -> Options -> Integer -> Builder
intNum Options
opt Integer
0
    [Term Rational
t] -> forall {c}. (Show c, RealFrac c) => Term c -> Builder
f Term Rational
t
    [Term Rational]
ts -> [Builder] -> Builder
list (Char -> Builder
B.singleton Char
'+' forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall {c}. (Show c, RealFrac c) => Term c -> Builder
f [Term Rational]
ts)
  where
    f :: Term c -> Builder
f (MIP.Term c
c [Var]
_) | Bool -> Bool
not (forall a. RealFrac a => a -> Bool
isInteger c
c) =
      forall a. HasCallStack => [Char] -> a
error ([Char]
"ToySolver.Converter.MIP2SMT.intExpr: fractional coefficient: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show c
c)
    f (MIP.Term c
c []) = Options -> Integer -> Builder
intNum Options
opt (forall a b. (RealFrac a, Integral b) => a -> b
floor c
c)
    f (MIP.Term (-1) [Var]
vs) = [Builder] -> Builder
list [Char -> Builder
B.singleton Char
'-', Term c -> Builder
f (forall c. c -> [Var] -> Term c
MIP.Term c
1 [Var]
vs)]
    f (MIP.Term c
c [Var]
vs) =
      case [Builder]
xs of
        [] -> Options -> Integer -> Builder
intNum Options
opt Integer
1
        [Builder
x] -> Builder
x
        [Builder]
_ -> [Builder] -> Builder
list (Char -> Builder
B.singleton Char
'*' forall a. a -> [a] -> [a]
: [Builder]
xs)
      where
        xs :: [Builder]
xs = [Options -> Integer -> Builder
intNum Options
opt (forall a b. (RealFrac a, Integral b) => a -> b
floor c
c) | c
c forall a. Eq a => a -> a -> Bool
/= c
1] forall a. [a] -> [a] -> [a]
++
             [Text -> Builder
B.fromText (Env
env forall k a. Ord k => Map k a -> k -> a
Map.! Var
v) | Var
v <- [Var]
vs]

realExpr :: Options -> Env -> MIP.Problem Rational -> MIP.Expr Rational -> Builder
realExpr :: Options -> Env -> Problem Rational -> Expr Rational -> Builder
realExpr Options
opt Env
env Problem Rational
mip Expr Rational
e =
  case forall c. Expr c -> [Term c]
MIP.terms Expr Rational
e of
    [] -> Options -> Rational -> Builder
realNum Options
opt Rational
0
    [Term Rational
t] -> Term Rational -> Builder
f Term Rational
t
    [Term Rational]
ts -> [Builder] -> Builder
list (Char -> Builder
B.singleton Char
'+' forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Term Rational -> Builder
f [Term Rational]
ts)
  where
    f :: Term Rational -> Builder
f (MIP.Term Rational
c []) = Options -> Rational -> Builder
realNum Options
opt Rational
c
    f (MIP.Term (-1) [Var]
vs) = [Builder] -> Builder
list [Char -> Builder
B.singleton Char
'-', Term Rational -> Builder
f (forall c. c -> [Var] -> Term c
MIP.Term Rational
1 [Var]
vs)]
    f (MIP.Term Rational
c [Var]
vs) =
      case [Builder]
xs of
        [] -> Options -> Rational -> Builder
realNum Options
opt Rational
1
        [Builder
x] -> Builder
x
        [Builder]
_ -> [Builder] -> Builder
list (Char -> Builder
B.singleton Char
'*' forall a. a -> [a] -> [a]
: [Builder]
xs)
      where
        xs :: [Builder]
xs = [Options -> Rational -> Builder
realNum Options
opt Rational
c | Rational
c forall a. Eq a => a -> a -> Bool
/= Rational
1] forall a. [a] -> [a] -> [a]
++
             [ Builder
v3
             | Var
v <- [Var]
vs
             , let v2 :: Text
v2 = Env
env forall k a. Ord k => Map k a -> k -> a
Map.! Var
v
             , let v3 :: Builder
v3 = if Problem Rational -> Var -> Bool
isInt Problem Rational
mip Var
v
                        then Options -> Builder -> Builder
toReal Options
opt (Text -> Builder
B.fromText Text
v2)
                        else Text -> Builder
B.fromText Text
v2
             ]

intNum :: Options -> Integer -> Builder
intNum :: Options -> Integer -> Builder
intNum Options
opt Integer
x =
  case Options -> Language
optLanguage Options
opt of
    Language
SMTLIB2
      | Integer
x forall a. Ord a => a -> a -> Bool
< Integer
0     -> [Builder] -> Builder
list [Char -> Builder
B.singleton Char
'-', forall a. Integral a => a -> Builder
B.decimal (forall a. Num a => a -> a
negate Integer
x)]
      | Bool
otherwise -> forall a. Integral a => a -> Builder
B.decimal Integer
x
    YICES YicesVersion
_ -> forall a. Integral a => a -> Builder
B.decimal Integer
x

realNum :: Options -> Rational -> Builder
realNum :: Options -> Rational -> Builder
realNum Options
opt Rational
r =
  case Options -> Language
optLanguage Options
opt of
    Language
SMTLIB2
      | Rational
r forall a. Ord a => a -> a -> Bool
< Rational
0     -> [Builder] -> Builder
list [Char -> Builder
B.singleton Char
'-', Rational -> Builder
f (forall a. Num a => a -> a
negate Rational
r)]
      | Bool
otherwise -> Rational -> Builder
f Rational
r
    YICES YicesVersion
Yices1 ->
      if forall a. Ratio a -> a
denominator Rational
r forall a. Eq a => a -> a -> Bool
== Integer
1
        then forall a. Integral a => a -> Builder
B.decimal (forall a. Ratio a -> a
numerator Rational
r)
        else forall a. Integral a => a -> Builder
B.decimal (forall a. Ratio a -> a
numerator Rational
r) forall a. Semigroup a => a -> a -> a
<> Char -> Builder
B.singleton Char
'/' forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
B.decimal (forall a. Ratio a -> a
denominator Rational
r)
    YICES YicesVersion
Yices2 ->
      case Rational -> Maybe [Char]
showRationalAsFiniteDecimal Rational
r of
        Just [Char]
s  -> [Char] -> Builder
B.fromString [Char]
s
        Maybe [Char]
Nothing -> forall a. Integral a => a -> Builder
B.decimal (forall a. Ratio a -> a
numerator Rational
r) forall a. Semigroup a => a -> a -> a
<> Char -> Builder
B.singleton Char
'/' forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
B.decimal (forall a. Ratio a -> a
denominator Rational
r)
  where
    f :: Rational -> Builder
f Rational
r = case Rational -> Maybe [Char]
showRationalAsFiniteDecimal Rational
r of
            Just [Char]
s  -> [Char] -> Builder
B.fromString [Char]
s
            Maybe [Char]
Nothing -> [Builder] -> Builder
list [Char -> Builder
B.singleton Char
'/', forall a. Integral a => a -> Builder
B.decimal (forall a. Ratio a -> a
numerator Rational
r) forall a. Semigroup a => a -> a -> a
<> Builder
".0", forall a. Integral a => a -> Builder
B.decimal (forall a. Ratio a -> a
denominator Rational
r) forall a. Semigroup a => a -> a -> a
<> Builder
".0"]

rel2 :: Options -> Env -> MIP.Problem Rational -> Bool -> MIP.BoundExpr Rational -> MIP.Expr Rational -> MIP.BoundExpr Rational -> Builder
rel2 :: Options
-> Env
-> Problem Rational
-> Bool
-> BoundExpr Rational
-> Expr Rational
-> BoundExpr Rational
-> Builder
rel2 Options
opt Env
env Problem Rational
mip Bool
q BoundExpr Rational
lb Expr Rational
e BoundExpr Rational
ub = [Builder] -> Builder
and' ([Builder]
c1 forall a. [a] -> [a] -> [a]
++ [Builder]
c2)
  where
    c1 :: [Builder]
c1 =
      case BoundExpr Rational
lb of
        BoundExpr Rational
MIP.NegInf -> []
        MIP.Finite Rational
x -> [Options
-> Env
-> Problem Rational
-> Bool
-> RelOp
-> Expr Rational
-> Rational
-> Builder
rel Options
opt Env
env Problem Rational
mip Bool
q RelOp
MIP.Ge Expr Rational
e Rational
x]
        BoundExpr Rational
MIP.PosInf -> [Builder
"false"]
    c2 :: [Builder]
c2 =
      case BoundExpr Rational
ub of
        BoundExpr Rational
MIP.NegInf -> [Builder
"false"]
        MIP.Finite Rational
x -> [Options
-> Env
-> Problem Rational
-> Bool
-> RelOp
-> Expr Rational
-> Rational
-> Builder
rel Options
opt Env
env Problem Rational
mip Bool
q RelOp
MIP.Le Expr Rational
e Rational
x]
        BoundExpr Rational
MIP.PosInf -> []

rel :: Options -> Env -> MIP.Problem Rational -> Bool -> MIP.RelOp -> MIP.Expr Rational -> Rational -> Builder
rel :: Options
-> Env
-> Problem Rational
-> Bool
-> RelOp
-> Expr Rational
-> Rational
-> Builder
rel Options
opt Env
env Problem Rational
mip Bool
q RelOp
op Expr Rational
lhs Rational
rhs
  | forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Problem Rational -> Var -> Bool
isInt Problem Rational
mip Var
v | Var
v <- forall a. Set a -> [a]
Set.toList (forall a. Variables a => a -> Set Var
MIP.vars Expr Rational
lhs)] Bool -> Bool -> Bool
&&
    forall (t :: * -> *). Foldable t => t Bool -> Bool
and [forall a. RealFrac a => a -> Bool
isInteger Rational
c | MIP.Term Rational
c [Var]
_ <- forall c. Expr c -> [Term c]
MIP.terms Expr Rational
lhs] Bool -> Bool -> Bool
&& forall a. RealFrac a => a -> Bool
isInteger Rational
rhs =
      Bool -> RelOp -> Builder -> Builder -> Builder
f Bool
q RelOp
op (Options -> Env -> Problem Rational -> Expr Rational -> Builder
intExpr Options
opt Env
env Problem Rational
mip Expr Rational
lhs) (Options -> Integer -> Builder
intNum Options
opt (forall a b. (RealFrac a, Integral b) => a -> b
floor Rational
rhs))
  | Bool
otherwise =
      Bool -> RelOp -> Builder -> Builder -> Builder
f Bool
q RelOp
op (Options -> Env -> Problem Rational -> Expr Rational -> Builder
realExpr Options
opt Env
env Problem Rational
mip Expr Rational
lhs) (Options -> Rational -> Builder
realNum Options
opt Rational
rhs)
  where
    f :: Bool -> MIP.RelOp -> Builder -> Builder -> Builder
    f :: Bool -> RelOp -> Builder -> Builder -> Builder
f Bool
True RelOp
MIP.Eql Builder
x Builder
y = [Builder] -> Builder
and' [Bool -> RelOp -> Builder -> Builder -> Builder
f Bool
False RelOp
MIP.Le Builder
x Builder
y, Bool -> RelOp -> Builder -> Builder -> Builder
f Bool
False RelOp
MIP.Ge Builder
x Builder
y]
    f Bool
_ RelOp
MIP.Eql Builder
x Builder
y = [Builder] -> Builder
list [Builder
"=", Builder
x, Builder
y]
    f Bool
_ RelOp
MIP.Le Builder
x Builder
y = [Builder] -> Builder
list [Builder
"<=", Builder
x, Builder
y]
    f Bool
_ RelOp
MIP.Ge Builder
x Builder
y = [Builder] -> Builder
list [Builder
">=", Builder
x, Builder
y]

toReal :: Options -> Builder -> Builder
toReal :: Options -> Builder -> Builder
toReal Options
opt Builder
x =
  case Options -> Language
optLanguage Options
opt of
    Language
SMTLIB2 -> [Builder] -> Builder
list [Builder
"to_real", Builder
x]
    YICES YicesVersion
_ -> Builder
x

assert :: Options -> (Builder, Maybe T.Text) -> Builder
assert :: Options -> (Builder, Maybe Text) -> Builder
assert Options
opt (Builder
x, Maybe Text
label) = [Builder] -> Builder
list [Builder
"assert", Builder
x']
  where
    x' :: Builder
x' = case Maybe Text
label of
           Just Text
name | Options -> Language
optLanguage Options
opt forall a. Eq a => a -> a -> Bool
== Language
SMTLIB2 ->
             [Builder] -> Builder
list [ Builder
"!"
                  , Builder
x
                  , Builder
":named"
                  , Text -> Builder
B.fromText (Options -> Text -> Text
encode Options
opt Text
name)
                  ]
           Maybe Text
_ -> Builder
x

constraint :: Options -> Bool -> Env -> MIP.Problem Rational -> MIP.Constraint Rational -> (Builder, Maybe T.Text)
constraint :: Options
-> Bool
-> Env
-> Problem Rational
-> Constraint Rational
-> (Builder, Maybe Text)
constraint Options
opt Bool
q Env
env Problem Rational
mip
  MIP.Constraint
  { constrLabel :: forall c. Constraint c -> Maybe Text
MIP.constrLabel     = Maybe Text
label
  , constrIndicator :: forall c. Constraint c -> Maybe (Var, c)
MIP.constrIndicator = Maybe (Var, Rational)
g
  , constrExpr :: forall c. Constraint c -> Expr c
MIP.constrExpr = Expr Rational
e
  , constrLB :: forall c. Constraint c -> BoundExpr c
MIP.constrLB = BoundExpr Rational
lb
  , constrUB :: forall c. Constraint c -> BoundExpr c
MIP.constrUB = BoundExpr Rational
ub
  } = (Builder
c1, Maybe Text
label)
  where
    c0 :: Builder
c0 = Options
-> Env
-> Problem Rational
-> Bool
-> BoundExpr Rational
-> Expr Rational
-> BoundExpr Rational
-> Builder
rel2 Options
opt Env
env Problem Rational
mip Bool
q BoundExpr Rational
lb Expr Rational
e BoundExpr Rational
ub
    c1 :: Builder
c1 = case Maybe (Var, Rational)
g of
           Maybe (Var, Rational)
Nothing -> Builder
c0
           Just (Var
var,Rational
val) ->
             [Builder] -> Builder
list [ Builder
"=>"
                  , Options
-> Env
-> Problem Rational
-> Bool
-> RelOp
-> Expr Rational
-> Rational
-> Builder
rel Options
opt Env
env Problem Rational
mip Bool
q RelOp
MIP.Eql (forall c. Num c => Var -> Expr c
MIP.varExpr Var
var) Rational
val
                  , Builder
c0
                  ]

conditions :: Options -> Bool -> Env -> MIP.Problem Rational -> [(Builder, Maybe T.Text)]
conditions :: Options
-> Bool -> Env -> Problem Rational -> [(Builder, Maybe Text)]
conditions Options
opt Bool
q Env
env Problem Rational
mip = forall {a}. [(Builder, Maybe a)]
bnds forall a. [a] -> [a] -> [a]
++ [(Builder, Maybe Text)]
cs forall a. [a] -> [a] -> [a]
++ [(Builder, Maybe Text)]
ss
  where
    vs :: Set Var
vs = forall c. Problem c -> Set Var
MIP.variables Problem Rational
mip
    bnds :: [(Builder, Maybe a)]
bnds = forall a b. (a -> b) -> [a] -> [b]
map forall {a}. Var -> (Builder, Maybe a)
bnd (forall a. Set a -> [a]
Set.toList Set Var
vs)
    bnd :: Var -> (Builder, Maybe a)
bnd Var
v = (Builder
c1, forall a. Maybe a
Nothing)
      where
        v2 :: Text
v2 = Env
env forall k a. Ord k => Map k a -> k -> a
Map.! Var
v
        (BoundExpr Rational
lb,BoundExpr Rational
ub) = forall c. Num c => Problem c -> Var -> Bounds c
MIP.getBounds Problem Rational
mip Var
v

        c0 :: Builder
c0 =
          case Options -> Language
optLanguage Options
opt of
            -- In SMT-LIB2 format, inequalities can be chained.
            -- For example, "(<= 0 x 10)" is equivalent to "(and (<= 0 x) (<= x 10))".
            --
            -- Supported solvers: cvc4-1.1, yices-2.2.1, z3-4.3.0
            -- Unsupported solvers: z3-4.0
            Language
SMTLIB2
              | BoundExpr Rational
lb forall a. Eq a => a -> a -> Bool
== forall r. Extended r
MIP.PosInf Bool -> Bool -> Bool
|| BoundExpr Rational
ub forall a. Eq a => a -> a -> Bool
== forall r. Extended r
MIP.NegInf -> Builder
"false"
              | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Builder]
args forall a. Ord a => a -> a -> Bool
>= Int
2 -> [Builder] -> Builder
list (Builder
"<=" forall a. a -> [a] -> [a]
: [Builder]
args)
              | Bool
otherwise -> Builder
"true"
                  where
                    args :: [Builder]
args = [Builder]
lb2 forall a. [a] -> [a] -> [a]
++ [Text -> Builder
B.fromText Text
v2] forall a. [a] -> [a] -> [a]
++ [Builder]
ub2
                    lb2 :: [Builder]
lb2 = case BoundExpr Rational
lb of
                            BoundExpr Rational
MIP.NegInf -> []
                            BoundExpr Rational
MIP.PosInf -> forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
                            MIP.Finite Rational
x
                              | Problem Rational -> Var -> Bool
isInt Problem Rational
mip Var
v -> [Options -> Integer -> Builder
intNum Options
opt (forall a b. (RealFrac a, Integral b) => a -> b
ceiling Rational
x)]
                              | Bool
otherwise -> [Options -> Rational -> Builder
realNum Options
opt Rational
x]
                    ub2 :: [Builder]
ub2 = case BoundExpr Rational
ub of
                            BoundExpr Rational
MIP.NegInf -> forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
                            BoundExpr Rational
MIP.PosInf -> []
                            MIP.Finite Rational
x
                              | Problem Rational -> Var -> Bool
isInt Problem Rational
mip Var
v -> [Options -> Integer -> Builder
intNum Options
opt (forall a b. (RealFrac a, Integral b) => a -> b
floor Rational
x)]
                              | Bool
otherwise -> [Options -> Rational -> Builder
realNum Options
opt Rational
x]
            YICES YicesVersion
_ -> [Builder] -> Builder
and' ([Builder]
s1 forall a. [a] -> [a] -> [a]
++ [Builder]
s2)
              where
                s1 :: [Builder]
s1 = case BoundExpr Rational
lb of
                       BoundExpr Rational
MIP.NegInf -> []
                       BoundExpr Rational
MIP.PosInf -> [Builder
"false"]
                       MIP.Finite Rational
x ->
                         if Problem Rational -> Var -> Bool
isInt Problem Rational
mip Var
v
                         then [[Builder] -> Builder
list [Builder
"<=", Options -> Integer -> Builder
intNum Options
opt (forall a b. (RealFrac a, Integral b) => a -> b
ceiling Rational
x), Text -> Builder
B.fromText Text
v2]]
                         else [[Builder] -> Builder
list [Builder
"<=", Options -> Rational -> Builder
realNum Options
opt Rational
x, Text -> Builder
B.fromText Text
v2]]
                s2 :: [Builder]
s2 = case BoundExpr Rational
ub of
                       BoundExpr Rational
MIP.NegInf -> [Builder
"false"]
                       BoundExpr Rational
MIP.PosInf -> []
                       MIP.Finite Rational
x ->
                         if Problem Rational -> Var -> Bool
isInt Problem Rational
mip Var
v
                         then [[Builder] -> Builder
list [Builder
"<=", Text -> Builder
B.fromText Text
v2, Options -> Integer -> Builder
intNum Options
opt (forall a b. (RealFrac a, Integral b) => a -> b
floor Rational
x)]]
                         else [[Builder] -> Builder
list [Builder
"<=", Text -> Builder
B.fromText Text
v2, Options -> Rational -> Builder
realNum Options
opt Rational
x]]

        c1 :: Builder
c1 = case forall c. Problem c -> Var -> VarType
MIP.getVarType Problem Rational
mip Var
v of
               VarType
MIP.SemiContinuousVariable ->
                 [Builder] -> Builder
or' [[Builder] -> Builder
list [Builder
"=", Text -> Builder
B.fromText Text
v2, Options -> Rational -> Builder
realNum Options
opt Rational
0], Builder
c0]
               VarType
MIP.SemiIntegerVariable ->
                 [Builder] -> Builder
or' [[Builder] -> Builder
list [Builder
"=", Text -> Builder
B.fromText Text
v2, Options -> Integer -> Builder
intNum Options
opt Integer
0], Builder
c0]
               VarType
_ ->
                 Builder
c0

    cs :: [(Builder, Maybe Text)]
cs = forall a b. (a -> b) -> [a] -> [b]
map (Options
-> Bool
-> Env
-> Problem Rational
-> Constraint Rational
-> (Builder, Maybe Text)
constraint Options
opt Bool
q Env
env Problem Rational
mip) (forall c. Problem c -> [Constraint c]
MIP.constraints Problem Rational
mip)
    ss :: [(Builder, Maybe Text)]
ss = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a}. Ord a => SOSConstraint a -> [(Builder, Maybe Text)]
sos (forall c. Problem c -> [SOSConstraint c]
MIP.sosConstraints Problem Rational
mip)
    sos :: SOSConstraint a -> [(Builder, Maybe Text)]
sos (MIP.SOSConstraint Maybe Text
label SOSType
typ [(Var, a)]
xs) = do
      (Var
x1,Var
x2) <- case SOSType
typ of
                    SOSType
MIP.S1 -> forall a. [a] -> [(a, a)]
pairs forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Var, a)]
xs
                    SOSType
MIP.S2 -> forall a. [a] -> [(a, a)]
nonAdjacentPairs forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ [(Var, a)]
xs
      let c :: Builder
c = Builder -> Builder
not' forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
and'
            [ [Builder] -> Builder
list [Builder
"/=", Builder
v3, Options -> Rational -> Builder
realNum Options
opt Rational
0]
            | Var
v<-[Var
x1,Var
x2]
            , let v2 :: Text
v2 = Env
env forall k a. Ord k => Map k a -> k -> a
Map.! Var
v
            , let v3 :: Builder
v3 = if Problem Rational -> Var -> Bool
isInt Problem Rational
mip Var
v
                       then Options -> Builder -> Builder
toReal Options
opt (Text -> Builder
B.fromText Text
v2)
                       else Text -> Builder
B.fromText Text
v2
            ]
      forall (m :: * -> *) a. Monad m => a -> m a
return (Builder
c, Maybe Text
label)

pairs :: [a] -> [(a,a)]
pairs :: forall a. [a] -> [(a, a)]
pairs [] = []
pairs (a
x:[a]
xs) = [(a
x,a
x2) | a
x2 <- [a]
xs] forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [(a, a)]
pairs [a]
xs

nonAdjacentPairs :: [a] -> [(a,a)]
nonAdjacentPairs :: forall a. [a] -> [(a, a)]
nonAdjacentPairs (a
x1:a
x2:[a]
xs) = [(a
x1,a
x3) | a
x3 <- [a]
xs] forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [(a, a)]
nonAdjacentPairs (a
x2forall a. a -> [a] -> [a]
:[a]
xs)
nonAdjacentPairs [a]
_ = []

mip2smt :: Options -> MIP.Problem Rational -> Builder
mip2smt :: Options -> Problem Rational -> Builder
mip2smt Options
opt Problem Rational
mip =
  forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Semigroup a => a -> a -> a
<> Char -> Builder
B.singleton Char
'\n') forall a b. (a -> b) -> a -> b
$
    [Builder]
options forall a. [a] -> [a] -> [a]
++ [Builder]
set_logic forall a. [a] -> [a] -> [a]
++ [Builder]
defs forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (Options -> (Builder, Maybe Text) -> Builder
assert Options
opt) (Options
-> Bool -> Env -> Problem Rational -> [(Builder, Maybe Text)]
conditions Options
opt Bool
False Env
env Problem Rational
mip)
    forall a. [a] -> [a] -> [a]
++ [ Options -> (Builder, Maybe Text) -> Builder
assert Options
opt (Builder
optimality, forall a. Maybe a
Nothing) | Options -> Bool
optOptimize Options
opt ]
    forall a. [a] -> [a] -> [a]
++ [ case Options -> Language
optLanguage Options
opt of
           Language
SMTLIB2 -> [Builder] -> Builder
list [Builder
"check-sat"]
           YICES YicesVersion
_ -> [Builder] -> Builder
list [Builder
"check"]
       | Options -> Bool
optCheckSAT Options
opt ]
  where
    vs :: Set Var
vs = forall c. Problem c -> Set Var
MIP.variables Problem Rational
mip
    real_vs :: Set Var
real_vs = Set Var
vs forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set Var
int_vs
    int_vs :: Set Var
int_vs = forall c. Problem c -> Set Var
MIP.integerVariables Problem Rational
mip forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall c. Problem c -> Set Var
MIP.semiIntegerVariables Problem Rational
mip
    realType :: [Char]
realType =
      case Options -> Language
optLanguage Options
opt of
        Language
SMTLIB2 -> [Char]
"Real"
        YICES YicesVersion
_ -> [Char]
"real"
    intType :: [Char]
intType  =
      case Options -> Language
optLanguage Options
opt of
        Language
SMTLIB2 -> [Char]
"Int"
        YICES YicesVersion
_ -> [Char]
"int"
    ts :: [(Var, [Char])]
ts = [(Var
v, [Char]
realType) | Var
v <- forall a. Set a -> [a]
Set.toList Set Var
real_vs] forall a. [a] -> [a] -> [a]
++ [(Var
v, [Char]
intType) | Var
v <- forall a. Set a -> [a]
Set.toList Set Var
int_vs]
    obj :: ObjectiveFunction Rational
obj = forall c. Problem c -> ObjectiveFunction c
MIP.objectiveFunction Problem Rational
mip
    env :: Env
env = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var
v, Options -> Text -> Text
encode Options
opt (forall t. Uninternable t => t -> Uninterned t
unintern Var
v)) | Var
v <- forall a. Set a -> [a]
Set.toList Set Var
vs]
    -- Note that identifiers of LPFile does not contain '-'.
    -- So that there are no name crash.
    env2 :: Env
env2 = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var
v, Options -> Text -> Text
encode Options
opt (forall t. Uninternable t => t -> Uninterned t
unintern Var
v forall a. Semigroup a => a -> a -> a
<> Text
"-2")) | Var
v <- forall a. Set a -> [a]
Set.toList Set Var
vs]

    options :: [Builder]
options =
      [ case Options -> Language
optLanguage Options
opt of
          Language
SMTLIB2 -> [Builder] -> Builder
list [Builder
"set-option", Builder
":produce-models", Builder
"true"]
          YICES YicesVersion
_ -> [Builder] -> Builder
list [Builder
"set-evidence!", Builder
"true"]
      | Options -> Bool
optProduceModel Options
opt Bool -> Bool -> Bool
&& Options -> Language
optLanguage Options
opt forall a. Eq a => a -> a -> Bool
/= YicesVersion -> Language
YICES YicesVersion
Yices2
      ]

    set_logic :: [Builder]
set_logic =
      case Options -> Maybe [Char]
optSetLogic Options
opt of
        Just [Char]
logic | Options -> Language
optLanguage Options
opt forall a. Eq a => a -> a -> Bool
== Language
SMTLIB2 -> [[Builder] -> Builder
list [Builder
"set-logic", [Char] -> Builder
B.fromString [Char]
logic]]
        Maybe [Char]
_ -> []

    defs :: [Builder]
defs = do
      (Var
v,[Char]
t) <- [(Var, [Char])]
ts
      let v2 :: Text
v2 = Env
env forall k a. Ord k => Map k a -> k -> a
Map.! Var
v
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
        case Options -> Language
optLanguage Options
opt of
          Language
SMTLIB2 -> Builder
"(declare-fun " forall a. Semigroup a => a -> a -> a
<> Text -> Builder
B.fromText Text
v2 forall a. Semigroup a => a -> a -> a
<> Builder
" () " forall a. Semigroup a => a -> a -> a
<> [Char] -> Builder
B.fromString [Char]
t forall a. Semigroup a => a -> a -> a
<> Builder
")"
          YICES YicesVersion
_ -> Builder
"(define " forall a. Semigroup a => a -> a -> a
<> Text -> Builder
B.fromText Text
v2 forall a. Semigroup a => a -> a -> a
<> Builder
"::" forall a. Semigroup a => a -> a -> a
<> [Char] -> Builder
B.fromString [Char]
t forall a. Semigroup a => a -> a -> a
<> Builder
") ; " forall a. Semigroup a => a -> a -> a
<> [Char] -> Builder
B.fromString  (Var -> [Char]
MIP.fromVar Var
v)

    optimality :: Builder
optimality = [Builder] -> Builder
list [Builder
"forall", Builder
decl, Builder
body]
      where
        decl :: Builder
decl =
          case Options -> Language
optLanguage Options
opt of
            Language
SMTLIB2 -> [Builder] -> Builder
list [[Builder] -> Builder
list [Text -> Builder
B.fromText (Env
env2 forall k a. Ord k => Map k a -> k -> a
Map.! Var
v), [Char] -> Builder
B.fromString [Char]
t] | (Var
v,[Char]
t) <- [(Var, [Char])]
ts]
            YICES YicesVersion
_ -> [Builder] -> Builder
list [Text -> Builder
B.fromText (Env
env2 forall k a. Ord k => Map k a -> k -> a
Map.! Var
v) forall a. Semigroup a => a -> a -> a
<> Builder
"::" forall a. Semigroup a => a -> a -> a
<> [Char] -> Builder
B.fromString [Char]
t | (Var
v,[Char]
t) <- [(Var, [Char])]
ts]
        body :: Builder
body = [Builder] -> Builder
list [Builder
"=>"
                    , [Builder] -> Builder
and' (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (Options
-> Bool -> Env -> Problem Rational -> [(Builder, Maybe Text)]
conditions Options
opt Bool
True Env
env2 Problem Rational
mip))
                    , [Builder] -> Builder
list [ if forall c. ObjectiveFunction c -> OptDir
MIP.objDir ObjectiveFunction Rational
obj forall a. Eq a => a -> a -> Bool
== OptDir
MIP.OptMin then Builder
"<=" else Builder
">="
                           , Options -> Env -> Problem Rational -> Expr Rational -> Builder
realExpr Options
opt Env
env Problem Rational
mip (forall c. ObjectiveFunction c -> Expr c
MIP.objExpr ObjectiveFunction Rational
obj), Options -> Env -> Problem Rational -> Expr Rational -> Builder
realExpr Options
opt Env
env2 Problem Rational
mip (forall c. ObjectiveFunction c -> Expr c
MIP.objExpr ObjectiveFunction Rational
obj)
                           ]
                    ]

encode :: Options -> T.Text -> T.Text
encode :: Options -> Text -> Text
encode Options
opt Text
s =
  case Options -> Language
optLanguage Options
opt of
    Language
SMTLIB2
     | (Char -> Bool) -> Text -> Bool
T.all Char -> Bool
p Text
s   -> Text
s
     | (Char -> Bool) -> Text -> Bool
T.any Char -> Bool
q Text
s   -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"cannot encode " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Text
s
     | Bool
otherwise -> Text
"|" forall a. Semigroup a => a -> a -> a
<> Text
s forall a. Semigroup a => a -> a -> a
<> Text
"|"
    YICES YicesVersion
_ -> (Char -> Text) -> Text -> Text
T.concatMap Char -> Text
f Text
s
  where
    p :: Char -> Bool
p Char
c = Char -> Bool
isAscii Char
c Bool -> Bool -> Bool
&& (Char -> Bool
isAlpha Char
c Bool -> Bool -> Bool
|| Char -> Bool
isDigit Char
c Bool -> Bool -> Bool
|| Char
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([Char]
"~!@$%^&*_-+=<>.?/" :: [Char]))
    q :: Char -> Bool
q Char
c = Char
c forall a. Eq a => a -> a -> Bool
== Char
'|' Bool -> Bool -> Bool
&& Char
c forall a. Eq a => a -> a -> Bool
== Char
'\\'

    -- Note that '[', ']', '\\' does not appear in identifiers of LP file.
    f :: Char -> Text
f Char
'(' = Text
"["
    f Char
')' = Text
"]"
    f Char
c | Char
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([Char]
"/\";" :: [Char]) = [Char] -> Text
T.pack forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => [Char] -> r
printf [Char]
"\\x%02d" (forall a. Enum a => a -> Int
fromEnum Char
c :: Int)
    f Char
c = Char -> Text
T.singleton Char
c

isInt :: MIP.Problem Rational -> MIP.Var -> Bool
isInt :: Problem Rational -> Var -> Bool
isInt Problem Rational
mip Var
v = VarType
vt forall a. Eq a => a -> a -> Bool
== VarType
MIP.IntegerVariable Bool -> Bool -> Bool
|| VarType
vt forall a. Eq a => a -> a -> Bool
== VarType
MIP.SemiIntegerVariable
  where
    vt :: VarType
vt = forall c. Problem c -> Var -> VarType
MIP.getVarType Problem Rational
mip Var
v

-- ------------------------------------------------------------------------

_testFile :: FilePath -> IO ()
_testFile :: [Char] -> IO ()
_testFile [Char]
fname = do
  Problem Scientific
mip <- FileOptions -> [Char] -> IO (Problem Scientific)
MIP.readLPFile forall a. Default a => a
def [Char]
fname
  Text -> IO ()
TLIO.putStrLn forall a b. (a -> b) -> a -> b
$ Builder -> Text
B.toLazyText forall a b. (a -> b) -> a -> b
$ Options -> Problem Rational -> Builder
mip2smt forall a. Default a => a
def (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Real a => a -> Rational
toRational Problem Scientific
mip)

_test :: IO ()
_test :: IO ()
_test = Text -> IO ()
TLIO.putStrLn forall a b. (a -> b) -> a -> b
$ Builder -> Text
B.toLazyText forall a b. (a -> b) -> a -> b
$ Options -> Problem Rational -> Builder
mip2smt forall a. Default a => a
def Problem Rational
_testdata

_testdata :: MIP.Problem Rational
Right Problem Rational
_testdata = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Real a => a -> Rational
toRational) forall a b. (a -> b) -> a -> b
$ forall s.
(Stream s, Token s ~ Char, IsString (Tokens s)) =>
FileOptions
-> [Char] -> s -> Either (ParseError s) (Problem Scientific)
MIP.parseLPString forall a. Default a => a
def [Char]
"test" forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
  [ [Char]
"Maximize"
  , [Char]
" obj: x1 + 2 x2 + 3 x3 + x4"
  , [Char]
"Subject To"
  , [Char]
" c1: - x1 + x2 + x3 + 10 x4 <= 20"
  , [Char]
" c2: x1 - 3 x2 + x3 <= 30"
  , [Char]
" c3: x2 - 3.5 x4 = 0"
  , [Char]
"Bounds"
  , [Char]
" 0 <= x1 <= 40"
  , [Char]
" 2 <= x4 <= 3"
  , [Char]
"General"
  , [Char]
" x4"
  , [Char]
"End"
  ]