struct Z3::FuncInterp

• Z3::FuncInterp
• Struct
• Value
• Object

Overview

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.

Defined in:

z3/func_interp.cr

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)

Instance Method Summary

• #[](*args) : AnyExpr

  What the function answers for these arguments, which for anything the model never had to decide is the else branch

• #arity
• #decl : FuncDecl
• #default : AnyExpr
• #entries : Array(Tuple(Array(AnyExpr), AnyExpr))
• #inspect(io)
• #size

  How many argument lists the model pinned down, not counting the else branch

• #to_s(io)

Constructor Detail

Instance Method Detail