将值赋给Z3中的bool变量C api

Question

我是Z3的新手。

我定义了一个bool类型变量a：
Z3_sort bool_type = Z3_mk_bool_sort（ctx）;
Z3_ast a = Z3_mk_const（ctx，Z3_mk_string_symbol（ctx，“a”），bool_type）;

我的问题是我如何分配不同的值给一个，似乎我不能直接分配Z3_L_TRUE它。

有什么建议吗？谢谢！

Answer 1

我的第一个建议是使用C++ API而不是C API。 使用C API非常容易出错。分布自带同时使用C和C++ API的例子：

https://github.com/Z3Prover/z3/blob/master/examples/c/test_capi.c

和

https://github.com/Z3Prover/z3/blob/master/examples/c++/example.cpp

你有看到创建逻辑变量的例子，比如你正在做的， 并添加约束逻辑变量的断言。 使用基于文本的API来理解逻辑建模更容易。 也就是说，我建议您使用SMT-LIB格式来模拟您的打算， ，这给您一种推断如何处理编程API的方法。

关于你的问题：在逻辑建模中没有“赋值”的概念。 你可以肯定地坚持平等。此外，当您检查可满足性时，Z3_L_TRUE是使用 的返回码。您可以使用方法Z3_mk_true创建逻辑常量“true”。