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

---

그것은에 의해 밝혀를 F의 정의에 재 작성 규칙을 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))