Не удалось проверить:! M_var2expr.empty () на питоне z3 - PullRequest
Новая
       9

Не удалось проверить:! M_var2expr.empty () на питоне z3

0 голосов
/ 11 декабря 2018

Это код, который выдает исключение. 

import z3
solver = z3.Solver()
v1, v2, v3, v4 = [z3.Bool("v{}".format(i)) for i in range(1,5)]
z3_prop1 = z3.And(z3.Or(z3.Or(z3.Not(z3.And(v1,v2)), z3.And(False, v3)),
       z3.And(z3.And(False, v2), z3.Or(z3.Not(False), v1))),
    z3.And(z3.And(z3.And(v3, v2), z3.And(v4, v1)),
        z3.Or(z3.Or(v2, v3), z3.And(v4, False))))
print(z3_prop1)
solver.reset()
solver.add(z3_prop1)
print("CHECK", solver.check()) # z3_prop1 is OK
z3_prop2 = z3.Not(z3_prop1)
solver.reset()
print(z3_prop2)
solver.add(z3_prop2)
print("CHECK", solver.check()) # z3_prop2 throws Error

Это вывод кода. 

And(Or(Or(Not(And(v1, v2)), And(False, v3)),
   And(And(False, v2), Or(Not(False), v1))),
And(And(And(v3, v2), And(v4, v1)),
    Or(Or(v2, v3), And(v4, False))))
CHECK unsat
Not(And(Or(Or(Not(And(v1, v2)), And(False, v3)),
       And(And(False, v2), Or(Not(False), v1))),
    And(And(And(v3, v2), And(v4, v1)),
        Or(Or(v2, v3), And(v4, False)))))
Failed to verify: !m_var2expr.empty()
libc++abi.dylib: terminating with uncaught foreign exception
[1]    10607 abort      python -m src.z3_solver

В чем причина исключения?

Моя среда выглядит следующим образом.

  • macOS 10.13.2
  • Z3 версия 4.8.0 - 64 бит (устанавливается brew)
  • Python 3.6.7 (Установлено pyenv)
  • pip z3 0.2.0
  • pip z3-solver 4.8.0.0

1 Ответ

0 голосов
/ 11 декабря 2018

Работает просто отлично для меня: 

$ python a.py
And(Or(Or(Not(And(v1, v2)), And(False, v3)),
       And(And(False, v2), Or(Not(False), v1))),
    And(And(And(v3, v2), And(v4, v1)),
        Or(Or(v2, v3), And(v4, False))))
('CHECK', unsat)
Not(And(Or(Or(Not(And(v1, v2)), And(False, v3)),
           And(And(False, v2), Or(Not(False), v1))),
        And(And(And(v3, v2), And(v4, v1)),
            Or(Or(v2, v3), And(v4, False)))))
('CHECK', sat)

Я тоже на Mac, и у меня есть: 

$ z3 --version
Z3 version 4.8.3 - 64 bit

Я подозреваю, что ваша установка как-то нарушена.Переустановка с нуля может решить проблему.

...