Z3 4.8.10

[jad-hamza]

I removed getAbsFunDecl (and the corresponding test suite) which crashes because the AST kind is Z3UnknownAST. Is that ok?

[samarion]

No, we need the absolute value fundecl it in Inox for the multiset encoding. Maybe it can be accessed differently though?

[jad-hamza]

Oh I somehow missed that call in Z3Native.scala. Can't we make a lambda here?

https://github.com/epfl-lara/inox/blob/c37411dc0c693142f9bff1a68e617d4bfb5be277/src/main/scala/inox/solvers/z3/Z3Native.scala#L449-L458

[samarion]

What do you mean by a "lambda"? Inox-level lambdas aren't available anymore at that point, we're directly communicating with the SMT solver here.

It might be possible to construct an abs function declaration though. I don't remember exactly how the Z3 API works, but I think we can construct simple non-recursive functions somehow and they might work in the SMT array map.

[samarion]

This API might work:

ScalaZ3/src/main/scala/z3/scala/Z3Context.scala

Line 471 in 73cec66

def mkArrayMap(f: Z3FuncDecl, args: Z3AST*): Z3AST = {

[jad-hamza]

Aren't there lambdas in Z3 now?
https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-quantifiers-and-lambda-binding

[samarion]

I would be worried they'll lead to quantifiers under the hood

[mario-bucev]

#80 should address the problem with getAbsFunDecl