Skip to content

Instantly share code, notes, and snippets.

View DoublePermsSum.hs
-- A Haskell based SMT solution attempt to:
-- https://stackoverflow.com/questions/69192991/how-many-different-sums-can-we-get-from-very-few-floats
import Data.List
import Control.Monad
import Data.SBV
-- Make a permutation from 0 to k-1
mkPerm :: Word8 -> Word8 -> Symbolic [SWord8]
View dt.hs
{-# 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
View gist:e08a65ac190da3ba88a2989a146a407e
(set-logic ALL)
(declare-fun v1 () Int)
(declare-fun v2 () Int)
(declare-fun v3 () Int)
(assert (distinct v1 v2))
(assert (>= 10 v1 0))
(assert (>= 10 v2 0))
(assert (>= 10 v3 0))
View DumpBounds.hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
import Data.SBV
import Data.Proxy
import Numeric
import Data.List
View PathCond.hs
import Data.SBV
import Data.SBV.Dynamic
import Data.SBV.Control
import Data.SBV.Internals
import Control.Monad.Reader (ask)
reachableCond :: SVal -> Symbolic SVal
reachableCond cond = do
st <- ask
@LeventErkok
LeventErkok / Garden.hs
Last active Mar 22, 2021
To Mock a Mockingbird puzzle in Haskell/SBV
View Garden.hs
-- A Haskell solution to:
--
-- https://stackoverflow.com/questions/53711168/modelling-a-logic-puzzle
--
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveAnyClass #-}
View IntX.hs
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE NamedFieldPuns #-}
import Data.SBV
import Data.SBV.Control
import GHC.Generics (Generic)
data SIntX = SIntX { isInf :: SBool
, xVal :: SInteger
@LeventErkok
LeventErkok / BoundedLists.hs
Created Sep 19, 2018
Bounded symbolic lists
View BoundedLists.hs
{-# LANGUAGE OverloadedLists #-}
import Data.SBV
import Data.SBV.List ((.++), (.:))
import qualified Data.SBV.List as L
import Data.Typeable
lcase :: (Typeable a, SymWord a, Mergeable b) => SList a -> b -> (SBV a -> SList a -> b) -> b
lcase s e c = ite (L.null s) e (c (L.head s) (L.tail s))
View Ouro.hs
import Data.SBV
leftAppend :: SInteger -> SInteger -> SInteger
leftAppend k n = ite (n .< 10 ) (n + k *10)
$ ite (n .< 100 ) (n + k *100)
$ ite (n .< 1000 ) (n + k * 1000)
$ ite (n .< 10000 ) (n + k * 10000)
$ ite (n .< 100000 ) (n + k * 100000)
$ ite (n .< 1000000 ) (n + k * 1000000)
$ ite (n .< 10000000 ) (n + k * 10000000)
@LeventErkok
LeventErkok / bitvec17.hs
Created Feb 22, 2018
Using "17-bit-vectors" in SBV
View bitvec17.hs
import Control.Monad.Trans (liftIO)
import Control.Monad.Reader (ask)
import Data.SBV.Dynamic
--------------------------------------------------------------------------------
-- I should really export the following four definitions from SBV.Dynamic
mkWordN :: Int -> String -> Symbolic SVal
mkWordN w nm = ask >>= liftIO . svMkSymVar Nothing (KBounded False w) (Just nm)