Получение доказательства от z3py

Я просматривал документацию Z3Py и для таких, как я, не смог понять, как получить доказательство от решателя (например, если я начну с экземпляра законов Де Моргана, как я могу извлечь доказательство из Z3Py экземпляра, шаг за шагом). Единственная ссылка, которую я видел, была для proof(self) в классе Solver, который предположительно получает доказательство последней проверки, если построение доказательства включено, но я продолжаю возвращать очень расплывчатую ошибку:

Traceback (most recent call last):
  File "example.py", line 36, in <module>
    prove(prop)
  File "example.py", line 15, in prove
    print(s.proof())
  File "src/api/python/z3.py", line 5851, in proof
  File "src/api/python/z3core.py", line 3770, in Z3_solver_get_proof
z3types.Z3Exception: 'invalid usage'`

Поэтому я считаю, что построение доказательства отключено по умолчанию (вероятно, из-за накладных расходов). Как его включить? Или это даже не достигает того, что, как мне кажется, должно быть достигнуто путем демонстрации вывода доказательства шаг за шагом из таких простых аксиом, как идемпотентность и т. д.?

Обновление: На самом деле, попробовав (и поверьте мне, я убедился, что моя версия самая последняя с веб-сайта Microsoft Research, и даже пересобрал ее и все такое) set_param неопределенный:

>>> from z3 import *
>>> print [s for s in dir(z3) if 'set_param' in s]
['Z3_fixedpoint_set_params', 'Z3_set_param_value', 'Z3_solver_set_params']
>>> set_param
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
NameError: name 'set_param' is not defined

Впоследствии я пытался использовать Z3_set_param_value, Z3_solver_set_params, а затем set_option(proof=True) (потому что он был указан как псевдоним для set_param` в справочнике) безрезультатно:

>>> set_option(proof=True)
Error setting 'PROOF', reason: unknown option.
terminate called after throwing an instance of 'z3_error'
Aborted (core dumped)

python z3 z3py
person Francesco Gramano    schedule 11.04.2015    source источник
comment
Связано: stackoverflow.com/q/49874498/1959808   -  person Ioannis Filippidis    schedule 25.09.2020
comment
Связано: stackoverflow.com/a/9115446/1959808   -  person Ioannis Filippidis    schedule 25.09.2020

Ответы (1)


arrow_upward
2
arrow_downward

Да, вы должны установить proof=True, чтобы включить доказательства. Более того, все выражения должны быть созданы в режиме, в котором включены доказательства. Один из способов сделать это заключается в следующем:

>>> set_param(proof=True)
>>> ctx = Context()
>>> s = Solver(ctx=ctx)
>>> x = Int('x', ctx=ctx)
>>> s.add(x > 0)
>>> s.add(x == 0)
>>> s.check()
unsat
>>> s.proof()
mp(mp(asserted(x > 0),
      rewrite((x > 0) == Not(x <= 0)),
      Not(x <= 0)),
   trans(monotonicity(trans(monotonicity(asserted(x == 0),
                                        (x <= 0) == (0 <= 0)),
                            rewrite((0 <= 0) == True),
                            (x <= 0) == True),
                      Not(x <= 0) == Not(True)),
         rewrite(Not(True) == False),
         Not(x <= 0) == False),
   False)

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

Если вы убедитесь, что перед любыми другими вызовами Z3 для режима проверки установлено значение True, вам не нужно нести свой собственный контекст. Другими словами, следующее также работает:

python.exe
>>> from z3 import *
>>> set_param(proof=True)
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s.add(x == 0)
>>> s.check()
unsat
>>> s.proof() 
mp(mp(asserted(x > 0),
      rewrite((x > 0) == Not(x <= 0)),
      Not(x <= 0)),
   trans(monotonicity(trans(monotonicity(asserted(x == 0),
                                        (x <= 0) == (0 <= 0)),
                          rewrite((0 <= 0) == True),
                        (x <= 0) == True),
                  Not(x <= 0) == Not(True)),
     rewrite(Not(True) == False),
     Not(x <= 0) == False),
  False)
person Nikolaj Bjorner    schedule 12.04.2015
comment
У меня возникла проблема с вашим решением, и я обновил свой вопрос, чтобы отразить новую информацию. - person Francesco Gramano; 12.04.2015
comment
Неважно, это кажется верным только для предварительно собранного z3. То же самое было не так после сборки Z3Py. - person Francesco Gramano; 13.04.2015