use std::ffi::CStr;
use std::fmt;
use z3_sys::*;
use crate::ast;
use crate::ast::Ast;
use Context;
use Goal;
impl<'ctx> Clone for Goal<'ctx> {
fn clone(&self) -> Self {
Self {
ctx: self.ctx,
z3_goal: self.z3_goal,
}
}
}
impl<'ctx> Goal<'ctx> {
pub(crate) unsafe fn wrap(ctx: &'ctx Context, z3_goal: Z3_goal) -> Goal<'ctx> {
Z3_goal_inc_ref(ctx.z3_ctx, z3_goal);
Goal { ctx, z3_goal }
}
pub fn new(ctx: &'ctx Context, models: bool, unsat_cores: bool, proofs: bool) -> Goal<'ctx> {
unsafe { Self::wrap(ctx, Z3_mk_goal(ctx.z3_ctx, models, unsat_cores, proofs)) }
}
pub fn assert(&self, ast: &impl ast::Ast<'ctx>) {
unsafe { Z3_goal_assert(self.ctx.z3_ctx, self.z3_goal, ast.get_z3_ast()) }
}
pub fn is_inconsistent(&self) -> bool {
unsafe { Z3_goal_inconsistent(self.ctx.z3_ctx, self.z3_goal) }
}
pub fn get_depth(&self) -> u32 {
unsafe { Z3_goal_depth(self.ctx.z3_ctx, self.z3_goal) }
}
pub fn get_size(&self) -> u32 {
unsafe { Z3_goal_size(self.ctx.z3_ctx, self.z3_goal) }
}
pub fn get_num_expr(&self) -> u32 {
unsafe { Z3_goal_num_exprs(self.ctx.z3_ctx, self.z3_goal) }
}
pub fn is_decided_sat(&self) -> bool {
unsafe { Z3_goal_is_decided_sat(self.ctx.z3_ctx, self.z3_goal) }
}
pub fn is_decided_unsat(&self) -> bool {
unsafe { Z3_goal_is_decided_unsat(self.ctx.z3_ctx, self.z3_goal) }
}
pub fn reset(&self) {
unsafe { Z3_goal_reset(self.ctx.z3_ctx, self.z3_goal) };
}
#[allow(clippy::needless_lifetimes)]
pub fn translate<'dest_ctx>(self, ctx: &'dest_ctx Context) -> Goal<'dest_ctx> {
unsafe {
Goal::wrap(
ctx,
Z3_goal_translate(self.ctx.z3_ctx, self.z3_goal, ctx.z3_ctx),
)
}
}
pub fn get_precision(&self) -> GoalPrec {
unsafe { Z3_goal_precision(self.ctx.z3_ctx, self.z3_goal) }
}
pub fn iter_formulas<'a, T>(&'a self) -> impl Iterator<Item = T> + 'a
where
T: Ast<'a>,
{
let goal_size = self.get_size() as usize;
let z3_ctx = self.ctx.z3_ctx;
let z3_goal = self.z3_goal;
(0..goal_size).map(move |i| {
let formula = unsafe { Z3_goal_formula(z3_ctx, z3_goal, i as u32) };
unsafe { T::wrap(self.ctx, formula) }
})
}
pub fn get_formulas<T>(&self) -> Vec<T>
where
T: Ast<'ctx>,
{
let goal_size = self.get_size() as usize;
let mut formulas: Vec<T> = Vec::with_capacity(goal_size);
for i in 0..goal_size {
let formula = unsafe { Z3_goal_formula(self.ctx.z3_ctx, self.z3_goal, i as u32) };
formulas.push(unsafe { T::wrap(self.ctx, formula) });
}
formulas
}
}
impl<'ctx> fmt::Display for Goal<'ctx> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
let p = unsafe { Z3_goal_to_string(self.ctx.z3_ctx, self.z3_goal) };
if p.is_null() {
return Result::Err(fmt::Error);
}
match unsafe { CStr::from_ptr(p) }.to_str() {
Ok(s) => write!(f, "{}", s),
Err(_) => Result::Err(fmt::Error),
}
}
}
impl<'ctx> fmt::Debug for Goal<'ctx> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
<Self as fmt::Display>::fmt(self, f)
}
}
impl<'ctx> Drop for Goal<'ctx> {
fn drop(&mut self) {
unsafe {
Z3_goal_dec_ref(self.ctx.z3_ctx, self.z3_goal);
};
}
}