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

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隐含；并检查结果是否不可满足（函数）。一个简单的想法是在 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)预期产生。它基于便宜得多（但不完整）的方法。另一个问题是此功能仅在交互式 shell 中可用。计划是在下一版本的编程 API 中提供这些功能。