How to get function interpretation as a single expression from the model?

[skmuduli92]

I am using HORN logic in Z3 to solve the following constraints using C++ API.

(set-logic HORN)
(declare-fun Inv ( Int Int Int Int) Bool)

(assert (forall ( (A Int) (B Int) (C Int) (D Int))
		(=> (and (> B 0) (= C A) (= D 0)) (Inv A B C D)) ))

(assert (forall ( (A Int) (B Int) (C Int) (D Int) (C1 Int) (D1 Int) )
		(=> (and (Inv A B C D) (< D B) (= C1 (+ C 1)) (= D1 (+ D 1)))   (Inv A B C1 D1) )  ))

(assert (forall ( (A Int) (B Int) (C Int) (D Int))
		(=> (and (Inv A B C D) (>= D B) )   (= C ( + A B) ) )))

(check-sat)
(get-model)

The above constraints are satisfiable and gives a model for the function (uninterpreted predicate) Inv. I want to get the interpretation from the model and translate it into another language say C/C++ function.

I could see in the func_interp class definition given in Z3++.h, where I could use the entry() and else_value() to traverse the function interpretation. But is there any way in Z3 where I could get the function interpretation as a single expression?

If there is no such method then how do I use the entry() and else_value() functions construct a single expression using ITEs?

[NikolajBjorner]

from z3 import *

file = """
(set-logic HORN)
(declare-fun Inv ( Int Int Int Int) Bool)

(assert (forall ( (A Int) (B Int) (C Int) (D Int))
		(=> (and (> B 0) (= C A) (= D 0)) (Inv A B C D)) ))

(assert (forall ( (A Int) (B Int) (C Int) (D Int) (C1 Int) (D1 Int) )
		(=> (and (Inv A B C D) (< D B) (= C1 (+ C 1)) (= D1 (+ D 1)))   (Inv A B C1 D1) )  ))

(assert (forall ( (A Int) (B Int) (C Int) (D Int))
		(=> (and (Inv A B C D) (>= D B) )   (= C ( + A B) ) )))

(check-sat)
(get-model)"""


s = SolverFor("HORN")
s.from_string(file)
print(s.check())
Inv = Function("Inv", IntSort(), IntSort(), IntSort(), IntSort(), BoolSort())
m = s.model()
print(m[Inv])

The model has methods that let you access the interpretation of functions.
Above is an example using python. Internally it uses Z3_model_get_func_interp