model - Z3如何生成模型？

Question

我目前正在使用 SMT 求解器 Z3 研究模型计数方法。有谁知道 Z3 如何为线性算术 (LIA) 生成模型？使用了哪种算法，在哪里可以找到该算法的源代码？

谢谢， 雅尼克

Answer 1

Z3 的源代码在https://github.com/z3prover/z3.git上。有几个算术求解器。Z3 通常使用双 Simplex。