Могу ли я проверить, имеет ли переменная детерминированное значение C++ API

Question

Я заметил, что Z3 может делать allsmt с некоторой бумаги. В моем проекте я должен искать детерминированные переменные в формуле SMT. По детерминированному я имею в виду, что переменная может принимать только одно значение int, чтобы сделать формулу выполнимой. Есть ли функция C++/c API, которая может выполнять эту задачу?

Лучшее, что я могу сделать до сих пор, - это многократно вызвать функцию solver.check() для отрицания каждой переменной, которой меня интересует. Есть ли более быстрый способ сделать это с помощью API?

В принципе, я хочу сделать allsmt и предикат абстракции/проекции.

Answer 1

Не существует специализированного API для проверки того, должны ли все модели данной переменной согласовываться с одним и тем же значением. Вы можете реализовать более или менее эффективные алгоритмы поверх Z3 для решения этого вопроса. Вот возможный алгоритм:

1. Получите модель M от Z3.
2. Для переменных, которые вас интересуют assert: Not (And ([(M.eval (x) == x) для x в Vars]))
3. Отметить выполнимость. Если новое состояние является неудовлетворительным, то оставшиеся variales в Vars должны иметь одинаковое значение. В противном случае удалите переменные из Vars, которые оценивают новое значение, отличное от старого M.eval (x), и повторяют (2), пока Vars не будет пуст или контекст будет неудовлетворителен.