Function filter_bound 

pub fn filter_bound(
    graph: &DiffGraph,
    file: &str,
    position: Position,
) -> Result<FilterBound, Error>

Derives the error bound of the f64 evaluation of graph.

With u = 2^-53, every node of degree g gets coefficients m, c, alpha and beta such that |true value| <= m * D^g, |computed value| <= c * D^g and |computed - true| <= (alpha * D + beta * E) * D^(g - 1):

• a leaf has g = 1, m = 1 + u, c = 1, alpha = u, beta = 1;
• a negation is exact and keeps the coefficients of its operand;
• the sum or difference of x and y, of equal degree, has m = m_x + m_y, c = (c_x + c_y)(1 + u), alpha = alpha_x + alpha_y + u (c_x + c_y) and beta = beta_x + beta_y;
• the product of x and y has g = g_x + g_y, m = m_x m_y, c = c_x c_y (1 + u), alpha = c_x alpha_y + m_y alpha_x + u c_x c_y and beta = c_x beta_y + m_y beta_x.

The root gives epsilon = alpha and kappa = beta. Every node is analysed once, in the order of the graph, so a shared subexpression counts as the single computation it is.

Errors

Returns an error, at position (the name of the predicate) in file, when the degree is so high that no D > 1 keeps every computed node below 2^1022, or that no D < 1 keeps the bound clear of underflow (see FilterBound::constants), and when the exact coefficients would take more than 2^26 bits in all. The coefficients of a sum are about 53 bits longer than those of its operands, so a sum written as one chain of more than about 1,560 terms reaches that limit; the same terms summed in a balanced tree, with let, need far fewer bits. The size is estimated node by node before any coefficient is computed, so a definition that is too large fails quickly.