How to get solutions for an expression in Z3

Question

I am trying to do something in theory very easy with Z3, but I am not sure how to do it.

So imagine I have this code in C:

int c;
if (c>=65 && C<91)
    int d = c + 32;

I would like to know possible solutions for d, for example 97. I try to express the problem in Z3 like this:

(declare-const c Int)
(assert (> c 64))
(assert (< c 91))
(define-fun d() Int
 (+ 32 c)
)
(assert (> d 0))
(check-sat)
(get-model)

But in this way I get solutions for c not for the variable d.

How should I do it?

Thank you very much!

Answer 1

If you want to get one solution for d, you can use:

(declare-const c Int)
(declare-const d Int)

(assert (> c 64))
(assert (< c 91))

(assert (= d (+ c 32)))
(check-sat)
(get-model)

If you want to find all solutions for d, you can repeatedly negate models and add them as constraints. See Taylor's response here: Z3: finding all satisfying models

Edit: Adding on, a slightly more direct translation of the program would use:

(>= 65 c)

rather than

(> 64 c)