Z3中的define-fun等效API

將Z3與文本格式一起使用，我可以使用define-fun來定義函數以供稍後重用。例如：Z3中的define-fun等效API

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

我不知道如何創建define-fun與Z3 API（我使用F＃），而不是到處重複函數體。我想用它來避免重複和調試公式更容易。我嘗試了Context.MkFuncDecl，但它似乎只生成未解釋的函數。

來源

2011-10-12 pad

define-fun命令只是創建一個宏。請注意，SMT 2.0標準不允許遞歸定義。 Z3將在解析時間內擴展my-div的每次出現次數。命令define-fun可用於使輸入文件更簡單易讀，但在內部它並不能真正幫助Z3。

在當前的API中，不支持創建宏。這不是一個真正的限制，因爲我們可以定義一個C或F＃函數來創建一個宏的實例。但是，您似乎想要顯示（並手動檢查）使用Z3 API創建的公式。在這種情況下，宏不會幫助你。

一種替代方法是使用量詞。你可以聲明未解釋的功能my-div和斷言普遍量化公式：

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

現在，您可以創建一個使用未解釋功能mydiv公式。

這種量化公式可以由Z3處理。實際上，有兩種方法可以處理這種量詞：

使用宏查找器：此預處理步驟標識實質上定義宏並擴展它們的量詞。但是，擴展只發生在預處理時間內，而不是在解析過程中（即公式構建時間）。要啓用模型搜索器，您必須使用MACRO_FINDER=true
另一個選項是使用MBQI（基於模型的量詞實例化）。這個模塊也可以處理這種量詞。但是，量詞將按需擴展。

當然，解決時間可能很大程度上取決於您使用的方法。例如，如果您的公式獨立於mydiv的「含義」而不可滿足，則方法2可能會更好。

來源

2011-10-12 18:53:47

謝謝你的詳細解答。使用通用量詞絕對是一個巧妙的技巧。我想知道使用通用量詞和未解釋函數的成本。我量化LIA的形式約束現在變成量化的UFLIA公式。這個改變是否嚴重影響了Z3的解決時間？ – pad

是的，公式將在'UFLIA'中，但它是UFLIA的一個可決定的片段。如果使用選項1（'MACRO_FINDER = true'），則性能影響應該非常小。 Z3會將這些量詞檢測爲宏，並將消除量詞和所有出現的輔助未解釋函數。因此，經過預處理後，問題將出現在「QF_LIA」中。選項2（'MBQI'）對性能的影響尚不明確，在一些問題中，Z3可能會更快，但其他問題會更慢。 –

謝謝！只是爲了澄清，我的原始公式是LIA與量詞，我想用LIA量詞消除來解決它們。選項1似乎對我更有吸引力，我將盡快嘗試。 – pad

我有同樣的問題。更具體而言，我所需要的功能：

Z3_ast Z3_mk_bvredxnor(Z3_context ctx, Z3_ast t)

執行過在參數傳遞給函數給出一個位向量的所有位的XNOR，並且由於該功能不返回長度1.

的位向量存在於API中，我開始使用：

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

然後，試圖調試我的約束是一場噩夢。

於是我想出了：

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

任何意見，以改善這將是受歡迎的。與此同時，它解決了我here

它的伎倆，但complexify我的模型的問題...

我也納悶：

因爲這是所有編程完成後，我假設MACRO_FINDER = TRUE不會有任何影響（因爲它是一個處理步驟）。
由於MBQI默認爲開啓狀態，因此無需激活它，對嗎？

來源

2013-02-28 20:55:33 Heyji

Z3中的define-fun等效API

回答

相關問題