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

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>

Loading content...

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

Loading content...

Provided methods

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

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

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

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

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

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

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

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