pull_nested_quantifiers 옵션이 Z3에서 simplify와 함께 작동합니까?

수식의 모든 중첩 된 한정 기호를 가장 바깥 쪽 레벨로 가져 오려고합니다. 나는 Z3에서 작동하려면 다음 명령을 예상하지만 그렇지 않은 :pull_nested_quantifiers 옵션이 Z3에서 simplify와 함께 작동합니까?

(set-option :pull-nested-quantifiers true) 
(simplify (exists ((x Int)) (and (>= x 0) 
          (forall ((y Int)) (and (>= y 1) (> x y))))))

:pull-nested-quantifiers의 목적은 무엇인가? SMT-LIB 또는 Z3 API를 사용하여 중첩 된 한정어를 가져올 수 있습니까?

출처

2012-03-06 pad

Z3 3.x에서 simplify 명령은 범용 로컬 단순화 단계 만 적용합니다. "Pull-Nested-Quantifiers"는 사전 처리 단계입니다. 향후 릴리스에서는 전술/전략으로 사용할 수 있습니다. Z3 3.2는 이미 SMT 2.0 프론트 엔드에 많은 전략/전술을 내장하고 있습니다. 다음 릴리즈에는 훨씬 더 많은 전술이있을 것입니다. API에서도 사용할 수 있습니다. 일부 프로젝트에서이 기능이 필요한 경우, 저에게 이메일을 보내 주시면 비공식 (베타) 릴리스를 드리겠습니다.

마지막으로 범용 한정 기호에 중첩 된 (범용) 수량 한정 기호가 없으면 모델 기반 수량 지정기 인스턴스화 MBQI 모듈이 훨씬 잘 작동하기 때문에이 전처리 단계가 있습니다. 귀하의 예제는 괜찮습니다. 왜냐하면 Z3가 실존을 없애고 x을 새로운 상수로 바꿀 것이기 때문입니다.

출처

2012-03-07 19:56:29

Prenex Normal Form으로 수식을 변환하기 위해 단순화 단계로 풀 중첩 된 한정 기호를 사용하고 싶습니다. 이 옵션은 전처리 단계로만 사용할 수있는 것으로 보입니다. 맞습니까? – pad

pull_nested_quantifiers 옵션이 Z3에서 simplify와 함께 작동합니까?

답변

관련 문제