CODEWITHSUNDEEP
z3
Maximiliano Cristia
Maximiliano Cristia

Reputation: 61

How to declare a record such that one of its fields is a function

I'm very new to Z3, so sorry for asking something silly.

I'm trying to define a record such that some of its fields are functions. I tried this:

(declare-datatypes (DOM RAN) ((PFun (mk-pfun (dom (DOM) Bool) (law (DOM) RAN)))))

with the intention that dom and ran are two fields whose type is a function (dom a function from DOM to Bool, and law a function from DOM to RAN). I tried also by enclosing the function type in parenthesis:

(declare-datatypes (DOM RAN) ((PFun (mk-pfun (dom ((DOM) Bool)) (law ((DOM) RAN))))))

bun none of these work.

I searched the tutorial but there are no examples of this.

Can you help me?

Thanks in advance for your answer.

All the best, Maxi

Upvotes: 2

Views: 187

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

Z3 is based on first-order logic. So, functions cannot be arguments of datatype constructors or other functions. That being said, you can “simulate” high-order features using arrays. You can write your datatype as

  (declare-datatypes (DOM RAN) ((PFun (mk-pfun (dom (Array DOM Bool)) 
                                               (law (Array DOM RAN))))))

Let p be a PFun and d a constant of sort DOM, then you write (select (dom p) d) to obtain dom(p)(d), and (select (law p) d) to obtain law(p)(d).

Upvotes: 1

Related Questions