因為課程要求，我不得不接觸求解器，之前有在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
好了，就先到這吧，明天還要復習，后邊想到什么再補充。
這篇博客僅僅是供我自己紀念和參考用，沒什么高深的技術，希望各位多多指教。