{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE OverloadedStrings #-}
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)
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
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]
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
'\\'
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"
]