alias Z3::AnySort

Overview

Any sort, as a value. The sorts with nothing to configure are singletons, and a Crystal class is already one of those, so they are the classes themselves - while a Bitvec or a Seq has to be instantiated with its size or its element sort.

Whichever it is, every sort answers to_unsafe with its Z3 sort, from_ast with an expression of itself, and cast with a Crystal object converted into one. Those three are what a Seq needs, since its element sort is only known at runtime.

Alias Definition

Z3::BitvecSort | Z3::BoolSort.class | Z3::CharSort.class | Z3::IntSort.class | Z3::RealSort.class | Z3::SeqSort | Z3::StringSort.class

Defined in:

z3.cr