Упрощение неинтерпретируемых функций в Z3

Question

Есть ли способ применить упрощения к неинтерпретированным функциям, определенным в z3, а не к целям и подцелям?

У меня есть следующий z3 код:

---

(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) 

---

И я получаю следующий результат:

---

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))) 
) 

---

Оказывается, что по pplying правила перезаписи для определения F, мы можем получить, что е равно второму аргументу по следующему выводу (х 2!):

(f!8 (k!7 x!1) (k!6 x!2)) 
= (f!8 false (k!6 x!2)) 
= (f!8 false x!2) 
=(x!2) 

Есть ли способ, чтобы получить z3, чтобы произвести следующее определение автоматически?

---

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

---

Спасибо за вашу помощь. С уважением, Освальдо.

Answer 1

Один из вариантов - попросить Z3 оценить выражение (f x y), где x и y являются свежими булевыми константами. Команда eval будет оценивать (f x y) в текущей модели и будет производить y в вашем примере. Вот полный пример (также доступен онлайн 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))