Вопросы по теме 'smt'
Доступ к элементам сортировки с несколькими полями
У меня возникли проблемы с использованием сортировки в формате SMTlib2. Например, я определяю интервал как:
(declare-sort Pair 2)
(define-sort Interval () (Pair Int Int))
Теперь, как я могу вернуть новый интервал из функции? например.:...
292 просмотров
schedule
11.01.2024
Z3 возвращает неизвестный
У меня есть простой набор ограничений, с которыми Z3 не справляется:
http://pastebin.com/3eaLQ9wx
Есть ли способ настроить ограничения, чтобы получить результат? Это простой пример большего набора ограничений (тысячи), но меня как-то...
527 просмотров
schedule
18.08.2022
установка z3py
У меня возникли проблемы с тем, чтобы заставить z3 работать с Python. Я использую Windows 7 64bit. Я скачал 64-битную версию Python 3.3.0 и 64-битную версию z3 4.3.0. Я обновил PATH и PYTHONPATH, включив в них каталог z3\bin. Однако, когда я...
1509 просмотров
schedule
24.01.2023
Как я могу решить ограничение минимизации в Z3?
Может ли кто-нибудь сказать мне, как я могу реализовать задачу минимизации целых чисел, подобную приведенной ниже, с помощью Z3py? Как я могу определить для всех утверждений? Здесь все переменные int sort.
Есть ли в Z3 специальный решатель...
1446 просмотров
schedule
10.06.2023
Для чего ключевое слово mutable в исходном коде Moses?
Речь идет об исходном коде системы статистического машинного перевода Moses . . В классе Factor проекта Mosesdecoder есть такое странное использование ключевого слова mutable :
class Factor {
__SOME_OTHER_CODE__
//...
236 просмотров
schedule
14.02.2023
Тесты SMT-LIB
Я хотел бы протестировать некоторые решатели SMT, и репозиторий SMT-LIB Benchmark [1,2] кажется хорошим местом для начала.
Однако ссылка не работает уже как минимум несколько дней. Кто-нибудь знает какое-либо другое место, где я могу найти эти...
412 просмотров
schedule
27.01.2024
Используйте Z3 и SMT-LIB для определения функции sqrt с вещественным числом.
Как я могу написать функцию sqrt в формате smt-libv2.
Примечание. Чтобы получить максимум два значения, я нашел здесь полезную ссылку: Используйте Z3 и SMT-LIB, чтобы получить максимум два значения .
540 просмотров
schedule
27.04.2023
Производительность решателя z3 SMT на разных платформах
У меня есть логические проблемы, написанные с использованием z3py. Я запускаю их как на своем ПК (intel core i5 + 8 ГБ ОЗУ), так и на кластере (32 процессора AMD Operaton 6320 + 500 ГБ ОЗУ). Нет большой разницы во времени выполнения, и иногда...
640 просмотров
schedule
22.03.2023
Z3 - проба вызывает ошибки сегментации
Я использую Java-API для связи с Z3 в Ubuntu Linux 14.04. Что касается Z3, я использую текущую версию master-ветки, найденную на github (скомпилированную сегодня).
Базовая структура формул, выполнимость которых я хочу проверить, выглядит следующим...
173 просмотров
schedule
30.12.2021
Присвоить значение определенному биту BitVecExpr в Z3
Вот мое утверждение Verilog:
reg[2:0] a; // Create register 'a' which is 3 bit.
assign a[1] = 1'b1; // Assigning value to 1st bit of register 'a'.
Я должен реализовать приведенное выше утверждение в Z3. Для 1-й строки оператора...
141 просмотров
schedule
12.03.2024
Почему Z3 не может решить этот случай без, казалось бы, тривиальной модификации?
Первоначальная проблема:
(declare-const a Real)
(declare-const b Bool)
(declare-const c Int)
(assert (distinct a 0.))
(assert (= b (distinct (* a a) 0.)))
(assert (= c (ite b 1 0)))
(assert (not (distinct c 0)))
(check-sat)
Результат...
95 просмотров
schedule
18.05.2023
Как отобразить конкретное ограничение unsat, а не все ядро (Z3, Python)
Как я могу перечислить только конкретные результаты ограничений из моего ненасыщенного ядра? У меня много условий, и печать всего ядра не печатает все. Я читал, что это можно сделать с помощью команд assert_and_track и unsat_core. Я нашел несколько...
804 просмотров
schedule
22.01.2024
Неявная и явная количественная оценка существования в формулах SMT
Учитывая следующий код:
from z3 import *
a,b,c = BitVecs('a b c', 32)
f1 = Exists([a, b, c], And(a + b == c, a < b, c == 1337))
f2 = And(a + b == c, a < b, c == 1337)
prove(f1 == f2)
Я бы предположил, что в этом примере z3 неявно...
202 просмотров
schedule
04.08.2023
Существует ли глобальная конструкция forall на языке SMT или расширение Z3?
По умолчанию глобальные переменные рассматриваются как экзистенциально квантифицированные. Например.
(declare-const x Int)
(assert (exists ((y Int)) (and (= x y) (= x y))))
(check-sat)
(get-model)
Дает
sat
(model
(define-fun y!0 ()...
505 просмотров
schedule
30.05.2023
∃-запросы и ∀-запросы с движком фиксированной точки Z3
Я смущен и изо всех сил пытаюсь понять, как связаны два разных формата ввода для движка с фиксированной точкой Z3. Краткий пример: предположим, я хочу доказать существование отрицательных чисел. Я объявляю функцию, которая возвращает 1 для...
501 просмотров
schedule
17.12.2022
Использование z3 api для решения LRA работает медленнее, чем использование z3 в терминале
Я пытаюсь использовать Z3 для решения случайной обобщенной задачи упаковки полос (LRA) и вызываю Z3 api в программе c, вот код.
Z3_context ctx;
Z3_ast fs;
LOG_MSG("smt2parser_example");
FILE *fp = fopen("smttest","r");
if(fp == NULL)
{...
63 просмотров
schedule
22.01.2023
Реализация побитовой обработки для арифметики с плавающей запятой в SMT
Мне было интересно, как люди реализуют бит-взрыв арифметических конструкций с плавающей запятой в решателях SMT. Существуют ли какие-либо существующие библиотеки или средства для этого (VHDL, ...) или они реализованы с нуля? Это представляет,...
578 просмотров
schedule
09.03.2022
Как z3 'smt_tactic' решает формулы QF_BV?
Когда z3 использует smt_tactic (вместо тактики qfbv ) для решения формулы QF_BV, будет ли он использовать битовые взрывы и использовать движок SAT? Когда я устанавливаю уровень детализации на 10, я не вижу битовых взрывов.
130 просмотров
schedule
16.11.2022
Как я могу сказать Z3, с чего начать при решении формулы?
В настоящее время я имею дело с ситуацией, когда утверждения Z3 содержат большое количество неравенств и равенств. Они зависят друг от друга таким образом, что наиболее эффективно начать решение формулы с присвоения значений переменным, используемым...
57 просмотров
schedule
14.10.2022
Какие дополнительные аксиомы нам нужно добавить, чтобы Z3 мог проверять выполнимость программ с повторениями?
Как мы знаем , Z3 имеет ограничения с рецидивами. Есть ли способ получить результат для следующей программы? какое дополнительное уравнение поможет z3 получить результат?
from z3 import *...
326 просмотров
schedule
23.07.2023
