如何在 Microsoft Z3 中执行 sin cos 运算

Question

在Microsoft Z3 Dot Net API 中，没有执行 sin cos 操作的函数。当我在网上检查时，我发现可以通过将函数转换为笛卡尔坐标来计算 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(("值是什么？

Answer 1

我不确定这是否适用于所有可能的情况(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)))

(代数数(。