LeventErkok

{-# OPTIONS_GHC -Wall -Werror #-}

-- | Solve the Advent-of-code, 2021, day 24: https://adventofcode.com/2021/day/24
--
-- Load it to ghci as:
--     ghci -package mtl ALU.hs
--
-- Boolean specifies if we maximize (True) or minimize (False)
--
-- >>> puzzle True

LeventErkok

-- Solution to:
--   https://stackoverflow.com/questions/70565942/how-to-find-3-triangles-passing-through-every-dot-of-a-5x5-grid-in-z3

{-
This prints:

*Main> main
1....
11...
1.1..

LeventErkok

-- 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]

LeventErkok

{-# 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

LeventErkok

(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))

LeventErkok

{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE Rank2Types          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}

import Data.SBV
import Data.Proxy
import Numeric
import Data.List

LeventErkok

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

-- A Haskell solution to:
--
--  https://stackoverflow.com/questions/53711168/modelling-a-logic-puzzle
--

{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveAnyClass      #-}

LeventErkok

{-# 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

{-# 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))