Multiple issues #45
Description
I'm trying to use Z3 via python bindings, and it doesn't quite work:
- Looks like there's no support for operator overloading. In python I can use
a = z3.Int('a'); a + 2, but here I had to domy $a = z3::Int('a'); $a.__add__(2)instead - Some symbols are randomly missing:
my $s = z3::Solver.new();results inCould not find symbol '&Solver' in 'z3'. I was able to usez3::SimpleSolver.new()though. - Segfault during calling some functions. In the following code
$s.add()segfaults:
unit module Day24;
use Inline::Python;
use z3:from<Python>;
our sub part2(Str $input) {
for z3::.keys {
.say
}
my $s = z3::SimpleSolver.new();
my ($spx, $spy, $spz, $svx, $svy, $svz) = z3::Ints(names=>'spx spy spz svx svy svz');
for $input.lines.kv -> $i, $line {
my ($pos, $vec) = $line.split(' @ ');
my ($px, $py, $pz) = $pos.split(', ');
my ($vx, $vy, $vz) = $vec.split(', ');
my $t = z3::Int("t$i");
my $a = $t.__mul__($vx).__add__($px);
my $b = $t.__mul__($svx).__add__($spx);
$s.add($a.__eq__($b));
}
return 0;
}#0 0x00007fffecb982e9 in PyObject_GetAttrString (v=0x0, name=0x5555557d87b0 "add") at Objects/object.c:796
w = <optimized out>
res = <optimized out>
#1 0x00007ffff42010ba in py_call_method () from /home/somebody/.raku/resources/15A7732F70D51B37276F0C1819FD5F091BA26D2D.so
No symbol table info available.
#2 0x00007ffff7f1d2ba in ffi_call_unix64 () at /mnt/portagetmp/portage/dev-libs/libffi-3.4.4-r2/work/libffi-3.4.4/src/x86/unix64.S:104
No locals.
#3 0x00007ffff7f1c6d1 in ffi_call_int (cif=cif@entry=0x7fffffffcba0, fn=fn@entry=0x7ffff4201093 <py_call_method>, rvalue=<optimized out>, rvalue@entry=0x7fffffffcb98, avalue=<optimized out>, closure=closure@entry=0x0)
at /mnt/portagetmp/portage/dev-libs/libffi-3.4.4-r2/work/libffi-3.4.4/src/x86/ffi64.c:673
classes = {X86_64_INTEGER_CLASS, X86_64_NO_CLASS, 3818208000, 758617458}
stack = <optimized out>
argp = <optimized out>
arg_types = <optimized out>
gprcount = 3
ssecount = <optimized out>
ngpr = 1
nsse = 0
i = <optimized out>
avn = <optimized out>
flags = <optimized out>
reg_args = <optimized out>
#4 0x00007ffff7f1ce2d in ffi_call (cif=cif@entry=0x7fffffffcba0, fn=fn@entry=0x7ffff4201093 <py_call_method>, rvalue=rvalue@entry=0x7fffffffcb98, avalue=avalue@entry=0x7fffffffcac0) at /mnt/portagetmp/portage/dev-libs/libffi-3.4.4-r2/work/libffi-3.4.4/src/x86/ffi64.c:710
arg_types = 0x200084d5b40
i = <optimized out>
nargs = 3
max_reg_struct_size = <optimized out>
#5 0x00007ffff783e3ff in MVM_nativecall_dispatch (tc=tc@entry=0x20000020000, res_type=<optimized out>, site=<optimized out>, args=...) at src/core/nativecall_libffi.c:1106
ret = 0x20008000001
result = 0x0
free_strs = <optimized out>
num_strs = <optimized out>
i = <optimized out>
body = <optimized out>
num_args = <optimized out>
arg_types = <optimized out>
ret_type = <optimized out>
entry_point = <optimized out>
values = <optimized out>
interval_id = <optimized out>
cif = {abi = FFI_UNIX64, nargs = 3, arg_types = 0x200084d5b40, rtype = 0x7ffff7f1e060 <ffi_type_pointer>, bytes = 0, flags = 7}
status = <optimized out>
ret = <optimized out>
ret = <optimized out>
ret = <optimized out>
ret = <optimized out>
ret = <optimized out>
ret = <optimized out>
ret = <optimized out>
ret = <optimized out>
ret = <optimized out>
ret = <optimized out>
ret = <optimized out>
ret = <optimized out>
ret = <optimized out>
ret = <optimized out>
#6 0x00007ffff78b11f2 in MVM_disp_program_record_end (tc=tc@entry=0x20000020000, record=record@entry=0x200005035e0) at src/disp/program.c:3197
site = <optimized out>
result_type = <optimized out>
#7 0x00007ffff782d3f8 in handle_end_of_dispatch_record (tc=0x20000020000) at src/core/callstack.c:567
disp_record = 0x200005035e0
remove_dispatch_frame = <optimized out>
__PRETTY_FUNCTION__ = "handle_end_of_dispatch_record"
#8 0x00007ffff78b126c in MVM_disp_program_record_end (tc=tc@entry=0x20000020000, record=record@entry=0x200005035e0) at src/disp/program.c:3099
site = <optimized out>
result_type = <optimized out>
#9 0x00007ffff782d3f8 in handle_end_of_dispatch_record (tc=0x20000020000) at src/core/callstack.c:567
disp_record = 0x200005035e0
remove_dispatch_frame = <optimized out>
__PRETTY_FUNCTION__ = "handle_end_of_dispatch_record"
#10 0x00007ffff782e7db in cleanup_dispatch_record_record (exceptional=0 '\000', tc=0x20000020000) at src/core/callstack.c:665
bytecode_was = 0x7ffff4369c82 "\b"
#11 MVM_callstack_unwind_frame (tc=tc@entry=0x20000020000, exceptional=exceptional@entry=0 '\000') at src/core/callstack.c:837
thunked = 0
__PRETTY_FUNCTION__ = "MVM_callstack_unwind_frame"
frame = <optimized out>
#12 0x00007ffff782a56a in MVM_frame_try_return (tc=0x20000020000) at src/core/frame.c:939
cur_frame = 0x2000017c1d0
#13 0x00007ffff781bf26 in MVM_interp_run (tc=0x0, initial_invoke=0x5555557d87b0, initial_invoke@entry=0x7ffff791d420 <toplevel_initial_invoke>, invoke_data=0x5555557d87b0, invoke_data@entry=0x7ffff791d420 <toplevel_initial_invoke>, outer_runloop=0x200083cc780,
outer_runloop@entry=0x0) at src/core/interp.c:578
value = <optimized out>
op = 0
LABELS = {0x7ffff7807174 <MVM_interp_run+212>, 0x7ffff781d034 <MVM_interp_run+90004>, 0x7ffff78074df <MVM_interp_run+1087>, 0x7ffff78074df <MVM_interp_run+1087>, 0x7ffff780dc18 <MVM_interp_run+27512>, 0x7ffff781cfbc <MVM_interp_run+89884>,
0x7ffff780d462 <MVM_interp_run+25538>, 0x7ffff780a619 <MVM_interp_run+13689>, 0x7ffff780a5e0 <MVM_interp_run+13632>, 0x7ffff780a5a7 <MVM_interp_run+13575>, 0x7ffff780a56e <MVM_interp_run+13518>, 0x7ffff780e17a <MVM_interp_run+28890>,
0x7ffff780d96a <MVM_interp_run+26826>, 0x7ffff780dfb0 <MVM_interp_run+28432>, 0x7ffff780d032 <MVM_interp_run+24466>, 0x7ffff78074f7 <MVM_interp_run+1111>, 0x7ffff781bffb <MVM_interp_run+85851>, 0x7ffff781bfc3 <MVM_interp_run+85795>,
0x7ffff781bf8a <MVM_interp_run+85738>, 0x7ffff781bf51 <MVM_interp_run+85681>, 0x7ffff781c0ff <MVM_interp_run+86111>, 0x7ffff781c0c0 <MVM_interp_run+86048>, 0x7ffff781c081 <MVM_interp_run+85985>, 0x7ffff781c034 <MVM_interp_run+85908>,
0x7ffff781c137 <MVM_interp_run+86167>, 0x7ffff781bcef <MVM_interp_run+85071>, 0x7ffff781bc86 <MVM_interp_run+84966>, 0x7ffff781bc23 <MVM_interp_run+84867>, 0x7ffff781c3b6 <MVM_interp_run+86806>, 0x7ffff781c340 <MVM_interp_run+86688>,
0x7ffff781c2c8 <MVM_interp_run+86568>, 0x7ffff781c24a <MVM_interp_run+86442>, 0x7ffff781cd28 <MVM_interp_run+89224>, 0x7ffff781cc9a <MVM_interp_run+89082>, 0x7ffff781c62f <MVM_interp_run+87439>, 0x7ffff781c49d <MVM_interp_run+87037>,
0x7ffff781be58 <MVM_interp_run+85432>, 0x7ffff781bde1 <MVM_interp_run+85313>, 0x7ffff781c5b8 <MVM_interp_run+87320>, 0x7ffff781c541 <MVM_interp_run+87201>, 0x7ffff781c6b6 <MVM_interp_run+87574>, 0x7ffff781c19a <MVM_interp_run+86266>,
0x7ffff781c430 <MVM_interp_run+86928>, 0x7ffff7816048 <MVM_interp_run+61352>, 0x7ffff7815fdb <MVM_interp_run+61243>, 0x7ffff781cf44 <MVM_interp_run+89764>, 0x7ffff781cf44 <MVM_interp_run+89764>, 0x7ffff7815f64 <MVM_interp_run+61124>,
0x7ffff781ce84 <MVM_interp_run+89572>, 0x7ffff781cb52 <MVM_interp_run+88754>, 0x7ffff781cad6 <MVM_interp_run+88630>, 0x7ffff781ca7a <MVM_interp_run+88538>, 0x7ffff781cd6f <MVM_interp_run+89295>, 0x7ffff781ce28 <MVM_interp_run+89480>,
0x7ffff781bef5 <MVM_interp_run+85589>, 0x7ffff781c7d8 <MVM_interp_run+87864>, 0x7ffff781c791 <MVM_interp_run+87793>, 0x7ffff781c74a <MVM_interp_run+87722>, 0x7ffff781cc53 <MVM_interp_run+89011>, 0x7ffff7816104 <MVM_interp_run+61540>,
0x7ffff781c8ad <MVM_interp_run+88077>, 0x7ffff781c81f <MVM_interp_run+87935>, 0x7ffff781c93b <MVM_interp_run+88219>, 0x7ffff781bd4c <MVM_interp_run+85164>, 0x7ffff781ca38 <MVM_interp_run+88472>, 0x7ffff781c207 <MVM_interp_run+86375>,
0x7ffff781c9d5 <MVM_interp_run+88373>, 0x7ffff7812d4a <MVM_interp_run+48298>, 0x7ffff7812cfa <MVM_interp_run+48218>, 0x7ffff7812cb6 <MVM_interp_run+48150>, 0x7ffff7812c7a <MVM_interp_run+48090>, 0x7ffff7812c37 <MVM_interp_run+48023>,
0x7ffff7812c06 <MVM_interp_run+47974>, 0x7ffff7812bd5 <MVM_interp_run+47925>, 0x7ffff7812ba4 <MVM_interp_run+47876>, 0x7ffff7812b73 <MVM_interp_run+47827>, 0x7ffff7812b31 <MVM_interp_run+47761>, 0x7ffff7812aef <MVM_interp_run+47695>,
0x7ffff7812aad <MVM_interp_run+47629>, 0x7ffff7812a71 <MVM_interp_run+47569>, 0x7ffff78129ee <MVM_interp_run+47438>, 0x7ffff78129a7 <MVM_interp_run+47367>, 0x7ffff781295b <MVM_interp_run+47291>, 0x7ffff7812919 <MVM_interp_run+47225>,
0x7ffff78128ab <MVM_interp_run+47115>, 0x7ffff7812840 <MVM_interp_run+47008>, 0x7ffff78127ee <MVM_interp_run+46926>, 0x7ffff781279c <MVM_interp_run+46844>, 0x7ffff7812751 <MVM_interp_run+46769>, 0x7ffff7812706 <MVM_interp_run+46694>,
0x7ffff78126bb <MVM_interp_run+46619>, 0x7ffff7812670 <MVM_interp_run+46544>, 0x7ffff7812615 <MVM_interp_run+46453>, 0x7ffff78125d0 <MVM_interp_run+46384>, 0x7ffff781258b <MVM_interp_run+46315>, 0x7ffff7812546 <MVM_interp_run+46246>,
0x7ffff7812501 <MVM_interp_run+46177>, 0x7ffff78124a2 <MVM_interp_run+46082>, 0x7ffff781245f <MVM_interp_run+46015>, 0x7ffff781241c <MVM_interp_run+45948>, 0x7ffff78123c5 <MVM_interp_run+45861>, 0x7ffff7812383 <MVM_interp_run+45795>,
0x7ffff7812341 <MVM_interp_run+45729>, 0x7ffff78122f7 <MVM_interp_run+45655>, 0x7ffff78122ab <MVM_interp_run+45579>, 0x7ffff7812261 <MVM_interp_run+45505>, 0x7ffff7812215 <MVM_interp_run+45429>, 0x7ffff78121cb <MVM_interp_run+45355>,
0x7ffff7812181 <MVM_interp_run+45281>, 0x7ffff781212a <MVM_interp_run+45194>, 0x7ffff781c8f4 <MVM_interp_run+88148>, 0x7ffff781cce1 <MVM_interp_run+89153>, 0x7ffff78120de <MVM_interp_run+45118>, 0x7ffff7812092 <MVM_interp_run+45042>,
0x7ffff7812048 <MVM_interp_run+44968>, 0x7ffff781c98e <MVM_interp_run+88302>, 0x7ffff7811ff2 <MVM_interp_run+44882>, 0x7ffff7811fa6 <MVM_interp_run+44806>, 0x7ffff7811f5a <MVM_interp_run+44730>, 0x7ffff7811f1a <MVM_interp_run+44666>,
0x7ffff7811edf <MVM_interp_run+44607>, 0x7ffff7811e8d <MVM_interp_run+44525>, 0x7ffff7811e3a <MVM_interp_run+44442>, 0x7ffff7811de8 <MVM_interp_run+44360>, 0x7ffff7811d43 <MVM_interp_run+44195>, 0x7ffff781c866 <MVM_interp_run+88006>,
0x7ffff781bd8e <MVM_interp_run+85230>, 0x7ffff781d0cf <MVM_interp_run+90159>, 0x7ffff781d0ca <MVM_interp_run+90154>, 0x7ffff781d0c5 <MVM_interp_run+90149>, 0x7ffff781d0c0 <MVM_interp_run+90144>, 0x7ffff781d0f2 <MVM_interp_run+90194>,
0x7ffff781d0ed <MVM_interp_run+90189>, 0x7ffff781d0e8 <MVM_interp_run+90184>, 0x7ffff781d0e3 <MVM_interp_run+90179>, 0x7ffff781d0de <MVM_interp_run+90174>, 0x7ffff781d0d9 <MVM_interp_run+90169>, 0x7ffff781d0d4 <MVM_interp_run+90164>,
0x7ffff780723a <MVM_interp_run+410>, 0x7ffff780723a <MVM_interp_run+410>, 0x7ffff7813994 <MVM_interp_run+51444>, 0x7ffff7813a47 <MVM_interp_run+51623>, 0x7ffff78139e6 <MVM_interp_run+51526>, 0x7ffff7813bf4 <MVM_interp_run+52052>,
0x7ffff7813b94 <MVM_interp_run+51956>, 0x7ffff7813b1c <MVM_interp_run+51836>, 0x7ffff7813aa7 <MVM_interp_run+51719>, 0x7ffff7813f63 <MVM_interp_run+52931>, 0x7ffff7813fdb <MVM_interp_run+53051>, 0x7ffff7813e6b <MVM_interp_run+52683>,
0x7ffff7813ee7 <MVM_interp_run+52807>, 0x7ffff7813def <MVM_interp_run+52559>, 0x7ffff7813d73 <MVM_interp_run+52435>, 0x7ffff7813ce2 <MVM_interp_run+52290>, 0x7ffff7813c54 <MVM_interp_run+52148>, 0x7ffff78144e9 <MVM_interp_run+54345>,
0x7ffff7814458 <MVM_interp_run+54200>, 0x7ffff7814408 <MVM_interp_run+54120>, 0x7ffff781461c <MVM_interp_run+54652>, 0x7ffff78145d7 <MVM_interp_run+54583>, 0x7ffff7814382 <MVM_interp_run+53986>, 0x7ffff781433b <MVM_interp_run+53915>,
0x7ffff78142e9 <MVM_interp_run+53833>, 0x7ffff781429d <MVM_interp_run+53757>, 0x7ffff781424b <MVM_interp_run+53675>, 0x7ffff78141f9 <MVM_interp_run+53593>, 0x7ffff78141ab <MVM_interp_run+53515>, 0x7ffff7814159 <MVM_interp_run+53433>,
0x7ffff7814107 <MVM_interp_run+53351>, 0x7ffff78140ae <MVM_interp_run+53262>, 0x7ffff7814053 <MVM_interp_run+53171>, 0x7ffff7811ce5 <MVM_interp_run+44101>, 0x7ffff7811c87 <MVM_interp_run+44007>, 0x7ffff7811c31 <MVM_interp_run+43921>,
0x7ffff7811bd8 <MVM_interp_run+43832>, 0x7ffff7811b35 <MVM_interp_run+43669>, 0x7ffff7811ad9 <MVM_interp_run+43577>, 0x7ffff7811b8e <MVM_interp_run+43758>, 0x7ffff7811a93 <MVM_interp_run+43507>, 0x7ffff7811a39 <MVM_interp_run+43417>,
0x7ffff781d1c7 <MVM_interp_run+90407>, 0x7ffff781d1af <MVM_interp_run+90383>, 0x7ffff78119e7 <MVM_interp_run+43335>, 0x7ffff7811996 <MVM_interp_run+43254>, 0x7ffff7811945 <MVM_interp_run+43173>, 0x7ffff7814bca <MVM_interp_run+56106>,
0x7ffff7814b71 <MVM_interp_run+56017>, 0x7ffff7814b18 <MVM_interp_run+55928>, 0x7ffff7814abe <MVM_interp_run+55838>, 0x7ffff7814a65 <MVM_interp_run+55749>, 0x7ffff7814a0c <MVM_interp_run+55660>, 0x7ffff78149af <MVM_interp_run+55567>,
0x7ffff781495d <MVM_interp_run+55485>, 0x7ffff781d0a8 <MVM_interp_run+90120>, 0x7ffff781cfa4 <MVM_interp_run+89860>, 0x7ffff781cfa4 <MVM_interp_run+89860>, 0x7ffff7814928 <MVM_interp_run+55432>, 0x7ffff78148e6 <MVM_interp_run+55366>,
0x7ffff7814889 <MVM_interp_run+55273>, 0x7ffff781481c <MVM_interp_run+55164>...}
cur_op = 0x7ffff4369c82 "\b"
bytecode_start = 0x7ffff43699fe "\214"
reg_base = 0x200005034d8
cu = 0x200006b6970
#14 0x00007ffff791e625 in MVM_vm_run_file (instance=instance@entry=0x20000010000, filename=filename@entry=0x5555555594c0 "/usr/share/perl6/runtime/perl6.moarvm") at src/moar.c:505
tc = <optimized out>
cu = <optimized out>
str = <optimized out>
#15 0x000055555555562e in main (argc=<optimized out>, argv=<optimized out>) at src/vm/moar/runner/main.c:480
instance = 0x20000010000
exec_path = 0x555555556170 "/usr/bin/rakudo"
exec_path_size = 15
exec_dir_path_temp = 0x5555555592a0 "/usr/bin"
exec_dir_path = <optimized out>
exec_dir_path_size = <optimized out>
nqp_home = 0x555555556139 "/usr/share/nqp"
nqp_home_size = <optimized out>
static_nqp_home = 0x555555556139 "/usr/share/nqp"
nqp_rel_path = "/../share/nqp"
nqp_rel_path_size = 13
nqp_check_path = "/lib/NQPCORE.setting.moarvm"
nqp_check_path_size = 27
rakudo_home = 0x555555556153 "/usr/share/perl6"
rakudo_home_size = <optimized out>
static_rakudo_home = 0x555555556153 "/usr/share/perl6"
option_rakudo_home = <optimized out>
perl6_rel_path = "/../share/perl6"
perl6_rel_path_size = 15
perl6_check_path = "/runtime/perl6.moarvm"
perl6_check_path_size = 21
lib_path = {0x5555555593d0 "/usr/share/nqp/lib", 0x555555559420 "/usr/share/perl6/lib", 0x555555559470 "/usr/share/perl6/runtime"}
perl6_file = 0x5555555594c0 "/usr/share/perl6/runtime/perl6.moarvm"
full_cleanup = <optimized out>
argi = <optimized out>
flag = <optimized out>
new_argc = <optimized out>
debugserverport = <optimized out>
start_suspended = <optimized out>