1
ответ
Абстрагирование над группами утверждений в Z3 / SMT-LIB
Есть ли в Z3 хорошие механизмы для абстрагирования над утверждениями? Я хочу создать «функцию», которая принимает параметры и делает утверждения об этих параметрах, возможно, с помощью «локальной переменной» ...
вопрос задан: 24 March 2019 03:52
1
ответ
Z3 считает модель несовместимой с аксиомами
При запуске этого кода на Python 3.6.7 с модулем z3-solver (4.8.0.0) модель, возвращаемая z3, кажется, не подходит для аксиом. f = z3.Function ('f', z3.IntSort (), z3.IntSort (), z3.IntSort ()) x = ...
вопрос задан: 18 January 2019 17:38
1
ответ
Булева матрица умножает векторное умножение в Z3
Как легко умножить переменную булеву матрицу на булевский вектор в Z3? Размеры матрицы и векторов известны и фиксированы. В моем случае есть только одна матрица, и нет необходимости ...
вопрос задан: 13 July 2018 15:25
0
ответов
Решить несколько уравнений, используя Z3
У меня есть следующая функция, которая принимает входную строку и число для генерации хеша, как показано ниже: #! / usr / bin / python def calc_hash (ключ, num): результат = 0 для i в диапазоне (len (ключ)): ...
вопрос задан: 10 March 2019 01:49
0
ответов
Решатель уравнений Z3 - операция с битовой маской
После обратного проектирования программы, я нашел ограничения. Я должен найти два числа без знака, такие, что: x + y = 0xC0ED91BD и x * y = Z В оригинальной программе, умножение ...
вопрос задан: 18 January 2019 20:10
0
ответов
Квантификаторы и шаблоны (формула QBF)
Я пытаюсь закодировать QBF в синтаксисе smt-lib 2 для z3. Запуск z3 приводит к предупреждению ПРЕДУПРЕЖДЕНИЕ: не удалось найти шаблон для квантификатора (идентификатор квантификатора: k!14), и результатом выполнимости является "...
вопрос задан: 23 May 2017 12:31
0
ответов
Может ли Z3 проверить выполнимость рекурсивных функций на ограниченных структурах данных?
Я знаю, что Z3 не может проверить выполнимость формул, содержащих рекурсивные функции. Но мне интересно, может ли Z3 обрабатывать такие формулы в ограниченных структурах данных. Например, я определил список ...
вопрос задан: 23 May 2017 10:29
0
ответов
Кто-нибудь пробовал доказать Z3 с помощью самого Z3?
Кто-нибудь пробовал доказывать Z3 с самим Z3? Возможно ли вообще доказать, что Z3 правильный, используя Z3? Более теоретически, можно ли доказать, что инструмент X правильный, используя сам X?
вопрос задан: 23 February 2017 11:06
0
ответов
(Z3Py )проверка всех решений уравнения
В Z3Py, как я могу проверить, имеет ли уравнение для заданных ограничений только одно решение? Если более одного решения, как я могу их перечислить?
вопрос задан: 8 June 2016 08:59
0
ответов
Создайте массив фиксированного размера и инициализируйте его.
Я собираюсь создать массив фиксированного размера и инициализировать его некоторыми значениями. Например, следующий код C++: a[0] = 10;
а[1] = 23;
а[2] = 27;
а[3] = 12;
а[4] = 19;
а[5] = 31;
а[6] = 41;
a[7]...
вопрос задан: 26 February 2014 21:37
0
ответов
TryFor в Z3 не прекращает проверку по истечении заданного срока
Я использую.NET API Z3. Когда я создаю решатель, вызывая :Solver s = ctx.MkSolver (ctx.TryFor (ctx.MkTactic ("qflia" ), TimeLimit )); и дайте ему TimeLimit 60 секунд (60000...
вопрос задан: 11 June 2013 17:57
0
ответов
( Z3Py )объявление функции
Я хотел бы найти коэффициенты c и t в простой формуле «результат = x *t + c» для некоторых заданных пар результат / x :из импорта z3 *x = Int ('x' )с=целое ('с' )t=Int ('t' )s=Решатель ()f = Функция ('f', IntSort (),...
вопрос задан: 9 August 2012 14:45
0
ответов
Понимание индексации связанных переменных в Z3
Я пытаюсь понять, как связанные переменные индексируются в z3. Вот в сниппете в z3py и соответствующий вывод.(http://rise4fun.com/Z3Py/plVw1)x, y = Ints ('x y' )f1 = ForAll (х, И (х...
вопрос задан: 5 August 2012 12:56
0
ответов
в чем разница между «упростить» и «решатель ctx --упростить» в z3
начиная с текущей версии, есть некоторая проблема в "ctx -Solver -Simple", как в примере http://rise4fun.com/Z3/CqRvz3 дает неправильный ответ. Я заменяю «ctx -Solver -Simplify» на «упрощение», например http :...
вопрос задан: 4 August 2012 13:29
0
ответов
Запуск проблем в Z3
Недавно я наблюдал несколько вариантов поведения Z3 в отношении срабатывания, которые я не понимаю. К сожалению, примеры взяты из больших файлов Boogie, поэтому я решил их описать...
вопрос задан: 26 July 2012 16:48
0
ответов
Преобразование целочисленного выражения Z3 в целое число C/C++
Я новичок в Z3 и искал ответ на свой вопрос здесь и в Google. К сожалению, я не добился успеха. Я использую Z3 4.0 C/C++ API. Я объявил неопределенную функцию d:(Целое Целое )Целое,...
вопрос задан: 25 July 2012 14:29
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
ответов
Разница между Z3 и coq
Мне интересно, может ли кто-нибудь сказать мне разницу между Z3 и coq? Мне кажется, что coq является помощником по доказательству в том смысле, что он требует от пользователя заполнения шагов доказательства, тогда как Z3 не имеет...
вопрос задан: 17 July 2012 22:10
0
ответов
Исключение квантификатора -Дополнительные вопросы
Большое спасибо Джошу и Леонардо за ответы на предыдущий вопрос. У меня есть еще несколько вопросов. <1> Рассмотрим другой пример. (существует k )i *k > = 4 и k > 1. Это имеет простое решение i >...
вопрос задан: 5 May 2012 22:38
0
ответов
Получение «хорошего» ненадежного ядра с помощью z3 (логика QF_BV)
Я использую решатель SMT Z3 для решения проблемы, которую я выразил в логике QF_BV, используя язык SMTLIB 2. Модель неудовлетворительна, и я пытаюсь заставить решатель создать ...
вопрос задан: 28 February 2012 10:36
0
ответов
Необычность теории массивов SMTLIB в Z3
При использовании массивов SMTLIB я заметил разницу между пониманием теории Z3 и моим. Я использую теорию массивов SMTLIB [0], которую можно найти на официальном сайте [1]. Я думаю, что мой ...
вопрос задан: 24 February 2012 13:43
0
ответов
тип данных содержит набор в Z3
как я могу создать тип данных, содержащий набор других объектов. По сути, я делаю следующий код: (define-sort Set (T) (Array Int T))
(declare-datatypes () ((A f1 (cons (value Int) (b (Set B) ...
вопрос задан: 18 February 2012 17:36
0
ответов
Квантификатор в Z3
По сути, я хочу попросить Z3 дать мне произвольное целое число, значение которого больше 10. Поэтому я пишу следующие утверждения: (declare-const х (Инт))
(assert (forall ((i Int)) (> i 10)))
(check -...
вопрос задан: 16 February 2012 15:05
0
ответов
Какова причина предупреждающего сообщения в Z3: «не удалось найти шаблон для квантификатора (идентификатор квантификатора: k! 18)»
Я обнаружил проблему, показанную в следующей простой программе SMT-LIB. Код SMT-LIB: (declare-fun isDigit (Int) Bool)
(assert (forall ((x Int)) (=> (isDigit x) (and (> = x 0) (& ...
вопрос задан: 8 February 2012 08:36
0
ответов
Может ли Z3 работать в инкрементном режиме?
Я использую Z3 в формулах QFBV. Мне было интересно, может ли Z3 работать постепенно с такими формулами, как решатели SAT, могут работать с логическими предложениями. В основном мне нужен способ реализовать следующий цикл: F = ...
вопрос задан: 2 February 2012 22:09
0
ответов
Контрпример вывода Z3
Когда формула в Z3 является неподтвержденной и указано (get-proof), есть результат, о котором я не нахожу никакой информации. Где я могу найти документацию по этому поводу? Мне кажется вполне ...
вопрос задан: 2 February 2012 10:29
0
ответов
Определение верхней/нижней границы для переменных в произвольной пропозициональной формуле [закрыто]
Дана произвольная пропозициональная формула PHI (линейные ограничения на некоторые переменные), какой лучший способ определить (приблизительную) верхнюю и нижнюю границы для каждой переменной? Некоторые переменные могут быть ...
вопрос задан: 24 January 2012 22:17
0
ответов
Несоответствие сортировки в модели
Я проанализировал формулу в QF_AUFLIA с помощью z3. В результате получилось sat. Модель, возвращенная (get-model), содержала следующие строки: (define-fun PCsc5_ () Int (ite (= 2 false) 23 33) Согласно ...
вопрос задан: 3 January 2012 10:03
0
ответов
Мягкие / жесткие ограничения в Z3
Как выразить мягкие и жесткие ограничения в Z3? Из API я знаю, что могут быть предположения (мягкие ограничения), но я не могу выразить это при использовании инструмента командной строки. Я ...
вопрос задан: 9 December 2011 00:50