Microsoft Z3中如何进行sin cos运算答案

【问题标题】：How to perform sin cos operation in Microsoft Z3Microsoft Z3中如何进行sin cos运算
【发布时间】：2018-01-30 21:31:58
【问题描述】：

在 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))”值是多少？

【问题讨论】：

标签： z3 smt

【解决方案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)))

（一个代数）。

【讨论】：