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

Question

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

set_option('model_evaluator.completion', True) 
set_option('smt.auto-config', False) 
set_option('auto-config', False) 

Что я должен сделать, чтобы получить конкретные значения этих переменных?

Answer 1

Опция auto-config не указывает Z3 печатать или опускать детали моделей; он просто включает или отключает автоматическую настройку решателя (на основе статических функций формулы).

Если переменной не присвоено значение в модели, это просто не имеет значения, то есть вы можете составить любое значение для него, и оно по-прежнему будет правильной моделью. В зависимости от того, какие решатели/тактика вы используете, опция model_evaluator.completion может решить эту проблему, но самый безопасный способ - включить завершение модели во время оценки модели, то есть использовать функцию eval(..) с model_completion=True