Вопросы по теме 'smt'
Z3: Извлечение значений экзистенциальной модели
Я играю с решателем Z3 QBVF и задаюсь вопросом, можно ли извлечь значения из экзистенциального утверждения. А именно, скажем, у меня есть следующее:
(assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x))))
В основном...
3148 просмотров
schedule
14.07.2022
Проблема с производительностью неудовлетворительных моделей
Я использую Z3 для создания ограниченного средства проверки моделей. Я сталкиваюсь со странной проблемой производительности при попытке реализовать тест на полноту. Тест на полноту должен убедиться, что все состояния содержат каждое состояние не...
242 просмотров
schedule
11.10.2022
Используйте Z3 и smtlib для расчета конфигурации / модели со смешанными значениями
Как рассчитать приписываемые значения? Вот пример:
(declare-fun x () bool)
(declare-fun y () bool)
(declare-fun z () bool)
(assert (AND x (OR y z)))
С этим я бы получил 2 модели:
x=true and y=true
x=true and z=true
Теперь я хочу...
570 просмотров
schedule
14.08.2022
исключение квантора по битовым векторам дает слишком сложные результаты
Я использую функцию ELIM_QUANTIFIERS Z3, чтобы исключить кванторы из формул над битовыми векторами. Я столкнулся со следующей ситуацией, когда Z3 дает правильный, но слишком сложный результат, и мне было интересно, существует ли способ переписать мою...
414 просмотров
schedule
18.10.2022
Кодирование дифференциального уравнения первого порядка в виде формулы первого порядка
Может ли кто-нибудь помочь мне указать, какое будет лучшее кодирование следующего уравнения с использованием формулы первого порядка, чтобы дать его в качестве входных данных для решателя SMT ??
x`=Ax+b
601 просмотров
schedule
08.05.2023
как упростить результат скрытия переменной с помощью z3?
Я хочу скрыть некоторые переменные и получить упрощенные результаты.
Я хочу скрыть c1 , c2 и d следующим образом:
(declare-const v1 Real)
(declare-const v2 Real)
(elim-quantifiers (exists ((c1 Real) (c2 Real)(d Real))...
147 просмотров
schedule
24.04.2024
Устранение переменных в решателях SAT / SMT
Есть ли в решении SMT / SAT какой-нибудь метод определения нерелевантных переменных по формуле? то есть те, которые могут иметь любое значение и не влияют на выполнимость формулы.
500 просмотров
schedule
11.06.2022
Скулемизация в Z3
Я пытаюсь удалить кванторы существования в своей теории, используя сколемизацию . Это означает, что я заменяю кванторы существования функциями, которые параметризуются универсальными кванторами переменных в области действия кванторов существования....
703 просмотров
schedule
28.09.2022
Z3 с интерполяцией Крейга (iz3)
Я пытаюсь сгенерировать интерполянты Крейга с помощью C API, но получаю неверные результаты. Однако, когда я выгружаю ту же проблему в файл через Z3_write_interpolation_problem и вызываю iZ3, я получаю ожидаемый интерполант.
Я прилагаю код, чтобы...
682 просмотров
schedule
20.05.2023
Доказательство теоремы Z3: теорема Пифагора (нелинейная арифметика)
Почему?
Контекст варианта использования, в котором возникает моя проблема
Я определяю 3 случайных элемента треугольника. Microsoft Z3 должен выводить:
Удовлетворительны ли ограничения или имеются недопустимые входные значения?
Модель для...
917 просмотров
schedule
16.02.2023
Повтор совпадающих моделей в Z3py
В следующем рабочем примере я пытаюсь получить совпавшие модели, в данном случае есть две подходящие модели:
t1= cl7 t2= cl4 t3= cl5
и
t1= cl4 t2= cl3 t3= cl9
Проблема заключается в повторении...
70 просмотров
schedule
09.01.2023
Как пошаговое решение работает в Z3?
У меня вопрос, как Z3 постепенно решает проблемы. Прочитав здесь несколько ответов, я обнаружил следующее:
Есть два способа использования Z3 для инкрементального решения: один - в режиме push / pop (стек), другой - с использованием...
3354 просмотров
schedule
29.01.2023
Как выполнить следующий код SMT-LIB с помощью Alt-Ergo
Следующий код SMT-LIB работает без проблем в Z3, MathSat и CVC4, но не работает в Alt-Ergo. Пожалуйста, дайте мне знать, что произойдет, большое спасибо:
(set-logic QF_UF)
(set-option :incremental true)
(set-option :produce-models true)...
512 просмотров
schedule
20.04.2022
Все возможные значения для типа данных записи в Z3?
Я пытаюсь определить тип данных записи в z3, состоящий из шести элементов разных типов. Вот как я это сделал: (declare-datatypes() ((S (mk-pair (p1 (P1type)) (p2 (P2type)) (p3 (P3type)) (m1 (bool)) (m2 (bool)) (m3 (bool)) )))) Но когда я использую...
598 просмотров
schedule
14.10.2022
Как определить количество решений данного экземпляра с помощью Mathsat
Mathsat поддерживает команду check-allsat , а Z3 ее не поддерживает. Пожалуйста, рассмотрите следующий пример:
(declare-fun m () Bool)
(declare-fun p () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun r () Bool)
(declare-fun...
289 просмотров
schedule
15.03.2023
Haskell: привязка к быстрому и простому SAT-решателю
Сегодня я тоже хотел рассмотреть варианты решения SAT в Haskell. Сначала я задумался о написании собственного интерфейса для решателя Picosat.
Затем я обнаружил, что существует библиотека SBV . Это интерфейсы для Z3, Yices, CVC4 и Boolector....
2293 просмотров
schedule
22.06.2022
Почему медленнее получать результат запроса из z3 java API, чем напрямую из z3?
Только что заметил, что для некоторых тестов очень медленно получать результат запроса от z3 через java API. Однако, если я просто выгружу запрос в формат smt2 и запущу z3 напрямую в командной строке, это займет меньше секунды. Интересно, почему?
157 просмотров
schedule
09.05.2023
Эксклюзивные типы данных в z3 (продолжение)
Я объявил эксклюзивный тип данных в z3, а также константу и небольшое утверждение:
(declare-datatypes () ((IntOrBool (bpart (b Bool)) (ipart (i Int)))))
(declare-fun iob () (IntOrBool))
(assert (= true (b iob)))
Я получаю ожидаемый...
64 просмотров
schedule
25.04.2022
Какова единица использования памяти в статистике Z3?
В каких единицах измеряется использование памяти в статистике z3? Это МБ или КБ?
И что именно означает память? Это максимальное использование памяти или совокупная сумма всех распределений во время выполнения?
170 просмотров
schedule
10.04.2022
Использование Z3 и SMT-LIB для поиска наивысшего палиндромного произведения
На основе "Разработка только для тестирования" с помощью средства доказательства теорем Z3 , Я пытаюсь закодировать проблему Эйлера 4 в SMT-LIB и решить ее с помощью Z3.
Задача состоит в том, чтобы найти наибольшее целочисленное палиндромное...
147 просмотров
schedule
11.06.2022
