You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
zahariel:df: 12:13 AM
pretty neat! you didn't use it to make a solver for rage of the quebecats? Grid is really brilliant but i feel like a useful extension would be an ability to pass generators for the val of the various parts, in case Int isn't good enough
mrwright 12:14 AM
I wrote a solver in Rust for Quebecats, and I've been trying to think of whether there's a nice way to do one in z3, but I haven't come up with any ideas I think would work.
zahariel:df: 12:14 AM
i mean Int is probably a good default most of the time, but i can certainly imagine situations in which something else would be useful
still, just that class is pretty useful, it covers most of the things you would need
mrwright 12:15 AM
The Int parts are being passed to z3's solver, so the possible types there are limited to ones z3 already knows about.
Though, yeah, being able to specify the variable type in a grid seems like it might be useful.
zahariel:df: 12:16 AM
well, only in that you're adding them directly to the solver in the various puzzle-specific things
you could just as easily say "hey, pass any function that takes a string and returns something; you're on your honor to know what it returns"
mrwright 12:17 AM
(Which in practice means, sometimes people might want the bit vector type instead of int, I guess...)
zahariel:df: 12:17 AM
and then when coding up the restrictions, you know the format of the val in each thing
mrwright 12:18 AM
Ah--so you mean, I could make a class that might include, say, multiple z3 variables or something.
zahariel:df: 12:18 AM
right
or just an ad-hoc hash or something
mrwright 12:18 AM
Yeah!
zahariel:df: 12:19 AM
but yeah Int is probably a safe choice most of the time
mrwright 12:19 AM
(There was one puzzle type I've done so far where that could have been useful, skyscrapers. Instead I ended up creating multiple grids, but it probably would have been somewhat cleaner with a single grid of more interesting structures.)
zahariel:df: 12:19 AM
oh i didn't even look!
mrwright 12:20 AM
I was only using the other grids as a convenient way to get more variables in each cell.
zahariel:df: 12:20 AM
but seriously grids are so common that just having an object that makes a grid with cells/edges/points all pre-linked-up is super useful
The text was updated successfully, but these errors were encountered:
zahariel:df: 12:13 AM
pretty neat! you didn't use it to make a solver for rage of the quebecats? Grid is really brilliant but i feel like a useful extension would be an ability to pass generators for the val of the various parts, in case Int isn't good enough
mrwright 12:14 AM
I wrote a solver in Rust for Quebecats, and I've been trying to think of whether there's a nice way to do one in z3, but I haven't come up with any ideas I think would work.
zahariel:df: 12:14 AM
i mean Int is probably a good default most of the time, but i can certainly imagine situations in which something else would be useful
still, just that class is pretty useful, it covers most of the things you would need
mrwright 12:15 AM
The Int parts are being passed to z3's solver, so the possible types there are limited to ones z3 already knows about.
Though, yeah, being able to specify the variable type in a grid seems like it might be useful.
zahariel:df: 12:16 AM
well, only in that you're adding them directly to the solver in the various puzzle-specific things
you could just as easily say "hey, pass any function that takes a string and returns something; you're on your honor to know what it returns"
mrwright 12:17 AM
(Which in practice means, sometimes people might want the bit vector type instead of int, I guess...)
zahariel:df: 12:17 AM
and then when coding up the restrictions, you know the format of the val in each thing
mrwright 12:18 AM
Ah--so you mean, I could make a class that might include, say, multiple z3 variables or something.
zahariel:df: 12:18 AM
right
or just an ad-hoc hash or something
mrwright 12:18 AM
Yeah!
zahariel:df: 12:19 AM
but yeah Int is probably a safe choice most of the time
mrwright 12:19 AM
(There was one puzzle type I've done so far where that could have been useful, skyscrapers. Instead I ended up creating multiple grids, but it probably would have been somewhat cleaner with a single grid of more interesting structures.)
zahariel:df: 12:19 AM
oh i didn't even look!
mrwright 12:20 AM
I was only using the other grids as a convenient way to get more variables in each cell.
zahariel:df: 12:20 AM
but seriously grids are so common that just having an object that makes a grid with cells/edges/points all pre-linked-up is super useful
The text was updated successfully, but these errors were encountered: