title: Z3 Theorem Prover: Pythagorean Theorem (Non-Linear Artithmetic)
body: <h2>Wherefore?</h2>
  
  <h3>The usecase context in which my problem occures</h3>
  
  <p>I define 3 random item of a triangle. Microsoft Z3 should output:</p>
  
  <ul>
  <li>Are the constraints satisfiabe or are there invalid input values?</li>
  <li>A model for all the other triangle items where all the variables are assigned to concrete values.</li>
  </ul>
  
  <p>In order to constrain the items i need to <strong><code>assert</code></strong> triangle equalities - i wanted to start out with the Pythagorean Theorem (<code>(h_c² + p² = b²) ^ (h_c² + q² = a²)</code>).</p>
  
  <h2>The Problem</h2>
  
  <p>I know that Microsoft Z3 has only limited capabilities to solve non-linear arithematic problems. But even some hand calculators are able to solve a very <em>simplified version</em> like this:</p>
  
  <pre><code>(set-option :print-success true)
  (set-option :produce-proofs true)
  (declare-const a Real)
  (declare-const b Real)
  (assert (= a 1.0))
  (assert (= b 1.0))
  (assert
      (exists
          ((c Real))
          (=
              (+
                  (* a a)
                  (* b b)
              )
              (* c c)
          )
      )
  )
  (check-sat)
  (get-model)
  </code></pre>
  
  <h2>The Question</h2>
  
  <ul>
  <li>Is there a way to get Microsoft Z3 to solve the Pythagorean Theorem if two values are given?</li>
  <li>Or: Is there another theorem prover which is able to handle these case of non-linear arithmetic?</li>
  </ul>
  
  <p>Thanks for your help concerning that - If anything is unclear, please comment.</p>