Z3의 Get-assignment

Question

(get-assignment) 명령은 Bool 일 경우 심볼 목록과 true/false 값을 반환해야합니다. 필자의 이해에 따르면, 다음과 같은 경우에만 수행 할 수 있습니다. produce-assignments가 true로 설정되고 (check-sat)가 sat 인 경우. 그러나, Z3에서 이것을 테스트하기 위해 작은 스크립트를 실행하면 (get-assignment) 그냥 공백을 반환합니다 (공백).

(set-option :produce-assignments true) 
(set-logic QF_UF) 
(declare-fun a() Bool) 
(declare-fun b() Bool) 
(assert (= a b)) 
(check-sat) 
(get-assignment) 

Answer 1

get-assignment의 의미는 직관적되지 않습니다 : 여기 내 스크립트입니다. named 하위 수식의 값을 표시합니다. SMT 2.0 reference (62 페이지)에서 :

get-assignment 는 수식을 입력 한 이전의 선택 세트에 대한 진실 할당을 요청 경량 얻을 값의 제한 버전 (29) 마찬가지로 여러 가지로. 이미 설명한 (get-proof) 다른 명령은 기본적으로 false 인 생산 할당 옵션이 true로 설정되어있는 경우에만 발행 될 수 있습니다 (아래 섹션 5.1.7 참조). 솔버는이 옵션을 지원하지 않아도됩니다. get-value와 마찬가지로, assertion-set 명령을 개입시키지 않고, 명령을보고하거나 또는 알려지지 않은 것을보고하는 명령 ( 알 수 없음)을보고하는 경우에만 발급받을 수 있습니다. 은 모든 쌍 (fb)의 시퀀스를 반환합니다. 여기서 b는 참 또는 거짓 이고 f는 모든 어설 션의 집합 에있는 형식 (이름이 t 인 f)의 레이블이며 t는 Bool을 정렬합니다. get-value와 마찬가지로 의 경우 가장 최근의 check-sat 명령의 응답이 있었고 인 경우 모든 어설 션 세트에는 반환 된 진리 지정과 일치하는 모델 ( 로직에 있음)이 보장됩니다. . 여기

두 개의 이름 subformulas (또한 온라인 here)를 사용하여 같은 예이다 : - 64 비트 - 빌드 그것은 가치가 무엇인지에 대한

(set-option :produce-assignments true) 
(set-logic QF_UF) 
(declare-fun a() Bool) 
(declare-fun b() Bool) 
(assert (! (= (! a :named a_val) b) :named eq_val)) 
(check-sat) 
(get-assignment)