Z3用户传播器中表达式注册问题的解析

问题背景

在使用Z3求解器的用户传播器(UserPropagator)功能时，开发者可能会遇到"expression is not registered"的错误提示。这个问题通常出现在尝试使用conflict函数的eqs参数时，表明某些表达式没有被正确注册到传播器系统中。

用户传播器基础

Z3的用户传播器是一种强大的扩展机制，允许开发者自定义约束传播逻辑。通过继承UserPropagateBase类并实现相应回调函数，开发者可以：

1. 注册需要监控的变量
2. 在变量被固定时接收通知
3. 主动触发冲突或传播新约束

错误原因分析

在原始代码中，开发者试图在_fixed回调函数中使用conflict方法的eqs参数来报告一个等式冲突：

def _fixed(self, ast, value):
    self.conflict(deps=[], eqs=[(ast, value)])

这里的问题在于eqs参数是专门用于处理通过add_eq回调注册的等式约束的。如果没有为这些表达式注册等式回调，Z3就无法识别它们，从而导致"expression is not registered"错误。

正确使用方法

正确的做法是使用deps参数来报告由固定变量引起的冲突：

def _fixed(self, ast, value):
    self.conflict(deps=[ast])

deps参数应该包含所有导致冲突的固定表达式。在这个例子中，当变量ast被固定为value时，我们直接将这个固定事件作为冲突的来源。

深入理解参数区别

1. deps参数：用于传递所有导致冲突的固定表达式，这些表达式必须是通过add方法注册过的变量。

2. eqs参数：专门用于处理通过add_eq回调注册的等式约束。只有当开发者实现了等式传播逻辑并注册了相关回调时，才能使用这个参数。

实际应用建议

在实际开发中，如果只是想基于变量的固定值来触发冲突，使用deps参数是最简单直接的方法。只有在需要处理复杂等式关系时，才需要考虑实现add_eq回调并使用eqs参数。

总结

理解Z3用户传播器中不同参数的使用场景对于正确实现自定义传播逻辑至关重要。deps和eqs服务于不同的目的，开发者需要根据具体需求选择合适的参数。当遇到"expression is not registered"错误时，检查表达式是否已正确注册以及是否使用了正确的参数类型是解决问题的关键步骤。