Z3 的参考资料 - 它是如何工作的[内部理论]？
References for Z3 - how does it work[internal theory]?
我有兴趣阅读 Z3 背后的内部理论。具体来说，我想阅读 Z3 SMT 求解器的工作原理，以及它如何为不正确的模型找到反例。我希望能够为一些非常简单的示例手动计算出轨迹。
不过，所有的Z3参考好像都是怎么编码的；或对其算法的非常高级的描述。我找不到所用算法的描述。此信息不是由 Microsoft public 提供的吗？
任何人都可以引用任何参考文献 (papers/books) 来全面了解 Z3 的理论 + 工作吗？
我个人认为最好的参考资料是 Kroening 和 Strichman 的 Decision Procedures book. (Make sure to get the 2nd edition as it has good updates!) It covers almost all topics of interest to certain depth, and has many references at the back for you to follow up on. The book also has a website http://www.decision-procedures.org 以及额外的阅读材料、幻灯片和项目想法。
该领域的另一本有趣的书是 Bradley 和 Manna 的 The Calculus of Computation. While this book isn't specific to SAT/SMT, it covers many of the similar topics and how these ideas play out in the realm of program verification. Also see http://theory.stanford.edu/~arbrad/pivc/index.html 相关 software/tools。
当然，这两本书都不是特定于 z3 的，因此您不会在其中找到任何关于 z3 本身是如何构造的详细信息。对于 z3 的编程及其背后的一些理论，Bjørner、de Moura、Nachmanson 和 Wintersteiger 的 "tutorial" paper 是一本很好的读物。
完成这些后，我建议您阅读开发人员的个别论文，具体取决于您的兴趣所在：
比约纳：https://www.microsoft.com/en-us/research/people/nbjorner/publications/
德莫拉：https://www.microsoft.com/en-us/research/people/leonardo/publications/
温特施泰格：https://www.microsoft.com/en-us/research/people/cwinter/publications/
纳赫曼森：https://www.microsoft.com/en-us/research/people/levnach/publications/
当然，互联网上有大量资源、许多论文、演示文稿、幻灯片等。您可以直接在本论坛中随意提问具体问题，或者对于真正的 z3 内部具体问题，您可以使用他们的discussions forum.
注关于Kroening和Strichman的书的版本差异，作者是这样说的：
The first edition of this book was adopted as a textbook in courses worldwide. It was published in 2008 and the field now called SMT was then in its infancy, without the standard terminology and canonic algorithms it has now; this second edition reflects these changes. It brings forward the DPLL(T) framework. It also expands the SAT chapter with modern SAT heuristics, and includes a new section about incremental satisfiability, and the related Constraints Satisfaction Problem (CSP). The chapter about quantifiers was expanded with a new section about general quantification using E-matching and a section about Effectively Propositional Reasoning (EPR). The book also includes a new chapter on the application of SMT in industrial software engineering and in computational biology, coauthored by Nikolaj Bjørner and Leonardo de Moura, and Hillel Kugler, respectively.
我有兴趣阅读 Z3 背后的内部理论。具体来说，我想阅读 Z3 SMT 求解器的工作原理，以及它如何为不正确的模型找到反例。我希望能够为一些非常简单的示例手动计算出轨迹。
不过，所有的Z3参考好像都是怎么编码的；或对其算法的非常高级的描述。我找不到所用算法的描述。此信息不是由 Microsoft public 提供的吗？
任何人都可以引用任何参考文献 (papers/books) 来全面了解 Z3 的理论 + 工作吗？
我个人认为最好的参考资料是 Kroening 和 Strichman 的 Decision Procedures book. (Make sure to get the 2nd edition as it has good updates!) It covers almost all topics of interest to certain depth, and has many references at the back for you to follow up on. The book also has a website http://www.decision-procedures.org 以及额外的阅读材料、幻灯片和项目想法。
该领域的另一本有趣的书是 Bradley 和 Manna 的 The Calculus of Computation. While this book isn't specific to SAT/SMT, it covers many of the similar topics and how these ideas play out in the realm of program verification. Also see http://theory.stanford.edu/~arbrad/pivc/index.html 相关 software/tools。
当然，这两本书都不是特定于 z3 的，因此您不会在其中找到任何关于 z3 本身是如何构造的详细信息。对于 z3 的编程及其背后的一些理论，Bjørner、de Moura、Nachmanson 和 Wintersteiger 的 "tutorial" paper 是一本很好的读物。
完成这些后，我建议您阅读开发人员的个别论文，具体取决于您的兴趣所在：
比约纳：https://www.microsoft.com/en-us/research/people/nbjorner/publications/
德莫拉：https://www.microsoft.com/en-us/research/people/leonardo/publications/
温特施泰格：https://www.microsoft.com/en-us/research/people/cwinter/publications/
纳赫曼森：https://www.microsoft.com/en-us/research/people/levnach/publications/
当然，互联网上有大量资源、许多论文、演示文稿、幻灯片等。您可以直接在本论坛中随意提问具体问题，或者对于真正的 z3 内部具体问题，您可以使用他们的discussions forum.
注关于Kroening和Strichman的书的版本差异，作者是这样说的：
The first edition of this book was adopted as a textbook in courses worldwide. It was published in 2008 and the field now called SMT was then in its infancy, without the standard terminology and canonic algorithms it has now; this second edition reflects these changes. It brings forward the DPLL(T) framework. It also expands the SAT chapter with modern SAT heuristics, and includes a new section about incremental satisfiability, and the related Constraints Satisfaction Problem (CSP). The chapter about quantifiers was expanded with a new section about general quantification using E-matching and a section about Effectively Propositional Reasoning (EPR). The book also includes a new chapter on the application of SMT in industrial software engineering and in computational biology, coauthored by Nikolaj Bjørner and Leonardo de Moura, and Hillel Kugler, respectively.