use std::cmp::{Eq, PartialEq};
use std::convert::{TryFrom, TryInto};
use std::ffi::{CStr, CString};
use std::fmt;
use std::hash::{Hash, Hasher};
use z3_sys::*;
use Context;
use Pattern;
use Sort;
use Symbol;
use Z3_MUTEX;
#[cfg(feature = "arbitrary-size-numeral")]
use num::bigint::BigInt;
#[cfg(feature = "arbitrary-size-numeral")]
use num::rational::BigRational;
pub struct Bool<'ctx> {
pub(crate) ctx: &'ctx Context,
pub(crate) z3_ast: Z3_ast,
}
pub struct Int<'ctx> {
pub(crate) ctx: &'ctx Context,
pub(crate) z3_ast: Z3_ast,
}
pub struct Real<'ctx> {
pub(crate) ctx: &'ctx Context,
pub(crate) z3_ast: Z3_ast,
}
pub struct BV<'ctx> {
pub(crate) ctx: &'ctx Context,
pub(crate) z3_ast: Z3_ast,
}
pub struct Array<'ctx> {
pub(crate) ctx: &'ctx Context,
pub(crate) z3_ast: Z3_ast,
}
pub struct Set<'ctx> {
pub(crate) ctx: &'ctx Context,
pub(crate) z3_ast: Z3_ast,
}
pub struct Datatype<'ctx> {
pub(crate) ctx: &'ctx Context,
pub(crate) z3_ast: Z3_ast,
}
pub struct Dynamic<'ctx> {
pub(crate) ctx: &'ctx Context,
pub(crate) z3_ast: Z3_ast,
}
macro_rules! unop {
( $f:ident, $z3fn:ident, $retty:ty ) => {
pub fn $f(&self) -> $retty {
<$retty>::new(self.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
$z3fn(self.ctx.z3_ctx, self.z3_ast)
})
}
};
}
macro_rules! binop {
( $f:ident, $z3fn:ident, $retty:ty ) => {
pub fn $f(&self, other: &Self) -> $retty {
<$retty>::new(self.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
$z3fn(self.ctx.z3_ctx, self.z3_ast, other.z3_ast)
})
}
};
}
macro_rules! varop {
( $f:ident, $z3fn:ident, $retty:ty ) => {
pub fn $f(&self, other: &[&Self]) -> $retty {
<$retty>::new(self.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let mut tmp = vec![self.z3_ast];
for a in other {
tmp.push(a.z3_ast)
}
assert!(tmp.len() <= 0xffff_ffff);
$z3fn(self.ctx.z3_ctx, tmp.len() as u32, tmp.as_ptr())
})
}
};
}
pub trait Ast<'ctx>: Sized + fmt::Debug {
fn get_ctx(&self) -> &'ctx Context;
fn get_z3_ast(&self) -> Z3_ast;
fn new(ctx: &'ctx Context, ast: Z3_ast) -> Self;
fn _eq(&self, other: &Self) -> Bool<'ctx> {
Bool::new(self.get_ctx(), unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_eq(self.get_ctx().z3_ctx, self.get_z3_ast(), other.get_z3_ast())
})
}
fn distinct(&self, other: &[&Self]) -> Bool<'ctx> {
Bool::new(self.get_ctx(), unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let mut tmp = vec![self.get_z3_ast()];
for a in other {
tmp.push(a.get_z3_ast())
}
assert!(tmp.len() <= 0xffff_ffff);
Z3_mk_distinct(self.get_ctx().z3_ctx, tmp.len() as u32, tmp.as_ptr())
})
}
fn get_sort(&self) -> Sort<'ctx> {
Sort::new(self.get_ctx(), unsafe {
Z3_get_sort(self.get_ctx().z3_ctx, self.get_z3_ast())
})
}
fn simplify(&self) -> Self {
Self::new(self.get_ctx(), unsafe {
Z3_simplify(self.get_ctx().z3_ctx, self.get_z3_ast())
})
}
fn substitute<T: Ast<'ctx>>(&self, substitutions: &[(&T, &T)]) -> Self {
Self::new(self.get_ctx(), unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let this_ast = self.get_z3_ast();
let num_exprs = substitutions.len() as ::std::os::raw::c_uint;
let mut froms: Vec<_> = vec![];
let mut tos: Vec<_> = vec![];
for (from_ast, to_ast) in substitutions {
froms.push(from_ast.get_z3_ast());
tos.push(to_ast.get_z3_ast());
}
Z3_substitute(
self.get_ctx().z3_ctx,
this_ast,
num_exprs,
froms.as_ptr(),
tos.as_ptr(),
)
})
}
}
macro_rules! impl_ast {
($ast:ident) => {
impl<'ctx> Ast<'ctx> for $ast<'ctx> {
fn new(ctx: &'ctx Context, ast: Z3_ast) -> Self {
assert!(!ast.is_null());
Self {
ctx,
z3_ast: unsafe {
debug!("new ast {:p}", ast);
let guard = Z3_MUTEX.lock().unwrap();
Z3_inc_ref(ctx.z3_ctx, ast);
ast
},
}
}
fn get_ctx(&self) -> &'ctx Context {
self.ctx
}
fn get_z3_ast(&self) -> Z3_ast {
self.z3_ast
}
}
impl<'ctx> From<$ast<'ctx>> for Z3_ast {
fn from(ast: $ast<'ctx>) -> Self {
ast.z3_ast
}
}
impl<'ctx> PartialEq for $ast<'ctx> {
fn eq(&self, other: &$ast<'ctx>) -> bool {
assert_eq!(self.ctx, other.ctx);
unsafe { Z3_is_eq_ast(self.ctx.z3_ctx, self.z3_ast, other.z3_ast) }
}
}
impl<'ctx> Eq for $ast<'ctx> {}
impl<'ctx> Clone for $ast<'ctx> {
fn clone(&self) -> Self {
debug!("clone ast {:p}", self.z3_ast);
Self::new(self.ctx, self.z3_ast)
}
}
impl<'ctx> Drop for $ast<'ctx> {
fn drop(&mut self) {
debug!("drop ast {:p}", self.z3_ast);
unsafe {
Z3_dec_ref(self.ctx.z3_ctx, self.z3_ast);
}
}
}
impl<'ctx> Hash for $ast<'ctx> {
fn hash<H: Hasher>(&self, state: &mut H) {
unsafe {
let u = Z3_get_ast_hash(self.ctx.z3_ctx, self.z3_ast);
u.hash(state);
}
}
}
impl<'ctx> fmt::Debug for $ast<'ctx> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
let p = unsafe { Z3_ast_to_string(self.ctx.z3_ctx, self.z3_ast) };
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::Display for $ast<'ctx> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
<Self as fmt::Debug>::fmt(self, f)
}
}
};
}
macro_rules! impl_from_try_into_dynamic {
($ast:ident, $as_ast:ident) => {
impl<'ctx> From<$ast<'ctx>> for Dynamic<'ctx> {
fn from(ast: $ast<'ctx>) -> Self {
Dynamic::new(ast.ctx, ast.z3_ast)
}
}
impl<'ctx> TryFrom<Dynamic<'ctx>> for $ast<'ctx> {
type Error = String;
fn try_from(ast: Dynamic<'ctx>) -> Result<Self, String> {
ast.$as_ast()
.ok_or_else(|| format!("Dynamic is not of requested type: {:?}", ast))
}
}
};
}
impl_ast!(Bool);
impl_from_try_into_dynamic!(Bool, as_bool);
impl_ast!(Int);
impl_from_try_into_dynamic!(Int, as_int);
impl_ast!(Real);
impl_from_try_into_dynamic!(Real, as_real);
impl_ast!(BV);
impl_from_try_into_dynamic!(BV, as_bv);
impl_ast!(Array);
impl_from_try_into_dynamic!(Array, as_array);
impl_ast!(Set);
impl<'ctx> From<Set<'ctx>> for Dynamic<'ctx> {
fn from(ast: Set<'ctx>) -> Self {
Dynamic::new(ast.ctx, ast.z3_ast)
}
}
impl<'ctx> Int<'ctx> {
#[cfg(feature = "arbitrary-size-numeral")]
pub fn from_big_int(ctx: &'ctx Context, value: &BigInt) -> Int<'ctx> {
Int::from_str(ctx, &value.to_str_radix(10)).unwrap()
}
pub fn from_str(ctx: &'ctx Context, value: &str) -> Option<Int<'ctx>> {
let sort = Sort::int(ctx);
let ast = unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let int_cstring = CString::new(value).unwrap();
let numeral_ptr = Z3_mk_numeral(ctx.z3_ctx, int_cstring.as_ptr(), sort.z3_sort);
if numeral_ptr.is_null() {
return None;
}
numeral_ptr
};
Some(Int::new(ctx, ast))
}
}
impl<'ctx> Real<'ctx> {
#[cfg(feature = "arbitrary-size-numeral")]
pub fn from_big_rational(ctx: &'ctx Context, value: &BigRational) -> Real<'ctx> {
let num = value.numer();
let den = value.denom();
Real::from_real_str(ctx, &num.to_str_radix(10), &den.to_str_radix(10)).unwrap()
}
pub fn from_real_str(ctx: &'ctx Context, num: &str, den: &str) -> Option<Real<'ctx>> {
let sort = Sort::real(ctx);
let ast = unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let fraction_cstring = CString::new(format!("{:} / {:}", num, den)).unwrap();
let numeral_ptr = Z3_mk_numeral(ctx.z3_ctx, fraction_cstring.as_ptr(), sort.z3_sort);
if numeral_ptr.is_null() {
return None;
}
numeral_ptr
};
Some(Real::new(ctx, ast))
}
}
impl_ast!(Datatype);
impl_from_try_into_dynamic!(Datatype, as_datatype);
impl_ast!(Dynamic);
impl<'ctx> Bool<'ctx> {
pub fn new_const<S: Into<Symbol>>(ctx: &'ctx Context, name: S) -> Bool<'ctx> {
let sort = Sort::bool(ctx);
Self::new(ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_const(ctx.z3_ctx, name.into().as_z3_symbol(ctx), sort.z3_sort)
})
}
pub fn fresh_const(ctx: &'ctx Context, prefix: &str) -> Bool<'ctx> {
let sort = Sort::bool(ctx);
Self::new(ctx, unsafe {
let pp = CString::new(prefix).unwrap();
let p = pp.as_ptr();
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_fresh_const(ctx.z3_ctx, p, sort.z3_sort)
})
}
pub fn from_bool(ctx: &'ctx Context, b: bool) -> Bool<'ctx> {
Self::new(ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
if b {
Z3_mk_true(ctx.z3_ctx)
} else {
Z3_mk_false(ctx.z3_ctx)
}
})
}
pub fn as_bool(&self) -> Option<bool> {
unsafe {
let guard = Z3_MUTEX.lock().unwrap();
match Z3_get_bool_value(self.ctx.z3_ctx, self.z3_ast) {
Z3_L_TRUE => Some(true),
Z3_L_FALSE => Some(false),
_ => None,
}
}
}
pub fn translate<'dest_ctx>(&self, dest: &'dest_ctx Context) -> Bool<'dest_ctx> {
Bool::new(dest, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_translate(self.ctx.z3_ctx, self.z3_ast, dest.z3_ctx)
})
}
pub fn ite<T>(&self, a: &T, b: &T) -> T
where
T: Ast<'ctx>,
{
T::new(self.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_ite(self.ctx.z3_ctx, self.z3_ast, a.get_z3_ast(), b.get_z3_ast())
})
}
varop!(and, Z3_mk_and, Self);
varop!(or, Z3_mk_or, Self);
binop!(xor, Z3_mk_xor, Self);
unop!(not, Z3_mk_not, Self);
binop!(iff, Z3_mk_iff, Self);
binop!(implies, Z3_mk_implies, Self);
pub fn pb_le(&self, other: &[&Bool<'ctx>], coeffs: Vec<i32>, k: i32) -> Bool<'ctx> {
Bool::new(self.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let mut tmp = vec![self.z3_ast];
for a in other {
tmp.push(a.z3_ast)
}
assert!(tmp.len() <= 0xffffffff);
let mut tmp_coeffs = coeffs.clone();
Z3_mk_pble(
self.ctx.z3_ctx,
tmp.len() as u32,
tmp.as_ptr(),
tmp_coeffs.as_mut_ptr(),
k,
)
})
}
pub fn pb_ge(&self, other: &[&Bool<'ctx>], coeffs: Vec<i32>, k: i32) -> Bool<'ctx> {
Bool::new(self.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let mut tmp = vec![self.z3_ast];
for a in other {
tmp.push(a.z3_ast)
}
assert!(tmp.len() <= 0xffffffff);
let mut tmp_coeffs = coeffs.clone();
Z3_mk_pbge(
self.ctx.z3_ctx,
tmp.len() as u32,
tmp.as_ptr(),
tmp_coeffs.as_mut_ptr(),
k,
)
})
}
pub fn pb_eq(&self, other: &[&Bool<'ctx>], coeffs: Vec<i32>, k: i32) -> Bool<'ctx> {
Bool::new(self.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let mut tmp = vec![self.z3_ast];
for a in other {
tmp.push(a.z3_ast)
}
assert!(tmp.len() <= 0xffffffff);
let mut tmp_coeffs = coeffs.clone();
Z3_mk_pbeq(
self.ctx.z3_ctx,
tmp.len() as u32,
tmp.as_ptr(),
tmp_coeffs.as_mut_ptr(),
k,
)
})
}
}
impl<'ctx> Int<'ctx> {
pub fn new_const<S: Into<Symbol>>(ctx: &'ctx Context, name: S) -> Int<'ctx> {
let sort = Sort::int(ctx);
Self::new(ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_const(ctx.z3_ctx, name.into().as_z3_symbol(ctx), sort.z3_sort)
})
}
pub fn fresh_const(ctx: &'ctx Context, prefix: &str) -> Int<'ctx> {
let sort = Sort::int(ctx);
Self::new(ctx, unsafe {
let pp = CString::new(prefix).unwrap();
let p = pp.as_ptr();
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_fresh_const(ctx.z3_ctx, p, sort.z3_sort)
})
}
pub fn from_i64(ctx: &'ctx Context, i: i64) -> Int<'ctx> {
let sort = Sort::int(ctx);
Self::new(ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_int64(ctx.z3_ctx, i, sort.z3_sort)
})
}
pub fn from_u64(ctx: &'ctx Context, u: u64) -> Int<'ctx> {
let sort = Sort::int(ctx);
Self::new(ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_unsigned_int64(ctx.z3_ctx, u, sort.z3_sort)
})
}
pub fn as_i64(&self) -> Option<i64> {
unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let mut tmp: ::std::os::raw::c_longlong = 0;
if Z3_get_numeral_int64(self.ctx.z3_ctx, self.z3_ast, &mut tmp) {
Some(tmp)
} else {
None
}
}
}
pub fn as_u64(&self) -> Option<u64> {
unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let mut tmp: ::std::os::raw::c_ulonglong = 0;
if Z3_get_numeral_uint64(self.ctx.z3_ctx, self.z3_ast, &mut tmp) {
Some(tmp)
} else {
None
}
}
}
pub fn from_real(ast: &Real<'ctx>) -> Int<'ctx> {
Self::new(ast.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_real2int(ast.ctx.z3_ctx, ast.z3_ast)
})
}
pub fn to_real(&self) -> Real<'ctx> {
Real::from_int(self)
}
pub fn from_bv(ast: &BV<'ctx>, signed: bool) -> Int<'ctx> {
Self::new(ast.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_bv2int(ast.ctx.z3_ctx, ast.z3_ast, signed)
})
}
pub fn to_ast(&self, sz: u32) -> BV<'ctx> {
BV::from_int(self, sz)
}
pub fn translate<'dest_ctx>(&self, dest: &'dest_ctx Context) -> Int<'dest_ctx> {
Int::new(dest, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_translate(self.ctx.z3_ctx, self.z3_ast, dest.z3_ctx)
})
}
varop!(add, Z3_mk_add, Self);
varop!(sub, Z3_mk_sub, Self);
varop!(mul, Z3_mk_mul, Self);
binop!(div, Z3_mk_div, Self);
binop!(rem, Z3_mk_rem, Self);
binop!(modulo, Z3_mk_mod, Self);
binop!(power, Z3_mk_power, Self);
unop!(unary_minus, Z3_mk_unary_minus, Self);
binop!(lt, Z3_mk_lt, Bool<'ctx>);
binop!(le, Z3_mk_le, Bool<'ctx>);
binop!(gt, Z3_mk_gt, Bool<'ctx>);
binop!(ge, Z3_mk_ge, Bool<'ctx>);
}
impl<'ctx> Real<'ctx> {
pub fn new_const<S: Into<Symbol>>(ctx: &'ctx Context, name: S) -> Real<'ctx> {
let sort = Sort::real(ctx);
Self::new(ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_const(ctx.z3_ctx, name.into().as_z3_symbol(ctx), sort.z3_sort)
})
}
pub fn fresh_const(ctx: &'ctx Context, prefix: &str) -> Real<'ctx> {
let sort = Sort::real(ctx);
Self::new(ctx, unsafe {
let pp = CString::new(prefix).unwrap();
let p = pp.as_ptr();
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_fresh_const(ctx.z3_ctx, p, sort.z3_sort)
})
}
pub fn from_real(ctx: &'ctx Context, num: i32, den: i32) -> Real<'ctx> {
Self::new(ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_real(
ctx.z3_ctx,
num as ::std::os::raw::c_int,
den as ::std::os::raw::c_int,
)
})
}
pub fn as_real(&self) -> Option<(i64, i64)> {
unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let mut num: i64 = 0;
let mut den: i64 = 0;
if Z3_get_numeral_small(self.ctx.z3_ctx, self.z3_ast, &mut num, &mut den) {
Some((num, den))
} else {
None
}
}
}
pub fn from_int(ast: &Int<'ctx>) -> Real<'ctx> {
Self::new(ast.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_int2real(ast.ctx.z3_ctx, ast.z3_ast)
})
}
pub fn to_int(&self) -> Int<'ctx> {
Int::from_real(self)
}
unop!(is_int, Z3_mk_is_int, Bool<'ctx>);
pub fn translate<'dest_ctx>(&self, dest: &'dest_ctx Context) -> Real<'dest_ctx> {
Real::new(dest, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_translate(self.ctx.z3_ctx, self.z3_ast, dest.z3_ctx)
})
}
varop!(add, Z3_mk_add, Self);
varop!(sub, Z3_mk_sub, Self);
varop!(mul, Z3_mk_mul, Self);
binop!(div, Z3_mk_div, Self);
binop!(power, Z3_mk_power, Self);
unop!(unary_minus, Z3_mk_unary_minus, Self);
binop!(lt, Z3_mk_lt, Bool<'ctx>);
binop!(le, Z3_mk_le, Bool<'ctx>);
binop!(gt, Z3_mk_gt, Bool<'ctx>);
binop!(ge, Z3_mk_ge, Bool<'ctx>);
}
macro_rules! bv_overflow_check_signed {
( $f:ident, $z3fn:ident) => {
pub fn $f(&self, other: &BV<'ctx>, b: bool) -> Bool<'ctx> {
Ast::new(self.ctx, unsafe {
$z3fn(self.ctx.z3_ctx, self.z3_ast, other.z3_ast, b)
})
}
};
}
impl<'ctx> BV<'ctx> {
pub fn new_const<S: Into<Symbol>>(ctx: &'ctx Context, name: S, sz: u32) -> BV<'ctx> {
let sort = Sort::bitvector(ctx, sz);
Self::new(ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_const(ctx.z3_ctx, name.into().as_z3_symbol(ctx), sort.z3_sort)
})
}
pub fn fresh_const(ctx: &'ctx Context, prefix: &str, sz: u32) -> BV<'ctx> {
let sort = Sort::bitvector(ctx, sz);
Self::new(ctx, unsafe {
let pp = CString::new(prefix).unwrap();
let p = pp.as_ptr();
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_fresh_const(ctx.z3_ctx, p, sort.z3_sort)
})
}
pub fn from_i64(ctx: &'ctx Context, i: i64, sz: u32) -> BV<'ctx> {
let sort = Sort::bitvector(ctx, sz);
Self::new(ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_int64(ctx.z3_ctx, i, sort.z3_sort)
})
}
pub fn from_u64(ctx: &'ctx Context, u: u64, sz: u32) -> BV<'ctx> {
let sort = Sort::bitvector(ctx, sz);
Self::new(ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_unsigned_int64(ctx.z3_ctx, u, sort.z3_sort)
})
}
pub fn as_i64(&self) -> Option<i64> {
unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let mut tmp: ::std::os::raw::c_longlong = 0;
if Z3_get_numeral_int64(self.ctx.z3_ctx, self.z3_ast, &mut tmp) {
Some(tmp)
} else {
None
}
}
}
pub fn as_u64(&self) -> Option<u64> {
unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let mut tmp: ::std::os::raw::c_ulonglong = 0;
if Z3_get_numeral_uint64(self.ctx.z3_ctx, self.z3_ast, &mut tmp) {
Some(tmp)
} else {
None
}
}
}
pub fn from_int(ast: &Int<'ctx>, sz: u32) -> BV<'ctx> {
Self::new(ast.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_int2bv(ast.ctx.z3_ctx, sz, ast.z3_ast)
})
}
pub fn to_int(&self, signed: bool) -> Int<'ctx> {
Int::from_bv(self, signed)
}
pub fn get_size(&self) -> u32 {
let sort = self.get_sort();
unsafe { Z3_get_bv_sort_size(self.ctx.z3_ctx, sort.z3_sort) }
}
pub fn translate<'dest_ctx>(&self, dest: &'dest_ctx Context) -> BV<'dest_ctx> {
BV::new(dest, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_translate(self.ctx.z3_ctx, self.z3_ast, dest.z3_ctx)
})
}
unop!(bvnot, Z3_mk_bvnot, Self);
unop!(bvneg, Z3_mk_bvneg, Self);
binop!(bvand, Z3_mk_bvand, Self);
binop!(bvor, Z3_mk_bvor, Self);
binop!(bvxor, Z3_mk_bvxor, Self);
binop!(bvnand, Z3_mk_bvnand, Self);
binop!(bvnor, Z3_mk_bvnor, Self);
binop!(bvxnor, Z3_mk_bvxnor, Self);
unop!(bvredand, Z3_mk_bvredand, Self);
unop!(bvredor, Z3_mk_bvredor, Self);
binop!(bvadd, Z3_mk_bvadd, Self);
binop!(bvsub, Z3_mk_bvsub, Self);
binop!(bvmul, Z3_mk_bvmul, Self);
binop!(bvudiv, Z3_mk_bvudiv, Self);
binop!(bvsdiv, Z3_mk_bvsdiv, Self);
binop!(bvurem, Z3_mk_bvurem, Self);
binop!(bvsrem, Z3_mk_bvsrem, Self);
binop!(bvsmod, Z3_mk_bvsmod, Self);
binop!(bvult, Z3_mk_bvult, Bool<'ctx>);
binop!(bvslt, Z3_mk_bvslt, Bool<'ctx>);
binop!(bvule, Z3_mk_bvule, Bool<'ctx>);
binop!(bvsle, Z3_mk_bvsle, Bool<'ctx>);
binop!(bvuge, Z3_mk_bvuge, Bool<'ctx>);
binop!(bvsge, Z3_mk_bvsge, Bool<'ctx>);
binop!(bvugt, Z3_mk_bvugt, Bool<'ctx>);
binop!(bvsgt, Z3_mk_bvsgt, Bool<'ctx>);
binop!(bvshl, Z3_mk_bvshl, Self);
binop!(bvlshr, Z3_mk_bvlshr, Self);
binop!(bvashr, Z3_mk_bvashr, Self);
binop!(bvrotl, Z3_mk_ext_rotate_left, Self);
binop!(bvrotr, Z3_mk_ext_rotate_left, Self);
binop!(concat, Z3_mk_concat, Self);
bv_overflow_check_signed!(bvadd_no_overflow, Z3_mk_bvadd_no_overflow);
binop!(bvadd_no_underflow, Z3_mk_bvadd_no_underflow, Bool<'ctx>);
binop!(bvsub_no_overflow, Z3_mk_bvsub_no_overflow, Bool<'ctx>);
bv_overflow_check_signed!(bvsub_no_underflow, Z3_mk_bvsub_no_underflow);
binop!(bvsdiv_no_overflow, Z3_mk_bvsdiv_no_overflow, Bool<'ctx>);
unop!(bvneg_no_overflow, Z3_mk_bvneg_no_overflow, Bool<'ctx>);
bv_overflow_check_signed!(bvmul_no_overflow, Z3_mk_bvmul_no_overflow);
binop!(bvmul_no_underflow, Z3_mk_bvmul_no_underflow, Bool<'ctx>);
pub fn extract(&self, high: u32, low: u32) -> Self {
Self::new(self.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_extract(self.ctx.z3_ctx, high, low, self.z3_ast)
})
}
pub fn sign_ext(&self, i: u32) -> Self {
Self::new(self.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_sign_ext(self.ctx.z3_ctx, i, self.z3_ast)
})
}
pub fn zero_ext(&self, i: u32) -> Self {
Self::new(self.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_zero_ext(self.ctx.z3_ctx, i, self.z3_ast)
})
}
}
impl<'ctx> Array<'ctx> {
pub fn new_const<S: Into<Symbol>>(
ctx: &'ctx Context,
name: S,
domain: &Sort<'ctx>,
range: &Sort<'ctx>,
) -> Array<'ctx> {
let sort = Sort::array(ctx, domain, range);
Self::new(ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_const(ctx.z3_ctx, name.into().as_z3_symbol(ctx), sort.z3_sort)
})
}
pub fn fresh_const(
ctx: &'ctx Context,
prefix: &str,
domain: &Sort<'ctx>,
range: &Sort<'ctx>,
) -> Array<'ctx> {
let sort = Sort::array(ctx, domain, range);
Self::new(ctx, unsafe {
let pp = CString::new(prefix).unwrap();
let p = pp.as_ptr();
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_fresh_const(ctx.z3_ctx, p, sort.z3_sort)
})
}
pub fn const_array(
ctx: &'ctx Context,
domain: &Sort<'ctx>,
val: &Dynamic<'ctx>,
) -> Array<'ctx> {
Self::new(ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_const_array(ctx.z3_ctx, domain.z3_sort, val.z3_ast)
})
}
pub fn translate<'dest_ctx>(&self, dest: &'dest_ctx Context) -> Array<'dest_ctx> {
Array::new(dest, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_translate(self.ctx.z3_ctx, self.z3_ast, dest.z3_ctx)
})
}
pub fn select(&self, index: &Dynamic<'ctx>) -> Dynamic<'ctx> {
Dynamic::new(self.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_select(self.ctx.z3_ctx, self.z3_ast, index.get_z3_ast())
})
}
pub fn store(&self, index: &Dynamic<'ctx>, value: &Dynamic<'ctx>) -> Self {
Self::new(self.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_store(
self.ctx.z3_ctx,
self.z3_ast,
index.get_z3_ast(),
value.get_z3_ast(),
)
})
}
}
impl<'ctx> Set<'ctx> {
pub fn new_const<S: Into<Symbol>>(
ctx: &'ctx Context,
name: S,
eltype: &Sort<'ctx>,
) -> Set<'ctx> {
let sort = Sort::set(ctx, eltype);
Self::new(ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_const(ctx.z3_ctx, name.into().as_z3_symbol(ctx), sort.z3_sort)
})
}
pub fn fresh_const(ctx: &'ctx Context, prefix: &str, eltype: &Sort<'ctx>) -> Set<'ctx> {
let sort = Sort::set(ctx, eltype);
Self::new(ctx, unsafe {
let pp = CString::new(prefix).unwrap();
let p = pp.as_ptr();
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_fresh_const(ctx.z3_ctx, p, sort.z3_sort)
})
}
pub fn translate<'dest_ctx>(&self, dest: &'dest_ctx Context) -> Set<'dest_ctx> {
Set::new(dest, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_translate(self.ctx.z3_ctx, self.z3_ast, dest.z3_ctx)
})
}
pub fn add(&self, element: &Dynamic<'ctx>) -> Set<'ctx> {
Set::new(self.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_set_add(self.ctx.z3_ctx, self.z3_ast, element.get_z3_ast())
})
}
pub fn del(&self, element: &Dynamic<'ctx>) -> Set<'ctx> {
Set::new(self.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_set_add(self.ctx.z3_ctx, self.z3_ast, element.get_z3_ast())
})
}
pub fn member(&self, element: &Dynamic<'ctx>) -> Bool<'ctx> {
Bool::new(self.ctx, unsafe {
let guard = Z3_MUTEX.lock().unwrap();
Z3_mk_set_add(self.ctx.z3_ctx, self.z3_ast, element.get_z3_ast())
})
}
varop!(intersect, Z3_mk_set_intersect, Self);
varop!(set_union, Z3_mk_set_union, Self);
binop!(set_subset, Z3_mk_set_subset, Bool<'ctx>);
unop!(complement, Z3_mk_set_complement, Self);
binop!(difference, Z3_mk_set_difference, Self);
}
impl<'ctx> Dynamic<'ctx> {
pub fn from_ast(ast: &impl Ast<'ctx>) -> Self {
Self::new(ast.get_ctx(), ast.get_z3_ast())
}
fn sort_kind(&self) -> SortKind {
unsafe { Z3_get_sort_kind(self.ctx.z3_ctx, Z3_get_sort(self.ctx.z3_ctx, self.z3_ast)) }
}
pub fn as_bool(&self) -> Option<Bool<'ctx>> {
match self.sort_kind() {
SortKind::Bool => Some(Bool::new(self.ctx, self.z3_ast)),
_ => None,
}
}
pub fn as_int(&self) -> Option<Int<'ctx>> {
match self.sort_kind() {
SortKind::Int => Some(Int::new(self.ctx, self.z3_ast)),
_ => None,
}
}
pub fn as_real(&self) -> Option<Real<'ctx>> {
match self.sort_kind() {
SortKind::Real => Some(Real::new(self.ctx, self.z3_ast)),
_ => None,
}
}
pub fn as_bv(&self) -> Option<BV<'ctx>> {
match self.sort_kind() {
SortKind::BV => Some(BV::new(self.ctx, self.z3_ast)),
_ => None,
}
}
pub fn as_array(&self) -> Option<Array<'ctx>> {
match self.sort_kind() {
SortKind::Array => Some(Array::new(self.ctx, self.z3_ast)),
_ => None,
}
}
pub fn as_datatype(&self) -> Option<Datatype<'ctx>> {
match self.sort_kind() {
SortKind::Datatype => Some(Datatype::new(self.ctx, self.z3_ast)),
_ => None,
}
}
}
impl<'ctx> Datatype<'ctx> {
pub fn new_const<S: Into<Symbol>>(ctx: &'ctx Context, name: S, sort: &Sort<'ctx>) -> Self {
assert_eq!(ctx, sort.ctx);
assert_eq!(sort.kind(), SortKind::Datatype);
Self::new(ctx, unsafe {
Z3_mk_const(ctx.z3_ctx, name.into().as_z3_symbol(ctx), sort.z3_sort)
})
}
pub fn fresh_const(ctx: &'ctx Context, prefix: &str, sort: &Sort<'ctx>) -> Self {
assert_eq!(ctx, sort.ctx);
assert_eq!(sort.kind(), SortKind::Datatype);
Self::new(ctx, unsafe {
let pp = CString::new(prefix).unwrap();
let p = pp.as_ptr();
Z3_mk_fresh_const(ctx.z3_ctx, p, sort.z3_sort)
})
}
pub fn translate<'dest_ctx>(&self, dest: &'dest_ctx Context) -> Datatype<'dest_ctx> {
Datatype::new(dest, unsafe {
Z3_translate(self.ctx.z3_ctx, self.z3_ast, dest.z3_ctx)
})
}
}
pub fn forall_const<'ctx>(
ctx: &'ctx Context,
bounds: &[&Dynamic<'ctx>],
patterns: &[&Pattern<'ctx>],
body: &Dynamic<'ctx>,
) -> Dynamic<'ctx> {
assert!(bounds.iter().all(|a| a.get_ctx() == ctx));
assert!(patterns.iter().all(|p| p.ctx == ctx));
assert_eq!(ctx, body.get_ctx());
if bounds.is_empty() {
return body.clone();
}
let bounds: Vec<_> = bounds.iter().map(|a| a.get_z3_ast()).collect();
let patterns: Vec<_> = patterns.iter().map(|p| p.z3_pattern).collect();
Ast::new(ctx, unsafe {
Z3_mk_forall_const(
ctx.z3_ctx,
0,
bounds.len().try_into().unwrap(),
bounds.as_ptr() as *const Z3_app,
patterns.len().try_into().unwrap(),
patterns.as_ptr() as *const Z3_pattern,
body.get_z3_ast(),
)
})
}
pub fn exists_const<'ctx>(
ctx: &'ctx Context,
bounds: &[&Dynamic<'ctx>],
patterns: &[&Pattern<'ctx>],
body: &Dynamic<'ctx>,
) -> Dynamic<'ctx> {
assert!(bounds.iter().all(|a| a.get_ctx() == ctx));
assert!(patterns.iter().all(|p| p.ctx == ctx));
assert_eq!(ctx, body.get_ctx());
let bounds: Vec<_> = bounds.iter().map(|a| a.get_z3_ast()).collect();
let patterns: Vec<_> = patterns.iter().map(|p| p.z3_pattern).collect();
Ast::new(ctx, unsafe {
Z3_mk_exists_const(
ctx.z3_ctx,
0,
bounds.len().try_into().unwrap(),
bounds.as_ptr() as *const Z3_app,
patterns.len().try_into().unwrap(),
patterns.as_ptr() as *const Z3_pattern,
body.get_z3_ast(),
)
})
}