Z3答案不满足约束

Question

我开始使用Z3，我给它一个玩具问题。我们的想法是为所有分配（A，B，C），中的至少一个（FA（B，C）==一个，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 =假，B =真，C =真）的情况下，如在下面的表中报告。

我在做什么错了，我怎么能得到满足约束条件，如第二个表格呈现规则的解决方案吗？

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

Answer 1

我不能复制这一点。当我运行程序时，我得到：

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

这似乎是正确的模式。请注意，这不同于你在说什么，因为它似乎交换fc和fa你的情况。

这很可能是一个已经修正了一个错误;我使用的是从GitHub源新鲜编译Z3。你可以升级你的Z3安装，看看问题是否会消失？