Skip to content

Commit

Permalink
2024-13
Browse files Browse the repository at this point in the history
  • Loading branch information
jurisk committed Dec 13, 2024
1 parent f3d6435 commit 790816d
Show file tree
Hide file tree
Showing 9 changed files with 62 additions and 46 deletions.
3 changes: 3 additions & 0 deletions ReadMe.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,9 @@

| Year-Day | Task | Scala | Rust | Others |
|----------|:-------------------------------------------------------------------------------|:-----------------------------------------------------------------------:|:----------------------------------------------:|:----------------------------------------------------------------------:|
| 2024-13 | [Claw Contraption](https://adventofcode.com/2024/day/13) | [Scala](scala2/src/main/scala/jurisk/adventofcode/y2024/Advent13.scala) | [Rust](rust/y2024/src/bin/solution_2024_13.rs) | |
| 2024-12 | [Garden Groups](https://adventofcode.com/2024/day/12) | [Scala](scala2/src/main/scala/jurisk/adventofcode/y2024/Advent12.scala) | [Rust](rust/y2024/src/bin/solution_2024_12.rs) | |
| 2024-11 | [Plutonian Pebbles](https://adventofcode.com/2024/day/11) | [Scala](scala2/src/main/scala/jurisk/adventofcode/y2024/Advent11.scala) | [Rust](rust/y2024/src/bin/solution_2024_11.rs) | |
| 2024-10 | [Hoof It](https://adventofcode.com/2024/day/10) | [Scala](scala2/src/main/scala/jurisk/adventofcode/y2024/Advent10.scala) | [Rust](rust/y2024/src/bin/solution_2024_10.rs) | |
| 2024-09 | [Disk Fragmenter](https://adventofcode.com/2024/day/9) | [Scala](scala2/src/main/scala/jurisk/adventofcode/y2024/Advent09.scala) | [Rust](rust/y2024/src/bin/solution_2024_09.rs) | |
| 2024-08 | [Resonant Collinearity](https://adventofcode.com/2024/day/8) | [Scala](scala2/src/main/scala/jurisk/adventofcode/y2024/Advent08.scala) | [Rust](rust/y2024/src/bin/solution_2024_08.rs) | |
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,8 @@ object Advent23 {
val _ = maximize(nanobotsInRange)
val _ = minimize(distanceFromOrigin)

val List(xc, yc, zc) = runExternal("x", "y", "z").map(resultToInt)
val List(xc, yc, zc) =
runExternal("x", "y", "z").getOrElse("Failed".fail).map(resultToInt)

val found = Coords3D(xc, yc, zc)

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,7 @@ object Advent21 {
}
}

val List(result) = runExternal(calculate)
val List(result) = runExternal(calculate).getOrElse("Failed".fail)
resultToLong(result)
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -292,7 +292,7 @@ object Advent16 {
Field2D.printCharField(debugField)
}

val List(result) = runExternal("energized")
val List(result) = runExternal("energized").getOrElse("Failed".fail)
resultToLong(result)
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -380,6 +380,7 @@ object Advent24 {

val List(pxS, pyS, pzS, vxS, vyS, vzS) = o
.runExternal("px", "py", "pz", "vx", "vy", "vz")
.getOrElse("Failed".fail)
.map(r => resultToLong(r))

val result = PositionAndVelocity3D(
Expand Down
50 changes: 24 additions & 26 deletions scala2/src/main/scala/jurisk/adventofcode/y2024/Advent13.scala
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
package jurisk.adventofcode.y2024

import cats.implicits.catsSyntaxOptionId
import jurisk.geometry.Coordinates2D
import jurisk.optimization.ImplicitConversions.{
RichArithExprIntSort,
Expand All @@ -12,43 +11,42 @@ import jurisk.utils.FileInput._
import jurisk.utils.Parsing.StringOps

import scala.annotation.nowarn
import scala.util.Try

object Advent13 {
type Input = List[Machine]
type N = Long
type C = Coordinates2D[Long]

sealed trait SolutionMode
private object SolutionMode {
object SolutionMode {
case object InternalZ3 extends SolutionMode
case object ExternalZ3 extends SolutionMode
}

private val SelectedMode: SolutionMode = SolutionMode.InternalZ3
private val CostA = 3
private val CostB = 1

final case class Machine(
buttonA: C,
buttonB: C,
prize: C,
) {
def solve: Option[N] = {
def bruteForceConstrained(limit: Int = 100): Option[N] = {
val results = for {
a <- 0L to 100
b <- 0L to 100
a <- 0L to limit
b <- 0L to limit
result = buttonA * a + buttonB * b
if result == prize
} yield 3 * a + b
} yield CostA * a + CostB * b

results.minOption
}

def solve2: Option[N] = Try {
solve2Q
}.toOption.flatten
def solve(
solutionMode: SolutionMode = SolutionMode.InternalZ3
): Option[N] = {
println(s"Solving $this")

def solve2Q: Option[N] = {
println(s"Trying to solve $this")
// a * ax + b * bx = px
// a * ay + b * by = py
// Minimize 3 * a + b
Expand All @@ -67,29 +65,29 @@ object Advent13 {
b >= Zero,
a * ax + b * bx === px,
a * ay + b * by === py,
cost === 3.constant * a + b,
cost === CostA.constant * a + CostB.constant * b,
)

val _ = minimize(cost)

val (ar, br) = SelectedMode match {
solutionMode match {
case SolutionMode.InternalZ3 =>
@nowarn("cat=deprecation")
val m = checkAndGetModel()
val ar = m.getConstInterp(a).toString
val br = m.getConstInterp(b).toString
(ar.toLong, br.toLong)
val modelResult = checkAndGetModel()
modelResult.map { m =>
m.getConstInterp(cost).toString.toLong
}

case SolutionMode.ExternalZ3 =>
val List(ar, br) = runExternal("a", "b").map(resultToLong)
(ar, br)
runExternal("cost").map { m =>
val List(cost) = m.map(resultToLong)
cost
}
}

(3 * ar + br).some
}
}

object Machine {
private object Machine {
def parse(s: String): Machine = {
def parseCoords(s: String, symbol: String): C = {
val Pattern = s"""X$symbol(\\d+), Y$symbol(\\d+)""".r
Expand All @@ -111,14 +109,14 @@ object Advent13 {
input.parseSections(Machine.parse)

def part1(data: Input): N =
data.flatMap(_.solve).sum
data.flatMap(_.bruteForceConstrained()).sum

def part2(data: Input): N = {
val adjusted = data.map(m =>
m.copy(prize = m.prize + Coordinates2D(10000000000000L, 10000000000000L))
)

adjusted.flatMap(_.solve2).sum
adjusted.flatMap(_.solve()).sum
}

def parseFile(fileName: String): Input =
Expand Down
31 changes: 19 additions & 12 deletions scala2/src/main/scala/jurisk/optimization/Optimizer.scala
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
package jurisk.optimization

import cats.implicits.catsSyntaxOptionId
import cats.implicits.{catsSyntaxOptionId, none}
import com.microsoft.z3.ArithExpr
import com.microsoft.z3.ArithSort
import com.microsoft.z3.BoolExpr
Expand All @@ -19,6 +19,7 @@ import com.microsoft.z3.Status
import com.microsoft.z3.enumerations.Z3_lbool
import jurisk.process.Runner
import jurisk.utils.Parsing.StringOps
import mouse.all.booleanSyntaxMouse
import org.scalatest.matchers.should.Matchers.convertToAnyShouldWrapper

// The https://github.com/tudo-aqua/z3-turnkey distribution did not work on task 2023-24 while the same SMT-LIB program
Expand All @@ -44,11 +45,11 @@ trait Optimizer {
def addConstraints(expressions: Expr[BoolSort]*): Unit

// Note - We were using `getConstInterp` to get the results from this
@deprecated("Use `runExternal` instead", "2023-12-24")
def checkAndGetModel(): Model
@deprecated("Prefer `runExternal` instead, as this one was glitching for some cases", "2023-12-24")
def checkAndGetModel(): Option[Model]

// TODO: Make type-safe?
def runExternal(evaluate: String*): List[String]
def runExternal(evaluate: String*): Option[List[String]]
def resultToInt(result: String): Int
def resultToLong(result: String): Long

Expand Down Expand Up @@ -164,13 +165,14 @@ private class Z3Optimizer(val context: Context, val optimize: Optimize)
def addConstraints(constraints: Expr[BoolSort]*): Unit =
optimize.Add(constraints: _*)

def checkAndGetModel(): Model = {
def checkAndGetModel(): Option[Model] = {
val status = optimize.Check()
assert(status == Status.SATISFIABLE, "Model is not satisfiable")
optimize.getModel
(status == Status.SATISFIABLE).option(
optimize.getModel
)
}

def runExternal(evaluate: String*): List[String] = {
def runExternal(evaluate: String*): Option[List[String]] = {
val debug = false

val programStart = optimize.toString
Expand All @@ -190,10 +192,15 @@ private class Z3Optimizer(val context: Context, val optimize: Optimize)

if (debug) println(results)

val lines = results.splitLines
lines.head.trim shouldEqual "sat"
lines.tail.size shouldEqual evaluate.length
lines.tail
results match {
case Left(_) =>
none
case Right(results) =>
val lines = results.splitLines
lines.head.trim shouldEqual "sat"
lines.tail.size shouldEqual evaluate.length
lines.tail.some
}
}

def resultToInt(result: String): Int =
Expand Down
9 changes: 6 additions & 3 deletions scala2/src/main/scala/jurisk/process/Runner.scala
Original file line number Diff line number Diff line change
@@ -1,13 +1,14 @@
package jurisk.process

import mouse.all.booleanSyntaxMouse
import org.scalatest.matchers.should.Matchers.convertToAnyShouldWrapper

import scala.io.Source
import scala.sys.process.ProcessIO
import scala.sys.process.stringSeqToProcess

object Runner {
def runSync(command: String*)(input: String): String = {
def runSync(command: String*)(input: String): Either[String, String] = {
val outputBuilder = new StringBuilder
val io = new ProcessIO(
in => {
Expand All @@ -22,7 +23,9 @@ object Runner {
_.close(),
)
val process = command.run(io)
process.exitValue() shouldEqual 0
outputBuilder.toString()
// Note - order is important
val exitValue = process.exitValue()
val result = outputBuilder.toString()
(exitValue == 0).either(result, result)
}
}
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package jurisk.adventofcode.y2024

import Advent13._
import jurisk.adventofcode.y2024.Advent13.SolutionMode.{ExternalZ3, InternalZ3}
import org.scalatest.freespec.AnyFreeSpec
import org.scalatest.matchers.should.Matchers._

Expand All @@ -20,8 +21,10 @@ class Advent13Spec extends AnyFreeSpec {

"part 2" - {
"test #0" in {
val example2 = testData.head
example2.solve2 shouldEqual Some(80 * 3 + 40)
val example = testData.head
val expected = Some(80 * 3 + 40)
example.solve(InternalZ3) shouldEqual expected
example.solve(ExternalZ3) shouldEqual expected
}

"real" in {
Expand Down

0 comments on commit 790816d

Please sign in to comment.