因为课程要求，我不得不接触求解器，之前有在ubuntu上装过一个叫stp的求解器，没怎么用；
今天在我的电脑（win10）上上装了一款更方便的求解器---z3，下面先详细介绍一下怎么安装和配置：
1、到 https://github.com/Z3Prover/z3 下载z3-master，如下图：
2、到 https://www.visualstudio.com/zh-hans/ 下载vs2017，选择下图中的大绿色对勾的选项下载（安装要等好久）：
3、配置python的环境变量。我的电脑→属性→高级系统设置→环境变量→双击系统变量中的Path→新建→用 "浏览"选择刚刚安装的Python的路径。
然后一直点确定就可以了，在cmd中输入python命令检查是否配置成功，如果没有，可以看这篇博客末尾的推荐链接。
4、打开vs2017开发人员命令提示符，用cd打开你的z3-master，输入 python scripts/mk_make.py -x
正常情况下会出现包含"build && nmake"的语句，然后输入cd build，再输入nmake；然后等上一段时间，这段时间啥也别做，看着屏幕就可以，
最后出现 Z3 was successfully built 就说明你的z3已经安装好了。
5、再给z3配置一下环境变量，跟配置Python的环境变量一样，路径需要配置到build。好了现在你可以在你cmd中输入z3 -h，看一下会出现什么吧。
6、为了进一步验证我们安装的z3能不能用，可以这样来。
打开vs2017开发人员命令提示符，进入build目录，然后输入 nmake examples；去看一下build目录下多了一个叫 cpp_example.exe的应用程序，
用cmd运行一下这个exe，你会看到一长串结果，这就说明我们的z3可以用了。
再来给出几个对想用求解器的同志有用的链接：
1、z3的安装和配置 ：https://blog.csdn.net/weixin_41529962/article/details/80274125
https://blog.csdn.net/weixin_41529962/article/details/80295088
https://blog.csdn.net/buaa1214wwj/article/details/53056238
2、Python环境变量的配置：https://www.cnblogs.com/huangbiquan/p/7784533.html
3、smt-lib的相关链接：http://smtlib.cs.uiowa.edu/news.shtml
好了，就先到这吧，明天还要复习，后边想到什么再补充。
这篇博客仅仅是供我自己纪念和参考用，没什么高深的技术，希望各位多多指教。