Tương đương với xác định vui trong Z3 API

Question

Sử dụng Z3 với định dạng văn bản, tôi có thể sử dụng define-fun để xác định các chức năng để sử dụng lại sau này. Ví dụ:

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

Tôi tự hỏi làm thế nào để tạo define-fun với Z3 API (tôi sử dụng F #) thay vì lặp lại những cơ quan chức năng ở khắp mọi nơi. Tôi muốn sử dụng nó để tránh trùng lặp và gỡ lỗi công thức dễ dàng hơn. Tôi đã thử với Context.MkFuncDecl, nhưng dường như chỉ tạo ra các hàm không diễn giải.

Answer 1

Lệnh define-fun chỉ tạo macro. Lưu ý rằng tiêu chuẩn SMT 2.0 không cho phép định nghĩa đệ quy. Z3 sẽ mở rộng mỗi lần xuất hiện của my-div trong thời gian phân tích cú pháp. Lệnh define-fun có thể được sử dụng để làm cho tệp đầu vào đơn giản và dễ đọc hơn, nhưng bên trong nó không thực sự hữu ích cho Z3.

Trong API hiện tại, không có hỗ trợ cho việc tạo macro. Đây không phải là một giới hạn thực sự, vì chúng ta có thể định nghĩa một hàm C hoặc F # để tạo ra các cá thể của một macro. Tuy nhiên, có vẻ như bạn muốn hiển thị (và kiểm tra thủ công) các công thức được tạo bằng cách sử dụng API Z3. Trong trường hợp này, macro sẽ không giúp bạn.

Một giải pháp thay thế là sử dụng định lượng. Bạn có thể khai báo một chức năng uninterpreted my-div và khẳng định công thức phổ biến định lượng:

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

Bây giờ, bạn có thể tạo công thức của bạn bằng cách sử dụng chức năng uninterpreted mydiv.

Loại công thức định lượng này có thể được xử lý bởi Z3. Trên thực tế, có hai tùy chọn để xử lý loại định lượng này:

1. Sử dụng công cụ tìm macro: bước tiền xử lý này xác định định lượng về cơ bản là xác định macro và mở rộng chúng. Tuy nhiên, việc mở rộng chỉ xảy ra trong thời gian tiền xử lý, không phải trong quá trình phân tích cú pháp (tức là thời gian xây dựng công thức). Để bật công cụ tìm mô hình, bạn phải sử dụng MACRO_FINDER=true
2. Tùy chọn khác là sử dụng MBQI (khởi tạo định lượng dựa trên mô hình). Mô-đun này cũng có thể xử lý loại định lượng này. Tuy nhiên, các định lượng sẽ được mở rộng theo yêu cầu.

Tất nhiên, thời gian giải quyết có thể phụ thuộc nhiều vào phương pháp bạn sử dụng. Ví dụ: nếu công thức của bạn không thỏa mãn một cách độc lập với "ý nghĩa" của mydiv, thì cách tiếp cận 2 có lẽ tốt hơn.

Answer 2

Tôi gặp vấn đề tương tự. Cụ thể hơn, tôi cần các chức năng:

Z3_ast Z3_mk_bvredxnor(Z3_context ctx, Z3_ast t) 

mà thực hiện một XNOR trên tất cả các bit của một bitvector đưa ra trong tham số cho hàm, và trả về một bitvector chiều dài 1.

Kể từ khi chức năng này không tồn tại trong API, tôi bắt đầu sử dụng:

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; 
} 

Sau đó, cố gắng gỡ lỗi những hạn chế của tôi là một cơn ác mộng.

Vì vậy, tôi đã đưa ra:

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); 
} 

Bất kỳ comment để cải thiện điều này sẽ được hoan nghênh. Trong lúc này, nó giải quyết vấn đề tôi đã here

Nó hiện các trick, nhưng complexify mô hình của tôi ...

Ngoài ra tôi tự hỏi:

• Vì đây là tất cả thực hiện programatically, tôi giả sử MACRO_FINDER = TRUE sẽ không có bất kỳ tác động nào (vì nó là một bước xử lý).
• Vì MBQI được bật theo mặc định, không cần phải kích hoạt, phải không?