palindrome.z3

(define-fun palindrome ((n Int)) Bool
    (exists ((a Int) (b Int) (c Int))
      (and (>= a 1) (<= a 9)
           (>= b 0) (<= b 9)
           (>= c 0) (<= c 9)
           (= n (+ (* 100000 a) (* 10000 b) (* 1000 c) (* 100 c) (* 10 b) a)))))

(define-fun solution ((n Int)) Bool
  (exists ((factor1 Int) (factor2 Int))
    (and (>= factor1 100) (< factor1 1000)
         (>= factor2 100) (< factor2 1000)
         (= n (* factor1 factor2))
         (palindrome n))))

(declare-const s Int)
(assert (and (solution s)
             (forall ((r Int))
                     (implies (solution r)
                              (<= r s)))))

(check-sat)
(get-model)