Skip to main content

z3/
symbol.rs

1use std::ffi::CString;
2use z3_sys::*;
3
4use crate::{Context, Symbol};
5
6impl Symbol {
7    pub fn as_z3_symbol(&self) -> Z3_symbol {
8        let ctx = &Context::thread_local();
9        match self {
10            Symbol::Int(i) => unsafe {
11                Z3_mk_int_symbol(ctx.z3_ctx.0, *i as ::std::os::raw::c_int).unwrap()
12            },
13            Symbol::String(s) => {
14                let ss = CString::new(s.clone()).unwrap();
15                let p = ss.as_ptr();
16                unsafe { Z3_mk_string_symbol(ctx.z3_ctx.0, p).unwrap() }
17            }
18        }
19    }
20}
21
22impl From<u32> for Symbol {
23    fn from(val: u32) -> Self {
24        Symbol::Int(val)
25    }
26}
27
28impl From<i32> for Symbol {
29    fn from(val: i32) -> Self {
30        Symbol::Int(val as u32)
31    }
32}
33
34impl From<String> for Symbol {
35    fn from(val: String) -> Self {
36        Symbol::String(val)
37    }
38}
39
40impl From<&str> for Symbol {
41    fn from(val: &str) -> Self {
42        Symbol::String(val.to_owned())
43    }
44}