2022 Day 3: Rucksack Reorganization

Advent of Code
1

Just a bit of light string manipulation today. I was surprised that there isn’t a Ada.Strings.Fixed.Index that takes a Character argument, only String or Maps.Character_Set.

advent/day3_2.adb at 42725c2a5c5446b055a5ca88d5237c3f487f7901 · JeremyGrosser/advent · GitHub

2

Right,
I had to make my own function to get the value of a Priority, based on

return Character'Pos (Item) - Character'Pos ('a') + 1;
return Character'Pos (Item) - Character'Pos ('A') + 27;

Ada.Strings.Maps could have that little function, like for ex.

function Index (Singleton : in Character;
                Set       : in Character_Set)
                return Natural;

so you could use

with Ada.Strings.Maps.;
use Ada.Strings.Maps;
Item : constant Character_Sequence :=
    "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ";
Item_Set : Character_Set := To_Set (Item);
Priority := Index ( C, Item_Set);  -- NOT in Ada.Strings.Maps
1 Like
3

I was also surprised about the missing Index function for searching a character in a string, so I briefly wrote my own

 function Index (Source : String; Pattern : Character) return Natural is
 begin
    for I in Source'Range loop
       if Source(I) = Pattern then return I; end if;
    end loop;
    return 0;
 end Index;
4

Need help with SPARK :nerd_face:

In my solution I declared an array with range 'A' .. 'z' as an index. I only use 'a' .. 'z' and 'A' .. 'Z' slices of it for actual values and other elements are initialized to an default value and never change. Any ideas how to help SPARK understand it?

To be more concrete, if I comment line 49 out gnatprove complains

day_03.adb:51:42: medium: predicate check might fail[#0]

@yannickmoy

5

You need a loop invariant in the loop at line 42 that modifies Found so that GNATprove knows that Found(J) is None for the other values. Something like:

pragma Loop_Invariant 
  (for all J not in Rucksack_Item => Found (J) = None);
1 Like
6

It was definitely a fun one, I tried doing something really weird with sets of characters this time. adventofcode/day3.adb at 36631ec28b90171803935debe34ee742efbde5c1 · AJ-Ianozi/adventofcode · GitHub

7

My naive solution : Compiler Explorer / adventofcode/main.adb at 53077dbff42a7e64de02e13e80c5d4e92af8899b · dkm/adventofcode · GitHub

8

Did you tried to transform your Character (say ‘c’) into a String ?

'c' & ""