Как правильно использовать команду Solver() в Python API Z3 с объявленной функцией

Question

Я получаю неожиданные результаты с помощью какого-либо скрипта с использованием Python API Z3. Я думаю, что я неправильно понимаю какой-то процесс или просто неправильно использовал какую-то команду. Например, предположим, что у меня есть следующий сценарий:

from z3 import * 

x = Int('x') 

def g(x): 
    if x == 0: 
     return 1 
    elif x > 0: 
     return x**(x+1) 

s = Solver() 
s.add(g(x) > x) 
print s.check() 
if s.check()== sat: 
    m = s.model() 
    m.evaluate(x, model_completion=True) 
    print m 

Это будет возвращать следующий вывод:

sat 
[x = 0] 

что это нормально, но если я заменить s.add(g(x) > x) на s.add(x > 1, g(x) > x), это возвращает unsat. Я ожидал чего-то вроде:

sat 
[x = 2] 

Может кто-нибудь помочь мне понять, что происходит?

Answer 1

Python if-then-else не переводит в if-then-else Z3. Вы должны использовать функцию «If». См. Здесь: https://github.com/Z3Prover/z3/blob/master/src/api/python/z3.py#L1092

Answer 2

Моих навыков Python немного недоразвиты, но я думаю, что важна концепция, лежащая в основе этой проблемы заключается в том, что функции Python не переводят на функцию Z3, например, if x == 0: ... не создать функцию Z3, которая проверяет все возможные значения x. Самый простой способ проверить - просто распечатать решатель, чтобы он показывал вам ограничения, просто добавьте print s. В вашем неудовлетворительном случае я получаю [x > 1, x < 1], что действительно неудовлетворительно.