Native cardinality constraint: at most k of the given Bool exprs are true. An {expr, weight} pair list weighs them instead, so Z3.at_most([{a, 3}, {b, 2}], 4) allows either one but not both.

Ruby's z3 spells the weighted form as an expr => weight Hash. Exprs can't be Hash keys here - see the Limitations section of the README.

Source

at_most(args : Array(Tuple(BoolExpr, Int32)), k : Int32)

Source

bitvec(name : String, size : UInt32)

Source

bool(name : String)

Source

char(name : String)

Source

distinct(args : Array(IntExpr))

Source

distinct(args : Array(RealExpr))

Source

distinct(args : Array(BoolExpr))

Source

distinct(args : Array(BitvecExpr))

Source

distinct(args : Array(CharExpr))

Source

distinct(args : Array(StringExpr))

Source

distinct(args : Array(SeqExpr))

Source

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

Source

distinct(args : Array(RoundingModeExpr))

Source

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

Source

exactly(args : Array(Tuple(BoolExpr, Int32)), k : Int32)

Source

float(name : String, ebits : Int, sbits : Int)

Source

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

Source

float(name : String, width : Int | Symbol)

Source

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

Source

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

An uninterpreted function - a symbol the solver decides the meaning of. The last sort is the range and the ones before it the domain, so Z3.function("f", Int, Int, Bool) is a two argument predicate. Apply it with f[x, y].

Source

int(name : String)

Source

mul(args : Array(IntExpr | Int32))

Source

mul(args : Array(RealExpr))

Source

or(args : Array(BoolExpr | Bool))

Source

or(args : Array(BitvecExpr))

Source

real(name : String)

Source

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. Declaring and defining are two steps so that the body can mention the function it defines, and so that mutually recursive functions can both be declared before either is defined:

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[...] ... }

A declaration never given a body is not an error and doesn't announce itself - it simply behaves as an uninterpreted function. Z3 doesn't check that the recursion terminates either, and one it can't finish unfolding comes back as Unknown.

A definition belongs to the context rather than to any solver, exactly as it would in an SMT-LIB script, so it is permanent and every solver made afterwards carries it.

Source

rounding_mode(name : String)

Source

seq(name : String, element_sort)

Source

string(name : String)

Source

version

Source