Struct ArrayInterpolator 

pub struct ArrayInterpolator;

Array theory interpolator

Trait Implementations

impl Debug for ArrayInterpolator

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for ArrayInterpolator

fn default() -> ArrayInterpolator

Returns the “default value” for a type.

impl TheoryInterpolator for ArrayInterpolator

fn name(&self) -> &'static str

Theory name

fn can_handle(&self, literals: &[&str]) -> bool

Check if this theory can handle the given literals

fn interpolate( &self, a_literals: &[InterpolantTerm], _b_literals: &[InterpolantTerm], _shared_symbols: &FxHashSet<Symbol>, ) -> Option<InterpolantTerm>

Generate theory-specific interpolant