sbv-9.0: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.Puzzles.AOC_2021_24

Description

A solution to the advent-of-code problem, 2021, day 24: http://adventofcode.com/2021/day/24.

Here is a high-level summary: We are essentially modeling the ALU of a fictional computer with 4 integer registers (w, x, y, z), and 6 instructions (inp, add, mul, div, mod, eql). You are given a program (hilariously called "monad"), and your goal is to figure out what the maximum and minimum inputs you can provide to this program such that when it runs register z ends up with the value 1. Please refer to the above link for the full description.

While there are multiple ways to solve this problem in SBV, the solution here demonstrates how to turn programs in this fictional language into actual Haskell/SBV programs, i.e., developing a little EDSL (embedded domain-specific language) for it. Hopefully this should provide a template for other similar programs.

Synopsis

Registers, values, and the ALU

type Register = String Source #

A Register in the machine, identified by its name.

type Value = SInt64 Source #

We operate on 64-bit signed integers. It is also possible to use the unbounded integers here as the problem description doesn't mention any size limitations. But performance isn't as good with unbounded integers, and 64-bit signed bit-vectors seem to fit the bill just fine, much like any other modern processor these days.

data Data Source #

An item of data to be processed. We can either be referring to a named register, or an immediate value.

Constructors

Reg 

Fields

Imm Int64 

Instances

Instances details
Num Data Source #

Num instance for Data. This is merely there for us to be able to represent programs in a natural way, i.e, lifting integers (positive and negative). Other methods are neither implemented nor needed.

Instance details

Defined in Documentation.SBV.Examples.Puzzles.AOC_2021_24

Methods

(+) :: Data -> Data -> Data #

(-) :: Data -> Data -> Data #

(*) :: Data -> Data -> Data #

negate :: Data -> Data #

abs :: Data -> Data #

signum :: Data -> Data #

fromInteger :: Integer -> Data #

w :: Data Source #

Shorthand for the w register.

x :: Data Source #

Shorthand for the x register.

y :: Data Source #

Shorthand for the y register.

z :: Data Source #

Shorthand for the z register.

data State Source #

The state of the machine. We keep track of the data values, along with the input parameters.

Constructors

State 

Fields

type ALU = StateT State Symbolic Source #

The ALU is simply a state transformer, manipulating the state, wrapped around SBV's Symbolic monad.

Operations

read :: Data -> ALU Value Source #

Reading a value. For a register, we simply look it up in the environment. For an immediate, we simply return it.

write :: Data -> Value -> ALU () Source #

Writing a value. We update the registers.

inp :: Data -> ALU () Source #

Reading an input value. In this version, we simply write a free symbolic value to the specified register, and keep track of the inputs explicitly.

add :: Data -> Data -> ALU () Source #

Addition.

mul :: Data -> Data -> ALU () Source #

Multiplication.

div :: Data -> Data -> ALU () Source #

Division.

mod :: Data -> Data -> ALU () Source #

Modulus.

eql :: Data -> Data -> ALU () Source #

Equality.

Running a program

run :: ALU () -> Symbolic State Source #

Run a given program, returning the final state. We simply start with the initial environment mapping all registers to zero, as specified in the problem specification.

Solving the puzzle

puzzle :: Bool -> IO () Source #

We simply run the monad program, and specify the constraints at the end. We take a boolean as a parameter, choosing whether we want to minimize or maximize the model-number. We have:

>>> puzzle True
Optimal model:
  Maximum model number = 96918996924991 :: Int64
>>> puzzle False
Optimal model:
  Minimum model number = 91811241911641 :: Int64

monad :: ALU () Source #

The program we need to crack. Note that different users get different programs on the Advent-Of-Code site, so this is simply one example. You can simply cut-and-paste your version instead. (Don't forget the pragma NegativeLiterals to GHC so add x -1 parses correctly as add x (-1).)