class

Z3::FuncDecl

Inherits Reference < Object

A function symbol - what SMT-LIB's declare-fun declares, and what a model hands back when it has decided what a function does.

Applying one with #[] gives an expression of the declared range sort, which is only known at runtime, so the result is an AnyExpr - a union - and has to be narrowed before anything at all can be done with it, == included:

f = Z3.function("f", Z3::IntSort, Z3::IntSort)
x = f[3].as(Z3::IntExpr)
solver.assert x == 10

This is the tax on there being no common Z3::Expr base class yet - see _TODO.md.

Constructors

declare(name : String, sorts : Array(AnySort)) : FuncDecl

Last sort is the range, the ones before it are the domain, the same order SMT-LIB's declare-fun uses

Source

declare_fresh(prefix : String, sorts : Array(AnySort)) : FuncDecl

Source

declare_rec(name : String, sorts : Array(AnySort)) : FuncDecl

Source

new(decl : LibZ3::FuncDecl)

Source

Class methods

recursive_decl_kind

Z3's answer for #recursive? is the decl kind Z3_OP_RECURSIVE, whose numeric value sits at the far end of an enum which grows between releases - so rather than writing the number down, we make one recursive declaration and ask Z3 what kind it came out as. Leaving it undefined is safe: nothing applies it, so no solver ever has to unfold it and no model mentions it.

Source

Instance methods

==(other : FuncDecl)

Z3 hash-conses declarations, so two decls of the same name and signature are one and the same pointer. Unlike an expression there's nothing for == to build - a declaration is not a value - so this answers the question directly, and a FuncDecl works as a Hash key.

Source

[](*args) : AnyExpr

Applies the function. Arguments are cast into the declared domain sorts, so f[3] works wherever f[IntSort[3]] does.

Source

arity

Source

call(*args) : AnyExpr

Source

define

Gives a recursive declaration its body - the define-fun-rec half of Z3.rec_function. The block gets one fresh variable per domain sort, as an Array because the arity is only known at runtime, and returns the body - which may call this very function:

fact = Z3.rec_function("fact", Z3::IntSort, Z3::IntSort)
fact.define do |args|
  n = args[0].as(Z3::IntExpr)
  (n <= 0).ite(1, n * fact[n - 1].as(Z3::IntExpr))
end

The Ruby gem takes the body as a block on Z3.RecFunction too. Here it's always this second step, because Crystal has no way to pass a variable number of block arguments and mutual recursion needs the two-step form anyway.

Only a declaration made by Z3.rec_function can be defined; Z3 says so itself for any other, which is a better error than anything we could check for here.

Source

domain(i : Int) : AnySort

Source

hash(hasher)

See Object#hash(hasher)

inspect(io)

name

range

recursive?

Whether this was declared by Z3.rec_function, which is worth asking because Z3 hands those back in places nothing else shows up - see Model#funcs.

Source

to_s(io)

Source

to_unsafe

Source