User-defined function doesn't agree with functions in printed models

[Halbaroth]

If we define a function in the input file, the model should print exactly the same function. For instance the input file:

(set-logic ALL)
(set-option :produce-models true)
(declare-fun f (Int) Int)
(assert (forall ((x Int) (y Int)) (= (f (+ x y)) (+ (f x) (f y)))))
(assert (= (f 0) 0))
(define-fun g () Bool (= (f 1) 1))
(check-sat-assuming (g))
(get-model)

produces the model:

unknown
(

 ; Functions

(define-fun f ((arg_0 Int)) Int (ite (= arg_0 1) 1 0))

 ; Constants

(define-fun g () Bool true)

 ; Arrays not yet supported

)

The value for f is correct but AE gives a new definition for g.

I think Steven reported this bug, but didn't create an issue for it.

[Gbury]

Actually in that case, we shouldn't print anything for 'g' : it's not a declared constant that needs a value; it is defined therefore its value is decided based on the values of the model.

[Halbaroth]

You mean that we shouldn't do so according to the SMTLIB standard?

[bclement-ocp]

Yes, functions that are defined but not declared should not be printed. I guess that's part of #706 technically but also not really (that one is actually about printing values, not terms, as definitions in the models).

The first step would be to understand how we can determine whether a function is defined or declared, I think that we lose that information fairly early (maybe during typechecking?).