Documentation.SBV.Examples.Puzzles.AOC_2021_24

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.

Registers, values, and the ALU

type Register = String

A Register in the machine, identified by its name.

type Value = SInt64

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

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

Constructors

Reg

Fields

• register :: Register

Imm Int64

Instances

Num Data

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.

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

Shorthand for the w register.

x :: Data

Shorthand for the x register.

y :: Data

Shorthand for the y register.

z :: Data

Shorthand for the z register.

data State

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

Constructors

State

Fields

• env :: Map Register Value

  Values of registers

• inputs :: [Value]

  Input parameters, stored in reverse.

type ALU = StateT State Symbolic

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

Operations

read :: Data -> ALU Value

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

Writing a value. We update the registers.

inp :: Data -> ALU ()

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

Addition.

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

Multiplication.

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

Division.

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

Modulus.

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

Equality.

Running a program

run :: ALU () -> Symbolic State

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

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

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