advent-2024-13-z3-linq.cs

List<Machine> machines = [];

foreach (var machine in input.Split("\n\n"))
{
    var lines = machine.Split("\n");

    var a = Split(lines[0]);
    var b = Split(lines[1]);
    var prize = Split(lines[2]);

    static string[] Split(string s) => s.Split([' ', ',', ':', '+', '='], StringSplitOptions.RemoveEmptyEntries);

    machines.Add(new Machine
    {
        A = (int.Parse(a[3]), int.Parse(a[5])),
        B = (int.Parse(b[3]), int.Parse(b[5])),
        Prize = (int.Parse(prize[2]) + 10000000000000L, int.Parse(prize[4]) + 10000000000000L)
    });
}

long sum = 0;
foreach (var machine in machines)
{
    if (ComputePresses(machine) is (long a, long b))
    {
        sum += Cost(a, b);
    }
}

Console.WriteLine(sum);

static long Cost(long a, long b) => a * 3 + b;

static (long a, long b) ComputePresses(in Machine machine)
{
    using var context = new Z3Context();

    long a_x = machine.A.X;
    long a_y = machine.A.Y;
    long b_x = machine.B.X;
    long b_y = machine.B.Y;
    long prize_x = machine.Prize.X;
    long prize_y = machine.Prize.Y;

    var theorem = from t in context.NewTheorem<(long a, long b)>()
                  where a_x * t.a + b_x * t.b == prize_x
                  where a_y * t.a + b_y * t.b == prize_y
                  select t;
    
    return theorem.Solve();
}

struct Machine
{
    public (int X, int Y) A;
    public (int X, int Y) B;
    public (long X, long Y) Prize;
}