Z3实数理论中root-object是什么？QF_NRA返回root-obj相关疑问

示例代码回顾 #

你运行的求解代码如下：

(set-logic QF_NRA)
(declare-const x Real)
(assert (= 2 (* x x)))
(check-sat)
sat
(get-model)
(
  (define-fun x () Real
    (root-obj (+ (^ x 2) (- 2)) 1))
)

1. root-obj的含义 #

QF_NRA对应的是非线性实数算术逻辑，这类问题中很多多项式的根是无理数，无法用分数或有限小数精确表示，Z3就采用root-obj格式来存储精确的代数数解。
root-obj的标准格式为(root-obj <一元多项式> <根索引>)：

• 第一个参数是仅含一个变量的多项式
• 第二个参数是正整数，代表多项式从小到大排序后的第n个实根
  你示例中的多项式为x²-2，它的两个实根按升序排列为-√2、√2，索引为1对应的就是-√2，也就是此时x的精确值为-√2。

2. 未使用define-fun-rec的原因 #

这里不存在递归定义，只是变量名重名导致的误解：
root-obj内部用到的x是多项式的形参哑变量，和你最开始声明的顶层变量x属于完全不同的作用域，二者没有任何关联。你完全可以把root-obj里的变量替换成任意其他名字，比如(root-obj (+ (^ t 2) (- 2)) 1)，含义完全不变。
顶层的define-fun只是把x赋值为这个多项式的第1个实根，整个定义过程没有自引用，自然不需要使用递归专用的define-fun-rec关键字。 #

内容的提问来源于stack exchange，提问作者chansey