Например, в приведенном ниже коде условие пути будет 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.
Спасибо
Например, в приведенном ниже коде условие пути будет 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.
Спасибо
С помощью Z3 API вы можете проверить, подразумевает ли A
B
, установив A
и not B
(функция Z3_assert_cnstr
); и проверка того, является ли результат неудовлетворительным или нет (функция 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)
, как и ожидалось. Он основан на гораздо более дешевых (но неполных) методах. Другая проблема заключается в том, что этот функционал доступен только в интерактивной оболочке. Планируется, что эти возможности будут доступны в программном API в следующем выпуске.