我有以下代码：

from clingo import Control

def on_model(m):
    print(m, m.optimality_proven)

ctl = Control(["0"])
ctl.add("base", (), "0 { a } 1. :~ a. [-1@0]")
ctl.ground([("base", ())])
solution = ctl.solve(on_model=on_model)
assert solution.exhausted

当我运行它时，输出是：

False
a False

我不明白为什么会这样 optimality_proven 标志设置为 False 在第二种情况下。clingo首先检查空模型，这是次优的，然后检查包含单个原子的模型 a ，这是最优的。但出于某种原因，它不知道它是最优的，即使搜索已经用尽了？这是不是因为只有在检查了这个模型后才会耗尽能量？但是，我怎样才能让这面旗子永远挂在墙上呢 True ? 我的意思是，我可以做一些变通方法，比如在数据库中存储和比较生成的模型 on_model 函数来检查自己的最佳性，但考虑到api提示该函数已经可用，这感觉非常不自然 optimality_proven 属性