Вопросы по теме 'z3py'
Z3py: как получить список переменных из формулы?
В Z3Py у меня есть формула. Как я могу получить список переменных, используемых в формуле?
Спасибо.
1613 просмотров
schedule
30.07.2023
Использование исключения квантифера с Z3 Python
Я пытаюсь найти значения для A,B,C,D, удовлетворяющие формуле g = And(ForAll([i, j, k], Implies(And(k <= 0, A * i + B * j + C * k + D <= 0), k + i - j <= 0)),Not(And(A==0,B==0,C==0))) , используя solve(g) . У этого есть много возможных...
450 просмотров
schedule
02.08.2023
Массивы и типы данных в Z3py
На самом деле я использую Z3py для планирования решения проблем и пытаюсь представить двухпроцессорную систему, в которой должны выполняться четыре процесса с разным временем выполнения.
Мои фактические данные: Процесс 1: Прибытие в 0 и время...
1598 просмотров
schedule
29.03.2022
Z3Py - получить все формулы, содержащие выражение
Можно ли в Z3Py получить список всех формул, в которых встречается какая-либо переменная / выражение? Пример:
s.add(x < 0)
s.add(x > y)
print s[y]
>>> x > y
130 просмотров
schedule
17.02.2023
z3py упрощение выражения
Я пытаюсь упростить выражение с помощью z3py, но не могу найти никакой документации о том, что делают разные тактики. Лучший ресурс, который я нашел, - это вопрос о переполнении стека , который перечисляет все тактики по названию.
Может ли...
355 просмотров
schedule
02.06.2022
Как определить количество решений данного экземпляра с помощью 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...
289 просмотров
schedule
15.03.2023
Где я могу найти руководства по z3py
rise4fun z3py недоступен в течение нескольких недель из-за некоторых проблем с безопасностью. Я пытался найти ресурсы для изучения z3py, но безуспешно. Пожалуйста, предложите несколько ресурсов для изучения z3py
2264 просмотров
schedule
24.03.2022
Проверка переполнения битового вектора z3 из python?
В C API для z3 есть такие функции, как Z3_mk_bvadd_no_overflow, но, похоже, они недоступны в Python API. Прежде чем я начну взламывать, чтобы решить эту проблему, я просто хотел бы убедиться, что это так, а также попросить добавить их в официальную...
1047 просмотров
schedule
07.01.2023
забава в Z3, возвращающая более одного элемента
Насколько я понимаю, я могу объявить функцию, которая возвращает более одного элемента. скажем, у меня есть функция x, которая получает сортировку T и возвращает сортировку U и сортировку R.
(объявление-сортировка T) (объявление-сортировка R)...
85 просмотров
schedule
24.06.2023
Головоломка с пересечением реки в z3
Я только начал изучать решатель z3. Я видел некоторые головоломки, решаемые z3, например, судоку и восемь ферзей. Мне просто интересно, решил ли кто-нибудь проблему пересечения реки в z3. z3 кажется очень хорошим решением проблем.
С Уважением
1389 просмотров
schedule
31.01.2023
ошибка z3py при преобразовании int в bitvec
From ( Z3: возможно ли суммировать BitVec и Real? ), я попытался преобразовать int в bitvec, используя
x = Int('x')
reg = BitVecRef(Z3_mk_int2bv(BitVecVal(x.ctx_ref(), 16, x)), x.ctx)
но я всегда получаю сообщение об ошибке: «Объект 'Ast' не...
721 просмотров
schedule
21.07.2022
Когда мне следует использовать функцию вместо переменной в Z3?
Я написал два решателя судоку в Z3, один раз с использованием 81 переменной, а другой с помощью функции, которая отображает координаты x и y в число в квадрате[x][y]. Я предполагаю, что вместо этого можно также использовать массив.
В чем разница...
130 просмотров
schedule
20.03.2023
Оптимизация тактики решателя для Circuit SAT
Я использую решатель Z3 с Python API для решения проблемы Circuit SAT . Он состоит из множества выражений Xor с 21 входом и выражений And с тремя входами. Z3 умеет решать мои маленькие примеры, но не справляется с большими.
Вместо...
323 просмотров
schedule
25.09.2022
Как получить список переменных из формулы z3?
У меня есть формула Z3 (в Z3py)
i=z3.Int('x')+z3.Int('y')<2
Как я могу получить список переменных x и y ?
677 просмотров
schedule
07.09.2022
Z3Py: Почему следующие предположения не выполняются?
Это может быть наивным вопросом, но почему следующее не приводит к удовлетворительному набору предположений?
Разве последнее предположение не следует непосредственно из предположений 2 и 3?
import z3
# Initialize variables
t = z3.Int('t')
z =...
76 просмотров
schedule
10.07.2022
Z3 Оптимизация, строгие неравенства
У меня проблема, о которой упоминалось ранее, и я не совсем понимаю решение (сочетание замены с упрощением). В моей кодировке у меня строгое неравенство, и мне нужно было бы установить эпсилон либо на 0, либо на очень маленькое значение. Например, у...
864 просмотров
schedule
23.02.2023
Z3 дает неожиданный UNSAT для всех формул
У меня есть фрагмент кода z3py ниже
I = Int('I')
x = Int('x')
a = Int('a')
O = Bool('O')
constraint1 = Implies(x==0,O)
constraint2 = Implies(And(x >= 6, O), x ==6)
test = And(constraint1,constraint2,(O == I <= a), I==x)
s = Solver()...
88 просмотров
schedule
01.10.2023
z3py: упростить вложенные хранилища с конкретными значениями
Я использую python API Z3 [версия 4.4.2 - 64 бит] и пытаюсь понять, почему z3 упрощает выражение в этом случае:
>>> a = Array('a', IntSort(), IntSort())
>>> a = Store(a, 0, 1)
>>> a = Store(a, 0, 3)
>>>...
64 просмотров
schedule
12.06.2023
Проблема при настройке параллельного Z3 с использованием z3 ‹smt2-file › CC_NUM_THREADS=3
Проблема при настройке параллельного Z3 с использованием z3 CC_NUM_THREADS=3
Я пытаюсь запустить параллельную версию z3 с CC_NUM_THREADS = 3 для моего файла smt2, появляется следующая ошибка.
ERROR: unknown parameter 'cc_num_threads'
Legal...
75 просмотров
schedule
26.07.2023
Z3Py: анализ выражений с использованием eval или z3.parse_smt2_string
Я пишу программу на Python, которая, помимо прочего, должна преобразовывать большие пропозициональные формулы в экземпляры z3. Например, формула f , которая может быть создана моей программой через
a = my_atomic_proposition("a") # Bool
b =...
1367 просмотров
schedule
27.06.2022
