;; Carries are 0 or 1 (declare-const c1 Int) (assert (&& (>= c1 0) (<= c1 1))) (declare-const c2 Int) (assert (&& (>= c2 0) (<= c2 1))) (declare-const c3 Int) (assert (&& (>= c3 0) (<= c3 1))) ;; All digits are in {0, 1, ... 9} (declare-const f Int) (assert (&& (>= f 0) (<= f 9))) (declare-const t Int) (assert (&& (>= t 0) (<= t 9))) (declare-const u Int) (assert (&& (>= u 0) (<= u 9))) (declare-const w Int) (assert (&& (>= w 0) (<= w 9))) (declare-const r Int) (assert (&& (>= r 0) (<= r 9))) (declare-const o Int) (assert (&& (>= o 0) (<= o 9))) ;; Arithmetic (assert (= (+ o o) (+ r (* 10 c1)))) (assert (= (+ c1 (+ w w)) (+ u (* 10 c2)))) (assert (= (+ c2 (+ t t)) (+ o (* 10 c3)))) (assert (= c3 f)) ;; First digits cannot be zero (assert (not (= t 0))) (assert (not (= f 0))) ;; Assumption: all digits are distinct (assert (distinct f t u w r o)) (check-sat) (get-model) (exit)