pub struct Simplifier<T: ExprMap<Option<ExprRef>>> { /* private fields */ }Expand description
Performs simplification and canonicalization on expressions and caches the results.
Implementations§
Source§impl<T: ExprMap<Option<ExprRef>>> Simplifier<T>
impl<T: ExprMap<Option<ExprRef>>> Simplifier<T>
pub fn new(cache: T) -> Self
pub fn simplify(&mut self, ctx: &mut Context, e: ExprRef) -> ExprRef
Sourcepub fn verify_simplification(
&self,
ctx: &mut Context,
solver: &mut impl SolverContext,
) -> Result<usize>
pub fn verify_simplification( &self, ctx: &mut Context, solver: &mut impl SolverContext, ) -> Result<usize>
Uses an SMT solver to check all simplification steps that have been made with this Simplifier. Returns the number of incorrect simplifications.
Auto Trait Implementations§
impl<T> Freeze for Simplifier<T>where
T: Freeze,
impl<T> RefUnwindSafe for Simplifier<T>where
T: RefUnwindSafe,
impl<T> Send for Simplifier<T>where
T: Send,
impl<T> Sync for Simplifier<T>where
T: Sync,
impl<T> Unpin for Simplifier<T>where
T: Unpin,
impl<T> UnsafeUnpin for Simplifier<T>where
T: UnsafeUnpin,
impl<T> UnwindSafe for Simplifier<T>where
T: UnwindSafe,
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