Есть ли способ упростить условия пути - PullRequest
Новая
       18

Есть ли способ упростить условия пути

2 голосов
/ 19 ноября 2011

Например, в приведенном ниже коде условие пути будет 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.

Спасибо

1 Ответ

1 голос
/ 19 ноября 2011

С помощью API Z3 вы можете проверить, подразумевает ли A B, утверждая A и not B (функция Z3_assert_cnstr);и проверка того, является ли результат неудовлетворительным или нет (функция Z3_check).Одна простая идея состоит в том, чтобы продолжать утверждать условия пути в контексте Z3.Перед утверждением A вы проверяете, подразумевается ли это контекстом или нет.Вы можете сделать это, используя следующий фрагмент кода.

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 в следующем выпуске.

...