有什麼方法可以簡化路徑條件

Question

例如，在下面的代碼中路徑條件將是x>0 && x+1>0。但由於x>0意味着x+1>0，有沒有什麼辦法可以在z3或pex API中只獲得x>0而不是兩者。

if(x>0) 
if(x+1>0) 
    //get path condition. 

感謝

Answer 1

隨着Z3 API，你可以檢查是否A通過聲明A和not B（Z3_assert_cnstr功能）意味着B;並檢查結果是否不令人滿意（Z3_check函數）。一個簡單的想法是繼續在Z3上下文中聲明路徑條件。在斷言A之前，請檢查它是否由上下文暗示。您可以使用以下C代碼完成該操作。

Z3_push(ctx); // create a backtracking point 
Z3_assert_cnstr(ctx, Z3_mk_not(ctx, A)); 
Z3_lbool r = Z3_check(ctx); 
Z3_pop(ctx); // remove backtracking point and 'not A' from the context 
if (r != Z3_L_FALSE) 
    Z3_assert_cnstr(ctx, A); // assert A only if it is not implied. 

Z3 3.2有一個小語言來指定求解和簡化表達式的策略。 在這種語言，你可以這樣寫：

(declare-const x Int) 
(assert (> x 0)) 
(assert (> (+ x 1) 0)) 
(apply (and-then simplify propagate-bounds)) 

這個簡單的戰略將產生(>= x 1)預期。它基於更便宜（但不完整）的方法。 另一個問題是此功能僅在交互式shell中可用。 該計劃是在下一版本的程序化API中提供這些功能。