z3 - 使用 z3_update_term 函数进行术语更新

Question

以下代码更改2为3in 表达式e1。

context z3_cont;
expr x = z3_cont.int_const("x");
expr e1 = (x==2);
expr e2 = (x==3);
Z3_ast ee[2];
ee[0]=e1.arg(0);
ee[1]=e2.arg(1);
e1 = to_expr(z3_cont,Z3_update_term(z3_cont,e1,2,ee));

有没有可能做得更容易？不幸的是，代码e1.arg(1) = e2.arg(1)不起作用。第二个问题是如何更改 Z3_AST 任意深度的表达式，例如e1.arg(1).arg(0) = e2.arg(1).arg(1)？

Answer 1

您可以使用Z3_substituteAPI。这是一个例子：

void substitute_example() {
    std::cout << "substitute example\n";
    context c;
    expr x(c);
    x = c.int_const("x");
    expr f(c);
    f = (x == 2) || (x == 1);
    std::cout << f << std::endl;

    expr two(c), three(c);
    two   = c.int_val(2);
    three = c.int_val(3);
    Z3_ast from[] = { two };
    Z3_ast to[]   = { three };
    expr new_f(c);
    // Replaces the expressions in from with to in f. 
    // The third argument is the size of the arrays from and to.
    new_f = to_expr(c, Z3_substitute(c, f, 1, from, to));

    std::cout << new_f << std::endl;
}

更新如果我们想x == 2用x == 3公式替换，我们应该写。

void substitute_example() {
    std::cout << "substitute example\n";
    context c;
    expr x(c), y(c);
    x = c.int_const("x");
    y = c.int_const("y");
    expr f(c);
    f = (x == 2) || (y == 2);
    std::cout << f << std::endl;

    expr from(c), to(c);
    from  = x == 2;
    to    = x == 3;
    Z3_ast _from[] = { from };
    Z3_ast _to[]   = { to };
    expr new_f(c);
    // Replaces the expressions in from with to in f. 
    // The third argument is the size of the arrays from and to.
    new_f = to_expr(c, Z3_substitute(c, f, 1, _from, _to));

    std::cout << new_f << std::endl;
}