Struct Z3CodeGen

pub struct Z3CodeGen<'a, 'ctx, S: SmtSolver<'ctx>> { /* private fields */ }

A code generator that generates Z3 expressions.

Implementations

impl<'a, 'ctx, S: SmtSolver<'ctx>> Z3CodeGen<'a, 'ctx, S>

pub fn new(context: &'a mut S, args: Vec<S::BV>) -> Self

Creates a new SMT code generator for the provided SmtSolver and arguments.

pub fn new_with_terms(context: &'a mut S, args: Vec<Term<S::BV>>) -> Self

Creates a new SMT code generator for the provided SmtSolver and arguments.

Trait Implementations

impl<'ctx, S: SmtSolver<'ctx>> CodeGenerator for Z3CodeGen<'_, 'ctx, S>

type T = Z3Expr<'ctx, S>

An expression in the generated code.

fn leaf_const(&mut self, value: i128) -> Self::T

Create a constant value.

fn leaf_arg(&mut self, arg_index: usize) -> Term<Self::T>

Create a value that loads the argument.

fn or(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Compute the bitwise OR.

fn not(&mut self, item: Self::T) -> Self::T

Negate the expression.

fn and(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Compute the bitwise AND.

fn xor(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Compute the bitwise XOR.

fn crop(&mut self, num_bits: u8, item: Self::T) -> Self::T

Crop the expression to the lowest num_bits bits.

fn shl(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Shift lhs left by rhs positions.

fn shr(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Shift lhs right by rhs positions.

fn rol(&mut self, num_bits: u8, lhs: Self::T, rhs: Self::T) -> Self::T

Crop lhs to num_bits, then rotate those bits rhs positions.

fn select(&mut self, num_skip: u8, num_take: u8, item: Self::T) -> Self::T

Select num_take bits starting at bit index num_skip from item.

fn sign_extend(&mut self, num_bits: u8, item: Self::T) -> Self::T

Crop the expression to the lowest num_bits bits, then sign-extend it.

fn parity(&mut self, item: Self::T) -> Self::T

Crop the expression to the lowest 8 bits, then compute the parity.

fn add(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Add two values.

fn sub(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Subtract rhs from lhs.

fn is_zero(&mut self, item: Self::T) -> Self::T

Return ‘1’ if the expression is zero, otherwise return ‘0’.

fn if_zero( &mut self, condition: Self::T, if_zero: Self::T, if_nonzero: Self::T, ) -> Self::T

If condition is zero, return if_zero. Otherwise, return if_nonzero.

fn cmp_lt(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Return ‘1’ if lhs is less than rhs, return ‘1’ otherwise.

fn unknown_op_any(&mut self, name: &str, _args: &[Self::T]) -> Self::T

Generate an error for an unknown operation.

fn byte_mask(&mut self, item: Self::T) -> Self::T

Return the byte mask for the expression.

fn bit_mask(&mut self, item: Self::T) -> Self::T

Return a bit mask for the given number of bits.

fn trailing_zeros(&mut self, item: Self::T) -> Self::T

Count the number of trailing zeros.

fn leading_zeros(&mut self, item: Self::T) -> Self::T

Count the number of leading zeros.

fn swap_bytes(&mut self, num_bits: u8, item: Self::T) -> Self::T

Reverse the order of the lowest ceil(num_bits / 8) bytes.

fn mul(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Multiply two values.

fn div(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Perform signed division.

fn div_unsigned(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Perform unsigned division.

fn rem(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Compute the signed remainder.

fn rem_unsigned(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Compute the unsigned remainder.

fn deposit_bits(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Perform the PDEP operation.

fn extract_bits(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Perform the PEXT operation

fn popcount(&mut self, item: Self::T) -> Self::T

Count the number of ones.

fn carryless_mul(&mut self, lhs: Self::T, rhs: Self::T) -> Self::T

Perform carryless multiplication.

fn simplify(&mut self, item: Self::T) -> Self::T

Simplify the expression, if possible.

fn unknown_op1(&mut self, name: &str, item: Self::T) -> Self::T

Generate an error for a 1-argument unknown operation.

fn unknown_op2(&mut self, name: &str, lhs: Self::T, rhs: Self::T) -> Self::T

Generate an error for a 2-argument unknown operation.

fn unknown_op3( &mut self, name: &str, arg0: Self::T, arg1: Self::T, arg2: Self::T, ) -> Self::T

Generate an error for a 3-argument unknown operation.