search

ahumenberger / Z3.jl

Julia interface to Z3
MIT License
57 stars 7 forks source link

Where are the methods defined? #2

Closed shashi closed 4 years ago

shashi commented 4 years ago

I'm looking for mk_lt... but it's not in the Z3 module's namespace. I'm not sure if I'm using this right. Where do I look for all the functions that are wrapped?

Thank you!

shashi commented 4 years ago

Ah, I see I can just do x < y, but I can't figure out where that method is defined...

julia> @edit x < y
ERROR: could not determine location of method definition
Stacktrace:
 [1] functionloc at ./methodshow.jl:153 [inlined]
 [2] functionloc at ./methodshow.jl:163 [inlined]
 [3] edit(::Function, ::Any) at /build/julia/src/julia-1.4.1/usr/share/julia/stdlib/v1.4/InteractiveUtils/src/editless.jl:220
 [4] top-level scope at REPL[6]:1
 [5] run_backend(::REPL.REPLBackend) at /home/shashi/.julia/packages/Revise/MgvIv/src/Revise.jl:1023
 [6] top-level scope at none:0

julia> @which x < y
<(arg1::Union{CxxWrap.SmartPointer{T2}, T2} where T2<:Z3.Expr, arg2::Union{CxxWrap.SmartPointer{T2}, T2} where T2<:Z3.Expr) in Z3
ahumenberger commented 4 years ago

The C++ part of the wrapper defines the types/methods which are exposed. The package CxxWrap.jl then creates the corresponding Julia types and methods. The functions for comparison are defined here:

https://github.com/ahumenberger/Z3.jl/blob/c18fd48b4f7e329e2b3c825f1fcf1d4bbd7dafdd/deps/src/z3jl.cpp#L247-L252

Note though that the current version does not yet expose everything from Z3's C++ API. But there should be a new version around soon (see https://github.com/Z3Prover/z3/issues/4183).

shashi commented 4 years ago

Perfect! Thank you!