use crate::node::{Array, BV};
use crate::option::BtorOption;
use crate::option::*;
use crate::timeout::{self, TimeoutState};
use boolector_sys::*;
use std::borrow::Borrow;
use std::ffi::{CStr, CString};
use std::fmt;
use std::os::raw::{c_char, c_void};
use std::pin::Pin;
pub struct Btor {
btor: *mut boolector_sys::Btor,
pub(crate) timeout_state: Pin<Box<timeout::TimeoutState>>, }
impl PartialEq for Btor {
fn eq(&self, other: &Self) -> bool {
self.btor == other.btor
}
}
impl Eq for Btor {}
impl fmt::Debug for Btor {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "<btor {:?}>", self.btor)
}
}
unsafe impl Send for Btor {}
unsafe impl Sync for Btor {}
impl Btor {
pub fn new() -> Self {
Self {
btor: unsafe { boolector_new() },
timeout_state: Pin::new(Box::new(timeout::TimeoutState::new())),
}
}
pub(crate) fn as_raw(&self) -> *mut boolector_sys::Btor {
self.btor
}
#[allow(clippy::cognitive_complexity)]
pub fn set_opt(&self, opt: BtorOption) {
match opt {
BtorOption::ModelGen(mg) => {
let val = match mg {
ModelGen::Disabled => 0,
ModelGen::Asserted => 1,
ModelGen::All => 2,
};
unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_MODEL_GEN, val) }
},
BtorOption::Incremental(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_INCREMENTAL, if b { 1 } else { 0 })
},
BtorOption::IncrementalSMT1(ismt1) => {
let val = match ismt1 {
IncrementalSMT1::Basic => BTOR_INCREMENTAL_SMT1_BASIC,
IncrementalSMT1::Continue => BTOR_INCREMENTAL_SMT1_CONTINUE,
};
unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_INCREMENTAL_SMT1, val) }
},
BtorOption::InputFileFormat(iff) => {
let val = match iff {
InputFileFormat::Autodetect => BTOR_INPUT_FORMAT_NONE,
InputFileFormat::Btor => BTOR_INPUT_FORMAT_BTOR,
InputFileFormat::Btor2 => BTOR_INPUT_FORMAT_BTOR2,
InputFileFormat::SMTLIBv1 => BTOR_INPUT_FORMAT_SMT1,
InputFileFormat::SMTLIBv2 => BTOR_INPUT_FORMAT_SMT2,
};
unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_INPUT_FORMAT, val) }
},
BtorOption::OutputNumberFormat(nf) => {
let val = match nf {
NumberFormat::Binary => BTOR_OUTPUT_BASE_BIN,
NumberFormat::Decimal => BTOR_OUTPUT_BASE_DEC,
NumberFormat::Hexadecimal => BTOR_OUTPUT_BASE_HEX,
};
unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_OUTPUT_NUMBER_FORMAT, val) }
},
BtorOption::OutputFileFormat(off) => {
let val = match off {
OutputFileFormat::BTOR => BTOR_OUTPUT_FORMAT_BTOR,
OutputFileFormat::SMTLIBv2 => BTOR_OUTPUT_FORMAT_SMT2,
OutputFileFormat::AigerASCII => BTOR_OUTPUT_FORMAT_AIGER_ASCII,
OutputFileFormat::AigerBinary => BTOR_OUTPUT_FORMAT_AIGER_BINARY,
};
unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_OUTPUT_FORMAT, val) }
},
BtorOption::SolverTimeout(duration) => {
self.timeout_state.set_timeout_duration(duration);
match duration {
None => {
unsafe { boolector_set_term(self.as_raw(), None, std::ptr::null_mut()) }
},
Some(_) => {
let ptr_to_ts: Pin<&TimeoutState> = (&self.timeout_state).as_ref();
let raw_ptr_to_ts: *const TimeoutState =
Pin::into_inner(ptr_to_ts) as *const TimeoutState;
let void_ptr_to_ts: *mut c_void = raw_ptr_to_ts as *mut c_void;
unsafe {
boolector_set_term(
self.as_raw(),
Some(timeout::callback),
void_ptr_to_ts,
)
}
},
}
},
BtorOption::SolverEngine(se) => {
let val = match se {
SolverEngine::Fun => BTOR_ENGINE_FUN,
SolverEngine::SLS => BTOR_ENGINE_SLS,
SolverEngine::Prop => BTOR_ENGINE_PROP,
SolverEngine::AIGProp => BTOR_ENGINE_AIGPROP,
SolverEngine::Quant => BTOR_ENGINE_QUANT,
};
unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_ENGINE, val) }
},
BtorOption::SatEngine(se) => {
let val = match se {
SatEngine::CaDiCaL => BTOR_SAT_ENGINE_CADICAL,
SatEngine::CMS => BTOR_SAT_ENGINE_CMS,
SatEngine::Lingeling => BTOR_SAT_ENGINE_LINGELING,
SatEngine::MiniSAT => BTOR_SAT_ENGINE_MINISAT,
SatEngine::PicoSAT => BTOR_SAT_ENGINE_PICOSAT,
};
unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_SAT_ENGINE, val) }
},
BtorOption::AutoCleanup(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_AUTO_CLEANUP, if b { 1 } else { 0 })
},
BtorOption::PrettyPrint(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_PRETTY_PRINT, if b { 1 } else { 0 })
},
BtorOption::Seed(u) => unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_SEED, u) },
BtorOption::RewriteLevel(rl) => {
let val = match rl {
RewriteLevel::None => 0,
RewriteLevel::TermLevel => 1,
RewriteLevel::More => 2,
RewriteLevel::Full => 3,
};
unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_REWRITE_LEVEL, val) }
},
BtorOption::SkeletonPreproc(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_SKELETON_PREPROC,
if b { 1 } else { 0 },
)
},
BtorOption::Ackermann(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_ACKERMANN, if b { 1 } else { 0 })
},
BtorOption::BetaReduce(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_BETA_REDUCE, if b { 1 } else { 0 })
},
BtorOption::EliminateSlices(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_ELIMINATE_SLICES,
if b { 1 } else { 0 },
)
},
BtorOption::VariableSubst(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_VAR_SUBST, if b { 1 } else { 0 })
},
BtorOption::UnconstrainedOpt(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_UCOPT, if b { 1 } else { 0 })
},
BtorOption::MergeLambdas(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_MERGE_LAMBDAS, if b { 1 } else { 0 })
},
BtorOption::ExtractLambdas(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_EXTRACT_LAMBDAS,
if b { 1 } else { 0 },
)
},
BtorOption::Normalize(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_NORMALIZE, if b { 1 } else { 0 })
},
BtorOption::NormalizeAdd(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_NORMALIZE_ADD, if b { 1 } else { 0 })
},
BtorOption::FunPreProp(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_FUN_PREPROP, if b { 1 } else { 0 })
},
BtorOption::FunPreSLS(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_FUN_PRESLS, if b { 1 } else { 0 })
},
BtorOption::FunDualProp(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_FUN_DUAL_PROP, if b { 1 } else { 0 })
},
BtorOption::FunDualPropQsortOrder(dpqo) => {
let val = match dpqo {
DualPropQsortOrder::Just => BTOR_DP_QSORT_JUST,
DualPropQsortOrder::Asc => BTOR_DP_QSORT_ASC,
DualPropQsortOrder::Desc => BTOR_DP_QSORT_DESC,
};
unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_FUN_DUAL_PROP_QSORT, val) }
},
BtorOption::FunJustification(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_FUN_JUST, if b { 1 } else { 0 })
},
BtorOption::FunJustificationHeuristic(jh) => {
let val = match jh {
JustificationHeuristic::Left => BTOR_JUST_HEUR_BRANCH_LEFT,
JustificationHeuristic::MinApp => BTOR_JUST_HEUR_BRANCH_MIN_APP,
JustificationHeuristic::MinDepth => BTOR_JUST_HEUR_BRANCH_MIN_DEP,
};
unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_FUN_JUST_HEURISTIC, val) }
},
BtorOption::FunLazySynthesize(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_FUN_LAZY_SYNTHESIZE,
if b { 1 } else { 0 },
)
},
BtorOption::FunEagerLemmas(el) => {
let val = match el {
EagerLemmas::None => BTOR_FUN_EAGER_LEMMAS_NONE,
EagerLemmas::Conf => BTOR_FUN_EAGER_LEMMAS_CONF,
EagerLemmas::All => BTOR_FUN_EAGER_LEMMAS_ALL,
};
unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_FUN_EAGER_LEMMAS, val) }
},
BtorOption::SLSNumFlips(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_NFLIPS, u)
},
BtorOption::SLSMoveStrategy(sms) => {
let val = match sms {
SLSMoveStrategy::BestMove => 0,
SLSMoveStrategy::RandomWalk => 1,
SLSMoveStrategy::FirstBestMove => 2,
SLSMoveStrategy::BestSameMove => 3,
SLSMoveStrategy::AlwaysProp => 4,
};
unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_STRATEGY, val) }
},
BtorOption::SLSJustification(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_JUST, if b { 1 } else { 0 })
},
BtorOption::SLSGroupWiseMoves(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_MOVE_GW, if b { 1 } else { 0 })
},
BtorOption::SLSRangeWiseMoves(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_SLS_MOVE_RANGE,
if b { 1 } else { 0 },
)
},
BtorOption::SLSSegmentWiseMoves(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_SLS_MOVE_SEGMENT,
if b { 1 } else { 0 },
)
},
BtorOption::SLSRandomWalkMoves(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_SLS_MOVE_RAND_WALK,
if b { 1 } else { 0 },
)
},
BtorOption::SLSRandomWalkProbability(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_PROB_MOVE_RAND_WALK, u)
},
BtorOption::SLSRandomizeAll(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_SLS_MOVE_RAND_ALL,
if b { 1 } else { 0 },
)
},
BtorOption::SLSRandomizeRange(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_SLS_MOVE_RAND_RANGE,
if b { 1 } else { 0 },
)
},
BtorOption::SLSPropagationMoves(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_MOVE_PROP, if b { 1 } else { 0 })
},
BtorOption::SLSPropagationMovesNumProp(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_MOVE_PROP_N_PROP, u)
},
BtorOption::SLSPropagationMovesNumRegular(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_MOVE_PROP_N_SLS, u)
},
BtorOption::SLSForceRandomWalks(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_SLS_MOVE_PROP_FORCE_RW,
if b { 1 } else { 0 },
)
},
BtorOption::SLSIncMoveTest(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_SLS_MOVE_INC_MOVE_TEST,
if b { 1 } else { 0 },
)
},
BtorOption::SLSRestarts(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_SLS_USE_RESTARTS,
if b { 1 } else { 0 },
)
},
BtorOption::SLSBanditScheme(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_SLS_USE_BANDIT,
if b { 1 } else { 0 },
)
},
BtorOption::PropNumSteps(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_NPROPS, u)
},
BtorOption::PropRestarts(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_PROP_USE_RESTARTS,
if b { 1 } else { 0 },
)
},
BtorOption::PropBanditScheme(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_PROP_USE_BANDIT,
if b { 1 } else { 0 },
)
},
BtorOption::PropPathSelectionMode(pathsel) => {
let val = match pathsel {
PropPathSelection::Controlling => BTOR_PROP_PATH_SEL_CONTROLLING,
PropPathSelection::Essential => BTOR_PROP_PATH_SEL_ESSENTIAL,
PropPathSelection::Random => BTOR_PROP_PATH_SEL_RANDOM,
};
unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PATH_SEL, val) }
},
BtorOption::PropInvValueProbability(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_USE_INV_VALUE, u)
},
BtorOption::PropFlipConditionProbability(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_FLIP_COND, u)
},
BtorOption::PropFlipConditionProbabilityConstant(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_FLIP_COND_CONST, u)
},
BtorOption::PropFlipConditionNumPaths(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_FLIP_COND_CONST_NPATHSEL, u)
},
BtorOption::PropFlipConditionProbabilityConstantDelta(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_FLIP_COND_CONST_DELTA, u)
},
BtorOption::PropSliceKeepDCProbability(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_SLICE_KEEP_DC, u)
},
BtorOption::PropConcatFlipProbability(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_CONC_FLIP, u)
},
BtorOption::PropSliceFlipProbability(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_SLICE_FLIP, u)
},
BtorOption::PropEqFlipProbability(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_EQ_FLIP, u)
},
BtorOption::PropAndFlipProbability(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_AND_FLIP, u)
},
BtorOption::AIGPropUseRestarts(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_AIGPROP_USE_RESTARTS,
if b { 1 } else { 0 },
)
},
BtorOption::AIGPropQuantSynthesis(pqs) => {
let val = match pqs {
AIGPropQuantSynthesis::None => BTOR_QUANT_SYNTH_NONE,
AIGPropQuantSynthesis::EL => BTOR_QUANT_SYNTH_EL,
AIGPropQuantSynthesis::ELMC => BTOR_QUANT_SYNTH_ELMC,
AIGPropQuantSynthesis::ELELMC => BTOR_QUANT_SYNTH_EL_ELMC,
AIGPropQuantSynthesis::ELMR => BTOR_QUANT_SYNTH_ELMR,
};
unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_QUANT_SYNTH, val) }
},
BtorOption::AIGPropQuantDualSolver(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_QUANT_DUAL_SOLVER,
if b { 1 } else { 0 },
)
},
BtorOption::AIGPropQuantSynthLimit(u) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_QUANT_SYNTH_LIMIT, u)
},
BtorOption::AIGPropSynthQI(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_QUANT_SYNTH_QI,
if b { 1 } else { 0 },
)
},
BtorOption::AIGPropQuantDER(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_QUANT_DER, if b { 1 } else { 0 })
},
BtorOption::AIGPropQuantCER(b) => unsafe {
boolector_set_opt(self.as_raw(), BTOR_OPT_QUANT_CER, if b { 1 } else { 0 })
},
BtorOption::AIGPropQuantMiniscope(b) => unsafe {
boolector_set_opt(
self.as_raw(),
BTOR_OPT_QUANT_MINISCOPE,
if b { 1 } else { 0 },
)
},
}
}
pub fn sat(&self) -> SolverResult {
self.timeout_state.restart_timer();
#[allow(non_upper_case_globals)]
match unsafe { boolector_sat(self.as_raw()) } as u32 {
BtorSolverResult_BTOR_RESULT_SAT => SolverResult::Sat,
BtorSolverResult_BTOR_RESULT_UNSAT => SolverResult::Unsat,
BtorSolverResult_BTOR_RESULT_UNKNOWN => SolverResult::Unknown,
u => panic!("Unexpected return value from boolector_sat(): {}", u),
}
}
pub fn push(&self, n: u32) {
unsafe { boolector_push(self.as_raw(), n) }
}
pub fn pop(&self, n: u32) {
unsafe { boolector_pop(self.as_raw(), n) }
}
pub fn duplicate(&self) -> Self {
let duplicated = Self {
btor: unsafe { boolector_clone(self.as_raw()) },
timeout_state: Pin::new(Box::new(TimeoutState::with_timeout_duration(
self.timeout_state.get_timeout_duration(),
))),
};
let ptr_to_ts: Pin<&TimeoutState> = (&self.timeout_state).as_ref();
let raw_ptr_to_ts: *const TimeoutState = Pin::into_inner(ptr_to_ts) as *const TimeoutState;
let void_ptr_to_ts: *mut c_void = raw_ptr_to_ts as *mut c_void;
unsafe { boolector_set_term(self.as_raw(), Some(timeout::callback), void_ptr_to_ts) }
duplicated
}
#[allow(clippy::if_same_then_else)]
pub fn get_matching_bv<R: Borrow<Btor> + Clone>(btor: R, bv: &BV<R>) -> Option<BV<R>> {
let node = unsafe { boolector_match_node(btor.borrow().as_raw(), bv.node) };
if node.is_null() {
None
} else if unsafe { boolector_is_array(btor.borrow().as_raw(), node) } {
None
} else {
Some(BV { btor, node })
}
}
pub fn get_matching_array<R: Borrow<Btor> + Clone>(
btor: R,
array: &Array<R>,
) -> Option<Array<R>> {
let node = unsafe { boolector_match_node(btor.borrow().as_raw(), array.node) };
if node.is_null() {
None
} else if unsafe { boolector_is_array(btor.borrow().as_raw(), node) } {
Some(Array { btor, node })
} else {
None
}
}
#[allow(clippy::if_same_then_else)]
pub fn get_bv_by_symbol<R: Borrow<Btor> + Clone>(btor: R, symbol: &str) -> Option<BV<R>> {
let cstring = CString::new(symbol).unwrap();
let symbol = cstring.as_ptr() as *const c_char;
let node = unsafe { boolector_match_node_by_symbol(btor.borrow().as_raw(), symbol) };
if node.is_null() {
None
} else if unsafe { boolector_is_array(btor.borrow().as_raw(), node) } {
None
} else {
Some(BV { btor, node })
}
}
pub fn get_array_by_symbol<R: Borrow<Btor> + Clone>(btor: R, symbol: &str) -> Option<Array<R>> {
let cstring = CString::new(symbol).unwrap();
let symbol = cstring.as_ptr() as *const c_char;
let node = unsafe { boolector_match_node_by_symbol(btor.borrow().as_raw(), symbol) };
if node.is_null() {
None
} else if unsafe { boolector_is_array(btor.borrow().as_raw(), node) } {
Some(Array { btor, node })
} else {
None
}
}
pub fn fixate_assumptions(&self) {
unsafe { boolector_fixate_assumptions(self.as_raw()) }
}
pub fn reset_assumptions(&self) {
unsafe { boolector_reset_assumptions(self.as_raw()) }
}
pub fn reset_stats(&self) {
unsafe { boolector_reset_stats(self.as_raw()) }
}
pub fn reset_time(&self) {
unsafe { boolector_reset_time(self.as_raw()) }
}
pub fn print_constraints(&self) -> String {
unsafe {
let tmpfile: *mut libc::FILE = libc::tmpfile();
if tmpfile.is_null() {
panic!("Failed to create a temp file");
}
boolector_dump_smt2(self.as_raw(), tmpfile);
assert_eq!(libc::fseek(tmpfile, 0, libc::SEEK_END), 0);
let length = libc::ftell(tmpfile);
if length < 0 {
panic!("ftell() returned a negative value");
}
assert_eq!(libc::fseek(tmpfile, 0, libc::SEEK_SET), 0);
let mut buffer = Vec::with_capacity(length as usize);
libc::fread(
buffer.as_mut_ptr() as *mut c_void,
1,
length as usize,
tmpfile,
);
libc::fclose(tmpfile);
buffer.set_len(length as usize);
String::from_utf8_unchecked(buffer)
}
}
pub fn print_model(&self) -> String {
unsafe {
let tmpfile: *mut libc::FILE = libc::tmpfile();
if tmpfile.is_null() {
panic!("Failed to create a temp file");
}
let format_cstring = CString::new("btor").unwrap();
boolector_print_model(
self.as_raw(),
format_cstring.as_ptr() as *mut c_char,
tmpfile,
);
assert_eq!(libc::fseek(tmpfile, 0, libc::SEEK_END), 0);
let length = libc::ftell(tmpfile);
if length < 0 {
panic!("ftell() returned a negative value");
}
assert_eq!(libc::fseek(tmpfile, 0, libc::SEEK_SET), 0);
let mut buffer = Vec::with_capacity(length as usize);
libc::fread(
buffer.as_mut_ptr() as *mut c_void,
1,
length as usize,
tmpfile,
);
libc::fclose(tmpfile);
buffer.set_len(length as usize);
String::from_utf8_unchecked(buffer)
}
}
pub fn get_version(&self) -> String {
let cstr = unsafe { CStr::from_ptr(boolector_version(self.as_raw())) };
cstr.to_str().unwrap().to_owned()
}
pub fn get_copyright(&self) -> String {
let cstr = unsafe { CStr::from_ptr(boolector_copyright(self.as_raw())) };
cstr.to_str().unwrap().to_owned()
}
}
impl Default for Btor {
fn default() -> Self {
Self::new()
}
}
impl Drop for Btor {
fn drop(&mut self) {
unsafe {
boolector_release_all(self.as_raw());
assert_eq!(boolector_get_refs(self.as_raw()) as i32, 0);
boolector_delete(self.as_raw());
}
}
}
#[derive(PartialEq, Eq, Clone, Copy, Debug)]
pub enum SolverResult {
Sat,
Unsat,
Unknown,
}