module Z3

Defined in:

z3.cr
z3/api.cr
z3/bitvec_expr.cr
z3/bitvec_sort.cr
z3/bool_expr.cr
z3/bool_sort.cr
z3/int_expr.cr
z3/int_sort.cr
z3/model.cr
z3/real_expr.cr
z3/real_sort.cr
z3/solver.cr

Constant Summary

VERSION = "0.1.0"

Class Method Summary

Class Method Detail

def self.add(args : Array(IntExpr | Int)) #

[View source]
def self.and(args : Array(BoolExpr | Bool)) #

[View source]
def self.bitvec(name, size : UInt32) #

[View source]
def self.bool(name) #

[View source]
def self.distinct(args : Array(IntExpr)) #

[View source]
def self.int(name) #

[View source]
def self.mul(args : Array(IntExpr | Int)) #

[View source]
def self.or(args : Array(BoolExpr | Bool)) #

[View source]
def self.real(name) #

[View source]
def self.version #

[View source]