Пустая модель в z3

z3py snippet:

x = Int('x') s = Solver() s.add(x <= x) print s.check() print s.model() print s.model().sexpr() 

http://rise4fun.com/Z3Py/mfPU

Вывод:

 sat [] 

Любое значение x будет делать, но z3 возвращает пустую модель. Имеет ли отсутствующая свободная переменная x в модели, указывает, что любое целочисленное значение является допустимой моделью?

Да, в Z3, если константа (такая как x ) не появляется в модели, то это «не заботится». То есть любое значение x удовлетворяет формуле. При оценке значения константы мы можем включить «завершение модели». То есть Z3 будет использовать произвольную интерпретацию для символов «не заботясь». Вот пример http://rise4fun.com/Z3Py/bvVO

 x = Int('x') s = Solver() s.add(x <= x) print s.check() m = s.model() print m.evaluate(x) print m.evaluate(x, model_completion=True) print m