Оценить выражение Z3

Question

У меня есть ограничение в Z3py, скажем,

z3.Real('x')<=3 

Есть простой, встроенный способ оценить ограничение, «истина» или «ложь» для потенциальной модели? Например, для оценки ограничения с z3.Real('x')->2 следует указать «true».

Answer 1

Вы можете либо оценить выражения под моделью, которые могут быть извлечены, когда Solver.check возвращает sat (получить модель с помощью Solver.model()), или вы можете представить свою собственную модель в качестве замены (когда только модель упоминает константы), а затем замените значения из модели на выражение, используя метод «substitute», а затем используйте «упростить» для оценки полученного выражения.