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/char_expr.cr
z3/char_sort.cr
z3/int_expr.cr
z3/int_sort.cr
z3/model.cr
z3/range_indexing.cr
z3/real_expr.cr
z3/real_sort.cr
z3/seq_expr.cr
z3/seq_sort.cr
z3/solver.cr
z3/string_expr.cr
z3/string_sort.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.

• .at_least(args : Array(BoolExpr), k : Int32)

  Native cardinality constraint: at least k of the given Bool exprs are true, or at least k units of weight when given {expr, weight} pairs

• .at_least(args : Array(Tuple(BoolExpr, Int32)), k : Int32)
• .at_most(args : Array(BoolExpr), k : Int32)

  Native cardinality constraint: at most k of the given Bool exprs are true.

• .at_most(args : Array(Tuple(BoolExpr, Int32)), k : Int32)
• .bitvec(name : String, size : UInt32)
• .bool(name : String)
• .char(name : String)
• .distinct(args : Array(IntExpr))
• .distinct(args : Array(RealExpr))
• .distinct(args : Array(BoolExpr))
• .distinct(args : Array(BitvecExpr))
• .distinct(args : Array(CharExpr))
• .distinct(args : Array(StringExpr))
• .distinct(args : Array(SeqExpr))
• .exactly(args : Array(BoolExpr), k : Int32)

  Native cardinality constraint: exactly k of the given Bool exprs are true, or exactly k units of weight when given {expr, weight} pairs

• .exactly(args : Array(Tuple(BoolExpr, Int32)), k : Int32)
• .int(name : String)
• .mul(args : Array(IntExpr | Int32))
• .mul(args : Array(RealExpr))
• .or(args : Array(BoolExpr | Bool))
• .or(args : Array(BitvecExpr))
• .real(name : String)
• .seq(name : String, element_sort)
• .string(name : String)
• .version

Class Method Detail