Z3使用哪种背后理论来证明约束不可满足？

Z3使用了许多不同的背后理论来证明约束不可满足，包括但不限于线性算术理论、位向量理论、数组理论和非线性实数算术理论等等。在默认情况下，Z3使用一组经过良好测试的默认理论，称为LRA（线性实数算术）。可以使用Z3 API来选择不同的理论或自定义自己的规则组合。

下面是一个使用Z3 API来指定使用LIA（线性整数算术）理论的Python示例：

from z3 import *

x = Int('x')
y = Int('y')
s = Solver()

# 使用LIA理论
s.set( 'theory.auto_config', False )
s.set( 'smt.arith.nl', False )
s.set( 'smt.arith.lia', True )

# 添加约束
s.add( x + y > 5 )
s.add( x - y < 7 )

# 检查是否为不可满足
print( s.check() )

在这个示例中，我们使用了Int定义整数类型的变量x和y。我们还创建了一个s变量来保存Solver对象。我们通过s.set()方法来指定我们要使用的LIA理论，并使用s.add()方法添加约束。最后，我们使用s.check()方法来检查约束是否不可满足。