SMT约束求解器Z3——java绑定

Z3是由微软公司开发的一个优秀的SMT求解器（也就定理证实器），它可以检查逻辑表达式的可知足性。html 1.下载 准备必要的组件：下载对应版本的Z3 编译文件，版本下载连接https://github.com/z3prover/z3/releasesjava 2.解压缩 3.项目导入 在Java项目中新建一个libs文件夹（若是没有的话），将z3\bin目录下的com.microsoft.z3.

>>阅读原文<<