elina/
util.rs

1// Could directly model these types in ast.rs and functions as methods on them,
2// but for the time being this works
3
4use std::ffi::CStr;
5use std::os::raw::c_char;
6use std::ptr::null_mut;
7
8use elina_sys::{elina_lincons0_fprint, elina_lincons0_t, fclose, free, open_memstream};
9
10use crate::ast::{Environment, Manager};
11
12/// This function converts an `elina_lincons0_t` to a `String`.
13///
14/// # Safety
15///
16/// This function necessarily will read from the passed raw pointer, making it unsafe.
17pub unsafe fn lincons0_to_string<M: Manager>(_man: &M, env: &Environment, lincons0: *mut elina_lincons0_t) -> String {
18    let mut buf: *mut c_char = null_mut();
19    let mut len = 0;
20    let fd = open_memstream(&mut buf, &mut len);
21    // to_env_names is okay here, because drop order guarantees it's only dropped after
22    // the function has exited, at which point we don't need to strings anymore
23    let mut env_names = env.to_env_names();
24    elina_lincons0_fprint(fd, lincons0, env_names.as_mut_ptr());
25    fclose(fd);
26    let res = CStr::from_ptr(buf).to_str().unwrap().to_string();
27    free(buf as *mut _);
28    std::mem::drop(env_names);
29    return res;
30    //
31    //
32    // UNFINISHED MANUAL IMPLEMENTATION:
33    //
34    // let linexpr = (*lincons0).linexpr0;
35    // let mut res = linexpr0_to_string(man, env, linexpr);
36    //
37    // match (*lincons0).constyp.into() {
38    //     ConsTyp::SUPEQ => res.push_str(" >= 0"),
39    //     ConsTyp::SUP => res.push_str(" > 0"),
40    //     ConsTyp::EQ => res.push_str(" = 0"),
41    //     ConsTyp::DISEQ => res.push_str(" <> 0"),
42    // }
43    //
44    // res
45}
46
47// // https://adventures.michaelfbryan.com/posts/rust-closures-in-ffi/
48// extern "C" fn each_test(i: size_t, dim: elina_dim_t, coeff: *mut elina_coeff_t) {
49//     println!("foreach called with: {} {} {:?}", i, dim, coeff);
50//
51// }
52//
53// pub fn linexpr0_to_string<M: Manager>(man: &M, env: &Environment, linexpr0: *mut elina_linexpr0_t) -> String {
54//     unsafe {
55//         let fd = open_file(CString::new("temp.txt").unwrap().into_raw());
56//         let env_names = env.to_env_names();
57//         elina_linexpr0_fprint(fd, linexpr0, *env_names);
58//         close_file(fd);
59//
60//         read_to_string("temp.txt").unwrap()
61//         // foreach_linterm_of_linexpr0(linexpr0, Some(each_test))
62//     }
63// }
64