查找"Horn"求解器对象的反例

Question

我正在努力学习如何编写代码，为horn子句提供反例，这是猜测的解释。在下面的代码中，让我成为未解释的函数(它是一个平凡的循环不变量(。前3个s.add((添加了I(x(的条件要求，第四个是I的猜测候选者。我试图使用s.prove指令来获得我猜测的I候选者的反例。在运行此代码时，我似乎收到了一个巨大的错误日志，有人能告诉我出了什么问题吗？

s = SolverFor("HORN")
I = Function('I', IntSort(), BoolSort()) 
x, x2 = Ints('x x2') 
s.set("produce-proofs", True)
s.add( ForAll( [x] ,Implies( x == 0  , I(x))) ) 
s.add( ForAll( [x, x2]  , Implies ( And( I(x), x2 == x + 1 , x < 5) ,  I(x2) )  ) ) 
s.add( ForAll( [x] ,Implies( And( I(x), Not(x < 5) ) , x == 5 ) ) ) 
s.add( ForAll( [x],  And( Implies( I(x) , (x == 2) ), Implies( (x == 2) , I(x) ) ) ) ) #Adding guessed invariant here!
assert unsat == s.check()
print(s.proof()) 

Answer 1

脚本中有几个错误；也许这可以追溯到不久前z3的另一个版本？在任何情况下，z3版本4.8.14都会执行以下操作：

from z3 import *
s = SolverFor("HORN")
I = Function('I', IntSort(), BoolSort())
x, x2 = Ints('x x2')
s.set("proof", True)
s.add( ForAll( [x] ,Implies( x == 0  , I(x))) )
s.add( ForAll( [x, x2]  , Implies ( And( I(x), x2 == x + 1 , x < 5) ,  I(x2) )  ) )
s.add( ForAll( [x] ,Implies( And( I(x), Not(x < 5) ) , x == 5 ) ) )
s.add( ForAll( [x],  And( Implies( I(x) , (x == 2) ), Implies( (x == 2) , I(x) ) ) ) ) #Adding guessed invariant here!
print(s.check())

不幸的是，它打印：

unknown

这意味着求解器无法确定输入是否可满足；它放弃并说CCD_ 1。早期版本的求解器可能已经能够成功地解决这个问题，提供了一个不令人满意的证明，或者一个模型，如果它是令人满意的。

我建议你追踪这个例子的来源，并找出他们使用的是z3的哪个版本。回到那个版本可能会帮助你取得进步。或者，如果您认为问题应该可以按原样解决，您可以在https://github.com/Z3Prover/z3/issues