z3 - Отличная библиотека

z3

1зной

1ответ

Простой Z3 упражнения возвращения неизвестно

Я начинаю с помощью SMT решателей, и я практиковал с этой простой задачей: Exercise 5. Using Z3 at the restaurant: (a) Encode the following menu choices into Z3 and determine what a customer could bu

4зной

1ответ

Как представить константу с плавающей запятой (например, 1e307) в стандарте SMT-LIB?

В настоящее время я делаю некоторые эксперименты на Z3, и я понятия не имею, для представления чисел с плавающей точкой постоянной буквальным (например, 1e307) в SMT: (declare-const a Real) (assert (

0зной

1ответ

Изменения кода для сборки z3 на Solaris

Мне нужно получить z3-здание на Solaris 8. Я взглянул на файл scoped_timer.cpp, который является единственным местом, где используется -D_LINUX_, и рисую. Я могу получить правильный код там для Solari

1зной

2ответ

Как правильно использовать команду Solver() в Python API Z3 с объявленной функцией

Я получаю неожиданные результаты с помощью какого-либо скрипта с использованием Python API Z3. Я думаю, что я неправильно понимаю какой-то процесс или просто неправильно использовал какую-то команду.

0зной

1ответ

SIGBUS crash on Solaris 8

Скомпилирован с g ++ 4.7.4 на Solaris 8. 32-разрядное приложение. Стек след Core was generated by `./z3'. Program terminated with signal 10, Bus error. \#0 0x012656ec in vector<unsigned long long

-1зной

1ответ

Как установить шаблон в переменной с помощью Z3Py

Я довольно новичок в Z3, но это проблема, с которой моя проблема может быть решена. У меня есть две переменные А и В и два шаблона так: pattern_1: 1010x11x pattern_2: x0x01111 , где 1 и 0 являются бит

3зной

1ответ

Почему Z3 не может решить этот вопрос без кажущейся тривиальной модификации?

Исходная задача: (declare-const a Real) (declare-const b Bool) (declare-const c Int) (assert (distinct a 0.)) (assert (= b (distinct (* a a) 0.))) (assert (= c (ite b 1 0))) (assert (not (di

0зной

1ответ

Показать все значения из модели Z3 (Python)

Когда я хочу получить значения всех переменных в экземпляре SMT2, я использую команду (set-option :auto-config false). В Z3py установка этого параметра не работает - модель не отображает переменные, к

0зной

1ответ

Функция возвращает отрицательное значение на основе параметра (Z3, Python)

Я эмулирую массив с простой функцией (Tab), и он не работает должным образом. Если я его код в SMT2, он работает хорошо, но в Z3py это не работает. from z3 import * A = BitVec('A', 8) B1 = BitVec('

1зной

1ответ

Почему этот нелинейный экземпляр не может быть решен решателем QF_NRA, но может быть решен решателем по умолчанию?

Может быть решен следующий экземпляр SMT2 (это UNSAT), но если я использую решатель qfnra, результат неизвестен. (declare-fun NONDET_INT_32_1() Int) (declare-fun lv_n_1_1() Int) (declare-fun lv_n_8_