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

z3

1зной

1ответ

Что такое «официальная» версия двигателя PDR в Z3?

Я тестировал двигатель PDR в Z3, и я не уверен, какую версию Z3 использовать. «Официальная» ветвь мастера из git, похоже, работает, но датирована ноябрем 2012 года. Я уверен, что с тех пор были улучше

3зной

1ответ

Удивляет поведение при попытке доказываем FORALL

Рассмотрим следующий SMT-LIB код: (set-option :auto_config false) (set-option :smt.mbqi false) ; (set-option :smt.case_split 3) (set-option :smt.qi.profile true) (declare-const x Int) (declare-

2зной

1ответ

Как закодировать фиксированное число истинных переменных?

Я говорю 10 булевых переменных. Я хочу, чтобы модель была выполнимой, если ровно 3 из них верны. Как я могу кодировать это как проблему SAT? Один из способов - создать все возможные комбинации, а зате

1зной

1ответ

Перегрузка оператора предиката оператора Z3 C++ не имеет неподписанной операции

Я смотрел документ класса expr из Z3 C++ API по следующей ссылке http://research.microsoft.com/en-us/um/redmond/projects/z3/classz3_1_1expr.html. Я нашел, что для оператора предиката, такого как «>»,

1зной

1ответ

Случайное семя для Z3 SAT Solver

Я использую Z3 как SAT solver для жесткой задачи выполнимости, закодированной в формате CNF/DIMACS. Будет ли иметь смысл рандомизации вход для того, чтобы увеличить шанс найти решение: перетасовать по

1зной

1ответ

Как определить перечисляемые типы в SMT-LIB для Z3

я ранее использовал API Z3 для определения перечисляемого типа как так let T = ctx.MkEnumSort("T", [| "a"; "b"; "c"|]) , который перечисляет элементы типа T как «а» «б» и «c» (и ничего больше). Одна

2зной

1ответ

Z3 - Как извлечь переменные из данной формулы?

Я использую Z3 C++ API (версия 4.3.1), и я хочу извлечь переменные формулы (объект типа expr). Я нашел similar question, но он находится в Z3py. Мне интересно, есть ли в Z3 C/C++ API метод для извлече