title: Simplify function interpretation in model
body: <p>In <a href="https://stackoverflow.com/questions/37472357/smt-check-uniqueness-and-totality-of-function">SMT: check uniqueness and totality of function</a> I gave a function axiomatization and asked Z3 for a model.  However because solving something with quantifiers in it is undecidable in general, Z3 times out.</p>
  
  <p>Here is a modified version in which the "int" case is modelled as a single value:</p>
  
  <pre><code>(declare-datatypes () ((ABC int error none)))
  (declare-fun f (ABC ABC) ABC)
  (assert (forall ((x ABC)) (=&gt; (or (= x int) (= x error) (= x none)) (= (f none x) none))))
  (assert (forall ((x ABC)) (=&gt; (or (= x int) (= x error) (= x none)) (= (f x none) none))))
  (assert (forall ((x ABC)) (=&gt; (or (= x int) (= x error)) (= (f error x) error))))
  (assert (forall ((x ABC)) (=&gt; (or (= x int) (= x error)) (= (f x error) error))))
  (assert (forall ((x ABC) (y ABC)) (=&gt; (and (= x int) (= y int)) (= (f x y) int))))
  (check-sat)
  (get-model)
  </code></pre>
  
  <p>Because there now are finitely many cases, Z3 gives an answer quickly:</p>
  
  <pre><code>sat
  (model
    (define-fun k!26 ((x!0 ABC)) ABC
      (ite (= x!0 error) error
      (ite (= x!0 int) int
        none)))
    (define-fun f!28 ((x!0 ABC) (x!1 ABC)) ABC
      (ite (and (= x!0 error) (= x!1 int)) error
      (ite (and (= x!0 int) (= x!1 error)) error
      (ite (and (= x!0 error) (= x!1 error)) error
      (ite (and (= x!0 int) (= x!1 int)) int
        none)))))
    (define-fun k!27 ((x!0 ABC)) ABC
      (ite (= x!0 error) error
      (ite (= x!0 int) int
        none)))
    (define-fun f ((x!0 ABC) (x!1 ABC)) ABC
      (f!28 (k!27 x!0) (k!26 x!1)))
  )
  </code></pre>
  
  <p>Both <code>k!26</code> and <code>k!27</code> actually just return their input (this is easily seen by checking all three cases).  Is it possible to simplify the model by eliminating these two functions automatically?</p>
  
  <p>Optimally I would like to have something like the following, although I see that might not be possible:</p>
  
  <pre><code>(define-fun f ((x!0 ABC) (x!1 ABC)) ABC
    (ite (or (= x!0 none) (= x!1 none)) none
    (ite (or (= x!0 error) (= x!1 error)) error
      int)))
  </code></pre>
  
  <p>I'm using Z3Py, but both general Z3-specific and Z3Py-specific answers are welcome.</p>