2

たとえば、以下のコードでは、パス条件はになります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.

ありがとう

4

1 に答える 1

1

Z3 API を使用すると、 and ( function);をアサートすることでA暗黙的かどうかを確認できます。結果が満足できないかどうかをチェックします（関数）。簡単なアイデアの 1 つは、Z3 コンテキストでパス条件をアサートし続けることです。をアサートする前に、コンテキストによって暗示されているかどうかを確認します。これは、次の C コードを使用して実現できます。BAnot BZ3_assert_cnstrZ3_checkA

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)、期待どおりに生成されます。これは、はるかに安価な (ただし不完全な) メソッドに基づいています。もう 1 つの問題は、この機能が対話型シェルでしか利用できないことです。次のリリースでは、これらの機能をプログラム API で利用できるようにする予定です。

于 2011-11-19T02:14:44.377 に答える