랜덤 솔루션 Yices 솔버

Question

나는 을 c 프로그램에서 사용하여 x > 100 표현을 해결하고 x에 대한 해결책을 얻고 싶습니다. 여기 내 코드는 다음과 같습니다.

#include<stdio.h> 
#include"yices_c.h" 

int main() { 
    yices_context ctx = yices_mk_context(); 
    char int_ty_name[] = "int"; 
    yices_type int_ty = yices_mk_type(ctx, int_ty_name); 
    char vname[] = "x"; 
    yices_expr e1 = yices_mk_num(ctx,100); 
    yices_var_decl v = yices_mk_var_decl(ctx,vname,int_ty); 
    yices_expr e2 = yices_mk_var_from_decl(ctx,v); 
    yices_expr eq1 = yices_mk_lt(ctx, e1, e2); 
    yices_assert(ctx, eq1); 
    yices_dump_context(ctx); 
    switch(yices_check(ctx)) { 
    case l_true: 
    printf("satisfiable\n"); 
    yices_model m = yices_get_model(ctx); 
    long i; 
    yices_get_int_value(m,v,&i); 
    printf("e2 = %d\n", i); 
    yices_display_model(m); 
    break; 
    case l_false: 
    printf("unsatisfiable\n"); 
    break; 
    case l_undef: 
    printf("unknown\n"); 
    break; 
    } 
    yices_del_context(ctx); 
    return 0; 
} 

이 프로그램의 결과는 항상 x =101입니다. 101은이 표현식에 대한 가능한 결과 중 하나 일뿐입니다. 솔버가 가능한 모든 결과 (임의의 정수 101에서 MAX_INT까지)에서 임의의 결과를 선택하기를 원합니다.

어떻게해야합니까?

Answer 1

yices_check(ctx) 대신 yices_find_weighted_model(ctx, 1)을 사용해보세요.

가중치 제한이없는 경우 yices_find_weighted_model(ctx, 0)은 의미 적으로 yices_check(ctx)과 같아야합니다. random이라고하는 두 번째 매개 변수 yices_find_weighted_model을 사용하면 기본값을 0이 아닌 값으로 설정하면 기본 결정 절차 대신 무작위 검색을 사용할 수 있습니다. documentation을 확인하십시오.

Answer 2

먼저 무작위로 결과가 표시됩니다. 다음에 무작위 델타가있는 임의 제한 조건 (X>nonRandomResult+delta 또는 X<nonRandomResult-delta)을 추가 할 수 있습니다.

해결할 수없는 한 이전 값의 절반을 갖는 새 델타로 제약 조건을 변경해야합니다. 솔루션을 얻 자마자 그 솔루션은 그 델타만큼 무작위적일 것입니다.