z3 — Могу ли я проверить, имеет ли переменная детерминированное значение с помощью API C ++
Я заметил, что Z3 может делать allsmt из какой-то бумаги. В моем проекте мне нужно искать детерминированные переменные в формуле SMT. Под детерминистическим я подразумеваю, что переменная может принимать только одно значение типа int, чтобы сделать формулу выполнимой. Существует ли функция API c ++ / c, которая может выполнить эту задачу?
Лучшее, что я могу сделать, — это вызывать функцию solver.check () много раз для отрицания каждой интересующей меня переменной. Есть ли более быстрый способ сделать это с помощью API?
По сути, я хочу сделать allsmt и предикат абстракции / проекции.
Решение
Не существует специализированного API для проверки, должны ли все модели данной переменной согласовывать одно и то же значение. Вы можете реализовать более или менее эффективные алгоритмы поверх Z3, чтобы решить этот вопрос.
Вот возможный алгоритм:
- Получить модель М от Z3.
- Для переменных, которые вас интересуют, утверждают: Not (And ([(M.eval (x) == x) для x в Vars]))
- Перепроверьте удовлетворенность. Если новое состояние неудовлетворительно, то остальные переменные в Vars должны иметь одинаковое значение. В противном случае удалите переменные из Vars, которые оценивают новое значение, отличное от старого M.eval (x), и повторяйте (2), пока Vars не станет пустым или контекст не будет неудовлетворительным.
Другие решения
Других решений пока нет …