因此？
在我的问题occures的用例情境
我定义一个三角形的3个随机项。 微软Z3应该输出：
- 是限制satisfiabe还是有无效的输入值？
- 模型的所有，所有的变量被分配到具体值其它三角项目。
为了约束我需要的物品assert三角平等-我想与勾股定理开始了（ (h_c² + p² = b²) ^ (h_c² + q² = a²)
问题
我知道，微软Z3只有有限的能力来解决非线性arithematic问题。 但是，即使一些手计算器能够解决一个非常简单的版本是这样的：
(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)
问题
- 有没有办法让微软Z3解决勾股定理如果给出两个值？
- 或者：难道还有其他的定理证明其能够处理非线性算法的这些情况？
感谢您的帮助是有关 - 如果有不清楚的地方，请评论。
Z3 has a new solver (nlsat) for nonlinear arithmetic. It is more efficient than other solvers (see this article). 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.
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 :pp-decimal).
Here is your example online.
In this example, when precise representation is used, Z3 will display the following result for c.
(root-obj (+ (^ x 2) (- 2)) 1)
It is saying that c is the first root of the polynomial x^2 - 2.
When we use (set-option :pp-decimal true), it will display
(- 1.4142135623?)
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.
BTW, you do not need the existential quantifier. We can simply use a constant c.
Here is an example (also available online at rise4fun):
(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 (> c 0))
(assert (= (+ (* a a) (* b b)) (* c c)))
(check-sat)
(get-model)
Here is another example that does not have a solution (also available online at rise4fun):
(set-option :pp-decimal true)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)
(assert (> c 0))
(assert (> a c))
(assert (= (+ (* a a) (* b b)) (* c c)))
(check-sat)
BTW, you should consider the Python interface for Z3. 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.
