Simplification of uninterpreted functions in Z3

Question

Is there a way to apply simplifications to uninterpreted functions defined in z3, and not to 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 rewriting rules to the definition of f, we can get that f is equal to the second argument (x! 2) with the following expression:

 (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 a way to get z3 to automatically create the next definition?

---

 (define-fun f ((x!1 Bool) (x!2 Bool)) Bool (x!2)) 

---

Thank you for your help. Sincerely, Osvaldo.

Answer 1

One option is to ask Z3 to evaluate the expression (fxy) , where x and y are fresh Boolean constants. The eval command will evaluate (fxy) in the current model and will produce y in your example. Here is a 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 (fxy) (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 (fxy))