Z3如何生成模型？

Question

我目前正在使用SMT求解器Z3進行模型計數。有誰知道Z3是如何爲例如線性算術（LIA）？使用哪種算法以及哪裏可以找到該算法的源代碼？

謝謝，爲Z3 Yannic

Answer 1

的源代碼是上https://github.com/z3prover/z3.git。 有幾個算術解算器。 Z3通常使用雙Simplex。