smt_scope/items/
theory.rs

1use core::num::NonZeroU32;
2
3#[cfg(feature = "mem_dbg")]
4use mem_dbg::{MemDbg, MemSize};
5
6use crate::{IString, StringTable};
7
8/// See https://github.com/Z3Prover/z3/blob/z3-4.13.4/src/ast/ast.h#L78-L88 and
9/// https://github.com/Z3Prover/z3/blob/z3-4.13.4/src/ast/ast.cpp#L1330-L1336
10/// These define the basic family IDs, we get them either as a number (e.g. in
11/// `[assign]` lines) or names (e.g. in `[eq-expl] th` lines). Other family IDs
12/// may be defined, which are represented as either `Other` or `Unknown`,
13/// depending on if we got a name or a number.
14#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
15#[cfg_attr(feature = "mem_dbg", copy_type)]
16#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
17pub enum TheoryKind {
18    Null,
19    Basic,
20    Label,
21    Pattern,
22    ModelValue,
23    UserSort,
24    Arith,
25    Polymorphic,
26
27    Other(IString),
28    Unknown(NonZeroU32),
29}
30
31impl TheoryKind {
32    pub fn from_id(id: i32) -> Self {
33        debug_assert!(id >= -1);
34        use TheoryKind::*;
35        match id {
36            -1 => Null,
37            0 => Basic,
38            1 => Label,
39            2 => Pattern,
40            3 => ModelValue,
41            4 => UserSort,
42            5 => Arith,
43            6 => Polymorphic,
44            _ => Unknown(NonZeroU32::new(id as u32).unwrap()),
45        }
46    }
47
48    pub fn from_name(name: &str, strings: &mut StringTable) -> Self {
49        use TheoryKind::*;
50        match name {
51            "null" => Null,
52            "basic" => Basic,
53            "label" => Label,
54            "pattern" => Pattern,
55            "model-value" => ModelValue,
56            "user-sort" => UserSort,
57            "arith" => Arith,
58            "polymorphic" => Polymorphic,
59            _ => Other(IString(strings.get_or_intern(name))),
60        }
61    }
62}
smt_scope/items/theory.rs

smt_scope/items/
theory.rs
