Trait haybale::backend::BV[−][src]

pub trait BV: Clone + PartialEq + Eq + Debug {
    type SolverRef: SolverRef<BV = Self>;
    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;

    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 { ... }
}

Trait for things which can act like bitvectors.

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

Associated Types

type SolverRef: SolverRef<BV = Self>[src]

Loading content...

Required methods

fn new(solver: Self::SolverRef, width: u32, name: Option<&str>) -> Self[src]

fn from_bool(solver: Self::SolverRef, b: bool) -> Self[src]

fn from_i32(solver: Self::SolverRef, i: i32, width: u32) -> Self[src]

fn from_u32(solver: Self::SolverRef, u: u32, width: u32) -> Self[src]

fn from_i64(solver: Self::SolverRef, i: i64, width: u32) -> Self[src]

fn from_u64(solver: Self::SolverRef, u: u64, width: u32) -> Self[src]

fn zero(solver: Self::SolverRef, width: u32) -> Self[src]

fn one(solver: Self::SolverRef, width: u32) -> Self[src]

fn ones(solver: Self::SolverRef, width: u32) -> Self[src]

fn from_binary_str(solver: Self::SolverRef, bits: &str) -> Self[src]

fn from_dec_str(solver: Self::SolverRef, num: &str, width: u32) -> Self[src]

fn from_hex_str(solver: Self::SolverRef, num: &str, width: u32) -> Self[src]

fn as_binary_str(&self) -> Option<String>[src]

fn as_u64(&self) -> Option<u64>[src]

fn as_bool(&self) -> Option<bool>[src]

fn get_a_solution(&self) -> Result<BVSolution>[src]

fn get_solver(&self) -> Self::SolverRef[src]

fn get_id(&self) -> i32[src]

fn get_width(&self) -> u32[src]

fn get_symbol(&self) -> Option<&str>[src]

fn set_symbol(&mut self, symbol: Option<&str>)[src]

fn is_const(&self) -> bool[src]

fn has_same_width(&self, other: &Self) -> bool[src]

fn assert(&self) -> Result<()>[src]

fn is_failed_assumption(&self) -> bool[src]

fn _eq(&self, other: &Self) -> Self[src]

fn _ne(&self, other: &Self) -> Self[src]

fn add(&self, other: &Self) -> Self[src]

fn sub(&self, other: &Self) -> Self[src]

fn mul(&self, other: &Self) -> Self[src]

fn udiv(&self, other: &Self) -> Self[src]

fn sdiv(&self, other: &Self) -> Self[src]

fn urem(&self, other: &Self) -> Self[src]

fn srem(&self, other: &Self) -> Self[src]

fn smod(&self, other: &Self) -> Self[src]

fn inc(&self) -> Self[src]

fn dec(&self) -> Self[src]

fn neg(&self) -> Self[src]

fn uaddo(&self, other: &Self) -> Self[src]

fn saddo(&self, other: &Self) -> Self[src]

fn usubo(&self, other: &Self) -> Self[src]

fn ssubo(&self, other: &Self) -> Self[src]

fn umulo(&self, other: &Self) -> Self[src]

fn smulo(&self, other: &Self) -> Self[src]

fn sdivo(&self, other: &Self) -> Self[src]

fn not(&self) -> Self[src]

fn and(&self, other: &Self) -> Self[src]

fn or(&self, other: &Self) -> Self[src]

fn xor(&self, other: &Self) -> Self[src]

fn nand(&self, other: &Self) -> Self[src]

fn nor(&self, other: &Self) -> Self[src]

fn xnor(&self, other: &Self) -> Self[src]

fn sll(&self, other: &Self) -> Self[src]

fn srl(&self, other: &Self) -> Self[src]

fn sra(&self, other: &Self) -> Self[src]

fn rol(&self, other: &Self) -> Self[src]

fn ror(&self, other: &Self) -> Self[src]

fn redand(&self) -> Self[src]

fn redor(&self) -> Self[src]

fn redxor(&self) -> Self[src]

fn ugt(&self, other: &Self) -> Self[src]

fn ugte(&self, other: &Self) -> Self[src]

fn sgt(&self, other: &Self) -> Self[src]

fn sgte(&self, other: &Self) -> Self[src]

fn ult(&self, other: &Self) -> Self[src]

fn ulte(&self, other: &Self) -> Self[src]

fn slt(&self, other: &Self) -> Self[src]

fn slte(&self, other: &Self) -> Self[src]

fn zext(&self, i: u32) -> Self[src]

fn sext(&self, i: u32) -> Self[src]

fn slice(&self, high: u32, low: u32) -> Self[src]

fn concat(&self, other: &Self) -> Self[src]

fn repeat(&self, n: u32) -> Self[src]

fn iff(&self, other: &Self) -> Self[src]

fn implies(&self, other: &Self) -> Self[src]

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

Loading content...

Provided methods

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

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).

A default implementation is provided in terms of the other trait methods.

fn sign_extend_to_bits(&self, bits: u32) -> Self[src]

Sign-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).

A default implementation is provided in terms of the other trait methods.

fn uadds(&self, other: &Self) -> Self[src]

Saturating addition, unsigned. The result will be the same as normal addition, except that if the operation would (unsigned) overflow, the maximum value (for that bitwidth) is returned instead.

A default implementation is provided in terms of the other trait methods.

fn sadds(&self, other: &Self) -> Self[src]

Saturating addition, signed. The result will be the same as normal addition, except that if the operation would (signed) overflow for being too positive / too negative, the largest / smallest signed value respectively (for that bitwidth) is returned instead.

A default implementation is provided in terms of the other trait methods.

fn usubs(&self, other: &Self) -> Self[src]

Saturating subtraction, unsigned. The result will be the same as normal subtraction, except that if the operation would overflow (result in a negative number), zero is returned instead.

A default implementation is provided in terms of the other trait methods.

fn ssubs(&self, other: &Self) -> Self[src]

Saturating subtraction, signed. The result will be the same as normal subtraction, except that if the operation would (signed) overflow for being too positive / too negative, the largest / smallest signed value respectively (for that bitwidth) is returned instead.

A default implementation is provided in terms of the other trait methods.

Loading content...

Implementations on Foreign Types

impl BV for BV<Rc<Btor>>[src]

Some prototypical BV and Memory implementations: boolector::BV<Rc<Btor>>, crate::simple_memory::Memory, and crate::cell_memory::Memory

type SolverRef = Rc<Btor>

Loading content...

Implementors

Loading content...