How to use `FILE` type?

[fatemender]

How to use `FILE` type?

[fatemender]

No reason, I just didn't have enough time to tweak the generated bindings. I would be happy to accept a PR for that! Otherwise, I think I might get back to that issue someday but not sure when.

[fatemender]

Hi,

it is not possible (or at least portable) to use std::fs::File and *mut FILE interchangeably, see this thread on Reddit. However you should be able to cast between *mut boolector_sys::FILE and *mut libc::FILE and use the libc crate functions. I currently can't check this, though, will try to make a working example in a few hours.

Hope that helps.

[cdisselkoen]

Great, that does help! I'll look at casting to libc::FILE. Thanks for the quick response!

[fatemender]

Just in case, here is a quick-and-dirty example.

use std::ffi::CString;
use std::ptr;

use boolector_sys as bs;
use libc;

fn main() {
    unsafe {
        let btor = bs::boolector_new();
        bs::boolector_set_opt(btor, bs::BtorOption_BTOR_OPT_MODEL_GEN, 1);
        let b8 = bs::boolector_bitvec_sort(btor, 8);
        let x = bs::boolector_var(btor, b8, ptr::null());
        let y = bs::boolector_var(btor, b8, ptr::null());
        let s56 = CString::new("56").unwrap();
        let c56 = bs::boolector_constd(btor, b8, s56.as_ptr());
        let mul = bs::boolector_mul(btor, x, y);
        let equ = bs::boolector_eq(btor, mul, c56);
        let filename = CString::new("output.txt").unwrap();
        let mode = CString::new("w").unwrap();
        let outfile = libc::fopen(filename.as_ptr(), mode.as_ptr());
        bs::boolector_assert(btor, equ);
        bs::boolector_dump_smt2(btor, outfile as _);
        assert_eq!(bs::boolector_sat(btor), bs::BtorSolverResult_BTOR_RESULT_SAT as _);
        let smt2 = CString::new("smt2").unwrap();
        bs::boolector_print_model(btor, smt2.as_ptr() as _, outfile as _);
        libc::fclose(outfile);
        bs::boolector_delete(btor);
    }
}

[cdisselkoen]

Great, thanks!

[cdisselkoen]

Actually, just curious - is there a reason that boolector-sys couldn't just use the libc::FILE type directly? Is there a benefit to having its own FILE type?