Как в Z3Py проверить, имеет ли уравнение для заданных ограничений только одно решение? Если решений несколько, как их перечислить?

Я создаю около 20 тысяч ограничений, и на моем компьютере их решение занимает около 3 минут. У меня разные ограничения, и ниже я привожу примеры и объясняю их. Я загрузил утверждения на http://filebin.ca/vKcV1gvuGG3 . Я заинтересован в решении...

Я использую z3py. У меня есть предикат над двумя целыми числами, которые необходимо оценить с использованием пользовательского алгоритма. Я пытался реализовать его, но без особого успеха. По-видимому, мне нужно процедурное вложение, которое сейчас...

Я пытаюсь решить ограничения с помощью решателя Z3 SMT в python. Ограничения включают как целые числа, так и битовые векторы. Я конвертирую BitVec в Int с помощью Z3_mk_bv2int. Я считаю, что следующие ограничения невыполнимы, но я получаю тест SAT...

Я заметил, что время проверки моих логических формул, написанных в z3py, сильно изменилось (с ~ 60 с до ~ 30 с, около 50%) после того, как я удалил «-» в именах переменных, которые я определил. E.g., vec = IntVector('vec-1',10) to vec...

Например, у меня есть ограничение x + y > 100 . Я не хочу, чтобы z3 давал мне значения x равными 1 или 2, и я не хочу, чтобы z3 давал значения y также равными 1 или 2. Итак, x и y могут быть любыми числами, кроме 1 или 2. Можем ли мы...

Я хочу найти максимальный интервал, в котором выражение e верно для всех x. Способ написания такой формулы должен быть: Exists d : ForAll x in (-d,d) . e and ForAll x not in (-d,d) . !e . Чтобы получить такое d , формула f в Z3 (если...

Я попытался реализовать функцию пола и потолка, как указано в следующей ссылке. https://math.stackexchange.com/questions/3619044/floor-or-ceiling-function-encoding-in-first-order-logic/3619320#3619320 Но запрос Z3 возвращает контрпример....

from z3 import * p = Int('p') q = Int('q') solve(Or(p==1,p==2,p==3), Or(q==1,q==2), Not(p==q), q==1) Дает мне [p = 2, q = 1] , но p может быть 2 или 3. Таким образом, ответ должен быть {2,3}. Как я могу сообщить z3 о нескольких ответах?