Struct Z3Solver

pub struct Z3Solver<'ctx> { /* private fields */ }

The Z3 SmtSolver.

Implementations

impl<'ctx> Z3Solver<'ctx>

pub fn new(context: &'ctx Context) -> Self

Creates a new Z3Solver from the provided context.

pub fn context(&self) -> &'ctx Context

Returns the [z3::Context] wrapped by this struct.

pub fn solver(&self) -> &Solver<'ctx>

Returns the [z3::Solver] wrapped by this struct.

impl Z3Solver<'static>

pub fn with_thread_local<T>( timeout: Duration, f: impl FnOnce(Z3Solver<'_>) -> T, ) -> T

Creates a new thread-local Z3Solver.

Trait Implementations

impl<'ctx> Clone for Z3Solver<'ctx>

fn clone(&self) -> Z3Solver<'ctx>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'ctx> Debug for Z3Solver<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'ctx> SmtBV<'ctx, Z3Solver<'ctx>> for BV<'ctx>

fn concat(self, other: Self) -> Self

fn extract(self, hi: u32, lo: u32) -> Self

fn zero_ext(self, num: u32) -> Self

fn sign_ext(self, num: u32) -> Self

fn bvshl(self, count: Self) -> Self

fn bvlshr(self, count: Self) -> Self

fn bvashr(self, count: Self) -> Self

fn get_size(&self) -> u32

Returns the size of the bitvector.

fn _eq(self, other: Self) -> Bool<'ctx>

Returns an SMT expression that performs an equality comparison between the two bitvectors.

fn bvurem(self, n: Self) -> Self

fn bvsrem(self, n: Self) -> Self

fn bvudiv(self, n: Self) -> Self

fn bvsdiv(self, n: Self) -> Self

fn bvrotl(self, count: Self) -> Self

fn bvslt(self, other: Self) -> Bool<'ctx>

fn bvsge(self, other: Self) -> Bool<'ctx>

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.

fn bvrotr(self, count: Self) -> Self

fn is_identical(&self, other: &Self) -> bool

Returns true if both expressions are structurally identical.

fn bvsgt(self, other: Self) -> Bool<'ctx>

fn bvugt(self, other: Self) -> Bool<'ctx>

fn bvult(self, other: Self) -> Bool<'ctx>

fn bvule(self, other: Self) -> Bool<'ctx>

fn bvuge(self, other: Self) -> Bool<'ctx>

fn as_u64(&self) -> Option<u64>

Converts the bitvector to an u64, if possible.

fn into_dynamic(self) -> Dynamic<'a, S>

Converts the bitvector into a Dynamic expression.

fn swap_bytes(self, num_bytes: usize) -> Self

Swaps the lowest num_bytes in the bitvector.

fn swap_bytes_to_128bits(self, num_bytes: usize) -> Self

Swaps the lowest num_bytes in the bitvector, and zero-extends to an 128-bit bitvector.

impl<'ctx> SmtBVArray<'ctx, Z3Solver<'ctx>> for BvArray<'ctx>

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.

fn _eq(self, other: Self) -> Bool<'ctx>

Returns an SMT expression that performs an equality comparison between the two bools.

fn is_identical(&self, other: &Self) -> bool

Returns true if both expressions are structurally identical.

fn select(self, index: BV<'ctx>) -> BV<'ctx>

Returns the value at the provided index in the array.

fn store(self, index: BV<'ctx>, value: BV<'ctx>) -> Self

Returns an updated array that contains value at index index.

fn element_size(&self) -> u32

Returns the size of the bitvector elements in the array.

fn index_size(&self) -> u32

Returns the size of the bitvector indices in the array.

fn into_dynamic(self) -> Dynamic<'a, S>

Converts the bool into a Dynamic expression.

impl<'ctx> SmtBool<'ctx, Z3Solver<'ctx>> for Bool<'ctx>

fn ite_bv(self, lhs: BV<'ctx>, rhs: BV<'ctx>) -> BV<'ctx>

Creates an If-Then-Else expression that returns bitvectors.

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.

fn _eq(self, other: Self) -> Bool<'ctx>

Returns an SMT expression that performs an equality comparison between the two bools.

fn as_bool(&self) -> Option<bool>

Converts the SMT boolean expression to a bool, if possible.

fn ite_int(self, lhs: Int<'ctx>, rhs: Int<'ctx>) -> Int<'ctx>

Creates an If-Then-Else expression that returns integers.

fn ite_bool(self, lhs: Bool<'ctx>, rhs: Bool<'ctx>) -> Bool<'ctx>

Creates an If-Then-Else expression that returns booleans.

fn ite_bv_array(self, lhs: BvArray<'ctx>, rhs: BvArray<'ctx>) -> BvArray<'ctx>

Creates an If-Then-Else expression that returns bitvector arrays.

fn is_identical(&self, other: &Self) -> bool

Returns true if both expressions are structurally identical.

fn ite_dynamic(self, lhs: Dynamic<'a, S>, rhs: Dynamic<'a, S>) -> Dynamic<'a, S>

Creates an If-Then-Else expression that returns Dynamics.

fn into_dynamic(self) -> Dynamic<'a, S>

Converts the bool into a Dynamic expression.

impl<'ctx> SmtInt<'ctx, Z3Solver<'ctx>> for Int<'ctx>

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.

fn as_u64(&self) -> Option<u64>

Converts the integer to an u64, if possible.

fn _eq(self, other: Self) -> Bool<'ctx>

Returns an SMT expression that performs an equality comparison between the two ints.

fn is_identical(&self, other: &Self) -> bool

Returns true if both expressions are structurally identical.

fn into_dynamic(self) -> Dynamic<'a, S>

Converts the integer into a Dynamic expression.

impl<'ctx> SmtModel<'ctx, Z3Solver<'ctx>> for Model<'ctx>

fn get_const_interp(&self, name: &BV<'ctx>) -> Option<BV<'ctx>>

Obtain the value for a constant in the model.

impl<'ctx> SmtModelRef<'ctx, Z3Solver<'ctx>> for ModelRef<'_, 'ctx>

fn to_model(&self) -> Option<Model<'ctx>>

Convert the reference into an owned model.

impl<'ctx> SmtSolver<'ctx> for Z3Solver<'ctx>

type BV = BV<'ctx>

Bitvector expressions

type Int = Int<'ctx>

Integer expressions

type Bool = Bool<'ctx>

Boolean expressions

type BvArray = BvArray<'ctx>

Bitvector array expressions

type ModelRef<'a> = ModelRef<'a, 'ctx> where Self: 'a

References to models for satisfied assertions.

type Model = Model<'ctx>

Models for satisfied assertions.

fn bv_from_i64(&mut self, val: i64, size: u32) -> Self::BV

Creates a bitvector from an i64.

fn bv_from_u64(&mut self, val: u64, size: u32) -> Self::BV

Creates a bitvector from an u64.

fn int_from_i64(&mut self, val: i64) -> Self::Int

Creates an int from an i64.

fn int_from_bv(&mut self, bv: Self::BV, signed: bool) -> Self::Int

Creates an int from a bitvector.

fn bv_from_int(&mut self, int: Self::Int, size: u32) -> Self::BV

Creates a bitvector from an Int.

fn new_bv_const(&mut self, name: impl AsRef<str>, size: u32) -> Self::BV

Declares a new bitvector constant.

fn check_assertions( &mut self, assertions: &[Self::Bool], ) -> SatResult<Self::ModelRef<'_>>

Runs the SMT solver on the provided assertions.

fn bool_from_bool(&mut self, val: bool) -> Self::Bool

Creates an SMT bool from a Rust bool.

fn int_from_u64(&mut self, val: u64) -> Self::Int

Creates an int from an u64.

fn forall_const( &mut self, vals: &[Dynamic<'ctx, Self>], condition: Self::Bool, ) -> Self::Bool

Creates a forall condition.

fn new_bool_const(&mut self, name: impl AsRef<str>) -> Self::Bool

Declares a new boolean constant.

fn new_bv_array_const( &mut self, name: impl AsRef<str>, index_size: u32, element_size: u32, ) -> Self::BvArray

Declare a new bitvector array constant.

fn bv_from_i128(&mut self, value: i128) -> Self::BV

Creates a bitvector from an i128.

fn extract_bits<const N: u32>( &mut self, src: Self::BV, mask: Self::BV, ) -> Self::BV

The PEXT operation.

fn popcount(&mut self, bv: &Self::BV, bv_size: u32) -> Self::Int

Counts the number of ones in bv.

fn deposit_bits<const N: u32>( &mut self, src: Self::BV, mask: Self::BV, ) -> Self::BV

The PDEP operation.

fn count_trailing_zeros(&mut self, bv: Self::BV) -> Self::BV

Count the number of trailing zeros in bv.

fn count_leading_zeros(&mut self, bv: Self::BV) -> Self::BV

Count the number of leading zeros in bv.