新手请教

[nobodxbodon]

也许开个Discussion方便讨论？

如之前打算，开始照着这个z3例程：

import functools
import z3

s = z3.Solver()

新布尔量 = z3.Bools(  # 甲, 乙 
    ["甲", "乙"]
)
各值 = {"甲": 新布尔量[0], "乙": 新布尔量[1]}

# 1. 甲温饱或乙温饱
s.add(functools.reduce(z3.Or, list(各值.values())))

# 2. 如甲温饱，则乙温饱
s.add(z3.If(
        各值['甲'],
        各值['乙'],
        True,
    ))

if s.check() != z3.sat:
    raise ValueError("有误")
结果 = s.model()
for 某项 in 结果:
    if 结果[某项]:
        print(str(某项) + '已温饱')
    else:
        print(str(某项) + '不温饱')

改写如下：

have 人类 nonempty_set, 甲 人类, 乙 人类
prop 温饱(x 人类)
know $温饱(甲) or $温饱(乙)
know $温饱(甲) => $温饱(乙)
$温饱(乙)

结果报错：

some atoms in the following fact are undeclared:
$温饱(=>, 乙)
know:
    $温饱(甲)
    $温饱(=>, 乙)

Execution Error: line 4
some atoms in the following fact are undeclared:
$温饱(=>, 乙)
know:
    $温饱(甲)
    $温饱(=>, 乙)

---
Error :(

[nobodxbodon]

改为如下后，不报错了：

have 人类 nonempty_set, 甲 人类, 乙 人类
prop 温饱(x 人类)
know $温饱(甲) or $温饱(乙)

prop 甲乙关系(甲, 乙 人类):
  $温饱(甲) => $温饱(乙)
know $甲乙关系(甲, 乙)
$温饱(乙)

返回：

$温饱(乙)

Unknown: line 8

---
Unknown :(

最后一句改为 $温饱(甲) 后，Success，但是由于这个prop的条件成立：

$温饱(甲)
is true. proved by
$温饱(甲) on line 6

看来是know $甲乙关系(甲, 乙) 的语义和“如果甲温饱则乙温饱”不同。继续看prop。。。

另外，感觉这句 know $温饱(甲) or $温饱(乙) 语义和 “甲乙中仅有一个温饱” 不同？

[malloc-realloc]

Oh! z3确实是一个很好的prover。您能把您的微信号发送到 [email protected] 来吗，我加一下您好友，然后我们线上会议一下。我非常愿意和您和您的伙伴们交流！！