我正在尝试对z3做些奇怪的事情。我正在尝试看看我是否可以使用z3从交互式定理证明者那里获得类似“应用”策略的信息。我有一个像ForAll([x], Implies(a(x),b(x))的定理，并且对于c的适当选择，目标b(x)在语法上等于x。如果可以正确实例化x，则可以将目标c替换为a(inst_x)。有没有一种方法可以使用z3获得适当的x？我不能只使用模型，因为c可能包含自由变量。
我一直在尝试是否可以在z3证明词中为Implies(ForAll([x],b(x)), c)之类的查询找到它，或者以某种方式使用E匹配模式工具，但是我很困惑。
z3内部必须具有复杂的匹配和统一功能，但我看不到它们在python界面中可能显示的位置。
建议？谢谢
这些都不能通过z3当前支持的任何API来使用，而且绝对不是Python层。最好的选择是直接使用z3本身的源代码并添加必要的钩子。不用说，这将需要深入研究源代码，并确保它随着z3本身的发展而保持最新。