Описание тега z3py
Python interface for the Z3 Theorem Prover
2
ответа
Ненулевой вектор в квантификаторе
Я хочу проверить формулу формы: Exists p . ForAll x != 0 . f(x, p) > 0 Реализация (которая не работает) заключается в следующем: def f0(x0, x1, x, y): return x1 ** 2 * y + x0 ** 2 * x s = Solver() x0, x1 = Reals('x0 x1') p0, p1 = Reals('p0 p1') s…
10 май '18 в 18:19
2
ответа
Объявить матрицу с неизвестным размером в Z3
Я знаю, что я могу объявить матрицу z3.Real в Z3 объявив его элементы индивидуально (может быть, через понимание списка). Есть ли способ представить матрицу с неизвестным размером? Например, рассмотрим следующий пример: при фильтрации изображений, д…
14 апр '17 в 02:42
1
ответ
Тайм-аут для решателя z3 в python
У меня проблемы с установкой таймаута для моего решателя: s = Solver() encoding = parse_smt2_file("ex.smt2") s.add(encoding) s.set("timeout", 600) solution = s.check() но я получаю следующую ошибку Traceback (most recent call last): File "/Users/X/D…
05 фев '15 в 07:23
1
ответ
Почему z3.And() работает медленно?
Я использую привязки Z3 Python для создания выражения And через z3.And(exprs) где exprs список питонов из 48000 ограничений на равенство по логическим переменным Эта операция занимает 2 секунды на MBP с процессором 2,6 ГГц. Что я могу делать не так?…
15 окт '14 в 06:21
1
ответ
Невозможно извлечь значение для Z3 EnumSort в z3py
В настоящее время я пытаюсь закодировать проблему в Z3, и я хочу смоделировать "трехуровневый" логический (то есть, логический с true, false а также unknown). Вот как я смоделировал это: #!/usr/bin/env python import z3 from collections import Ordere…
17 окт '17 в 12:41
1
ответ
Использование массива в Z3PY
Я использую z3 для своего исследования, и у меня есть следующая проблема. Я анализирую модель выполнимой формулы, которая содержит массивы, но я не понимаю результатов модели. Например, у меня есть две переменные 'pkgcounter' и 'rxlen' и два предлож…
19 июл '16 в 13:53
0
ответов
Как получить z3 в пичарме?
Я просто подумал, что должен попробовать Pycharm и Z3 доказатель теоремы, но мне трудно его настроить. Метод 1 Я использую Windows 8, и моей первой попыткой было установить пакет z3 с помощью pycharm (пакет z3-solver в меню "Настройки" -> "Интерпрет…
25 мар '17 в 08:32
2
ответа
z3 проверка переполнения битвектора из python?
C API для z3 имеет такие функции, как Z3_mk_bvadd_no_overflow, но они, похоже, недоступны из Python API. Прежде чем приступить к взлому, чтобы решить эту проблему, я просто хочу убедиться, что это так, а также попросить, чтобы они были добавлены в о…
21 мар '14 в 20:26
1
ответ
Как определить количество решений данного экземпляра с помощью Mathsat
Mathsat поддерживает команду check-allsat и Z3 не поддерживает его. Пожалуйста, рассмотрите следующий пример: (declare-fun m () Bool) (declare-fun p () Bool) (declare-fun b () Bool) (declare-fun c () Bool) (declare-fun r () Bool) (declare-fun al () …
05 ноя '13 в 01:43
1
ответ
z3py: как проверить информацию трассировки при использовании z3 python api
Предположим, я хочу проверить информацию трассировки "random_split". я написал enable_trace("random_split") в моем скрипте Python, который использует Z3 Python API, но ничего не появляется. Интересно, как мне проверить информацию трассировки при исп…
24 ноя '15 в 16:31
1
ответ
Z3py не может решить энергетический оператор
Я новичок в Z3py, и я использовал последнюю z3py z3-4.4.2.4e7a867cd995-x64-win. Но мне просто интересно, почему z3py не может решить следующий код. from z3 import * x = Int('x') s = Solver() s.add(x**2 == 4) print s.check() Я узнал, а не сел.
25 фев '16 в 19:22
1
ответ
.datalog формат с использованием Z3
Я пытаюсь использовать расширение Z3: muZ с ограничениями с фиксированной запятой после этого урока: https://rise4fun.com/Z3/tutorial/fixedpoints. Как отмечено в этом руководстве, принимаются три различных текстовых формата ввода. Базовый каталог да…
11 июн '18 в 15:01
1
ответ
Исключение квантификаторов z3 в синтаксисе SMTLIB
У меня есть следующий пример устранения квантификаторов с использованием z3py ниже. Однако я хотел бы переписать его с использованием синтаксиса SMTLIB (код ниже кода Python). Каким-то образом я не получил такой же вывод, как то, что я получил от Py…
06 июн '17 в 02:03
2
ответа
Z3 Prover возвращает неверное решение
Я пытаюсь решить уравнение с Z3 Thoerem Prover в Python. Но решение, которое я получаю, неверно. from z3 import * solv = Solver() x = Int("x") y = Int("y") z = Int("z") s = Solver() s.add(x/(y+z)+y/(x+z)+z/(x+y)==10, x>0, y>0, z>0) s.add() …
08 окт '17 в 21:05
1
ответ
Оценить BitVec в Z3Py
Я изучаю Z3 и, возможно, мой вопрос не подходит, поэтому, пожалуйста, будьте терпеливы. Предположим, у меня есть следующее: c1, c2 = z3.BitVec('c1', 32), z3.BitVec('c2', 32) c1 = c1 + c1 c2 = c2 + c2 c2 = c2 + c1 c1 = c1 + c2 e1 = z3.simplify(c1) e2…
04 мар '18 в 06:54
1
ответ
Как использовать пошаговое решение с z3py
Я использую Python API решателя Z3 для поиска оптимизированных расписаний. Он работает довольно хорошо, за исключением того, что иногда он очень медленный даже для небольших графиков (иногда очень быстрый). Причиной этого, вероятно, является то, что…
10 июл '18 в 18:35
2
ответа
Как я могу получить доступ к отображению переменных, используемому при дробеструйной обработке?
Я модифицирую инструмент, который использует Z3 (в частности, API-интерфейс Python) для решения ограничений битового вектора. Мне нужно использовать конкретный внешний SAT-решатель вместо внутреннего Z3, так что я первым делом использую тактику Then…
18 июн '15 в 16:57
1
ответ
Как эффективно решать комбинации теорий в Z3
Я пытаюсь решить проблему, которая включает пропозициональную выполнимость (с квантификаторами) и линейную арифметику. Я сформулировал проблему, и Z3 может решить ее, но это занимает неоправданно много времени. Я пытался помочь Z3 вместе с определен…
06 дек '13 в 19:02
1
ответ
Нахождение самой слабой предпосылки с помощью z3py
Я хочу найти самое слабое предварительное условие, заданное действием и последующим условием, используя z3py. Учитывая действие N = N + 1 и почтовое условие N == 5 самым слабым предварительным условием было бы N == 4. Используя Тактику solve-eqs это…
23 июн '13 в 05:24
0
ответов
Как реализовать логику AND в Z3Py
Я хочу реализовать ограничение, которое требует логики AND в Z3Py. Предположим, у нас есть две переменные a а также bЯ просто хочу добавить одно ограничение, которое требует a == 0 а также b == 1, Там должно быть несколько способов, которые могут сд…
31 июл '18 в 19:45