- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我目前正在使用 Z3py 来推导一些不变量,这些不变量被编码为 horn-clauses 的结合,同时还为不变量提供模板。如果您看到下面的代码片段,我首先从一个简单的示例开始。
x = 0;
while(x < 5){
x += 1
}
assert(x == 5)
这转化为喇叭子句
x = 0 => Inv(x)
x < 5/\Inv(x) => Inv(x +1)
不是( x < 5)/\Inv(x) => x = 5
这里的不变量是 x <= 5。
我已经为 a*x + b <= c 形式的不变量提供了一个模板因此求解器所要做的就是猜测一组可以减少到 x <= 5 的 a、b 和 c 的值。
但是,当我对其进行编码时,我总是感到不满意。如果尝试断言 Not (x==5) 我得到 a=2 、 b = 1/8 和 c = 2 作为反例对我来说意义不大。
我在下面提供了我的代码,对于纠正我的编码的任何帮助,我将不胜感激。
x = Real('x')
x_2 = Real('x_2')
a = Real('a')
b = Real('b')
c = Real('c')
s = Solver()
s.add(ForAll([x],And(
Implies(x == 0 , a*x + b <= c),
Implies(And(x_2 == x + 1, x < 5, a*x + b <= c), a*x_2 + b <= c),
Implies(And(a*x + b <= c, Not(x < 5)), x==5)
)))
if (s.check() == sat):
print(s.model())
编辑:这对我来说变得陌生了。如果我删除 x_2 定义并在第二个 horn 子句中将 x_2 替换为 (x + 1) 并删除 x_2 = x_2 + 1,无论我写 Not( x==5) 还是 x==5 我都会感到不满意在最后的号角子句中。
最佳答案
有两件事阻止了您的原始编码工作:
1) 不可能满足x_2 == x + 1
对于所有 x
对于 x_2
的单个值.因此,如果你要写 x_2 == x + 1
, 两者 x
和 x_2
需要普遍量化。
2) 有点令人惊讶的是,这个问题在整数中是可满足的,但在实数中却不是。您可以看到子句 x < 5 /\ Inv(x) => Inv(x + 1)
的问题.如果x
是整数,则 x <= 5
满足.但是,如果 x
允许是任何实际值,那么你可以有 x == 4.5
, 满足 x < 5
和 x <= 5
, 但不是 x + 1 <= 5
, 所以 Inv(x) = (x <= 5)
在现实中不满足这个问题。
此外,您可能会发现定义 Inv(x)
很有帮助,它清理了很多代码。以下是这些更改对您的问题的编码:
from z3 import *
# Changing these from 'Int' to 'Real' changes the problem from sat to unsat.
x = Int('x')
x_2 = Int('x_2')
a = Int('a')
b = Int('b')
c = Int('c')
def Inv(x):
return a*x + b <= c
s = Solver()
# I think this is the simplest encoding for your problem.
clause1 = Implies(x == 0 , Inv(x))
clause2 = Implies(And(x < 5, Inv(x)), Inv(x + 1))
clause3 = Implies(And(Inv(x), Not(x < 5)), x == 5)
s.add(ForAll([x], And(clause1, clause2, clause3)))
# Alternatively, if clause2 is specified with x_2, then x_2 needs to be
# universally quantified. Note the ForAll([x, x_2]...
#clause2 = Implies(And(x_2 == x + 1, x < 5, Inv(x)), Inv(x_2))
#s.add(ForAll([x, x_2], And(clause1, clause2, clause3)))
# Print result all the time, to avoid confusing unknown with unsat.
result = s.check()
print result
if (result == sat):
print(s.model())
还有一件事:写a*x + b <= c
对我来说有点奇怪作为模板,因为这与 a*x <= d
相同对于某个整数 d
.
关于logic - 使用 Z3py 对 horn 子句进行不变归纳,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/38807093/
最近我听说了一些有关 HORN 的信息,想知道它可以解决哪些问题,或者在现实生活中使用它有何好处。 http://code.google.com/p/hornget/ 最佳答案 我已经为 horn 编
如今,在自动程序验证中,将问题作为 Horn 子句系统的解决方案是很流行的,其中大多数 Horn 子句定义了不变量的归纳条件,然后一些约束定义了要匹配的安全条件。 一种文件格式是 SMT-LIB:子句
我正在尝试通过 NumPy 和 OpenCV 实现 Horn-Schunck 光流算法我用 Horn-Schunck method on wiki和 original paper 但是我的实现在以下简
关闭。这个问题不满足Stack Overflow guidelines .它目前不接受答案。 想改善这个问题吗?更新问题,使其成为 on-topic对于堆栈溢出。 6年前关闭。 Improve thi
我正在尝试使用 Z3 的 HORN 逻辑(set-logic HORN)对一些命令式程序进行编码,但在定义子句时遇到一些困难(使用 SMT2)。谁能告诉我在哪里可以找到有关 Z3 的此功能的良好文档来
我目前正在使用 Z3py 来推导一些不变量,这些不变量被编码为 horn-clauses 的结合,同时还为不变量提供模板。如果您看到下面的代码片段,我首先从一个简单的示例开始。 x = 0; whil
Winston 和 Horn states 的“Lisp”中的问题 19-2, In depth-first search, all of the partial paths in the queue
我是一名优秀的程序员,十分优秀!