z3

0зной

1ответ

Найти логические условия для эквивалентности двух формул?

Я разместил related question, но тогда я думаю, что это было не очень ясно. Я хотел бы перефразировать проблему следующим образом: Две формулы a1 == a + b (1) и a1 == b (2) эквивалентны, если a == 0.

z3 z3py 2013-06-14

---

1зной

1ответ

PROOF_MODE влияет на результат проверки

Мы пытаемся использовать z3 для создания доказательств через C API (через ScalaZ3). , мы тем самым обеспечиваем создание доказательств, устанавливая PROOF = true. Это, однако, влияет на результат друг

z3 2013-06-17

---

0зной

2ответ

Как решить пример лжецов/говорящих правду, используя Z3Py и Z3 SMT-LIB

Пример Проблема: Предположим, что лжецы всегда говорят, что это ложь, и правда-кассиры всегда говорят, что это правда. Предположим, что Эми, Боб, Кэл, Дэн, Эрни и Фрэнсис - либо лжец, либо правдист. A

z3 z3py 2013-06-17

---

0зной

1ответ

Извлечь границы узла извлечения в z3py

Я использую z3py. Мой вопрос в том, как получить границы узла Extract? Я думал, что Extract будет функция арностью три, но это не так: >>> x = BitVecVal(3, 32) >>> e = Extract(15, 0, x) >>> e.decl()

z3 z3py 2013-06-18

---

0зной

1ответ

Z3Python: ForAll вызывает зависание моего кода или возвращает Unsat, почему?

Я все еще борюсь с проблемой findiong a так, чтобы a * b == b со всем значением b. Ожидаемый результат: a == 1. У меня есть два решения ниже. (A) Я реализовал это с помощью квантора ForAll в нижнем ко

z3 z3py 2013-06-19

---