Описание тега z3-fixedpoint

Вопросы с тегом
Вопросы о механизме неподвижной точки средства доказательства теорем Z3.
0 ответов

Роговая оговорка в Z3 висит

У меня есть следующий фрагмент кода с использованием самой последней версии z3-solver это прекрасно работает: def test_list_elt_gt_1(): ll = Datatype('ll') ll.declare('empty') ll.declare('cons', ('car', IntSort()), ('cdr', ll)) ll = ll.create() list…
07 авг '19 в 13:38
1 ответ

Роговые предложения с умножением в Z3

Я только начал копаться в решателе с фиксированной запятой в Z3 и подготовил пример, который зависает при использовании умножения, но завершается при определении умножения как серии дополнений. Поскольку я новичок в работе с клаузлами Хорна, может б…
01 авг '19 в 08:22
1 ответ

Почему Z3 возвращает Неизвестно для этих пунктов рога

Я использую Z3, чтобы решить свои предложения рог. В теле предложений Horn неинтерпретированные предикаты должны быть положительными. Однако мне нужно отрицание некоторых неинтерпретированных предикатов. Я видел несколько примеров, в которых отрицан…
11 окт '19 в 11:39
1 ответ

Какие придирки эквивалентны этим положениям?

Я использую Z3 и расширенный синтаксис SMT-LIB2 для решения моих предложений рог. Я знаю, что заголовок предложения рог должен быть неинтерпретируемым предикатом; но мне интересно, как мне переписать следующие пункты, чтобы они были набором предложе…
14 окт '19 в 15:15
0 ответов

Как написать предложение рог с ложным головой в Z3?

Я использую Z3 и расширенный синтаксис SMT-LIB2 для решения моих предложений рог. Заголовок предложения рог должен быть неинтерпретируемым предикатом; но мне интересно, как я могу переписать следующий пункт как пункт рог. (declare-rel p(Int)) (decla…
15 окт '19 в 13:06
0 ответов

Z3: сочетание оптимизации и фиксированных точек

Я могу объяснить любую необходимую глубину, но короче говоря, мой проект использует оптимизатор Z3 для поиска максимального решения проблемы SAT с весами, связанными с логическими переменными. Помимо этого, другая часть моего проекта эффективно реал…
14 сен '19 в 21:27
2 ответа

Запрос Python Z3 API: можем ли мы получить частичную модель, используя z3 python API, когда решатель возвращает неизвестный статус

Я почти уверен, что это как-то связано с API Python. Есть ли способ вернуть частичную модель из z3, даже если статусunknown? Пытаюсь вытащить модель из z3 даже когда статус возвращается unknownрезультат. Не удается поднятьexception за model not avai…
02 сен '20 в 11:04
0 ответов

почему результат решения z3 horn неизвестен и почему это неизвестная причина

Я использую z3 для проверки эквивалентности. Я пытаюсь использовать z3 horn solver, чтобы ускорить время решения z3, и я столкнулся со следующей проблемой: Хочу проверить, совпадают ли две программы или нет. Логика двух программ - P1: a2 = a1 + 2, г…
12 июн '20 в 22:41
1 ответ

z3: предложения Horn / фиксированные точки над индуктивными типами данных

Я пытаюсь сделать утверждения об эквивалентности программ, используя фиксированные точки z3, и обнаружил, что любая рекурсия, даже тривиально разрешимая рекурсия, полностью подавляет z3. В этом руководстве по z3py в качестве примера использования фи…
17 сен '20 в 21:19
0 ответов

Как использовать модельно-ориентированную проекцию Z3 из C/C++?

Я хочу использовать модельно-ориентированную проекцию, которая поставляется с Z3 / Spacer из C / C++, я заметил Z3_qe_model_project в "z3_spacer.h", однако после нескольких экспериментов я так и не понял, как его использовать, так как по нему нет до…
09 авг '21 в 16:39