Trait SmtSolver

pub trait SmtSolver<'a>: Sized + Debug {
    type BV: SmtBV<'a, Self>;
    type Int: SmtInt<'a, Self>;
    type Bool: SmtBool<'a, Self>;
    type BvArray: SmtBVArray<'a, Self>;
    type ModelRef<'r>: SmtModelRef<'a, Self>
       where Self: 'r;
    type Model: SmtModel<'a, Self>;

    // Required methods
    fn bv_from_i64(&mut self, val: i64, size: u32) -> Self::BV;
    fn bv_from_u64(&mut self, val: u64, size: u32) -> Self::BV;
    fn bv_from_int(&mut self, int: Self::Int, size: u32) -> Self::BV;
    fn new_bv_const(&mut self, name: impl AsRef<str>, size: u32) -> Self::BV;
    fn new_bool_const(&mut self, name: impl AsRef<str>) -> Self::Bool;
    fn new_bv_array_const(
        &mut self,
        name: impl AsRef<str>,
        index_size: u32,
        element_size: u32,
    ) -> Self::BvArray;
    fn int_from_i64(&mut self, val: i64) -> Self::Int;
    fn int_from_u64(&mut self, val: u64) -> Self::Int;
    fn int_from_bv(&mut self, bv: Self::BV, signed: bool) -> Self::Int;
    fn bool_from_bool(&mut self, val: bool) -> Self::Bool;
    fn forall_const(
        &mut self,
        vals: &[Dynamic<'a, Self>],
        condition: Self::Bool,
    ) -> Self::Bool;
    fn check_assertions<'me>(
        &'me mut self,
        assertions: &[Self::Bool],
    ) -> SatResult<Self::ModelRef<'me>>;

    // Provided methods
    fn bv_from_i128(&mut self, value: i128) -> Self::BV { ... }
    fn extract_bits<const N: u32>(
        &mut self,
        src: Self::BV,
        mask: Self::BV,
    ) -> Self::BV { ... }
    fn popcount(&mut self, bv: &Self::BV, bv_size: u32) -> Self::Int { ... }
    fn deposit_bits<const N: u32>(
        &mut self,
        src: Self::BV,
        mask: Self::BV,
    ) -> Self::BV { ... }
    fn count_trailing_zeros(&mut self, bv: Self::BV) -> Self::BV { ... }
    fn count_leading_zeros(&mut self, bv: Self::BV) -> Self::BV { ... }
}

An SMT solver.

Required Associated Types

type BV: SmtBV<'a, Self>

Bitvector expressions

type Int: SmtInt<'a, Self>

Integer expressions

type Bool: SmtBool<'a, Self>

Boolean expressions

type BvArray: SmtBVArray<'a, Self>

Bitvector array expressions

type ModelRef<'r>: SmtModelRef<'a, Self> where Self: 'r

References to models for satisfied assertions.

type Model: SmtModel<'a, Self>

Models for satisfied assertions.

Required Methods

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 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 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<'a, 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.

Provided Methods

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.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

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

type BV = BV<'ctx>

type Int = Int<'ctx>

type Bool = Bool<'ctx>

type BvArray = BvArray<'ctx>

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

type Model = Model<'ctx>

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

type BV = CacheBV<'ctx, S>

type Int = CacheInt<'ctx, S>

type Bool = CacheBool<'ctx, S>

type BvArray = CacheBVArray<'ctx, S>

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

type Model = CacheModel<'ctx, S>