Struct CachedSolver

pub struct CachedSolver<'ctx, S: SmtSolver<'ctx>, C: SolverCache> { /* private fields */ }

A solver that uses caching.

Implementations

impl<'ctx, S: SmtSolver<'ctx>, C: SolverCache> CachedSolver<'ctx, S, C>

pub fn new(inner: S, cache: C) -> Self

Creates a new CachedSolver.

The CachedSolver first checks cache if there is a cached assertion result. If there is not, it invokes inner to solve the assertions.

Trait Implementations

impl<'ctx, S: SmtSolver<'ctx>, C: SolverCache> Debug for CachedSolver<'ctx, S, C>

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

Formats the value using the given formatter.

impl<'ctx, S: SmtSolver<'ctx> + 'ctx, C: SolverCache> SmtBV<'ctx, CachedSolver<'ctx, S, C>> for CacheBV<'ctx, S>

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

Returns true if both expressions are structurally identical.

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 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 bvrotr(self, count: Self) -> Self

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

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

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

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

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

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

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

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

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

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.

fn get_size(&self) -> u32

Returns the size of the bitvector.

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, S: SmtSolver<'ctx> + 'ctx, C: SolverCache> SmtBVArray<'ctx, CachedSolver<'ctx, S, C>> for CacheBVArray<'ctx, S>

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

Returns true if both expressions are structurally identical.

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

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

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.

fn select( self, index: <CachedSolver<'ctx, S, C> as SmtSolver<'ctx>>::BV, ) -> <CachedSolver<'ctx, S, C> as SmtSolver<'ctx>>::BV

Returns the value at the provided index in the array.

fn store( self, index: <CachedSolver<'ctx, S, C> as SmtSolver<'ctx>>::BV, value: <CachedSolver<'ctx, S, C> as SmtSolver<'ctx>>::BV, ) -> 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, S: SmtSolver<'ctx> + 'ctx, C: SolverCache> SmtBool<'ctx, CachedSolver<'ctx, S, C>> for CacheBool<'ctx, S>

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

Returns true if both expressions are structurally identical.

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

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

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.

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

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

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

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

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

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

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

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

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

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

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, S: SmtSolver<'ctx> + 'ctx, C: SolverCache> SmtInt<'ctx, CachedSolver<'ctx, S, C>> for CacheInt<'ctx, S>

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

Returns true if both expressions are structurally identical.

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

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

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 into_dynamic(self) -> Dynamic<'a, S>

Converts the integer into a Dynamic expression.

impl<'ctx, S: SmtSolver<'ctx> + 'ctx, C: SolverCache> SmtModel<'ctx, CachedSolver<'ctx, S, C>> for CacheModel<'ctx, S>

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

Obtain the value for a constant in the model.

impl<'r, 'ctx, S: SmtSolver<'ctx> + 'r + 'ctx, C: SolverCache> SmtModelRef<'ctx, CachedSolver<'ctx, S, C>> for CacheModelRef<'r, 'ctx, S>

fn to_model(&self) -> Option<CacheModel<'ctx, S>>

Convert the reference into an owned model.

impl<'ctx, S: SmtSolver<'ctx> + 'ctx, C: SolverCache> SmtSolver<'ctx> for CachedSolver<'ctx, S, C>

type BV = CacheBV<'ctx, S>

Bitvector expressions

type Int = CacheInt<'ctx, S>

Integer expressions

type Bool = CacheBool<'ctx, S>

Boolean expressions

type BvArray = CacheBVArray<'ctx, S>

Bitvector array expressions

type ModelRef<'r> = CacheModelRef<'r, 'ctx, S> where Self: 'r, S: 'r

References to models for satisfied assertions.

type Model = CacheModel<'ctx, S>

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 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 new_bool_const(&mut self, name: impl AsRef<str>) -> Self::Bool

Declares a new boolean constant.

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

Creates an int from an i64.

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

Creates an int from an u64.

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

Creates an int from a bitvector.

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

Creates an SMT bool from a Rust bool.

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

Creates a forall condition.

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

Runs the SMT solver on the provided assertions.

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.