0
ответов
Использование перезаписи терминов в процедурах принятия решений для бит-векторной арифметики
Я работаю над проектом, в центре внимания которого лежит использование перезаписи терминов для решения / упрощения задач арифметики битовых векторов фиксированного размера, что полезно для сделать как предварительный шаг к какому-то решению ...
вопрос задан: 25 November 2011 18:31
0
ответов
Эквивалент define-fun в Z3 API
Используя Z3 с текстовым форматом, я могу использовать define-fun для определения функций для повторного использования в дальнейшем. Например: (define-fun mydiv ((x Real) (y Real)) Real (if (not (= y 0.0)) (/ xy) 0.0)) ...
вопрос задан: 12 October 2011 13:07
0
ответов
Подсчет ссылок Z3_ast подсчитывает ссылки вне Z3?
В Z3 есть 2 режима: автоматический подсчет ссылок и ручной. Я понимаю, как работает ручной подсчет ссылок. Благодаря примеру. Но как Z3 узнает, когда нужно удалить узел AST в автоматическом ref -...
вопрос задан: 21 September 2011 19:29
0
ответов
Можно ли использовать Z3 для рассуждений о подстроках?
Я пытаюсь использовать Z3 для рассуждений о подстроках и столкнулся с некоторым неинтуитивным поведением. Z3 возвращает 'sat', когда его спрашивают, появляется ли 'xy' в 'xy', но он возвращает 'unknown', когда ...
вопрос задан: 20 August 2011 09:30
0
ответов
Поддерживает ли Z3 интерполяцию Крейга
Может ли Z3 генерировать интерполянты Крейга (по крайней мере, для логики высказываний?).
Я не нашел его в документации Z3.
вопрос задан: 10 August 2011 10:32
0
ответов
Ищете практические примеры использования SMT Z3 (например, DbC) и альтернативу Z3 с открытым исходным кодом? [закрыто]
Я заинтересовался и искал практические примеры использования SMT Z3 (например, DbC) с кодом и альтернативами этому инструменту с открытым исходным кодом. Так что на самом деле Меня интересует подобное формальное решение Z3 ...
вопрос задан: 3 August 2011 22:17