z3 - 如何在微软 Z3 中进行正余弦运算

在 Microsoft Z3 Dot Net API 中，没有执行正余弦运算的功能。上网查了一下，发现sin和cos函数值可以通过将函数转换为笛卡尔坐标来计算。

例如:

if x = cos(theta) and y = sin(theta)
x^2 + y^2 = 1

使用这个逻辑，我们可以为 sin cos 函数生成值。

我可以生成以下代码:

(set-info :status sat)

(set-option :pp.decimal true)
(set-option :model_validate false)

(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun theta () Real)

(assert (= (cos theta) x))
(assert (= (sin theta) y))
(assert (= (+ (* x x) (* y y)) 1))
(check-sat-using qfnra-nlsat)
(get-model)
(reset)

我现在得到的输出是这样的:

sat
(model
  (define-fun x () Real
    0.125)
  (define-fun y () Real
    (- 0.9921567416?))
  (define-fun theta () Real
    (+ (acos (- 0.125)) pi))
)

我不清楚的是，如何获得 Z3 中给定 theta 的 sin(theta) 或 cos(theta) 值？谁能帮我制作smt代码？

我在结果中得到的“(+ (acos (- 0.125)) pi))”值是多少？

最佳答案

我不确定这是否适用于所有可能的情况(nlsat 有点特殊)，但是您可以使用 get-value 来获取模型下评估的任意表达式，例如，在 (check-sat-using ...) 之后，您可以添加

(get-value (theta))
(get-value ((sin theta)))

要得到

((theta (+ (acos (- 0.125)) pi)))
(((sin theta) (- 0.9921567416?)))

注意 ? 表示该值已被截断；有调整精度的选项。例如，没有 pp.decimal=true ，精确的结果报告为

(((sin theta) (root-obj (+ (* 64 (^ x 2)) (- 63)) 1)))

(一个代数数)。

关于z3 - 如何在微软 Z3 中进行正余弦运算，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/48530851/