Enum boolector::option::AIGPropQuantSynthesis
source · [−]pub enum AIGPropQuantSynthesis {
None,
EL,
ELMC,
ELELMC,
ELMR,
}
Variants
None
Do not synthesize skolem functions (use model values for instantiation)
EL
Use enumerative learning to synthesize skolem functions
ELMC
Use enumerative learning modulo the predicates in the cone of influence of the existential variables to synthesize skolem functions
ELELMC
Chain the EL
and ELMC
approaches to synthesize skolem functions
ELMR
Use enumerative learning modulo the given root constraints to synthesize skolem functions
Auto Trait Implementations
impl RefUnwindSafe for AIGPropQuantSynthesis
impl Send for AIGPropQuantSynthesis
impl Sync for AIGPropQuantSynthesis
impl Unpin for AIGPropQuantSynthesis
impl UnwindSafe for AIGPropQuantSynthesis
Blanket Implementations
sourceimpl<T> BorrowMut<T> for T where
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more