关于C++版本z3库的使用心得

C++版本的z3库使用起来要比python要复杂一些，而且网上也没有python版本那么多的教程，自己使用了一段时间，逐渐上手，把自己使用过的一些网站和一些使用心得系统的记录一下：

一、使用学习Z3的一些常用网址：

1.官方给的C++z3示例：

2.z3的API大全：

3.一个比较全的z3示例网站：

4.简易教程（有些不能用的在下面会说）：

6.chatgpt，多问，多试：

二、一些常用的技巧:

1.环境语句的位置：

如果要创建全局环境，直接在命名空间之后创建即可，如图：

2.二维数组的构建：

3.与或关系的写法：

不能直接简单地用&&或者||来实现与或关系，会报错，建议是用expr关键字写好，然后直接在求解器中添加最后的关键字，如图：

4.函数的输出（整型、浮点数类型）：

我们在用求解器的时候，常常是封装在函数中使用，通常需要对求解器求得的模型值进行输出，在这其中，整型和浮点型的转化方法也略有不同，不能想python中一样直接粗暴的输出。下面是我写过的两个整型和浮点型的示例：

（1）整型：

（2)浮点型：

其他类型也有对应的转化关键字，用到哪种查哪种即可。