Struct Machine 

pub struct Machine<D: Discretization> { /* private fields */ }

Interval evaluation machine with persistent state and discretization.

A machine is compiled from a list of real-number expressions via MachineBuilder::build, and can then be evaluated at specific input points using Machine::apply. Returns an opaque machine that can be passed to Machine::apply to evaluate the compiled real expression on a specific point.

Internally, a machine converts expressions into a simple register machine. Compilation is fairly slow, so the ideal use case is to compile a function once and then apply it to multiple points.

If more than one expression is provided, common subexpressions will be identified and eliminated during compilation. This makes Rival ideal for evaluating large families of related expressions, a feature that is heavily used in Herbie. Note that each expression can use a different discretization.

Implementations

impl<D: Discretization> Machine<D>

pub fn instruction_count(&self) -> usize

Return the total number of instructions in the compiled machine.

pub fn argument_count(&self) -> usize

Return the number of input arguments expected by this machine.

pub fn target_precision(&self) -> u32

Return the discretization’s target precision in bits.

pub fn min_precision(&self) -> u32

Return the minimum working precision in bits.

pub fn max_precision(&self) -> u32

Return the maximum working precision in bits.

pub fn argument_precision(&self) -> u32

Return the precision used for input arguments.

pub fn set_max_precision(&mut self, bits: u32)

Set the maximum working precision in bits.

pub fn iterations(&self) -> usize

Return the number of iterations needed for the most recent call to Machine::apply.

pub fn bumps(&self) -> usize

Return the number of bumps detected during the most recent call to Machine::apply.

pub fn set_profiling_enabled(&mut self, enabled: bool)

Enable or disable per-instruction profiling.

pub fn profiling_enabled(&self) -> bool

Returns whether per-instruction profiling is enabled.

pub fn execution_records(&self) -> &[Execution]

Return a slice of recorded Execution records from the profiling buffer.

pub fn clear_executions(&mut self)

Reset the profiling buffer, discarding all recorded executions.

pub fn instruction_names(&self) -> Vec<&'static str>

Return the operation name for each instruction in the machine.

pub fn configure_baseline(&mut self)

Reconfigure the machine to use the baseline strategy.

The baseline strategy uses a single global precision for all instructions, doubling it each iteration. This is simpler but less efficient than the default adaptive precision tuning.

pub fn take_executions(&mut self) -> Vec<Execution>

Return a snapshot of recorded Execution records and reset the internal buffer pointer.

impl<D: Discretization> Machine<D>

pub fn apply( &mut self, args: &[Ival], hint: Option<&[Hint]>, max_iterations: usize, ) -> Result<Vec<Ival>, RivalError>

Evaluate the compiled real expressions on an input point represented as a slice of intervals.

args must be the same length as the vars passed to MachineBuilder::build. The output is a vector of output values of the same length as the exprs passed to MachineBuilder::build.

hint can be provided from a previous call to Machine::analyze_with_hints to speed up evaluation. Pass None for default behavior.

max_iterations sets the maximum number of re-evaluation iterations before giving up.

Errors

Returns RivalError::InvalidInput if the point is an invalid input to at least one of the compiled expressions. Returns RivalError::Unsamplable if Rival is unable to evaluate at least one expression.

Note that apply will only return Ok if it can prove that it has correctly-rounded the output. It will only return InvalidInput if it can prove that at least one output expression in the machine throws on the given input.

pub fn apply_baseline( &mut self, args: &[Ival], hint: Option<&[Hint]>, ) -> Result<Vec<Ival>, RivalError>

Evaluate the machine using the baseline strategy.

The baseline strategy uses a single global precision for all instructions, doubling it each iteration. This is simpler but less efficient than Machine::apply, which uses adaptive per-instruction precision tuning.

Call Machine::configure_baseline before using this method to set up the machine for baseline evaluation.

pub fn analyze_baseline_with_hints( &mut self, rect: &[Ival], hint: Option<&[Hint]>, ) -> (Ival, Vec<Hint>, bool)

Analyze an input rectangle using the baseline strategy, returning status, next hints, and a convergence flag.

See Machine::analyze_with_hints for details on the return values.

pub fn analyze_baseline(&mut self, rect: &[Ival]) -> Ival

Analyze a hyper-rectangle using the baseline strategy and return only the boolean interval status.

See Machine::analyze for details on the return value.

pub fn analyze_with_hints( &mut self, rect: &[Ival], hint: Option<&[Hint]>, ) -> (Ival, Vec<Hint>, bool)

Analyze an input rectangle using adaptive precision tuning.

Returns a (status, hints, converged) tuple:

• status is a boolean interval indicating whether a call to Machine::apply with inputs in the supplied rect is guaranteed to raise an error. If false is returned, there is no point calling apply with any point in the input range. If uncertain, some points may raise errors while others may not, though nothing is guaranteed. If true is returned, InvalidInput will not be raised for any point in the range; however, Unsamplable may still be raised.

• hints is a vector of Hints that can be passed to subsequent calls to Machine::apply to skip unnecessary computation.

• converged indicates whether the analysis has converged.

pub fn analyze(&mut self, rect: &[Ival]) -> Ival

Analyze a hyper-rectangle and return only the boolean interval status.

Returns a boolean interval which indicates whether a call to Machine::apply, with inputs in the supplied rect, is guaranteed to raise an error.

In other words, if false is returned, there is no point calling apply with any point in the input range. If uncertain, some points in the range may raise errors, while others may not, though nothing is guaranteed. If true is returned, RivalError::InvalidInput will not be raised for any point in the range. However, RivalError::Unsamplable may still be raised.

The advantage of analyze over apply is that it applies to whole ranges of input points and is much faster.