Skip to content

Instantly share code, notes, and snippets.

@LeventErkok
Created April 25, 2019 04:34
Show Gist options
  • Save LeventErkok/20f1eeb1505b0ff6e8569b9108405a57 to your computer and use it in GitHub Desktop.
Save LeventErkok/20f1eeb1505b0ff6e8569b9108405a57 to your computer and use it in GitHub Desktop.
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ScopedTypeVariables #-}
import Data.SBV
import Data.SBV.Char
import Data.SBV.Tuple
import Data.SBV.Control
import Data.Generics
import Data.SBV.Either
import qualified Data.SBV.List as L
-- Term type; the deriving clause is just so SBV can treat it
-- as a symbolic value; there is no other meaning to it.
-- Note that Tm cannot really be recursive.
data Tm = TmSLF String [Float]
| TmInt Integer
| TmBool Bool
deriving (Show, HasKind, Read, SymVal, Data, SMTValue)
-- The underlying symbolic representation as an SMTLib level symbolic value
type STm = SEither (String, [Float])
(Either Integer Bool)
-- Extract a symbolic value in a more recognizable form
queryTm :: STm -> Query Tm
queryTm v = do sv <- getValue v
case sv of
Left (s, fs) -> return $ TmSLF s fs
(Right (Left i)) -> return $ TmInt i
(Right (Right b)) -> return $ TmBool b
-- Since we don't have case splits, we have to define recognizers ourselves.
isTmSLF :: STm -> SBool
isTmSLF = isLeft
tmSLF :: STm -> STuple String [Float]
tmSLF = fromLeft
-- Same as above
isTmTFloat :: STm -> SBool
isTmTFloat x = isRight x .&& isLeft (fromRight x)
tmInt :: STm -> SInteger
tmInt = fromLeft . fromRight
-- Same as above
isTmBool :: STm -> SBool
isTmBool x = isRight x .&& isRight (fromRight x)
tmBool :: STm -> SBool
tmBool = fromRight . fromRight
-- A very simple example
ex :: Symbolic Tm
ex = do x :: STm <- free "x"
-- enforce a certain shape
constrain $ isTmSLF x
constrain $ L.length ((tmSLF x)^._2) .> 2
-- make sure the first element in the list is a float that is at least 10
-- and the string is hello world..
let elts :: SList Float
elts = (tmSLF x)^._2
telt :: SFloat
telt = elts L..!! 0
-- We have to say that there are at least 1 elements, the first is an integer, and it's > 10
-- This is clunky, but is the only way without pattern matching
constrain $ (tmSLF x)^._1 .== "hello world"
constrain $ L.length elts .>= 1
constrain $ telt .>= 10
-- grab the result
query $ do ensureSat
queryTm x
-- *Main> test
-- TmSLF "hello world" [24.001955,NaN,1.469368e-39]
test :: IO Tm
test = runSMT ex
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment