Z3_benchmark_to_smtlib_string（）的輸入參數

我想使用函數Z3_benchmark_to_smtlib_string（）。這裏是我使用的論據：Z3_benchmark_to_smtlib_string（）的輸入參數

Z3_benchmark_to_smtlib_string(
        ctx,   /* this one is valid */ 
        "test",  /* this one is random, I don't understand it */ 
        "QF_UFBV", /* I got this name from the smtlib website, valid ? */ 
        "sat",  /* not sure about this one either */ 
        NULL,   /* not sure about this one either */ 
        nb_assumptions, /* should be ok */ 
        assumptions, /* should be ok too */ 
        NULL);   /* not sure about this one, is this mandatory ? */

任何幫助將受到歡迎。

與此同時，我使用我的顯示在飛行的假設，使用：

Z3_set_ast_print_mode（CTX，Z3_PRINT_SMTLIB2_COMPLIANT）;

en得到如下的奇怪字符：？x21，？x24，？x37，（見下文）。任何暗示解決這個問題？

由於提前，

（讓（（？X21（bvand（_ bv582 32）（ITE（=（（_ SIGN_EXTEND 24）（_ bv98 8））（（_ SIGN_EXTEND 24）| Mem5 [8] |））（_ bv64 32）（_ bv0 32）））））（let（（x24（bvand？x21（ite（bvsgt（（_ sign_extend 24）（_ bv98 8））（（__ sign_extend 24）| Mem5 [8] |））（_ bv128 32）（_ bv0 32）））））（__ bv97 8））（（__ sign_extend 24）| Mem6 [8] |））（_ bv64 32）（_ bv0 32）））））（bvand？x37（ite（bvsgt（（_ sign_extend 24）（__ sign_extend 24）| Mem6 [8] |））（_ bv128 32）（_ bv0 32））））））

來源

2012-03-27 Heyji

此功能相當陳舊。它是在SMT 2.0不存在時創建的。 SMT 1.0基準測試看起來像這樣：

(benchmark example 
:status sat 
:logic QF_LIA 
:extrafuns ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int)) 
:assumption (>= (- x1 x2) 1) 
:assumption (>= (- x1 x2) 3) 
:assumption (= x3 x5) 
:formula (= x2 (* 6 x4)) 
)

您正在使用的功能是用於生成此格式的基準。這就是爲什麼我們有參數如name,logic,status等。它們對應於上面示例中的註釋。此外，SMT 1.0問題由0個或更多的假設和1個公式組成。

當SMT 2.0被引入，該方法被擴展在SMT打印基準2.0格式，當我們有

Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT);

奇怪字符是用於在打印公式時避免指數爆破只是輔助let聲明。請注意，Z3 AST是DAG而不是樹。使用具有大量共享的C API創建DAG非常簡單。例如：

a_1 = Z3_mk_bvadd(b, c) 
a_2 = Z3_mk_bvmul(a1, a1) 
a_3 = Z3_mk_bvadd(a2, a2) 
a_4 = Z3_mk_bvmul(a3, a3) 
...

AST a_100是一個非常緊湊的內存對象。如果我們試圖在不使用輔助let聲明的情況下將其打印爲樹，則輸出將非常巨大。

請注意，這個函數產生的輸出從來不會被人類消耗掉。它主要用於爲SMT-LIB存儲庫生成基準。

來源

2012-03-28 08:08:08

Z3_benchmark_to_smtlib_string（）的輸入參數

回答

相關問題