Enum TheoryKind 

pub enum TheoryKind {
    Null,
    Basic,
    Label,
    Pattern,
    ModelValue,
    UserSort,
    Arith,
    Polymorphic,
    Other(IString),
    Unknown(NonZeroU32),
}

See https://github.com/Z3Prover/z3/blob/z3-4.13.4/src/ast/ast.h#L78-L88 and https://github.com/Z3Prover/z3/blob/z3-4.13.4/src/ast/ast.cpp#L1330-L1336 These define the basic family IDs, we get them either as a number (e.g. in [assign] lines) or names (e.g. in [eq-expl] th lines). Other family IDs may be defined, which are represented as either Other or Unknown, depending on if we got a name or a number.

Variants

Null

Basic

Label

Pattern

ModelValue

UserSort

Arith

Polymorphic

Other(IString)

Unknown(NonZeroU32)

Implementations

impl TheoryKind

pub fn from_id(id: i32) -> Self

pub fn from_name(name: &str, strings: &mut StringTable) -> Self

Trait Implementations

impl Clone for TheoryKind

fn clone(&self) -> TheoryKind

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for TheoryKind

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Hash for TheoryKind

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for TheoryKind

fn eq(&self, other: &TheoryKind) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for TheoryKind

impl Eq for TheoryKind

impl StructuralPartialEq for TheoryKind