생성 된 모델 값의 Z3 임의성

Question

Z3에서 생성 된 모델 값에 대한 결과의 임의성에 영향을 미치려고합니다. 필자가 이해하는 한, 이것에 대한 옵션은 매우 제한적입니다. 선형 산술의 경우, 단선 해석기는 주어진 제약 조건을 여전히 만족시키는 무작위 결과를 허용하지 않습니다. 내가 작업을 진행하게 보이지 않는 그러나, 옵션 smt.arith.random_initial_value는 ("false)를 선형 연산 (기본의 단순 기반 절차에서 임의 초기 값을 사용")가

from z3 import * 
set_option('smt.arith.random_initial_value',True) 
x = Int('x') 
y = Int('y') 
s = Solver() 
s.add(x+y > 0) 
s.check() 
s.model() 

결과적으로 항상 [y = 0, x = 1]을 생성하는 것처럼 보입니다. 주어진 제약 조건에서 사용되지 않은 변수에 대한 모델 완성조차도 항상 결정 론적 결과를 산출합니다.

이 옵션의 작동 방식에 대한 아이디어 나 힌트가 있으십니까?

Answer 1

잡기에 감사드립니다. 무작위 종자가 산술 이론에 넘어 가지 않게 만든 버그가있었습니다. 불안정한 지점 (수정 here)에서 수정되었습니다.

이 예 :

(set-option :smt.arith.random_initial_value true) 
(declare-const x Int) 
(declare-const y Int) 
(assert (> (+ x y) 0)) 
(check-sat-using (using-params qflra :random_seed 1)) 
(get-model) 
(check-sat-using (using-params qflra :random_seed 2)) 
(get-model) 
(check-sat-using (using-params qflra :random_seed 3)) 
(get-model) 

지금 세 가지 모델을 생성합니다

sat 
model 
    (define-fun y() Int 
    4294966763) 
    (define-fun x() Int 
    4294966337) 
) 
sat 
(model 
    (define-fun y() Int 
    216) 
    (define-fun x() Int 
    4294966341) 
) 
sat 
(model 
    (define-fun y() Int 
    196) 
    (define-fun x() Int 
    4294966344) 
) 

이 옵션을 (제대로 통과되지 않은 다른 장소에있을 수 있습니다 것 같습니다 예를 들어, 설정을 사용하는 경우 qflra 전술을 직접 호출하는 대신 논리를 사용함), 우리는 여전히 그것을 조사하고 있습니다.