smt

1зной

1ответ

как распечатать вывод в шестнадцатеричном формате

этот вывод программы Boolector для печати в двоичном формате. Но мне нужно в шестнадцатеричном формате. так, как печатать шестнадцатеричный формат в boolector. (set-logic QF_BV) (set-info :smt-lib-ve

0зной

1ответ

Управляйте стратегией решения Z3

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

0зной

1ответ

Z3Py: Разбор выражений с использованием eval или z3.parse_smt2_string

Я пишу программу python, которая, среди прочего, должна преобразовывать большие формулы пропозиции в экземпляры z3. Например, формула f, которая может быть создана с помощью моей программы через a = m

0зной

1ответ

понимание карты памяти AnGR

я работаю над одной из проблем AnGR-Doc (https://github.com/angr/angr-doc/blob/2d45c9e6d9f91e83988719aa19940aec2cfd8747/examples/ekopartyctf2015_rev100/solve.py), но в моем подходе я имею такую ситу

1зной

1ответ

Как анализировать проблемы производительности z3?

У меня 37 подобных проблем с SMT2, каждый в двух вариантах, которые меня устраивают compact и unrolled. В проблемах используется инкрементное SMT-решение, и каждый (check-sat) возвращает unsat. В комп

1зной

1ответ

Как вырезать/подписать расширение битрейдеров в Z3?

Мне не удалось выполнить нулевое расширение на битвектор с использованием интерфейса Z3 SMT. Из того, что я узнал, читая источники, для этого есть функции, и они доступны для различных привязок (C, C+

0зной

1ответ

Записи с Z3

Я довольно внимательно посмотрел документацию и руководства и сам попробовал несколько вещей. Однако решение моих проблем уклоняется от меня. Это то, что говорит учебник о записях, но мне не ясно, как