Ошибка с рекурсивными функциями?

Question

Я пытаюсь рекурсивные функции в z3, и мне любопытно, есть ли ошибка с построением модели. Рассмотрим:

(define-fun-rec f ((x Int)) Int 
        (ite (> x 1) 
         (f (- x 1)) 
         1)) 
(check-sat) 
(get-value ((f 0))) 

Здесь f фактически постоянная функция 1, только что определили в глупо. Для этого входа, z3 печатает:

sat 
(((f 0) 0)) 

Это кажется неправильным, так как f 0 должна равняться 1.

Что интересно, если я утверждаю, что z3 предлагает в качестве результата, то я получаю правильный unsat ответ:

(define-fun-rec f ((x Int)) Int 
        (ite (> x 1) 
         (f (- x 1)) 
         1)) 
(assert (= (f 0) 0)) 
(check-sat) 

я получаю:

unsat 

Так, похоже, z3 на самом деле делает теперь f 0 не может быть 0; даже несмотря на то, что в предыдущем случае эта модель была произведена очень хорошо.

Принимая это один шаг дальше, если я выдаю:

(define-fun-rec f ((x Int)) Int 
        (ite (> x 1) 
         (f (- x 1)) 
         1)) 
(assert (= (f 0) 1)) 
(check-sat) 
(get-model) 

Тогда z3 отвечает:

sat 
(model 
    (define-fun f ((x!0 Int)) Int 
    1) 
) 

который действительно разумный ответ.

Итак, возможно, есть ошибка с рекурсивными функциями при определенных условиях?

Answer 1

Используемые модели не отражают график рекурсивных определений функций. Таким образом, при оценке рекурсивных функций по значениям, которые не были видны во время решения, это может привести к произвольным результатам. Это поведение теперь изменяется, поскольку рекурсивные определения включены в модели.