우리가 얻을 Z3 옵션에서 C-API

를 사용하여 임의 화 설정 Z3 - 임의의 씨앗을 설정할 수있는 C의 API가있는 경우, 내가 궁금우리가 얻을 Z3 옵션에서 C-API

Search heuristics: 
    -rd:num  random case-split frequency (default: 2). 
    -rs:num  random seed.

다음 API를 사용하여 시간 제한을 설정합니다. 임의 시드와 비슷한 것이 있습니까?

params = Z3_mk_params(ctx);   
Z3_params_set_uint(ctx, params, Z3_mk_string_symbol(ctx, ":timeout"), timeout);    
Z3_solver_set_params(ctx, solver, params);

고마워요!

출처

2012-12-28 Raj

매개 변수의 이름은 :random-seed입니다. 값은 unsigned int입니다.

즉, 다음 Z3 버전 (v4.3.2)은 매개 변수 설정에 대한 지원이 훨씬 향상 될 것입니다. 향상된 기능은 unstable (작업 중) 지점 http://z3.codeplex.com에 이미 있습니다.

출처

2012-12-28 16:52:25

그냥 명확히하기 위해, z3을 실행할 때마다 동일한 모델을 얻을 것이라고 랜덤 시드가 보증합니까? 감사! – rsinha

예. Z3는 결정 론적이라고 가정합니다. 일련의 입력 매개 변수와 플랫폼 (예 : Linux)이 주어지면 Z3은 항상 동일한 결과를 생성해야합니다. 그렇지 않은 경우 Z3의 버그이며 수정해야합니다. 과거 버그를 수정했습니다. –

우리가 얻을 Z3 옵션에서 C-API

답변

관련 문제