module Z3

Defined in:

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))
• .distinct(args : Array(FloatExpr))

  Z3's own .distinct, so this is term inequality - +zero and -zero are distinct floats even though +zero == -zero, and two NaNs are not

• .distinct(args : Array(RoundingModeExpr))
• .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)
• .float(name : String, ebits : Int, sbits : Int)
• .float(name : String, sort : FloatSort)

  The sort is a width - 16, 32, 64 or 128 - a name - :half, :single, :double or :quadruple - a FloatSort, or the two bit counts spelled out

• .float(name : String, width : Int | Symbol)
• .fresh_function(prefix : String, *sorts : AnySort) : FuncDecl

  The same as Z3.function with a name Z3 picks, for helper functions which mustn't collide with anything you've named

• .function(name : String, *sorts : AnySort) : FuncDecl

  An uninterpreted function - a symbol the solver decides the meaning of.

• .int(name : String)
• .mul(args : Array(IntExpr | Int32))
• .mul(args : Array(RealExpr))
• .or(args : Array(BoolExpr | Bool))
• .or(args : Array(BitvecExpr))
• .real(name : String)
• .rec_function(name : String, *sorts : AnySort) : FuncDecl

  A function which is its body, rather than one the solver gets to interpret - SMT-LIB's define-fun-rec.

• .rounding_mode(name : String)
• .seq(name : String, element_sort)
• .string(name : String)
• .version

Class Method Detail

even = Z3.rec_function("even", Z3::IntSort, Z3::BoolSort)
odd = Z3.rec_function("odd", Z3::IntSort, Z3::BoolSort)
even.define { |args| ... odd[...] ... }
odd.define { |args| ... even[...] ... }