对数据类型使用 Z3 QFNRA 策略：交互或内联

Question

在Non-linear arithmetic and uninterpreted functions 中，Leonardo de Moura 表示qfnra-nlsat 策略尚未与 Z3 的其余部分完全集成。我以为两年来情况有所改变，但显然整合还不是很完整。

在下面的示例中，我将数据类型纯粹用于“软件工程”目的：将我的数据组织成记录。即使没有未解释的函数，Z3 仍然无法给我一个解决方案：

(declare-datatypes () (
    (Point (point (point-x Real) (point-y Real)))
    (Line (line (line-a Real) (line-b Real) (line-c Real)))))

(define-fun point-line-subst ((p Point) (l Line)) Real
    (+ (* (line-a l) (point-x p)) (* (line-b l) (point-y p)) (line-c l)))

(declare-const p Point)
(declare-const l Line)

(assert (> (point-y p) 20.0))
(assert (= 0.0 (point-line-subst p l)))

(check-sat-using qfnra-nlsat)
(get-model)

---

> unknown
(model 
)

但是，如果我手动内联所有函数，Z3 会立即找到模型：

(declare-const x Real)
(declare-const y Real)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)

(assert (> y 20.0))
(assert (= 0.0 (+ (* a x) (* b y) c)))

(check-sat-using qfnra-nlsat)
(get-model)

---

> sat
(model 
  (define-fun y () Real
    21.0)
  (define-fun a () Real
    0.0)
  (define-fun x () Real
    0.0)
  (define-fun b () Real
    0.0)
  (define-fun c () Real
    0.0)
)

我的问题是，有没有办法自动执行这种内联？我对以下任一工作流程都满意：

1. 使用“先内联，然后应用 qfnra-nlsat”的策略启动 Z3。我还没有找到这样做的方法，但也许我看起来不够好。
2. 使用simplify 的某些版本启动Z3 进行内联。在第一次调用的结果（内联版本）上第二次启动 Z3。

换句话说，如何让qfnra-nlsat 与元组一起工作？

谢谢！

Answer 1

没错，NLSAT 求解器仍未与其他理论集成。目前，只有在运行它之前消除所有数据类型（或其他理论的元素），我们才能使用它。我相信目前 Z3 内部没有有用的现有策略，所以这必须提前完成。一般来说，制定战术并不难，例如，像这样：

(check-sat-using (and-then simplify qfnra-nlsat))

但简化器不够强大，无法消除此问题中的数据类型常量。 （各自的实现文件是datatype_rewriter.cpp和datatype_simplifier_plugin.cpp。）