[−][src]Enum boolector::option::AIGPropQuantSynthesis
Variants
Do not synthesize skolem functions (use model values for instantiation)
Use enumerative learning to synthesize skolem functions
Use enumerative learning modulo the predicates in the cone of influence of the existential variables to synthesize skolem functions
Chain the EL and ELMC approaches to synthesize skolem functions
Use enumerative learning modulo the given root constraints to synthesize skolem functions
Auto Trait Implementations
impl RefUnwindSafe for AIGPropQuantSynthesis[src]
impl Send for AIGPropQuantSynthesis[src]
impl Sync for AIGPropQuantSynthesis[src]
impl Unpin for AIGPropQuantSynthesis[src]
impl UnwindSafe for AIGPropQuantSynthesis[src]
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized, [src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized, [src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized, [src]
T: ?Sized,
pub fn borrow_mut(&mut self) -> &mut T[src]
impl<T> From<T> for T[src]
impl<T, U> Into<U> for T where
U: From<T>, [src]
U: From<T>,
impl<T, U> TryFrom<U> for T where
U: Into<T>, [src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
pub fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>, [src]
U: TryFrom<T>,