z3中的unsat核心函数
假设我使用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))) 我想使用post中的以下代码片段从这个连接中提取每个单独的断言：How to use z3 split clauses of unsat cores & try to find out unsat core again
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))) model是真或假，如何获得x = 1, y = -1等算术值
非常感谢您的任何建议。非常感谢。
回答 1
Stack Overflow用户
发布于 2012-11-29 14:57:55
当为F = F.simplify()时，表达式(< (+ x y) 3)将转换为(not (<= 3 (+ x y)))。在您使用的代码片段中，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";
}
}https://stackoverflow.com/questions/13531738
复制相似问题
腾讯云开发者
