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}