Z3含AugInt简单数据类型的查询超时问题解决问询

背景定义 #

以下是扩展整数类型AugInt的定义，包含正无穷（infty）、负无穷（ninfty）和普通整数，并重载了比较运算符<=：

(declare-datatypes ((AugInt 0)) (((infty) (ninfty) (integer (val Int)))))
(declare-fun <= (AugInt AugInt) Bool)
(declare-fun <= (AugInt Int) Bool)
(declare-fun <= (Int AugInt) Bool)
(assert (forall ((x AugInt) (y AugInt))
  (let ((a!1 (ite ((_ is (infty () AugInt)) y)
                  true
                  (ite ((_ is (ninfty () AugInt)) y) false (<= (val x) (val y))))))
    (= (<= x y)
       (ite ((_ is (infty () AugInt)) x)
            (= y infty)
            (ite ((_ is (ninfty () AugInt)) x) true a!1))))))
(assert (forall ((x AugInt) (y Int)) (= (<= x y) (<= x (integer y)))))
(assert (forall ((x Int) (y AugInt)) (= (<= x y) (<= (integer x) y))))

当前问题 #

• 可满足查询：能正常终止并返回有效模型，示例查询如下：

(declare-fun r1_B () AugInt)
(declare-fun l1_B () AugInt)
(assert (forall ((out Int) ($c0 Int) ($c2 Int) ($c4 Int))
  (let ((a!1 (or (= out 1)
                 (and (= out (+ $c0 $c2))
                      (<= l1_B $c0)
                      (<= $c0 r1_B)
                      (<= l1_B $c2)
                      (<= $c2 r1_B)))))
    (=> a!1 (and (<= l1_B out) (<= out r1_B))))))
(assert (and (<= ninfty l1_B)
     (<= r1_B infty)
     (or (not (= ninfty l1_B)) (not (= infty r1_B)))))

• 不可满足查询：会超时无法终止，示例查询如下：

(declare-fun r1_B () AugInt)
(declare-fun l1_B () AugInt)
(assert (forall ((out Int) ($c0 Int) ($c2 Int) ($c4 Int))
  (let ((a!1 (or (= out 1)
                 (and (= out (+ $c0 $c2))
                      (<= l1_B $c0)
                      (<= $c0 r1_B)
                      (<= l1_B $c2)
                      (<= $c2 r1_B)))))
    (=> a!1 (and (<= l1_B out) (<= out r1_B))))))
(assert (and (<= 1 l1_B)
     (<= r1_B infty)
     (or (not (= (integer 1) l1_B)) (not (= infty r1_B)))))

• 尝试启用新版量词引擎（sat.smt=true）后，不可满足查询可被证明，但可满足查询无法处理。

可行优化方案 #

1. 添加量词实例化模式 #

给全称量词指定实例化模式，引导Z3优先处理关键情况，避免无意义的全域实例化。修改后的断言如下：

(assert (forall ((out Int) ($c0 Int) ($c2 Int) ($c4 Int))
  :pattern ((= out 1) (= out (+ $c0 $c2)))
  (let ((a!1 (or (= out 1)
                 (and (= out (+ $c0 $c2))
                      (<= l1_B $c0)
                      (<= $c0 r1_B)
                      (<= l1_B $c2)
                      (<= $c2 r1_B)))))
    (=> a!1 (and (<= l1_B out) (<= out r1_B))))))

模式指定Z3优先实例化out=1或out=+$c0 $c2的情况，大幅减少搜索空间。

2. 拆分复杂全称断言 #

将原有的复合断言拆分为两个独立的全称量词，每个对应一种out的情况，简化推理逻辑：

; 单独处理out=1的约束
(assert (forall ((out Int))
  :pattern ((= out 1))
  (=> (= out 1) (and (<= l1_B out) (<= out r1_B)))))

; 单独处理out=$c0+$c2的约束
(assert (forall ((out Int) ($c0 Int) ($c2 Int))
  :pattern ((= out (+ $c0 $c2)))
  (=> (and (= out (+ $c0 $c2))
           (<= l1_B $c0)
           (<= $c0 r1_B)
           (<= l1_B $c2)
           (<= $c2 r1_B))
      (and (<= l1_B out) (<= out r1_B)))))

拆分后每个量词的逻辑更简单，Z3的实例化策略能更精准触发，避免组合爆炸。

3. 调整量词实例化选项 #

保留默认量词引擎，调整实例化相关选项平衡处理效率，示例配置：

(set-option :smt.qi.eager_threshold 100)
(set-option :smt.qi.max_multi_patterns 5)

• smt.qi.eager_threshold：控制 eager 实例化的阈值，避免过早触发大量实例化
• smt.qi.max_multi_patterns：限制多模式实例化的数量，减少冗余计算

4. 简化AugInt比较逻辑 #

将AugInt的<=定义改为扁平化结构，减少嵌套ite带来的推理复杂度：

(declare-datatypes ((AugInt 0)) (((infty) (ninfty) (integer (val Int)))))

; 定义AugInt间的<=关系
(assert (forall ((x AugInt) (y AugInt))
  (or (is ninfty x)
      (is infty y)
      (and (is integer x) (is integer y) (<= (val x) (val y)))
      (and (is integer x) (is ninfty y) false)
      (and (is infty x) (is integer y) (= y infty)))))

; 重载与Int的比较
(assert (forall ((x AugInt) (y Int)) (= (<= x y) (<= x (integer y)))))
(assert (forall ((x Int) (y AugInt)) (= (<= x y) (<= (integer x) y))))

扁平化的定义让Z3更容易解析比较约束，提升推理速度。

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