TSN领域有很多文章使用z3 solver求解约束可满足性问题。典型的工作包括Silviu S. Craciunas 等人的Scheduling Real-Time Communication in IEEE 802.1Qbv Time Sensitive Networks。前些年用过z3 solver试图尝试复现他们的工作，在这里总结下手动安装z3的教程。
下载安装visual studio Community 2019
下载地址： https://learn.microsoft.com/zh-cn/visualstudio/releases/2019/release-notes
安装教程参考： https://zhuanlan.zhihu.com/p/94998894
选择工作负载时，可勾选使用C++的桌面开发或Python 开发，看你习惯什么编程语言了
下载python 3.6.7
下载及安装教程参考：https://www.cnblogs.com/lvtaohome/p/11121377.html
下载并解压z3-master包 ，我这里它放到了电脑d盘下
下载z3地址： https://github.com/Z3Prover/z3
打开开始菜单，在Visual Studio 2019文件夹下找到x86-x64 Cross Tools Command prompt for VS2019，打开后依次输入
d:cd z3-masterpython scripts/mk_make.py -xcd buildnmake等待一段时间后，就会出现z3 was successfully built