SNatX.hs

#!/usr/bin/env stack
{- stack script
  --resolver nightly-2018-11-23
  --package sbv
-}

{-# LANGUAGE DeriveAnyClass  #-}
{-# LANGUAGE DeriveGeneric   #-}
{-# LANGUAGE BlockArguments  #-}

import Control.Monad ((<=<))
import Data.SBV
import Data.SBV.Control
import GHC.Generics (Generic)

newtype SNatX = SNatX { xVal  :: SInteger }
  deriving (Generic, Mergeable)

instance Show SNatX where
  show (SNatX val) = case unliteral val of
    Just (-1) -> "∞"
    Just n    -> show n
    _         -> "<symbolic>"

inf :: SNatX
inf = SNatX (-1)

isInf :: SNatX -> SBool
isInf (SNatX n) = n .== -1

instance Num SNatX where
  x + y = ite (isInf x ||| isInf y)
              inf
              (SNatX (xVal x + xVal y))
  x * y = ite ((isInf x &&& y ./= 0) ||| (isInf y &&& x ./= 0)) -- 0 * ∞ = ∞ * 0 = 0
              inf
              (SNatX (xVal x * xVal y))
  fromInteger = SNatX . literal

instance EqSymbolic SNatX where
  (SNatX a) .== (SNatX b) = a .== b

instance OrdSymbolic SNatX where
  a .< b = ite (isInf a) false
         $ ite (isInf b) true
         $ xVal a .< xVal b

freeSNatX :: String -> Symbolic SNatX
freeSNatX nm = do
  v <- sInteger $ nm <> "_xVal"
  constrain $ v .>= -1
  return $ SNatX v

main :: IO ()
main = print =<< sat do
  [x, y, z] <- mapM freeSNatX ["x", "y", "z"]
  return $ bAnd
    [ x .== x+1 -- x = ∞
    , x .== x*y -- y ≠ 0
    , y .< x    -- y ≠ ∞
    , z*x .== 0 -- z = 0
    ]