Skip to content

Multiple issues #45

Description

@DarthGandalf

I'm trying to use Z3 via python bindings, and it doesn't quite work:

  1. 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 do my $a = z3::Int('a'); $a.__add__(2) instead
  2. Some symbols are randomly missing: my $s = z3::Solver.new(); results in Could not find symbol '&Solver' in 'z3'. I was able to use z3::SimpleSolver.new() though.
  3. 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 = "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/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>

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions