CODEWITHSUNDEEP
pythonarraysz3z3py
anticlockwise
anticlockwise

Reputation: 13

Z3py - function k!0 generated when solving constraints on Array variables

During our research activity, we are investigating Arrays in z3py (Python API for Z3 v4.4.2).
We were wondering why z3 provides as a result more Array functions than asked. For example, here k!0 pops out:

>>> A = Array('A', IntSort(), IntSort())
>>> solve(A[0] == 0)
[A = [0 -> 0, else -> 0], k!0 = [0 -> 0, else -> 0]]

It seems like z3 uses k!0 as an auxiliary function, but we did'nt find anything in the documentation.
Is there any reference about this?

Upvotes: 1

Views: 152

Answers (1)

shhyou
shhyou

Reputation: 332

Z3 creates a function k!0 from Int (array index) to values and cast it into an array. Though it is not printed in the Python binding, this can be seen from Z3 REPL.

This is briefly described in the Array models subsection http://rise4fun.com/Z3/tutorialcontent/guide#h26.

(declare-const a1 (Array Int Int))
(assert (= (select a1 0) 0))
(check-sat)
;=> sat

(get-model)
;=> (model 
;     (define-fun a1 () (Array Int Int)
;       (_ as-array k!0))
;     (define-fun k!0 ((x!0 Int)) Int
;       (ite (= x!0 0) 0
;         0))
;   )

Upvotes: 2

Related Questions