2

假设我使用 API 阅读了 SMTLIB 公式：

context ctx;
...
expr F = to_expr(ctx, Z3_parse_smtlib2_file(ctx,argv[1],0,0,0,0,0,0));

该表达式F是以下形式的断言的合取：

(and (< (+ x y) 3)
     (> (- x1 x2) 0)
     (< (- x1 x2) 4)
     (not (= (- x1 x2) 1))
     (not (= (- x1 x2) 2))
     (not (= (- x1 x2) 3)))

我想使用帖子中的以下代码片段从这个连词中提取每个单独的断言：如何使用未饱和核心的 z3 拆分子句并尝试再次找出未饱和核心

    F = F.simplify();
    for (unsigned i = 0; i < F.num_args(); i++) {
        expr Ai = F.arg(i);
        // ... Do something with Ai, just printing in this example.
        std::cout << Ai << "\n";
    }

使用后F.arg(i)，原来的从句(< (+ x y) 3)变成了(not (<= 3 (+ x y)))。这是我的

a) 问题：我怎样才能把子句(not (<= 3 (+ x y)))放在(< (+ x y) 3)？

b) 问题：在这种情况下，我认为符号的<=意思是暗示，而不是小于。我对吗？

c）问题：由于子句(not (<= 3 (+ x y)))模型是真还是假，我怎样才能得到算术值，例如x = 1, y = -1？

非常感谢任何建议。非常感谢。

4

1 回答 1

2

表达式(< (+ x y) 3)转换为(not (<= 3 (+ x y)))when F = F.simplify()。在您使用的代码片段中，该方法simplify()用于“扁平化”嵌套的“and”。也就是说，公式(and (and A B) (and C (and D E)))被展平为(and A B C D E). 然后，可以使用 for 循环轻松遍历所有合取项。但是，它simplify()还将在输入公式中执行其他转换。请记住，所有转换都保持等效性。即输入和输出公式在逻辑上是等价的。如果simplify()不希望应用的转换，我建议您避免使用此方法。如果还想遍历嵌套的“and”，可以使用辅助todo向量。这是一个例子：

expr_vector todo(c);
todo.push_back(F);
while (!todo.empty()) {
    expr current = todo.back();
    todo.pop_back();
    if (current.decl().decl_kind() == Z3_OP_AND) {
        // it is an AND, then put children into the todo list
        for (unsigned i = 0; i < current.num_args(); i++) {
            todo.push_back(current.arg(i));
        }
    }
    else {
        // do something with current
        std::cout << current << "\n";
    }
}
于 2012-11-29T06:57:55.463 回答