0

次のコードはin 式 に変更2されます。3e1

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)は機能しません。2 番目の質問は、Z3_AST の任意の深さで式を変更する方法e1.arg(1).arg(0) = e2.arg(1).arg(1)です。

4

1 に答える 1

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;
}
于 2013-05-23T15:18:55.240 に答える