constraining the choice of models for uninterpreted functions in Z3
<p>I a nutshell, I want z3 to verify implications of the form 
<code>forall x1, x2, ..., xn. exists y1, ..., yn. P =&gt; Q</code>
My difficulty is that I need to obtain the definitions of <code>y1, ..., yn</code>  in terms of the variables <code>x1, ..., xn</code> that cause the implication to hold. </p>

<p>For example. Suppose I want to check: </p>

<p><code>forall x1, x2. exists y. (= x1 (f x2)) =&gt; (= x1 (f y))</code></p>

<p>I would like to understand that by setting <code>y</code> to <code>x2</code>, this implication holds. </p>

<p>For this concrete example, I'm trying to do this by asking z3 to give me a model for: </p>

<p><code>(declare-fun f (Int) Int)</code></p>

<p><code>(forall ((_x Int) (_y Int))(exists ((_b Int)) (=&gt; (= _x (f _y)) (= _x (f _b)))))</code></p>

<p>However, it is giving me models which instantiate f to 
functions that do not make sense in my case. For instance, functions that 
map all integers to 0. When I tried to constrain the choice of f by asserting that it is surjective, the solver just timed out. </p>

<p>I'm grateful for any help I can get :) </p>