CODEWITHSUNDEEP
z3
Myron King
Myron King

Reputation: 11

anonymous functions

I have found the support for anonymous functions (lambda expressions) in Yices to be extremely helpful. I am now trying to use Z3 to implement a tool, but I have not been able to figure out if this feature is supported. I am invoking the tool using the -smt2 flag. thanks for your help.

Upvotes: 1

Views: 255

Answers (1)

Malte Schwerhoff
Malte Schwerhoff

Reputation: 12852

AFAIK, lambda expressions are neither supported by Z3 (see this answer by Nikolaj Bjorner, one of the main Z3 developers), nor are they part of the SMTLib2 standard. Solvers that support lambda expressions, for example, Yices or veriT, support them as a custom extension to the SMTLib2 standard.

Depending on your needs (which you might want to illustrate by adding an example to your questions) you could try Z3 macros (define-fun), or a front-end like Z3Py that, compared with writing SMTLib code manually, simplifies working with Z3 a lot.

Upvotes: 2

Related Questions