Ответ Z3 не удовлетворяет ограничению - PullRequest
Новая
       9

Ответ Z3 не удовлетворяет ограничению

0 голосов
/ 04 февраля 2019

Я начинаю с 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 Ответ

0 голосов
/ 04 февраля 2019

Я не могу повторить это.Когда я запускаю вашу программу, я получаю: 

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

, которая кажется правильной моделью.Обратите внимание, что это отличается от того, что вы получаете, так как кажется, что вы поменяете местами fc и fa в вашем случае.

Это вполне может быть ошибка, которая уже была исправлена;Я использую только что скомпилированный z3 из github источников.Можете ли вы обновить установку z3 и посмотреть, исчезнет ли проблема?

...