BV for Advent of Code Problem

[David Silverman]

I thought bit vectors might be perfect for an Advent of Code problem, but couldn't get it to work with an #/\ condition between two bv_gt items.  

Advent problem: https://adventofcode.com/2016/day/20

Here's the code: https://github.com/dsagman/advent-of-code/blob/main/2016/day20/day20.pi

And copied below.

% import sat. % sub 4 seconds for sat

import cp. % 0.15 seconds for cp, ff, split

import util.

main =>

nolog,

% Data = read_file_lines("test"),

Data = read_file_lines("day"),

Rs = [[P[1], P[2]].map(to_int) : D in Data, P=split(D,"-")],

IP :: 0..max(Rs.flatten),

% IP = new_bv(32)

foreach (R in Rs)

% (bv_gt(R[1].int_to_bv,IP) #\/ bv_gt(IP,R[2].int_to_bv)) % doesn't work

(IP #< R[1] #\/ IP #> R[2])

end,

% Sols = solve_all([$seq],IP),

Sols = solve_all([ffs,split],IP),

printf("Answer Part 1: %w\n",min(Sols)),

printf("Answer Part 2: %w\n",len(Sols)).

[Neng-Fa Zhou]

For this problem you don't need to use bv constraints, as the maximum integer allowed fits into a 32-bit word. But I agree with you that it'd be convenient to have implied and reified bv constraints for some applications. With these constraints, you can write something like:

reif_bv_gt(B1,X,Y), reif_bv(B2,U,V), B1+B2 #>= 1

Cheers,

NF