Описание тега z3
Z3 - это высокопроизводительное средство доказательства теорем, разрабатываемое Microsoft Research.
1
ответ
Z3 Python API - когда он будет доступен
В руководстве по Z3-Python указано, что для локального использования Z3 с Python необходимо использовать библиотеку Python в выпуске Z3. Однако моя установка последней версии (3.2) не содержала такой папки. Я предполагаю, что это означает, что папка…
29 апр '12 в 22:56
1
ответ
Получать новые ненасыщенные ядра
Там Я пытаюсь извлечь предложение из формул и изменить полярность одного предложения каждый раз, когда решается сб, вычисляя модели и помещая предложение в набор. Если это решено ненадлежащим образом, то найдите новые ненасыщенные ядра. Но постепенн…
05 фев '13 в 21:12
1
ответ
Установите Z3 в Windows
Я загрузил файл Z3 4.3.0 для Windows (64 бита), который находится на сайте: http://z3.codeplex.com/releases. Когда я пытаюсь запустить файл z3.exe, который находится в папке bin. Запрос появляется и исчезает сразу. Мне нужно было знать, как запустит…
16 мар '13 в 17:22
2
ответа
Ненулевой вектор в квантификаторе
Я хочу проверить формулу формы: Exists p . ForAll x != 0 . f(x, p) > 0 Реализация (которая не работает) заключается в следующем: def f0(x0, x1, x, y): return x1 ** 2 * y + x0 ** 2 * x s = Solver() x0, x1 = Reals('x0 x1') p0, p1 = Reals('p0 p1') s…
10 май '18 в 18:19
1
ответ
z3 числовые ограничения: что лучше?
Какой из следующих двух способов записи (эквивалентных) ограничений предпочтителен (с точки зрения производительности) при решении целочисленных вещественных ограничений с использованием z3? (assert (=> (и (<= значение 0,0009765625) (<значение 0,001…
22 июл '13 в 18:48
1
ответ
Импорт Z3 в Visual Studio 2010
Z3 Prover от Microsoft Research может быть построен с использованием компиляторов Visual Studio и nmake, Это сделало бы его естественным подходом для разработки с использованием Visual Studio, и я предполагаю, что это то, что делают разработчики (ил…
22 июн '13 в 09:01
1
ответ
Может ли z3 прочитать выходной файл MathSAT как его входной файл?
Мне нужно провести несколько экспериментов с использованием z3 и mathsat. Я уже закончил эксперименты с mathsat. Написание входного файла для mathsat занимает много времени, и я не хочу снова записывать входные файлы для z3. Mathsat поддерживает соз…
04 янв '13 в 12:22
1
ответ
Как проверить, назначен ли z3::expr
Я использую z3 через интерфейс C++. z3::expr может быть базовой переменной / константой (c.real_const, c.real_val) или выражением. Я часто сталкивался с ошибкой, вызванной использованием z3::expr. Проблема может быть описана с помощью следующего код…
25 апр '14 в 06:11
1
ответ
Буги странно утверждают (ложно) поведение
Я работаю с Буги, и я столкнулся с некоторыми видами поведения, которые я не понимаю. Я использую assert(false) как способ проверить, если предыдущий assume заявления абсурдны. Например, в следующем случае программа проверена без ошибок... type T; c…
23 мар '17 в 20:07
1
ответ
Условное заявление Z3
Как написать условное утверждение в Z3. eg: if (a%2==0){ value=1 } Я пытаюсь добиться этого в Z3 Solver от Microsoft Research, но пока не повезло
01 июн '17 в 18:18
2
ответа
Объявить матрицу с неизвестным размером в Z3
Я знаю, что я могу объявить матрицу z3.Real в Z3 объявив его элементы индивидуально (может быть, через понимание списка). Есть ли способ представить матрицу с неизвестным размером? Например, рассмотрим следующий пример: при фильтрации изображений, д…
14 апр '17 в 02:42
1
ответ
Не может распознать символ "!" при использовании topredicate в BAP
Я попытался использовать инструмент topredicate в bap для перевода il в SMT-LIB2. Но эта команда возвращает ошибку: ./topredicate -il test.il -post "R_EBP:u32 != R_ESP:u32 -solver z3 -noopt -stp-out test.smt Ошибка: Исключение синтаксического анализ…
27 окт '14 в 09:11
1
ответ
Доступен ли обратный вызов при удалении объекта Z3_ast?
Я использую C++ API для z3, поэтому мне не нужно беспокоиться о подсчете ссылок или управлении памятью. Тем не менее, я хотел бы хранить информацию о z3 AST, используя std::map вдоль линий std::map<Z3_ast, some_struct>, Когда конкретный объект…
07 дек '16 в 16:55
1
ответ
Z3 на архитектурах не x86
Я проверял переносимость инструмента, используя Z3 (git-версия 2012-12-21, последняя "основная" версия), и, таким образом, пытался скомпилировать Z3 на Sparc64. Мне пришлось возиться с src/util/hwf.cpp так что он будет относиться к Sparc64, а не тол…
12 фев '14 в 10:26
1
ответ
Различные результаты между Z3 двоичного и Z3 API
Я пробую Z3 с примерами квантификаторов из http://rise4fun.com/Z3/tutorial/guide. Два примера отлично работают с онлайн-версией Z3 (думаю, это будет Z3 4.0) . (set-option :auto-config false) ; disable automatic self configuration (set-option :mbqi f…
03 май '12 в 20:48
1
ответ
Тайм-аут для решателя z3 в python
У меня проблемы с установкой таймаута для моего решателя: s = Solver() encoding = parse_smt2_file("ex.smt2") s.add(encoding) s.set("timeout", 600) solution = s.check() но я получаю следующую ошибку Traceback (most recent call last): File "/Users/X/D…
05 фев '15 в 07:23
1
ответ
Почему z3.And() работает медленно?
Я использую привязки Z3 Python для создания выражения And через z3.And(exprs) где exprs список питонов из 48000 ограничений на равенство по логическим переменным Эта операция занимает 2 секунды на MBP с процессором 2,6 ГГц. Что я могу делать не так?…
15 окт '14 в 06:21
1
ответ
Невозможно извлечь значение для Z3 EnumSort в z3py
В настоящее время я пытаюсь закодировать проблему в Z3, и я хочу смоделировать "трехуровневый" логический (то есть, логический с true, false а также unknown). Вот как я смоделировал это: #!/usr/bin/env python import z3 from collections import Ordere…
17 окт '17 в 12:41
0
ответов
Поддержка отладки в Boogie
Я работаю над проектом, использующим Boogie для проверки распределенных приложений. В моей работе мне нужна лучшая поддержка отладки, когда проверка не удалась. Я просмотрел параметры командной строки и нашел следующие параметры полезными в моем кон…
22 ноя '17 в 11:01
1
ответ
Использование массива в Z3PY
Я использую z3 для своего исследования, и у меня есть следующая проблема. Я анализирую модель выполнимой формулы, которая содержит массивы, но я не понимаю результатов модели. Например, у меня есть две переменные 'pkgcounter' и 'rxlen' и два предлож…
19 июл '16 в 13:53