我是 Z3 的新手，仍然找不到如何根据不同的可能评估来表达有条件的新任务。在 https://github.com/Z3Prover/z3/blob/master/examples/c/test_capi.c#L1846的 If-then-else 示例中， 我仍然需要将分配设置为 true 或 false，并且当我想要根据对另一个变量的可能评估使其为真或假。我怎样才能做到这一点？
在评估示例中，我希望计算的值用于影响稍后将通过断言检查的仍未评估的值。因此，如果这是我如何将使用新的（基于评估的）条件评估的模型再次返回到上下文的方式？即我想做没有最终评估的复合条件。那可能吗？
以下行来自ite_example()：
ite = Z3_mk_ite(ctx, f, one, zero)
创建一个表达式，该表达式将计算（符号）项的one计算结果，如果f计算结果为真，或者zero计算结果为任何结果，如果f计算结果为假。在ite_example中，f总是计算为false，但它可能是布尔排序的任何其他（符号）项。
例如，
x = mk_int_var(ctx, "x");
y = mk_int_var(ctx, "y");
x_eq_y = Z3_mk_eq(ctx, x, y);
将创建一个名为 的术语x_eq_y，表示“x = y”，它是布尔排序的。