Z3::FuncInterp
Inherits Struct < Value < Object
What a model decided an uninterpreted function does: the argument lists it had to
pin down, plus the else branch which answers for every other one. Z3 picks one of
the values as that fallback, so the entries are only the exceptions to it.
The Ruby gem is a Hash from argument lists to values, with Hash's own default
holding the else branch. Expressions can't be Hash keys here - see the
Limitations section of the README - so this is a list of {args, value} pairs and
#[] walks it.
Constructors
new(decl : Z3::FuncDecl, entries : Array(Tuple(Array(Z3::BitvecExpr | Z3::BoolExpr | Z3::CharExpr | Z3::FloatExpr | Z3::IntExpr | Z3::RealExpr | Z3::RoundingModeExpr | Z3::SeqExpr | Z3::StringExpr), Z3::BitvecExpr | Z3::BoolExpr | Z3::CharExpr | Z3::FloatExpr | Z3::IntExpr | Z3::RealExpr | Z3::RoundingModeExpr | Z3::SeqExpr | Z3::StringExpr)), default : Z3::BitvecExpr | Z3::BoolExpr | Z3::CharExpr | Z3::FloatExpr | Z3::IntExpr | Z3::RealExpr | Z3::RoundingModeExpr | Z3::SeqExpr | Z3::StringExpr)
SourceInstance methods
[](*args) : AnyExpr
What the function answers for these arguments, which for anything the model
never had to decide is the else branch
arity
Sourcedecl
Sourcedefault
Sourceentries
Sourceinspect(io)
Sourceto_s(io)
Source