abstract struct Int

Overview

Ruby gets 2 + expr from Integer#coerce. Crystal has no such protocol, so every reversed operator has to be spelled out - one per Crystal type which can be cast into the sort on the other side.

Included Modules

Defined in:

z3/core_ext.cr

Instance Method Summary

Instance Method Detail

def !=(other : Z3::BitvecExpr) #

[View source]
def !=(other : Z3::IntExpr) #

[View source]
def !=(other : Z3::RealExpr) #

[View source]
def &(other : Z3::BitvecExpr) #

[View source]
def *(other : Z3::BitvecExpr) #

[View source]
def *(other : Z3::IntExpr) #

[View source]
def *(other : Z3::RealExpr) #

[View source]
def +(other : Z3::BitvecExpr) #

A Bitvec literal takes its size from the expression it's paired with, and the comparisons are all sign-dependent, so they're #signed_lt and friends only


[View source]
def +(other : Z3::IntExpr) #

[View source]
def +(other : Z3::RealExpr) #

[View source]
def -(other : Z3::BitvecExpr) #

[View source]
def -(other : Z3::IntExpr) #

[View source]
def -(other : Z3::RealExpr) #

[View source]
def /(other : Z3::IntExpr) #

[View source]
def /(other : Z3::RealExpr) #

[View source]
def <(other : Z3::IntExpr) #

[View source]
def <(other : Z3::RealExpr) #

[View source]
def <=(other : Z3::IntExpr) #

[View source]
def <=(other : Z3::RealExpr) #

[View source]
def ==(other : Z3::BitvecExpr) #

[View source]
def ==(other : Z3::IntExpr) #

[View source]
def ==(other : Z3::RealExpr) #

[View source]
def >(other : Z3::IntExpr) #

[View source]
def >(other : Z3::RealExpr) #

[View source]
def >=(other : Z3::IntExpr) #

[View source]
def >=(other : Z3::RealExpr) #

[View source]
def ^(other : Z3::BitvecExpr) #

[View source]
def |(other : Z3::BitvecExpr) #

[View source]