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

Question

我正在尝试学习如何编写代码以给出 horn 从句的反例及其猜测的解释。在下面的代码中，让 I 成为未解释的函数（这是一个简单的循环不变量）。前3个s.add()为I(x)添加条件要求，第4个为I的猜测候选，我尝试用s.prove指令得到我猜测的候选的反例对于我。我似乎在运行这段代码上遇到了一个巨大的错误日志，谁能告诉我哪里出了问题？

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

这意味着求解器无法确定输入是否可满足；它放弃并说 unknown。求解器的早期版本可能已经能够成功解决这个问题，提供不可满足性证明，或者模型应该是可满足的。

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

提交错误报告

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

Finding counterexamples for a "Horn" solver object

z3

z3py