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

• .add(args : Array(IntExpr | Int32))
• .add(args : Array(RealExpr))
• .and(args : Array(BoolExpr | Bool))
• .and(args : Array(BitvecExpr))

  Bitvec has no n-ary and/or in Z3, so reduce with the bitwise operators.

• .bitvec(name, size : UInt32)
• .bool(name)
• .distinct(args : Array(IntExpr))
• .distinct(args : Array(RealExpr))
• .distinct(args : Array(BoolExpr))
• .distinct(args : Array(BitvecExpr))
• .int(name)
• .mul(args : Array(IntExpr | Int32))
• .mul(args : Array(RealExpr))
• .or(args : Array(BoolExpr | Bool))
• .or(args : Array(BitvecExpr))
• .real(name)
• .version

Class Method Detail