在z3中设置LIA逻辑

Question

我尝试使用python接口为LIA实例使用一种特定的策略。我试图使用：

solver = Tactic('lia').solver()

不幸的是，我收到了“未知战术”的信息。当我改为使用qflia时，也是一样的。对于这种情况，我能做些什么来使用最好的策略呢？在

Answer 1

没有针对LIA问题的定制策略，但是有一种针对QF_LIA（即无量词的LIA）的策略，称为“qflia”，因此它不应该报告错误。这对我有用：

from z3 import *

s = Tactic('qflia').solver()

x = Int('x')
s.add(x < 5)
print(s.check())