Równoważnik określenia-zabawy w Z3 API

Question

Używając Z3 z formatem tekstowym, mogę użyć funkcji define-fun do zdefiniowania funkcji do ponownego użycia w późniejszym czasie. Na przykład:

(define-fun mydiv ((x Real) (y Real)) Real 
    (if (not (= y 0.0)) 
     (/ x y) 
     0.0)) 

Zastanawiam się, jak tworzyć define-fun z Z3 API (używam F #) zamiast powtarzać ciało funkcji wszędzie. Chcę go użyć, aby uniknąć powielania i debugowania formuł. Próbowałem z Context.MkFuncDecl, ale wydaje się generować tylko funkcje nieinterpretowane.

Answer 1

Komenda define-fun tworzy właśnie makro. Zauważ, że standard SMT 2.0 nie dopuszcza definicji rekursywnych. Z3 rozszerzy każde wystąpienie my-div podczas analizowania czasu. Polecenie define-fun może być użyte w celu uproszczenia i łatwiejszego odczytu pliku wejściowego, ale wewnętrznie nie pomaga Z3.

W bieżącym interfejsie API nie ma obsługi tworzenia makr. To nie jest prawdziwe ograniczenie, ponieważ możemy zdefiniować funkcję C lub F #, która tworzy wystąpienia makra. Wygląda jednak na to, że chcesz wyświetlić (i ręcznie sprawdzić) formuły utworzone za pomocą interfejsu API Z3. W takim przypadku makra nie pomogą.

Jedną z alternatyw jest użycie kwantyfikatorów. Można zadeklarować zinterpretowane funkcję my-div i dochodzić powszechnie ilościowo wzoru:

(declare-fun mydiv (Real Real) Real) 
(assert (forall ((x Real) (y Real)) 
       (= (mydiv x y) 
        (if (not (= y 0.0)) 
         (/ x y) 
         0.0)))) 

Teraz można utworzyć formułę, korzystając z funkcji mydiv zinterpretowane.

Ten rodzaj oznaczania ilościowego może być obsługiwany przez Z3. Faktycznie, istnieją dwie opcje do obsługi tego rodzaju kwantyfikator:

1. wykorzystać makro Finder: Ten krok przerób identyfikuje kwantyfikatorów, które są zasadniczo definiowanie makr i rozwinąć je. Jednak ekspansja zachodzi tylko w czasie przetwarzania wstępnego, a nie podczas parsowania (to jest czasu konstrukcji formuły). Aby włączyć wyszukiwarkę modeli, należy użyć MACRO_FINDER=true
2. Inną opcją jest użycie MBQI (modelowanie kwantyfikatora oparte na modelu). Ten moduł może również obsługiwać tego rodzaju kwantyfikator. Kwantyfikatory zostaną jednak rozszerzone na żądanie.

Oczywiście, czas rozwiązywania może w dużym stopniu zależeć od tego, z którego podejścia korzystasz. Na przykład, jeśli twoja formuła jest niezadowalająca niezależnie od "znaczenia" mydiv, wówczas podejście 2 jest prawdopodobnie lepsze.

Answer 2

Mam ten sam problem. Bardziej szczegółowo, to potrzebne funkcje:

Z3_ast Z3_mk_bvredxnor(Z3_context ctx, Z3_ast t) 

który wykonuje XNOR nad wszystkimi bitami o bitvector podanym w argumencie funkcji i zwraca bitvector długości 1.

Ponieważ ta funkcja nie jest dostępna istnieje w API, zacząłem używać:

Z3_ast mk_bvredxnor(Z3_context ctx, Z3_ast t) 
{ 
    size_t i; 
    size_t s = Z3_get_bv_sort_size(ctx,Z3_get_sort(ctx,t)); 
    Z3_ast ret = Z3_mk_extract(ctx,0,0,t); 
    for(i=1;i<s;i++) 
     ret = Z3_mk_bvxnor(ctx,ret,Z3_mk_extract(ctx,i,i,t)); 
    return ret; 
} 

Następnie, próbując zdebugować moje ograniczenia był koszmar.

Więc wymyśliłem:

Z3_func_decl getBvredxnorDecl(Z3_context ctx, int size) 
{ 
static bool sizes[64]={0}; 
static Z3_func_decl declTab[64]={0}; 

if(sizes[size]) 
    return declTab[size]; 

    Z3_sort bv_size = Z3_mk_bv_sort(ctx, size); 
    Z3_sort bv1  = Z3_mk_bv_sort(ctx, 1); 

    stringstream buff; 
    buff << "bvredxnor" << size; 
    Z3_symbol var_name = Z3_mk_string_symbol(ctx,"X"); 
    Z3_symbol func_name = Z3_mk_string_symbol(ctx, buff.str().c_str()); 

    Z3_func_decl bvredxnorDecl = Z3_mk_func_decl(ctx, 
               func_name, 
               1, 
               &bv_size, 
               bv1); 
declTab[size]=bvredxnorDecl; 

    Z3_ast b = Z3_mk_bound(ctx,0,bv_size); /* bounded variable */ 
    Z3_ast bvredxnorApp = Z3_mk_app(ctx,bvredxnorDecl, 1, &b); 

    Z3_pattern pattern = Z3_mk_pattern(ctx,1,&bvredxnorApp); 

    Z3_ast bvredxnor_def = mk_bvredxnor(ctx,b); 
    Z3_ast def = Z3_mk_eq(ctx,bvredxnorApp,bvredxnor_def); 

    Z3_ast axiom = Z3_mk_forall(ctx,0,1,&pattern,1,&bv_size,&name,def); 

    Z3_assert_cnstr(ctx,axiom); 

return bvredxnorDecl; 
} 

Z3_ast bvredxnor(Z3_context ctx, Z3_ast t) 
{ 
int size = Z3_get_bv_sort_size(ctx,Z3_get_sort(ctx,t)); 
return Z3_mk_app(ctx,getBvredxnorDecl(ctx,size),1, &t); 
} 

żadnych uwag do poprawy byłoby to mile widziane. W tym czasie, to rozwiązuje problem miałem here

robi trick, ale complexify mojego modelu ...

Również zastanawiam

• Ponieważ to wszystko zrobić programowo, I załóżmy, że MACRO_FINDER = TRUE nie będzie miało żadnego wpływu (ponieważ jest to krok przetwarzania).
• Ponieważ MBQI jest domyślnie włączony, nie ma potrzeby go aktywować, prawda?