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.

Object Safety

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>