代码之家 › 专栏 › 技术社区 › Hatshepsut

Z3答案不满足约束条件

z3py z3

0

Hatshepsut · 技术社区 · 6 年前

我刚开始使用Z3,我给了它一个玩具问题。其思想是,对于(a,b,c)的所有赋值,至少(fa(b,c)==a,fb(a,c)==b,fc(a,b)==c)中的一个必须为真。

模型报告

[fc = [else -> And(Not(Var(1)), Var(0))],
  fa = [else -> And(Var(1), Var(0))],
  fb = [else -> False]]

这似乎不满足(a=False,b=True,c=True)情况的约束,如下表所述。

我做错了什么,如何得到满足约束的解决方案,如第二个表中的规则?

import pandas as pd
from z3 import Bools, Function, BoolSort, Solver, ForAll, Or

a, b, c = Bools("a b c")
fa = Function("fa", BoolSort(), BoolSort(), BoolSort())
fb = Function("fb", BoolSort(), BoolSort(), BoolSort())
fc = Function("fc", BoolSort(), BoolSort(), BoolSort())

s = Solver()
s.add(ForAll([a, b, c], Or(fa(b, c) == a, fb(a, c) == b, fc(a, b) == c)))


def tabulate(fa, fb, fc):
    mi = pd.MultiIndex.from_product(
        [[False, True] for _ in range(3)], names=["a", "b", "c"]
    )
    df = pd.DataFrame(index=mi).reset_index()
    return (
        df.assign(fa=fa, fb=fb, fc=fc)
        .assign(
            fb_correct=lambda x: x.fb == x.b,
            fa_correct=lambda x: x.fa == x.a,
            fc_correct=lambda x: x.fc == x.c,
        )
        .assign(any_correct=lambda x: x.fb_correct | x.fa_correct | x.fc_correct)
        .astype(int)
    )


print(s.check())
print(s.model())

# sat
# [fc = [else -> And(Not(Var(1)), Var(0))],
#  fa = [else -> And(Var(1), Var(0))],
#  fb = [else -> False]]

print(tabulate(fb=False, fa=lambda x: x.b & x.c, fc=lambda x: x.a & ~x.b))

#    a  b  c  fa  fb  fc  fb_correct  fa_correct  fc_correct  any_correct
# 0  0  0  0   0   0   0           1           1           1            1
# 1  0  0  1   0   0   0           1           1           0            1
# 2  0  1  0   0   0   0           0           1           1            1
# 3  0  1  1   1   0   0           0           0           0            0
# 4  1  0  0   0   0   1           1           0           0            1
# 5  1  0  1   0   0   1           1           0           1            1
# 6  1  1  0   0   0   0           0           0           1            1
# 7  1  1  1   1   0   0           0           1           0            1


# Correct answer:
print(
    tabulate(fb=lambda x: ~x.a | x.b, fa=lambda x: x.b & x.c, fc=lambda x: x.a & ~x.b)
)

#    a  b  c  fa  fb  fc  fb_correct  fa_correct  fc_correct  any_correct
# 0  0  0  0   0   1   0           0           1           1            1
# 1  0  0  1   0   1   0           0           1           0            1
# 2  0  1  0   0   1   0           1           1           1            1
# 3  0  1  1   1   1   0           1           0           0            1
# 4  1  0  0   0   0   1           1           0           0            1
# 5  1  0  1   0   0   1           1           0           1            1
# 6  1  1  0   0   1   0           1           0           1            1
# 7  1  1  1   1   1   0           1           1           0            1

版本:z3解算器==4.8.0.0.post1

1 回复 | 直到 6 年前

1

alias 6 年前

我无法复制这一点。当我运行您的程序时,我得到:

[fc = [else -> And(Var(0), Var(1))],
 fa = [else -> And(Var(0), Not(Var(1)))],
 fb = [else -> False]]

fc fa

它很可能是一个已经修复的bug;我使用的是来自github源代码的新编译的z3。你能升级你的z3安装,看看问题是否消失了吗?