Z3 고정 소수점 엔진의 두 가지 입력 형식이 서로 어떻게 관련되어 있는지 혼란스럽고 분투하고 있습니다. 간단한 예 : 음수의 존재를 증명하고 싶다고 가정 해 봅시다. 음수가 아닌 경우 1을 반환하고 음수 인 경우 0을 반환하는 함수를 선언하고 함수가 0을 반환하는 인수가 있으면 해결자가 실패하도록 요청하는 함수를 선언합니다. 그러나 하나의 제한이 있습니다. 적어도 하나가 존재하면 해결자를 sat 음수가 아닌 경우 모두 unsat입니다.Z3 고정 소수점 엔진을 사용하는 ∃-queries 및 ∀-queries
그것은 declare-rel 및 query 형식을 사용하여 하찮게입니다 :
(declare-rel f (Int Int))
(declare-rel fail())
(declare-var n Int)
(declare-var m Int)
(rule (=> (< n 0) (f n 0)))
(rule (=> (>= n 0) (f n 1)))
(rule (=> (and (f n m) (= m 0)) fail))
(query fail)
을하지만 (forall에) 순수 SMT-LIB2 형식을 사용하면서 까다로운된다. 예를 들어, 직선
(set-logic HORN)
(declare-fun f (Int Int) Bool)
(declare-fun fail() Bool)
(assert (forall ((n Int))
(=> (< n 0) (f n 0))))
(assert (forall ((n Int))
(=> (>= n 0) (f n 1))))
(assert (forall ((n Int) (m Int))
(=> (and (f n m) (= m 0)) fail)))
(assert (not fail))
(check-sat)
은 unsat을 반환합니다. 당연히 (= m 0)을 (= m 1)으로 변경하면 결과가 동일합니다. sat은 fail을 의미하고 (= m 2)에서 얻을 수 있습니다. 문제는 내가 이해할 수 없다는 것인데, 해답을 구하는 방법이 형식을 사용하는 것입니다. 대답 sat 즉, 우리는 ∀-해결책을 찾기 위해 요청할 수 있습니다 forall 형을 사용하는 동안 나는 순간에 그것을 이해하고있어 어떻게
는 해석이 해석 (또는 불변) 모든 에 대한 모든 주장을 satisfiying을 발견 할 수 있음을 의미 값이고 unsat은 그러한 기능이 없음을 의미합니다. 즉 은을 증명하려고 시도합니다. 즉, 'proof'(불변 식)를 모델에 넣습니다 (분명히, sat 일 때). declare-rel 형식 해결사에서 솔루션을 보내고 반대로
query는 제약이 ∃ - 정량에 따라 일부 변수처럼
에 대한 솔루션을 검색합니다. 즉, 의 카운터 예제을 제공합니다. unsat의 경우에만 불변량을 인쇄 할 수 있습니다.
- 내가 올바른 그것을 이해하고 있습니까 : 나는 몇 가지 질문이 있습니까? 몇 가지 핵심 아이디어를 놓친 것처럼 느껴집니다. 예를 들어, 을
(assert (forall ...))으로 표현하는 방법에 대한 일반적인 아이디어는 정말 도움이 될 것입니다 (질문 2를 자동으로 답합니다). - 순수 SMT-LIB2 형식으로 이러한 ∃-constraints (반올림 할 때
sat출력)를 풀 수있는 방법이 있습니까? 그렇다면 어떻게?
Nikolaj, 명확하고 완전한 답변을 주셔서 대단히 감사합니다. – dvvrd