Вопросы по теме 'z3py'

Непечатаемый Solver.model()
Следующая программа генерирует модель Z3, которую нельзя распечатать (то есть print solver.model() выдает исключение), используя последнюю версию Z3 из главной ветки git (коммит 89c1785b): x = Int('x') a = Array('a', IntSort(), BoolSort()) b =...
374 просмотров
z3 z3py
schedule 17.04.2023
Z3Python: пример массива?
Я ищу некоторые примеры кода, использующие теорию массивов в Z3 python, но не могу их найти. пожалуйста, может ли кто-нибудь привести несколько примеров кода? Благодарность!
713 просмотров
z3 z3py
schedule 13.09.2023
z3py на MacOSX: не удается получить модель
Я вижу странную проблему с z3py на Mac, мне было интересно, видел ли кто-нибудь это раньше: $ cat bug.py from z3 import * x = Int('x') s = Solver() s.add(x > 5) print(s.check()) print(s.model()) $ python bug.py sat [x = ] Значение x...
183 просмотров
z3 z3py
schedule 13.02.2023
Переменные Z3Py Bool преобразуются в Int в модели
Я использую API Python для Z3, чтобы создать инструмент для своих исследований. У меня возникла следующая проблема: я генерирую набор ограничений Z3 с помощью скрипта Python. Поскольку набор может быть непоследовательным, я отслеживаю каждую формулу...
1454 просмотров
boolean int z3 z3py
schedule 03.02.2023
Код дает неверный результат с ForAll, почему?
Я пытаюсь использовать квантификатор ForAll для b , поэтому формула a * b == b с каждым b даст мне в результате a == 1 . Я реализовал это в приведенном ниже коде (Z3 python): from z3 import * a, b, a1 = BitVecs('a b a1', 32) f = True f...
971 просмотров
python z3 z3py
schedule 31.01.2023
Z3Python: ForAll вызывает зависание моего кода или возвращает Unsat, почему?
Я все еще борюсь с проблемой поиска значения a , чтобы a * b == b со всем значением b . Ожидаемый результат a == 1 . У меня есть два решения ниже. (A) Я реализовал это с помощью квантификатора ForAll в приведенном ниже коде (поправьте...
86 просмотров
z3 z3py
schedule 20.02.2023
Как выполнить исключение квантификатора с помощью Python API Z3
Как я могу выполнить исключение квантификатора с помощью Python API Z3? Хотя я проверил руководство и API, не смог этого сделать. У меня есть формула с квантификатором существования, и я хочу, чтобы Z3 выдал мне новую формулу, чтобы этот квантор...
1705 просмотров
z3 smt z3py
schedule 17.05.2022
Решатель z3: z3-SMT на платформе Mac
Мне нужно поработать над решателем Z3 SMT для моей магистерской диссертации. Я уже проверил учебные пособия для Z3-SMT, которые основаны на входных данных SMT-Lib. Но я смог установить только z3-Py, для которого нужно знание Python. Я хотел знать,...
1527 просмотров
z3 z3py
schedule 20.10.2022
Возможная ошибка с Z3: Z3 не может доказать теорему в топологии
Я пытаюсь доказать с помощью Z3 теорему общей топологии, изложенную в Топология TPTP Я перевожу приведенный там код, используя следующий код Z3-SMT-LIB ;; File : TOP001-2 : TPTP v6.0.0. Released v1.0.0. ;; Domain : Topology ;;...
149 просмотров
topology z3 z3py theorem-proving
schedule 07.07.2022
объявление алгебраического типа данных другого алгебраического типа данных?
Мне интересно, возможно ли создать алгебраический тип данных, который зависит от другого алгебраического типа данных в Z3Py. Например, скажем, я определил свой собственный тип данных Bool и хочу сам определить список Bool: from z3 import * Bool...
171 просмотров
z3 z3py
schedule 31.01.2023
Случайность Z3 сгенерированных значений модели
Я пытаюсь повлиять на случайность результатов для значений модели, сгенерированных Z3. Насколько я понимаю, возможности для этого очень ограничены: в случае линейной арифметики симплексный решатель не допускает случайных результатов, которые...
667 просмотров
z3 z3py
schedule 31.03.2024
Использование for all с неинтерпретируемыми сортировками JAVA API
Я пытаюсь изучить Z3 с помощью java API, так как нет документации. Я просматривал документацию C API, но до сих пор не могу найти четкого примера того, как использовать некоторые основные функции. Я пытаюсь закодировать этот код Z3 (который...
487 просмотров
java z3 z3py z3c.form
schedule 04.06.2023
странное поведение при проверке сб Z3
Может кто-нибудь увидеть, что я делаю неправильно.... Я использую квантификатор для всех, чтобы создать две строки: (assert(forall((t Task)) (not (mustPrecede t t)))) (assert(forall((t1 Task)(t2 Task)(t3 Task)) (implies (and (mustPrecede t1...
84 просмотров
z3 z3py
schedule 19.08.2022
Z3py — Создать выражение Z3py из строки, или Что происходит с «не» в eval?
Я пытаюсь решить ограничения в выражении if или while с помощью Z3py. Поскольку Z3py ожидает таких выражений, как True, False или Z3py-Boolean, мне пришлось решить, как преобразовать ограничения, которые являются просто строками, в правильную форму....
296 просмотров
python eval z3py
schedule 03.10.2022
Есть ли в Z3 способ сгенерировать неопределенное количество предположений для проверки?
Моя программа Python использует Z3 Python API. Он генерирует ряд предположений, которые Z3 проверяет с помощью команды: check(P1, P2,....Pn) Затем я получаю unsat ядро ​​с помощью команды: unsat_core() Есть ли способ использовать в...
76 просмотров
python z3 z3py
schedule 03.03.2023
Создание константы из сортировки в Z3 Python API
Учитывая сортировку Z3 и строку s , я пытаюсь создать константу Z3 такого рода с именем s . Например, учитывая IntSort() и имя "x" , я хотел бы получить целочисленную константу с именем "x" . Я знаю, что могу заставить его вызывать...
602 просмотров
python z3 z3py
schedule 22.06.2022
Формализация достижимости в z3py
Я пытаюсь формализовать свойство достижимости, чтобы я мог найти удовлетворительное решение, если оно существует, путь длиной 4 (что означает, что есть 3 промежуточных узла, через которые соединяются 2 желаемых узла). Примечание. Я ограничиваю поиск...
174 просмотров
z3 smt z3py
schedule 09.11.2022
Используйте z3 для подтверждения идентичности булевой/арифметической формулы
Я пытаюсь использовать z3 для подтверждения следующей личности: х+у == х^у + 2*(х&у) То есть мы можем заменить любое дополнение смесью логических и арифметических инструкций (пример взят из главы 2.2, Hacker's Delight). ). Я...
223 просмотров
python z3 z3py
schedule 21.11.2022
Как создать ограничение в Z3py, чтобы проверить, является ли список перестановкой другого?
Я новичок в Z3py, и я борюсь с этим уже почти неделю ... Я не нахожу достаточно информации, чтобы помочь мне в учебниках, и хорошего примера (функции Exists), который может мне помочь .
446 просмотров
python z3 z3py
schedule 11.03.2023
Решатель Z3 возвращает unsat, когда формула должна быть удовлетворительной
У меня есть «простая» формула, которую решатель Z3 (интерфейс Python) не может обработать. Он работает довольно долго (30 минут), а затем возвращается неизвестным, хотя я могу найти удовлетворительное задание вручную менее чем за минуту. Это...
262 просмотров
python z3 z3py sat-solvers
schedule 30.01.2023