Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>Z3 has a new solver (nlsat) for nonlinear arithmetic. It is more efficient than other solvers (<a href="http://research.microsoft.com/en-us/um/people/leonardo/files/IJCAR2012.pdf" rel="nofollow">see this article</a>). The new solver is complete for quantifier-free problems. However, the new solver does not support proof generation. If we disable proof generation, then Z3 will use nlsat and easily solve the problem. Based on your question, it seems you are really looking for solutions, thus disabling proof generation does not seem to be an issue.</p> <p>Moreover, Z3 does not produce approximate solutions (like hand calculators). It uses a precise representation for real algebraic numbers. We can also ask Z3 to display the result in decimal notation (option <code>:pp-decimal</code>). <a href="http://rise4fun.com/Z3/DkLv" rel="nofollow">Here is your example online</a>.</p> <p>In this example, when precise representation is used, Z3 will display the following result for <code>c</code>.</p> <pre><code>(root-obj (+ (^ x 2) (- 2)) 1) </code></pre> <p>It is saying that <code>c</code> is the first root of the polynomial <code>x^2 - 2</code>. When we use <code>(set-option :pp-decimal true)</code>, it will display</p> <pre><code>(- 1.4142135623?) </code></pre> <p>The question mark is used to indicate the result is truncated. Note that, the result is negative. However, it is indeed a solution for the problem you posted. Since, you are looking for triangles, you should assert that the constants are all > 0. </p> <p>BTW, you do not need the existential quantifier. We can simply use a constant <code>c</code>. Here is an example (also available <a href="http://rise4fun.com/Z3/gUO9" rel="nofollow">online at rise4fun</a>):</p> <pre><code>(set-option :pp-decimal true) (declare-const a Real) (declare-const b Real) (declare-const c Real) (assert (= a 1.0)) (assert (= b 1.0)) (assert (&gt; c 0)) (assert (= (+ (* a a) (* b b)) (* c c))) (check-sat) (get-model) </code></pre> <p>Here is another example that does not have a solution (also available <a href="http://rise4fun.com/Z3/9sldh" rel="nofollow">online at rise4fun</a>):</p> <pre><code>(set-option :pp-decimal true) (declare-const a Real) (declare-const b Real) (declare-const c Real) (assert (&gt; c 0)) (assert (&gt; a c)) (assert (= (+ (* a a) (* b b)) (* c c))) (check-sat) </code></pre> <p>BTW, you should consider the <a href="http://rise4fun.com/Z3Py/tutorial/guide" rel="nofollow">Python interface for Z3</a>. It is much more user friendly. The tutorial that I linked has examples in Kinematics. They also use nonlinear arithmetic to encode simple high-school physics problems. </p>
    singulars
    1. This table or related slice is empty.
    1. POZ3 Theorem Prover: Pythagorean Theorem (Non-Linear Artithmetic)
      singulars
      1. PTQuestion
    1. PTAnswer
    1. This table or related slice is empty.
    1. USLeonardo de Moura
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. POZ3 Theorem Prover: Pythagorean Theorem (Non-Linear Artithmetic)
      singulars
      1. PTQuestion
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    3. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTAcceptedByOriginator
    1. COI never wanted to express that hand calculators are able to do more things than Z3. I just wanted to reveal that it's a very simple usecase and that there just has to be a way to do that.
      singulars
      1. PO
      1. USfdj815
    2. COI understand. No problem. In my post, I tried to make the point that your example is not as simple as you think. Most SMT solvers cannot handle this problem, since they cannot even represent the solution precisely. Z3 without nlsat can't solve it. The hand calculator also does not really solve the problem, it just computes an approximated "solution". Suppose we also assert `(assert (= c 1.4142135623))`, is the problem still satisfiable? No, it is not. However, if we use approximations, we may incorrectly say it is. http://rise4fun.com/Z3/JWYC
      singulars
      1. PO
      1. USLeonardo de Moura
    3. COI took a look at Z3Py. - Looks nice and thanks.
      singulars
      1. PO
      1. USfdj815
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload