【发布时间】：2014-10-25 09:25:31
【问题描述】：
从之前在 StackExchange 上提出的许多问题中，我了解到该理论 插件现在在 Z3 4.x 中已被弃用，现在预计需要编写自己的理论求解器并从头开始编译 Z3。
但是，我找不到有关如何实施此类新理论求解器的任何指南和/或简单的工作示例。有没有我错过的地方已经可用？如果没有，有没有人写了一个新的理论求解器来分享代码？
【问题讨论】：
标签： z3
【发布时间】：2014-10-25 09:25:31
【问题描述】：
目前还没有新理论的官方示例或文档。首先，您应该决定您是否需要一个与 smt 内核中的所有其他理论集成的实际理论，或者您的目标是否可以在一个策略内实现（这可能需要更少的编码工作）。
我目前正在研究浮点数的理论插件，这是一个特别简单的理论，因为它只将浮点约束转换为位向量（然后是布尔值）。这部分还没有在master分支中，但是你可以在src/smt/theory_fpa.cpp/.h的fpa-api分支中看到它（确保在网页上选择了正确的分支，否则你只会看到尚未实现的存根.)
【讨论】：
-
我查看了有关 Z3 C/C++/Python API 的理论_fpa、策略和所有文档。如果我是对的，我没有在您的代码中看到任何添加到 Z3 引擎的回调的原因是您的理论没有做额外的推理。也就是说，位向量可以完全表示 fpa，并且 theory_fpa 真正充当接口，使用户能够使用数字而不是位序列。但是，我对具有额外推理能力的理论感兴趣，例如 Nikolaj 关于工程新理论的论文。是否有任何简单的理论实现，例如那些理论？如果没有，我会有更具体的问题。
-
没错，theory_fpa 就是一个特别简单的例子。为此，我不知道其他类似的简单示例。不过，在高层次上，这里唯一缺少的是assign_eh 和final_check。您必须决定要在 assign_eh 中完成多少工作，以及调用 final_check 时将完成多少工作。当然，您也可以查看所有其他理论实现。 src/smt/smt_theory.h 包含具有大量 cmets 的理论的基类。