search

epfl-lara / ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver
Apache License 2.0
121 stars 33 forks source link

Z3 4.8.10 #79

Open jad-hamza opened 3 years ago

jad-hamza commented 3 years ago

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

samarion commented 3 years ago

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

jad-hamza commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

This API might work: https://github.com/epfl-lara/ScalaZ3/blob/73cec6661a74153f16cc34f3c143d0cc78e64a42/src/main/scala/z3/scala/Z3Context.scala#L471

jad-hamza commented 3 years ago

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

samarion commented 3 years ago

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

mario-bucev commented 2 years ago

80 should address the problem with getAbsFunDecl