简化涉及有限域变量的表达式

Question

ctx-solver-simplify 策略仅适用于布尔变量，那么我将如何处理有限域上的变量（例如，使用哪种策略）？比如z只能取3个值0,1,2，那么如何将Or(z==0,z==1,z==2)简化为true？

此外，即使是布尔表达式，ctx-solver-simplify 的策略也没有完全简化。例如：

x,y,z = z3.Bools('x y z')
c1 = z3.And(x==True,y==True,z==True)
c2 = z3.And(x==True,y==True,z==False)
c3 = z3.And(x==True,y==False,z==True)
c4 = z3.And(x==True,y==True,z==False)
z3.Tactic('ctx-solver-simplify')(z3.Or([c1,c2,c3,c4]))
[[Or(And(x, z), And(x == True, y == True, z == False))]]

如何获得And(x, Or(z, y)) 之类的信息？

谢谢！

Answer 1

将布尔（或其他有限域）问题简化为最小形式是一个难题。 ctx-solver-simplify 策略是更昂贵的简化器之一，但它并没有一直到可证明的最小形式。

来自其他领域的问题（例如，像 z \in {0, 1, 2} 这样的枚举）必须首先转换为布尔值才能使用这种策略，但也许其他策略会更适合，也许有点-矢量编码也会有所帮助。