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)