在z3中使用战术时有空未饱和核数

Question

使用战术时，Solver返回空的unsat核心。

案例1：

s = Solver()
x = Real('x')
B = Bool('b')
C = Bool('c')
s.add(B == (x > 1))
s.add(C == (x == -1))
s.check(B, C)

案例2：

s = Then('simplify', 'solve-eqs', 'smt').solver()
x = Real('x')
B = Bool('b')
C = Bool('c')
s.add(B == (x > 1))
s.add(C == (x == -1))
s.check(B, C)

[在两种情况下，支票都会返回unsat（应有），但是在第二种情况下，我使用战术时会得到一个空的unsat核心。在使用带有策略的求解器时，有什么方法可以使不满意的核心？

PS：这些确实是简单的演示示例。我正在处理一个更大的问题，我遇到了许多LRA约束（在这种策略可能会有所帮助的情况下），我需要提取未饱和的核。

Answer 1

如果您使用战术，则需要显式启用unsat核心。以下作品：

from z3 import *
s = Then('simplify', 'solve-eqs', 'smt').solver()
s.set(unsat_core=True)
x = Real('x')
B = Bool('b')
C = Bool('c')
s.add(B == (x > 1))
s.add(C == (x == -1))
s.check(B, C)

print s.unsat_core()

注意第三行对s.set的呼叫。输出：

$ python b.py
[b, c]