在 Z3 中:如何制定基于其他条件的条件(基于变量的评估)

Question

我是 Z3 的新手，仍然找不到如何根据不同的可能评估来表达有条件的新赋值。在 If-then-else 示例中https://github.com/Z3Prover/z3/blob/master/examples/c/test_capi.c#L1846我仍然需要将赋值为 true 或 false，以及当我想根据对另一个变量的可能评估使其为真或假时。我该怎么做？

在评估示例中，我希望计算的值用于影响稍后将通过断言检查的仍未计算的值。因此，如果这是我如何将具有新的（基于评估的）条件的联合国评估模型再次返回到上下文中的方式？即我想在没有最终评估的情况下做复合条件。这可能吗？

Answer 1

ite_example()中的以下行：

ite  = Z3_mk_ite(ctx, f, one, zero)

创建一个表达式，该表达式将计算为one计算的（符号）项的任何内容（如果f计算结果为 true），或者如果f计算为 false，则计算结果为zero计算的任何内容。在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"，它是布尔排序的。