part2-tpl.smt2

(set-logic AUFLIA)

(declare-sort RPS 0)
(declare-fun rock () RPS)
(declare-fun paper () RPS)
(declare-fun scissors () RPS)

(declare-sort OUTCOME 0)
(declare-fun win () OUTCOME)
(declare-fun lose () OUTCOME)
(declare-fun draw () OUTCOME)

(declare-fun A () RPS)
(declare-fun B () RPS)
(declare-fun C () RPS)

(declare-fun X () OUTCOME)
(declare-fun Y () OUTCOME)
(declare-fun Z () OUTCOME)

(assert (= A rock))
(assert (= B paper))
(assert (= C scissors))

(assert (= X lose))
(assert (= Y draw))
(assert (= Z win))

(declare-fun shape-score (RPS) Int)
(assert (= 1 (shape-score rock)))
(assert (= 2 (shape-score paper)))
(assert (= 3 (shape-score scissors)))

(declare-fun outcome-score (OUTCOME) Int)
(assert (= 0 (outcome-score lose)))
(assert (= 3 (outcome-score draw)))
(assert (= 6 (outcome-score win)))

(define-fun game-outcome ((opponent RPS) (player RPS)) OUTCOME
    (ite (= player opponent)
         draw
         (ite (or (and (= player rock)     (= opponent scissors))
                  (and (= player paper)    (= opponent rock))
                  (and (= player scissors) (= opponent paper)))
              win
              lose)))
(assert (= win (game-outcome scissors rock)))
(assert (= lose (game-outcome paper rock)))
(assert (= draw (game-outcome rock rock)))

; ; I think I could define this using game-outcome and maybe forall, but...
; (define-fun shape-for-outcome ((opponent RPS) (outcome OUTCOME)) RPS
;     (ite (= outcome draw)
;          opponent
;          (ite (or (and (= outcome win)  (= opponent rock))
;                   (and (= outcome lose) (= opponent scissors)))
;               paper
;               (ite (or (and (= outcome win)  (= opponent paper))
;                        (and (= outcome lose) (= opponent rock)))
;                    scissors
;                    rock))))

(declare-fun shape-for-outcome (RPS OUTCOME) RPS)
(assert (forall ((opponent RPS) (player RPS))
        (let ((outcome (game-outcome opponent player)))
             (= player (shape-for-outcome opponent outcome)))))

(assert (= paper    (shape-for-outcome rock win)))
(assert (= scissors (shape-for-outcome rock lose)))
(assert (= rock     (shape-for-outcome rock draw)))

(define-fun game-score ((opponent RPS) (outcome OUTCOME)) Int
    (+ (shape-score (shape-for-outcome opponent outcome))
       (outcome-score outcome)))

(assert (= 4 (game-score A Y)))
(assert (= 1 (game-score B X)))
(assert (= 7 (game-score C Z)))

(declare-const final-score Int)

(assert (= final-score (+
%EXPRS%
)))

(check-sat)
(get-value (final-score))

part2.rb

exprs = File.readlines('input')
  .map { |l| "(game-score #{l.chomp})" }
  .join("\n")

smt2 = File.read('part2-tpl.smt2').sub('%EXPRS%', exprs)
File.write('part2-out.smt2', smt2)