class
Z3::FuncDecl
- Z3::FuncDecl
- Reference
- Object
Overview
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 == 10This is the tax on there being no common Z3::Expr base class yet - see _TODO.md.
Defined in:
z3/func_decl.crConstructors
-
.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-funuses - .declare_fresh(prefix : String, sorts : Array(AnySort)) : FuncDecl
- .declare_rec(name : String, sorts : Array(AnySort)) : FuncDecl
- .new(decl : LibZ3::FuncDecl)
Class Method Summary
-
.recursive_decl_kind : UInt32
Z3's answer for
#recursive?is the decl kindZ3_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.
Instance Method Summary
-
#==(other : FuncDecl)
Z3 hash-conses declarations, so two decls of the same name and signature are one and the same pointer.
-
#[](*args) : AnyExpr
Applies the function.
- #arity
- #call(*args) : AnyExpr
-
#define(&) : self
Gives a recursive declaration its body - the
define-fun-rechalf ofZ3.rec_function. - #domain(i : Int) : AnySort
-
#hash(hasher)
See
Object#hash(hasher) - #inspect(io)
- #name : String
- #range : AnySort
-
#recursive?
Whether this was declared by
Z3.rec_function, which is worth asking because Z3 hands those back in places nothing else shows up - seeModel#funcs. - #to_s(io)
- #to_unsafe : LibZ3::FuncDecl
Constructor Detail
Last sort is the range, the ones before it are the domain, the same order
SMT-LIB's declare-fun uses
Class Method Detail
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.
Instance Method Detail
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.
Applies the function. Arguments are cast into the declared domain sorts, so
f[3] works wherever f[IntSort[3]] does.
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))
endThe 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.
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.