z3

2зной

1ответ

(применить qe) не устраняет сразу все кванторы?

Я прошу Z3 сделать исключение квантификатора в теории UFLIA, используя интерфейс SMTLIB 2. Поэтому я утверждаю формулу с 21 экзистенциально квантифицированными переменными, из них семь являются целыми

z3 quantifiers 2013-08-26

---

5зной

1ответ

Интерпретация статистики Z3

Я получил несколько статистических данных из пробегов Z3. Мне нужно понять, что это значит. Я довольно ржавый и не в курсе последних событий, связанных с решением сит и SMT, поэтому я попытался найти

z3 smt usage-statistics sat-solvers 2013-08-28

---

0зной

1ответ

Невозможно установить параметр pdr_use_farkas в Z3py

Когда я пытаюсь установить механизм фиксированной точки в PDR, и я пытаюсь установить параметр pdr_use_farkas, я получаю сообщение об ошибке unknown_parameter. В частности, я использую следующие парам

python z3 fixed-point z3py 2013-09-06

---

0зной

1ответ

z3 имеет неразрешенные символы на Ubuntu 12.04 x86

Z3 с http://research.microsoft.com/projects/z3/z3-3.2.tar.gz на Ubuntu 12.04 x86, похоже, имеют неразрешенные символы. Запуск простого приложения, которое использует Z3 привязки результатов в: ./app:

ubuntu compilation symbols z3 2013-09-06

---

0зной

1ответ

стратегия Z3 для решения системы с условными целочисленных дополнений

Я использую Z3, чтобы решить систему, состоящую из булевых ограничений на переменные Vi, а также ограничение следующего вида: L < If(V0, T0, F0) + If(V1, T1, F1) + ... + If(Vn, Tn, Fn) <= H где L, H

z3 2013-09-09

---

4зной

1ответ

Z3: Предложение случайных решений в решении

Я попытался следующий код в http://rise4fun.com/z3/tutorial (declare-const a Int) (assert (> a 100)) (check-sat) (get-model) результат всегда a=101. Мне нужна некоторая случайность в ответе, что

z3 2013-09-12

---