weight.sh

#!/bin/sh
set -euo pipefail
IFS=$'\n\t'

cvc4 --lang=smt << EOF
(set-option :produce-assignments true)

(set-logic ALL_SUPPORTED)

(declare-const frac Int)
(declare-const five Int)
(declare-const ten Int)
(declare-const quarter Int)
(declare-const plate Int)

(assert (> 2 frac))
(assert (> 2 five))
(assert (> 2 ten))
(assert (> 2 quarter))

(assert (> frac (- 1)))
(assert (> five (- 1)))
(assert (> ten (- 1)))
(assert (> quarter (- 1)))
(assert (> plate (- 1)))

(declare-const i0 Real)
(declare-const i1 Real)
(declare-const i2 Real)
(declare-const i3 Real)
(declare-const i4 Real)
(declare-const i5 Real)

(assert (= i0 (* 2.5 (* 2 frac))))
(assert (= i1 (* 5 (* 2 five))))
(assert (= i2 (* 10 (* 2 ten))))
(assert (= i3 (* 25 (* 2 quarter))))
(assert (= i4 (* 45 (* 2 plate))))

(assert (= i5 (+ (+ (+ (+ i0 i1) i2) i3) i4)))

(assert (= i5 (- $1 45)))

(check-sat)

(get-value (frac five ten quarter plate))

EOF