1
ответ
Абстрагирование над группами утверждений в Z3 / SMT-LIB
Есть ли в Z3 хорошие механизмы для абстрагирования над утверждениями? Я хочу создать «функцию», которая принимает параметры и делает утверждения об этих параметрах, возможно, с помощью «локальной переменной» ...
вопрос задан: 24 March 2019 03:52
1
ответ
Булева матрица умножает векторное умножение в Z3
Как легко умножить переменную булеву матрицу на булевский вектор в Z3? Размеры матрицы и векторов известны и фиксированы. В моем случае есть только одна матрица, и нет необходимости ...
вопрос задан: 13 July 2018 15:25
0
ответов
Как скрыть переменную в Z3
Скажем, у меня есть t1
вопрос задан: 24 July 2012 06:35
0
ответов
Как преобразовать формулу в дизъюнктивную нормальную форму?
Скажем, учитывая формулу (t1>=2 или t2>=3 )и (t3>=1 )Я хочу получить ее дизъюнктивную нормальную форму (t1>=2 и t3>=1 )или (t2>=3 и t3>=1 )Как добиться этого в Z3?
вопрос задан: 22 July 2012 09:45
0
ответов
Ограничения решателей SMT
Традиционно большая часть работы с вычислительной логикой была либо пропозициональной, и в этом случае вы использовали SAT (решатель булевой выполнимости ), либо первый -порядок, и в этом случае вы использовали теорему первого -порядка...
вопрос задан: 21 July 2012 13:11
0
ответов
Необычность теории массивов SMTLIB в Z3
При использовании массивов SMTLIB я заметил разницу между пониманием теории Z3 и моим. Я использую теорию массивов SMTLIB [0], которую можно найти на официальном сайте [1]. Я думаю, что мой ...
вопрос задан: 24 February 2012 13:43
0
ответов
Использование перезаписи терминов в процедурах принятия решений для бит-векторной арифметики
Я работаю над проектом, в центре внимания которого лежит использование перезаписи терминов для решения / упрощения задач арифметики битовых векторов фиксированного размера, что полезно для сделать как предварительный шаг к какому-то решению ...
вопрос задан: 25 November 2011 18:31
0
ответов
Можно ли использовать Z3 для рассуждений о подстроках?
Я пытаюсь использовать Z3 для рассуждений о подстроках и столкнулся с некоторым неинтуитивным поведением. Z3 возвращает 'sat', когда его спрашивают, появляется ли 'xy' в 'xy', но он возвращает 'unknown', когда ...
вопрос задан: 20 August 2011 09:30
0
ответов
SMT-решатели для арифметики битовых векторов
Я планирую несколько экспериментов в символьном исполнении кода C, используя готовый решатель SMT и задаваясь вопросом, какой решатель использовать; глядя, например, участники конкурса SMT,и взяв только open -...
вопрос задан: 7 June 2011 10:33