z3 - 在有界上下文中对数组进行量化

Question

在有界上下文（即所有基本排序都是位向量）中，我们将（2-dim）集合建模为数组。在某些公理中，我们需要对这个数组进行量化。一旦我们包含了这样的公理，求解器就会返回未知数。从句法的角度来看，这种量词超出了 的范围FOL，但我们期望求解器能够识别/使用有界上下文信息。

1. 为什么求解器不使用有界上下文信息？
2. 有没有可能在没有手动量词爆破的情况下将这个教给求解器？

这是一个最小的例子：

(define-sort Any () (_ BitVec 6))
(define-sort Object () (_ BitVec 3))
(define-sort Field () (_ BitVec 2))

(define-sort Heap () (Array Object Field Any))
(define-sort LocSet () (Array Object Field Bool))

(declare-fun foo (Heap LocSet Heap) Heap)
(assert
 (forall 
  ((?h Heap) (?s LocSet) (?h2 Heap) (?o Object) (?f Field))
  (= (select (foo ?h ?s ?h2) ?o ?f)
     (select (ite (select ?s ?o ?f) ?h ?h2) ?o ?f))))

(check-sat)