search

ahumenberger / Z3.jl

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

fail gracefully #5

Closed shashi closed 4 years ago

shashi commented 4 years ago 
julia> isprovable((a > -2) & (a < 2), constraints)
terminate called after throwing an instance of 'z3::exception'

signal (6): Aborted
in expression starting at REPL[10]:1
gsignal at /usr/bin/../lib/libc.so.6 (unknown line)
abort at /usr/bin/../lib/libc.so.6 (unknown line)
__verbose_terminate_handler at /build/gcc/src/gcc/libstdc++-v3/libsupc++/vterminate.cc:95
__terminate at /build/gcc/src/gcc/libstdc++-v3/libsupc++/eh_terminate.cc:48
terminate at /build/gcc/src/gcc/libstdc++-v3/libsupc++/eh_terminate.cc:58
__cxa_throw at /build/gcc/src/gcc/libstdc++-v3/libsupc++/eh_throw.cc:95
_ZN2z36solver3addERKNS_4exprE at /home/shashi/.julia/dev/Z3/deps/src/libz3jl.so (unknown line)
_ZN5jlcxx6detail11CallFunctorIvJRN2z36solverERKNS2_4exprEEE5applyEPKvNS_13WrappedCppPtrESB_ at /home/shashi/.julia/dev/Z3/deps/src/libz3jl.so (unknown line)
add at ./none:0
issatisfiable at /home/shashi/.julia/dev/SymbolicSAT/src/SymbolicSAT.jl:58
isprovable at /home/shashi/.julia/dev/SymbolicSAT/src/SymbolicSAT.jl:71
unknown function (ip: 0x7f48c444402b)
unknown function (ip: 0x7f4901946855)
unknown function (ip: 0x7f49019464fa)
unknown function (ip: 0x7f4901947d84)
unknown function (ip: 0x7f4901948832)
unknown function (ip: 0x7f4901966371)
unknown function (ip: 0x7f4901966a08)
jl_toplevel_eval_in at /usr/bin/../lib/libjulia.so.1 (unknown line)
unknown function (ip: 0x7f48f4943e04)
unknown function (ip: 0x7f48f4b69bf9)
run_backend at /home/shashi/.julia/packages/Revise/MgvIv/src/Revise.jl:1023
unknown function (ip: 0x7f4901946855)
unknown function (ip: 0x7f49019464fa)
unknown function (ip: 0x7f4901947d84)
unknown function (ip: 0x7f4901948832)
unknown function (ip: 0x7f4901966371)
jl_toplevel_eval_in at /usr/bin/../lib/libjulia.so.1 (unknown line)
unknown function (ip: 0x7f48f4943e04)
unknown function (ip: 0x7f48f4b69bf9)
unknown function (ip: 0x7f48f4b69ef4)
unknown function (ip: 0x7f490194c439)
unknown function (ip: (nil))
Allocations: 63966637 (Pool: 63944336; Big: 22301); GC: 65
[1]    26027 abort (core dumped)  julia

This is quite jarring haha. It sounds like an exception was not caught on the Julia side... How is this usually fixed? I can attempt a PR.

ahumenberger commented 4 years ago

This should be fixed with the new Z3 version where z3::exception is then a subclass of std::exception. The latter is then caught on the Julia side via CxxWrap.jl

ahumenberger commented 4 years ago

Also the operator & only works for bitvector expressions (see https://z3prover.github.io/api/html/namespacez3.html#a6849e10009affbf81993e415c09b1ae2). If you use it for other expressions like the one above, then Z3 throws an exception. To take the conjunction of expressions you have to use and(x>2, y==1) or and([x>2, y==1]). Similar with or.

shashi commented 4 years ago

Fantastic! your suggestions worked!! Thank you!