use std::convert::TryInto;
use std::ffi::CStr;
use std::fmt;
use z3_sys::*;
use Context;
use FuncDecl;
use Sort;
use SortDiffers;
use Symbol;
impl<'ctx> Sort<'ctx> {
pub(crate) unsafe fn wrap(ctx: &'ctx Context, z3_sort: Z3_sort) -> Sort<'ctx> {
Z3_inc_ref(ctx.z3_ctx, Z3_sort_to_ast(ctx.z3_ctx, z3_sort));
Sort { ctx, z3_sort }
}
pub fn uninterpreted(ctx: &'ctx Context, name: Symbol) -> Sort<'ctx> {
unsafe {
Self::wrap(
ctx,
Z3_mk_uninterpreted_sort(ctx.z3_ctx, name.as_z3_symbol(ctx)),
)
}
}
pub fn bool(ctx: &'ctx Context) -> Sort<'ctx> {
unsafe { Self::wrap(ctx, Z3_mk_bool_sort(ctx.z3_ctx)) }
}
pub fn int(ctx: &'ctx Context) -> Sort<'ctx> {
unsafe { Self::wrap(ctx, Z3_mk_int_sort(ctx.z3_ctx)) }
}
pub fn real(ctx: &'ctx Context) -> Sort<'ctx> {
unsafe { Self::wrap(ctx, Z3_mk_real_sort(ctx.z3_ctx)) }
}
pub fn float(ctx: &'ctx Context, ebits: u32, sbits: u32) -> Sort<'ctx> {
unsafe { Self::wrap(ctx, Z3_mk_fpa_sort(ctx.z3_ctx, ebits, sbits)) }
}
pub fn float32(ctx: &'ctx Context) -> Sort<'ctx> {
unsafe { Self::wrap(ctx, Z3_mk_fpa_sort(ctx.z3_ctx, 8, 24)) }
}
pub fn double(ctx: &'ctx Context) -> Sort<'ctx> {
unsafe { Self::wrap(ctx, Z3_mk_fpa_sort(ctx.z3_ctx, 11, 53)) }
}
pub fn string(ctx: &'ctx Context) -> Sort<'ctx> {
unsafe { Self::wrap(ctx, Z3_mk_string_sort(ctx.z3_ctx)) }
}
pub fn bitvector(ctx: &'ctx Context, sz: u32) -> Sort<'ctx> {
unsafe { Self::wrap(ctx, Z3_mk_bv_sort(ctx.z3_ctx, sz as ::std::os::raw::c_uint)) }
}
pub fn array(ctx: &'ctx Context, domain: &Sort<'ctx>, range: &Sort<'ctx>) -> Sort<'ctx> {
unsafe {
Self::wrap(
ctx,
Z3_mk_array_sort(ctx.z3_ctx, domain.z3_sort, range.z3_sort),
)
}
}
pub fn set(ctx: &'ctx Context, elt: &Sort<'ctx>) -> Sort<'ctx> {
unsafe { Self::wrap(ctx, Z3_mk_set_sort(ctx.z3_ctx, elt.z3_sort)) }
}
/// Create an enumeration sort.
///
/// Creates a Z3 enumeration sort with the given `name`.
/// The enum variants will have the names in `enum_names`.
/// Three things are returned:
/// - the created `Sort`,
/// - constants to create the variants,
/// - and testers to check if a value is equal to a variant.
///
/// # Examples
/// ```
/// # use z3::{Config, Context, SatResult, Solver, Sort, Symbol};
/// # let cfg = Config::new();
/// # let ctx = Context::new(&cfg);
/// # let solver = Solver::new(&ctx);
/// let (colors, color_consts, color_testers) = Sort::enumeration(
/// &ctx,
/// "Color".into(),
/// &[
/// "Red".into(),
/// "Green".into(),
/// "Blue".into(),
/// ],
/// );
///
/// let red_const = color_consts[0].apply(&[]);
/// let red_tester = &color_testers[0];
/// let eq = red_tester.apply(&[&red_const]);
///
/// assert_eq!(solver.check(), SatResult::Sat);
/// let model = solver.get_model().unwrap();;
///
/// assert!(model.eval(&eq, true).unwrap().as_bool().unwrap().as_bool().unwrap());
/// ```
pub fn enumeration(
ctx: &'ctx Context,
name: Symbol,
enum_names: &[Symbol],
) -> (Sort<'ctx>, Vec<FuncDecl<'ctx>>, Vec<FuncDecl<'ctx>>) {
let enum_names: Vec<_> = enum_names.iter().map(|s| s.as_z3_symbol(ctx)).collect();
let mut enum_consts = vec![std::ptr::null_mut(); enum_names.len()];
let mut enum_testers = vec![std::ptr::null_mut(); enum_names.len()];
let sort = unsafe {
Self::wrap(
ctx,
Z3_mk_enumeration_sort(
ctx.z3_ctx,
name.as_z3_symbol(ctx),
enum_names.len().try_into().unwrap(),
enum_names.as_ptr(),
enum_consts.as_mut_ptr(),
enum_testers.as_mut_ptr(),
),
)
};
// increase ref counts
for i in &enum_consts {
unsafe {
Z3_inc_ref(ctx.z3_ctx, *i as Z3_ast);
}
}
for i in &enum_testers {
unsafe {
Z3_inc_ref(ctx.z3_ctx, *i as Z3_ast);
}
}
// convert to Rust types
let enum_consts: Vec<_> = enum_consts
.iter()
.map(|z3_func_decl| FuncDecl {
ctx,
z3_func_decl: *z3_func_decl,
})
.collect();
let enum_testers: Vec<_> = enum_testers
.iter()
.map(|z3_func_decl| FuncDecl {
ctx,
z3_func_decl: *z3_func_decl,
})
.collect();
(sort, enum_consts, enum_testers)
}
pub fn kind(&self) -> SortKind {
unsafe { Z3_get_sort_kind(self.ctx.z3_ctx, self.z3_sort) }
}
/// Returns `Some(e)` where `e` is the number of exponent bits if the sort
/// is a `FloatingPoint` and `None` otherwise.
pub fn float_exponent_size(&self) -> Option<u32> {
if self.kind() == SortKind::FloatingPoint {
Some(unsafe { Z3_fpa_get_ebits(self.ctx.z3_ctx, self.z3_sort) })
} else {
None
}
}
/// Returns `Some(s)` where `s` is the number of significand bits if the sort
/// is a `FloatingPoint` and `None` otherwise.
pub fn float_significand_size(&self) -> Option<u32> {
if self.kind() == SortKind::FloatingPoint {
Some(unsafe { Z3_fpa_get_sbits(self.ctx.z3_ctx, self.z3_sort) })
} else {
None
}
}
/// Return if this Sort is for an `Array` or a `Set`.
///
/// # Examples
/// ```
/// # use z3::{Config, Context, Sort, ast::Ast, ast::Int, ast::Bool};
/// # let cfg = Config::new();
/// # let ctx = Context::new(&cfg);
/// let bool_sort = Sort::bool(&ctx);
/// let int_sort = Sort::int(&ctx);
/// let array_sort = Sort::array(&ctx, &int_sort, &bool_sort);
/// let set_sort = Sort::set(&ctx, &int_sort);
/// assert!(array_sort.is_array());
/// assert!(set_sort.is_array());
/// assert!(!int_sort.is_array());
/// assert!(!bool_sort.is_array());
/// ```
pub fn is_array(&self) -> bool {
self.kind() == SortKind::Array
}
/// Return the `Sort` of the domain for `Array`s of this `Sort`.
///
/// If this `Sort` is an `Array` or `Set`, it has a domain sort, so return it.
/// If this is not an `Array` or `Set` `Sort`, return `None`.
/// # Examples
/// ```
/// # use z3::{Config, Context, Sort, ast::Ast, ast::Int, ast::Bool};
/// # let cfg = Config::new();
/// # let ctx = Context::new(&cfg);
/// let bool_sort = Sort::bool(&ctx);
/// let int_sort = Sort::int(&ctx);
/// let array_sort = Sort::array(&ctx, &int_sort, &bool_sort);
/// let set_sort = Sort::set(&ctx, &int_sort);
/// assert_eq!(array_sort.array_domain().unwrap(), int_sort);
/// assert_eq!(set_sort.array_domain().unwrap(), int_sort);
/// assert!(int_sort.array_domain().is_none());
/// assert!(bool_sort.array_domain().is_none());
/// ```
pub fn array_domain(&self) -> Option<Sort> {
if self.is_array() {
unsafe {
let domain_sort = Z3_get_array_sort_domain(self.ctx.z3_ctx, self.z3_sort);
if domain_sort.is_null() {
None
} else {
Some(Self::wrap(self.ctx, domain_sort))
}
}
} else {
None
}
}
/// Return the `Sort` of the range for `Array`s of this `Sort`.
///
/// If this `Sort` is an `Array` it has a range sort, so return it.
/// If this `Sort` is a `Set`, it has an implied range sort of `Bool`.
/// If this is not an `Array` or `Set` `Sort`, return `None`.
/// # Examples
/// ```
/// # use z3::{Config, Context, Sort, ast::Ast, ast::Int, ast::Bool};
/// # let cfg = Config::new();
/// # let ctx = Context::new(&cfg);
/// let bool_sort = Sort::bool(&ctx);
/// let int_sort = Sort::int(&ctx);
/// let array_sort = Sort::array(&ctx, &int_sort, &bool_sort);
/// let set_sort = Sort::set(&ctx, &int_sort);
/// assert_eq!(array_sort.array_range().unwrap(), bool_sort);
/// assert_eq!(set_sort.array_range().unwrap(), bool_sort);
/// assert!(int_sort.array_range().is_none());
/// assert!(bool_sort.array_range().is_none());
/// ```
pub fn array_range(&self) -> Option<Sort> {
if self.is_array() {
unsafe {
let range_sort = Z3_get_array_sort_range(self.ctx.z3_ctx, self.z3_sort);
if range_sort.is_null() {
None
} else {
Some(Self::wrap(self.ctx, range_sort))
}
}
} else {
None
}
}
}
impl<'ctx> Clone for Sort<'ctx> {
fn clone(&self) -> Self {
unsafe { Self::wrap(self.ctx, self.z3_sort) }
}
}
impl<'ctx> fmt::Display for Sort<'ctx> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
let p = unsafe { Z3_sort_to_string(self.ctx.z3_ctx, self.z3_sort) };
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 Sort<'ctx> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
<Self as fmt::Display>::fmt(self, f)
}
}
impl<'ctx> PartialEq<Sort<'ctx>> for Sort<'ctx> {
fn eq(&self, other: &Sort<'ctx>) -> bool {
unsafe { Z3_is_eq_sort(self.ctx.z3_ctx, self.z3_sort, other.z3_sort) }
}
}
impl<'ctx> Eq for Sort<'ctx> {}
impl<'ctx> Drop for Sort<'ctx> {
fn drop(&mut self) {
unsafe {
Z3_dec_ref(
self.ctx.z3_ctx,
Z3_sort_to_ast(self.ctx.z3_ctx, self.z3_sort),
);
}
}
}
impl<'ctx> SortDiffers<'ctx> {
pub fn new(left: Sort<'ctx>, right: Sort<'ctx>) -> Self {
Self { left, right }
}
pub fn left(&self) -> &Sort {
&self.left
}
pub fn right(&self) -> &Sort {
&self.right
}
}
impl<'ctx> fmt::Display for SortDiffers<'ctx> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
write!(
f,
"Can not compare nodes, Sort does not match. Nodes contain types {} and {}",
self.left, self.right
)
}
}