pub struct EquivEncoder<'a> { /* private fields */ }Expand description
Encoder that handles Bool, Int, BitVec, and Array Z3 expressions for equivalence checking.
Implementations§
Source§impl<'a> EquivEncoder<'a>
impl<'a> EquivEncoder<'a>
Sourcepub fn new(
bool_vars: &'a HashMap<String, Bool>,
int_vars: &'a HashMap<String, Int>,
bv_vars: &'a HashMap<String, BV>,
array_vars: &'a HashMap<String, Array>,
) -> Self
pub fn new( bool_vars: &'a HashMap<String, Bool>, int_vars: &'a HashMap<String, Int>, bv_vars: &'a HashMap<String, BV>, array_vars: &'a HashMap<String, Array>, ) -> Self
Create a full encoder with all variable maps.
Sourcepub fn encode_as_bool(&self, expr: &VerifyExpr) -> Bool
pub fn encode_as_bool(&self, expr: &VerifyExpr) -> Bool
Encode as a Z3 Bool, coercing if necessary.
Auto Trait Implementations§
impl<'a> Freeze for EquivEncoder<'a>
impl<'a> RefUnwindSafe for EquivEncoder<'a>
impl<'a> !Send for EquivEncoder<'a>
impl<'a> !Sync for EquivEncoder<'a>
impl<'a> Unpin for EquivEncoder<'a>
impl<'a> UnsafeUnpin for EquivEncoder<'a>
impl<'a> UnwindSafe for EquivEncoder<'a>
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more