z3 - 使用数据类型为 : interaction or inlining 的 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)
)

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

使用“先内联，然后应用 qfnra-nlsat 的策略启动 Z3。我还没有找到这样做的方法，但也许我看起来不够好。

使用某些版本的 simplify 启动 Z3做内联。根据第一次调用的结果(内联版本)第二次启动 Z3。

换句话说，如何制作 qfnra-nlsat使用元组？

谢谢!

Answer 1

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

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

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