Trait haybale::backend::BV

source ·

pub trait BV: Clone + PartialEq + Eq + Debug {
    type SolverRef: SolverRef<BV = Self>;

Show 82 methods    // Required methods
    fn new(solver: Self::SolverRef, width: u32, name: Option<&str>) -> Self;
    fn from_bool(solver: Self::SolverRef, b: bool) -> Self;
    fn from_i32(solver: Self::SolverRef, i: i32, width: u32) -> Self;
    fn from_u32(solver: Self::SolverRef, u: u32, width: u32) -> Self;
    fn from_i64(solver: Self::SolverRef, i: i64, width: u32) -> Self;
    fn from_u64(solver: Self::SolverRef, u: u64, width: u32) -> Self;
    fn zero(solver: Self::SolverRef, width: u32) -> Self;
    fn one(solver: Self::SolverRef, width: u32) -> Self;
    fn ones(solver: Self::SolverRef, width: u32) -> Self;
    fn from_binary_str(solver: Self::SolverRef, bits: &str) -> Self;
    fn from_dec_str(solver: Self::SolverRef, num: &str, width: u32) -> Self;
    fn from_hex_str(solver: Self::SolverRef, num: &str, width: u32) -> Self;
    fn as_binary_str(&self) -> Option<String>;
    fn as_u64(&self) -> Option<u64>;
    fn as_bool(&self) -> Option<bool>;
    fn get_a_solution(&self) -> Result<BVSolution>;
    fn get_solver(&self) -> Self::SolverRef;
    fn get_id(&self) -> i32;
    fn get_width(&self) -> u32;
    fn get_symbol(&self) -> Option<&str>;
    fn set_symbol(&mut self, symbol: Option<&str>);
    fn is_const(&self) -> bool;
    fn has_same_width(&self, other: &Self) -> bool;
    fn assert(&self) -> Result<()>;
    fn is_failed_assumption(&self) -> bool;
    fn _eq(&self, other: &Self) -> Self;
    fn _ne(&self, other: &Self) -> Self;
    fn add(&self, other: &Self) -> Self;
    fn sub(&self, other: &Self) -> Self;
    fn mul(&self, other: &Self) -> Self;
    fn udiv(&self, other: &Self) -> Self;
    fn sdiv(&self, other: &Self) -> Self;
    fn urem(&self, other: &Self) -> Self;
    fn srem(&self, other: &Self) -> Self;
    fn smod(&self, other: &Self) -> Self;
    fn inc(&self) -> Self;
    fn dec(&self) -> Self;
    fn neg(&self) -> Self;
    fn uaddo(&self, other: &Self) -> Self;
    fn saddo(&self, other: &Self) -> Self;
    fn usubo(&self, other: &Self) -> Self;
    fn ssubo(&self, other: &Self) -> Self;
    fn umulo(&self, other: &Self) -> Self;
    fn smulo(&self, other: &Self) -> Self;
    fn sdivo(&self, other: &Self) -> Self;
    fn not(&self) -> Self;
    fn and(&self, other: &Self) -> Self;
    fn or(&self, other: &Self) -> Self;
    fn xor(&self, other: &Self) -> Self;
    fn nand(&self, other: &Self) -> Self;
    fn nor(&self, other: &Self) -> Self;
    fn xnor(&self, other: &Self) -> Self;
    fn sll(&self, other: &Self) -> Self;
    fn srl(&self, other: &Self) -> Self;
    fn sra(&self, other: &Self) -> Self;
    fn rol(&self, other: &Self) -> Self;
    fn ror(&self, other: &Self) -> Self;
    fn redand(&self) -> Self;
    fn redor(&self) -> Self;
    fn redxor(&self) -> Self;
    fn ugt(&self, other: &Self) -> Self;
    fn ugte(&self, other: &Self) -> Self;
    fn sgt(&self, other: &Self) -> Self;
    fn sgte(&self, other: &Self) -> Self;
    fn ult(&self, other: &Self) -> Self;
    fn ulte(&self, other: &Self) -> Self;
    fn slt(&self, other: &Self) -> Self;
    fn slte(&self, other: &Self) -> Self;
    fn zext(&self, i: u32) -> Self;
    fn sext(&self, i: u32) -> Self;
    fn slice(&self, high: u32, low: u32) -> Self;
    fn concat(&self, other: &Self) -> Self;
    fn repeat(&self, n: u32) -> Self;
    fn iff(&self, other: &Self) -> Self;
    fn implies(&self, other: &Self) -> Self;
    fn cond_bv(&self, truebv: &Self, falsebv: &Self) -> Self;

    // Provided methods
    fn zero_extend_to_bits(&self, bits: u32) -> Self { ... }
    fn sign_extend_to_bits(&self, bits: u32) -> Self { ... }
    fn uadds(&self, other: &Self) -> Self { ... }
    fn sadds(&self, other: &Self) -> Self { ... }
    fn usubs(&self, other: &Self) -> Self { ... }
    fn ssubs(&self, other: &Self) -> Self { ... }
}

Expand description

Trait for things which can act like bitvectors.

These methods mirror the methods available on boolector::BV; detailed docs are available there.

Required Associated Types§

source

type SolverRef: SolverRef<BV = Self>

Required Methods§

source

fn cond_bv(&self, truebv: &Self, falsebv: &Self) -> Self

Provided Methods§

source

fn zero_extend_to_bits(&self, bits: u32) -> Self

Zero-extend a BV to the specified number of bits. The input BV can be already the desired size (in which case this function is a no-op) or smaller (in which case this function will extend), but not larger (in which case this function will panic).