Struct TreeInterpolator 

pub struct TreeInterpolator { /* private fields */ }

Tree interpolation for hierarchical formulas

Given a tree of formulas where leaves are UNSAT, compute interpolants for internal nodes

Implementations

impl TreeInterpolator

pub fn new(config: InterpolationConfig) -> Self

Create a new tree interpolator

pub fn interpolate_tree( &self, nodes: &[TreeNode], ) -> Result<FxHashMap<usize, InterpolantTerm>, InterpolationError>

Compute tree interpolants

Returns an interpolant for each non-leaf node

Trait Implementations

impl Debug for TreeInterpolator

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

Formats the value using the given formatter.

impl Default for TreeInterpolator

fn default() -> Self

Returns the “default value” for a type.