DEV Community

Discussion on: Open Source Adventures: Episode 06: How my crystal-z3 compares with bcardiff's crystal-z3

View post
Collapse
 
asterite profile image
Ary Borenszweig •

Hi! The reason Brian used to_unsafe is because that method is implicitly called when you pass something to C and the type doesn't match: crystal-lang.org/reference/1.3/syn...

So in your case if you define a to_unsafe for Z3::IntExpr that returns @expr, you could replace this:

    def ==(other)
      BoolExpr.new API.mk_eq(@expr, sort[other]._expr)
    end
Enter fullscreen mode Exit fullscreen mode

with this:

    def ==(other)
      BoolExpr.new API.mk_eq(self, sort[other])
    end
Enter fullscreen mode Exit fullscreen mode

which might be nicer to read/write, depending on personal taste.

Collapse
 
taw profile image
Tomasz Wegrzanowski •

Is it true even if I mark to_unsafe as protected?

To be honest if users call something called to_unsafe they only have themselves to blame. I just didn't want it to be called expr as that might encourage segfault-prone code.

Collapse
 
asterite profile image
Ary Borenszweig •

Hm, good point. Apparently it doesn't work if to_unsafe is protected or private, but I think it should. I'll ask to change that.