Как Z3 конвертирует expr в SMT? Есть ли способ проверить это? - PullRequest
Новая
       80

Как Z3 конвертирует expr в SMT? Есть ли способ проверить это?

0 голосов
/ 14 марта 2020

Я прошел через связанные вопросы, и они не отвечают на мой запрос.

Используя Z3, cpp, у меня есть выражение 

expr e1=((x[0]=tru && y[0]!=tru)||(x[0]!=tru &&y[0]=tru));

Где tru - тавтология.

Когда я печатаю это выражение, я получаю 

(let ((a!1 (and (or x0 (not x0)) (distinct y0 (or x0 (not x0))))))
  (or a!1 (or x0 (not x0))))

, и это не то, что я хотел, чтобы мой e1 представлял. Могу ли я как-то конвертировать expr в SMT самостоятельно, чтобы я мог проверить, правильно ли он переводится? Или есть способ напечатать выражение простым способом, которым я его представлял, а не в эффективной структуре (с использованием поддеревьев, таких как a!1 и т. Д.) На языке SMT? Возможно, выключатель, который я могу выключить?

1 Ответ

0 голосов
/ 15 марта 2020

Некоторые «переводы» неизбежны. Поскольку Z3 создает дерево разбора для ваших выражений, оно переписывает их во внутренние формы. Это не просто для «эффективности». Это также тот случай, когда некоторые поверхностные формы просто не имеют внутреннего представления, а скорее переписаны.

Хорошая печать - другой вопрос, конечно. Есть много способов контролировать, насколько хороша печать. Если вы запустите z3 -p и посмотрите на вывод для раздела pretty-printing, вы увидите: 

[module] pp, description: pretty printer
    bounded (bool) (default: false)
    bv_literals (bool) (default: true)
    bv_neg (bool) (default: false)
    decimal (bool) (default: false)
    decimal_precision (unsigned int) (default: 10)
    fixed_indent (bool) (default: false)
    flat_assoc (bool) (default: true)
    fp_real_literals (bool) (default: false)
    max_depth (unsigned int) (default: 5)
    max_indent (unsigned int) (default: 4294967295)
    max_num_lines (unsigned int) (default: 4294967295)
    max_ribbon (unsigned int) (default: 80)
    max_width (unsigned int) (default: 80)
    min_alias_size (unsigned int) (default: 10)
    pretty_proof (bool) (default: false)
    simplify_implies (bool) (default: true)
    single_line (bool) (default: false)

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

    pp.max_depth      --> 4294967295
    pp.min_alias_size --> 4294967295

(число не имеет большого значения, просто сделайте их достаточно большими.) Эти две настройки должны избегать симпатичного принтера из создания a!1 поддеревьев вы видите.

К сожалению, что именно означают эти параметры, не так уж хорошо задокументировано. Некоторые из них, вы можете догадаться по их названию, другие - поиграть и посмотреть, как они влияют. Но если вы действительно хотите знать, как они изменяют вывод, вам придется копаться в самом исходном коде z3. Желаем удачи!

...