Simplifying uninterpreted functions in Z3

Question

Is there any way to apply simplifications to uninterpreted functions defined in z3, rather than the goals and subgoals ? I have the following z3 code : ``` (declare-fun f (Bool Bool) Bool) (assert (forall ((b1 Bool) (b2 Bool)) (implies b2 (f b1 b2)))) (assert (exists ((b1 Bool) (b2 Bool)) (not (f b1 b2)))) (check-sat) (get-model) ``` And I get the following output: ``` sat (model (define-fun b1!1 () Bool false) (define-fun b2!0 () Bool false) (define-fun k!7 ((x!1 Bool)) Bool false) (define-fun f!8 ((x!1 Bool) (x!2 Bool)) Bool (ite (and (= x!1 false) (= x!2 true)) true false)) (define-fun k!6 ((x!1 Bool)) Bool (ite (= x!1 false) false true)) (define-fun f ((x!1 Bool) (x!2 Bool)) Bool (f!8 (k!7 x!1) (k!6 x!2))) ) ``` It turns out that by applying rewrite rules to the definition of f, we can get that f is equal to the second argument (x!2) by the following derivation: ``` (f!8 (k!7 x!1) (k!6 x!2)) = (f!8 false (k!6 x!2)) = (f!8 false x!2) =(x!2) ``` Is there any way to get z3 to produce…

Accepted Answer

One option is to ask Z3 to evaluate the expression `(f x y)` where `x` and `y` are fresh Boolean constants. The `eval` command will evaluated `(f x y)` in the current model, and will produce `y` in your example. Here is the complete example (also available online here):

```
(declare-fun f (Bool Bool) Bool)

; x and y are free Boolean constants that will be used to create the expression (f x y)
(declare-const x Bool)
(declare-const y Bool)

(assert (forall ((b1 Bool) (b2 Bool))
        (implies b2 (f b1 b2))))
(assert (exists ((b1 Bool) (b2 Bool))
        (not (f b1 b2))))
(check-sat)

(eval (f x y))
```

Simplifying uninterpreted functions in Z3

Solution

Problem