Вопросы по теме 'z3'
Значения терминов массива в моделях z3
Я использую z3 для своих исследований, и у меня есть следующая проблема. Я анализирую модель выполнимой формулы, которая содержит массивы и неинтерпретируемые функции. Я хотел бы проверить определенные записи массива.
В примерах руководства по z3...
802 просмотров
schedule
16.04.2024
Инкрементальные вызовы Z3 на UFBV с push-вызовами и без них
Я использую Z3 для запросов UFBV. В настоящее время запрос содержит 2 вызова check-sat . Если я поставлю push 1 сразу после check-sat , Z3 решит запрос за 30 секунд. Если я вообще не ставлю push 1 , то есть имею два вызова check-sat без...
1025 просмотров
schedule
17.04.2023
Могу ли я указать решение или область поиска в Z3?
Поясню свой вопрос на примере:
Предположим, у меня есть область возможных дискретных целых чисел, например, -1, 0, 2, 3, 5 и 6. Теперь я ищу решение (или модель) для переменной x, которое будет удовлетворять следующим ограничениям:
(x > 0) && (x...
160 просмотров
schedule
09.04.2023
Работает ли опция pull_nested_quantifiers с упрощением в Z3?
Я хотел бы вывести все вложенные квантификаторы в формулу на самый внешний уровень. Я ожидал, что следующие команды будут работать в Z3, но они не работают:
(set-option :pull-nested-quantifiers true)
(simplify (exists ((x Int)) (and (>= x 0)...
232 просмотров
schedule
29.06.2023
Квантификатор против неквантификатора
У меня вопрос по квантификаторам.
Предположим, что у меня есть массив, и я хочу вычислить индекс массива 0, 1 и 2 для этого массива -
(declare-const cpuA (Array Int Int))
(assert (or (= (select cpuA 0) 0) (= (select cpuA 0) 1)))
(assert (or (=...
740 просмотров
schedule
12.02.2024
как скомпилировать пример кода из Z3 под linux
Я скачал z3 для версии для Linux и пытался заставить его работать под Linux, но он не компилировался (я компилировал код примера с помощью gcc). Я получил список неопределенных ссылок от компилятора gcc. Я полагаю, что указал расположение файла lib...
842 просмотров
schedule
23.05.2024
Переписывание формул
В этой статье (раздел 3.2) говорится, что z3 применяется переписывание/упрощение формул перед выполнением каких-либо других шагов.
Предположим, у меня есть формула в QF_UF , состоящая из нескольких операторов assert . Есть ли какое-либо...
288 просмотров
schedule
26.05.2023
Дает ли Z3 минимальное невыполнимое ядро до сих пор?
Я хочу знать, может ли Z3 сейчас дать минимальное неудовлетворительное ядро. Или есть кто разработал хорошую поддержку для этого? Кто-нибудь знает это?
Спасибо большое.
1191 просмотров
schedule
09.01.2024
Создание экземпляра квантификатора на основе модели и фрагмент стратифицированной сортировки
в документации Z3 говорится о экземпляре квантификатора на основе модели (MBQI):
Фрагмент стратифицированных сортов
Фрагмент статифицированных сортировок - еще один разрешимый фрагмент многих формул сортированной логики первого порядка....
326 просмотров
schedule
06.01.2024
Z3 .NET API для квантификатора существования
Я пытаюсь использовать Z3 .net API, чтобы получить выражение квантификатора существования. Ниже приведен мой код:
RealExpr c = ctx.MkRealConst("c");
BoolExpr Eqzero = ctx.MkGt(c,ctx.MkReal(0));
BoolExpr Gezero = ctx.MkGe(c,ctx.MkReal(0));...
330 просмотров
schedule
24.04.2023
как определить-fun с помощью C # API
Используя Z3 с текстовым форматом, я могу использовать define-fun для определения функций для повторного использования позже. Например:
（define-fun test((a Int) (b Int)) Int
（ite (and (> a 2) (<= b 3))
1...
235 просмотров
schedule
20.04.2023
в чем разница между упрощением и ctx-solver-simplify в z3
начиная с текущей версии, есть некоторая проблема в "ctx-solver-simplify", как в примере http://rise4fun.com/Z3/CqRv z3 дает неверный ответ. Я заменил «ctx-solver-simplify» на «упростить», например http://rise4fun.com/Z3/x9X4 Мне интересно, в чем...
1846 просмотров
schedule
01.06.2022
(Z3Py) какие-либо ограничения в объявлении функций?
Есть ли ограничения в объявлении функций?
Например, этот фрагмент кода возвращает unsat.
from z3 import *
def one_op (op, arg1, arg2):
if op==1:
return arg1*arg2
if op==2:
return arg1-arg2
if op==3:
return...
249 просмотров
schedule
30.10.2023
Компиляция привязки z3 ocaml в linux
Я пытаюсь скомпилировать привязку OCaml для z3 в Linux.
Я попытался использовать предоставленный Makefile: я сделал «сделать ocamlrelease», но он прерывается с ошибкой cp: cannot stat `ml_release/build-lib.sh': нет такого файла или каталога
Я...
447 просмотров
schedule
05.12.2022
Поддерживает ли Z3 преобразование Real-to-Int?
В Z3 вы должны to_real получить реальный эквивалент Int. Есть ли какая-то поддержка обратных преобразований, то есть усечения, округления и т.п.? В отрицательном случае, каким может быть наиболее удобный для Z3 способ их определения, если таковой...
700 просмотров
schedule
27.04.2022
Доступ к элементам сортировки с несколькими полями
У меня возникли проблемы с использованием сортировки в формате SMTlib2. Например, я определяю интервал как:
(declare-sort Pair 2)
(define-sort Interval () (Pair Int Int))
Теперь, как я могу вернуть новый интервал из функции? например.:...
292 просмотров
schedule
11.01.2024
Моделирование доступа к памяти на Z3
Я моделирую доступ к памяти программы с помощью Z3, и у меня есть сомнения относительно производительности, которыми я хотел бы поделиться.
Я хотел компактно смоделировать что-то вроде:
memset(dst, 0, 1000);
Моя первая попытка состояла в...
408 просмотров
schedule
17.12.2022
Асимметричное поведение в ctx-solver-simplify
Я вижу довольно неожиданное поведение ctx-solver-simplify , где порядок параметров для z3.And(), кажется, имеет значение, используя последнюю версию Z3 из основной ветки https://git01.codeplex.com/z3 (89c1785b):
#!/usr/bin/python
import z3
a,...
636 просмотров
schedule
30.01.2023
Z3 возвращает неизвестный
У меня есть простой набор ограничений, с которыми Z3 не справляется:
http://pastebin.com/3eaLQ9wx
Есть ли способ настроить ограничения, чтобы получить результат? Это простой пример большего набора ограничений (тысячи), но меня как-то...
527 просмотров
schedule
18.08.2022
Z3: преобразовать выражение Z3py в SMT-LIB2 из объекта Solver
Этот вопрос очень похож на: Z3: преобразовать выражение Z3py в SMT-LIB2?
Можно ли генерировать вывод SMT-LIB2 из объекта Solver?
1025 просмотров
schedule
06.03.2022
