smt_scope/items/
meaning.rs

1#[cfg(feature = "mem_dbg")]
2use mem_dbg::{MemDbg, MemSize};
3
4use crate::{BigRational, BigUint, IString};
5
6#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
7#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
8#[derive(Debug, Clone, PartialEq, Eq, Hash)]
9pub enum Meaning {
10    Arith(Box<BigRational>),
11    BitVec(Box<BitVec>),
12    Unknown {
13        /// The theory in which the value should be interpreted (e.g. `bv`)
14        theory: IString,
15        /// The value of the term (e.g. `#x0000000000000001` or `#b1`)
16        value: IString,
17    },
18}
19
20#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
21#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
22#[derive(Debug, Clone, PartialEq, Eq, Hash)]
23pub struct BitVec {
24    pub value: BigUint,
25    pub bits: u32,
26}