有什么办法可以简化路径条件

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和not B（Z3_assert_cnstr函数）来检查A是否暗示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 中提供这些功能。