how to describe SMT problems?

EndlessSky.hs

module Main where

import           Data.SBV

-- main :: IO ()
main = do
  res <- optimize Lexicographic $ do
           -- create two piles of bools, each pile has a bool for each possible component
           -- x1@[x11, x12, x13] <- sBools ["x11", "x12", "x13"]
           -- map the costs onto the bools?!

           maximize "sum thrust and steering" (thrust + steering :: SInteger)

engineSpace :: SInteger
engineSpace = 100 -- max space

minTurn :: SInteger
minTurn = 60 -- random guess?

getThrust (_,_,th,_) = th
getTurn (_,_,_,tu) = tu
getSize (_,s,_,_) = s


{- many engines, with different amounts of thrust and turning
a ship has limited space
What combination of engines fits into the ship, and gives the most thrust? -}

-- values from https://github.com/endless-sky/endless-sky/blob/master/data/engines.txt
-- name, size, thrust, turning
engines :: [(String, SInteger, SFloat, SFloat)]
engines = [ ("X1050", 20, 4.0, 110) -- has both thrust and turning!
          , ("X1200", 12, 0, 160)
          , ("X1700", 16, 6.0, 0)
          , ("X2200", 20, 0, 307)
          , ("X2700", 27, 11.5, 0)
          , ("X3200", 35, 0, 590)
          , ("X3700", 46, 22.1, 0)
          , ("X4200", 59, 0, 1132)
          , ("X4700", 79, 42.5, 0)
          , ("X5200", 100, 0, 2174)
          , ("X5700", 134, 81.5, 0)
          , ("Chipmunk Thruster", 20, 9.6, 0)
          , ("Chipmunk Steering", 15, 0, 256)
          , ("Greyhound Steering", 26, 0, 492)
          , ("Greyhound Thruster", 34, 18.4, 0)
          , ("Impala Steering", 43, 0, 944)
          , ("Impala Thruster", 58, 35.4, 0)
          , ("Orca Steering", 74, 0, 1812)
          , ("Orca Thruster", 98, 67.9, 0)
          , ("Tyrant Steering", 125, 0, 3479)
          , ("Tyrant Thruster", 167, 130.5, 0)
          , ("A120 Thruster", 22, 15.4, 0)
          , ("A125 Steering", 16, 0, 392)
          , ("A250 Thruster", 34, 27.3, 0)
          , ("A255 Steering", 25, 0, 687)
          , ("A370 Thruster", 53, 47.6, 0)
          , ("A375 Steering", 38, 0, 1192)
          , ("A520 Thruster", 82, 81.9, 0)
          , ("A525 Steering", 60, 0, 2050)
          , ("A860 Thruster", 127, 139.7, 0)
          , ("A865 Steering", 92, 0, 3509)
          , ("Baellie", 24, 10.1, 250) -- hai
          , ("Basrem Thruster", 18, 13.2, 0)
          , ("Benga Thruster", 28, 23.6, 0)
          , ("Biroo Thruster", 44, 41.5, 0)
          , ("Bondir Thruster", 63, 66.1, 0)
          , ("Bufaer Thruster", 104, 120.1, 0)
          , ("Basrem Steering", 12, 0, 309)
          , ("Benga Steering", 20, 0, 577)
          , ("Biroo Steering", 32, 0, 1054)
          , ("Bondir Steering", 49, 0, 1758)
          , ("Bufaer Steering", 76, 0, 3043)
          , ("Coalition Large Steering", 25, 0, 711.9) -- coalition
          , ("Coalition Large Thruster", 32, 26.2, 0)
          , ("Coalition Small Steering", 7, 0, 178.8)
          , ("Coalition Small Thruster", 9, 6.6, 0)
          , ("Korath Asteroid Steering", 10, 0, 280) -- Korath
          , ("Korath Asteroid Thruster", 14, 11.2, 0)
          , ("Korath Comet Steering", 18, 0, 568.8)
          , ("Korath Comet Thruster", 24, 21.8, 0)
          , ("Korath Lunar Steering", 30, 0, 1056)
          , ("Korath Lunar Thruster", 40, 41.2, 0)
          , ("Korath Planetary Steering", 52, 0, 2069.6)
          , ("Korath Planetary Thruster", 69, 80.0, 0)
          , ("Korath Stellar Steering", 89, 0, 4005)
          , ("Korath Stellar Thruster", 118, 153.4, 0)
          ]



{- start with "one engine that gives the most thrust" -}