부울 함수를 'check-sat'가 가정으로 지원하지 않습니까?

Question

다음 예제에서는 각 가정에 대해 단일 부울 상수가 아닌 "(declare-const p (Int) Bool)"와 같은 해석되지 않은 부울 함수를 사용하려고했습니다. 하지만 작동하지 않습니다 (컴파일 오류가 발생합니다).

(set-option :produce-unsat-cores true) 
(set-option :produce-models true) 

(declare-fun p (Int) Bool) 
      ;(declare-const p1 Bool) 
      ;(declare-const p2 Bool) 
      ; (declare-const p3 Bool) 

;; We assert (=> p C) to track C using p 
(declare-const x Int) 
(declare-const y Int) 
(assert (=> (p 1) (> x 10))) 
;; An Boolean constant may track more than one formula 
(assert (=> (p 1) (> y x))) 

(assert (=> (p 2) (< y 5))) 
(assert (=> (p 3) (> y 0))) 

(check-sat (p 1) (p 2) (p 3)) 
(get-unsat-core) 

출력

Z3(18, 16): ERROR: invalid check-sat command, 'not' expected, assumptions must be Boolean literals 
Z3(19, 19): ERROR: unsat core is not available 

나는 그것이 (지원되지 않는) 불가능하다는 것을 이해 부울 기능을 사용할 수 있습니다. 그 뒤에 어떤 이유가 있습니까? 거기에 다른 방법이 있습니까?

Answer 1

Z3은 문제를 해결하기 전에 많은 단순화를 적용하기 때문에 이러한 제한이 있습니다. 그들 중 일부는 수식과 용어를 다시 작성합니다. 실제로 Z3에 의해 해결되는 문제는 입력 문제와 매우 다른 경우가 많습니다. 우리는 단순화 된 가정을 원래의 가정으로 추적하거나 보조 변수를 도입 할 것입니다. 부울 리터럴을 제한하면이 문제가 방지되고 인터페이스가 매우 깨끗해집니다. 이 제한은 표현을 제한하지 않는다는 점에 유의하십시오. 다른 어설 션을 추적하기 위해 많은 부울 변수를 선언하는 것이 너무 성가시다. 나는 Z3Py라는 새로운 Python 프론트 엔드를 살펴 보길 권한다. SMT 2.0보다 훨씬 편리하게 사용할 수 있습니다. 이 예에서 해석되지 않은 술어 p을 만드는 대신 "벡터"(실제로는 파이썬 목록) o 부울 상수가 만들어집니다.

Z3Py online tutorial에는 많은 예제가 들어 있습니다.

Z3Py에서 보조 변수를 만드는 방법을 구현할 수도 있습니다. 트릭을 수행하는 스크립트는 다음과 같습니다. 모든 배관 작업을 수행하는 check_ext 함수를 정의했습니다. http://rise4fun.com/Z3Py/B4