CODEWITHSUNDEEP
pythonz3smtz3pyz3-fixedpoint
user2408329
user2408329

Reputation: 75

Array as a parameter to a relation in z3 fixedpoint solver

I am using array as a parameter to a relation in z3 fixedpoint solver. I am trying to get array value in the certificate which satisfies my query. When I run this on z3 it throws an error stating Uninterpreted 'a1' in A(#1,#0,#3).

Why is array being treated as uninterpreted? Does this imply uninterpreted functions cannot be used as arguments to a relation in fixedpoint solver? 

(declare-rel A (Int Int (Array Int Int)))
(declare-rel q1 (Int Int  (Array Int Int)))
(declare-const a1 (Array Int Int))
(declare-var a Int) 
(declare-var b Int)
(declare-var i Int)

(rule (=> (A (+ a 1) b (store a1 i 2)) (A a b a1)))

(rule (=> (= a b) (A a b a1)))

(rule (=> (and (A a b a1) (= a 0) (= b 1)) (q1 a b  a1)))

(query q1 :print-certificate true)

Upvotes: 2

Views: 203

Answers (0)

Related Questions