LeventErkok

{------------------------------------------------
A Haskell solution to: http://www.coinheist.com/rubik/a_regular_crossword/grid.pdf
using the Z3 SMT solver.

Z3 finds the following solution in about 7 mins
on my Mac Core-i5, and another 7 mins to prove
it's unique.

   NHPEHAS
   DIOMOMTH

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

; Automatically generated by SBV. Do not edit.
(set-option :produce-models true)
; Has unbounded values (Int/Real) or uninterpreted sorts; no logic specified.
; --- uninterpreted sorts ---
(declare-sort A 0)  ; N.B. Uninterpreted: A.A: not a nullary constructor
; --- literal constants ---
(define-fun s_2 () Bool false)
(define-fun s_1 () Bool true)
; --- skolem constants ---
(declare-fun s0 () Int) ; tracks user variable "x1"

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

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

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

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

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

(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